Refactor validator definitions for easier reuse (#202)

Co-authored-by: Emina Torlak <[email protected]>

cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean

@@ -431,7 +431,7 @@ theorem entityUID?_some_implies_entity_lit {x : Expr} {euid : EntityUID}
   split at h₁ <;> simp at h₁ ; subst h₁ ; rfl
 
 
-theorem actionUID?_some_implies_action_lit {x : Expr} {euid : EntityUID} {acts : ActionStore}
+theorem actionUID?_some_implies_action_lit {x : Expr} {euid : EntityUID} {acts : ActionSchema}
   (h₁ : actionUID? x acts = some euid) :
   x = Expr.lit (.entityUID euid) ∧
   acts.contains euid = true
@@ -468,11 +468,11 @@ theorem entityUIDs?_some_implies_entity_lits {x : Expr} {euids : List EntityUID}
     exact h₄
 
 theorem entity_type_in_false_implies_inₑ_false {euid₁ euid₂ : EntityUID} {env : Environment} {entities : Entities}
-  (h₁ : InstanceOfEntityTypeStore entities env.ets)
-  (h₂ : EntityTypeStore.descendentOf env.ets euid₁.ty euid₂.ty = false) :
+  (h₁ : InstanceOfEntitySchema entities env.ets)
+  (h₂ : EntitySchema.descendentOf env.ets euid₁.ty euid₂.ty = false) :
   inₑ euid₁ euid₂ entities = false
 := by
-  simp [EntityTypeStore.descendentOf] at h₂
+  simp [EntitySchema.descendentOf] at h₂
   simp [inₑ] ; by_contra h₃ ; simp at h₃
   rcases h₃ with h₃ | h₃
   case inl => subst h₃ ; simp at h₂
@@ -488,16 +488,16 @@ theorem entity_type_in_false_implies_inₑ_false {euid₁ euid₂ : EntityUID} {
   case h_2 => simp [Set.contains, Set.elts, Set.empty] at h₃
 
 theorem action_type_in_eq_action_inₑ (euid₁ euid₂ : EntityUID) {env : Environment} {entities : Entities}
-  (h₁ : InstanceOfActionStore entities env.acts)
+  (h₁ : InstanceOfActionSchema entities env.acts)
   (h₂ : env.acts.contains euid₁) :
-  inₑ euid₁ euid₂ entities = ActionStore.descendentOf env.acts euid₁ euid₂
+  inₑ euid₁ euid₂ entities = ActionSchema.descendentOf env.acts euid₁ euid₂
 := by
-  simp [InstanceOfActionStore] at h₁
-  simp [ActionStore.contains] at h₂
+  simp [InstanceOfActionSchema] at h₁
+  simp [ActionSchema.contains] at h₂
   cases h₃ : Map.find? env.acts euid₁ <;> simp [h₃] at h₂
   rename_i entry
   have ⟨data, h₁₁, h₁₂⟩ := h₁ euid₁ entry h₃
-  simp [inₑ, ActionStore.descendentOf, h₃, Entities.ancestorsOrEmpty, h₁₁]
+  simp [inₑ, ActionSchema.descendentOf, h₃, Entities.ancestorsOrEmpty, h₁₁]
   rcases h₄ : euid₁ == euid₂ <;> simp at h₄ <;> simp [h₄, h₁₂]
 
 theorem type_of_mem_is_soundₑ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilities} {env : Environment} {request : Request} {entities : Entities} {ety₁ ety₂ : EntityType}
@@ -536,13 +536,13 @@ theorem type_of_mem_is_soundₑ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
   have ⟨_, hents, hacts⟩ := h₂
   cases ha : actionUID? x₁ env.acts <;> simp [ha] at h₇ h₈ h₉
   case none =>
-    cases hin : EntityTypeStore.descendentOf env.ets euid₁.ty euid₂.ty <;>
+    cases hin : EntitySchema.descendentOf env.ets euid₁.ty euid₂.ty <;>
     simp [hin] at h₇ h₈ h₉
     simp [entity_type_in_false_implies_inₑ_false hents hin] at h₉
   case some =>
     cases he : entityUID? x₂ <;> simp [he] at h₇ h₈ h₉
     case none =>
-      cases hin : EntityTypeStore.descendentOf env.ets euid₁.ty euid₂.ty <;>
+      cases hin : EntitySchema.descendentOf env.ets euid₁.ty euid₂.ty <;>
       simp [hin] at h₇ h₈ h₉
       simp [entity_type_in_false_implies_inₑ_false hents hin] at h₉
     case some =>
@@ -554,7 +554,7 @@ theorem type_of_mem_is_soundₑ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
       simp [evaluate] at h₅ h₆ ; subst h₅ h₆
       have h₁₀ := action_type_in_eq_action_inₑ auid euid hacts ha''
       simp [h₁₀] at h₈ h₉
-      cases heq : ActionStore.descendentOf env.acts auid euid <;> simp [heq] at h₈ h₉
+      cases heq : ActionSchema.descendentOf env.acts auid euid <;> simp [heq] at h₈ h₉
 
 theorem entity_set_type_implies_set_of_entities {vs : List Value} {ety : EntityType}
   (h₁ : InstanceOfType (Value.set (Set.mk vs)) (CedarType.set (CedarType.entity ety))) :
@@ -588,13 +588,13 @@ theorem entity_set_type_implies_set_of_entities {vs : List Value} {ety : EntityT
     apply h₅ euid heuid
 
 theorem entity_type_in_false_implies_inₛ_false {euid : EntityUID} {euids : List EntityUID} {ety : EntityType} {env : Environment} {entities : Entities}
-  (h₁ : InstanceOfEntityTypeStore entities env.ets)
-  (h₂ : EntityTypeStore.descendentOf env.ets euid.ty ety = false)
+  (h₁ : InstanceOfEntitySchema entities env.ets)
+  (h₂ : EntitySchema.descendentOf env.ets euid.ty ety = false)
   (h₃ : ∀ euid, euid ∈ euids → euid.ty = ety) :
   Set.any (fun x => inₑ euid x entities) (Set.make euids) = false
 := by
-  simp [InstanceOfEntityTypeStore] at h₁
-  simp [EntityTypeStore.descendentOf] at h₂
+  simp [InstanceOfEntitySchema] at h₁
+  simp [EntitySchema.descendentOf] at h₂
   rw [Set.make_any_iff_any]
   by_contra h₄ ; simp at h₄
   have ⟨euid', h₄, h₅⟩ := h₄
@@ -691,17 +691,17 @@ theorem evaluate_entity_set_eqv {vs : List Value} {euids euids' : List EntityUID
   case right => apply hl₁
 
 theorem action_type_in_eq_action_inₛ {auid : EntityUID} {euids euids' : List EntityUID} {env : Environment} {entities : Entities}
-  (h₁ : InstanceOfActionStore entities env.acts)
+  (h₁ : InstanceOfActionSchema entities env.acts)
   (h₂ : env.acts.contains auid)
   (h₃ : euids ≡ euids') :
   Set.any (fun x => inₑ auid x entities) (Set.make euids) ↔
-  ∃ euid, euid ∈ euids' ∧ ActionStore.descendentOf env.acts auid euid
+  ∃ euid, euid ∈ euids' ∧ ActionSchema.descendentOf env.acts auid euid
 := by
   rw [Set.make_any_iff_any]
-  simp [ActionStore.contains] at h₂
+  simp [ActionSchema.contains] at h₂
   cases h₄ : Map.find? env.acts auid <;> simp [h₄] at h₂
   rename_i entry
-  simp [InstanceOfActionStore] at h₁
+  simp [InstanceOfActionSchema] at h₁
   specialize h₁ auid entry
   constructor <;> intro h₄ <;> rename_i hfnd <;>
   simp [hfnd] at h₁ <;>
@@ -716,9 +716,9 @@ theorem action_type_in_eq_action_inₛ {auid : EntityUID} {euids euids' : List E
     simp [inₑ] at h₅
     rcases h₅ with h₅ | h₅
     case inl =>
-      subst h₅ ; simp [ActionStore.descendentOf]
+      subst h₅ ; simp [ActionSchema.descendentOf]
     case inr =>
-      simp [ActionStore.descendentOf, hfnd]
+      simp [ActionSchema.descendentOf, hfnd]
       intro _
       simp [Entities.ancestorsOrEmpty, hl₁, hr₁] at h₅
       exact h₅
@@ -729,7 +729,7 @@ theorem action_type_in_eq_action_inₛ {auid : EntityUID} {euids euids' : List E
     have ⟨_, h₃⟩ := h₃
     simp [List.subset_def] at h₃
     specialize h₃ h₄ ; simp [h₃]
-    simp [ActionStore.descendentOf, hfnd] at h₅
+    simp [ActionSchema.descendentOf, hfnd] at h₅
     by_cases h₆ : auid = euid <;> simp [h₆] at h₅
     case pos =>
       subst h₆ ; simp [inₑ]
@@ -774,13 +774,13 @@ theorem type_of_mem_is_soundₛ {x₁ x₂ : Expr} {c₁ c₁' c₂' : Capabilit
   simp [typeOfInₛ] at *
   cases ha : actionUID? x₁ env.acts <;> simp [ha] at h₈ h₉ h₁₀
   case none =>
-    cases hin : EntityTypeStore.descendentOf env.ets euid.ty ety₂ <;>
+    cases hin : EntitySchema.descendentOf env.ets euid.ty ety₂ <;>
     simp [hin] at h₈ h₉ h₁₀
     simp [entity_type_in_false_implies_inₛ_false hents hin hty₇] at h₁₀
   case some =>
     cases he : entityUIDs? x₂ <;> simp [he] at h₈ h₉ h₁₀
     case none =>
-      cases hin : EntityTypeStore.descendentOf env.ets euid.ty ety₂ <;>
+      cases hin : EntitySchema.descendentOf env.ets euid.ty ety₂ <;>
       simp [hin] at h₈ h₉ h₁₀
       simp [entity_type_in_false_implies_inₛ_false hents hin hty₇] at h₁₀
     case some =>

cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean

@@ -85,7 +85,7 @@ For every entity in the store,
 3. The entity's ancestors' types are consistent with the ancestor information
    in the type store.
 -/
-def InstanceOfEntityTypeStore (entities : Entities) (ets: EntityTypeStore) : Prop :=
+def InstanceOfEntitySchema (entities : Entities) (ets: EntitySchema) : Prop :=
   ∀ uid data, entities.find? uid = some data →
     ∃ entry, ets.find? uid.ty = some entry ∧
       InstanceOfType data.attrs (.record entry.attrs) ∧
@@ -95,17 +95,17 @@ def InstanceOfEntityTypeStore (entities : Entities) (ets: EntityTypeStore) : Pro
 For every action in the entity store, the action's ancestors are consistent
 with the ancestor information in the action store.
 -/
-def InstanceOfActionStore (entities : Entities) (as: ActionStore) : Prop :=
-  ∀ (uid : EntityUID) (entry : ActionStoreEntry),
+def InstanceOfActionSchema (entities : Entities) (as: ActionSchema) : Prop :=
+  ∀ (uid : EntityUID) (entry : ActionSchemaEntry),
   Map.find? as uid = some entry →
   ∃ data,
     Map.find? entities uid = some data ∧
     data.ancestors = entry.ancestors
 
 def RequestAndEntitiesMatchEnvironment (env : Environment) (request : Request) (entities : Entities) : Prop :=
   InstanceOfRequestType request env.reqty ∧
-  InstanceOfEntityTypeStore entities env.ets ∧
-  InstanceOfActionStore entities env.acts
+  InstanceOfEntitySchema entities env.ets ∧
+  InstanceOfActionSchema entities env.acts
 
 ----- Theorems -----
 
@@ -271,14 +271,14 @@ theorem required_attribute_is_present {r : Map Attr Value} {rty : RecordType} {a
 theorem well_typed_entity_attributes {env : Environment} {request : Request} {entities : Entities} {uid: EntityUID} {d: EntityData} {rty : RecordType}
   (h₁ : RequestAndEntitiesMatchEnvironment env request entities)
   (h₂ : Map.find? entities uid = some d)
-  (h₃ : EntityTypeStore.attrs? env.ets uid.ty = some rty) :
+  (h₃ : EntitySchema.attrs? env.ets uid.ty = some rty) :
   InstanceOfType d.attrs (.record rty)
 := by
   have ⟨_, h₁, _⟩ := h₁
-  simp [InstanceOfEntityTypeStore] at h₁
+  simp [InstanceOfEntitySchema] at h₁
   specialize h₁ uid d h₂
   have ⟨entry, h₁₂, h₁, _⟩ := h₁
-  unfold EntityTypeStore.attrs? at h₃
+  unfold EntitySchema.attrs? at h₃
   simp [h₁₂] at h₃
   subst h₃
   exact h₁

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -22,6 +22,16 @@ namespace Cedar.Validation
 open Cedar.Data
 open Cedar.Spec
 
+inductive TypeError where
+  | lubErr (ty₁ : CedarType) (ty₂ : CedarType)
+  | unexpectedType (ty : CedarType)
+  | attrNotFound (ty : CedarType) (attr : Attr)
+  | unknownEntity (ety : EntityType)
+  | extensionErr (xs : List Expr)
+  | emptySetErr
+  | incompatibleSetTypes (ty : List CedarType)
+deriving Repr, DecidableEq
+
 abbrev Capabilities := List (Expr × Attr)
 
 def Capabilities.singleton (e : Expr) (a : Attr) : Capabilities := [(e, a)]
@@ -31,17 +41,6 @@ abbrev ResultType := Except TypeError (CedarType × Capabilities)
 def ok (ty : CedarType) (c : Capabilities := ∅) : ResultType := .ok (ty, c)
 def err (e : TypeError) : ResultType := .error e
 
-structure RequestType where
-  principal : EntityType
-  action : EntityUID
-  resource : EntityType
-  context : RecordType
-
-structure Environment where
-  ets : EntityTypeStore
-  acts : ActionStore
-  reqty : RequestType
-
 def typeOfLit (p : Prim) (env : Environment) : ResultType :=
   match p with
   | .bool true     => ok (.bool .tt)
@@ -131,7 +130,7 @@ def entityUIDs? : Expr → Option (List EntityUID)
   | .set xs => xs.mapM entityUID?
   | _       => .none
 
-def actionUID? (x : Expr) (acts: ActionStore) : Option EntityUID := do
+def actionUID? (x : Expr) (acts: ActionSchema) : Option EntityUID := do
   let uid ← entityUID? x
   if acts.contains uid then .some uid else .none
 

cedar-lean/Cedar/Validation/Types.lean

@@ -61,58 +61,67 @@ abbrev QualifiedType := Qualified CedarType
 
 abbrev RecordType := Map Attr QualifiedType
 
-inductive TypeError where
-  | lubErr (ty₁ : CedarType) (ty₂ : CedarType)
-  | unexpectedType (ty : CedarType)
-  | attrNotFound (ty : CedarType) (attr : Attr)
-  | unknownEntity (ety : EntityType)
-  | extensionErr (xs : List Expr)
-  | emptySetErr
-  | incompatibleSetTypes (ty : List CedarType)
-
-structure EntityTypeStoreEntry where
+structure EntitySchemaEntry where
   ancestors : Cedar.Data.Set EntityType
   attrs : RecordType
 
-abbrev EntityTypeStore := Map EntityType EntityTypeStoreEntry
+abbrev EntitySchema := Map EntityType EntitySchemaEntry
 
-def EntityTypeStore.contains (ets : EntityTypeStore) (ety : EntityType) : Bool :=
+def EntitySchema.contains (ets : EntitySchema) (ety : EntityType) : Bool :=
   (ets.find? ety).isSome
 
-def EntityTypeStore.attrs? (ets : EntityTypeStore) (ety : EntityType) : Option RecordType :=
-  (ets.find? ety).map EntityTypeStoreEntry.attrs
+def EntitySchema.attrs? (ets : EntitySchema) (ety : EntityType) : Option RecordType :=
+  (ets.find? ety).map EntitySchemaEntry.attrs
 
-def EntityTypeStore.descendentOf (ets : EntityTypeStore) (ety₁ ety₂ : EntityType) : Bool :=
+def EntitySchema.descendentOf (ets : EntitySchema) (ety₁ ety₂ : EntityType) : Bool :=
   if ety₁ = ety₂
   then true
   else match ets.find? ety₁ with
     | .some entry => entry.ancestors.contains ety₂
     | .none => false
 
-structure ActionStoreEntry where
-  ancestors : Cedar.Data.Set EntityUID
+structure ActionSchemaEntry where
+  appliesToPrincipal : Set EntityType
+  appliesToResource : Set EntityType
+  ancestors : Set EntityUID
+  context : RecordType
 
-abbrev ActionStore := Map EntityUID ActionStoreEntry
+abbrev ActionSchema := Map EntityUID ActionSchemaEntry
 
-def ActionStore.contains (as : ActionStore) (uid : EntityUID) : Bool :=
+def ActionSchema.contains (as : ActionSchema) (uid : EntityUID) : Bool :=
   (as.find? uid).isSome
 
-def ActionStore.descendentOf (as : ActionStore)  (uid₁ uid₂ : EntityUID) : Bool :=
+def ActionSchema.descendentOf (as : ActionSchema)  (uid₁ uid₂ : EntityUID) : Bool :=
   if uid₁ == uid₂
   then true
   else match as.find? uid₁ with
     | .some entry => entry.ancestors.contains uid₂
     | .none => false
 
+structure Schema where
+  ets : EntitySchema
+  acts : ActionSchema
+
+structure RequestType where
+  principal : EntityType
+  action : EntityUID
+  resource : EntityType
+  context : RecordType
+
+structure Environment where
+  ets : EntitySchema
+  acts : ActionSchema
+  reqty : RequestType
+
 ----- Derivations -----
 
 deriving instance Repr, DecidableEq for BoolType
 deriving instance Repr, DecidableEq, Inhabited for ExtType
 deriving instance Repr, DecidableEq, Inhabited for Qualified
 deriving instance Repr, Inhabited for CedarType
-deriving instance Repr for TypeError
-deriving instance Repr for EntityTypeStoreEntry
-deriving instance Repr for ActionStoreEntry
+deriving instance Repr for ActionSchemaEntry
+deriving instance Repr for EntitySchemaEntry
+deriving instance Repr for Schema
 
 mutual
 
@@ -185,6 +194,4 @@ end
 
 instance : DecidableEq CedarType := decCedarType
 
-deriving instance DecidableEq for TypeError
-
 end Cedar.Validation

cedar-lean/Cedar/Validation/Validator.lean

@@ -25,23 +25,11 @@ open Cedar.Data
 
 ----- Definitions -----
 
-structure SchemaActionEntry where
-  appliesToPrincipal : Set EntityType
-  appliesToResource : Set EntityType
-  ancestors : Set EntityUID
-  context : RecordType
-
-abbrev SchemaActionStore := Map EntityUID SchemaActionEntry
-
-structure Schema where
-  ets : EntityTypeStore
-  acts : SchemaActionStore
-
 /--
 For a given action, compute the cross-product of the applicable principal and
 resource types.
 -/
-def SchemaActionEntry.toRequestTypes (action : EntityUID) (entry : SchemaActionEntry) : List RequestType :=
+def ActionSchemaEntry.toRequestTypes (action : EntityUID) (entry : ActionSchemaEntry) : List RequestType :=
   entry.appliesToPrincipal.toList.foldl (fun acc principal =>
     let reqtys : List RequestType :=
       entry.appliesToResource.toList.map (fun resource =>
@@ -59,7 +47,7 @@ def Schema.toEnvironments (schema : Schema) : List Environment :=
     schema.acts.toList.foldl (fun acc (action,entry) => entry.toRequestTypes action ++ acc) ∅
   requestTypes.map ({
     ets := schema.ets,
-    acts := schema.acts.mapOnValues (fun entry => { ancestors := entry.ancestors }),
+    acts := schema.acts,
     reqty := ·
   })
 
@@ -144,8 +132,6 @@ def validate (policies : Policies) (schema : Schema) : ValidationResult :=
 
 ----- Derivations -----
 
-deriving instance Repr for SchemaActionEntry
-deriving instance Repr for Schema
 deriving instance Repr for ValidationError
 
 /-