From fb56deac5957b03fe595026b2efbc9f873f59f36 Mon Sep 17 00:00:00 2001 From: Craig Disselkoen Date: Wed, 26 Feb 2025 13:23:33 -0800 Subject: [PATCH 1/3] update for 1495 (#553) Signed-off-by: Craig Disselkoen --- cedar-lean/Cedar/Validation/Types.lean | 24 +- cedar-lean/CedarProto/ActionDecl.lean | 14 +- cedar-lean/CedarProto/EntityDecl.lean | 27 +- cedar-lean/CedarProto/Schema.lean | 111 ++--- cedar-lean/CedarProto/Type.lean | 412 ++++++------------ .../CedarProto-test-data/entities.protodata | 4 +- .../CedarProto-test-data/entity.protodata | Bin 141 -> 141 bytes .../CedarProto-test-data/policyset.protodata | Bin 571 -> 571 bytes .../schema_attrs.protodata | Bin 547 -> 409 bytes .../schema_basic.protodata | 34 +- .../schema_commontypes.protodata | Bin 256 -> 177 bytes .../schema_tags.protodata | Bin 151 -> 95 bytes .../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 18 files changed, 230 insertions(+), 416 deletions(-) diff --git a/cedar-lean/Cedar/Validation/Types.lean b/cedar-lean/Cedar/Validation/Types.lean index 4b821e5fb..068e7e0d5 100644 --- a/cedar-lean/Cedar/Validation/Types.lean +++ b/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 diff --git a/cedar-lean/CedarProto/ActionDecl.lean b/cedar-lean/CedarProto/ActionDecl.lean index 5fef9229c..b3f5fa5a3 100644 --- a/cedar-lean/CedarProto/ActionDecl.lean +++ b/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) | _ => diff --git a/cedar-lean/CedarProto/EntityDecl.lean b/cedar-lean/CedarProto/EntityDecl.lean index f8a2a3715..fed6d6771 100644 --- a/cedar-lean/CedarProto/EntityDecl.lean +++ b/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,6 +46,12 @@ 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 @@ -52,13 +59,13 @@ def mergeDescendants (result : EntityDecl) (x : Array Spec.Name) : EntityDecl := } @[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 diff --git a/cedar-lean/CedarProto/Schema.lean b/cedar-lean/CedarProto/Schema.lean index e8d7204ec..5138311da 100644 --- a/cedar-lean/CedarProto/Schema.lean +++ b/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) diff --git a/cedar-lean/CedarProto/Type.lean b/cedar-lean/CedarProto/Type.lean index 6131b31a6..c90686388 100644 --- a/cedar-lean/CedarProto/Type.lean +++ b/cedar-lean/CedarProto/Type.lean @@ -13,6 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. -/ + import Cedar.Spec import Cedar.Validation import Protobuf.Enum @@ -25,379 +26,212 @@ import CedarProto.Name open Proto -namespace Cedar.Validation - -namespace Proto --- AttributeType <-> QualifiedType -def EntityRecordKind := CedarType - deriving Inhabited +namespace Cedar.Validation.Proto --- We create a type for every constructor, as we'll go --- about parsing the message differently for each -def EntityRecordKind.Record := EntityRecordKind -instance : Inhabited EntityRecordKind.Record where - default := .record default +mutual +inductive PrimType where + | string + | bool + | long +deriving Repr, Inhabited + +structure RecordType where + attrs : List (String × (Qualified ProtoType)) +deriving Repr, Inhabited + +inductive ProtoType where + | prim (p : PrimType) + | set (elTy : ProtoType) + | entity (ety : Spec.Name) + | record (rty : RecordType) + | ext (extTy : Spec.Name) +deriving Repr, Inhabited +end -def EntityRecordKind.Entity := EntityRecordKind -instance : Inhabited EntityRecordKind.Entity where - default := .entity default +namespace PrimType +@[inline] +def fromInt(n : Int) : Except String PrimType := + match n with + | 0 => .ok .string + | 1 => .ok .bool + | 2 => .ok .long + | n => .error s!"Field {n} does not exist in enum" -def EntityRecordKind.ActionEntity := EntityRecordKind -instance : Inhabited EntityRecordKind.ActionEntity where - default := .entity default -end Proto +instance : ProtoEnum PrimType := { + fromInt := fromInt +} +end PrimType -namespace QualifiedType +namespace Qualified @[inline] -def mergeType (result : QualifiedType) (x : CedarType) : QualifiedType := +def mergeType (result : Qualified α) (x : α) : Qualified α := -- Replace the type information, keep the qualified constructor match result with | .required _ => .required x | .optional _ => .optional x @[inline] -def mergeIsRequired (result : QualifiedType) (required : Bool) : QualifiedType := +def mergeIsRequired (result : Qualified α) (required : Bool) : Qualified α := -- Replace constructor, keep data if required then .required result.getType else .optional result.getType --- NOTE: parseField and merge both require mutual recursion and can be found --- at the end of this file. -end QualifiedType - -namespace Proto.EntityRecordKind - -inductive AnyEntity where - | any - -namespace AnyEntity -@[inline] -def fromInt (n : Int) : Except String AnyEntity := - match n with - | 0 => .ok .any - | n => .error s!"Field {n} does not exist in enum" -instance : ProtoEnum AnyEntity where - fromInt := fromInt -end AnyEntity - -namespace Record -@[inline] -def mergeAttributes (result : Record) (m2 : RecordType) : Record := - match result with - -- todo: this re-sorts every time we merge. - -- to be more efficient, we would have to use a type other than CedarType - -- here temporarily, which held Proto.Map instead of Cedar.Data.Map; - -- accumulate a Proto.Map, and then convert once at the end to Cedar.Data.Map. - -- See for instance how `EntityDecl` accumulates attributes. - | .record m1 => .record (Cedar.Data.Map.make (m2.kvs ++ m1.kvs)) - | _ => panic!("EntityRecordKind.Record is not set to the CedarType.record constructor") - @[inline] -def merge (x1 x2 : Record) : Record := +def merge [Field α] (x1 x2 : Qualified α) : Qualified α := match x1, x2 with - | .record m1, .record m2 => match m1.kvs with - | [] => .record m2 - | _ => .record (Cedar.Data.Map.make (m2.kvs ++ m1.kvs)) - | _, _ => panic!("EntityRecordKind.Record is not set to the CedarType.record constructor") + | .required t1, .required t2 => .required (Field.merge t1 t2) + | .optional t1, .optional t2 => .optional (Field.merge t1 t2) + | _, _ => x2 --- parseField requires mutual recursion and can be found at the end of the file -end Record +-- parseField requires mutual recursion and can be found at the end of this +-- file. +end Qualified -namespace Entity +namespace RecordType @[inline] -def mergeE (result : Entity) (e2 : Spec.Name) : Entity := - match result with - | .entity e1 => .entity (Field.merge e1 e2) - | _ => panic!("Entity expected CedarType constructor to be .entity") +def mergeAttrs (result : RecordType) (x : List (String × (Qualified ProtoType))) : RecordType := + { attrs := result.attrs ++ x } @[inline] -def merge (x1 x2 : Entity) : Entity := - match x1, x2 with - | .entity e1, .entity e2 => .entity (Field.merge e1 e2) - | _, _ => panic!("Entity expected CedarType constructor to be .entity") - -instance : Field Entity := Field.fromInterField .entity merge +def merge (x1 x2 : RecordType) : RecordType := + match x1.attrs with + | [] => { attrs := x2.attrs } + | _ => { attrs := x1.attrs ++ x2.attrs } -end Entity +-- parseField requires mutual recursion and can be found at the end of the file +end RecordType -namespace ActionEntity --- Note: Ignore the Attributes in the ActionEntity message --- since this isn't represented in the formal model +namespace ProtoType @[inline] -def mergeName (result : ActionEntity) (e2 : Spec.Name) : ActionEntity := +def mergePrim (result : ProtoType) (x : PrimType) : ProtoType := match result with - | .entity e1 => .entity (Field.merge e1 e2) - | _ => panic!("ActionEntity expected CedarType constructor to be .entity") - -@[inline] -def merge (x1 x2 : ActionEntity) : ActionEntity := - match x1, x2 with - | .entity e1, .entity e2 => .entity (Field.merge e1 e2) - | _, _ => panic!("ActionEntity expected CedarType constructor to be .entity") + | .prim p => .prim (Field.merge p x) + | _ => .prim x @[inline] -def parseField (t : Tag) : BParsec (MergeFn ActionEntity) := do - match t.fieldNum with - | 1 => - let x : Spec.Name ← Field.guardedParse t - pure (pure $ mergeName · x) - | _ => - t.wireType.skip - pure ignore - -instance : Message ActionEntity := { - parseField := parseField - merge := merge -} -end ActionEntity - -@[inline] -def mergeAnyEntity (_ : EntityRecordKind) (x : AnyEntity) : EntityRecordKind := - match x with - | .any => panic!("Not Implemented") - -@[inline] -def mergeRecord (result : EntityRecordKind) (x : Record) : EntityRecordKind := - have m2 := match x with - | .record m => m - | _ => panic!("EntityRecordKind.Record is not set to the CedarType.record constructor") +def mergeEntity (result : ProtoType) (x : Spec.Name) : ProtoType := match result with - | .record m1 => match m1.kvs with - | [] => .record m2 - | _ => .record (Cedar.Data.Map.make (m2.kvs ++ m1.kvs)) - | _ => .record m2 + | .entity n => .entity (Field.merge n x) + | _ => .entity x @[inline] -def mergeEntity (result : EntityRecordKind) (x : Entity) : EntityRecordKind := - have e2 := match x with - | .entity e => e - | _ => panic!("EntityRecordKind.Entity is not set to the CedarType.entity constructor") +def mergeExt (result : ProtoType) (x : Spec.Name) : ProtoType := match result with - | .entity e1 => .entity (Field.merge e1 e2) - | _ => .entity e2 + | .ext n => .ext (Field.merge n x) + | _ => .ext x +mutual @[inline] -def mergeActionEntity (result : EntityRecordKind) (x : ActionEntity) : EntityRecordKind := - have e2 := match x with - | .entity e => e - | _ => panic!("EntityRecordKind.ActionEntity is not set to the CedarType.entity constructor") +partial def mergeSet (result : ProtoType) (x : ProtoType) : ProtoType := match result with - | .entity e1 => .entity (Field.merge e1 e2) - | _ => .entity e2 - -@[inline] -def merge (x1 x2 : EntityRecordKind) : EntityRecordKind := - match x1, x2 with - | .entity e1, .entity e2 => .entity (Field.merge e1 e2) - | .record m1, .record m2 => .record (Cedar.Data.Map.make (m2.kvs ++ m1.kvs)) - | .entity _, .record _ => x2 - | .record _, .entity _ => x2 - | _, _ => panic!("Expected EntityRecordKind to be CedarType.record or CedarType.entity") - --- NOTE: parseField requires mutual recursion and can be found at the end of the file -end Proto.EntityRecordKind - -namespace CedarType - --- Note that Cedar.Validation.CedarType is defined as --- inductive CedarType where --- | bool (bty : BoolType) --- | int --- | string --- | entity (ety : EntityType) --- | set (ty : CedarType) --- | record (rty : Map Attr (Qualified CedarType)) --- | ext (xty : ExtType) - -inductive Ty where - | never - | true - | false - | emptySetType - | bool - | string - | long -deriving Inhabited + | .set elty => .set (ProtoType.merge elty x) + | _ => .set x -namespace Ty @[inline] -def fromInt(n : Int) : Except String Ty := - match n with - | 0 => .ok .never - | 1 => .ok .true - | 2 => .ok .false - | 3 => .ok .emptySetType - | 4 => .ok .bool - | 5 => .ok .string - | 6 => .ok .long - | n => .error s!"Field {n} does not exist in enum" - -instance : ProtoEnum Ty := { - fromInt := fromInt -} -end Ty +partial def mergeRecord (result : ProtoType) (x : RecordType) : ProtoType := + match result with + | .record m => .record (RecordType.merge m x) + | _ => .record x @[inline] -def mergeTy (_ : CedarType) (x : Ty) : CedarType := - match x with - | .never => panic!("Unexpected never type") - | .true => .bool .tt - | .false => .bool .ff - | .emptySetType => panic!("Expected type of set elements to be specified") - | .bool => .bool .anyBool - | .string => .string - | .long => .int - - -partial def merge (x1 x2 : CedarType) : CedarType := +partial def merge (x1 x2 : ProtoType) : ProtoType := match x1, x2 with + | .prim p1, .prim p2 => .prim (Field.merge p1 p2) + | .set el1, .set el2 => .set (merge el1 el2) | .entity e1, .entity e2 => .entity (Field.merge e1 e2) - | .record m1, .record m2 => match m1.kvs with - | [] => .record m2 - | _ => .record (Data.Map.make (m2.kvs ++ m1.kvs)) - | .set t1, .set t2 => .set (merge t1 t2) + | .record m1, .record m2 => .record (RecordType.merge m1 m2) + | .ext x1, .ext x2 => .ext (Field.merge x1 x2) -- For the rest of the fields, replace | _, _ => x2 +end -@[inline] -def mergeType (result : CedarType) (x2 : CedarType) : CedarType := - match result with - | .set x1 => .set (merge x1 x2) - | _ => .set x2 - -@[inline] -def mergeEr (result : CedarType) (x : Proto.EntityRecordKind) : CedarType := - match result, x with - | .entity e1, .entity e2 => .entity (Field.merge e1 e2) - | .record m1, .record m2 => match m1.kvs with - | [] => .record m2 - | _ => .record (Data.Map.make (m2.kvs ++ m1.kvs)) - | _, .record _ => x - | _, .entity _ => x - | _, _ => panic!("Expected EntityRecordKind to be CedarType.record or CedarType.entity") - -@[inline] -def mergeName (_ : CedarType) (xty : Cedar.Spec.Name) : BParsec CedarType := - match xty.id with - | "ipaddr" => pure $ .ext .ipAddr - | "decimal" => pure $ .ext .decimal - | xty => throw s!"mergeName: unknown extension type {xty}" - - -end CedarType - -@[inline] -def QualifiedType.merge (x1 x2 : QualifiedType) : QualifiedType := - match x1, x2 with - | .required t1, .required t2 => .required (CedarType.merge t1 t2) - | .optional t1, .optional t2 => .optional (CedarType.merge t1 t2) - | .optional _, .required _ => x2 - | .required _, .optional _ => x2 +partial def toCedarType : ProtoType → CedarType + | .prim .bool => .bool .anyBool + | .prim .long => .int + | .prim .string => .string + | .set t => .set t.toCedarType + | .entity e => .entity e + | .record r => .record $ Data.Map.make $ r.attrs.map λ (k,v) => (k, v.map toCedarType) + | .ext n => match n.id with -- ignoring n.path because currently no extension types have nonempty namespaces + | "ipaddr" => .ext .ipAddr + | "decimal" => .ext .decimal + | _ => panic!(s!"unknown extension type name: {n}") +end ProtoType mutual -partial def QualifiedType.parseField (t : Tag) : BParsec (MergeFn QualifiedType) := do - have : Message CedarType := { parseField := CedarType.parseField, merge := CedarType.merge} +partial def QualifiedProtoType.parseField (t : Tag) : BParsec (MergeFn (Qualified ProtoType)) := do + have : Message ProtoType := { parseField := ProtoType.parseField, merge := ProtoType.merge} match t.fieldNum with | 1 => - let x : CedarType ← Field.guardedParse t - pure (pure $ QualifiedType.mergeType · x) + let x : ProtoType ← Field.guardedParse t + pure (pure $ Qualified.mergeType · x) | 2 => let x : Bool ← Field.guardedParse t - pure (pure $ QualifiedType.mergeIsRequired · x) - | _ => - t.wireType.skip - pure ignore - -partial def Proto.EntityRecordKind.parseField (t : Tag) : BParsec (MergeFn Proto.EntityRecordKind) := do - have : Message Proto.EntityRecordKind.Record := { parseField := Proto.EntityRecordKind.Record.parseField, merge := Proto.EntityRecordKind.Record.merge } - match t.fieldNum with - | 1 => - let x : Proto.EntityRecordKind.AnyEntity ← Field.guardedParse t - pure (pure $ Proto.EntityRecordKind.mergeAnyEntity · x) - | 2 => - let x : Proto.EntityRecordKind.Record ← Field.guardedParse t - pure (pure $ Proto.EntityRecordKind.mergeRecord · x) - | 3 => - let x : Proto.EntityRecordKind.Entity ← Field.guardedParse t - pure (pure $ Proto.EntityRecordKind.mergeEntity · x) - | 4 => - let x : Proto.EntityRecordKind.ActionEntity ← Field.guardedParse t - pure (pure $ Proto.EntityRecordKind.mergeActionEntity · x) + pure (pure $ Qualified.mergeIsRequired · x) | _ => t.wireType.skip pure ignore -partial def Proto.EntityRecordKind.Record.parseField (t : Tag) : BParsec (MergeFn Proto.EntityRecordKind.Record) := do - have : Message QualifiedType := { parseField := QualifiedType.parseField, merge := QualifiedType.merge } +partial def RecordType.parseField (t : Tag) : BParsec (MergeFn RecordType) := do + have : Message ProtoType := { parseField := ProtoType.parseField, merge := ProtoType.merge } + have : Message (Qualified ProtoType) := { parseField := QualifiedProtoType.parseField, merge := Qualified.merge } match t.fieldNum with | 1 => - let x : Proto.Map String QualifiedType ← Field.guardedParse t - pure (pure $ Proto.EntityRecordKind.Record.mergeAttributes · (Cedar.Data.Map.mk x.toList)) -- using `mk` instead of `make` because we know `mergeAttributes` will re-sort anyway + let x : Proto.Map String (Qualified ProtoType) ← Field.guardedParse t + pure (pure $ RecordType.mergeAttrs · x.toList) | _ => t.wireType.skip pure ignore -partial def CedarType.parseField (t : Tag) : BParsec (MergeFn CedarType) := do - have : Message CedarType := {parseField := CedarType.parseField, merge := CedarType.merge } - have : Message Proto.EntityRecordKind := {parseField := Proto.EntityRecordKind.parseField, merge := Proto.EntityRecordKind.merge } +partial def ProtoType.parseField (t : Tag) : BParsec (MergeFn ProtoType) := do + have : Message ProtoType := { parseField := ProtoType.parseField, merge := ProtoType.merge } + have : Message RecordType := { parseField := RecordType.parseField, merge := RecordType.merge } match t.fieldNum with | 1 => - let x : CedarType.Ty ← Field.guardedParse t - pure (pure $ CedarType.mergeTy · x) + let x : PrimType ← Field.guardedParse t + pure (pure $ ProtoType.mergePrim · x) | 2 => - let x : CedarType ← Field.guardedParse t - pure (pure $ CedarType.mergeType · x) + let x : ProtoType ← Field.guardedParse t + pure (pure $ ProtoType.mergeSet · x) | 3 => - let x : Proto.EntityRecordKind ← Field.guardedParse t - pure (pure $ CedarType.mergeEr · x) + let x : Spec.Name ← Field.guardedParse t + pure (pure $ ProtoType.mergeEntity · x) | 4 => - let x : Cedar.Spec.Name ← Field.guardedParse t - pure (CedarType.mergeName · x) + let x : RecordType ← Field.guardedParse t + pure (pure $ ProtoType.mergeRecord · x) + | 5 => + let x : Spec.Name ← Field.guardedParse t + pure (pure $ ProtoType.mergeExt · x) | _ => t.wireType.skip pure ignore -end - -namespace QualifiedType -instance : Message QualifiedType := { - parseField := parseField - merge := merge -} -end QualifiedType -namespace Proto.EntityRecordKind -instance : Message Proto.EntityRecordKind := { - parseField := parseField - merge := merge -} -end Proto.EntityRecordKind +end -namespace Proto.EntityRecordKind.Record -instance : Message Proto.EntityRecordKind.Record := { +namespace RecordType +instance : Message RecordType := { parseField := parseField merge := merge } -end Proto.EntityRecordKind.Record +end RecordType -namespace Proto.EntityRecordKind.ActionEntity -instance : Message Proto.EntityRecordKind.ActionEntity := { +namespace ProtoType +instance : Message ProtoType := { parseField := parseField merge := merge } -end Proto.EntityRecordKind.ActionEntity +end ProtoType -namespace CedarType -instance : Message CedarType := { - parseField := parseField - merge := merge +instance : Message (Qualified ProtoType) := { + parseField := QualifiedProtoType.parseField + merge := Qualified.merge } -end CedarType -end Cedar.Validation +end Cedar.Validation.Proto 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..5010edd514af4d98564ae1c8daf474f25ce4c9ba 100644 GIT binary patch delta 39 ucmeBW>}8bU;^t!GVssK>bQEHA7UJb%PD(5iV&h`rV&Y(!$g4Kd$r}J`R0Yxi delta 40 vcmeBW>}BNT;^t!GVssK>bQEHAo+zWnFT~5moRnB3#Ky(K#l*od(a9SCbyNl6 diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata index 246a7d55f645ff7e82d5c7f40c843f45d8c424cf..39d186c3b1f01345edb5db40e494516f86b4161c 100644 GIT binary patch delta 75 zcmdnZvYTb%!-k2B4<{!w#!i04=xSjg#L2~8ke`#8TxlRA0%IB>M2!%lh6qtZ0JNAF A82|tP delta 66 ycmdnZvYTaM{iBJD^^+4BW3@%N*bDM=GLtI}g*XvRxTpa_)L`;nMz_h5OgsR{pcDoG diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata index 7b7819b1a5e85fa0390ffee3d128c967150e02ad..723e71b19ff66939d61c04c26bcd18405932128c 100644 GIT binary patch literal 409 zcmZXQ!A^rf5QaMxO8KdX)1EkP;)Rk2E92sPNm$MNn{I=ih_<7IZ| zpV^sje*~C<3b>=h2idgBV$dVc;LW|1vItbOFUcfJKn+I-GW$qM(x+V?Ns@vL#|YV# zOHr1fCr*HTj#>Arn`RVo18VsiYjuGIeABjXZn%dNOrLe{#!XTJBiOzVX8hh)rLu(2 zkwT^w^{(3v?B5yPWM{vWz$y>?N%*g-mBl|roJR;7Q+K_7NlD#W?i*aGHIf6+;pnmWw`gO%*8ktic5R5q2lFV*88#BnJ$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..26856c0a8 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 +B + +  A -B ? - - -ActionReadX* +B"   -ActionReadX": -AB -BB -AA - - -ActionRead- +ActionReadX* +A2 +B2 +A%   ActionRead  -ActionReadX"0 - - -ActionWrite +ActionReadX   -ActionWrite" \ No newline at end of file +ActionWrite \ 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..aa821b7b7f22491e517911fefcca8a21cac0cf98 100644 GIT binary patch literal 177 zcmYL?I|{-;6h(dJV{+0A53!g=7_3A@1Q!qkF2EfGKcI!v*y!rb8x)&+Z*eY%f(+?c zSRH(WytQOpjhuLgytJX#i55Ol7`0bJNxMy3?>H*T_Vm2Phvvsie-7XG@9QM&kX|>e f!;0EGxp|nI#WM?2l23@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..77be9ca4a1e8f301964e129e140b6830bbaba350 100644 GIT binary patch literal 95 zcmd;*;9}-tbd%!cVyqJ4;9?PC;$RS9)B=)R+#nejEwB(5ABf|s#V*7u1!OpK@q_qI YLO{X|M7VHqfdm}E0$iLRwll~O04qiYNdN!< 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/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 Date: Wed, 26 Feb 2025 13:53:26 -0800 Subject: [PATCH 2/3] update for cedar#1506 (#554) 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/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 409 -> 409 bytes .../schema_basic.protodata | 20 ++++++++--------- .../schema_commontypes.protodata | Bin 177 -> 177 bytes .../schema_tags.protodata | Bin 95 -> 95 bytes .../CedarProto-test-data/set.protodata | 5 +---- .../thisiscedar.protodata | 1 - .../CedarProto-test-data/true.protodata | 1 - .../CedarProto-test-data/user_alice.protodata | 1 - 39 files changed, 50 insertions(+), 107 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/entity.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata index 5010edd514af4d98564ae1c8daf474f25ce4c9ba..ea255c8805ece2f0593ec96de58ae2ef2e957336 100644 GIT binary patch delta 96 zcmeBWY-BXy;^t!GVssK>bQEHA7UJe&PD(5iV&P)qU=WhyVouA?7ZNWL<>KYy7WfYX hj1z6Nlm)n0N)pqJggCg^q*%%lbBvTAB8G4gLjVF|7aITo delta 108 zcmZo<>}9m!;^t!GVssK>bQEHA7UJb%PD(5iV&h`rV&Y&BQsH7w%g+~*<&rLvD6j4+D%`Y!gki)P=ZMN)pqJgt)jkxY(pv$`W&olptb;NMeQnv0N9s 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 39d186c3b1f01345edb5db40e494516f86b4161c..6ee4624c65a80f62e5546316e13ecb879d3645c0 100644 GIT binary patch delta 229 zcmdnZGJ%DcE1!$KAU`KFxza!=Wg@S&nTC^^khqg52a6DQ5GNOt0J9KtT7JG13y{e! z1s6(6EaD1>=`* a#055qrKGYTRY(M;*-(fR&YZlLF#`Z%1~94s delta 296 zcmbQhvYUmMtCowsAU`KFxza$WXdgHfD0%9v5cGBh2w$c<*=Tdc2=3o*M z=MoJP1{=vF#GRUxnJ$}|l$n!RQVF$)iL0FvW}1;u&14luCwEIOb0<>{c90v3q`BC+ zSh<*`7!zTPBp4%EN`Q+mhzDvoOG#xxDpxejEJLAyiFLZ{N?Zy-a$GDE*U3y?!I&W? KB!ZCVgfjv05;ju+ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/policyset_just_templates.protodata b/cedar-lean/UnitTest/CedarProto-test-data/policyset_just_templates.protodata index 9296f7276a166abf149b303d794417c70cded707..331b9a2ea744fcb9c30ae953e0d6ce09439dea18 100644 GIT binary patch delta 25 gcmXregS4(2@>DJsY}f mP|8cpT^}~IV|@M!(7jE=kswz{B^w6UmV!JfD>7US%V6` zL?~zQVdq8hXly3>uuj>z5gLrZ;as1W{QmotGGbJIqKeTN5h&*?EM!>iXd>XXUY)O0 d@}Fo_HyTRm>!#hdQ4*+H4a9T3X-LcW=nJVp9XS91 diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata index 26856c0a8..afec18049 100644 --- a/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata +++ b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata @@ -1,23 +1,23 @@ - - -B  A -B" +B + + +B + + +ActionWrite"   ActionReadX* A2 -B2 -A% +A2 +B%   ActionRead  -ActionReadX - - -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 aa821b7b7f22491e517911fefcca8a21cac0cf98..22797b11b164c47baebf3a7eb51ef1403ea8a773 100644 GIT binary patch delta 67 zcmdnUxRH^Ei;Ihyi_u94NVrX8*Wq;pv$$A6qRtatjV3lJNO5s;F;)q&a4~T(XaR*C KL4=bLNC5ys;s~?= delta 67 zcmdnUxRH^ai@1hXf)8gX%QF;)q&a4~T(Oe|C6*8<8p Lfe1$ Date: Thu, 27 Feb 2025 12:21:17 -0800 Subject: [PATCH 3/3] more elegant Protobuf.Message impl (#555) Signed-off-by: Craig Disselkoen --- cedar-lean/CedarProto/ActionDecl.lean | 85 ++++++++------------------- cedar-lean/CedarProto/Schema.lean | 4 +- 2 files changed, 26 insertions(+), 63 deletions(-) diff --git a/cedar-lean/CedarProto/ActionDecl.lean b/cedar-lean/CedarProto/ActionDecl.lean index b3f5fa5a3..1a1ac466f 100644 --- a/cedar-lean/CedarProto/ActionDecl.lean +++ b/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,78 +39,34 @@ namespace Cedar.Validation.Proto -- the transform structure ActionDecl where name : Spec.EntityUID - descendants : Array Spec.EntityUID + descendants : Repeated Spec.EntityUID context : Proto.Map String (Qualified ProtoType) - principal_types : Array Spec.Name - resource_types : Array Spec.Name + 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 : Proto.Map String (Qualified ProtoType)) : 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 : Proto.Map String (Qualified ProtoType) ← Field.guardedParse t - pure (pure $ mergeContext · x) - | 5 => - let x : Repeated Spec.Name ← Field.guardedParse t - pure (pure $ mergePrincipalTypes · x) - | 6 => - 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 } diff --git a/cedar-lean/CedarProto/Schema.lean b/cedar-lean/CedarProto/Schema.lean index 5138311da..bbd6fa0e0 100644 --- a/cedar-lean/CedarProto/Schema.lean +++ b/cedar-lean/CedarProto/Schema.lean @@ -69,8 +69,8 @@ def toSchema (schema : Schema) : Validation.Schema := let ancestorMap := descendantsToAncestors descendantMap 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 + appliesToPrincipal := Data.Set.make decl.principalTypes.toList + appliesToResource := Data.Set.make decl.resourceTypes.toList ancestors := ancestorMap.find! decl.name context := Data.Map.make $ decl.context.toList.map λ (k,v) => (k, v.map ProtoType.toCedarType) })