[cedar-lean] add some more utility functions

cedar-lean/Cedar/Spec/Template.lean

@@ -61,6 +61,8 @@ abbrev Templates := Map TemplateID Template
 
 abbrev SlotEnv := Map SlotID EntityUID
 
+def SlotEnv.empty : SlotEnv := Map.empty
+
 structure TemplateLinkedPolicy where
   id : PolicyID
   templateId : TemplateID

cedar-lean/Cedar/Spec/Value.lean

@@ -132,7 +132,7 @@ deriving instance Repr, DecidableEq, BEq for Except
 deriving instance Repr, DecidableEq for Error
 deriving instance Repr, DecidableEq, Inhabited, Lean.ToJson for Name
 deriving instance Repr, DecidableEq, Inhabited for EntityType
-deriving instance Repr, DecidableEq, Inhabited for EntityUID
+deriving instance Repr, DecidableEq, Inhabited, Lean.ToJson for EntityUID
 deriving instance Repr, DecidableEq, Inhabited for Prim
 deriving instance Repr, Inhabited for Value
 

cedar-lean/Cedar/Validation/Validator.lean

@@ -51,6 +51,23 @@ def Schema.toEnvironments (schema : Schema) : List Environment :=
     reqty := ·
   })
 
+/-- Return the environment for the particular (p,a,r) tuple, or `none` if this
+is not a valid tuple in this schema -/
+def Schema.getEnvironment (schema : Schema) (principalTy resourceTy : EntityType) (action : EntityUID) : Option Environment := do
+  let ase ← schema.acts.find? action
+  match ase.appliesToPrincipal.contains principalTy, ase.appliesToResource.contains resourceTy with
+  | true, true => some {
+    ets := schema.ets,
+    acts := schema.acts,
+    reqty := {
+      principal := principalTy,
+      action := action,
+      resource := resourceTy,
+      context := ase.context,
+    }
+  }
+  | _, _ => none -- principal and/or resource type are invalid for that action
+
 inductive ValidationError where
   | typeError (pid : PolicyID) (error : TypeError)
   | impossiblePolicy (pid : PolicyID)

cedar-lean/DiffTest/Parser.lean

@@ -367,6 +367,12 @@ def jsonToTemplate (json : Lean.Json) : ParseResult Template := do
     condition := condition
   }
 
+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"
+
 def jsonToTemplateLinkedPolicy (id : PolicyID) (json : Lean.Json) : ParseResult TemplateLinkedPolicy := do
   let templateId ← getJsonField json "template_id" >>= jsonToString
   let slotEnvKVs ← getJsonField json "values" >>= jsonObjToKVList