diff --git a/cedar-lean/Cedar/Thm/Validation/RequestEntityValidation.lean b/cedar-lean/Cedar/Thm/Validation/RequestEntityValidation.lean index 329eab2fe..8e6789d55 100644 --- a/cedar-lean/Cedar/Thm/Validation/RequestEntityValidation.lean +++ b/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₄ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean index 404192c0a..ffe5a000c 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean +++ b/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₅ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean index b47febf48..4328eb33f 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Types.lean +++ b/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₃ diff --git a/cedar-lean/Cedar/Validation/RequestEntityValidator.lean b/cedar-lean/Cedar/Validation/RequestEntityValidator.lean index a4b91057b..24e13ac85 100644 --- a/cedar-lean/Cedar/Validation/RequestEntityValidator.lean +++ b/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") /-- diff --git a/cedar-lean/Cedar/Validation/Types.lean b/cedar-lean/Cedar/Validation/Types.lean index 05a74f1e3..4b821e5fb 100644 --- a/cedar-lean/Cedar/Validation/Types.lean +++ b/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 :=