From 9271f0bf4e337413e8d9667871b06622f10b1e2b Mon Sep 17 00:00:00 2001 From: Craig Disselkoen Date: Wed, 26 Feb 2025 20:50:59 +0000 Subject: [PATCH] update for cedar#1506 Signed-off-by: Craig Disselkoen --- cedar-lean/CedarProto/Entities.lean | 18 +++++---- cedar-lean/CedarProto/Expr.lean | 21 +--------- cedar-lean/CedarProto/Request.lean | 2 +- .../CedarProto-test-data/345.protodata | 1 - .../CedarProto-test-data/abac.protodata | Bin 124 -> 108 bytes .../CedarProto-test-data/action.protodata | 3 +- .../app_widget_123.protodata | 1 - .../complicated.protodata | Bin 114 -> 86 bytes .../CedarProto-test-data/contains.protodata | 11 +----- .../CedarProto-test-data/decimal.protodata | 16 +++----- .../emptyrecord.protodata | Bin 4 -> 2 bytes .../CedarProto-test-data/emptyset.protodata | Bin 4 -> 2 bytes .../emptystring.protodata | Bin 6 -> 4 bytes .../CedarProto-test-data/entities.protodata | 4 +- .../CedarProto-test-data/entity.protodata | Bin 141 -> 129 bytes .../CedarProto-test-data/false.protodata | Bin 6 -> 4 bytes .../has_and_get.protodata | Bin 71 -> 57 bytes .../has_and_get_tags.protodata | Bin 87 -> 69 bytes .../CedarProto-test-data/ip.protodata | 15 +++----- .../CedarProto-test-data/is.protodata | Bin 151 -> 125 bytes .../CedarProto-test-data/like.protodata | Bin 78 -> 66 bytes .../nested_record.protodata | Bin 85 -> 71 bytes .../CedarProto-test-data/nested_set.protodata | Bin 65 -> 47 bytes .../not_and_neg.protodata | Bin 72 -> 52 bytes .../plus_and_minus_and_times.protodata | 16 ++------ .../CedarProto-test-data/policyset.protodata | Bin 571 -> 528 bytes .../policyset_just_templates.protodata | Bin 48 -> 46 bytes .../policyset_one_static_policy.protodata | Bin 28 -> 26 bytes .../principal_in_resource_owners.protodata | Bin 32 -> 24 bytes .../CedarProto-test-data/rbac.protodata | Bin 100 -> 98 bytes .../CedarProto-test-data/record.protodata | 17 ++++----- .../CedarProto-test-data/request.protodata | 8 ++-- .../schema_attrs.protodata | Bin 547 -> 409 bytes .../schema_basic.protodata | 36 ++++++------------ .../schema_commontypes.protodata | Bin 256 -> 177 bytes .../schema_tags.protodata | Bin 151 -> 95 bytes .../CedarProto-test-data/set.protodata | 5 +-- .../thisiscedar.protodata | 1 - .../CedarProto-test-data/true.protodata | 1 - .../CedarProto-test-data/type_bool.protodata | 6 +-- .../CedarProto-test-data/type_ip.protodata | 8 ++-- .../CedarProto-test-data/type_long.protodata | 6 +-- .../type_record.protodata | Bin 65 -> 52 bytes .../type_set_of_string.protodata | Bin 34 -> 25 bytes .../type_string.protodata | Bin 32 -> 23 bytes .../CedarProto-test-data/user_alice.protodata | 1 - 46 files changed, 61 insertions(+), 136 deletions(-) diff --git a/cedar-lean/CedarProto/Entities.lean b/cedar-lean/CedarProto/Entities.lean index 5ed9a4e55..af1e74407 100644 --- 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 index b0a131e17..8dce44f01 100644 --- 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 index 68c522e1e..ae352c26b 100644 --- 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 index 29aa9d1f6..50825947e 100644 --- a/cedar-lean/UnitTest/CedarProto-test-data/345.protodata +++ b/cedar-lean/UnitTest/CedarProto-test-data/345.protodata @@ -1,3 +1,2 @@ -  \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/abac.protodata b/cedar-lean/UnitTest/CedarProto-test-data/abac.protodata index 9aecfdac3d53537bfb381cac32746e7374c9e3dc..42008102b467f5f534c645a126e0d64e9fc34b70 100644 GIT binary patch delta 57 zcmb=);pGb9VlT+g$xN;^5b~VJE1_hdrN<@eBrL=vz#zpN#LdMdz$C<)U!Ip*BqVAj MEF>7jKQUYt0A6nkVE_OC delta 73 zcmd0);pIxIu literal 6 Ncmd;L;bM|v0002E05t#r diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata index 2d3ae0f96..db32d48d4 100644 --- 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 \ No newline at end of file +DEF234 \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata index 28187f7237fdd0b869fbda405c1ced20b8b7cf2e..ea255c8805ece2f0593ec96de58ae2ef2e957336 100644 GIT binary patch delta 102 zcmeBWY-F_J;^t!GVssK>bQEHA7UJe&PD(5iV&P)qU=WhyVouA?7ZNWL<>KYy7WfYX mj9fr@0mg|=D#`*}EG3EQMnW81Y*H*`i8)3}5D`PTh#>%Hx))3U delta 114 zcmZo<>}7P~;^t!GVssK>bQEHA7EDVDOt93v%&m?4swApnqf7wiB4 diff --git a/cedar-lean/UnitTest/CedarProto-test-data/false.protodata b/cedar-lean/UnitTest/CedarProto-test-data/false.protodata index c08daef2ea7aec1139740f0b297852a2ae7409d0..35e768746b28650503df11e49fa714fca48ea651 100644 GIT binary patch literal 4 Lcmd;L;$Q#(073v2 literal 6 Ncmd;L;bP)o0001#03!eZ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata index 3686cc0f15fc44fe6e60de41c1e68280a52c50fe..082ffefadf3349b7c8ae602355bba2cb224f362c 100644 GIT binary patch literal 57 xcmdNg=Mst%;9?SB5aLQnEl4aX$xY2G5mI!L7ZM7>5SQZQVwYkKPRvOy1^`<;4J7~o literal 71 zcmd;b)pF(%;}VGy;$q=q5?~PGN=Yq9EGo%O%_|YoHd;W(}sttc*aF4Zh$E+H;~AU-aZiPka(Kow5f l9Be{RAuc8XCLy-+%#`%h5-DLW!61Gv7N8h|5IaPy7yt(T5SIV| diff --git a/cedar-lean/UnitTest/CedarProto-test-data/like.protodata b/cedar-lean/UnitTest/CedarProto-test-data/like.protodata index 45922a5266bafc1da4d17016b83b8e75333a91b8..2c3222bf94fbe5e0879f17f0c9c6a39019e42bf5 100644 GIT binary patch delta 24 fcmeZs5=wI5k_(dI5)TsP5(whs;tXP+C}#iwHKzn9 delta 36 rcmZ?rljHJ9^5W9qQVUYylIM~QlI9ZQ5(yIG;^pEF;^bnPC}aQtYVQS5 diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata index 4780bf0037a510147893f0220c10e6e9defcb319..cb65965f8ba5cc6de0424e9db086dd2f13bd20cb 100644 GIT binary patch literal 71 zcmb<&<&x)O&PdD^lBg2n;^bmX5@O+E;$Q$V6G2P?1}-Homeln0Vj-y_2`+9fPAT@1 UjLc$%%wnJ#b}80Gh2qo_0D!RzpO1unTF e87^L+B&QU6Nk(R|LS`|D!^JMeny65mS^@wD>D*i;bP%p5?}(zH?+Qsq*1QWO&B615WMU_@1v MlvpIi2G+q005Wz5@&Et; 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 index 0854d25ed..72a7ed72b 100644 --- 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 +  \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata index 246a7d55f645ff7e82d5c7f40c843f45d8c424cf..6ee4624c65a80f62e5546316e13ecb879d3645c0 100644 GIT binary patch delta 246 zcmdnZGJ%DcE1!$KAU`KFxza!=W#T()GYuy-A#o>B4i+KqAWkkO0cIiQwETQ279f*d z3NDnCSi}_$(`hK=GdY)0msu`IX7WNt8D1`Ln2fQI!$e*gLuD&PA$ccR4kjVtAVHu( zOhVkLIhpC1NtrpBC6!>anYb!pnv8_* k#055qrKGYTb@ENX~M}X!u?t8EOA6cAyRxRK|heafI4%cWZCxFYrts zEfX){B58vOWiW{5<-*TJKpJr1*0PJ0#CpNtC#MfEQ8I<K^BOPh+P=ns9`NAf3=K z_OUGHJetubc%XL5r){ew({;DH!5El2%6yw-Cm~(Jd(Ir;W5%&wJqJttjKnH3ek3QLS``p;i4~%dp Wai;Y)=F`hy*^^&`6&$k2E92sPNmpX1$M>Fi>yz0Bsl z%+AdF@I{z{$|M9Sp23+@Oh!Cg;fRPpH3#q#>B~jOAk86swoW0=3iQGekj*h`-&I`? zVg{g!T^Tq@wxEXZut~4M@b;g*9*zUcn6QAWo94qdJGj8~RdsgzB$i{~nFEXQ$$5n( zWKCWj+I`R7ZfFmhuMqz;-AAqJF z_#=WMeJ}v-ahq-sj>npqgy=Vip(x<6hTo}PHK()!OQs3H>I6`bW`?XO#m%vlKkF_y A4*&oF literal 547 zcmZut%Sr=55TuiRB()}vt#}wOVef($2{DN5=ofg=>$tnF3vMDY;AaSeU*XXY@GJZu zdv>!LNf_v%i|*>G!Y82%y5x`M*AeKB19W4Vam($@^i zd4N8z7>uG3Vdz9B9M)gko2EA-;%~wpM0Aoa%lVA`>)d9y{Iv~@-$}m_zdBN}-fyKE z$mw+bw8#`oB77H7EOS|&mX&=J^va36z*J9oj6;N#o!MgDx2P8SCaP7qh?=lma^hJA yej||V6rDMTt{CHjbH#81wPwq6w)l7x)0^hwKzrO##3%ogxmlFUoR7AE?Zyu`t4<;S diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata index 160056a77..afec18049 100644 --- 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" \ No newline at end of file +ActionReadX \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata index 8b8da158308891c14ce24270a8f6cca886d931da..22797b11b164c47baebf3a7eb51ef1403ea8a773 100644 GIT binary patch literal 177 zcmd<$;$r4vbP@s*Zd@uLwwn|;7h{zW8y6D?g8-wH02gDW5H}a65W5ho6j0ik3#`Kt zqJtHr!&xYcOMr`mi_I~)Br`uxh$SdBF+~Zg5vEOmQOT5xF;U2XOHWCMOCDsZ6qlHi k2$v8Sb6S2r&23@n8rp6Kf*6|HxWc+VD3CG z2Lm`zIlHZxx=a=3wktVnL}I81eRM)EQ9`IYdx#k^5KqiqVIKPSvS84N=^Izwx@xwr zd?_Rd;p@ZgQeWwAPSugm|Jh_OJ8rRts+eIVOD+&u2G=rRY6((|ML5C`&bh7)&=)6B RZQz6YyU7fUwkgjo@*AGq9EAV? diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata index e03fdf2c5364c684cd1126d2496154df845dbab4..398636559fa38b85004fb9db9a636ee46edbd23f 100644 GIT binary patch literal 95 zcmd<$<6`Dwbk$-PVwD0i9J%;Gd?z6w;RYgHxVS+AE?O)?OdJec5+IJ76fYNJl@JFP WSWJLX3naq{l5qwzxj;-uun_<=KL$wv literal 151 zcmXYqK@vbP3`HmCsL&Zc3%aVUTNLe~oL&=FFL_CR7+f=5=oNvE${Jpzx#1MWH4wW> vdt&-f>I_*6#Ji{rukeoPfn_}!>5trGmZ0BKaUEK3d~uOy8AS{qBq`7f35*JG diff --git a/cedar-lean/UnitTest/CedarProto-test-data/set.protodata b/cedar-lean/UnitTest/CedarProto-test-data/set.protodata index b1eb76279..1ba57d757 100644 --- 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 \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/thisiscedar.protodata b/cedar-lean/UnitTest/CedarProto-test-data/thisiscedar.protodata index 0bf077759..32ad9a9e5 100644 --- 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 \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/true.protodata b/cedar-lean/UnitTest/CedarProto-test-data/true.protodata index f1576131e..9553a942d 100644 --- a/cedar-lean/UnitTest/CedarProto-test-data/true.protodata +++ b/cedar-lean/UnitTest/CedarProto-test-data/true.protodata @@ -1,3 +1,2 @@ -  \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_bool.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_bool.protodata index 0998f11e3..410d410f9 100644 --- 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 -  \ No newline at end of file + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_ip.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_ip.protodata index 7b69d5323..98adde79c 100644 --- 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  \ No newline at end of file +* +ipaddr \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_long.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_long.protodata index 1df272a58..b6514a7b9 100644 --- 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 -  \ No newline at end of file + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata index cab92bbd489e809cc005553ac76d2ed1a08f9c03..2e5fb324585335ed8e35b723d29cf9788529f08c 100644 GIT binary patch literal 52 zcmd-w;$r4vbd}QPVo5A1DH2lVl2?-D;^kt_NX!*t<6`1q5Mbou;bKWmPcIf?0rHsy F7y-fn2IBw# literal 65 zcmd 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 index 39ec5f9622b7d59dc4b01b433d4ca70c680f584b..96374bd4a4c3a90a46b9eb3750acd034c3bd55ed 100644 GIT binary patch literal 25 gcmd-Q=VIn!bd?g|Vo5A1DH7t~Vi98EU=Uyg042`?#{d8T literal 34 lcmd;5;9}-tbQO{WQ&Iw4EQuv0MM4~0EJ92itOAS*i~u~a1AYJi diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata index 1499c6e31036f90147c3d9008fa5ca4e656edca3..b48c92d40114e3d1deacc685a3b13e52e59a9608 100644 GIT binary patch literal 23 ecmd-Q