Cedar protobuf structures

cedar-lean/Cedar/Spec/Template.lean

@@ -34,19 +34,23 @@ abbrev SlotID := String
 inductive EntityUIDOrSlot where
   | entityUID (entity : EntityUID)
   | slot (id : SlotID)
+deriving Repr, DecidableEq
 
 inductive ScopeTemplate where
   | any
   | eq (entityOrSlot : EntityUIDOrSlot)
   | 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

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

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

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