update for 1495

cedar-lean/Cedar/Validation/Types.lean

@@ -26,6 +26,7 @@ inductive BoolType where
   | anyBool
   | tt
   | ff
+deriving Repr
 
 def BoolType.not : BoolType → BoolType
   | .anyBool => .anyBool
@@ -35,19 +36,33 @@ def BoolType.not : BoolType → BoolType
 inductive ExtType where
   | ipAddr
   | decimal
+deriving Repr
 
 inductive Qualified (α : Type u) where
   | optional (a : α)
   | required (a : α)
+deriving Repr
 
-def Qualified.getType {α} : Qualified α → α
+namespace Qualified
+
+instance [Inhabited α] : Inhabited (Qualified α) where
+  default := .required default
+
+def getType {α} : Qualified α → α
   | optional a => a
   | required a => a
 
-def Qualified.isRequired {α} : Qualified α → Bool
+def isRequired {α} : Qualified α → Bool
   | optional _ => false
   | required _ => true
 
+-- effectively making Qualified a functor
+def map {α β} (f : α → β) : Qualified α → Qualified β
+  | optional a => optional (f a)
+  | required a => required (f a)
+
+end Qualified
+
 inductive CedarType where
   | bool (bty : BoolType)
   | int
@@ -56,6 +71,10 @@ inductive CedarType where
   | set (ty : CedarType)
   | record (rty : Map Attr (Qualified CedarType))
   | ext (xty : ExtType)
+deriving Repr
+
+instance : Inhabited CedarType where
+  default := .int
 
 abbrev QualifiedType := Qualified CedarType
 
@@ -120,6 +139,7 @@ structure ActionSchemaEntry where
   appliesToResource : Set EntityType
   ancestors : Set EntityUID
   context : RecordType
+deriving Repr, Inhabited
 
 abbrev ActionSchema := Map EntityUID ActionSchemaEntry
 

cedar-lean/CedarProto/ActionDecl.lean

@@ -33,12 +33,10 @@ namespace Cedar.Validation.Proto
 structure ActionDecl where
   name : Spec.EntityUID
   descendants : Array Spec.EntityUID
-  context : CedarType
+  context : Proto.Map String (Qualified ProtoType)
   principal_types : Array Spec.Name
   resource_types : Array Spec.Name
-
-instance : Inhabited ActionDecl where
-  default := ActionDecl.mk default default (CedarType.record default) default default
+deriving Repr, Inhabited
 
 namespace ActionDecl
 
@@ -55,7 +53,7 @@ def mergeDescendants (result : ActionDecl) (x : Array Spec.EntityUID) : ActionDe
   }
 
 @[inline]
-def mergeContext (result : ActionDecl) (x : CedarType) : ActionDecl :=
+def mergeContext (result : ActionDecl) (x : Proto.Map String (Qualified ProtoType)) : ActionDecl :=
   {result with
     context := Field.merge result.context x
   }
@@ -92,12 +90,12 @@ def parseField (t : Tag) : BParsec (MergeFn ActionDecl) := do
       let x : Repeated Spec.EntityUID ← Field.guardedParse t
       pure (pure $ mergeDescendants · x)
     | 4 =>
-      let x : CedarType ← Field.guardedParse t
+      let x : Proto.Map String (Qualified ProtoType) ← Field.guardedParse t
       pure (pure $ mergeContext · x)
-    | 7 =>
+    | 5 =>
       let x : Repeated Spec.Name ← Field.guardedParse t
       pure (pure $ mergePrincipalTypes · x)
-    | 8 =>
+    | 6 =>
       let x : Repeated Spec.Name ← Field.guardedParse t
       pure (pure $ mergeResourceTypes · x)
     | _ =>

cedar-lean/CedarProto/EntityDecl.lean

@@ -28,12 +28,13 @@ namespace Cedar.Validation.Proto
 -- Note: EntitySchemaEntry takes ancestors, so we'll create this intermediate
 -- representation. Once we gather all the entries, we will perform the transform.
 structure EntityDecl where
+  name : Spec.Name
   /-- All (transitive) descendants. Assumes TC is computed before encoding into protobuf. -/
   descendants : Array Spec.Name
-  attrs : Proto.Map String QualifiedType
-  tags : Option CedarType
-  enums: Array String
-deriving Inhabited
+  attrs : Proto.Map String (Qualified ProtoType)
+  tags : Option ProtoType
+  enums : Array String
+deriving Repr, Inhabited
 
 namespace EntityDecl
 
@@ -45,20 +46,26 @@ def mergeOption [Field α] (x1 x2 : Option α) : Option α :=
   | some x, none => some x
   | none, none => none
 
+@[inline]
+def mergeName (result : EntityDecl) (x : Spec.Name) : EntityDecl :=
+  {result with
+    name := Field.merge result.name x
+  }
+
 @[inline]
 def mergeDescendants (result : EntityDecl) (x : Array Spec.Name) : EntityDecl :=
   {result with
     descendants := result.descendants ++ x
   }
 
 @[inline]
