RFC 53 Lean model and proofs (#530)

Signed-off-by: Shaobo He <shaobohe@amazon.com>

Author: shaobo-he-aws

cedar-lean/Cedar/Thm/Validation/RequestEntityValidation.lean

@@ -15,12 +15,17 @@ theorem instance_of_bool_type_refl (b : Bool) (bty : BoolType) :
   intro h₀
   cases h₁ : b <;> cases h₂ : bty <;> subst h₁ <;> subst h₂ <;> simp only [Bool.false_eq_true] at *
 
-theorem instance_of_entity_type_refl (e : EntityUID) (ety : EntityType) :
-  instanceOfEntityType e ety = true → InstanceOfEntityType e ety
+theorem instance_of_entity_type_refl (e : EntityUID) (ety : EntityType) (eids: EntityType → Option (Set String)) :
+  instanceOfEntityType e ety eids = true → InstanceOfEntityType e ety
 := by
   simp only [InstanceOfEntityType, instanceOfEntityType]
   intro h₀
-  simp only [beq_iff_eq] at h₀
+  have h₁ : (ety == e.ty) := by
+    simp at h₀
+    have ⟨ e₁, _ ⟩ := h₀
+    simp
+    exact e₁
+  simp only [beq_iff_eq] at h₁
   assumption
 
 theorem instance_of_ext_type_refl (ext : Ext) (extty : ExtType) :
@@ -30,8 +35,8 @@ theorem instance_of_ext_type_refl (ext : Ext) (extty : ExtType) :
   intro h₀
   cases h₁ : ext <;> cases h₂ : extty <;> subst h₁ <;> subst h₂ <;> simp only [Bool.false_eq_true] at *
 
-theorem instance_of_type_refl (v : Value) (ty : CedarType) :
-  instanceOfType v ty = true → InstanceOfType v ty
+theorem instance_of_type_refl (v : Value) (ty : CedarType) (schema: EntitySchema) :
+  instanceOfType v ty schema = true → InstanceOfType v ty
 := by
   intro h₀
   unfold instanceOfType at h₀
@@ -75,7 +80,7 @@ theorem instance_of_type_refl (v : Value) (ty : CedarType) :
       simp only [← Set.in_list_iff_in_set] at hv
       specialize h₀ ⟨v, hv⟩
       simp only [List.attach_def, List.mem_pmap_subtype, hv, true_implies] at h₀
-      exact instance_of_type_refl v sty h₀
+      exact instance_of_type_refl v sty schema h₀
     all_goals
       contradiction
     all_goals
@@ -114,7 +119,7 @@ theorem instance_of_type_refl (v : Value) (ty : CedarType) :
         simp only [h₈] at h₇
         simp only [h₈, Option.some.injEq] at h₂
         subst h₂
-        exact instance_of_type_refl v vl.getType h₇
+        exact instance_of_type_refl v vl.getType schema h₇
       intro k qty h₁ h₂
       have ⟨⟨_, h₄⟩, h₅⟩ := h₀
       clear h₀
@@ -158,8 +163,8 @@ decreasing_by
     have := Map.sizeOf_lt_of_value h₁
     omega
 
-theorem instance_of_request_type_refl (request : Request) (reqty : RequestType) :
-  instanceOfRequestType request reqty = true → InstanceOfRequestType request reqty
+theorem instance_of_request_type_refl (request : Request) (reqty : RequestType) (schema: EntitySchema):
+  instanceOfRequestType request reqty schema = true → InstanceOfRequestType request reqty
 := by
   intro h₀
   simp only [InstanceOfRequestType]
@@ -203,15 +208,18 @@ theorem instance_of_entity_schema_refl (entities : Entities) (ets : EntitySchema
     split at h₀ <;> try simp only [reduceCtorEq] at h₀
     rename_i h₃
     constructor
-    · exact instance_of_type_refl (Value.record data.attrs) (CedarType.record entry.attrs) h₃
+    · exact instance_of_type_refl (Value.record data.attrs) (CedarType.record entry.attrs) ets h₃
     · split at h₀ <;> try simp only [reduceCtorEq] at h₀
       rename_i h₄
       simp only [Set.all, List.all_eq_true] at h₄
       constructor
       · intro anc ancin
         simp only [Set.contains, List.elem_eq_mem, decide_eq_true_eq] at h₄
         rw [← Set.in_list_iff_in_set] at ancin
-        exact h₄ anc ancin
+        have h₅ := h₄ anc ancin
+        simp at h₅
+        have ⟨ h₆, _ ⟩  := h₅
+        exact h₆
       · split at h₀ <;> try simp only [reduceCtorEq] at h₀
         unfold InstanceOfEntityTags
         rename_i h₅
@@ -247,8 +255,8 @@ theorem instance_of_action_schema_refl (entities : Entities) (acts : ActionSchem
 
 
 
-theorem request_and_entities_match_env (env : Environment) (request : Request) (entities : Entities) :
-  requestMatchesEnvironment env request →
+theorem request_and_entities_match_env (env : Environment) (request : Request) (entities : Entities) (schema: EntitySchema) :
+  requestMatchesEnvironment env request schema →
   entitiesMatchEnvironment env entities = .ok () →
   RequestAndEntitiesMatchEnvironment env request entities
 := by
@@ -257,7 +265,7 @@ theorem request_and_entities_match_env (env : Environment) (request : Request) (
   simp only [requestMatchesEnvironment] at h₀
   simp only [entitiesMatchEnvironment] at h₁
   constructor
-  exact instance_of_request_type_refl request env.reqty h₀
+  exact instance_of_request_type_refl request env.reqty schema h₀
   cases h₂ : instanceOfEntitySchema entities env.ets <;> simp only [h₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at h₁
   constructor
   exact instance_of_entity_schema_refl entities env.ets h₂

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

@@ -902,8 +902,11 @@ private theorem no_tags_type_implies_no_tags {uid : EntityUID} {env : Environmen
     replace ⟨e', h₂, h₃⟩ := h₂
     simp only [hf', Option.some.injEq] at h₂
     subst h₂
-    simp only [h₃] at h₁
-    simp only [h₁, map_empty_contains_instance_of_ff]
+    simp only [EntitySchemaEntry.tags?] at h₁ h₃
+    split at h₃
+    · simp only [h₃] at h₁
+      simp only [h₁, map_empty_contains_instance_of_ff]
+    · simp only [h₁, map_empty_contains_instance_of_ff]
   · exact map_empty_contains_instance_of_ff
 
 private theorem no_type_implies_no_tags {uid : EntityUID} {env : Environment} {entities : Entities}
@@ -1070,6 +1073,8 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e
   replace ⟨_, h₅, h₇⟩ := h₅
   simp only [hf₂, Option.some.injEq] at h₅
   subst h₅
+  simp only [EntitySchemaEntry.tags?] at h₂ h₇
+  split at h₇
   simp only [h₇] at h₂
   have hf₃ := Map.findOrErr_returns d.tags s Error.tagDoesNotExist
   rcases hf₃ with ⟨v, hf₃⟩ | hf₃ <;>
@@ -1084,6 +1089,7 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e
     simp only [Entities.tagsOrEmpty, hf₁, Map.contains_iff_some_find?] at h₁
     replace ⟨_, h₁⟩ := h₁
     simp only [Map.findOrErr_err_iff_find?_none, h₁, reduceCtorEq] at hf₃
+  · cases h₇
 
 theorem type_of_binaryApp_is_sound {op₂ : BinaryOp} {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities}
   (h₁ : CapabilitiesInvariant c₁ request entities)

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

@@ -80,7 +80,7 @@ def InstanceOfRequestType (request : Request) (reqty : RequestType) : Prop :=
   InstanceOfType request.context (.record reqty.context)
 
 def InstanceOfEntityTags (data : EntityData) (entry : EntitySchemaEntry) : Prop :=
-  match entry.tags with
+  match entry.tags? with
   | .some tty => ∀ v ∈ data.tags.values, InstanceOfType v tty
   | .none     => data.tags = Map.empty
 

cedar-lean/Cedar/Validation/RequestEntityValidator.lean

@@ -39,7 +39,11 @@ def instanceOfBoolType (b : Bool) (bty : BoolType) : Bool :=
   | _, .anyBool => true
   | _, _ => false
 
-def instanceOfEntityType (e : EntityUID) (ety : EntityType ) : Bool := ety == e.ty
+def instanceOfEntityType (e : EntityUID) (ety : EntityType ) (eids: EntityType → Option (Set String)) : Bool :=
+  ety == e.ty &&
+  match eids ety with
+  | .some eids => eids.contains e.eid
+  | _ => true
 
 def instanceOfExtType (ext : Ext) (extty: ExtType) : Bool :=
 match ext, extty with
@@ -52,17 +56,17 @@ match rty.find? k with
     | .some qty => if qty.isRequired then r.contains k else true
     | _ => true
 
-def instanceOfType (v : Value) (ty : CedarType) : Bool :=
+def instanceOfType (v : Value) (ty : CedarType) (schema: EntitySchema) : Bool :=
   match v, ty with
   | .prim (.bool b), .bool bty => instanceOfBoolType b bty
   | .prim (.int _), .int => true
   | .prim (.string _), .string => true
-  | .prim (.entityUID e), .entity ety => instanceOfEntityType e ety
-  | .set s, .set ty => s.elts.attach.all (λ ⟨v, _⟩ => instanceOfType v ty)
+  | .prim (.entityUID e), .entity ety => instanceOfEntityType e ety schema.entityTypeMembers?
+  | .set s, .set ty => s.elts.attach.all (λ ⟨v, _⟩ => instanceOfType v ty schema)
   | .record r, .record rty =>
     r.kvs.all (λ (k, _) => rty.contains k) &&
     (r.kvs.attach₂.all (λ ⟨(k, v), _⟩ => (match rty.find? k with
-        | .some qty => instanceOfType v qty.getType
+        | .some qty => instanceOfType v qty.getType schema
         | _ => true))) &&
     rty.kvs.all (λ (k, _) => requiredAttributePresent r rty k)
   | .ext x, .ext xty => instanceOfExtType x xty
@@ -79,11 +83,11 @@ def instanceOfType (v : Value) (ty : CedarType) : Bool :=
         simp only [Map.mk.sizeOf_spec]
         omega
 
-def instanceOfRequestType (request : Request) (reqty : RequestType) : Bool :=
-  instanceOfEntityType request.principal reqty.principal &&
+def instanceOfRequestType (request : Request) (reqty : RequestType) (schema: EntitySchema) : Bool :=
+  instanceOfEntityType request.principal reqty.principal schema.entityTypeMembers? &&
   request.action == reqty.action &&
-  instanceOfEntityType request.resource reqty.resource &&
-  instanceOfType request.context (.record reqty.context)
+  instanceOfEntityType request.resource reqty.resource schema.entityTypeMembers? &&
+  instanceOfType request.context (.record reqty.context) schema
 
 /--
 For every entity in the store,
@@ -97,14 +101,16 @@ def instanceOfEntitySchema (entities : Entities) (ets : EntitySchema) : EntityVa
   entities.toList.forM λ (uid, data) => instanceOfEntityData uid data
 where
   instanceOfEntityTags (data : EntityData) (entry : EntitySchemaEntry) : Bool :=
-    match entry.tags with
-    | .some tty => data.tags.values.all (instanceOfType · tty)
+    match entry.tags? with
+    | .some tty => data.tags.values.all (instanceOfType · tty ets)
     | .none     => data.tags == Map.empty
   instanceOfEntityData uid data :=
     match ets.find? uid.ty with
     |  .some entry =>
-      if instanceOfType data.attrs (.record entry.attrs) then
-        if data.ancestors.all (λ ancestor => entry.ancestors.contains ancestor.ty) then
+      if instanceOfType data.attrs (.record entry.attrs) ets then
+        if data.ancestors.all (λ ancestor =>
+          entry.ancestors.contains ancestor.ty &&
+          instanceOfEntityType ancestor ancestor.ty ets.entityTypeMembers?) then
           if instanceOfEntityTags data entry then .ok ()
           else .error (.typeError s!"entity tags inconsistent with type store")
         else .error (.typeError s!"entity ancestors inconsistent with type store")
@@ -125,10 +131,10 @@ where
                        else .error (.typeError "action ancestors inconsistent with type store information")
       | _ => .error (.typeError s!"action type {uid.eid} not defined in type store")
 
-def requestMatchesEnvironment (env : Environment) (request : Request) : Bool := instanceOfRequestType request env.reqty
+def requestMatchesEnvironment (env : Environment) (request : Request) (schema : EntitySchema): Bool := instanceOfRequestType request env.reqty schema
 
 def validateRequest (schema : Schema) (request : Request) : RequestValidationResult :=
-  if ((schema.toEnvironments.any (requestMatchesEnvironment · request)))
+  if ((schema.toEnvironments.any (requestMatchesEnvironment · request schema.ets)))
   then .ok ()
   else .error (.typeError "request could not be validated in any environment")
 
@@ -158,7 +164,7 @@ def updateSchema (schema : Schema) (actionSchemaEntities : Entities) : Schema :=
       let entriesWithType := actionSchemaEntities.filter (λ k _ => k.ty == ty)
       let allAncestorsForType := List.flatten (entriesWithType.values.map (λ edt =>
         edt.ancestors.elts.map (·.ty) ))
-      let ese : EntitySchemaEntry := {
+      let ese : EntitySchemaEntry := .standard {
         ancestors := Set.make allAncestorsForType,
         attrs := Map.empty,
         tags := Option.none

cedar-lean/Cedar/Validation/Typechecker.lean

@@ -59,7 +59,7 @@ def typeOfLit (p : Prim) (env : Environment) : ResultType :=
   | .int _         => ok .int
   | .string _      => ok .string
   | .entityUID uid =>
-    if env.ets.contains uid.ty || env.acts.contains uid
+    if env.ets.isValidEntityUID uid || env.acts.contains uid
     then ok (.entity uid.ty)
     else err (.unknownEntity uid.ty)
 

cedar-lean/Cedar/Validation/Types.lean

@@ -61,21 +61,52 @@ abbrev QualifiedType := Qualified CedarType
 
 abbrev RecordType := Map Attr QualifiedType
 
-structure EntitySchemaEntry where
+structure StandardSchemaEntry where
   ancestors : Cedar.Data.Set EntityType
   attrs : RecordType
   tags : Option CedarType
 
+inductive EntitySchemaEntry where
+  | standard (ty: StandardSchemaEntry)
+  | enum (eids: Set String)
+
+def EntitySchemaEntry.isValidEntityUID (entry: EntitySchemaEntry) (eid: String): Bool :=
+  match entry with
+  | .standard _ => true
+  | .enum eids => eids.contains eid
+
+def EntitySchemaEntry.tags? : EntitySchemaEntry → Option CedarType
+  | .standard ty => ty.tags
+  | .enum _ => none
+
+def EntitySchemaEntry.attrs : EntitySchemaEntry → RecordType
+  | .standard ty => ty.attrs
+  | .enum _ => Map.empty
+
+def EntitySchemaEntry.ancestors : EntitySchemaEntry → Set EntityType
+  | .standard ty => ty.ancestors
+  | .enum _ => Set.empty
+
 abbrev EntitySchema := Map EntityType EntitySchemaEntry
 
+def EntitySchema.entityTypeMembers? (ets: EntitySchema) (et: EntityType) : Option (Set String) :=
+  match ets.find? et with
+  | .some (.enum eids) => .some eids
+  | _ => .none
+
+def EntitySchema.isValidEntityUID (ets : EntitySchema) (uid : EntityUID) : Bool :=
+  match ets.find? uid.ty with
+  | .some entry => entry.isValidEntityUID uid.eid
+  | .none   => false
+
 def EntitySchema.contains (ets : EntitySchema) (ety : EntityType) : Bool :=
   (ets.find? ety).isSome
 
 def EntitySchema.attrs? (ets : EntitySchema) (ety : EntityType) : Option RecordType :=
   (ets.find? ety).map EntitySchemaEntry.attrs
 
 def EntitySchema.tags? (ets : EntitySchema) (ety : EntityType) : Option (Option CedarType) :=
-  (ets.find? ety).map EntitySchemaEntry.tags
+  (ets.find? ety).map EntitySchemaEntry.tags?
 
 def EntitySchema.descendentOf (ets : EntitySchema) (ety₁ ety₂ : EntityType) : Bool :=
   if ety₁ = ety₂
@@ -124,6 +155,7 @@ deriving instance Repr, DecidableEq, Inhabited for ExtType
 deriving instance Repr, DecidableEq, Inhabited for Qualified
 deriving instance Repr, Inhabited for CedarType
 deriving instance Repr for ActionSchemaEntry
+deriving instance Repr for StandardSchemaEntry
 deriving instance Repr for EntitySchemaEntry
 deriving instance Repr for Schema
 
@@ -198,4 +230,24 @@ end
 
 instance : DecidableEq CedarType := decCedarType
 
+deriving instance DecidableEq for StandardSchemaEntry
+
+def decEntitySchemaEntry (e₁ e₂: EntitySchemaEntry) : Decidable (e₁ = e₂) := by
+  cases e₁ <;> cases e₂
+  case standard.standard t₁ t₂ =>
+    exact match decEq t₁ t₂ with
+    | isTrue h => isTrue (by rw [h])
+    | isFalse _ => isFalse (by intro h; injection h; contradiction)
+  case enum.enum l₁ l₂ =>
+    exact match decEq l₁ l₂ with
+    | isTrue h => isTrue (by rw [h])
+    | isFalse _ => isFalse (by intro h; injection h; contradiction)
+  all_goals {
+    apply isFalse
+    intro h
+    injection h
+  }
+
+instance : DecidableEq EntitySchemaEntry := decEntitySchemaEntry
+
 end Cedar.Validation

cedar-lean/CedarProto/ValidationRequest.lean

@@ -28,7 +28,6 @@ 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
 

cedar-lean/CedarProto/ValidatorSchema.lean

@@ -72,17 +72,13 @@ def toEntitySchema (ets : EntityTypeWithTypesMap) : EntitySchema :=
   Data.Map.make (ets.map
     (λ (k,v) => (k,
       if v.enums.isEmpty then
-      {
+      .standard {
         ancestors := ancestorMap.find! k,
         attrs := Data.Map.make v.attrs.kvs,
         tags := v.tags,
       }
       else
-      {
-        ancestors := ancestorMap.find! k,
-        attrs := Data.Map.empty,
-        tags := none,
-      }
+      .enum $ Cedar.Data.Set.mk v.enums.toList
       )))
 end Cedar.Validation.Proto.EntityTypeWithTypesMap