Check validity of entity store keys

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

@@ -206,8 +206,18 @@ theorem instance_of_entity_schema_refl (entities : Entities) (ets : EntitySchema
     exists entry
     simp only [true_and]
     split at h₀ <;> try simp only [reduceCtorEq] at h₀
-    rename_i h₃
     constructor
+    rename_i hv
+    simp only [EntitySchemaEntry.isValidEntityEID] at hv
+    simp only [IsValidEntityEID]
+    split at hv
+    · simp
+    · simp
+      rw [Set.contains_prop_bool_equiv] at hv
+      exact hv
+    split at h₀ <;> try simp only [reduceCtorEq] at h₀
+    constructor
+    rename_i 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₄

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

@@ -504,7 +504,7 @@ theorem entity_type_in_false_implies_inₑ_false {euid₁ euid₂ : EntityUID} {
   split at h₃
   case h_1 data h₄ =>
     rw [Set.contains_prop_bool_equiv] at h₃
-    have ⟨entry, h₂₁, _, h₂₂, _⟩ := h₁ euid₁ data h₄
+    have ⟨entry, h₂₁, _, _, h₂₂, _⟩ := h₁ euid₁ data h₄
     specialize h₂₂ euid₂ h₃
     rw [←Set.contains_prop_bool_equiv] at h₂₂
     simp [h₂₁, h₂₂] at h₂
@@ -636,7 +636,7 @@ theorem entity_type_in_false_implies_inₛ_false {euid : EntityUID} {euids : Lis
     cases h₆ : Map.find? entities euid <;>
     simp only [h₆, List.not_mem_nil] at h₅
     rename_i data
-    replace ⟨entry, h₁, _, h₇, _⟩ := h₁ euid data h₆
+    replace ⟨entry, h₁, _, _, h₇, _⟩ := h₁ euid data h₆
     specialize h₇ euid' h₅
     split at h₂ <;> try contradiction
     rename_i h₈
@@ -1067,7 +1067,7 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e
   simp only [hf₁, Except.bind_ok, Except.bind_err, false_implies, Except.error.injEq, or_self, or_false, true_and,
     type_is_inhabited, and_self, reduceCtorEq]
   rw [Map.findOrErr_ok_iff_find?_some] at hf₁
-  replace ⟨entry, hf₂, _, _, h₂⟩  := h₂.right.left uid d hf₁
+  replace ⟨entry, hf₂, _, _, _, h₂⟩  := h₂.right.left uid d hf₁
   simp only [InstanceOfEntityTags] at h₂
   simp only [EntitySchema.tags?, Option.map_eq_some'] at h₅
   replace ⟨_, h₅, h₇⟩ := h₅

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

@@ -84,6 +84,11 @@ def InstanceOfEntityTags (data : EntityData) (entry : EntitySchemaEntry) : Prop
   | .some tty => ∀ v ∈ data.tags.values, InstanceOfType v tty
   | .none     => data.tags = Map.empty
 
+def IsValidEntityEID (entry: EntitySchemaEntry) (eid: String) : Prop :=
+  match entry with
+  | .standard _ => True
+  | .enum eids => eid ∈ eids
+
 /--
 For every entity in the store,
 1. The entity's type is defined in the type store.
@@ -95,6 +100,7 @@ For every entity in the store,
 def InstanceOfEntitySchema (entities : Entities) (ets: EntitySchema) : Prop :=
   ∀ uid data, entities.find? uid = some data →
     ∃ entry, ets.find? uid.ty = some entry ∧
+      IsValidEntityEID entry uid.eid ∧
       InstanceOfType data.attrs (.record entry.attrs) ∧
       (∀ ancestor, ancestor ∈ data.ancestors → ancestor.ty ∈ entry.ancestors) ∧
       InstanceOfEntityTags data entry
@@ -285,7 +291,7 @@ theorem well_typed_entity_attributes {env : Environment} {request : Request} {en
   have ⟨_, h₁, _⟩ := h₁
   simp [InstanceOfEntitySchema] at h₁
   specialize h₁ uid d h₂
-  have ⟨entry, h₁₂, h₁, _⟩ := h₁
+  have ⟨entry, h₁₂, _, h₁, _⟩ := h₁
   unfold EntitySchema.attrs? at h₃
   simp [h₁₂] at h₃
   subst h₃

cedar-lean/Cedar/Validation/RequestEntityValidator.lean

@@ -107,14 +107,16 @@ where
   instanceOfEntityData uid data :=
     match ets.find? uid.ty with
     |  .some entry =>
-      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")
-      else .error (.typeError "entity attributes do not match type store")
+      if entry.isValidEntityEID uid.eid 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")
+        else .error (.typeError "entity attributes do not match type store")
+      else .error (.typeError s!"invalid entity uid: {uid}")
     | _ => .error (.typeError "entity type not defined in type store")
 
 /--

cedar-lean/Cedar/Validation/Types.lean

@@ -70,7 +70,7 @@ inductive EntitySchemaEntry where
   | standard (ty: StandardSchemaEntry)
   | enum (eids: Set String)
 
-def EntitySchemaEntry.isValidEntityUID (entry: EntitySchemaEntry) (eid: String): Bool :=
+def EntitySchemaEntry.isValidEntityEID (entry: EntitySchemaEntry) (eid: String): Bool :=
   match entry with
   | .standard _ => true
   | .enum eids => eids.contains eid
@@ -96,7 +96,7 @@ def EntitySchema.entityTypeMembers? (ets: EntitySchema) (et: EntityType) : Optio
 
 def EntitySchema.isValidEntityUID (ets : EntitySchema) (uid : EntityUID) : Bool :=
   match ets.find? uid.ty with
-  | .some entry => entry.isValidEntityUID uid.eid
+  | .some entry => entry.isValidEntityEID uid.eid
   | .none   => false
 
 def EntitySchema.contains (ets : EntitySchema) (ety : EntityType) : Bool :=