-def mergeAttributes (result : EntityDecl) (x : Proto.Map String QualifiedType) : EntityDecl :=
+def mergeAttributes (result : EntityDecl) (x : Proto.Map String (Qualified ProtoType)) : EntityDecl :=
   {result with
     attrs := result.attrs ++ x
   }
 
 @[inline]
-def mergeTags (result : EntityDecl) (x : CedarType) : EntityDecl :=
+def mergeTags (result : EntityDecl) (x : ProtoType) : EntityDecl :=
   {result with
     tags := mergeOption result.tags (some x)
   }
@@ -72,6 +79,7 @@ def mergeEnums (result : EntityDecl) (x : Array String) : EntityDecl :=
 @[inline]
 def merge (x y : EntityDecl) : EntityDecl :=
   {
+    name := Field.merge x.name y.name
     descendants := y.descendants ++ x.descendants
     attrs := x.attrs ++ y.attrs
     tags := mergeOption x.tags y.tags
@@ -81,14 +89,17 @@ def merge (x y : EntityDecl) : EntityDecl :=
 @[inline]
 def parseField (t : Tag) : BParsec (MergeFn EntityDecl) := do
   match t.fieldNum with
+    | 1 =>
+      let x : Spec.Name ← Field.guardedParse t
+      pure (pure $ mergeName · x)
     | 2 =>
       let x : Repeated Spec.Name ← Field.guardedParse t
       pure (pure $ mergeDescendants · x)
     | 3 =>
-      let x : Proto.Map String QualifiedType ← Field.guardedParse t
+      let x : Proto.Map String (Qualified ProtoType) ← Field.guardedParse t
       pure (pure $ mergeAttributes · x)
     | 5 =>
-      let x : CedarType ← Field.guardedParse t
+      let x : ProtoType ← Field.guardedParse t
       pure (pure $ mergeTags · x)
     | 6 =>
       let x : Repeated String ← Field.guardedParse t

cedar-lean/CedarProto/Schema.lean

@@ -25,16 +25,10 @@ open Proto
 
 namespace Cedar.Validation.Proto
 
-def EntityTypeToEntityDeclMap := Proto.Map Spec.Name EntityDecl
-  deriving Inhabited, Field
-
-def EntityUidToActionDeclMap := Proto.Map Spec.EntityUID ActionDecl
-  deriving Inhabited, Field
-
 structure Schema where
-  ets : EntityTypeToEntityDeclMap
-  acts : EntityUidToActionDeclMap
-deriving Inhabited
+  ets : Array EntityDecl
+  acts : Array ActionDecl
+deriving Repr, Inhabited
 
 /-
 The Rust data types store _descendant_ information for the entity type store
@@ -45,88 +39,71 @@ The definitions and utility functions below are used to convert the descendant
 representation to the ancestor representation.
 -/
 @[inline]
-private def findInMapValues [LT α] [DecidableEq α] [DecidableLT α] (m : Data.Map α (Data.Set α)) (k₁ : α) : Data.Set α :=
-  let setOfSets := List.map (λ (k₂,v) => if v.contains k₁ then Data.Set.singleton k₂ else Data.Set.empty) m.toList
-  setOfSets.foldl (λ acc v => acc.union v) Data.Set.empty
+private def findInMapValues [LT α] [DecidableEq α] [DecidableLT α] (m : List (α × (Data.Set α))) (k₁ : α) : Data.Set α :=
+  let setOfSets := m.map λ (k₂,v) => if v.contains k₁ then Data.Set.singleton k₂ else Data.Set.empty
+  setOfSets.foldl Data.Set.union Data.Set.empty
 
 @[inline]
-private def descendantsToAncestors [LT α] [DecidableEq α] [DecidableLT α] (descendants : Data.Map α (Data.Set α)) : Data.Map α (Data.Set α) :=
-  Data.Map.make (List.map
-    (λ (k,_) => (k, findInMapValues descendants k)) descendants.toList)
+private def descendantsToAncestors [LT α] [DecidableEq α] [DecidableLT α] (descendants : List (α × (Data.Set α))) : Data.Map α (Data.Set α) :=
+  Data.Map.make (descendants.map λ (k,_) => (k, findInMapValues descendants k))
 
-end Cedar.Validation.Proto
+namespace Schema
 
-namespace Cedar.Validation.Proto.EntityTypeToEntityDeclMap
-@[inline]
-def toEntitySchema (ets : EntityTypeToEntityDeclMap) : EntitySchema :=
-  let ets := ets.toList
-  let descendantMap := Data.Map.make $
-    ets.map λ (k,v) => (k, Data.Set.mk v.descendants.toList)
+def toSchema (schema : Schema) : Validation.Schema :=
+  let ets := schema.ets.toList
+  let descendantMap := ets.map λ decl => (decl.name, Data.Set.make decl.descendants.toList)
   let ancestorMap := descendantsToAncestors descendantMap
-  Data.Map.make $ ets.map λ (k,v) =>
-    (k,
-      if v.enums.isEmpty then
+  let ets := Data.Map.make $ ets.map λ decl =>
+    (decl.name,
+      if decl.enums.isEmpty then
       .standard {
-        ancestors := ancestorMap.find! k
-        attrs := Data.Map.make v.attrs.toList
-        tags := v.tags
+        ancestors := ancestorMap.find! decl.name
+        attrs := Data.Map.make $ decl.attrs.toList.map λ (k,v) => (k, v.map ProtoType.toCedarType)
+        tags := decl.tags.map ProtoType.toCedarType
       }
       else
-      .enum $ Cedar.Data.Set.mk v.enums.toList
+      .enum $ Cedar.Data.Set.make decl.enums.toList
     )
-end Cedar.Validation.Proto.EntityTypeToEntityDeclMap
-
-namespace Cedar.Validation.Proto.EntityUidToActionDeclMap
--- Needed for panic
-deriving instance Inhabited for ActionSchemaEntry
-
-@[inline]
-def toActionSchema (acts : EntityUidToActionDeclMap) : ActionSchema :=
-  let acts := acts.toList
-  let descendantMap := Data.Map.make $
-    acts.map λ (k,v) => (k, Data.Set.make v.descendants.toList)
+  let acts := schema.acts.toList
+  let descendantMap := acts.map λ decl => (decl.name, Data.Set.make decl.descendants.toList)
   let ancestorMap := descendantsToAncestors descendantMap
-  Data.Map.make $ acts.map λ (k,v) =>
-    match v.context with
-      | .record rty =>
-        (k, {
-          appliesToPrincipal := Data.Set.make v.principal_types.toList,
-          appliesToResource := Data.Set.make v.resource_types.toList,
-          ancestors := ancestorMap.find! k,
-          context := rty
-        })
-      | _ => panic!("EntityUidWithActionsIdMap.toActionSchema : context should be record-typed")
-end Cedar.Validation.Proto.EntityUidToActionDeclMap
-
-namespace Cedar.Validation.Proto.Schema
+  let acts := Data.Map.make $ acts.map λ decl =>
+    (decl.name, {
+      appliesToPrincipal := Data.Set.make decl.principal_types.toList
+      appliesToResource := Data.Set.make decl.resource_types.toList
+      ancestors := ancestorMap.find! decl.name
+      context := Data.Map.make $ decl.context.toList.map λ (k,v) => (k, v.map ProtoType.toCedarType)
+    })
+  { ets, acts }
+
 @[inline]
-def mergeEntityTypes (result : Schema) (x : EntityTypeToEntityDeclMap) : Schema :=
+def mergeEntityDecls (result : Schema) (x : Array EntityDecl) : Schema :=
   {result with
-    ets := Field.merge result.ets x
+    ets := result.ets ++ x
   }
 
 @[inline]
-def mergeActionIds (result : Schema) (x : EntityUidToActionDeclMap) : Schema :=
+def mergeActionDecls (result : Schema) (x : Array ActionDecl) : Schema :=
   {result with
-    acts := Field.merge result.acts x
+    acts := result.acts ++ x
   }
 
 @[inline]
 def merge (x y : Schema) : Schema :=
   {
-    ets := Field.merge x.ets y.ets
-    acts := Field.merge x.acts y.acts
+    ets := x.ets ++ y.ets
+    acts := x.acts ++ y.acts
   }
 
 @[inline]
 def parseField (t : Tag) : BParsec (MergeFn Schema) := do
   match t.fieldNum with
     | 1 =>
-      let x : EntityTypeToEntityDeclMap ← Field.guardedParse t
-      pure (pure $ mergeEntityTypes · x)
+      let x : Repeated EntityDecl ← Field.guardedParse t
+      pure (pure $ mergeEntityDecls · x)
     | 2 =>
-      let x : EntityUidToActionDeclMap ← Field.guardedParse t
-      pure (pure $ mergeActionIds · x)
+      let x : Repeated ActionDecl ← Field.guardedParse t
+      pure (pure $ mergeActionDecls · x)
     | _ =>
       t.wireType.skip
       pure ignore
@@ -136,10 +113,6 @@ instance : Message Schema := {
   merge := merge
 }
 
-@[inline]
-def toSchema (v : Schema) : Validation.Schema :=
-  .mk v.ets.toEntitySchema v.acts.toActionSchema
-
 end Cedar.Validation.Proto.Schema
 
 
@@ -152,16 +125,12 @@ namespace Cedar.Validation.Schema
 
 @[inline]
 private def ES.merge (x1 x2 : EntitySchema) : EntitySchema :=
-  have x1 : Data.Map Spec.EntityType EntitySchemaEntry := x1
-  have x2 : Data.Map Spec.EntityType EntitySchemaEntry := x2
   match x1.kvs with
     | [] => x2
     | _ => Data.Map.make (x2.kvs ++ x1.kvs)
 
 @[inline]
 private def AS.merge (x1 x2 : ActionSchema) : ActionSchema :=
-  have x1 : Data.Map Spec.EntityUID ActionSchemaEntry := x1
-  have x2 : Data.Map Spec.EntityUID ActionSchemaEntry := x2
   match x1.kvs with
     | [] => x2
     | _ => Data.Map.make (x2.kvs ++ x1.kvs)