diff --git a/cedar-lean/Cedar/Spec/Template.lean b/cedar-lean/Cedar/Spec/Template.lean index 7f2cfeb95..059075232 100644 --- a/cedar-lean/Cedar/Spec/Template.lean +++ b/cedar-lean/Cedar/Spec/Template.lean @@ -34,6 +34,7 @@ abbrev SlotID := String inductive EntityUIDOrSlot where | entityUID (entity : EntityUID) | slot (id : SlotID) +deriving Repr, DecidableEq inductive ScopeTemplate where | any @@ -41,12 +42,15 @@ inductive ScopeTemplate where | mem (entityOrSlot : EntityUIDOrSlot) | is (ety : EntityType) | isMem (ety : EntityType) (entityOrSlot : EntityUIDOrSlot) +deriving Repr, DecidableEq inductive PrincipalScopeTemplate where | principalScope (scope : ScopeTemplate) +deriving Repr, DecidableEq inductive ResourceScopeTemplate where | resourceScope (scope : ScopeTemplate) +deriving Repr, DecidableEq abbrev TemplateID := String @@ -56,6 +60,7 @@ structure Template where actionScope : ActionScope resourceScope : ResourceScopeTemplate condition : Conditions +deriving Repr, DecidableEq abbrev Templates := Map TemplateID Template @@ -67,40 +72,41 @@ structure TemplateLinkedPolicy where id : PolicyID templateId : TemplateID slotEnv : SlotEnv +deriving Repr abbrev TemplateLinkedPolicies := List TemplateLinkedPolicy -def EntityUIDOrSlot.link? (slotEnv : SlotEnv) : EntityUIDOrSlot → Option EntityUID - | entityUID entity => .some entity - | slot id => slotEnv.find? id +def EntityUIDOrSlot.link? (slotEnv : SlotEnv) : EntityUIDOrSlot → Except String EntityUID + | entityUID entity => .ok entity + | slot id => slotEnv.findOrErr id s!"missing binding for slot {id}" -def ScopeTemplate.link? (slotEnv : SlotEnv) : ScopeTemplate → Option Scope - | .any => .some .any +def ScopeTemplate.link? (slotEnv : SlotEnv) : ScopeTemplate → Except String Scope + | .any => .ok .any | .eq entityOrSlot => do let entity ← entityOrSlot.link? slotEnv - .some (.eq entity) + .ok (.eq entity) | .mem entityOrSlot => do let entity ← entityOrSlot.link? slotEnv - .some (.mem entity) - | .is ety => .some (.is ety) + .ok (.mem entity) + | .is ety => .ok (.is ety) | .isMem ety entityOrSlot => do let entity ← entityOrSlot.link? slotEnv - .some (.isMem ety entity) + .ok (.isMem ety entity) -def PrincipalScopeTemplate.link? (slotEnv : SlotEnv) : PrincipalScopeTemplate → Option PrincipalScope +def PrincipalScopeTemplate.link? (slotEnv : SlotEnv) : PrincipalScopeTemplate → Except String PrincipalScope | .principalScope s => do let s ← s.link? slotEnv - .some (.principalScope s) + .ok (.principalScope s) -def ResourceScopeTemplate.link? (slotEnv : SlotEnv) : ResourceScopeTemplate → Option ResourceScope +def ResourceScopeTemplate.link? (slotEnv : SlotEnv) : ResourceScopeTemplate → Except String ResourceScope | .resourceScope s => do let s ← s.link? slotEnv - .some (.resourceScope s) + .ok (.resourceScope s) -def Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) : Option Policy := do +def Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) : Except String Policy := do let principalScope ← template.principalScope.link? slotEnv let resourceScope ← template.resourceScope.link? slotEnv - .some { + .ok { id := id, effect := template.effect, principalScope := principalScope, @@ -109,11 +115,11 @@ def Template.link? (template : Template) (id : PolicyID) (slotEnv : SlotEnv) : O condition := template.condition } -def linkPolicy? (templates : Templates) (link : TemplateLinkedPolicy) : Option Policy := do - let template ← templates.find? link.templateId +def linkPolicy? (templates : Templates) (link : TemplateLinkedPolicy) : Except String Policy := do + let template ← templates.findOrErr link.templateId s!"templateId {link.templateId} not found" template.link? link.id link.slotEnv -def link? (templates : Templates) (links : TemplateLinkedPolicies) : Option Policies := +def link? (templates : Templates) (links : TemplateLinkedPolicies) : Except String Policies := links.mapM (linkPolicy? templates) end Cedar.Spec diff --git a/cedar-lean/Cedar/Spec/Wildcard.lean b/cedar-lean/Cedar/Spec/Wildcard.lean index 2606f9c97..720e3d0cd 100644 --- a/cedar-lean/Cedar/Spec/Wildcard.lean +++ b/cedar-lean/Cedar/Spec/Wildcard.lean @@ -25,6 +25,9 @@ inductive PatElem where | justChar (c : Char) deriving Repr, DecidableEq, Inhabited +instance : Coe Char PatElem where + coe c := .justChar c + def PatElem.lt : PatElem → PatElem → Bool | .justChar c₁, .justChar c₂ => c₁ < c₂ | .star, .justChar _ => true diff --git a/cedar-lean/CedarProto.lean b/cedar-lean/CedarProto.lean new file mode 100644 index 000000000..5bb506d59 --- /dev/null +++ b/cedar-lean/CedarProto.lean @@ -0,0 +1,41 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import CedarProto.ActionConstraint +import CedarProto.AuthorizationRequest +import CedarProto.Context +import CedarProto.Entities +import CedarProto.Entity +import CedarProto.EntityReference +import CedarProto.EntityType +import CedarProto.EntityUID +import CedarProto.EntityUIDEntry +import CedarProto.Expr +import CedarProto.LiteralPolicy +import CedarProto.LiteralPolicySet +import CedarProto.Name +import CedarProto.PrincipalConstraint +import CedarProto.PrincipalOrResourceConstraint +import CedarProto.Request +import CedarProto.ResourceConstraint +import CedarProto.TemplateBody +import CedarProto.Type +import CedarProto.ValidationRequest +import CedarProto.ValidatorActionId +import CedarProto.ValidatorApplySpec +import CedarProto.ValidatorEntityType +import CedarProto.ValidatorSchema +import CedarProto.Value diff --git a/cedar-lean/CedarProto/ActionConstraint.lean b/cedar-lean/CedarProto/ActionConstraint.lean new file mode 100644 index 000000000..369c545af --- /dev/null +++ b/cedar-lean/CedarProto/ActionConstraint.lean @@ -0,0 +1,178 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Enum + +-- Message Dependencies +import CedarProto.EntityUID + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.ActionScope is defined as +-- inductive ActionScope where +-- | actionScope (scope : Scope) +-- | actionInAny (ls : List EntityUID) + +namespace Proto +-- Constructors for ActionScope + +inductive ActionScope.Ty where + | any +deriving Inhabited + +def ActionScope.In := ActionScope +def ActionScope.Eq := ActionScope +end Proto + +namespace Proto.ActionScope.Ty +@[inline] +def fromInt (n : Int) : Except String ActionScope.Ty := + match n with + | 0 => .ok .any + | n => .error s!"Field {n} does not exist in enum" + +instance : ProtoEnum ActionScope.Ty := { + fromInt := fromInt +} +end Proto.ActionScope.Ty + +namespace Proto.ActionScope.In +instance : Inhabited ActionScope.In where + default := .actionInAny default + +@[inline] +def mergeEuids (result : ActionScope.In) (e2 : Array EntityUID) : ActionScope.In := + match result with + | .actionInAny e1 => .actionInAny (e1 ++ e2.toList) + | _ => panic!("ActionScope.In expected ActionScope constructor to be set to .actionInAny") + +@[inline] +def merge (x1 x2 : ActionScope.In) : ActionScope.In := + match x1, x2 with + | .actionInAny e1, .actionInAny e2 => + .actionInAny (e1 ++ e2) + | _, _ => panic!("ActionScope.In expected ActionScope constructor to be set to .actionInAny") + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.In) := do + match t.fieldNum with + | 1 => + let x : Repeated EntityUID ← Field.guardedParse t + pure (mergeEuids · x) + | _ => + t.wireType.skip + pure id + +instance : Message ActionScope.In := { + parseField := parseField + merge := merge +} +end Proto.ActionScope.In + +namespace Proto.ActionScope.Eq +instance : Inhabited ActionScope.Eq where + default := .actionScope (.eq default) + +@[inline] +def mergeEuid (result : ActionScope.Eq) (e2 : EntityUID) : ActionScope.Eq := + match result with + | .actionScope (.eq e1) => .actionScope (.eq (Field.merge e1 e2)) + | _ => panic!("ActionScope.Eq expected ActionScope constructor to be set to .actionScope .eq") + +@[inline] +def merge (x1 x2 : ActionScope.Eq) : ActionScope.Eq := + match x2 with + | .actionScope (.eq e) => mergeEuid x1 e + | _ => panic!("ActionScope.Eq expected ActionScope constructor to be set to .actionScope .eq") + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope.Eq) := do + match t.fieldNum with + | 1 => + let x : EntityUID ← Field.guardedParse t + pure (mergeEuid · x) + | _ => + t.wireType.skip + pure id + +instance : Message ActionScope.Eq := { + parseField := parseField + merge := merge +} +end Proto.ActionScope.Eq + +namespace ActionScope + +@[inline] +def mergeTy (_ : ActionScope) (x : Proto.ActionScope.Ty) : ActionScope := + match x with + | .any => .actionScope (Scope.any) + +@[inline] +def mergeIn (result : ActionScope) (x : Proto.ActionScope.In) : ActionScope := + have e2 := match x with + | .actionInAny e => e + | _ => panic!("Proto.ActionScope.In expected to have constructor .actionInAny") + match result with + | .actionInAny e1 => .actionInAny (e1 ++ e2) + | _ => .actionInAny e2 + +@[inline] +def mergeEq (result : ActionScope) (x : Proto.ActionScope.Eq) : ActionScope := + have e2 := match x with + | .actionScope (.eq e) => e + | _ => panic!("Proto.ActionScope.Eq expected to have constructor .actionScope .eq") + match result with + | .actionScope (.eq e1) => .actionScope (.eq (Field.merge e1 e2)) + | _ => .actionScope (.eq e2) + +@[inline] +def merge (x1 x2 : ActionScope) : ActionScope := + match x1, x2 with + | .actionScope (.eq e1), .actionScope (.eq e2) => + -- Merge entity data + .actionScope (.eq (Field.merge e1 e2)) + | .actionInAny l1, .actionInAny l2 => + -- Merge entity uids + .actionInAny (l1 ++ l2) + | _, _ => x2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ActionScope) := do + match t.fieldNum with + | 1 => + let x : Proto.ActionScope.Ty ← Field.guardedParse t + pure (mergeTy · x) + | 2 => + let x : Proto.ActionScope.In ← Field.guardedParse t + pure (mergeIn · x) + | 3 => + let x : Proto.ActionScope.Eq ← Field.guardedParse t + pure (mergeEq · x) + | _ => + t.wireType.skip + pure id + +instance : Message ActionScope := { + parseField := parseField + merge := merge +} + +end ActionScope + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/AuthorizationRequest.lean b/cedar-lean/CedarProto/AuthorizationRequest.lean new file mode 100644 index 000000000..1694d0d89 --- /dev/null +++ b/cedar-lean/CedarProto/AuthorizationRequest.lean @@ -0,0 +1,83 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.Request +import CedarProto.LiteralPolicySet +import CedarProto.Entities + +open Proto + +namespace Cedar.Spec +structure AuthorizationRequest where + request : Request + entities : Entities + policies : Policies +deriving Inhabited, DecidableEq, Repr + +namespace AuthorizationRequest + +@[inline] +def mergeRequest (result : AuthorizationRequest) (x : Request) : AuthorizationRequest := + {result with + request := Field.merge result.request x + } + +@[inline] +def mergeEntities (result : AuthorizationRequest) (x : Entities) : AuthorizationRequest := + {result with + entities := Field.merge result.entities x + } + +@[inline] +def mergePolicies (result : AuthorizationRequest) (x : Policies) : AuthorizationRequest := + {result with + policies := Field.merge result.policies x + } + +@[inline] +def merge (x y : AuthorizationRequest) : AuthorizationRequest := + { + request := Field.merge x.request y.request + entities := Field.merge x.entities y.entities + policies := Field.merge x.policies y.policies + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn AuthorizationRequest) := do + match t.fieldNum with + | 1 => + let x : Request ← Field.guardedParse t + pure (mergeRequest · x) + | 2 => + let x : Policies ← Field.guardedParse t + pure (mergePolicies · x) + | 3 => + let x : Entities ← Field.guardedParse t + pure (mergeEntities · x) + | _ => + t.wireType.skip + pure id + +instance : Message AuthorizationRequest := { + parseField := parseField + merge := merge +} + +end AuthorizationRequest + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Context.lean b/cedar-lean/CedarProto/Context.lean new file mode 100644 index 000000000..6597decbc --- /dev/null +++ b/cedar-lean/CedarProto/Context.lean @@ -0,0 +1,63 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.Map +import Protobuf.String + +-- Message Dependencies +import CedarProto.Value + +open Proto + +namespace Cedar.Spec + +def Context := Cedar.Data.Map Attr Value +deriving Inhabited + +namespace Context + +@[inline] +def mergeValue (result : Context) (x : Value) : Context := + match x with + | .record m => Cedar.Data.Map.mk (result.kvs ++ m.kvs) + | _ => panic!("Context is not of correct type") + +@[inline] +def merge (x1 : Context) (x2 : Context) : Context := + -- Avoid a sort if x1 is empty + match x1.kvs with + | [] => x2 + | _ => Cedar.Data.Map.make (x2.kvs ++ x1.kvs) + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn Context) := do + match t.fieldNum with + | 1 => + let x : Value ← Field.guardedParse t + pure (mergeValue · x) + | _ => + t.wireType.skip + pure id + +instance : Message Context := { + parseField := parseField + merge := merge +} + +end Context + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Entities.lean b/cedar-lean/CedarProto/Entities.lean new file mode 100644 index 000000000..46118de6f --- /dev/null +++ b/cedar-lean/CedarProto/Entities.lean @@ -0,0 +1,85 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.Entity + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.Entities is defined as +-- abbrev Entities := Map EntityUID EntityData + +-- Note that EntityData doesn't contain EntityUID, therefore +-- we need to parse an intermediate representation EntityProto +-- which contains that and transform it to the appropriate types. + +def EntitiesProto : Type := Array EntityProto +deriving instance Inhabited for EntitiesProto + +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 + result ++ x + +@[inline] +def merge (x : EntitiesProto) (y : EntitiesProto) : EntitiesProto := + have x : Array EntityProto := x + have y : Array EntityProto := y + x ++ y + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn EntitiesProto) := do + match t.fieldNum with + | 1 => + let x : Repeated EntityProto ← Field.guardedParse t + pure (mergeEntities · x) + -- Ignoring 3 | mode + | _ => + t.wireType.skip + pure id + +instance : Message EntitiesProto := { + parseField := parseField + merge := merge +} + +@[inline] +def toEntities (e : EntitiesProto) : Entities := + Cedar.Data.Map.make (e.toList.map λ entity => ⟨entity.uid, entity.data⟩) + +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.Data.Map.make (e2.kvs ++ e1.kvs) + +instance : Field Entities := Field.fromInterField EntitiesProto.toEntities merge + +end Entities + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Entity.lean b/cedar-lean/CedarProto/Entity.lean new file mode 100644 index 000000000..2673daef7 --- /dev/null +++ b/cedar-lean/CedarProto/Entity.lean @@ -0,0 +1,126 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.EntityUID +import CedarProto.Value + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.EntityData is defined as +-- structure EntityData where +-- attrs : Map Attr Value +-- ancestors : Set EntityUID +-- tags : Map Tag Value + +-- NOTE: EntityData is defined in Cedar.Spec.Entities +-- however it doesn't have the uid field which is +-- needed when crafting Entities, therefore +-- we store within an intermediate representation instead + +structure EntityProto where + uid : EntityUID + data : EntityData +deriving Inhabited, DecidableEq, Repr + +namespace EntityProto + +@[inline] +def mergeUid (result : EntityProto) (x : EntityUID) : EntityProto := + {result with + uid := Field.merge result.uid x + } + +@[inline] +def mergeAttrs (result : EntityProto) (x : Array (String × Value)) : EntityProto := + {result with + data.attrs := Cedar.Data.Map.mk (result.data.attrs.kvs ++ x.toList) + } + +@[inline] +def mergeAncestors (result : EntityProto) (x : Array EntityUID) : EntityProto := + {result with + data.ancestors := Cedar.Data.Set.mk (result.data.ancestors.elts ++ x.toList) + } + +@[inline] +def mergeTags (result : EntityProto) (x : Array (String × Value)) : EntityProto := + {result with + data.tags := Cedar.Data.Map.mk (result.data.tags.kvs ++ x.toList) + } + +@[inline] +def merge (x : EntityProto) (y : EntityProto) : EntityProto := + { + uid := Field.merge x.uid y.uid + data.attrs := Cedar.Data.Map.mk (x.data.attrs.kvs ++ y.data.attrs.kvs) + data.ancestors := Cedar.Data.Set.mk (x.data.ancestors.elts ++ y.data.ancestors.elts) + data.tags := Cedar.Data.Map.mk (x.data.tags.kvs ++ y.data.tags.kvs) + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn EntityProto) := do + match t.fieldNum with + | 1 => + let x : EntityUID ← Field.guardedParse t + pure (mergeUid · x) + | 2 => + let x : Proto.Map String Value ← Field.guardedParse t + pure (mergeAttrs · x) + | 3 => + let x : Repeated EntityUID ← Field.guardedParse t + pure (mergeAncestors · x) + | 4 => + let x : Proto.Map String Value ← Field.guardedParse t + pure (mergeTags · x) + | _ => + t.wireType.skip + pure id + +instance : Message EntityProto := { + parseField := parseField + merge := merge +} + +end EntityProto + +namespace EntityData + +@[inline] +def mkWf (e : EntityData) : EntityData := + { + attrs := Cedar.Data.Map.make e.attrs.kvs + ancestors := Cedar.Data.Set.make e.ancestors.elts + tags := Cedar.Data.Map.make e.tags.kvs + } + +end EntityData + +namespace EntityProto + +@[inline] +def mkWf (e : EntityProto) : EntityProto := + { + uid := e.uid + data := e.data.mkWf + } + +end EntityProto + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/EntityReference.lean b/cedar-lean/CedarProto/EntityReference.lean new file mode 100644 index 000000000..76a3184f4 --- /dev/null +++ b/cedar-lean/CedarProto/EntityReference.lean @@ -0,0 +1,98 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Enum + +-- Message Dependencies +import CedarProto.EntityUID + +open Proto + +namespace Cedar.Spec + +namespace Proto +inductive EntityReferenceType where + | slot +deriving Inhabited + +namespace EntityReferenceType +@[inline] +def fromInt (n : Int) : Except String EntityReferenceType := + match n with + | 0 => .ok .slot + | n => .error s!"Field {n} does not exist in enum" + +instance : ProtoEnum EntityReferenceType := { + fromInt := fromInt +} +end EntityReferenceType +end Proto + +namespace EntityUIDOrSlot + +deriving instance Inhabited for EntityUIDOrSlot + +@[inline] +def mergeTy (result : EntityUIDOrSlot) (x : Proto.EntityReferenceType) : EntityUIDOrSlot := + -- For enums, if result is already of the same type, then we don't do anything + -- otherwise, we construct a default object of the new type. + match x with + | .slot => match result with + | .entityUID _ => .slot default + | .slot _ => result + +@[inline] +def mergeEuid (result : EntityUIDOrSlot) (x : EntityUID) : EntityUIDOrSlot := + match result with + | .entityUID e => .entityUID (Field.merge e x) + | .slot _ => .entityUID x + +@[inline] +def merge (x : EntityUIDOrSlot) (y : EntityUIDOrSlot) : EntityUIDOrSlot := + match y with + | .entityUID e2 => mergeEuid x e2 + | .slot s2 => match x with + | .entityUID _ => y + | .slot s1 => .slot (Field.merge s1 s2) + + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUIDOrSlot) := do + match t.fieldNum with + | 1 => + let x : Proto.EntityReferenceType ← Field.guardedParse t + pure (mergeTy · x) + | 2 => + let x : EntityUID ← Field.guardedParse t + pure (mergeEuid · x) + | _ => + t.wireType.skip + pure id + +instance : Message EntityUIDOrSlot := { + parseField := parseField + merge := merge +} + +@[inline] +def withSlot (x : EntityUIDOrSlot) (s : SlotID) : EntityUIDOrSlot := + match x with + | .entityUID _ => x + | .slot _ => .slot s + +end EntityUIDOrSlot + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/EntityType.lean b/cedar-lean/CedarProto/EntityType.lean new file mode 100644 index 000000000..b376886fc --- /dev/null +++ b/cedar-lean/CedarProto/EntityType.lean @@ -0,0 +1,62 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message + +-- Message Dependencies +import CedarProto.Name + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.EntityType is defined as +-- abbrev EntityType := Name + +-- Note: We don't want it to automatically reduce like +-- abbrev and @[reducible] as this causes issues +-- with typeclass resolution when calling Field.parse +def EntityTypeProto := Cedar.Spec.Name +deriving Inhabited, DecidableEq, Repr, LT + +namespace EntityTypeProto + +@[inline] +def mergeName (x1 : EntityTypeProto) (x2 : Name) : EntityTypeProto := + (@Field.merge Name) x1 x2 + +@[inline] +def merge (x1 : EntityTypeProto) (x2 : EntityTypeProto) : EntityTypeProto := + mergeName x1 x2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn EntityTypeProto) := do + match t.fieldNum with + | 1 => + let x : Name ← Field.guardedParse t + pure (mergeName · x) + | _ => + t.wireType.skip + pure id + +instance : Message EntityTypeProto := { + parseField := parseField + merge := merge +} + +end EntityTypeProto + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/EntityUID.lean b/cedar-lean/CedarProto/EntityUID.lean new file mode 100644 index 000000000..e914f426c --- /dev/null +++ b/cedar-lean/CedarProto/EntityUID.lean @@ -0,0 +1,73 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityType + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.EntityUID is defined as +-- structure EntityUID where +-- ty : EntityType +-- eid : String + +namespace EntityUID + +@[inline] +def mergeTy (result : EntityUID) (ty : EntityTypeProto) : EntityUID := + {result with + ty := Field.merge result.ty ty + } + +@[inline] +def mergeEid (result : EntityUID) (eid : String) : EntityUID := + {result with + eid := Field.merge result.eid eid + } + +@[inline] +def merge (x1 : EntityUID) (x2 : EntityUID) : EntityUID := + {x1 with + ty := Field.merge x1.ty x2.ty + eid := Field.merge x1.eid x2.eid + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUID) := do + match t.fieldNum with + | 1 => + let x : EntityTypeProto ← Field.guardedParse t + pure (mergeTy · x) + | 2 => + let x : String ← Field.guardedParse t + pure (mergeEid · x) + | _ => + t.wireType.skip + pure id + +instance : Message EntityUID := { + parseField := parseField + merge := merge +} + +end EntityUID + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/EntityUIDEntry.lean b/cedar-lean/CedarProto/EntityUIDEntry.lean new file mode 100644 index 000000000..f37b0687d --- /dev/null +++ b/cedar-lean/CedarProto/EntityUIDEntry.lean @@ -0,0 +1,57 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityUID + +open Proto + +namespace Cedar.Spec + +/-- for the purposes of the Lean implementation, EntityUIDEntry can just be EntityUID -/ +def EntityUIDEntry := EntityUID +deriving instance Inhabited for EntityUIDEntry + +namespace EntityUIDEntry + +@[inline] +def mergeEuid (x1 : EntityUIDEntry) (x2 : EntityUID) : EntityUIDEntry := + (@Field.merge EntityUID) x1 x2 + +@[inline] +def merge (x1 : EntityUIDEntry) (x2 : EntityUIDEntry) : EntityUIDEntry := + mergeEuid x1 x2 + +def parseField (t : Proto.Tag) : BParsec (MergeFn EntityUIDEntry) := do + match t.fieldNum with + | 1 => + let x : EntityUID ← Field.guardedParse t + pure (mergeEuid · x) + | _ => + t.wireType.skip + pure id + +instance : Message EntityUIDEntry := { + parseField := parseField + merge := merge +} + +end EntityUIDEntry + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Expr.lean b/cedar-lean/CedarProto/Expr.lean new file mode 100644 index 000000000..2c0af35fd --- /dev/null +++ b/cedar-lean/CedarProto/Expr.lean @@ -0,0 +1,975 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import Cedar +import Protobuf.Message +import Protobuf.Enum +import Protobuf.Map + +-- Message Dependencies +import CedarProto.EntityUID + +open Proto + +namespace Cedar.Spec + +namespace Prim + +-- Note that Cedar.Spec.Prim is defined as +-- inductive Prim where +-- | bool (b : Bool) +-- | int (i : Int64) +-- | string (s : String) +-- | entityUID (uid : EntityUID) +-- Note: This is the same as Literal in the proto file + +@[inline] +def merge_bool (p : Prim) (b2 : Bool) : Prim := + match p with + | .bool b1 => Prim.bool (Field.merge b1 b2) + | _ => Prim.bool b2 + +@[inline] +def merge_int (_ : Prim) (pi : Proto.Int64) : Prim := + have i : Int := pi + if H1 : i < Cedar.Data.INT64_MIN then + panic!("Integer less than INT64_MIN") + else if H2 : i > Cedar.Data.INT64_MAX then + panic!("Integer greater than INT64_MAX") + else + have h1 : Cedar.Data.INT64_MIN ≤ i ∧ i ≤ Cedar.Data.INT64_MAX := by + unfold Proto.Int64 at * + omega + + -- Override semantics + Prim.int (Cedar.Data.Int64.mk i h1) + +@[inline] +def merge_string (p : Prim) (s2 : String) : Prim := + match p with + | .string s1 => Prim.string (Field.merge s1 s2) + | _ => Prim.string s2 + +@[inline] +def merge_euid (p : Prim) (euid2 : EntityUID) : Prim := + match p with + | .entityUID euid1 => Prim.entityUID (Field.merge euid1 euid2) + | _ => Prim.entityUID euid2 + +@[inline] +def merge (p1 : Prim) (p2 : Prim) : Prim := + match p2 with + | .bool b2 => merge_bool p1 b2 + | .int i2 => + let i2₁ : Int := i2 + let i2₂ : Proto.Int64 := i2₁ + merge_int p1 i2₂ + | .string s2 => merge_string p1 s2 + | .entityUID e2 => merge_euid p1 e2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn Prim) := do + match t.fieldNum with + | 1 => + let x : Bool ← Field.guardedParse t + pure (merge_bool · x) + | 2 => + let x : Int64 ← Field.guardedParse t + pure (merge_int · x) + | 3 => + let x : String ← Field.guardedParse t + pure (merge_string · x) + | 4 => + let x : EntityUID ← Field.guardedParse t + pure (merge_euid · x) + | _ => + t.wireType.skip + pure id + +instance : Message Prim := { + parseField := parseField + merge := merge +} + +end Prim + +namespace Var +@[inline] +def fromInt (n : Int) : Except String Var := + match n with + | 0 => .ok .principal + | 1 => .ok .action + | 2 => .ok .resource + | 3 => .ok .context + | n => .error s!"Field {n} does not exist in enum" + +instance : Inhabited Var where + default := .principal + +instance : ProtoEnum Var := { + fromInt := fromInt +} + +end Var + +namespace Proto + +-- Wrapper type +def ExprKind := Expr + deriving Inhabited + +-- Recursive constructors for Expr +def ExprKind.If := ExprKind +instance : Inhabited ExprKind.If where + default := .ite default default default + +def ExprKind.And := ExprKind +instance : Inhabited ExprKind.And where + default := .and default default + +def ExprKind.Or := ExprKind +instance : Inhabited ExprKind.Or where + default := .or default default + +def ExprKind.UnaryApp := ExprKind +instance : Inhabited ExprKind.UnaryApp where + default := .unaryApp default default + +def ExprKind.BinaryApp := ExprKind +instance : Inhabited ExprKind.BinaryApp where + default := .binaryApp default default default + +def ExprKind.ExtensionFunctionApp := ExprKind +instance : Inhabited ExprKind.ExtensionFunctionApp where + default := .call default default + +def ExprKind.GetAttr := ExprKind +instance : Inhabited ExprKind.GetAttr where + default := .getAttr default default + +def ExprKind.HasAttr := ExprKind +instance : Inhabited ExprKind.HasAttr where + default := .hasAttr default default + +def ExprKind.Like := ExprKind +instance : Inhabited ExprKind.Like where + default := .unaryApp (.like default) default + +def ExprKind.Is := ExprKind +instance : Inhabited ExprKind.Is where + default := .unaryApp (.is default) default + +def ExprKind.Set := ExprKind +instance : Inhabited ExprKind.Set where + default := .set default + +def ExprKind.Record := ExprKind +instance : Inhabited ExprKind.Record where + default := .record default + +end Proto + +def Expr.merge (e1 : Expr) (e2 : Expr) : Expr := + match e1, e2 with + | .lit p1, .lit p2 => .lit (Field.merge p1 p2) + | .var v1, .var v2 => .var (Field.merge v1 v2) + | .ite cond1 then1 else1, .ite cond2 then2 else2 => + .ite (merge cond1 cond2) (merge then1 then2) (merge else1 else2) + | .and left1 right1, .and left2 right2 => + .and (merge left1 left2) (merge right1 right2) + | .or left1 right1, .or left2 right2 => + .or (merge left1 left2) (merge right1 right2) + | .unaryApp op1 e1, .unaryApp op2 e2 => + let newOp := match op1, op2 with + | .like p1, .like p2 => .like (p1 ++ p2) + | .is et1, .is et2 => .is (Field.merge et1 et2) + | _, _ => op2 + .unaryApp newOp (merge e1 e2) + | .binaryApp _ left1 right1, .binaryApp op2 left2 right2 => + .binaryApp op2 (merge left1 left2) (merge right1 right2) + | .getAttr e1 a1, .getAttr e2 a2 => + .getAttr (merge e1 e2) (Field.merge a1 a2) + | .hasAttr e1 a1, .hasAttr e2 a2 => + .hasAttr (merge e1 e2) (Field.merge a1 a2) + | .set es1, .set es2 => .set (es1 ++ es2) + | .record m1, .record m2 => .record (m1 ++ m2) + | .call _ args1, .call fn2 args2 => .call fn2 (args1 ++ args2) + | _, _ => e2 + +namespace Proto.ExprKind.If +@[inline] +def mergeTestExpr (result : ExprKind.If) (x : Expr) : ExprKind.If := + match result with + | .ite testExpr thenExpr elseExpr => .ite (Expr.merge testExpr x) thenExpr elseExpr + | _ => panic!("Expected ExprKind.If to have .ite constructor") + +@[inline] +def mergeThenExpr (result : ExprKind.If) (x : Expr) : ExprKind.If := + match result with + | .ite testExpr thenExpr elseExpr => .ite testExpr (Expr.merge thenExpr x) elseExpr + | _ => panic!("Expected ExprKind.If to have .ite constructor") + +@[inline] +def mergeElseExpr (result : ExprKind.If) (x : Expr) : ExprKind.If := + match result with + | .ite testExpr thenExpr elseExpr => .ite testExpr thenExpr (Expr.merge elseExpr x) + | _ => panic!("Expected ExprKind.If to have .ite constructor") + +@[inline] +def merge (x1 x2 : ExprKind.If) : ExprKind.If := + match x1, x2 with + | .ite c1 t1 e1, .ite c2 t2 e2 => + .ite (Expr.merge c1 c2) (Expr.merge t1 t2) (Expr.merge e1 e2) + | _, _ => panic!("Expected ExprKind.If to have .ite constructor") + +-- parseField requires mutual recursion and thus can be found at the end +-- of the file +end Proto.ExprKind.If + +namespace Proto.ExprKind.And +@[inline] +def mergeLeft (result : ExprKind.And) (x : Expr) : ExprKind.And := + match result with + | .and left right => .and (Expr.merge left x) right + | _ => panic!("Expected ExprKind.And to have .and constructor") + +@[inline] +def mergeRight (result : ExprKind.And) (x : Expr) : ExprKind.And := + match result with + | .and left right => .and left (Expr.merge right x) + | _ => panic!("Expected ExprKind.And to have .and constructor") + +@[inline] +def merge (x1 x2 : ExprKind.And) : ExprKind.And := + match x1, x2 with + | .and l1 r1, .and l2 r2 => + .and (Expr.merge l1 l2) (Expr.merge r1 r2) + | _, _ => panic!("Expected Proto.Expr.And to have .and constructor") + +-- parseField requires mutual recursion and thus can be found at the end +-- of the file +end Proto.ExprKind.And + +namespace Proto.ExprKind.Or +@[inline] +def mergeLeft (result : ExprKind.Or) (x : Expr) : ExprKind.Or := + match result with + | .or left right => .or (Expr.merge left x) right + | _ => panic!("Expected ExprKind.Or to have .or constructor") + +@[inline] +def mergeRight (result : ExprKind.Or) (x : Expr) : ExprKind.Or := + match result with + | .or left right => .or left (Expr.merge right x) + | _ => panic!("Expected ExprKind.Or to have .or constructor") + +@[inline] +def merge (x1 x2 : ExprKind.Or) : ExprKind.Or := + match x1, x2 with + | .or l1 r1, .or l2 r2 => + .or (Expr.merge l1 l2) (Expr.merge r1 r2) + | _, _ => panic!("Expected ExprKind.Or to have .or constructor") + +-- parseField requires mutual recursion and thus can be found at the end +-- of the file +end Proto.ExprKind.Or + +namespace Proto.ExprKind.UnaryApp +inductive Op where + | not + | neg +deriving Inhabited + +namespace Op +@[inline] +def fromInt (n : Int) : Except String Op := + match n with + | 0 => .ok .not + | 1 => .ok .neg + | n => .error s!"Field {n} does not exist in enum" + +instance : Inhabited Op where + default := .not + +instance : ProtoEnum Op := { + fromInt := fromInt +} +end Op + +@[inline] +def mergeOp (result : ExprKind.UnaryApp) (x : Op) : ExprKind.UnaryApp := + -- Since op is an enum, we perform a replacement + match result with + | .unaryApp _ expr => match x with + | .not => .unaryApp .not expr + | .neg => .unaryApp .neg expr + | _ => panic!("Expected ExprKind.UnaryApp to be of constructor .unaryApp") + +@[inline] +def mergeArg (result : ExprKind.UnaryApp) (e2 : Expr) : ExprKind.UnaryApp := + match result with + | .unaryApp op e1 => .unaryApp op (Expr.merge e1 e2) + | _ => panic!("Expected ExprKind.UnaryApp to be of constructor .unaryApp") + +@[inline] +def merge (x1 x2 : ExprKind.UnaryApp) : ExprKind.UnaryApp := + match x1, x2 with + | .unaryApp _ e1, .unaryApp op2 e2 => + .unaryApp op2 (Expr.merge e1 e2) + | _, _ => panic!("Expected ExprKind.UnaryApp to be of constructor .unaryApp") + +-- parseField requires mutual recursion and can be found at the end of the file +end Proto.ExprKind.UnaryApp + +namespace Proto.ExprKind.BinaryApp +inductive Op where + | eq + | less + | lesseq + | add + | sub + | mul + | in + | contains + | containsAll + | containsAny + | getTag + | hasTag +deriving Inhabited + +namespace Op +@[inline] +def fromInt (n : Int) : Except String Op := + match n with + | 0 => .ok .eq + | 1 => .ok .less + | 2 => .ok .lesseq + | 3 => .ok .add + | 4 => .ok .sub + | 5 => .ok .mul + | 6 => .ok .in + | 7 => .ok .contains + | 8 => .ok .containsAll + | 9 => .ok .containsAny + | 10 => .ok .getTag + | 11 => .ok .hasTag + | n => .error s!"Field {n} does not exist in enum" + +instance : Inhabited Op where + default := .eq + +instance : ProtoEnum Op := { + fromInt := fromInt +} +end Op + +@[inline] +def mergeOp (result : ExprKind.BinaryApp) (x : Op) : ExprKind.BinaryApp := + match result with + | .binaryApp _ left right => match x with + | .eq => .binaryApp .eq left right + | .less => .binaryApp .less left right + | .lesseq => .binaryApp .lessEq left right + | .add => .binaryApp .add left right + | .sub => .binaryApp .sub left right + | .mul => .binaryApp .mul left right + | .in => .binaryApp .mem left right + | .contains => .binaryApp .contains left right + | .containsAll => .binaryApp .containsAll left right + | .containsAny => .binaryApp .containsAny left right + | .getTag => .binaryApp .getTag left right + | .hasTag => .binaryApp .hasTag left right + | _ => panic!("Expected ExprKind.BinaryApp to have constructor .binaryApp") + +@[inline] +def mergeLeft (result : ExprKind.BinaryApp) (e2 : Expr) : ExprKind.BinaryApp := + match result with + | .binaryApp op e1 right => .binaryApp op (Expr.merge e1 e2) right + | _ => panic!("Expected ExprKind.BinaryApp to have constructor .binaryApp") + +@[inline] +def mergeRight (result : ExprKind.BinaryApp) (e2 : Expr) : ExprKind.BinaryApp := + match result with + | .binaryApp op left e1 => .binaryApp op left (Expr.merge e1 e2) + | _ => panic!("Expected ExprKind.BinaryApp to have constructor .binaryApp") + +@[inline] +def merge (x1 x2 : ExprKind.BinaryApp) : ExprKind.BinaryApp := + match x1, x2 with + | .binaryApp _ l1 r1, .binaryApp op2 l2 r2 => + .binaryApp op2 (Expr.merge l1 l2) (Expr.merge r1 r2) + | _, _ => panic!("Expected ExprKind.BinaryApp to have constructor .binaryApp") + +-- parseField requires mutual reucrsion and can be found at the end of the file +end Proto.ExprKind.BinaryApp + +namespace Proto.ExprKind.ExtensionFunctionApp +@[inline] +def mergeName (result : ExprKind.ExtensionFunctionApp) (xfn : Name) : ExprKind.ExtensionFunctionApp := + match result with + | .call _ es => match xfn.id with + | "decimal" => .call .decimal es + | "lessThan" => .call .lessThan es + | "lessThanOrEqual" => .call .lessThanOrEqual es + | "greaterThan" => .call .greaterThan es + | "greaterThanOrEqual" => .call .greaterThanOrEqual es + | "ip" => .call .ip es + | "isIpv4" => .call .isIpv4 es + | "isIpv6" => .call .isIpv6 es + | "isLoopback" => .call .isLoopback es + | "isMulticast" => .call .isMulticast es + | "isInRange" => .call .isInRange es + | xfn => panic! s!"mergeName: unknown extension function {xfn}" + | _ => panic!("Expected ExprKind.ExtensionFunctionApp to have constructor .call") + +@[inline] +def mergeArgs (result : ExprKind.ExtensionFunctionApp) (es2 : Array Expr) : ExprKind.ExtensionFunctionApp := + match result with + | .call n1 es1 => .call n1 (es1 ++ es2.toList) + | _ => panic!("Expected ExprKind.ExtensionFunctionApp to have constructor .call") + +@[inline] +def merge (x1 x2 : ExprKind.ExtensionFunctionApp) : ExprKind.ExtensionFunctionApp := + match x1, x2 with + | .call _ args1, .call fn2 args2 => + .call fn2 (args1 ++ args2) + | _, _ => panic!("Expected ExprKind.ExtensionFunctionApp to have constructor .call") + +-- parseFIeld requires mutual recursion and can be found at the end of the file +end Proto.ExprKind.ExtensionFunctionApp + +namespace Proto.ExprKind.GetAttr +@[inline] +def mergeAttr (result : ExprKind.GetAttr) (attr2 : String) : ExprKind.GetAttr := + match result with + | .getAttr expr attr1 => .getAttr expr (Field.merge attr1 attr2) + | _ => panic!("Expected ExprKind.GetAttr to be constructor .getAttr") + +@[inline] +def mergeExpr (result : ExprKind.GetAttr) (e2 : Expr) : ExprKind.GetAttr := + match result with + | .getAttr e1 attr => .getAttr (Expr.merge e1 e2) attr + | _ => panic!("Expected ExprKind.GetAttr to be constructor .getAttr") + +@[inline] +def merge (x1 x2 : ExprKind.GetAttr) : ExprKind.GetAttr := + match x1, x2 with + | .getAttr e1 a1, .getAttr e2 a2 => + .getAttr (Expr.merge e1 e2) (Field.merge a1 a2) + | _, _ => panic!("Expected ExprKind.GetAttr to be constructor .getAttr") + +-- parseField requires mutual recursion and can be found at the end of this file +end Proto.ExprKind.GetAttr + +namespace Proto.ExprKind.HasAttr +@[inline] +def mergeAttr (result : ExprKind.HasAttr) (attr2 : String) : ExprKind.HasAttr := + match result with + | .hasAttr expr attr1 => .hasAttr expr (Field.merge attr1 attr2) + | _ => panic!("Expected ExprKind.HasAttr to be constructor .hasAttr") + +@[inline] +def mergeExpr (result : ExprKind.HasAttr) (e2 : Expr) : ExprKind.HasAttr := + match result with + | .hasAttr e1 attr => .hasAttr (Expr.merge e1 e2) attr + | _ => panic!("Expected ExprKind.HasAttr to be constructor .hasAttr") + +@[inline] +def merge (x1 x2 : ExprKind.HasAttr) : ExprKind.HasAttr := + match x1, x2 with + | .hasAttr e1 a1, .hasAttr e2 a2 => + .hasAttr (Expr.merge e1 e2) (Field.merge a1 a2) + | _, _ => panic!("Expected ExprKind.HasAttr to be constructor .hasAttr") + +-- parseField requires mutual recursion and can be found at the end of this file +end Proto.ExprKind.HasAttr + +namespace PatElem +inductive Ty where + | star +deriving Inhabited + +namespace Ty +def fromInt (n : Int) : Except String Ty := + match n with + | 0 => .ok .star + | n => .error s!"Field {n} does not exist in enum" + +instance : ProtoEnum Ty := { + fromInt := fromInt +} +end Ty + +@[inline] +def mergeTy (_ : PatElem) (x : Ty) : PatElem := + -- With enums we perform replacement + match x with + | .star => .star + +@[inline] +def mergeC (_ : PatElem) (x2 : String) : PatElem := + -- With a single character we'll perform replacement + match x2.data with + | [c2] => .justChar c2 + | _ => panic!("Only expected a single character in PatElem") + +@[inline] +def merge (_ : PatElem) (y : PatElem) : PatElem := + -- Each constructor of the sum type merges through + -- replacement, so we'll do the same here + y + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn PatElem) := do + match t.fieldNum with + | 1 => + let x : Ty ← Field.guardedParse t + pure (λ s => mergeTy s x) + | 2 => + let x : String ← Field.guardedParse t + pure (λ s => mergeC s x) + | _ => + t.wireType.skip + pure id + +instance : Message PatElem := { + parseField := parseField + merge := merge +} +end PatElem + +namespace Proto.ExprKind.Like +@[inline] +def mergeExpr (result : ExprKind.Like) (e2 : Expr) : ExprKind.Like := + match result with + | .unaryApp (.like pat) e1 => .unaryApp (.like pat) (Expr.merge e1 e2) + | _ => panic!("Expected ExprKind.Like to have constructor .unaryApp .like") + +@[inline] +def mergePattern (result : ExprKind.Like) (pat2 : Array PatElem) : ExprKind.Like := + match result with + | .unaryApp (.like pat1) e => .unaryApp (.like (pat1 ++ pat2.toList)) e + | _ => panic!("Expected ExprKind.Like to have constructor .unaryApp .like") + +@[inline] +def merge (x1 x2 : ExprKind.Like) : ExprKind.Like := + match x1, x2 with + | .unaryApp (.like p1) e1, .unaryApp (.like p2) e2 => + .unaryApp (.like (p1 ++ p2)) (Expr.merge e1 e2) + | _, _ => panic!("Expected ExprKind.Like to have constructor .unaryApp .like") + +-- parseField relies on mutual recursion and can be found at the end of the file +end Proto.ExprKind.Like + +namespace Proto.ExprKind.Is +@[inline] +def mergeExpr (result : ExprKind.Is) (e2 : Expr) : ExprKind.Is := + match result with + | .unaryApp (.is et) e1 => .unaryApp (.is et) (Expr.merge e1 e2) + | _ => panic!("Expected ExprKind.Is to have constructor .unaryApp .is") + +@[inline] +def mergeEt (result : ExprKind.Is) (et2 : EntityTypeProto) : ExprKind.Is := + match result with + | .unaryApp (.is et1) e => .unaryApp (.is (Field.merge et1 et2)) e + | _ => panic!("Expected ExprKind.Is to have constructor .unaryApp .is") + +@[inline] +def merge (x1 x2 : ExprKind.Is) : ExprKind.Is := + match x1, x2 with + | .unaryApp (.is et1) e1, .unaryApp (.is et2) e2 => + .unaryApp (.is (Field.merge et1 et2)) (Expr.merge e1 e2) + | _, _ => panic!("Expected ExprKind.Is to have constructor .unaryApp .is") + +-- parseField relies on mutual recursion and can be found at the end of the file +end Proto.ExprKind.Is + +namespace Proto.ExprKind.Set +@[inline] +def mergeElems (result : ExprKind.Set) (es2 : Array Expr) : ExprKind.Set := + match result with + | .set es1 => .set (es1 ++ es2.toList) + | _ => panic!("Expected ExprKind.Set to have the .set constructor") + +@[inline] +def merge (x1 x2 : ExprKind.Set) : ExprKind.Set := + match x1, x2 with + | .set es1, .set es2 => .set (es1 ++ es2) + | _, _ => panic!("Expected ExprKind.Set to have the .set constructor") + +-- parseField relies on mutual recursion and can be found at the +-- end of the file +end Proto.ExprKind.Set + +namespace Proto.ExprKind.Record +@[inline] +def mergeItems (result : ExprKind.Record) (its2 : Array (String × Expr)) : ExprKind.Record := + match result with + | .record its1 => .record (its1 ++ its2.toList) + | _ => panic!("Expected ExprKind.Record to have constructor .record") + +@[inline] +def merge (x1 x2 : ExprKind.Record) : ExprKind.Record := + match x1, x2 with + | .record items1, .record items2 => .record (items1 ++ items2) + | _, _ => panic!("Expected ExprKind.Record to have constructor .record") + +-- parseField relies on mutual recursion and can be found at the +-- end of the file +end Proto.ExprKind.Record + +namespace Proto.ExprKind + +@[inline] +def mergePrim (result : ExprKind) (p2 : Prim) : ExprKind := + match result with + | .lit p1 => .lit (Field.merge p1 p2) + | _ => .lit p2 + +@[inline] +def mergeVar (result : ExprKind) (v2 : Var) : ExprKind := + match result with + | .var v1 => .var (Field.merge v1 v2) + | _ => .var v2 + +@[inline] +def mergeIf (result : ExprKind) (x : ExprKind.If) : ExprKind := + match result with + | .ite _ _ _ => ExprKind.If.merge result x + | _ => x + +@[inline] +def mergeAnd (result : ExprKind) (x : ExprKind.And) : ExprKind := + match result with + | .and _ _ => ExprKind.And.merge result x + | _ => x + +@[inline] +def mergeOr (result : ExprKind) (x : ExprKind.Or) : ExprKind := + match result with + | .or _ _ => ExprKind.Or.merge result x + | _ => x + +@[inline] +def mergeUApp (result : ExprKind) (x : ExprKind.UnaryApp) : ExprKind := + match result with + | .unaryApp _ _ => ExprKind.UnaryApp.merge result x + | _ => x + +@[inline] +def mergeBApp (result : ExprKind) (x : ExprKind.BinaryApp) : ExprKind := + match result with + | .binaryApp _ _ _ => ExprKind.BinaryApp.merge result x + | _ => x + +@[inline] +def mergeExtApp (result : ExprKind) (x : ExprKind.ExtensionFunctionApp) : ExprKind := + match result with + | .call _ _ => ExprKind.ExtensionFunctionApp.merge result x + | _ => x + +@[inline] +def mergeGetAttr (result : ExprKind) (x : ExprKind.GetAttr) : ExprKind := + match result with + | .getAttr _ _ => ExprKind.GetAttr.merge result x + | _ => x + +@[inline] +def mergeHasAttr (result : ExprKind) (x : ExprKind.HasAttr) : ExprKind := + match result with + | .hasAttr _ _ => ExprKind.HasAttr.merge result x + | _ => x + +@[inline] +def mergeLike (result : ExprKind) (x : ExprKind.Like) : ExprKind := + match result with + | .unaryApp (.like _) _ => ExprKind.Like.merge result x + | _ => x + +@[inline] +def mergeIs (result : ExprKind) (x : ExprKind.Is) : ExprKind := + match result with + | .unaryApp (.is _) _ => ExprKind.Is.merge result x + | _ => x + +@[inline] +def mergeSet (result : ExprKind) (x : ExprKind.Set) : ExprKind := + match result with + | .set _ => ExprKind.Set.merge result x + | _ => x + +@[inline] +def mergeRecord (result : ExprKind) (x : ExprKind.Record) : ExprKind := + match result with + | .record _ => ExprKind.Record.merge result x + | _ => x + +@[inline] +def merge (x1 x2 : ExprKind) : ExprKind := + Expr.merge x1 x2 + +-- parseField relies on mutual recursion which can be found at the +-- 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 + +partial def Proto.ExprKind.If.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.If → Proto.ExprKind.If) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.If.mergeTestExpr · x) + | 2 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.If.mergeThenExpr · x) + | 3 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.If.mergeElseExpr · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.And.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.And → Proto.ExprKind.And) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.And.mergeLeft · x) + | 2 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.And.mergeRight · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.Or.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.Or → Proto.ExprKind.Or) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.Or.mergeLeft · x) + | 2 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.Or.mergeRight · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.UnaryApp.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.UnaryApp → Proto.ExprKind.UnaryApp) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Proto.ExprKind.UnaryApp.Op ← Field.guardedParse t + pure (Proto.ExprKind.UnaryApp.mergeOp · x) + | 2 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.UnaryApp.mergeArg · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.BinaryApp.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.BinaryApp → Proto.ExprKind.BinaryApp) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Proto.ExprKind.BinaryApp.Op ← Field.guardedParse t + pure (λ s => Proto.ExprKind.BinaryApp.mergeOp s x) + | 2 => + let x : Expr ← Field.guardedParse t + pure (λ s => Proto.ExprKind.BinaryApp.mergeLeft s x) + | 3 => + let x : Expr ← Field.guardedParse t + pure (λ s => Proto.ExprKind.BinaryApp.mergeRight s x) + | _ => + t.wireType.skip + pure (λ s => s) + +partial def Proto.ExprKind.ExtensionFunctionApp.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.ExtensionFunctionApp → Proto.ExprKind.ExtensionFunctionApp) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Name ← Field.guardedParse t + pure (Proto.ExprKind.ExtensionFunctionApp.mergeName · x) + | 2 => + let x : Repeated Expr ← Field.guardedParse t + pure (Proto.ExprKind.ExtensionFunctionApp.mergeArgs · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.GetAttr.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.GetAttr → Proto.ExprKind.GetAttr) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.GetAttr.mergeExpr · x) + | 2 => + let x : String ← Field.guardedParse t + pure (Proto.ExprKind.GetAttr.mergeAttr · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.HasAttr.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.HasAttr → Proto.ExprKind.HasAttr) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.HasAttr.mergeExpr · x) + | 2 => + let x : String ← Field.guardedParse t + pure (Proto.ExprKind.HasAttr.mergeAttr · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.Like.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.Like → Proto.ExprKind.Like) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.Like.mergeExpr · x) + | 2 => + let x : Repeated PatElem ← Field.guardedParse t + pure (Proto.ExprKind.Like.mergePattern · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.Is.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.Is → Proto.ExprKind.Is) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Expr ← Field.guardedParse t + pure (Proto.ExprKind.Is.mergeExpr · x) + | 2 => + let x : EntityTypeProto ← Field.guardedParse t + pure (Proto.ExprKind.Is.mergeEt · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.Set.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.Set → Proto.ExprKind.Set) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Repeated Expr ← Field.guardedParse t + pure (Proto.ExprKind.Set.mergeElems · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.Record.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind.Record → Proto.ExprKind.Record) := do + have : Message Expr := { parseField := Expr.parseField, merge := Expr.merge } + match t.fieldNum with + | 1 => + let x : Proto.Map String Expr ← Field.guardedParse t + pure (Proto.ExprKind.Record.mergeItems · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.ExprKind.parseField (t : Proto.Tag) : BParsec (Proto.ExprKind → Proto.ExprKind) := 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 } + have : Message Proto.ExprKind.UnaryApp := { parseField := Proto.ExprKind.UnaryApp.parseField, merge := Proto.ExprKind.UnaryApp.merge } + have : Message Proto.ExprKind.BinaryApp := { parseField := Proto.ExprKind.BinaryApp.parseField, merge := Proto.ExprKind.BinaryApp.merge } + have : Message Proto.ExprKind.ExtensionFunctionApp := { parseField := Proto.ExprKind.ExtensionFunctionApp.parseField, merge := Proto.ExprKind.ExtensionFunctionApp.merge } + have : Message Proto.ExprKind.GetAttr := { parseField := Proto.ExprKind.GetAttr.parseField, merge := Proto.ExprKind.GetAttr.merge } + have : Message Proto.ExprKind.HasAttr := { parseField := Proto.ExprKind.HasAttr.parseField, merge := Proto.ExprKind.HasAttr.merge } + have : Message Proto.ExprKind.Like := { parseField := Proto.ExprKind.Like.parseField, merge := Proto.ExprKind.Like.merge } + have : Message Proto.ExprKind.Is := { parseField := Proto.ExprKind.Is.parseField, merge := Proto.ExprKind.Is.merge } + 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 + pure (Proto.ExprKind.mergePrim · x) + | 2 => + let x : Var ← Field.guardedParse t + pure (Proto.ExprKind.mergeVar · x) + | 4 => + let x : Proto.ExprKind.If ← Field.guardedParse t + pure (Proto.ExprKind.mergeIf · x) + | 5 => + let x : Proto.ExprKind.And ← Field.guardedParse t + pure (Proto.ExprKind.mergeAnd · x) + | 6 => + let x : Proto.ExprKind.Or ← Field.guardedParse t + pure (Proto.ExprKind.mergeOr · x) + | 7 => + let x : Proto.ExprKind.UnaryApp ← Field.guardedParse t + pure (Proto.ExprKind.mergeUApp · x) + | 8 => + let x : Proto.ExprKind.BinaryApp ← Field.guardedParse t + pure (Proto.ExprKind.mergeBApp · x) + | 9 => + let x : Proto.ExprKind.ExtensionFunctionApp ← Field.guardedParse t + pure (Proto.ExprKind.mergeExtApp · x) + | 10 => + let x : Proto.ExprKind.GetAttr ← Field.guardedParse t + pure (Proto.ExprKind.mergeGetAttr · x) + | 11 => + let x : Proto.ExprKind.HasAttr ← Field.guardedParse t + pure (Proto.ExprKind.mergeHasAttr · x) + | 12 => + let x : Proto.ExprKind.Like ← Field.guardedParse t + pure (Proto.ExprKind.mergeLike · x) + | 13 => + let x : Proto.ExprKind.Is ← Field.guardedParse t + pure (Proto.ExprKind.mergeIs · x) + | 14 => + let x : Proto.ExprKind.Set ← Field.guardedParse t + pure (Proto.ExprKind.mergeSet · x) + | 15 => + let x : Proto.ExprKind.Record ← Field.guardedParse t + pure (Proto.ExprKind.mergeRecord · x) + | _ => + t.wireType.skip + pure id + +partial def Expr.parseField (t : Proto.Tag) : BParsec (Expr → 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 (Expr.mergeExprKind · x) + | _ => + t.wireType.skip + pure id + +end + +instance : Message Expr := { + parseField := Expr.parseField + merge := Expr.merge +} + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/LiteralPolicy.lean b/cedar-lean/CedarProto/LiteralPolicy.lean new file mode 100644 index 000000000..1a262b4df --- /dev/null +++ b/cedar-lean/CedarProto/LiteralPolicy.lean @@ -0,0 +1,98 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.EntityUID + +open Proto + +namespace Cedar.Spec + +namespace TemplateLinkedPolicy + +-- Note that Cedar.Spec.TemplateLinkedPolicy is defined as +-- structure TemplateLinkedPolicy where +-- id : PolicyID +-- templateId : TemplateID +-- slotEnv : SlotEnv +deriving instance Inhabited for TemplateLinkedPolicy + + +@[inline] +def mergeId (result : TemplateLinkedPolicy) (x : String) : TemplateLinkedPolicy := + {result with + id := Field.merge result.id x + } + +@[inline] +def mergeTemplateId (result : TemplateLinkedPolicy) (x : String) : TemplateLinkedPolicy := + {result with + templateId := Field.merge result.templateId x + } + +@[inline] +def mergePrincipalEuid (result : TemplateLinkedPolicy) (x : EntityUID) : TemplateLinkedPolicy := + {result with + slotEnv := Cedar.Data.Map.mk (("?principal", x) :: result.slotEnv.kvs) + } + +@[inline] +def mergeResourceEuid (result : TemplateLinkedPolicy) (x : EntityUID) : TemplateLinkedPolicy := + {result with + slotEnv := Cedar.Data.Map.mk (("?resource", x) :: result.slotEnv.kvs) + } + +@[inline] +def merge (x : TemplateLinkedPolicy) (y : TemplateLinkedPolicy) : TemplateLinkedPolicy := + { + id := Field.merge x.id y.id + templateId := Field.merge x.id y.id + slotEnv := Cedar.Data.Map.mk (x.slotEnv.kvs ++ y.slotEnv.kvs) + } + +def parseField (t : Proto.Tag) : BParsec (MergeFn TemplateLinkedPolicy) := do + match t.fieldNum with + | 1 => + let x : String ← Field.guardedParse t + pure (mergeTemplateId · x) + | 2 => + let x : String ← Field.guardedParse t + pure (mergeId · x) + | 4 => + let x : EntityUID ← Field.guardedParse t + pure (mergePrincipalEuid · x) + | 5 => + let x : EntityUID ← Field.guardedParse t + pure (mergeResourceEuid · x) + | _ => + t.wireType.skip + pure (λ s => s) + +instance : Message TemplateLinkedPolicy := { + parseField := parseField + merge := merge +} + +@[inline] +def mkWf (t : TemplateLinkedPolicy) : TemplateLinkedPolicy := + {t with + slotEnv := Cedar.Data.Map.make t.slotEnv.kvs + } + +end TemplateLinkedPolicy + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/LiteralPolicySet.lean b/cedar-lean/CedarProto/LiteralPolicySet.lean new file mode 100644 index 000000000..2ad6da123 --- /dev/null +++ b/cedar-lean/CedarProto/LiteralPolicySet.lean @@ -0,0 +1,90 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.TemplateBody +import CedarProto.LiteralPolicy + +open Proto + +namespace Cedar.Spec + +structure LiteralPolicySet where + templates : Array (String × Template) + links : Array (String × TemplateLinkedPolicy) +deriving Inhabited + +namespace LiteralPolicySet + +@[inline] +def mergeTemplates (result : LiteralPolicySet) (x : Array (String × Template)) : LiteralPolicySet := + {result with + templates := result.templates ++ x + } + +@[inline] +def mergeLinks (result : LiteralPolicySet) (x : Array (String × TemplateLinkedPolicy)) : LiteralPolicySet := + {result with + links := result.links ++ x + } + +@[inline] +def merge (x y : LiteralPolicySet) : LiteralPolicySet := + { + templates := x.templates ++ y.templates + links := x.links ++ y.links + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn LiteralPolicySet) := do + match t.fieldNum with + | 1 => + let x : Proto.Map String Template ← Field.guardedParse t + pure (mergeTemplates · x) + | 2 => + let x : Proto.Map String TemplateLinkedPolicy ← Field.guardedParse t + pure (mergeLinks · x) + | _ => + t.wireType.skip + pure id + +instance : Message LiteralPolicySet := { + parseField := parseField + merge := merge +} + +end LiteralPolicySet + + +namespace Policies + +@[inline] +def fromLiteralPolicySet (x : LiteralPolicySet) : Policies := + let templates := Cedar.Data.Map.make x.templates.toList + let links := x.links.map (λ ⟨id, p⟩ => (p.mergeId id).mkWf) + match link? templates links.toList with + | .ok policies => policies + | .error e => panic!(s!"fromLiteralPolicySet: failed to link templates: {e}\n templates: {repr templates}\n links: {repr links.toList}}") + +@[inline] +private def merge (x y : Policies) : Policies := + x ++ y + +instance : Field Policies := Field.fromInterField fromLiteralPolicySet merge + +end Policies +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Name.lean b/cedar-lean/CedarProto/Name.lean new file mode 100644 index 000000000..b5311b623 --- /dev/null +++ b/cedar-lean/CedarProto/Name.lean @@ -0,0 +1,67 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +open Proto + +namespace Cedar.Spec.Name + +-- Note that Cedar.Spec.Name is defined as +-- structure Name where +-- id : String +-- path : List String +-- deriving Inhabited, Repr, DecidableEq + +@[inline] +def mergeId (result : Name) (x : String) : Name := + {result with + id := Field.merge result.id x + } + +@[inline] +def mergePath (result : Name) (path_elem : Repeated String) : Name := + {result with + path := result.path ++ path_elem.toList + } + +@[inline] +def merge (x y : Name) : Name := + { + id := Field.merge x.id y.id + path := x.path ++ y.path + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn Name) := do + match t.fieldNum with + | 1 => + let x : String ← Field.guardedParse t + pure (mergeId · x) + | 2 => + let x : Repeated String ← Field.guardedParse t + pure (mergePath · x) + | _ => + t.wireType.skip + pure (λ s => s) + +instance : Message Name := { + parseField := parseField + merge := merge +} + +end Cedar.Spec.Name diff --git a/cedar-lean/CedarProto/PrincipalConstraint.lean b/cedar-lean/CedarProto/PrincipalConstraint.lean new file mode 100644 index 000000000..9846f7b09 --- /dev/null +++ b/cedar-lean/CedarProto/PrincipalConstraint.lean @@ -0,0 +1,55 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.PrincipalOrResourceConstraint + +open Proto + +namespace Cedar.Spec +namespace PrincipalScopeTemplate + +deriving instance Inhabited for PrincipalScopeTemplate + + +@[inline] +def mergeConstraint (result : PrincipalScopeTemplate) (x : Cedar.Spec.ScopeTemplate) : PrincipalScopeTemplate := + have ⟨ sc1 ⟩ := result + .principalScope (ScopeTemplate.merge sc1 (x.withSlot "?principal")) + +@[inline] +def merge (x : PrincipalScopeTemplate) (y : PrincipalScopeTemplate) : PrincipalScopeTemplate := + have ⟨ sc1 ⟩ := x + have ⟨ sc2 ⟩ := y + .principalScope (ScopeTemplate.merge sc1 sc2) + +def parseField (t : Proto.Tag) : BParsec (MergeFn PrincipalScopeTemplate) := do + match t.fieldNum with + | 1 => + let x : ScopeTemplate ← Field.guardedParse t + pure (mergeConstraint · x) + | _ => + t.wireType.skip + pure id + +instance : Message PrincipalScopeTemplate := { + parseField := parseField + merge := merge +} + +end PrincipalScopeTemplate +end Cedar.Spec diff --git a/cedar-lean/CedarProto/PrincipalOrResourceConstraint.lean b/cedar-lean/CedarProto/PrincipalOrResourceConstraint.lean new file mode 100644 index 000000000..c3b6e292d --- /dev/null +++ b/cedar-lean/CedarProto/PrincipalOrResourceConstraint.lean @@ -0,0 +1,299 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.EntityReference +import CedarProto.EntityType + +open Proto + +namespace Cedar.Spec + +namespace Proto +-- Constructors for ScopeTemplate + +inductive ScopeTemplate.Ty where + | any +deriving Inhabited + +def ScopeTemplate.In := ScopeTemplate +def ScopeTemplate.Eq := ScopeTemplate +def ScopeTemplate.Is := ScopeTemplate +def ScopeTemplate.IsIn := ScopeTemplate +end Proto + +namespace Proto.ScopeTemplate.Ty +@[inline] +def fromInt (n : Int) : Except String ScopeTemplate.Ty := + match n with + | 0 => .ok .any + | n => .error s!"Field {n} does not exist in enum" + +instance : ProtoEnum ScopeTemplate.Ty := { + fromInt := fromInt +} +end Proto.ScopeTemplate.Ty + +namespace Proto.ScopeTemplate.In +instance : Inhabited ScopeTemplate.In where + default := .mem default +@[inline] +def mergeER (result : ScopeTemplate.In) (e2 : EntityUIDOrSlot) : ScopeTemplate.In := + match result with + | .mem e1 => .mem (Field.merge e1 e2) + | _ => panic!("ScopeTemplate.In expected ScopeTemplate constructor to be set to .in") + +@[inline] +def merge (x1 x2 : ScopeTemplate.In) : ScopeTemplate.In := + have e2 := match x2 with + | .mem e => e + | _ => panic!("ScopeTemplate.In expected ScopeTemplate constructor to be set to .in") + mergeER x1 e2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ScopeTemplate.In) := do + match t.fieldNum with + | 1 => + let x : EntityUIDOrSlot ← Field.guardedParse t + pure (mergeER · x) + | _ => + t.wireType.skip + pure id + +instance : Message ScopeTemplate.In := { + parseField := parseField + merge := merge +} +end Proto.ScopeTemplate.In + +namespace Proto.ScopeTemplate.Eq +instance : Inhabited ScopeTemplate.Eq where + default := .eq default + +@[inline] +def mergeER (result : ScopeTemplate.Eq) (e2 : EntityUIDOrSlot) : ScopeTemplate.Eq := + match result with + | .eq e1 => .eq (Field.merge e1 e2) + | _ => panic!("ScopeTemplate.Eq expected ScopeTemplate constructor to be set to .eq") + +@[inline] +def merge (x1 x2 : ScopeTemplate.Eq) : ScopeTemplate.Eq := + have e2 := match x2 with + | .eq e => e + | _ => panic!("ScopeTemplate.Eq expected ScopeTemplate constructor to be set to .eq") + mergeER x1 e2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ScopeTemplate.Eq) := do + match t.fieldNum with + | 1 => + let x : EntityUIDOrSlot ← Field.guardedParse t + pure (mergeER · x) + | _ => + t.wireType.skip + pure id + +instance : Message ScopeTemplate.Eq := { + parseField := parseField + merge := merge +} +end Proto.ScopeTemplate.Eq + +namespace Proto.ScopeTemplate.Is +instance : Inhabited ScopeTemplate.Is where + default := .is default + +@[inline] +def mergeET (result : ScopeTemplate.Is) (e2 : EntityTypeProto) : ScopeTemplate.Is := + match result with + | .is e1 => .is (Field.merge e1 e2) + | _ => panic!("ScopeTemplate.Is expected ScopeTemplate constructor to be set to .is") + +@[inline] +def merge (x1 x2 : ScopeTemplate.Is) : ScopeTemplate.Is := + have e2 := match x2 with + | .is e => e + | _ => panic!("ScopeTemplate.Is expected ScopeTemplate constructor to be set to .is") + mergeET x1 e2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ScopeTemplate.Is) := do + match t.fieldNum with + | 1 => + let x : EntityTypeProto ← Field.guardedParse t + pure (mergeET · x) + | _ => + t.wireType.skip + pure id + +instance : Message ScopeTemplate.Is := { + parseField := parseField + merge := merge +} +end Proto.ScopeTemplate.Is + +namespace Proto.ScopeTemplate.IsIn +instance : Inhabited ScopeTemplate.IsIn where + default := .isMem default default + +@[inline] +def mergeER (result : ScopeTemplate.IsIn) (er2 : EntityUIDOrSlot) : ScopeTemplate.IsIn := + match result with + | .isMem et er1 => .isMem et (Field.merge er1 er2) + | _ => panic!("ScopeTemplate.IsIn expected ScopeTemplate constructor to be set to .isMem") + +@[inline] +def mergeET (result : ScopeTemplate.IsIn) (et2 : EntityTypeProto) : ScopeTemplate.IsIn := + match result with + | .isMem et1 er => .isMem (Field.merge et1 et2) er + | _ => panic!("ScopeTemplate.IsIn expected ScopeTemplate constructor to be set to .isMem") + +@[inline] +def merge (x1 x2 : ScopeTemplate.IsIn) : ScopeTemplate.IsIn := + have ⟨et2, er2⟩ := match x2 with + | .isMem et er => (et, er) + | _ => panic!("ScopeTemplate.IsIn expected ScopeTemplate constructor to be set to .isMem") + match x1 with + | .isMem et1 er1 => .isMem (Field.merge et1 et2) (Field.merge er1 er2) + | _ => panic!("ScopeTemplate.IsIn expected ScopeTemplate constructor to be set to .isMem") + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ScopeTemplate.IsIn) := do + match t.fieldNum with + | 1 => + let x : EntityUIDOrSlot ← Field.guardedParse t + pure (mergeER · x) + | 2 => + let x : EntityTypeProto ← Field.guardedParse t + pure (mergeET · x) + | _ => + t.wireType.skip + pure id + +instance : Message ScopeTemplate.IsIn := { + parseField := parseField + merge := merge +} +end Proto.ScopeTemplate.IsIn + +namespace ScopeTemplate + +-- Note that Cedar.Spec.ScopeTemplate is defined as +-- inductive ScopeTemplate where +-- | any +-- | eq (entityOrSlot : EntityUIDOrSlot) +-- | mem (entityOrSlot : EntityUIDOrSlot) +-- | is (ety : EntityType) +-- | isMem (ety : EntityType) (entityOrSlot : EntityUIDOrSlot) +deriving instance Inhabited for ScopeTemplate + + +deriving instance Inhabited for EntityUIDOrSlot + +@[inline] +def mergeTy (_ : ScopeTemplate) (x : Proto.ScopeTemplate.Ty) : ScopeTemplate := + match x with + | .any => .any + +@[inline] +def mergeIn (result : ScopeTemplate) (x : Proto.ScopeTemplate.In) : ScopeTemplate := + have er2 := match x with + | .mem e => e + | _ => panic!("Proto.ScopeTemplate.In expected to have constructor .mem") + match result with + | .mem er1 => .mem (Field.merge er1 er2) + | _ => .mem er2 + +@[inline] +def mergeEq (result : ScopeTemplate) (x : Proto.ScopeTemplate.Eq) : ScopeTemplate := + have er2 := match x with + | .eq e => e + | _ => panic!("Proto.ScopeTemplate.Eq expected to have constructor .eq") + match result with + | .eq er1 => .eq (Field.merge er1 er2) + | _ => .eq er2 + +@[inline] +def mergeIs (result : ScopeTemplate) (x : Proto.ScopeTemplate.Is) : ScopeTemplate := + have et2 := match x with + | .is e => e + | _ => panic!("Proto.ScopeTemplate.Is expected to have constructor .is") + match result with + | .is et1 => .is (Field.merge et1 et2) + | _ => .is et2 + +@[inline] +def mergeIsIn (result : ScopeTemplate) (x : Proto.ScopeTemplate.IsIn) : ScopeTemplate := + have ⟨et2, er2⟩ := match x with + | .isMem et er => (et, er) + | _ => panic!("Proto.ScopeTemplate.IsIn expected to have constructor .isMem") + match result with + | .isMem et1 er1 => .isMem (Field.merge et1 et2) (Field.merge er1 er2) + | _ => .isMem et2 er2 + + +@[inline] +def merge (x1 : ScopeTemplate) (x2 : ScopeTemplate) : ScopeTemplate := + -- If x1 and x2 have different constructors, then + -- return x2, otherwise merge the fields + match x1, x2 with + | .any, .any => .any + | .mem e1, .mem e2 => .mem (Field.merge e1 e2) + | .eq e1, .eq e2 => .eq (Field.merge e1 e2) + | .is n1, .is n2 => .is (Field.merge n1 n2) + | .isMem n1 e1, .isMem n2 e2 => .isMem (Field.merge n1 n2) (Field.merge e1 e2) + | _, _ => x2 + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn ScopeTemplate) := do + match t.fieldNum with + | 1 => + let x : Proto.ScopeTemplate.Ty ← Field.guardedParse t + pure (mergeTy · x) + | 2 => + let x : Proto.ScopeTemplate.In ← Field.guardedParse t + pure (mergeIn · x) + | 3 => + let x : Proto.ScopeTemplate.Eq ← Field.guardedParse t + pure (mergeEq · x) + | 4 => + let x : Proto.ScopeTemplate.Is ← Field.guardedParse t + pure (mergeIs · x) + | 5 => + let x : Proto.ScopeTemplate.IsIn ← Field.guardedParse t + pure (mergeIsIn · x) + | _ => + t.wireType.skip + pure id + +instance : Message ScopeTemplate := { + parseField := parseField + merge := merge +} + +@[inline] +def withSlot (x : ScopeTemplate) (s : SlotID) : ScopeTemplate := + match x with + | .any => .any + | .mem er => .mem (er.withSlot s) + | .eq er => .eq (er.withSlot s) + | .is et => .is et + | .isMem et er => .isMem et (er.withSlot s) + +end ScopeTemplate + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Request.lean b/cedar-lean/CedarProto/Request.lean new file mode 100644 index 000000000..f0c1177bd --- /dev/null +++ b/cedar-lean/CedarProto/Request.lean @@ -0,0 +1,97 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityUIDEntry +import CedarProto.Value +import CedarProto.Context + +open Proto + +namespace Cedar.Spec + +-- Note that Cedar.Spec.Request is defined as +-- structure Request where +-- principal : EntityUID +-- action : EntityUID +-- resource : EntityUID +-- context : Map Attr Value + +namespace Request + +@[inline] +def mergePrincipal (result : Request) (x : EntityUIDEntry) : Request := + {result with + principal := Field.merge result.principal x + } + +@[inline] +def mergeAction (result : Request) (x : EntityUIDEntry) : Request := + {result with + action := Field.merge result.action x + } + +@[inline] +def mergeResource (result : Request) (x : EntityUIDEntry) : Request := + {result with + resource := Field.merge result.resource x + } + +@[inline] +def mergeContext (result : Request) (x : Context) : Request := + {result with + context := (@Field.merge Context) result.context x + } + +@[inline] +def merge (x : Request) (y : Request) : Request := + { + principal := Field.merge x.principal y.principal + action := Field.merge x.action y.action + resource := Field.merge x.resource y.resource + context := (@Field.merge Context) x.context y.context + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn Request) := do + match t.fieldNum with + | 1 => + let x : EntityUIDEntry ← Field.guardedParse t + pure (mergePrincipal · x) + | 2 => + let x : EntityUIDEntry ← Field.guardedParse t + pure (mergeAction · x) + | 3 => + let x : EntityUIDEntry ← Field.guardedParse t + pure (mergeResource · x) + | 4 => + let x : Context ← Field.guardedParse t + pure (mergeContext · x) + | _ => + t.wireType.skip + pure id + +instance : Message Request := { + parseField := parseField + merge := merge +} + +end Request + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/ResourceConstraint.lean b/cedar-lean/CedarProto/ResourceConstraint.lean new file mode 100644 index 000000000..249872312 --- /dev/null +++ b/cedar-lean/CedarProto/ResourceConstraint.lean @@ -0,0 +1,55 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.PrincipalOrResourceConstraint + +open Proto + +namespace Cedar.Spec + +namespace ResourceScopeTemplate + +deriving instance Inhabited for ResourceScopeTemplate + + +@[inline] +def mergeConstraint (result : ResourceScopeTemplate) (x : ScopeTemplate) : ResourceScopeTemplate := + let ⟨ sc1 ⟩ := result + .resourceScope (ScopeTemplate.merge sc1 (x.withSlot "?resource")) + +@[inline] +def merge (x : ResourceScopeTemplate) (y : ResourceScopeTemplate) : ResourceScopeTemplate := + let ⟨ sc1 ⟩ := x + let ⟨ sc2 ⟩ := y + .resourceScope (ScopeTemplate.merge sc1 sc2) + +def parseField (t : Proto.Tag) : BParsec (MergeFn ResourceScopeTemplate) := do + match t.fieldNum with + | 1 => + let x : ScopeTemplate ← Field.guardedParse t + pure (mergeConstraint · x) + | _ => + t.wireType.skip + pure id + +instance : Message ResourceScopeTemplate := { + parseField := parseField + merge := merge +} + +end ResourceScopeTemplate diff --git a/cedar-lean/CedarProto/TemplateBody.lean b/cedar-lean/CedarProto/TemplateBody.lean new file mode 100644 index 000000000..8a7c17719 --- /dev/null +++ b/cedar-lean/CedarProto/TemplateBody.lean @@ -0,0 +1,146 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar + +-- Message Dependencies +import CedarProto.Expr +import CedarProto.PrincipalConstraint +import CedarProto.ActionConstraint +import CedarProto.ResourceConstraint + +open Proto + +namespace Cedar.Spec + +namespace Effect +def fromInt (n : Int) : Except String Effect := + match n with + | 0 => .ok .forbid + | 1 => .ok .permit + | n => .error s!"Field {n} does not exist in enum" + +instance : Inhabited Effect := { + default := .forbid +} + +instance : ProtoEnum Effect := { + fromInt := fromInt +} +end Effect + +namespace Conditions + +@[inline] +def merge (c1 c2 : Conditions) : Conditions := + c1 ++ c2 + +-- Emulating the behavior from the JSON parser +-- where it is assumed that conditions are formed +-- from one condition of type "when" +@[inline] +private def fromExpr (e : Expr) : Conditions := + [{kind := .when, body := e}] + +instance : Field Conditions := Field.fromInterField fromExpr merge + +end Conditions + +namespace Template + +-- Note that Cedar.Spec.Template is defined as +-- structure Template where +-- effect : Effect +-- principalScope : PrincipalScopeTemplate +-- actionScope : ActionScope +-- resourceScope : ResourceScopeTemplate +-- condition : Conditions + +-- Forbid is the default for Rust protobuf, but Lean auto-derives `permit` as +-- the default. We use a manual derivation here to resolve the discrepancy. +instance : Inhabited Effect where default := .forbid +deriving instance Inhabited for Template -- must come after the Inhabited Effect instance + +@[inline] +def mergeEffect (result : Template) (x : Effect) : Template := + {result with + effect := Field.merge result.effect x + } + +@[inline] +def mergePrincipalScope (result : Template) (x : PrincipalScopeTemplate) : Template := + {result with + principalScope := Field.merge result.principalScope x + } + +@[inline] +def mergeActionScope (result : Template) (x : ActionScope) : Template := + {result with + actionScope := Field.merge result.actionScope x + } + +@[inline] +def mergeResourceScope (result : Template) (x : ResourceScopeTemplate) : Template := + {result with + resourceScope := Field.merge result.resourceScope x + } + +@[inline] +def mergeConditions (result : Template) (x : Conditions) : Template := + {result with + condition := Field.merge result.condition x + } + +@[inline] +def merge (x y : Template) : Template := + { + effect := Field.merge x.effect y.effect + principalScope := Field.merge x.principalScope y.principalScope + actionScope := Field.merge x.actionScope y.actionScope + resourceScope := Field.merge x.resourceScope y.resourceScope + condition := Field.merge x.condition y.condition + } + +@[inline] +def parseField (t : Proto.Tag) : BParsec (MergeFn Template) := do + match t.fieldNum with + -- NOTE: Doesn't look like id gets utilized in this message + | 4 => + let x : Effect ← Field.guardedParse t + pure (mergeEffect · x) + | 5 => + let x : PrincipalScopeTemplate ← Field.guardedParse t + pure (mergePrincipalScope · x) + | 6 => + let x : ActionScope ← Field.guardedParse t + pure (mergeActionScope · x) + | 7 => + let x : ResourceScopeTemplate ← Field.guardedParse t + pure (mergeResourceScope · x) + | 8 => + let x : Conditions ← Field.guardedParse t + pure (mergeConditions · x) + | _ => + t.wireType.skip + pure id + +instance : Message Template := { + parseField := parseField + merge := merge +} + +end Template + +end Cedar.Spec diff --git a/cedar-lean/CedarProto/Type.lean b/cedar-lean/CedarProto/Type.lean new file mode 100644 index 000000000..51c501fd0 --- /dev/null +++ b/cedar-lean/CedarProto/Type.lean @@ -0,0 +1,426 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Enum +import Protobuf.Message +import Protobuf.Map +import Protobuf.String + +-- Message Dependencies +import CedarProto.Name +import CedarProto.EntityType + +open Proto + +namespace Cedar.Validation + +namespace Proto +-- AttributeType <-> QualifiedType +-- Attributes <-> RecordType +def EntityRecordKind := CedarType + deriving Inhabited + +-- 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 + +def EntityRecordKind.Entity := EntityRecordKind +instance : Inhabited EntityRecordKind.Entity where + default := .entity default + +def EntityRecordKind.ActionEntity := EntityRecordKind +instance : Inhabited EntityRecordKind.ActionEntity where + default := .entity default +end Proto + +namespace RecordType +def mergeAttrs (result : RecordType) (x : Array (String × QualifiedType)) : RecordType := + Cedar.Data.Map.mk (result.kvs ++ x.toList) + +def merge (x1 x2 : RecordType) : RecordType := + Cedar.Data.Map.mk (x1.kvs ++ x2.kvs) + +end RecordType + +namespace QualifiedType + +@[inline] +def mergeType (result : QualifiedType) (x : CedarType) : QualifiedType := + -- 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 := + -- 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 Ty where + | AnyEntity + +namespace Ty +@[inline] +def fromInt (n : Int) : Except String Ty := + match n with + | 0 => .ok .AnyEntity + | n => .error s!"Field {n} does not exist in enum" +instance : ProtoEnum Ty where + fromInt := fromInt +end Ty + +namespace Record +@[inline] +def mergeAttributes (result : Record) (m2 : RecordType) : Record := + have m2 : Cedar.Data.Map Cedar.Spec.Attr (Qualified CedarType) := m2 + match result with + | .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 := + 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") + +-- parseField requires mutual recursion and can be found at the end of the file +end Record + +namespace Entity +@[inline] +def mergeE (result : Entity) (e2 : Spec.EntityTypeProto) : Entity := + match result with + | .entity e1 => .entity (Field.merge e1 e2) + | _ => panic!("Entity expected CedarType constructor to be .entity") + +@[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") + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn Entity) := do + match t.fieldNum with + | 1 => + let x : Spec.EntityTypeProto ← Field.guardedParse t + pure (mergeE · x) + | _ => + t.wireType.skip + pure id + +instance : Message Entity := { + parseField := parseField + merge := merge +} +end Entity + +namespace ActionEntity +-- Note: Ignore the Attributes in the ActionEntity message +-- since this isn't represented in the formal model + +@[inline] +def mergeName (result : ActionEntity) (e2 : Spec.EntityTypeProto) : ActionEntity := + 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") + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ActionEntity) := do + match t.fieldNum with + | 1 => + let x : Spec.EntityTypeProto ← Field.guardedParse t + pure (mergeName · x) + | _ => + t.wireType.skip + pure id + +instance : Message ActionEntity := { + parseField := parseField + merge := merge +} +end ActionEntity + +@[inline] +def mergeTy (_ : EntityRecordKind) (x : Ty) : EntityRecordKind := + match x with + | .AnyEntity => 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") + match result with + | .record m1 => match m1.kvs with + | [] => .record m2 + | _ => .record (Cedar.Data.Map.make (m2.kvs ++ m1.kvs)) + | _ => .record m2 + +@[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") + match result with + | .entity e1 => .entity (Field.merge e1 e2) + | _ => .entity e2 + +@[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") + 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 + +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 + +@[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 := + match x1, x2 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)) + | .set t1, .set t2 => .set (merge t1 t2) + -- For the rest of the fields, replace + | _, _ => x2 + +@[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) : CedarType := + match xty.id with + | "ipaddr" => .ext .ipAddr + | "decimal" => .ext .decimal + | xty => panic! 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 + + +mutual +partial def RecordType.parseField (t : Tag) : BParsec (RecordType → RecordType) := do + have : Message QualifiedType := { parseField := QualifiedType.parseField, merge := QualifiedType.merge } + match t.fieldNum with + | 1 => + let x : Proto.Map String QualifiedType ← Field.guardedParse t + pure (RecordType.mergeAttrs · x) + | _ => + t.wireType.skip + pure id + +partial def QualifiedType.parseField (t : Tag) : BParsec (QualifiedType → QualifiedType) := do + have : Message CedarType := { parseField := CedarType.parseField, merge := CedarType.merge} + match t.fieldNum with + | 1 => + let x : CedarType ← Field.guardedParse t + pure (QualifiedType.mergeType · x) + | 2 => + let x : Bool ← Field.guardedParse t + pure (QualifiedType.mergeIsRequired · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.EntityRecordKind.parseField (t : Tag) : BParsec (Proto.EntityRecordKind → 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.Ty ← Field.guardedParse t + pure (Proto.EntityRecordKind.mergeTy · x) + | 2 => + let x : Proto.EntityRecordKind.Record ← Field.guardedParse t + pure (Proto.EntityRecordKind.mergeRecord · x) + | 3 => + let x : Proto.EntityRecordKind.Entity ← Field.guardedParse t + pure (Proto.EntityRecordKind.mergeEntity · x) + | _ => + t.wireType.skip + pure id + +partial def Proto.EntityRecordKind.Record.parseField (t : Tag) : BParsec (Proto.EntityRecordKind.Record → Proto.EntityRecordKind.Record) := do + have : Message RecordType := { parseField := RecordType.parseField, merge := RecordType.merge } + match t.fieldNum with + | 1 => + let x : RecordType ← Field.guardedParse t + pure (Proto.EntityRecordKind.Record.mergeAttributes · x) + | _ => + t.wireType.skip + pure id + +partial def CedarType.parseField (t : Tag) : BParsec (CedarType → CedarType) := do + have : Message CedarType := {parseField := CedarType.parseField, merge := CedarType.merge } + have : Message Proto.EntityRecordKind := {parseField := Proto.EntityRecordKind.parseField, merge := Proto.EntityRecordKind.merge } + match t.fieldNum with + | 1 => + let x : CedarType.Ty ← Field.guardedParse t + pure (CedarType.mergeTy · x) + | 2 => + let x : CedarType ← Field.guardedParse t + pure (CedarType.mergeType · x) + | 3 => + let x : Proto.EntityRecordKind ← Field.guardedParse t + pure (CedarType.mergeEr · x) + | 4 => + let x : Cedar.Spec.Name ← Field.guardedParse t + pure (CedarType.mergeName · x) + | _ => + t.wireType.skip + pure id +end + +namespace RecordType +instance : Message RecordType := { + parseField := parseField + merge := merge +} +end RecordType + +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 + +namespace Proto.EntityRecordKind.Record +instance : Message Proto.EntityRecordKind.Record := { + parseField := parseField + merge := merge +} +end Proto.EntityRecordKind.Record + +namespace CedarType +instance : Message CedarType := { + parseField := parseField + merge := merge +} +end CedarType + +end Cedar.Validation diff --git a/cedar-lean/CedarProto/ValidationRequest.lean b/cedar-lean/CedarProto/ValidationRequest.lean new file mode 100644 index 000000000..4e1410124 --- /dev/null +++ b/cedar-lean/CedarProto/ValidationRequest.lean @@ -0,0 +1,81 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.ValidatorSchema +import CedarProto.LiteralPolicySet + + +open Proto + +namespace Cedar.Validation.Proto + +deriving instance DecidableEq for ActionSchemaEntry +deriving instance DecidableEq for ActionSchema +deriving instance DecidableEq for EntitySchemaEntry +deriving instance DecidableEq for EntitySchema +deriving instance DecidableEq for Schema + +structure ValidationRequest where + schema : Schema + policies : Spec.Policies +deriving Inhabited, DecidableEq, Repr + +namespace ValidationRequest + +@[inline] +def mergeSchema (result : ValidationRequest) (x : Schema) : ValidationRequest := + {result with + schema := Field.merge result.schema x + } + +@[inline] +def mergePolicies (result : ValidationRequest) (x : Spec.Policies) : ValidationRequest := + {result with + policies := Field.merge result.policies x + } + +@[inline] +def merge (x y : ValidationRequest) : ValidationRequest := + { + schema := Field.merge x.schema y.schema + policies := x.policies ++ y.policies + } + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ValidationRequest) := do + match t.fieldNum with + | 1 => + let x : Schema ← Field.guardedParse t + pure (mergeSchema · x) + | 2 => + let x : Spec.Policies ← Field.guardedParse t + pure (mergePolicies · x) + | _ => + t.wireType.skip + pure id + +instance : Message ValidationRequest := { + parseField := parseField + merge := merge +} + +end ValidationRequest + +end Cedar.Validation.Proto diff --git a/cedar-lean/CedarProto/ValidatorActionId.lean b/cedar-lean/CedarProto/ValidatorActionId.lean new file mode 100644 index 000000000..dd0260fa7 --- /dev/null +++ b/cedar-lean/CedarProto/ValidatorActionId.lean @@ -0,0 +1,93 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityUID +import CedarProto.Expr +import CedarProto.Type +import CedarProto.ValidatorApplySpec + +open Proto + +namespace Cedar.Validation.Proto + +-- Note: EntitySchemaEntry takes ancestors, +-- so we'll create an intermediate representation +-- once we gather all the entries, we will perform +-- the transform +structure ValidatorActionId where + appliesTo : ValidatorApplySpec + descendants : Array Spec.EntityUID + context : CedarType + +instance : Inhabited ValidatorActionId where + default := ValidatorActionId.mk default default (CedarType.record default) + +namespace ValidatorActionId + +@[inline] +def mergeAppliesTo (result : ValidatorActionId) (x : ValidatorApplySpec) : ValidatorActionId := + {result with + appliesTo := Field.merge result.appliesTo x + } + +@[inline] +def mergeDescendants (result : ValidatorActionId) (x : Array Spec.EntityUID) : ValidatorActionId := + {result with + descendants := result.descendants ++ x + } + +@[inline] +def mergeContext (result : ValidatorActionId) (x : CedarType) : ValidatorActionId := + {result with + context := Field.merge result.context x + } + +@[inline] +def merge (x y : ValidatorActionId) : ValidatorActionId := + { + appliesTo := Field.merge x.appliesTo y.appliesTo + descendants := x.descendants ++ y.descendants + context := Field.merge x.context y.context + } + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ValidatorActionId) := do + match t.fieldNum with + | 2 => + let x : ValidatorApplySpec ← Field.guardedParse t + pure (mergeAppliesTo · x) + | 3 => + let x : Repeated Spec.EntityUID ← Field.guardedParse t + pure (mergeDescendants · x) + | 4 => + let x : CedarType ← Field.guardedParse t + pure (mergeContext · x) + | _ => + t.wireType.skip + pure id + +instance : Message ValidatorActionId := { + parseField := parseField + merge := merge +} + +end ValidatorActionId + +end Cedar.Validation.Proto diff --git a/cedar-lean/CedarProto/ValidatorApplySpec.lean b/cedar-lean/CedarProto/ValidatorApplySpec.lean new file mode 100644 index 000000000..d1332c9a9 --- /dev/null +++ b/cedar-lean/CedarProto/ValidatorApplySpec.lean @@ -0,0 +1,73 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityType + +open Proto + +namespace Cedar.Validation.Proto + +structure ValidatorApplySpec where + principalApplySpec : Array Spec.EntityTypeProto + resourceApplySpec : Array Spec.EntityTypeProto +deriving Inhabited + +namespace ValidatorApplySpec + +@[inline] +def mergePas (result : ValidatorApplySpec) (x : Array Spec.EntityTypeProto) : ValidatorApplySpec := + {result with + principalApplySpec := result.principalApplySpec ++ x + } + +@[inline] +def mergeRas (result : ValidatorApplySpec) (x : Array Spec.EntityTypeProto) : ValidatorApplySpec := + {result with + resourceApplySpec := result.resourceApplySpec ++ x + } + +@[inline] +def merge (x y : ValidatorApplySpec) : ValidatorApplySpec := + { + principalApplySpec := x.principalApplySpec ++ y.principalApplySpec + resourceApplySpec := x.resourceApplySpec ++ y.resourceApplySpec + } + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ValidatorApplySpec) := do + match t.fieldNum with + | 1 => + let x : Repeated Spec.EntityTypeProto ← Field.guardedParse t + pure (mergePas · x) + | 2 => + let x : Repeated Spec.EntityTypeProto ← Field.guardedParse t + pure (mergeRas · x) + | _ => + t.wireType.skip + pure id + +instance : Message ValidatorApplySpec := { + parseField := parseField + merge := merge +} + +end ValidatorApplySpec + +end Cedar.Validation.Proto diff --git a/cedar-lean/CedarProto/ValidatorEntityType.lean b/cedar-lean/CedarProto/ValidatorEntityType.lean new file mode 100644 index 000000000..788c7e1cd --- /dev/null +++ b/cedar-lean/CedarProto/ValidatorEntityType.lean @@ -0,0 +1,125 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.EntityType +import CedarProto.Type + +open Proto + +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 ValidatorEntityType where + /-- All (transitive) descendants. Assumes TC is computed before encoding into protobuf. -/ + descendants : Array Spec.EntityTypeProto + attrs : RecordType + tags : Option CedarType +deriving Inhabited + +-- the Tag message in Validator.proto +structure TagMessage where + optional_type: CedarType +deriving Repr, Inhabited + +namespace TagMessage + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn TagMessage) := do + match t.fieldNum with + | 1 => + let ty : CedarType ← Field.guardedParse t + pure λ { optional_type := old_ty } => { optional_type := Field.merge old_ty ty } + | _ => + t.wireType.skip + pure id + +@[inline] +def merge (x y : TagMessage) : TagMessage := + { + optional_type := Message.merge x.optional_type y.optional_type + } + +instance : Message TagMessage where + parseField := parseField + merge := merge + +end TagMessage + +namespace ValidatorEntityType + +@[inline] +def mergeOption [Field α] (x1 x2 : Option α) : Option α := + match x1, x2 with + | some s1, some s2 => some (Field.merge s1 s2) + | none, some x => some x + | some x, none => some x + | none, none => none + +@[inline] +def mergeDescendants (result : ValidatorEntityType) (x : Array Spec.EntityTypeProto) : ValidatorEntityType := + {result with + descendants := result.descendants ++ x + } + +@[inline] +def mergeAttributes (result : ValidatorEntityType) (x : RecordType) : ValidatorEntityType := + {result with + attrs := Field.merge result.attrs x + } + +@[inline] +def mergeTags (result : ValidatorEntityType) (x : TagMessage) : ValidatorEntityType := + {result with + tags := mergeOption result.tags (some x.optional_type) + } + +@[inline] +def merge (x y : ValidatorEntityType) : ValidatorEntityType := + { + descendants := y.descendants ++ x.descendants + attrs := Field.merge x.attrs y.attrs + tags := mergeOption x.tags y.tags + } + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ValidatorEntityType) := do + match t.fieldNum with + | 2 => + let x : Repeated Spec.EntityTypeProto ← Field.guardedParse t + pure (mergeDescendants · x) + | 3 => + let x : RecordType ← Field.guardedParse t + pure (mergeAttributes · x) + | 5 => + let x : TagMessage ← Field.guardedParse t + pure (mergeTags · x) + | _ => + t.wireType.skip + pure id + +instance : Message ValidatorEntityType := { + parseField := parseField + merge := merge +} + +end ValidatorEntityType + +end Cedar.Validation.Proto diff --git a/cedar-lean/CedarProto/ValidatorSchema.lean b/cedar-lean/CedarProto/ValidatorSchema.lean new file mode 100644 index 000000000..91ffc6fe6 --- /dev/null +++ b/cedar-lean/CedarProto/ValidatorSchema.lean @@ -0,0 +1,185 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message +import Protobuf.String + +-- Message Dependencies +import CedarProto.ValidatorEntityType +import CedarProto.ValidatorActionId + +open Proto + +namespace Cedar.Validation.Proto + +def EntityTypeWithTypesMap := Proto.Map Spec.EntityTypeProto ValidatorEntityType + deriving Inhabited, Field + +def EntityUidWithActionsIdMap := Proto.Map Spec.EntityUID ValidatorActionId + deriving Inhabited, Field + +structure ValidatorSchema where + ets : EntityTypeWithTypesMap + acts : EntityUidWithActionsIdMap +deriving Inhabited + +instance : Data.DecidableLT Spec.EntityTypeProto := by + unfold Spec.EntityTypeProto + apply inferInstance + +/- +The Rust data types store _descendant_ information for the entity type store +and action store, but _ancestor_ information for the entity store. The Lean +formalization standardizes on ancestor information. + +The definitions and utility functions below are used to convert the descendant +representation to the ancestor representation. +-/ +@[inline] +private def findInMapValues [LT α] [DecidableEq α] [Data.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 + +@[inline] +private def descendantsToAncestors [LT α] [DecidableEq α] [Data.DecidableLT α] (descendants : Data.Map α (Data.Set α)) : Data.Map α (Data.Set α) := + Data.Map.make (List.map + (λ (k,_) => (k, findInMapValues descendants k)) descendants.toList) + +end Cedar.Validation.Proto + +namespace Cedar.Validation.Proto.EntityTypeWithTypesMap +@[inline] +def toEntitySchema (ets : EntityTypeWithTypesMap) : EntitySchema := + let ets := ets.toList + let descendantMap := Data.Map.make (List.map (λ (k,v) => + have descendants := Data.Set.mk v.descendants.toList + (k, descendants)) + ets) + let ancestorMap := descendantsToAncestors descendantMap + Data.Map.make (ets.map + (λ (k,v) => (k, + { + ancestors := ancestorMap.find! k, + attrs := Data.Map.make v.attrs.kvs, + tags := v.tags, + }))) +end Cedar.Validation.Proto.EntityTypeWithTypesMap + +namespace Cedar.Validation.Proto.EntityUidWithActionsIdMap +-- Needed for panic +deriving instance Inhabited for ActionSchemaEntry + +@[inline] +def toActionSchema (acts : EntityUidWithActionsIdMap) : ActionSchema := + let acts := acts.toList + let descendantMap := Data.Map.make (List.map (λ (k,v) => + have descendants := Data.Set.make v.descendants.toList + (k, descendants)) + acts) + let ancestorMap := descendantsToAncestors descendantMap + Data.Map.make (List.map (λ (k,v) => + match v.context with + | .record rty => + (k, { + appliesToPrincipal := Data.Set.make v.appliesTo.principalApplySpec.toList, + appliesToResource := Data.Set.make v.appliesTo.resourceApplySpec.toList, + ancestors := ancestorMap.find! k, + context := rty + }) + | _ => + panic!("EntityUidWithActionsIdMap.toActionSchema : context should be record-typed") + ) acts) +end Cedar.Validation.Proto.EntityUidWithActionsIdMap + +namespace Cedar.Validation.Proto.ValidatorSchema +@[inline] +def mergeEntityTypes (result : ValidatorSchema) (x : EntityTypeWithTypesMap) : ValidatorSchema := + {result with + ets := Field.merge result.ets x + } + +@[inline] +def mergeActionIds (result : ValidatorSchema) (x : EntityUidWithActionsIdMap) : ValidatorSchema := + {result with + acts := Field.merge result.acts x + } + +@[inline] +def merge (x y : ValidatorSchema) : ValidatorSchema := + { + ets := Field.merge x.ets y.ets + acts := Field.merge x.acts y.acts + } + +@[inline] +def parseField (t : Tag) : BParsec (MergeFn ValidatorSchema) := do + match t.fieldNum with + | 1 => + let x : EntityTypeWithTypesMap ← Field.guardedParse t + pure (mergeEntityTypes · x) + | 2 => + let x : EntityUidWithActionsIdMap ← Field.guardedParse t + pure (mergeActionIds · x) + | _ => + t.wireType.skip + pure id + +instance : Message ValidatorSchema := { + parseField := parseField + merge := merge +} + +@[inline] +def toSchema (v : ValidatorSchema) : Schema := + .mk v.ets.toEntitySchema v.acts.toActionSchema + +end Cedar.Validation.Proto.ValidatorSchema + + +namespace Cedar.Validation.Schema + +-- Note that Cedar.Validation.Schema is defined as +-- structure Schema where +-- ets : EntitySchema +-- acts : ActionSchema + +@[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) + +@[inline] +def merge (x1 x2 : Schema) : Schema := + { + ets := ES.merge x1.ets x2.ets + acts := AS.merge x1.acts x2.acts + } + +deriving instance Inhabited for Schema +instance : Field Schema := Field.fromInterField Proto.ValidatorSchema.toSchema merge + +end Cedar.Validation.Schema diff --git a/cedar-lean/CedarProto/Value.lean b/cedar-lean/CedarProto/Value.lean new file mode 100644 index 000000000..7b31b3bca --- /dev/null +++ b/cedar-lean/CedarProto/Value.lean @@ -0,0 +1,53 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ +import Cedar +import Protobuf.Message + +-- Message Dependencies +import CedarProto.Expr + +open Proto + +namespace Cedar.Spec.Value + +@[inline] +def merge (v1 : Value) (v2 : Value) : Value := + match v1, v2 with + | .prim p1, .prim p2 => .prim (Field.merge p1 p2) + | .set s1, .set s2 => Cedar.Data.Set.mk (s1.elts ++ s2.elts) + | .record m1, .record m2 => Cedar.Data.Map.mk (m1.kvs ++ m2.kvs) + | _, _ => v2 -- note this includes all the .ext cases + +private def extExprToValue (xfn : ExtFun) (args : List Expr) : Value := + match xfn, args with + | .decimal, [.lit (.string s)] => match Spec.Ext.Decimal.decimal s with + | .some v => .ext (.decimal v) + | .none => panic! s!"exprToValue: failed to parse decimal {s}" + | .ip, [.lit (.string s)] => match Spec.Ext.IPAddr.ip s with + | .some v => .ext (.ipaddr v) + | .none => panic! s!"exprToValue: failed to parse ip {s}" + | _, _ => panic! ("exprToValue: unexpected extension value\n" ++ toString (repr (Expr.call xfn args))) + +private partial def exprToValue : Expr → Value + | .lit p => .prim p + | .record r => .record (Cedar.Data.Map.make (r.map λ ⟨attr, e⟩ => ⟨attr, exprToValue e⟩)) + | .set s => .set (Cedar.Data.Set.make (s.map exprToValue)) + | .call xfn args => extExprToValue xfn args + | _ => panic!("exprToValue: invalid input expression") + +instance : Field Value := Field.fromInterField exprToValue merge + +end Cedar.Spec.Value diff --git a/cedar-lean/DiffTest/Parser.lean b/cedar-lean/DiffTest/Parser.lean index 154eaf360..9cd49cbcc 100644 --- a/cedar-lean/DiffTest/Parser.lean +++ b/cedar-lean/DiffTest/Parser.lean @@ -370,8 +370,8 @@ def jsonToTemplate (json : Lean.Json) : ParseResult Template := do def jsonToPolicy (json : Lean.Json) : ParseResult Policy := do let template ← jsonToTemplate json match template.link? "static policy" SlotEnv.empty with - | some policy => .ok policy - | none => .error s!"jsonToPolicy: found a template, not a static policy" + | .ok policy => .ok policy + | .error e => .error s!"jsonToPolicy: found a template, not a static policy: {e}" def jsonToTemplateLinkedPolicy (id : PolicyID) (json : Lean.Json) : ParseResult TemplateLinkedPolicy := do let templateId ← getJsonField json "template_id" >>= jsonToString @@ -392,8 +392,8 @@ def jsonToPolicies (json : Lean.Json) : ParseResult Policies := do let templates ← mapMValues templatesKVs jsonToTemplate let links ← getJsonField json "links" >>= jsonToTemplateLinkedPolicies match link? (Map.make templates) links with - | .some policies => .ok policies - | .none => .error s!"jsonToPolicies: failed to link templates\n{json.pretty}" + | .ok policies => .ok policies + | .error e => .error s!"jsonToPolicies: failed to link templates: {e}\n\n{json.pretty}" def jsonToPrimType (json : Lean.Json) : ParseResult CedarType := do let tag ← jsonToString json @@ -466,16 +466,6 @@ def invertJsonActionSchema (acts : JsonActionSchema) : ActionSchema := context := v.context })) acts) --- Add special "unspecified" entity type with no attributes or ancestors or tags -def addUnspecifiedEntityType (ets : EntitySchema) : EntitySchema := - let unspecifiedEntry : EntitySchemaEntry := - { - ancestors := Set.empty - attrs := Map.empty - tags := Option.none - } - Map.make (ets.toList ++ [({id := "", path := []}, unspecifiedEntry)]) - mutual partial def jsonToQualifiedCedarType (json : Lean.Json) : ParseResult (Qualified CedarType) := do @@ -556,7 +546,7 @@ partial def jsonToSchema (json : Lean.Json) : ParseResult Schema := do let actionsKVs ← getJsonField json "actionIds" >>= jsonArrayToKVList let actions ← mapMKeysAndValues actionsKVs jsonToEuid jsonToActionSchemaEntry .ok { - ets := addUnspecifiedEntityType (invertJsonEntitySchema (Map.make entityTypes)) + ets := invertJsonEntitySchema (Map.make entityTypes) acts := invertJsonActionSchema (Map.make actions) } diff --git a/cedar-lean/Protobuf/Enum.lean b/cedar-lean/Protobuf/Enum.lean index 6f837af45..8845f4de3 100644 --- a/cedar-lean/Protobuf/Enum.lean +++ b/cedar-lean/Protobuf/Enum.lean @@ -38,7 +38,7 @@ def parseEnum (α : Type) [ProtoEnum α] : BParsec α := do instance [ProtoEnum α] : Field α := { parse := (parseEnum α) - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } diff --git a/cedar-lean/Protobuf/Field.lean b/cedar-lean/Protobuf/Field.lean index e6f70ca97..525757951 100644 --- a/cedar-lean/Protobuf/Field.lean +++ b/cedar-lean/Protobuf/Field.lean @@ -25,7 +25,7 @@ namespace Proto class Field (α : Type) where parse : BParsec α - checkWireType : WireType → Bool + expectedWireType : WireType merge : α → α → α namespace Field @@ -54,16 +54,16 @@ def interpret? {α : Type} [Field α] [Inhabited α] (b : ByteArray) : Except St @[inline] def guardWireType {α : Type} [Field α] (wt : WireType) : BParsec Unit := do - let wtMatches := (@Field.checkWireType α) wt - if not wtMatches then - throw s!"WireType mismatch" + let foundWt := Field.expectedWireType α + if foundWt ≠ wt then + throw s!"WireType mismatch: found {repr foundWt}, expected {repr wt}" @[inline] def fromInterField {α β : Type} [Inhabited α] [Field α] (convert : α → β) (merge : β → β → β) : Field β := { parse := do let intMessage : α ← Field.parse pure (convert intMessage) - checkWireType := Field.checkWireType α + expectedWireType := Field.expectedWireType α merge := merge } diff --git a/cedar-lean/Protobuf/Map.lean b/cedar-lean/Protobuf/Map.lean index 99b32a45e..07d35c7c5 100644 --- a/cedar-lean/Protobuf/Map.lean +++ b/cedar-lean/Protobuf/Map.lean @@ -46,11 +46,7 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar let tag1 ← Tag.parse let result ← match tag1.fieldNum with | 1 => - let wt1Matches := (@Field.checkWireType KeyT) tag1.wireType - if not wt1Matches then - throw s!"WireType mismatch" - else - let key : KeyT ← Field.parse + let key : KeyT ← Field.guardedParse tag1 -- Since the fields are optional, check to see if we're done parsing now let curPos ← BParsec.pos @@ -59,21 +55,14 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar else let tag2 ← Tag.parse - let wt2Matches := (@Field.checkWireType ValueT) tag2.wireType - if not wt2Matches then - throw s!"WireType mismatch" - else if tag2.fieldNum != 2 then throw s!"Expected Field Number 2 within map, not {tag2.fieldNum}" else - let value : ValueT ← Field.parse + + let value : ValueT ← Field.guardedParse tag2 pure #[(Prod.mk key value)] | 2 => - let wt1Matches := (@Field.checkWireType ValueT) tag1.wireType - if not wt1Matches then - throw s!"WireType mismatch" - else - let value : ValueT ← Field.parse + let value : ValueT ← Field.guardedParse tag1 -- Since the fields are optional, check to see if we're done parsing now let curPos ← BParsec.pos @@ -82,14 +71,11 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar else let tag2 ← Tag.parse - let wt2Matches := (@Field.checkWireType KeyT) tag2.wireType - if not wt2Matches then - throw s!"WireType mismatch" - else if tag2.fieldNum != 1 then throw s!"Expected Field Number 1 within map, not {tag2.fieldNum}" else - let key : KeyT ← Field.parse + + let key : KeyT ← Field.guardedParse tag2 pure #[(Prod.mk key value)] | _ => throw "Unexpected Field Number within Map Element" @@ -103,7 +89,7 @@ def parse [Inhabited KeyT] [Inhabited ValueT] [Field KeyT] [Field ValueT] : BPar instance {α β : Type} [Inhabited α] [Inhabited β] [Field α] [Field β] : Field (Map α β) := { parse := parse - checkWireType := (· = WireType.LEN) + expectedWireType := WireType.LEN merge := Field.Merge.concatenate } end Map diff --git a/cedar-lean/Protobuf/Message.lean b/cedar-lean/Protobuf/Message.lean index 6fa786a2d..ec8bb089a 100644 --- a/cedar-lean/Protobuf/Message.lean +++ b/cedar-lean/Protobuf/Message.lean @@ -28,6 +28,14 @@ namespace Proto def MergeFn (α : Type) : Type := (α → α) class Message (α : Type) [Inhabited α] where + /-- + Parse a field, given the Tag and the data in the BParsec (updating the + BParsec iterator position appropriately). + Return a `MergeFn`, which when applied to the previous value α, + gives you the final value α which is the result of the parse. + Note in particular that returning `id` as the `MergeFn` results in + just taking the previous value as-is, ignoring the newly parsed data. + -/ parseField : Tag → BParsec (MergeFn α) merge : α → α → α @@ -60,8 +68,6 @@ private def parseMessageHelper [Inhabited α] [Message α] (remaining : Nat) (re (parseMessageHelper (remaining - elementSize) newResult) - - @[inline] def parse [Inhabited α] [Message α] : BParsec α := do let remaining ← BParsec.remaining @@ -90,7 +96,7 @@ def interpret! [Inhabited α] [Message α] (b : ByteArray) : α := instance [Inhabited α] [Message α] : Field α := { parse := parseWithLen - checkWireType := (· = WireType.LEN) + expectedWireType := WireType.LEN merge := merge } diff --git a/cedar-lean/Protobuf/Packed.lean b/cedar-lean/Protobuf/Packed.lean index 592cf1bdb..01f2b70aa 100644 --- a/cedar-lean/Protobuf/Packed.lean +++ b/cedar-lean/Protobuf/Packed.lean @@ -51,7 +51,7 @@ def parse (α : Type) [Field α] : BParsec (Array α) := do instance [Field α] : Field (Repeated α) := { parse := (parse α) - checkWireType := Field.checkWireType α + expectedWireType := Field.expectedWireType α merge := Field.Merge.concatenate } @@ -87,7 +87,7 @@ def parse (α : Type) [Field α] : BParsec (Array α) := do instance [Field α] : Field (Packed α) := { parse := (parse α) - checkWireType := (· = WireType.LEN) + expectedWireType := WireType.LEN merge := Field.Merge.concatenate } diff --git a/cedar-lean/Protobuf/String.lean b/cedar-lean/Protobuf/String.lean index 1f2278689..4247f15ba 100644 --- a/cedar-lean/Protobuf/String.lean +++ b/cedar-lean/Protobuf/String.lean @@ -96,7 +96,7 @@ def parse_string : BParsec String := do instance : Field String := { parse := parse_string - checkWireType := (· = WireType.LEN) + expectedWireType := WireType.LEN merge := Field.Merge.override } diff --git a/cedar-lean/Protobuf/Varint.lean b/cedar-lean/Protobuf/Varint.lean index f0b64fe4e..8cce0d6ce 100644 --- a/cedar-lean/Protobuf/Varint.lean +++ b/cedar-lean/Protobuf/Varint.lean @@ -85,7 +85,7 @@ def parse_uint64 : BParsec UInt64 := do instance : Field UInt64 := { parse := parse_uint64 - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } @@ -107,7 +107,7 @@ def parse_uint32 : BParsec UInt32 := do instance : Field UInt32 := { parse := parse_uint32 - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } @@ -128,7 +128,7 @@ def parse_int32 : BParsec Int32 := do instance : Field Int32 := { parse := parse_int32 - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } @@ -148,7 +148,7 @@ def parse_int64 : BParsec Int64 := do instance : Field Int64 := { parse := parse_int64 - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } @@ -161,7 +161,7 @@ def parse_bool : BParsec Bool := do instance : Field Bool := { parse := Proto.parse_bool - checkWireType := (· = WireType.VARINT) + expectedWireType := WireType.VARINT merge := Field.Merge.override } diff --git a/cedar-lean/Protobuf/WireType.lean b/cedar-lean/Protobuf/WireType.lean index f4cc9531f..f21231a48 100644 --- a/cedar-lean/Protobuf/WireType.lean +++ b/cedar-lean/Protobuf/WireType.lean @@ -14,12 +14,12 @@ limitations under the License. -/ -namespace Proto - /-! Protobuf Wire Types -/ +namespace Proto + inductive WireType where | VARINT : WireType | I64 : WireType diff --git a/cedar-lean/UnitTest.lean b/cedar-lean/UnitTest.lean index 456bb4aba..e31468939 100644 --- a/cedar-lean/UnitTest.lean +++ b/cedar-lean/UnitTest.lean @@ -14,6 +14,7 @@ limitations under the License. -/ +import UnitTest.CedarProto import UnitTest.Decimal import UnitTest.IPAddr import UnitTest.Main diff --git a/cedar-lean/UnitTest/CedarProto-test-data/345.protodata b/cedar-lean/UnitTest/CedarProto-test-data/345.protodata new file mode 100644 index 000000000..2bbe8e587 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/345.protodata @@ -0,0 +1,3 @@ + + +345 \ 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 new file mode 100644 index 000000000..5c9a5b7de Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/abac.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/action.protodata b/cedar-lean/UnitTest/CedarProto-test-data/action.protodata new file mode 100644 index 000000000..70c2ecbce --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/action.protodata @@ -0,0 +1,3 @@ + + +action \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/app_widget_123.protodata b/cedar-lean/UnitTest/CedarProto-test-data/app_widget_123.protodata new file mode 100644 index 000000000..54b372d61 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/app_widget_123.protodata @@ -0,0 +1,6 @@ + +J +H"F +' +% +WidgetApp App::Widget::"123"123App::Widget::"123"App::Widget::"123" \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/complicated.protodata b/cedar-lean/UnitTest/CedarProto-test-data/complicated.protodata new file mode 100644 index 000000000..30b760817 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/complicated.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/contains.protodata b/cedar-lean/UnitTest/CedarProto-test-data/contains.protodata new file mode 100644 index 000000000..3cfacec43 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/contains.protodata @@ -0,0 +1,18 @@ + +B +r +7 + +/)[2,3,User::"alice"].contains(context.foo) +7 + +/)[2,3,User::"alice"].contains(context.foo) + +w +u"s +9 +7 +User/)[2,3,User::"alice"].contains(context.foo)alice/ )[2,3,User::"alice"].contains(context.foo)/ )[2,3,User::"alice"].contains(context.foo)-)[2,3,User::"alice"].contains(context.foo)q +>R< +5 +/)[2,3,User::"alice"].contains(context.foo)foo/ )[2,3,User::"alice"].contains(context.foo)-))[2,3,User::"alice"].contains(context.foo) \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/decimal.protodata b/cedar-lean/UnitTest/CedarProto-test-data/decimal.protodata new file mode 100644 index 000000000..1d5687393 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/decimal.protodata @@ -0,0 +1,16 @@ + +J + + +lessThan +}J{ +: +decimal/+decimal("3.14").lessThan(decimal("3.1416"))= + +3.141+decimal("3.14").lessThan(decimal("3.1416"))/++decimal("3.14").lessThan(decimal("3.1416")) +J +< +decimal1+decimal("3.14").lessThan(decimal("3.1416"))? + + +3.14161!+decimal("3.14").lessThan(decimal("3.1416"))1+decimal("3.14").lessThan(decimal("3.1416"))/++decimal("3.14").lessThan(decimal("3.1416")) \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptyrecord.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptyrecord.protodata new file mode 100644 index 000000000..0e3c707c0 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/emptyrecord.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptyset.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptyset.protodata new file mode 100644 index 000000000..c382c2cf8 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/emptyset.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/emptystring.protodata b/cedar-lean/UnitTest/CedarProto-test-data/emptystring.protodata new file mode 100644 index 000000000..d89b7ddc8 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/emptystring.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata b/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata new file mode 100644 index 000000000..7fc494d9c --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/entities.protodata @@ -0,0 +1,11 @@ + + + + + +ABC123 + + + + +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 new file mode 100644 index 000000000..da7166b17 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/entity.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/false.protodata b/cedar-lean/UnitTest/CedarProto-test-data/false.protodata new file mode 100644 index 000000000..a1b5f0f1d Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/false.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/.gitignore b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/.gitignore new file mode 100644 index 000000000..fa8d85ac5 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/.gitignore @@ -0,0 +1,2 @@ +Cargo.lock +target diff --git a/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/Cargo.toml b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/Cargo.toml new file mode 100644 index 000000000..b59a53e8e --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/Cargo.toml @@ -0,0 +1,30 @@ +[package] +name = "generate-protodata" +rust-version = "1.77" +version = "4.1.0" +homepage = "https://cedarpolicy.com" +license = "Apache-2.0" +edition = "2021" +repository = "https://github.com/cedar-policy/cedar-spec" + +[dependencies] +cedar-policy-core = { git = "https://github.com/cedar-policy/cedar", version = "*", features = ["protobufs"] } +cedar-policy-validator = { git = "https://github.com/cedar-policy/cedar", version = "*", features = ["protobufs"] } +miette = { version = "7.1.0", features = ["fancy"] } +prost = "0.13" + +[lints.rust] +unsafe_code = "forbid" +unexpected_cfgs = "deny" +missing_debug_implementations = "deny" +rust-2018-idioms = "deny" + +[lints.clippy] +nursery = { level = "warn", priority = -1 } +missing_const_for_fn = "allow" +needless_doctest_main = "allow" +result_large_err = "allow" +large_enum_variant = "allow" +redundant_clone = "deny" +todo = "deny" +unimplemented = "deny" diff --git a/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/src/main.rs b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/src/main.rs new file mode 100644 index 000000000..838f28879 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/generate-protodata/src/main.rs @@ -0,0 +1,359 @@ +use cedar_policy_core::{ + ast, entities, + extensions::Extensions, + parser::{parse_policy_or_template, parse_policyset, Loc}, +}; +use cedar_policy_validator::types as validator_types; +use prost::Message; +use std::collections::{BTreeMap, HashMap, HashSet}; +use std::path::{Path, PathBuf}; +use std::str::FromStr; + +fn output_dir() -> PathBuf { + std::env::var("OUTPUT_DIR") + .map(PathBuf::from) + .unwrap_or(PathBuf::from_str(".").unwrap()) +} + +#[track_caller] +fn encode_expr(path: impl AsRef, e: &str) { + let expr: ast::Expr = e.parse().unwrap(); + let proto: ast::proto::Expr = (&expr).into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +/// Encodes using the protobuf TemplateBody format +#[track_caller] +fn encode_policy_as_template(path: impl AsRef, p: &str) { + let policy: ast::Template = parse_policy_or_template(None, p).unwrap().into(); + let proto: ast::proto::TemplateBody = (&policy).into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_policyset(path: impl AsRef, ps: &ast::PolicySet) { + let proto: ast::proto::LiteralPolicySet = ps.into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_request(path: impl AsRef, r: &ast::Request) { + let proto: ast::proto::Request = r.into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_entity(path: impl AsRef, e: &ast::Entity) { + let proto: ast::proto::Entity = e.into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_entities(path: impl AsRef, es: &entities::Entities) { + let proto: ast::proto::Entities = es.into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_val_type(path: impl AsRef, ty: &validator_types::Type) { + let proto: cedar_policy_validator::proto::Type = ty.into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +#[track_caller] +fn encode_schema(path: impl AsRef, s: &str) { + let (schema, warnings) = cedar_policy_validator::ValidatorSchema::from_cedarschema_str( + s, + &Extensions::all_available(), + ) + .map_err(|e| format!("{:?}", miette::Report::new(e))) + .unwrap(); + assert_eq!(warnings.count(), 0); + let proto: cedar_policy_validator::proto::ValidatorSchema = (&schema).into(); + let encoded = proto.encode_to_vec(); + std::fs::write(output_dir().join(path.as_ref()), encoded).unwrap(); +} + +fn main() { + encode_expr("false.protodata", "false"); + encode_expr("true.protodata", "true"); + encode_expr("345.protodata", "345"); + encode_expr("emptystring.protodata", r#""""#); + encode_expr("thisiscedar.protodata", r#""this is Cedar""#); + encode_expr("action.protodata", "action"); + encode_expr("user_alice.protodata", r#"User::"alice""#); + encode_expr("app_widget_123.protodata", r#"App::Widget::"123""#); + encode_expr("emptyset.protodata", "[]"); + encode_expr("set.protodata", r#"[-2, "minustwo"]"#); + encode_expr( + "nested_set.protodata", + "[ [1, 2], [3, principal.foo], false ]", + ); + encode_expr("emptyrecord.protodata", "{}"); + encode_expr("record.protodata", "{ ham: 3, eggs: 7 }"); + encode_expr( + "nested_record.protodata", + r#"{ ham: { a: 0, b: false }, eggs: ["this is", "a set"] }"#, + ); + encode_expr( + "principal_in_resource_owners.protodata", + "principal in resource.owners", + ); + encode_expr( + "has_and_get.protodata", + r#"principal has department && principal.department == "Sales""#, + ); + encode_expr( + "has_and_get_tags.protodata", + r#"principal.hasTag("department") && principal.getTag("department") == "Sales""#, + ); + encode_expr( + "not_and_neg.protodata", + "!principal.foo || -(principal.bar) != 3", + ); + encode_expr( + "plus_and_minus_and_times.protodata", + "32 + context.count - 7 * 4", + ); + encode_expr( + "contains.protodata", + r#"[2,3,User::"alice"].contains(context.foo)"#, + ); + encode_expr("like.protodata", r#"context.a.b.c.d like "a*b**cd""#); + encode_expr( + "is.protodata", + r#"App::Widget::"123" is App::Widget && resource.widget is App::Widget in principal.widgets"#, + ); + encode_expr( + "complicated.protodata", + "(if context.foo < 3 then principal.foo else principal.bar).a.b.contains(context.abc)", + ); + encode_expr( + "ip.protodata", + r#"ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))"#, + ); + encode_expr( + "decimal.protodata", + r#"decimal("3.14").lessThan(decimal("3.1416"))"#, + ); + + encode_policy_as_template( + "rbac.protodata", + r#"permit(principal == User::"a b c", action, resource is App::Widget);"#, + ); + encode_policy_as_template( + "abac.protodata", + r#"permit(principal, action, resource) when { principal == resource.owner } unless { resource.sensitive };"#, + ); + + let mut policyset: ast::PolicySet = parse_policyset(r#" + permit(principal, action == Action::"do", resource == Blob::"thing") when { context.foo - 7 == context.bar }; + forbid(principal is UnauthenticatedUser, action, resource) when { resource.requiresAuthentication }; + @foo("bar") + permit(principal, action in [Action::"1", Action::"2"], resource) when { ["a", "b", "c"].contains(resource.type) }; + permit(principal == ?principal, action, resource) when { resource.eligibility > 2 }; + "#).unwrap(); + policyset + .link( + ast::PolicyID::from_string("policy3"), + ast::PolicyID::from_string("linkedpolicy"), + HashMap::from_iter([( + ast::SlotId::principal(), + ast::EntityUID::with_eid_and_type("User", "alice").unwrap(), + )]), + ) + .unwrap(); + encode_policyset("policyset.protodata", &policyset); + + encode_request( + "request.protodata", + &ast::Request::new( + ( + ast::EntityUID::with_eid_and_type("User", "alice").unwrap(), + None, + ), + ( + ast::EntityUID::with_eid_and_type("Action", "access").unwrap(), + Some(Loc::new(2..5, "source code".into())), + ), + ( + ast::EntityUID::with_eid_and_type("Folder", "data").unwrap(), + None, + ), + ast::Context::from_pairs( + [("foo".into(), ast::RestrictedExpr::val(true))], + Extensions::all_available(), + ) + .unwrap(), + None::<&ast::RequestSchemaAllPass>, + Extensions::all_available(), + ) + .unwrap(), + ); + + encode_entity( + "entity.protodata", + &ast::Entity::new( + ast::EntityUID::from_components( + ast::EntityType::from_normalized_str("A::B").unwrap(), + ast::Eid::new("C"), + None, + ), + [ + ("foo".into(), "[1, -1]".parse().unwrap()), + ("bar".into(), ast::RestrictedExpr::val(false)), + ], + HashSet::from_iter([ + ast::EntityUID::with_eid_and_type("Parent", "1").unwrap(), + ast::EntityUID::with_eid_and_type("Grandparent", "A").unwrap(), + ]), + [ + ("tag1".into(), ast::RestrictedExpr::val("val1")), + ("tag2".into(), ast::RestrictedExpr::val("val2")), + ], + Extensions::all_available(), + ) + .unwrap(), + ); + + encode_entities( + "entities.protodata", + &entities::Entities::from_entities( + [ + ast::Entity::with_uid(ast::EntityUID::with_eid_and_type("ABC", "123").unwrap()), + ast::Entity::with_uid(ast::EntityUID::with_eid_and_type("DEF", "234").unwrap()), + ], + None::<&entities::AllEntitiesNoAttrsSchema>, + entities::TCComputation::ComputeNow, + Extensions::all_available(), + ) + .unwrap(), + ); + + let primitive_bool = validator_types::Type::Primitive { + primitive_type: validator_types::Primitive::Bool, + }; + let primitive_long = validator_types::Type::Primitive { + primitive_type: validator_types::Primitive::Long, + }; + let primitive_string = validator_types::Type::Primitive { + primitive_type: validator_types::Primitive::String, + }; + + encode_val_type("type_true.protodata", &validator_types::Type::True); + encode_val_type("type_false.protodata", &validator_types::Type::False); + encode_val_type("type_bool.protodata", &primitive_bool); + encode_val_type("type_long.protodata", &primitive_long.clone()); + encode_val_type("type_string.protodata", &primitive_string.clone()); + encode_val_type( + "type_set_of_string.protodata", + &validator_types::Type::Set { + element_type: Some(Box::new(primitive_string.clone())), + }, + ); + encode_val_type( + "type_ip.protodata", + &validator_types::Type::ExtensionType { + name: ast::Name::parse_unqualified_name("ipaddr").unwrap(), + }, + ); + encode_val_type( + "type_record.protodata", + &validator_types::Type::EntityOrRecord(validator_types::EntityRecordKind::Record { + attrs: validator_types::Attributes { + attrs: BTreeMap::from_iter([ + ( + "ham".into(), + validator_types::AttributeType::required_attribute( + primitive_string.clone(), + ), + ), + ( + "eggs".into(), + validator_types::AttributeType::optional_attribute(primitive_long.clone()), + ), + ]), + }, + open_attributes: validator_types::OpenTag::ClosedAttributes, + }), + ); + + encode_schema( + "schema_basic.protodata", + r#" + entity A; + entity B in A; + action Read, Write; + action ReadX in Read appliesTo { + principal: [A], + resource: [A, B], + }; + "#, + ); + + encode_schema( + "schema_attrs.protodata", + r#" + entity A, B; + entity C { + a: Bool, + b: Long, + c?: String, + d: A, + e: Set, + f: ipaddr, + g: { ham: String, eggs?: Long, owner: C }, + }; + action Read, Write; + action ReadX in Read appliesTo { + principal: [A, B], + resource: [B, C], + context: { + a: String, + b?: B, + c: Set, + d: decimal, + e: { ham?: Bool, eggs: Long, manager: B }, + }, + }; + "#, + ); + + encode_schema( + "schema_commontypes.protodata", + r#" + entity A, B, C; + type Z = String; + type Y = Set; + entity F in [A, B] { z: Z, y?: Set }; + action Read appliesTo { + principal: [A, B], + resource: [C], + context: { + a?: { z?: Z, y: { foo: Y } }, + y: Y, + }, + }; + "#, + ); + + encode_schema( + "schema_tags.protodata", + r#" + entity A, B; + entity C tags String; + entity D in B tags Set; + entity E tags Set; + + type Z = String; + entity F in [A, B] { z: Set } tags Z; + "#, + ); +} diff --git a/cedar-lean/UnitTest/CedarProto-test-data/generate.sh b/cedar-lean/UnitTest/CedarProto-test-data/generate.sh new file mode 100755 index 000000000..00b25ad41 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/generate.sh @@ -0,0 +1,3 @@ +#!/bin/bash + +cd generate-protodata && OUTPUT_DIR=.. cargo run diff --git a/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata new file mode 100644 index 000000000..465893eba Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get.protodata differ 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 new file mode 100644 index 000000000..40f11036f Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/has_and_get_tags.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/ip.protodata b/cedar-lean/UnitTest/CedarProto-test-data/ip.protodata new file mode 100644 index 000000000..f2eb438f6 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/ip.protodata @@ -0,0 +1,14 @@ + +J + + isInRange +J +8 +ip2.ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))G + +  192.168.0.14 .ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))2..ip("192.168.0.1").isInRange(ip("192.0.0.0/8")) +J +: +ip4.ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))G + +  192.0.0.0/84 .ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))4.ip("192.168.0.1").isInRange(ip("192.0.0.0/8"))2..ip("192.168.0.1").isInRange(ip("192.0.0.0/8")) \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/is.protodata b/cedar-lean/UnitTest/CedarProto-test-data/is.protodata new file mode 100644 index 000000000..72908fb1e Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/is.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/like.protodata b/cedar-lean/UnitTest/CedarProto-test-data/like.protodata new file mode 100644 index 000000000..b8d3a52e5 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/like.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata new file mode 100644 index 000000000..75171b95a Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/nested_record.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/nested_set.protodata b/cedar-lean/UnitTest/CedarProto-test-data/nested_set.protodata new file mode 100644 index 000000000..3f3f25616 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/nested_set.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/not_and_neg.protodata b/cedar-lean/UnitTest/CedarProto-test-data/not_and_neg.protodata new file mode 100644 index 000000000..79e3798a9 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/not_and_neg.protodata differ 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 new file mode 100644 index 000000000..86c6ad189 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/plus_and_minus_and_times.protodata @@ -0,0 +1,13 @@ + +B +B& + + 32 + context.count - 7 * 4U +1R/ +& + 32 + context.count - 7 * 4count  32 + context.count - 7 * 432 + context.count - 7 * 4| +XBV( + + 32 + context.count - 7 * 4( + + 32 + context.count - 7 * 4 32 + context.count - 7 * 432 + context.count - 7 * 4 \ 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 new file mode 100644 index 000000000..6fad51aad Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/policyset.protodata differ 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 new file mode 100644 index 000000000..2d51596ba Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/principal_in_resource_owners.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/rbac.protodata b/cedar-lean/UnitTest/CedarProto-test-data/rbac.protodata new file mode 100644 index 000000000..e1c9c3c06 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/rbac.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/record.protodata b/cedar-lean/UnitTest/CedarProto-test-data/record.protodata new file mode 100644 index 000000000..13db88f19 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/record.protodata @@ -0,0 +1,10 @@ + +WzU +( +ham! + +{ ham: 3, eggs: 7 } +) +eggs! + +{ ham: 3, eggs: 7 }{ ham: 3, eggs: 7 } \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/request.protodata b/cedar-lean/UnitTest/CedarProto-test-data/request.protodata new file mode 100644 index 000000000..c64a19e83 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/request.protodata @@ -0,0 +1,22 @@ + + + + + +Useralice) + + + + +Actionaccess source code + + + + +Folderdata" + +z + +foo + + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata new file mode 100644 index 000000000..1977bf9af Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/schema_attrs.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata new file mode 100644 index 000000000..955fb11fa Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/schema_basic.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata new file mode 100644 index 000000000..8147169df Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/schema_commontypes.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata b/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata new file mode 100644 index 000000000..bc4d66fc4 Binary files /dev/null and b/cedar-lean/UnitTest/CedarProto-test-data/schema_tags.protodata differ diff --git a/cedar-lean/UnitTest/CedarProto-test-data/set.protodata b/cedar-lean/UnitTest/CedarProto-test-data/set.protodata new file mode 100644 index 000000000..e3966fc89 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/set.protodata @@ -0,0 +1,10 @@ + +SrQ +' + + [-2, "minustwo"] +& + + +minustwo +[-2, "minustwo"][-2, "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 new file mode 100644 index 000000000..9f98af614 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/thisiscedar.protodata @@ -0,0 +1,3 @@ + + + this is Cedar"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 new file mode 100644 index 000000000..a6c18c4e5 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/true.protodata @@ -0,0 +1,3 @@ + + +true \ 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 new file mode 100644 index 000000000..322f84548 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_bool.protodata @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_false.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_false.protodata new file mode 100644 index 000000000..009a24fee --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_false.protodata @@ -0,0 +1 @@ + \ 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 new file mode 100644 index 000000000..c8e059fa0 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_ip.protodata @@ -0,0 +1,2 @@ +" +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 new file mode 100644 index 000000000..426aefb51 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_long.protodata @@ -0,0 +1 @@ + \ 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 new file mode 100644 index 000000000..b00259f9f --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_record.protodata @@ -0,0 +1,8 @@ +#! + + +eggs + + +ham + \ No newline at end of file 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 new file mode 100644 index 000000000..56885a6e9 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_set_of_string.protodata @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata new file mode 100644 index 000000000..c565d872f --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_string.protodata @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/type_true.protodata b/cedar-lean/UnitTest/CedarProto-test-data/type_true.protodata new file mode 100644 index 000000000..e19a122a5 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/type_true.protodata @@ -0,0 +1 @@ + \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto-test-data/user_alice.protodata b/cedar-lean/UnitTest/CedarProto-test-data/user_alice.protodata new file mode 100644 index 000000000..670fe94c4 --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto-test-data/user_alice.protodata @@ -0,0 +1,6 @@ + +; +9"7 + + +User User::"alice"alice  User::"alice"  User::"alice" \ No newline at end of file diff --git a/cedar-lean/UnitTest/CedarProto.lean b/cedar-lean/UnitTest/CedarProto.lean new file mode 100644 index 000000000..1755907eb --- /dev/null +++ b/cedar-lean/UnitTest/CedarProto.lean @@ -0,0 +1,534 @@ +/- + Copyright Cedar Contributors + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + https://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +-/ + +import CedarProto +import Protobuf +import UnitTest.Run + +/-! This file defines unit tests for CedarProto functions. -/ + +namespace Cedar.Spec.Expr +open Cedar.Data +/-- Ensures that records are sorted by key, including recursively -/ +partial def mkWf : Cedar.Spec.Expr → Cedar.Spec.Expr + | .lit p => .lit p + | .var v => .var v + | .ite a b c => .ite a.mkWf b.mkWf c.mkWf + | .and a b => .and a.mkWf b.mkWf + | .or a b => .or a.mkWf b.mkWf + | .unaryApp op x => .unaryApp op x.mkWf + | .binaryApp op a b => .binaryApp op a.mkWf b.mkWf + | .getAttr x attr => .getAttr x.mkWf attr + | .hasAttr x attr => .hasAttr x.mkWf attr + | .set xs => .set (xs.map mkWf) + | .record pairs => + let m := Map.make (pairs.map λ (k, v) => (k, v.mkWf)) + .record m.kvs + | .call xfn xs => .call xfn (xs.map mkWf) +end Cedar.Spec.Expr + +namespace Cedar.Spec.Policies +def sortByPolicyId : Cedar.Spec.Policies → Cedar.Spec.Policies + | ps => ps.mergeSort λ a b => a.id < b.id +end Cedar.Spec.Policies + +namespace UnitTest.CedarProto + +open CedarProto +open Cedar.Data + +/-- + `filename` is expected to be the name of a file containing binary protobuf data. + This test will ensure that that binary data deserializes into the value `expected`. +-/ +def testDeserializeProtodata [Inhabited α] [DecidableEq α] [Repr α] [Proto.Message α] + (filename : String) (expected : α) : TestCase IO := + test s!"Deserialize {filename}" ⟨λ () => do + let buf ← IO.FS.readBinFile filename + let parsed : Except String α := Proto.Message.interpret? buf + match parsed with + | .ok req => checkEq req expected + | .error e => pure (.error e) + ⟩ + +/-- + Similar to `testDeserializeProtodata`, but `f` is applied to the deserialized + value before comparing to `expected` +-/ +def testDeserializeProtodata' [Inhabited α] [DecidableEq β] [Repr β] [Proto.Message α] + (filename : String) (f : α → β) (expected : β) : TestCase IO := + test s!"Deserialize {filename}" ⟨λ () => do + let buf ← IO.FS.readBinFile filename + let parsed : Except String α := Proto.Message.interpret? buf + match parsed with + | .ok req => checkEq (f req) expected + | .error e => pure (.error e) + ⟩ + +private def mkUid (path : List String) (ty : String) (eid : String) : Cedar.Spec.EntityUID := + { ty := { path, id := ty }, eid } + +def tests := [ + suite (m := IO) "Cedar Protobuf deserialization tests" [ + testDeserializeProtodata "UnitTest/CedarProto-test-data/false.protodata" + (Cedar.Spec.Expr.lit (.bool false)), + testDeserializeProtodata "UnitTest/CedarProto-test-data/true.protodata" + (Cedar.Spec.Expr.lit (.bool true)), + testDeserializeProtodata "UnitTest/CedarProto-test-data/345.protodata" + (Cedar.Spec.Expr.lit (.int (Int64.mk 345 (by decide)))), + testDeserializeProtodata "UnitTest/CedarProto-test-data/emptystring.protodata" + (Cedar.Spec.Expr.lit (.string "")), + testDeserializeProtodata "UnitTest/CedarProto-test-data/thisiscedar.protodata" + (Cedar.Spec.Expr.lit (.string "this is Cedar")), + testDeserializeProtodata "UnitTest/CedarProto-test-data/action.protodata" + (Cedar.Spec.Expr.var .action), + testDeserializeProtodata "UnitTest/CedarProto-test-data/user_alice.protodata" + (Cedar.Spec.Expr.lit (.entityUID (mkUid [] "User" "alice"))), + testDeserializeProtodata "UnitTest/CedarProto-test-data/app_widget_123.protodata" + (Cedar.Spec.Expr.lit (.entityUID (mkUid ["App"] "Widget" "123"))), + testDeserializeProtodata "UnitTest/CedarProto-test-data/emptyset.protodata" + (Cedar.Spec.Expr.set []), + testDeserializeProtodata "UnitTest/CedarProto-test-data/set.protodata" + (Cedar.Spec.Expr.set [ + .lit (.int (Int64.mk (-2) (by decide))), + .lit (.string "minustwo"), + ]), + testDeserializeProtodata "UnitTest/CedarProto-test-data/nested_set.protodata" + (Cedar.Spec.Expr.set [ + .set [ .lit (.int (Int64.mk 1 (by decide))), .lit (.int (Int64.mk 2 (by decide))) ], + .set [ .lit (.int (Int64.mk 3 (by decide))), .getAttr (.var .principal) "foo" ], + .lit (.bool false), + ]), + testDeserializeProtodata "UnitTest/CedarProto-test-data/emptyrecord.protodata" + (Cedar.Spec.Expr.record []), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/record.protodata" + Cedar.Spec.Expr.mkWf + (.record [ + ("eggs", .lit (.int (Int64.mk 7 (by decide)))), + ("ham", .lit (.int (Int64.mk 3 (by decide)))), + ]), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/nested_record.protodata" + Cedar.Spec.Expr.mkWf + (.record [ + ("eggs", .set [ .lit (.string "this is"), .lit (.string "a set") ]), + ("ham", .record [ + ("a", .lit (.int (Int64.mk 0 (by decide)))), + ("b", .lit (.bool false)), + ]), + ]), + testDeserializeProtodata "UnitTest/CedarProto-test-data/principal_in_resource_owners.protodata" + (Cedar.Spec.Expr.binaryApp .mem (.var .principal) (.getAttr (.var .resource) "owners")), + testDeserializeProtodata "UnitTest/CedarProto-test-data/has_and_get.protodata" + (Cedar.Spec.Expr.and + (.hasAttr (.var .principal) "department") + (.binaryApp .eq (.getAttr (.var .principal) "department") (.lit (.string "Sales"))) + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/has_and_get_tags.protodata" + (Cedar.Spec.Expr.and + (.binaryApp .hasTag (.var .principal) (.lit (.string "department"))) + (.binaryApp .eq (.binaryApp .getTag (.var .principal) (.lit (.string "department"))) (.lit (.string "Sales"))) + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/not_and_neg.protodata" + (Cedar.Spec.Expr.or + (.unaryApp .not (.getAttr (.var .principal) "foo")) + (.unaryApp .not (.binaryApp .eq + (.unaryApp .neg (.getAttr (.var .principal) "bar")) + (.lit (.int (Int64.mk 3 (by decide)))) + )) + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/plus_and_minus_and_times.protodata" + (Cedar.Spec.Expr.binaryApp .sub + (.binaryApp .add (.lit (.int (Int64.mk 32 (by decide)))) (.getAttr (.var .context) "count")) + (.binaryApp .mul (.lit (.int (Int64.mk 7 (by decide)))) (.lit (.int (Int64.mk 4 (by decide))))) + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/contains.protodata" + (Cedar.Spec.Expr.binaryApp .contains + (.set [ + (.lit (.int (Int64.mk 2 (by decide)))), + (.lit (.int (Int64.mk 3 (by decide)))), + (.lit (.entityUID (mkUid [] "User" "alice"))), + ]) + (.getAttr (.var .context) "foo") + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/like.protodata" + (Cedar.Spec.Expr.unaryApp (.like ['a', .star, 'b', .star, .star, 'c', 'd']) + (.getAttr (.getAttr (.getAttr (.getAttr (.var .context) "a") "b") "c") "d") + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/is.protodata" + (Cedar.Spec.Expr.and + (.unaryApp (.is { id := "Widget", path := ["App"] }) + (.lit (.entityUID (mkUid ["App"] "Widget" "123"))) + ) + (.and + (.unaryApp (.is { id := "Widget", path := ["App"] }) (.getAttr (.var .resource) "widget")) + (.binaryApp .mem (.getAttr (.var .resource) "widget") (.getAttr (.var .principal) "widgets")) + ) + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/complicated.protodata" + (Cedar.Spec.Expr.binaryApp .contains + (.getAttr + (.getAttr + (.ite + (.binaryApp .less (.getAttr (.var .context) "foo") (.lit (.int (Int64.mk 3 (by decide))))) + (.getAttr (.var .principal) "foo") + (.getAttr (.var .principal) "bar") + ) + "a" + ) + "b" + ) + (.getAttr (.var .context) "abc") + ), + testDeserializeProtodata "UnitTest/CedarProto-test-data/ip.protodata" + (Cedar.Spec.Expr.call .isInRange [ + (.call .ip [.lit (.string "192.168.0.1")]), + (.call .ip [.lit (.string "192.0.0.0/8")]), + ]), + testDeserializeProtodata "UnitTest/CedarProto-test-data/decimal.protodata" + (Cedar.Spec.Expr.call .lessThan [ + (.call .decimal [.lit (.string "3.14")]), + (.call .decimal [.lit (.string "3.1416")]), + ]), + testDeserializeProtodata "UnitTest/CedarProto-test-data/rbac.protodata" + ({ + effect := .permit + principalScope := .principalScope (.eq (.entityUID (mkUid [] "User" "a b c"))) + actionScope := .actionScope .any + resourceScope := .resourceScope (.is { id := "Widget", path := ["App"] }) + condition := [{ kind := .when, body := .lit (.bool true) }] + } : Cedar.Spec.Template), + testDeserializeProtodata "UnitTest/CedarProto-test-data/abac.protodata" + ({ + effect := .permit + principalScope := .principalScope .any + actionScope := .actionScope .any + resourceScope := .resourceScope .any + condition := [ + -- On the Rust side, the `when` and `unless` were collapsed into a + -- single condition before serializing to protobuf + { + kind := .when + body := .and + (.binaryApp .eq (.var .principal) (.getAttr (.var .resource) "owner")) + (.unaryApp .not (.getAttr (.var .resource) "sensitive")) + }, + ] + } : Cedar.Spec.Template), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/policyset.protodata" + (Cedar.Spec.Policies.sortByPolicyId ∘ Cedar.Spec.Policies.fromLiteralPolicySet) + [ + { + id := "linkedpolicy" + effect := .permit + principalScope := .principalScope (.eq (mkUid [] "User" "alice")) + actionScope := .actionScope .any + resourceScope := .resourceScope .any + condition := [{ + kind := .when + body := .unaryApp .not (.binaryApp .lessEq + (.getAttr (.var .resource) "eligibility") + (.lit (.int (Int64.mk 2 (by decide)))) + ) + }] + }, + { + id := "policy0" + effect := .permit + principalScope := .principalScope .any + actionScope := .actionScope (.eq (mkUid [] "Action" "do")) + resourceScope := .resourceScope (.eq (mkUid [] "Blob" "thing")) + condition := [{ + kind := .when + body := .binaryApp .eq + (.binaryApp .sub + (.getAttr (.var .context) "foo") + (.lit (.int (Int64.mk 7 (by decide)))) + ) + (.getAttr (.var .context) "bar") + }] + }, + { + id := "policy1" + effect := .forbid + principalScope := .principalScope (.is { id := "UnauthenticatedUser", path := [] }) + actionScope := .actionScope .any + resourceScope := .resourceScope .any + condition := [{ + kind := .when + body := .getAttr (.var .resource) "requiresAuthentication" + }] + }, + { + id := "policy2" + effect := .permit + principalScope := .principalScope .any + actionScope := .actionInAny [ + (mkUid [] "Action" "1"), + (mkUid [] "Action" "2"), + ] + resourceScope := .resourceScope .any + condition := [{ + kind := .when + body := .binaryApp .contains + (.set [.lit (.string "a"), .lit (.string "b"), .lit (.string "c")]) + (.getAttr (.var .resource) "type") + }] + }, + ], + testDeserializeProtodata "UnitTest/CedarProto-test-data/request.protodata" + ({ + principal := mkUid [] "User" "alice" + action := mkUid [] "Action" "access" + resource := mkUid [] "Folder" "data" + context := Map.make [ ("foo", .prim (.bool true)) ] + } : Cedar.Spec.Request), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/entity.protodata" + Cedar.Spec.EntityProto.mkWf + ({ + uid := mkUid ["A"] "B" "C" + data := { + attrs := Map.make [ + ("foo", .set (Set.make [ + (.prim (.int (Int64.mk 1 (by decide)))), + (.prim (.int (Int64.mk (-1) (by decide)))), + ])), + ("bar", .prim (.bool false)), + ] + ancestors := Set.make [ + (mkUid [] "Parent" "1"), + (mkUid [] "Grandparent" "A"), + ] + tags := Map.make [ + ("tag1", .prim (.string "val1")), + ("tag2", .prim (.string "val2")), + ] + } + }), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/entities.protodata" + Cedar.Spec.EntitiesProto.toEntities + ((Map.make [ + (mkUid [] "ABC" "123", { attrs := Map.empty, ancestors := Set.empty, tags := Map.empty }), + (mkUid [] "DEF" "234", { attrs := Map.empty, ancestors := Set.empty, tags := Map.empty }), + ]) : Cedar.Spec.Entities), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_true.protodata" + (Cedar.Validation.CedarType.bool .tt), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_false.protodata" + (Cedar.Validation.CedarType.bool .ff), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_bool.protodata" + (Cedar.Validation.CedarType.bool .anyBool), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_long.protodata" + (Cedar.Validation.CedarType.int), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_string.protodata" + (Cedar.Validation.CedarType.string), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_set_of_string.protodata" + (Cedar.Validation.CedarType.set Cedar.Validation.CedarType.string), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_ip.protodata" + (Cedar.Validation.CedarType.ext .ipAddr), + testDeserializeProtodata "UnitTest/CedarProto-test-data/type_record.protodata" + (Cedar.Validation.CedarType.record (Map.make [ + ("eggs", .optional .int), + ("ham", .required .string), + ])), + testDeserializeProtodata' "UnitTest/CedarProto-test-data/schema_basic.protodata" + Cedar.Validation.Proto.ValidatorSchema.toSchema + { + ets := Map.make [ + ({ id := "A", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "B", path := [] }, { + attrs := Map.empty + ancestors := Set.make [{ id := "A", path := [] }] + tags := none + }), + ] + acts := Map.make [ + (mkUid [] "Action" "Read", { + appliesToPrincipal := Set.empty + appliesToResource := Set.empty + ancestors := Set.empty + context := Map.empty + }), + (mkUid [] "Action" "Write", { + appliesToPrincipal := Set.empty + appliesToResource := Set.empty + ancestors := Set.empty + context := Map.empty + }), + (mkUid [] "Action" "ReadX", { + appliesToPrincipal := Set.make [{ id := "A", path := [] }] + appliesToResource := Set.make [{ id := "A", path := [] }, { id := "B", path := [] }] + ancestors := Set.make [mkUid [] "Action" "Read"] + context := Map.empty + }), + ] + }, + testDeserializeProtodata' "UnitTest/CedarProto-test-data/schema_attrs.protodata" + Cedar.Validation.Proto.ValidatorSchema.toSchema + { + ets := Map.make [ + ({ id := "A", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "B", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "C", path := [] }, { + attrs := Map.make [ + ("a", .required (.bool .anyBool)), + ("b", .required .int), + ("c", .optional .string), + ("d", .required (.entity { id := "A", path := [] })), + ("e", .required (.set (.entity {id := "B", path := [] }))), + ("f", .required (.ext .ipAddr)), + ("g", .required (.record (Map.make [ + ("eggs", .optional .int), + ("ham", .required .string), + ("owner", .required (.entity { id := "C", path := [] })), + ]))), + ] + ancestors := Set.empty + tags := none + }), + ] + acts := Map.make [ + (mkUid [] "Action" "Read", { + appliesToPrincipal := Set.empty + appliesToResource := Set.empty + ancestors := Set.empty + context := Map.empty + }), + (mkUid [] "Action" "Write", { + appliesToPrincipal := Set.empty + appliesToResource := Set.empty + ancestors := Set.empty + context := Map.empty + }), + (mkUid [] "Action" "ReadX", { + appliesToPrincipal := Set.make [{ id := "A", path := [] }, { id := "B", path := [] }] + appliesToResource := Set.make [{ id := "B", path := [] }, { id := "C", path := [] }] + ancestors := Set.make [mkUid [] "Action" "Read"] + context := Map.make [ + ("a", .required .string), + ("b", .optional (.entity { id := "B", path := [] })), + ("c", .required (.set (.entity { id := "A", path := [] }))), + ("d", .required (.ext .decimal)), + ("e", .required (.record (Map.make [ + ("eggs", .required .int), + ("ham", .optional (.bool .anyBool)), + ("manager", .required (.entity { id := "B", path := [] })), + ]))) + ] + }), + ] + }, + testDeserializeProtodata' "UnitTest/CedarProto-test-data/schema_commontypes.protodata" + Cedar.Validation.Proto.ValidatorSchema.toSchema + { + ets := Map.make [ + ({ id := "A", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "B", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "C", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "F", path := [] }, { + attrs := Map.make [ + ("z", .required .string), + ("y", .optional (.set (.set (.entity { id := "C", path := [] })))), + ] + ancestors := Set.make [{ id := "A", path := [] }, { id := "B", path := [] }] + tags := none + }), + ] + acts := Map.make [ + (mkUid [] "Action" "Read", { + appliesToPrincipal := Set.make [{ id := "A", path := [] }, { id := "B", path := [] }] + appliesToResource := Set.make [{ id := "C", path := [] }] + ancestors := Set.empty + context := Map.make [ + ("a", .optional (.record (Map.make [ + ("z", .optional .string), + ("y", .required (.record (Map.make [ + ("foo", .required (.set (.entity { id := "C", path := [] }))), + ]))) + ]))), + ("y", .required (.set (.entity { id := "C", path := [] }))), + ] + }) + ] + }, + testDeserializeProtodata' "UnitTest/CedarProto-test-data/schema_tags.protodata" + Cedar.Validation.Proto.ValidatorSchema.toSchema + { + ets := Map.make [ + ({ id := "A", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "B", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := none + }), + ({ id := "C", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := some .string + }), + ({ id := "D", path := [] }, { + attrs := Map.empty + ancestors := Set.make [{ id := "B", path := [] }] + tags := some (.set .string) + }), + ({ id := "E", path := [] }, { + attrs := Map.empty + ancestors := Set.empty + tags := some (.set (.entity { id := "A", path := [] })) + }), + ({ id := "F", path := [] }, { + attrs := Map.make [ + ("z", .required (.set .string)), + ] + ancestors := Set.make [{ id := "A", path := [] }, { id := "B", path := [] }] + tags := some .string + }), + ] + acts := Map.empty + } + ] +] + +-- Uncomment for interactive debugging +-- #eval TestSuite.runAll tests + +end UnitTest.CedarProto diff --git a/cedar-lean/UnitTest/Main.lean b/cedar-lean/UnitTest/Main.lean index d78127f0b..f172d7877 100644 --- a/cedar-lean/UnitTest/Main.lean +++ b/cedar-lean/UnitTest/Main.lean @@ -14,6 +14,7 @@ limitations under the License. -/ +import UnitTest.CedarProto import UnitTest.Datetime import UnitTest.Decimal import UnitTest.IPAddr @@ -27,7 +28,8 @@ def tests := Decimal.tests ++ IPAddr.tests ++ Wildcard.tests ++ - Proto.tests + Proto.tests ++ + CedarProto.tests def main : IO UInt32 := do TestSuite.runAll tests diff --git a/cedar-lean/UnitTest/Proto.lean b/cedar-lean/UnitTest/Proto.lean index 256a0978b..333c2581d 100644 --- a/cedar-lean/UnitTest/Proto.lean +++ b/cedar-lean/UnitTest/Proto.lean @@ -26,8 +26,6 @@ import UnitTest.Run /-! Test Cases for Protobuffer functions -/ -open Proto - -- Show DecidableEq of Except for unit tests namespace Except instance [DecidableEq α] [DecidableEq β] : DecidableEq (Except α β) := by @@ -92,7 +90,6 @@ instance : ProtoEnum A where fromInt := get? end A - def tests := [ UnitTest.suite "General protobuf deserialization tests" ([ UnitTest.test "false" ⟨λ () => UnitTest.checkEq @@ -167,3 +164,8 @@ def tests := [ ⟩, ] : List (UnitTest.TestCase IO)) ] + +-- Uncomment for interactive debugging +-- #eval TestSuite.runAll tests + +end Proto diff --git a/cedar-lean/lakefile.lean b/cedar-lean/lakefile.lean index 3758c5659..4fa6bb4da 100644 --- a/cedar-lean/lakefile.lean +++ b/cedar-lean/lakefile.lean @@ -37,6 +37,9 @@ lean_lib UnitTest where lean_lib Protobuf where defaultFacets := #[LeanLib.staticFacet] +lean_lib CedarProto where + defaultFacets := #[LeanLib.staticFacet] + lean_exe CedarUnitTests where root := `UnitTest.Main