Merge remote-tracking branch 'origin/main' into feature/shaobo/tpe-ex…

…perimental

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

@@ -24,6 +24,13 @@ import CedarProto.Type
 
 open Proto
 
+macro "update " f:Lean.Parser.Term.structInstLVal : term => `(λ x v => { x with $f := v })
+
+def parseFieldElement {α β} [Field β] (t : Tag) (f : α → β) (g : α → β → α) : BParsec (MergeFn α) := do
+  let x : β ← Field.guardedParse t
+  let merge result x := g result (Field.merge (f result) x)
+  pure (pure $ merge · x)
+
 namespace Cedar.Validation.Proto
 
 -- Note: EntitySchemaEntry takes ancestors,
@@ -32,80 +39,34 @@ namespace Cedar.Validation.Proto
 -- the transform
 structure ActionDecl where
   name : Spec.EntityUID
-  descendants : Array Spec.EntityUID
-  context : CedarType
-  principal_types : Array Spec.Name
-  resource_types : Array Spec.Name
-
-instance : Inhabited ActionDecl where
-  default := ActionDecl.mk default default (CedarType.record default) default default
+  descendants : Repeated Spec.EntityUID
+  context : Proto.Map String (Qualified ProtoType)
+  principalTypes : Repeated Spec.Name
+  resourceTypes : Repeated Spec.Name
+deriving Repr, Inhabited
 
 namespace ActionDecl
 
-@[inline]
-def mergeName (result : ActionDecl) (x : Spec.EntityUID) : ActionDecl :=
-  {result with
-    name := Field.merge result.name x
-  }
-
-@[inline]
-def mergeDescendants (result : ActionDecl) (x : Array Spec.EntityUID) : ActionDecl :=
-  {result with
-    descendants := result.descendants ++ x
-  }
-
-@[inline]
-def mergeContext (result : ActionDecl) (x : CedarType) : ActionDecl :=
-  {result with
-    context := Field.merge result.context x
-  }
-
-@[inline]
-def mergePrincipalTypes (result : ActionDecl) (x : Array Spec.Name) : ActionDecl :=
-  {result with
-    principal_types := result.principal_types ++ x
-  }
-
-@[inline]
-def mergeResourceTypes (result : ActionDecl) (x : Array Spec.Name) : ActionDecl :=
-  {result with
-    resource_types := result.resource_types ++ x
-  }
-
 @[inline]
 def merge (x y : ActionDecl) : ActionDecl :=
   {
-    name := Field.merge x.name y.name
-    descendants := x.descendants ++ y.descendants
-    context := Field.merge x.context y.context
-    principal_types := x.principal_types ++ y.principal_types
-    resource_types := x.resource_types ++ y.resource_types
+    name           := Field.merge x.name           y.name
+    descendants    := Field.merge x.descendants    y.descendants
+    context        := Field.merge x.context        y.context
+    principalTypes := Field.merge x.principalTypes y.principalTypes
+    resourceTypes  := Field.merge x.resourceTypes  y.resourceTypes
   }
 
-@[inline]
-def parseField (t : Tag) : BParsec (MergeFn ActionDecl) := do
-  match t.fieldNum with
-    | 1 =>
-      let x : Spec.EntityUID ← Field.guardedParse t
-      pure (pure $ mergeName · x)
-    | 3 =>
-      let x : Repeated Spec.EntityUID ← Field.guardedParse t
-      pure (pure $ mergeDescendants · x)
-    | 4 =>
-      let x : CedarType ← Field.guardedParse t
-      pure (pure $ mergeContext · x)
-    | 7 =>
-      let x : Repeated Spec.Name ← Field.guardedParse t
-      pure (pure $ mergePrincipalTypes · x)
-    | 8 =>
-      let x : Repeated Spec.Name ← Field.guardedParse t
-      pure (pure $ mergeResourceTypes · x)
-    | _ =>
-      t.wireType.skip
-      pure ignore
-
 instance : Message ActionDecl := {
-  parseField := parseField
+  parseField (t : Tag) := do
+    match t.fieldNum with
+      | 1 => parseFieldElement t name (update name)
+      | 3 => parseFieldElement t descendants (update descendants)
+      | 4 => parseFieldElement t context (update context)
+      | 5 => parseFieldElement t principalTypes (update principalTypes)
+      | 6 => parseFieldElement t resourceTypes (update resourceTypes)
+      | _ => let _ ← t.wireType.skip ; pure ignore
+
   merge := merge
 }
 

cedar-lean/CedarProto/Entities.lean

@@ -31,19 +31,24 @@ namespace Cedar.Spec
 
 def EntitiesProto : Type := Array EntityProto
 deriving instance Inhabited for EntitiesProto
+instance : HAppend EntitiesProto EntitiesProto EntitiesProto where
+  hAppend x y :=
+    let x : Array EntityProto := x
+    let y : Array EntityProto := y
+    x ++ y
+instance : HAppend EntitiesProto (Array EntityProto) EntitiesProto where
+  hAppend x y :=
+    let x : Array EntityProto := x
+    x ++ y
 
 namespace EntitiesProto
 
 @[inline]
-def mergeEntities (result : EntitiesProto) (x : Repeated EntityProto) : EntitiesProto :=
-  have x : Array EntityProto := x.map λ xi => { xi with data := xi.data.mkWf }
-  have result : Array EntityProto := result
+def mergeEntities (result : EntitiesProto) (x : Array EntityProto) : EntitiesProto :=
   result ++ x
 
 @[inline]
 def merge (x : EntitiesProto) (y : EntitiesProto) : EntitiesProto :=
-  have x : Array EntityProto := x
-  have y : Array EntityProto := y
   x ++ y
 
 @[inline]
@@ -52,7 +57,6 @@ def parseField (t : Proto.Tag) : BParsec (MergeFn EntitiesProto) := do
     | 1 =>
       let x : Repeated EntityProto ← Field.guardedParse t
       pure (pure $ mergeEntities · x)
-    -- Ignoring 3 | mode
     | _ =>
       t.wireType.skip
       pure ignore
@@ -71,8 +75,6 @@ end EntitiesProto
 namespace Entities
 @[inline]
 def merge (e1 : Entities) (e2 : Entities) : Entities :=
-  let e1 : Cedar.Data.Map EntityUID EntityData := e1
-  let e2 : Cedar.Data.Map EntityUID EntityData := e2
   -- Don't sort if e1 is empty
   match e1.kvs with
     | [] => e2

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/Expr.lean

@@ -729,14 +729,6 @@ def merge (x1 x2 : ExprKind) : ExprKind :=
 -- end of this file
 end Proto.ExprKind
 
-namespace Expr
--- There's one additinoal message wrapped around ExprKind
--- that we need to parse
-@[inline]
-def mergeExprKind (x1 : Expr) (x2 : Proto.ExprKind) : Expr :=
-  Expr.merge x1 x2
-end Expr
-
 -- Expr depends on ExprKind and ExprKind is a sum type
 -- where many of the constructors depend on Expr
 mutual
@@ -897,7 +889,7 @@ partial def Proto.ExprKind.Record.parseField (t : Proto.Tag) : BParsec (MergeFn
       t.wireType.skip
       pure ignore
 
-partial def Proto.ExprKind.parseField (t : Proto.Tag) : BParsec (MergeFn Proto.ExprKind) := do
+partial def Expr.parseField (t : Proto.Tag) : BParsec (MergeFn Expr) := do
   have : Message Proto.ExprKind.If := { parseField := Proto.ExprKind.If.parseField, merge := Proto.ExprKind.If.merge }
   have : Message Proto.ExprKind.And := { parseField := Proto.ExprKind.And.parseField, merge := Proto.ExprKind.And.merge }
   have : Message Proto.ExprKind.Or := { parseField := Proto.ExprKind.Or.parseField, merge := Proto.ExprKind.Or.merge }
@@ -911,7 +903,6 @@ partial def Proto.ExprKind.parseField (t : Proto.Tag) : BParsec (MergeFn Proto.E
   have : Message Proto.ExprKind.Set := { parseField := Proto.ExprKind.Set.parseField, merge := Proto.ExprKind.Set.merge }
   have : Message Proto.ExprKind.Record := { parseField := Proto.ExprKind.Record.parseField, merge := Proto.ExprKind.Record.merge }
 
-
   match t.fieldNum with
     | 1 =>
       let x : Prim ← Field.guardedParse t
@@ -959,16 +950,6 @@ partial def Proto.ExprKind.parseField (t : Proto.Tag) : BParsec (MergeFn Proto.E
       t.wireType.skip
       pure ignore
 
-partial def Expr.parseField (t : Proto.Tag) : BParsec (MergeFn Expr) := do
-  have : Message Proto.ExprKind := { parseField := Proto.ExprKind.parseField, merge := Proto.ExprKind.merge }
-  match t.fieldNum with
-    | 1 =>
-      let x : Proto.ExprKind ← Field.guardedParse t
-      pure (pure $ Expr.mergeExprKind · x)
-    | _ =>
-      t.wireType.skip
-      pure ignore
-
 end
 
 instance : Message Expr := {

cedar-lean/CedarProto/Request.lean

@@ -58,7 +58,7 @@ def mergeContext (result : Request) (x : Value) : Request :=
   match x with
   | .record pairs =>
     {result with
-      context := Data.Map.mk (result.context.kvs ++ pairs.kvs)
+      context := Data.Map.make (result.context.kvs ++ pairs.kvs)
     }
   | _ => panic!("Context is not of correct type")