update for cedar#1506

Signed-off-by: Craig Disselkoen <cdiss@amazon.com>
cedar-policy · Feb 26, 2025 · 9271f0b · 9271f0b
1 parent 7f3e72a
commit 9271f0b
Show file tree

Hide file tree

Showing 46 changed files with 61 additions and 136 deletions.
diff --git a/cedar-lean/CedarProto/Entities.lean b/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

diff --git a/cedar-lean/CedarProto/Expr.lean b/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 := {

diff --git a/cedar-lean/CedarProto/Request.lean b/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")
 

diff --git a/cedar-lean/UnitTest/CedarProto-test-data/345.protodata b/cedar-lean/UnitTest/CedarProto-test-data/345.protodata
@@ -1,3 +1,2 @@
 
-
 �
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/abac.protodata b/cedar-lean/UnitTest/CedarProto-test-data/abac.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/action.protodata b/cedar-lean/UnitTest/CedarProto-test-data/action.protodata
@@ -1,2 +1 @@
-
-
+
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/app_widget_123.protodata b/cedar-lean/UnitTest/CedarProto-test-data/app_widget_123.protodata
@@ -1,5 +1,4 @@
 
-
 "
 
 WidgetApp123
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/complicated.protodata b/cedar-lean/UnitTest/CedarProto-test-data/complicated.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/contains.protodata b/cedar-lean/UnitTest/CedarProto-test-data/contains.protodata
@@ -1,17 +1,10 @@
-
-BB@+
-)r'
-
+B4#r!
 
 
-
 
 
-
 
 "
 
-Useralice
-R
-
+UseraliceR	
 foo
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/decimal.protodata b/cedar-lean/UnitTest/CedarProto-test-data/decimal.protodata
@@ -1,17 +1,11 @@
+J@
 
-JJH
 
-
-lessThan
-J
+lessThanJ
 
-decimal
-
-
-3.14
-J
+decimal
+3.14J
 
-decimal
-
+decimal
 
 3.1416
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptyrecord.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptyrecord.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptyset.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptystring.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptystring.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata
@@ -2,8 +2,8 @@
 
 
 
-DEF234
+ABC123
 
 
 
-ABC123
+DEF234
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/false.protodata b/cedar-lean/UnitTest/CedarProto-test-data/false.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/has_and_get_tags.protodata b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get_tags.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/ip.protodata b/cedar-lean/UnitTest/CedarProto-test-data/ip.protodata
@@ -1,14 +1,9 @@
-
-MJK
+JC
 
-	isInRange
-J
+	isInRangeJ
 
-ip
-
-192.168.0.1
-J
+ip
+192.168.0.1J
 
-ip
-
+ip
 192.0.0.0/8

diff --git a/cedar-lean/UnitTest/CedarProto-test-data/is.protodata b/cedar-lean/UnitTest/CedarProto-test-data/is.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/like.protodata b/cedar-lean/UnitTest/CedarProto-test-data/like.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_set.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_set.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/not_and_neg.protodata b/cedar-lean/UnitTest/CedarProto-test-data/not_and_neg.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/plus_and_minus_and_times.protodata b/cedar-lean/UnitTest/CedarProto-test-data/plus_and_minus_and_times.protodata
@@ -1,13 +1,5 @@
-
-?B=!
-B
-
- 
-R
-
-count
-B
-
-
-
+B/B
+ R
+countB
+
 

diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset_just_templates.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset_just_templates.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset_one_static_policy.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset_one_static_policy.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/principal_in_resource_owners.protodata b/cedar-lean/UnitTest/CedarProto-test-data/principal_in_resource_owners.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/rbac.protodata b/cedar-lean/UnitTest/CedarProto-test-data/rbac.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/record.protodata
@@ -1,10 +1,7 @@
-
-!z
-
-ham
-
-
-
-eggs
-
-
+z
+
+eggs
+
+
+ham
+
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/request.protodata b/cedar-lean/UnitTest/CedarProto-test-data/request.protodata
@@ -5,9 +5,7 @@
 
 Actionaccess
 
-Folderdata"
-z
-
-foo
-
+Folderdata"z
+
+foo
 
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata
@@ -1,35 +1,23 @@
 
-
-
-B
-
-B 
-
-
-A
+
+
 
 A
-B ?
+B
+
+
+B
 
 
-ActionReadX*
+ActionWrite"
 
 
-ActionReadX":
-AB
-BB
-AA
-
-
-ActionRead-
+ActionReadX*
+A2
+A2
+B%
 
 
 ActionRead
 
-ActionReadX"0
-
-
-ActionWrite
-
-
-ActionWrite"
+ActionReadX
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/set.protodata b/cedar-lean/UnitTest/CedarProto-test-data/set.protodata
@@ -1,9 +1,6 @@
-
-#r!
-
+r
 
 ���������
-
 
 
 minustwo
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/thisiscedar.protodata b/cedar-lean/UnitTest/CedarProto-test-data/thisiscedar.protodata
@@ -1,3 +1,2 @@
 
-
 this is Cedar

diff --git a/cedar-lean/UnitTest/CedarProto-test-data/true.protodata b/cedar-lean/UnitTest/CedarProto-test-data/true.protodata
@@ -1,3 +1,2 @@
 
-
 
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_bool.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_bool.protodata
@@ -1,8 +1,6 @@
 
-
-
-E
+
 
 E
 attr
- 
+
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_ip.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_ip.protodata
@@ -1,10 +1,8 @@
 
-&
-
-E
+
 
 E
 attr
 
-"
-ipaddr 
+*
+ipaddr
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_long.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_long.protodata
@@ -1,8 +1,6 @@
 
-
-
-E
+
 
 E
 attr
- 
+
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_set_of_string.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_set_of_string.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata
diff --git a/cedar-lean/UnitTest/CedarProto-test-data/user_alice.protodata b/cedar-lean/UnitTest/CedarProto-test-data/user_alice.protodata
@@ -1,5 +1,4 @@
 
-
 "
 
 Useralice
-Original file line number
+Diff line change
@@ Expand Up / @@ -2,8 +2,8 @@ @@
-    DEF234
+    ABC123
-    ABC123
+    DEF234