From 5e64bec88fd73a6e64d9ced941d2be973ad3ed40 Mon Sep 17 00:00:00 2001 From: John Kastner Date: Thu, 6 Mar 2025 18:56:34 +0000 Subject: [PATCH] Extend typechecker inversion lemma for type annotation Signed-off-by: John Kastner --- .../Cedar/Thm/Validation/Typechecker/And.lean | 102 ++++++------ .../Thm/Validation/Typechecker/BinaryApp.lean | 22 +++ .../Typechecker/BinaryApp/GetTag.lean | 60 +++---- .../Thm/Validation/Typechecker/Call.lean | 49 ++++++ .../Thm/Validation/Typechecker/GetAttr.lean | 33 ++-- .../Thm/Validation/Typechecker/HasAttr.lean | 68 +++++--- .../Validation/Typechecker/IfThenElse.lean | 80 +++++----- .../Thm/Validation/Typechecker/LitVar.lean | 9 ++ .../Cedar/Thm/Validation/Typechecker/Or.lean | 113 +++++++------ .../Thm/Validation/Typechecker/Record.lean | 148 +++++++++++------- .../Cedar/Thm/Validation/Typechecker/Set.lean | 61 +++++--- .../Thm/Validation/Typechecker/UnaryApp.lean | 27 +++- cedar-lean/Cedar/Validation/Typechecker.lean | 6 +- 13 files changed, 486 insertions(+), 292 deletions(-) diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean index 2d70bb61e..709ac25a0 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean @@ -26,17 +26,20 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation -theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.and x₁ x₂) c env = Except.ok (ty, c')) : - ∃ bty₁ c₁, - (typeOf x₁ c env).typeOf = .ok (.bool bty₁, c₁) ∧ +theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.and x₁ x₂) c env = Except.ok (tx, c')) : + ∃ tx₁ bty₁ c₁, + typeOf x₁ c env = .ok (tx₁, c₁) ∧ + tx₁.typeOf = .bool bty₁ ∧ if bty₁ = BoolType.ff - then ty.typeOf = .bool BoolType.ff ∧ c' = ∅ - else ∃ bty₂ c₂, - (typeOf x₂ (c ∪ c₁) env).typeOf = .ok (.bool bty₂, c₂) ∧ + then tx = tx₁ ∧ c' = ∅ + else ∃ bty tx₂ bty₂ c₂, + tx = (.and tx₁ tx₂ (.bool bty)) ∧ + typeOf x₂ (c ∪ c₁) env = .ok (tx₂, c₂) ∧ + tx₂.typeOf = .bool bty₂ ∧ if bty₂ = BoolType.ff - then ty.typeOf = .bool BoolType.ff ∧ c' = ∅ - else ty.typeOf = .bool (lubBool bty₁ bty₂) ∧ c' = c₁ ∪ c₂ + then bty = BoolType.ff ∧ c' = ∅ + else bty = lubBool bty₁ bty₂ ∧ c' = c₁ ∪ c₂ := by simp [typeOf] at h₁ cases h₂ : typeOf x₁ c env <;> simp [h₂] at * @@ -46,10 +49,9 @@ theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : En case ok.h_1 h₃ => have ⟨ hl₁, hr₁ ⟩ := h₁ subst hl₁ hr₁ - exists BoolType.ff, res₁.snd - simp [ResultType.typeOf, Except.map, h₃] + exists res₁.fst, BoolType.ff, res₁.snd case ok.h_2 bty₁ h₃ h₄ => - exists bty₁, res₁.snd + exists res₁.fst, bty₁, res₁.snd simp [h₄, ResultType.typeOf, Except.map] split ; contradiction cases h₄ : typeOf x₂ (c ∪ res₁.snd) env <;> simp [h₄] at * @@ -57,39 +59,46 @@ theorem type_of_and_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : En split at h₁ <;> simp at h₁ <;> have ⟨hty, hc⟩ := h₁ <;> subst hty hc case isFalse.ok.h_1 hty₂ => - exists BoolType.ff, res₂.snd + exists .ff, res₂.fst + apply And.intro (by simp) + exists .ff, res₂.snd case isFalse.ok.h_2 hty₂ => - exists BoolType.tt, res₂.snd ; simp [←hty₂] - cases bty₁ <;> simp at h₃ <;> simp [lubBool, TypedExpr.typeOf] + exists bty₁, res₂.fst + apply And.intro (by simp) + exists BoolType.tt, res₂.snd + cases bty₁ + case ff => contradiction + all_goals + simp [hty₂, lubBool] case isFalse.ok.h_3 bty₂ h₄ h₅ hty₂ => + exists .anyBool, res₂.fst + apply And.intro (by simp) exists BoolType.anyBool, res₂.snd - cases bty₂ <;> simp at * - simp [hty₂, lubBool] - split <;> rename_i h₆ - · simp [h₆, TypedExpr.typeOf] - · rfl + have _ : bty₂ = .anyBool := by + cases bty₂ <;> simp at h₄ h₅ ⊢ + subst bty₂ + cases bty₁ <;> simp [hty₂, lubBool] -theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} +theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : typeOf (Expr.and x₁ x₂) c₁ env = Except.ok (ty, c₂)) + (h₃ : typeOf (Expr.and x₁ x₂) c₁ env = Except.ok (tx, c₂)) (ih₁ : TypeOfIsSound x₁) (ih₂ : TypeOfIsSound x₂) : GuardedCapabilitiesInvariant (Expr.and x₁ x₂) c₂ request entities ∧ - ∃ v, EvaluatesTo (Expr.and x₁ x₂) request entities v ∧ InstanceOfType v ty.typeOf + ∃ v, EvaluatesTo (Expr.and x₁ x₂) request entities v ∧ InstanceOfType v tx.typeOf := by - have ⟨bty₁, rc₁, h₄, h₅⟩ := type_of_and_inversion h₃ - split_type_of h₄ ; rename_i h₄ hl₄ hr₄ + have ⟨tx₁, bty₁, rc₁, h₄, h₅, h₆⟩ := type_of_and_inversion h₃ specialize ih₁ h₁ h₂ h₄ have ⟨ih₁₁, v₁, ih₁₂, ih₁₃⟩ := ih₁ - rw [hl₄] at ih₁₃ + rw [h₅] at ih₁₃ have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃ subst hb₁ - split at h₅ - case isTrue h₆ => - subst h₆ - have ⟨hty, hc⟩ := h₅ - rw [hty, hc] + split at h₆ + case isTrue h₇ => + subst h₇ + have ⟨hty, hc⟩ := h₆ + rw [hty, hc, h₅] apply And.intro empty_guarded_capabilities_invariant have h₇ := instance_of_ff_is_false ih₁₃ simp at h₇ ; subst h₇ @@ -98,13 +107,13 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;> try exact type_is_inhabited (CedarType.bool BoolType.ff) exact false_is_instance_of_ff - case isFalse h₆ => - have ⟨bty₂, rc₂, hₜ, h₇⟩ := h₅ - split at h₇ <;> have ⟨hty, hc⟩ := h₇ <;> rw [hty, hc] - case isTrue h₈ => - subst h₈ + case isFalse h₇ => + replace ⟨bty, tx₂, bty₂, rc₂, htx, htx₂, hty₂, h₆⟩ := h₆ + split at h₆ <;> have ⟨hbty, hc⟩ := h₆ <;> subst bty c₂ tx + case isTrue hbty₂ => + subst bty₂ apply And.intro empty_guarded_capabilities_invariant - exists false ; simp [false_is_instance_of_ff] + exists false ; simp [TypedExpr.typeOf, false_is_instance_of_ff] cases b₁ case false => rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> @@ -115,22 +124,20 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env simp [GuardedCapabilitiesInvariant] at ih₁₁ specialize ih₁₁ ih₁₂ have h₇ := capability_union_invariant h₁ ih₁₁ - split_type_of hₜ ; rename_i hₜ hlₜ hrₜ - subst hr₄ - specialize ih₂ h₇ h₂ hₜ + specialize ih₂ h₇ h₂ htx₂ have ⟨_, v₂, ih₂₂, ih₂₃⟩ := ih₂ simp [EvaluatesTo] at ih₂₂ rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;> simp [Result.as, ih₂₂, Coe.coe, Value.asBool, Lean.Internal.coeM, pure, Except.pure] - rw [hlₜ] at ih₂₃ + rw [hty₂] at ih₂₃ have h₈ := instance_of_ff_is_false ih₂₃ subst h₈ simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe] - case isFalse h₈ => + case isFalse hbty₂ => cases b₁ case false => rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> - simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant] <;> + simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant, TypedExpr.typeOf] <;> try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂)) apply instance_of_lubBool simp [ih₁₃] @@ -140,26 +147,23 @@ theorem type_of_and_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂)) simp [GuardedCapabilitiesInvariant] at ih₁₁ specialize ih₁₁ ih₁₂ - split_type_of hₜ ; rename_i hₜ hlₜ hrₜ - subst hr₄ have h₇ := capability_union_invariant h₁ ih₁₁ - specialize ih₂ h₇ h₂ hₜ + specialize ih₂ h₇ h₂ htx₂ have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂ simp [EvaluatesTo] at ih₂₂ rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;> simp [EvaluatesTo, evaluate, Result.as, ih₂₂, Coe.coe, Value.asBool, Lean.Internal.coeM, pure, Except.pure] <;> try exact type_is_inhabited (CedarType.bool (lubBool bty₁ bty₂)) - rw [hlₜ] at ih₂₃ + rw [hty₂] at ih₂₃ have ⟨b₂, hb₂⟩ := instance_of_bool_is_bool ih₂₃ subst hb₂ - cases b₂ <;> simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe] + cases b₂ <;> simp [TypedExpr.typeOf, CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe] case false => apply instance_of_lubBool ; simp [ih₂₃] case true => apply And.intro · simp [GuardedCapabilitiesInvariant] at ih₂₁ specialize ih₂₁ ih₂₂ - rw [hrₜ] at ih₂₁ exact capability_union_invariant ih₁₁ ih₂₁ · apply instance_of_lubBool ; simp [ih₁₃] diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean index 17c74720a..0e9469a4c 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean @@ -35,6 +35,28 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation +theorem type_of_binaryApp_inversion {op₂ : BinaryOp} {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (htx : typeOf (Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (tx, c')) : + ∃ tx₁ c₁ tx₂ c₂, + typeOf x₁ c env = Except.ok (tx₁, c₁) ∧ + typeOf x₂ c env = Except.ok (tx₂, c₂) ∧ + ∃ ty, tx = .binaryApp op₂ tx₁ tx₂ ty +:= by + simp only [typeOf] at htx + cases htx₁ : typeOf x₁ c env <;> simp only [htx₁, Except.bind_err, reduceCtorEq] at htx + cases htx₂ : typeOf x₂ c env <;> simp only [htx₂, Except.bind_err, Except.bind_ok, reduceCtorEq] at htx + rename_i r₁ r₂ + simp [typeOfBinaryApp, typeOfEq, ifLubThenBool, typeOfGetTag, typeOfHasTag, ok, err] at htx + (split at htx <;> try split at htx <;> try split at htx <;> try split at htx) <;> try simp at htx + all_goals + have ⟨ htx, _ ⟩ := htx + rw [←htx] + exists r₁.fst, r₁.snd, r₂.fst, r₂.snd + and_intros + · rfl + · rfl + · simp only [TypedExpr.binaryApp.injEq, true_and, exists_eq'] + 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) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp/GetTag.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp/GetTag.lean index 9d481ae2c..628acbcba 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp/GetTag.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp/GetTag.lean @@ -26,13 +26,16 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation -theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = .ok (ty, c₂)) : +theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = .ok (tx, c₂)) : c₂ = [] ∧ - ∃ ety c₁' c₂', - (typeOf x₁ c₁ env).typeOf = .ok (.entity ety, c₁') ∧ - (typeOf x₂ c₁ env).typeOf = .ok (.string, c₂') ∧ - env.ets.tags? ety = some (some ty.typeOf) ∧ + ∃ ety ty tx₁ tx₂ c₁' c₂', + typeOf x₁ c₁ env = .ok (tx₁, c₁') ∧ + tx₁.typeOf = .entity ety ∧ + typeOf x₂ c₁ env = .ok (tx₂, c₂') ∧ + tx₂.typeOf = .string ∧ + env.ets.tags? ety = some (some ty) ∧ + tx = .binaryApp .getTag tx₁ tx₂ ty ∧ (x₁, .tag x₂) ∈ c₁ := by simp only [typeOf] at h₁ @@ -41,37 +44,36 @@ theorem type_of_getTag_inversion {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} { rename_i tyc₁ tyc₂ cases tyc₁ cases tyc₂ - rename_i ty₁ c₁' ty₂ c₂' + rename_i tx₁ c₁' tx₂ c₂' simp only at h₁ - cases h₄ : ty₁.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₄] at h₁ - cases h₅ : ty₂.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₅] at h₁ + cases h₄ : tx₁.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₄] at h₁ + cases h₅ : tx₂.typeOf <;> simp [typeOfBinaryApp, err, reduceCtorEq, h₅] at h₁ rename_i ety simp only [typeOfGetTag, List.empty_eq] at h₁ split at h₁ <;> simp only [ok, err, Except.bind_err, reduceCtorEq] at h₁ split at h₁ <;> simp only [Except.bind_ok, Except.bind_err, Except.ok.injEq, Prod.mk.injEq, List.nil_eq, reduceCtorEq] at h₁ + rename_i ty _ _ rename_i h₆ h₇ replace ⟨h₁, h₁'⟩ := h₁ subst h₁ h₁' simp only [true_and] - exists ety + exists ety, ty, tx₁, tx₂ simp only [ResultType.typeOf, Except.map, h₄, h₅, h₆, h₇] simp [TypedExpr.typeOf] -theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} +theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = Except.ok (ty, c₂)) + (h₃ : typeOf (Expr.binaryApp .getTag x₁ x₂) c₁ env = Except.ok (tx, c₂)) (ih₁ : TypeOfIsSound x₁) (ih₂ : TypeOfIsSound x₂) : GuardedCapabilitiesInvariant (Expr.binaryApp .getTag x₁ x₂) c₂ request entities ∧ - ∃ v, EvaluatesTo (Expr.binaryApp .getTag x₁ x₂) request entities v ∧ InstanceOfType v ty.typeOf + ∃ v, EvaluatesTo (Expr.binaryApp .getTag x₁ x₂) request entities v ∧ InstanceOfType v tx.typeOf := by - replace ⟨hc, ety, c₁', c₂', h₃, h₄, h₅, h₆⟩ := type_of_getTag_inversion h₃ + replace ⟨hc, ety, ty, tx₁, tx₂, c₁', c₂', h₃, h₄, h₅, h₆, ht, htx, hc₁⟩ := type_of_getTag_inversion h₃ subst hc - split_type_of h₃ ; rename_i h₃ hl₃ hr₃ - split_type_of h₄ ; rename_i h₄ hl₄ hr₄ replace ⟨_, v₁, ih₁, hty₁⟩ := ih₁ h₁ h₂ h₃ - replace ⟨_, v₂, ih₂, hty₂⟩ := ih₂ h₁ h₂ h₄ + replace ⟨_, v₂, ih₂, hty₂⟩ := ih₂ h₁ h₂ h₅ simp only [EvaluatesTo] at * simp only [GuardedCapabilitiesInvariant, evaluate] rcases ih₁ with ih₁ | ih₁ | ih₁ | ih₁ <;> @@ -80,9 +82,9 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e rcases ih₂ with ih₂ | ih₂ | ih₂ | ih₂ <;> simp only [ih₂, Except.bind_ok, Except.bind_err, false_implies, Except.error.injEq, or_false, or_true, true_and, reduceCtorEq] any_goals (apply type_is_inhabited) - rw [hl₃] at hty₁ + rw [h₄] at hty₁ replace ⟨uid, hty₁, hv₁⟩ := instance_of_entity_type_is_entity hty₁ - rw [hl₄] at hty₂ + rw [h₆] at hty₂ replace ⟨s, hv₂⟩ := instance_of_string_is_string hty₂ subst hv₁ hv₂ hty₁ simp only [apply₂, hasTag, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq, false_or, exists_eq_left'] @@ -94,26 +96,26 @@ theorem type_of_getTag_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {e rw [Map.findOrErr_ok_iff_find?_some] at 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₅ - 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₂ + simp [EntitySchema.tags?, Option.map_eq_some'] at ht + replace ⟨_, ht₁, ht₂⟩ := ht + simp only [hf₂, Option.some.injEq] at ht₁ + subst ht₁ + simp only [EntitySchemaEntry.tags?] at h₂ ht₂ + split at ht₂ + simp only [ht₂] at h₂ have hf₃ := Map.findOrErr_returns d.tags s Error.tagDoesNotExist rcases hf₃ with ⟨v, hf₃⟩ | hf₃ <;> simp only [hf₃, false_implies, Except.error.injEq, or_self, false_and, exists_const, and_false, Except.ok.injEq, false_or, exists_eq_left', reduceCtorEq] - · simp only [← List.empty_eq, empty_capabilities_invariant request entities, implies_true, true_and, reduceCtorEq] + · simp only [htx, TypedExpr.typeOf, ← List.empty_eq, empty_capabilities_invariant request entities, implies_true, true_and, reduceCtorEq] apply h₂ exact Map.findOrErr_ok_implies_in_values hf₃ - · replace h₁ := h₁.right x₁ x₂ h₆ + · replace h₁ := h₁.right x₁ x₂ hc₁ simp only [EvaluatesTo, evaluate, ih₁, ih₂, apply₂, hasTag, Except.bind_ok, Except.ok.injEq, Value.prim.injEq, Prim.bool.injEq, false_or, reduceCtorEq] at h₁ 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₇ + · cases ht₂ end Cedar.Thm diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean index 16b93d05f..ed4c8f314 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean @@ -26,6 +26,55 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation +theorem type_of_call_args_inversion {xs : List Expr} {txs : List TypedExpr} {c : Capabilities} {env : Environment} + (htxs : (xs.mapM₁ λ x => justType (typeOf x.val c env)) = Except.ok txs) : + List.Forall₂ (λ xᵢ txᵢ => ∃ cᵢ, typeOf xᵢ c env = Except.ok (txᵢ, cᵢ)) xs txs +:= +match xs with +| [] => by + replace htxs : txs = [] := + by simpa [List.mapM₁, pure, Except.pure] using htxs + subst htxs + constructor +| x :: xs => by + simp only [List.mapM₁, List.attach, List.attachWith, List.pmap_cons, List.mapM_cons, bind_pure_comp] at htxs + cases htx : justType (typeOf x c env) <;> simp only [htx, Except.bind_err, reduceCtorEq] at htxs + simp only [justType, Except.map] at htx + split at htx <;> simp only [reduceCtorEq, Except.ok.injEq] at htx + subst htx + simp only [List.mapM_pmap_subtype (fun x => justType (typeOf x c env))] at htxs + cases htxs' : List.mapM (fun x => justType (typeOf x c env)) xs <;> + simp only [htxs', Except.map_error, Except.map_ok, Except.bind_ok, reduceCtorEq, Except.ok.injEq] at htxs + subst txs + constructor + · rename_i r _ _ + exists r.snd + · have ih := @type_of_call_args_inversion xs + simp [ih, htxs', List.mapM₁] + +theorem type_of_call_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (htx : typeOf (Expr.call xfn xs) c env = Except.ok (tx, c')) : + ∃ txs, + (∃ ty, tx = .call xfn txs ty) ∧ + List.Forall₂ (λ xᵢ txᵢ => ∃ cᵢ, typeOf xᵢ c env = .ok (txᵢ, cᵢ)) xs txs +:= by + simp only [typeOf, typeOfCall] at htx + cases htx₁ : xs.mapM₁ fun x => justType (typeOf x.val c env) <;> simp only [htx₁, Except.bind_err, Except.bind_ok, reduceCtorEq] at htx + rename_i txs + exists txs + and_intros + · split at htx <;> + (first + | contradiction + | cases htx₁ : typeOfConstructor Ext.Decimal.decimal xs (CedarType.ext ExtType.decimal) <;> simp only [htx₁] at htx + | cases htx₁ : typeOfConstructor Ext.IPAddr.ip xs (CedarType.ext ExtType.ipAddr) <;> simp only [htx₁] at htx + | cases htx₁ : typeOfConstructor Cedar.Spec.Ext.Datetime.parse xs (.ext .datetime) <;> simp only [htx₁] at htx + | cases htx₁ : typeOfConstructor Cedar.Spec.Ext.Datetime.Duration.parse xs (.ext .duration) <;> simp only [htx₁] at htx + | skip) <;> + simp only [ok, err, Except.ok.injEq, Prod.mk.injEq, Except.bind_ok, Except.bind_err, reduceCtorEq] at htx <;> + simp [←htx] + · exact type_of_call_args_inversion htx₁ + theorem type_of_call_decimal_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr} (h₁ : typeOf (Expr.call .decimal xs) c env = Except.ok (ty, c')) : ty.typeOf = .ext .decimal ∧ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean index 70c2a1b84..4f36ee124 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/GetAttr.lean @@ -37,25 +37,27 @@ theorem getAttrInRecord_has_empty_capabilities {x₁ : Expr} {a : Attr} {c₁ c simp [ok, err] at h₁ <;> simp [h₁] -theorem type_of_getAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.getAttr x₁ a) c₁ env = Except.ok (ty, c₂)) : +theorem type_of_getAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.getAttr x₁ a) c₁ env = Except.ok (tx, c₂)) : c₂ = ∅ ∧ - ∃ c₁', - (∃ ety, (typeOf x₁ c₁ env).typeOf = Except.ok (.entity ety, c₁')) ∨ - (∃ rty, (typeOf x₁ c₁ env).typeOf = Except.ok (.record rty, c₁')) + ∃ tx₁ c₁', + typeOf x₁ c₁ env = .ok (tx₁, c₁') ∧ + tx = .getAttr tx₁ a tx.typeOf ∧ + ((∃ ety, tx₁.typeOf = .entity ety) ∨ + (∃ rty, tx₁.typeOf = .record rty)) := by simp [typeOf] at h₁ cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁ case ok res => have ⟨ty₁, c₁'⟩ := res simp [typeOfGetAttr, bind, Except.bind] at h₁ - simp only [ResultType.typeOf, Except.map] split at h₁ <;> try contradiction · simp [List.empty_eq, Except.ok.injEq, Prod.mk.injEq, false_and, exists_const, CedarType.record.injEq, exists_and_right, exists_eq', true_and, false_or, and_true, reduceCtorEq] split at h₁ <;> simp [ok] at h₁ rename_i heq₁ _ _ heq₂ simp [heq₁, ←h₁] + simp [TypedExpr.typeOf] apply getAttrInRecord_has_empty_capabilities heq₂ · simp only [List.empty_eq, Except.ok.injEq, Prod.mk.injEq, CedarType.entity.injEq, exists_and_right, exists_eq', true_and, false_and, exists_const, or_false, and_true, reduceCtorEq] @@ -63,6 +65,7 @@ theorem type_of_getAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabili split at h₁ <;> simp [ok] at h₁ rename_i heq₁ _ _ _ _ _ heq₃ simp [heq₁, ←h₁] + simp [TypedExpr.typeOf] apply getAttrInRecord_has_empty_capabilities heq₃ theorem type_of_getAttr_is_sound_for_records {x₁ : Expr} {a : Attr} {c₁ c₁' : Capabilities} {env : Environment} {rty : RecordType} {request : Request} {entities : Entities} {v₁ : Value} @@ -200,20 +203,20 @@ theorem type_of_getAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilit GuardedCapabilitiesInvariant (Expr.getAttr x₁ a) c₂ request entities ∧ ∃ v, EvaluatesTo (Expr.getAttr x₁ a) request entities v ∧ InstanceOfType v ty.typeOf := by - have ⟨h₅, c₁', h₄⟩ := type_of_getAttr_inversion h₃ + have ⟨h₅, tx, c₁', h₄, h₆, h₇⟩ := type_of_getAttr_inversion h₃ subst h₅ apply And.intro empty_guarded_capabilities_invariant - rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ <;> - split_type_of h₄ <;> rename_i h₄ hl₄ hr₄ <;> - have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ <;> + rcases h₇ with ⟨ety, h₇⟩ | ⟨rty, h₇⟩ <;> + have ⟨_, v₁, h₆, h₈⟩ := ih h₁ h₂ h₄ <;> simp [EvaluatesTo] at h₆ <;> simp [EvaluatesTo, evaluate] <;> - rw [hl₄] at h₇ <;> rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆] <;> try exact type_is_inhabited ty.typeOf - · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.entity ety, c₁') := by simp [h₄, hl₄, ResultType.typeOf, Except.map]; exact hr₄ - exact type_of_getAttr_is_sound_for_entities h₁ h₂ h₃ h₈ h₆ h₇ - · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.record rty, c₁') := by simp [h₄, hl₄, ResultType.typeOf, Except.map]; exact hr₄ - exact type_of_getAttr_is_sound_for_records h₁ h₃ h₈ h₆ h₇ + · have h₉ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.entity ety, c₁') := by simp [h₄, ResultType.typeOf, Except.map]; exact h₇ + rw [h₇] at h₈ + exact type_of_getAttr_is_sound_for_entities h₁ h₂ h₃ h₉ h₆ h₈ + · have h₉ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.record rty, c₁') := by simp [h₄, ResultType.typeOf, Except.map]; exact h₇ + rw [h₇] at h₈ + exact type_of_getAttr_is_sound_for_records h₁ h₃ h₉ h₆ h₈ end Cedar.Thm diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean index e2bbfbb1d..7f7969aff 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/HasAttr.lean @@ -26,30 +26,48 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation -theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {e' : TypedExpr} - (h₁ : typeOf (Expr.hasAttr x₁ a) c₁ env = Except.ok (e', c₂)) : +theorem hasAttrInRecord_has_empty_or_singleton_capabilities {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {rty : RecordType} {ty₁ : CedarType} : + hasAttrInRecord rty x₁ a c₁ b = Except.ok (ty₁, c₂) → + c₂ = ∅ ∨ c₂ = Capabilities.singleton x₁ (.attr a) +:= by + intro h₁ + simp [hasAttrInRecord] at h₁ + split at h₁ <;> + (try split at h₁) <;> + simp [ok, err] at h₁ <;> + simp [h₁] + +theorem type_of_hasAttr_inversion {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.hasAttr x₁ a) c₁ env = Except.ok (tx, c₂)) : (c₂ = ∅ ∨ c₂ = Capabilities.singleton x₁ (.attr a)) ∧ - ∃ c₁', - (∃ ety, (typeOf x₁ c₁ env).typeOf = Except.ok (.entity ety, c₁')) ∨ - (∃ rty, (typeOf x₁ c₁ env).typeOf = Except.ok (.record rty, c₁')) + ∃ tx₁ c₁', + typeOf x₁ c₁ env = .ok (tx₁, c₁') ∧ + tx = .hasAttr tx₁ a tx.typeOf ∧ + ((∃ ety, tx₁.typeOf = .entity ety) ∨ + (∃ rty, tx₁.typeOf = .record rty)) := by - simp [typeOf, typeOfHasAttr] at h₁ + simp [typeOf] at h₁ cases h₂ : typeOf x₁ c₁ env <;> simp [h₂] at h₁ case ok res => have ⟨ty₁, c₁'⟩ := res - simp only [ResultType.typeOf, Except.map] - simp at h₁ - split at h₁ - <;> simp [err, ok, hasAttrInRecord] at h₁ - <;> rename_i heq - <;> rw [heq] - <;> split at h₁ - <;> try split at h₁ - <;> try split at h₁ - all_goals { - simp [ok] at h₁ - try simp [h₁] - } + simp [typeOfHasAttr, bind, Except.bind] at h₁ + split at h₁ <;> try contradiction + · simp + split at h₁ <;> simp [ok] at h₁ + rename_i heq₁ _ _ heq₂ + simp [heq₁, ←h₁] + simp [TypedExpr.typeOf] + apply hasAttrInRecord_has_empty_or_singleton_capabilities heq₂ + · split at h₁ + · split at h₁ <;> simp [ok] at h₁ + rename_i heq₁ _ _ _ _ _ heq₃ + simp [heq₁, ←h₁] + simp [TypedExpr.typeOf] + apply hasAttrInRecord_has_empty_or_singleton_capabilities heq₃ + · split at h₁ <;> simp [ok, err] at h₁ + rename_i heq₁ _ _ heq₃ + simp [heq₁, ←h₁] + simp [TypedExpr.typeOf] theorem type_of_hasAttr_is_sound_for_records {x₁ : Expr} {a : Attr} {c₁ c₁' : Capabilities} {env : Environment} {rty : RecordType} {request : Request} {entities : Entities} {v₁ : Value} (h₁ : CapabilitiesInvariant c₁ request entities) @@ -172,7 +190,7 @@ theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilit GuardedCapabilitiesInvariant (Expr.hasAttr x₁ a) c₂ request entities ∧ ∃ v, EvaluatesTo (Expr.hasAttr x₁ a) request entities v ∧ InstanceOfType v ty.typeOf := by - have ⟨h₅, c₁', h₄⟩ := type_of_hasAttr_inversion h₃ + have ⟨h₅, ty₁, c₁', hty₁, hty, h₄⟩ := type_of_hasAttr_inversion h₃ apply And.intro case left => simp [GuardedCapabilitiesInvariant, CapabilitiesInvariant] @@ -185,17 +203,15 @@ theorem type_of_hasAttr_is_sound {x₁ : Expr} {a : Attr} {c₁ c₂ : Capabilit simp [EvaluatesTo, h₆] case right => rcases h₄ with ⟨ety, h₄⟩ | ⟨rty, h₄⟩ <;> - split_type_of h₄ <;> rename_i h₄ hl₄ hr₄ <;> - have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ h₄ <;> + have ⟨_, v₁, h₆, h₇⟩ := ih h₁ h₂ hty₁ <;> simp [EvaluatesTo] at h₆ <;> simp [EvaluatesTo, evaluate] <;> - rw [hl₄] at h₇ <;> + rw [h₄] at h₇ <;> rcases h₆ with h₆ | h₆ | h₆ | h₆ <;> simp [h₆] <;> try exact type_is_inhabited ty.typeOf - · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.entity ety, c₁') := by simp [h₄, hl₄, hr₄, ResultType.typeOf, Except.map] + · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.entity ety, c₁') := by simp [h₄, hty₁, ResultType.typeOf, Except.map] exact type_of_hasAttr_is_sound_for_entities h₁ h₂ h₃ h₈ h₆ h₇ - · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.record rty, c₁') := by simp [h₄, hl₄, hr₄, ResultType.typeOf, Except.map] + · have h₈ : (typeOf x₁ c₁ env).typeOf = Except.ok (CedarType.record rty, c₁') := by simp [h₄, hty₁, ResultType.typeOf, Except.map] exact type_of_hasAttr_is_sound_for_records h₁ h₃ h₈ h₆ h₇ - end Cedar.Thm diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/IfThenElse.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/IfThenElse.lean index 24e507e0d..deb9a52ed 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/IfThenElse.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/IfThenElse.lean @@ -25,42 +25,49 @@ namespace Cedar.Thm open Cedar.Spec open Cedar.Validation -theorem type_of_ite_inversion {x₁ x₂ x₃ : Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.ite x₁ x₂ x₃) c env = Except.ok (ty, c')) : - ∃ bty₁ c₁ ty₂ c₂ ty₃ c₃, - (typeOf x₁ c env).typeOf = .ok (.bool bty₁, c₁) ∧ +theorem type_of_ite_inversion {x₁ x₂ x₃ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.ite x₁ x₂ x₃) c env = Except.ok (tx, c')) : + ∃ tx₁ bty₁ c₁ tx₂ c₂ tx₃ c₃, + tx = TypedExpr.ite tx₁ tx₂ tx₃ tx.typeOf ∧ + typeOf x₁ c env = .ok (tx₁, c₁) ∧ + tx₁.typeOf = .bool bty₁ ∧ match bty₁ with | .ff => - typeOf x₃ c env = .ok (ty₃, c₃) ∧ ty = ty₃ ∧ c' = c₃ + typeOf x₃ c env = .ok (tx₃, c₃) ∧ + tx.typeOf = tx₃.typeOf ∧ c' = c₃ | .tt => - typeOf x₂ (c ∪ c₁) env = .ok (ty₂, c₂) ∧ - ty = ty₂ ∧ c' = c₁ ∪ c₂ + typeOf x₂ (c ∪ c₁) env = .ok (tx₂, c₂) ∧ + tx.typeOf = tx₂.typeOf ∧ c' = c₁ ∪ c₂ | .anyBool => - typeOf x₂ (c ∪ c₁) env = .ok (ty₂, c₂) ∧ - typeOf x₃ c env = .ok (ty₃, c₃) ∧ - (ty₂.typeOf ⊔ ty₃.typeOf) = (.some ty.typeOf) ∧ c' = (c₁ ∪ c₂) ∩ c₃ + typeOf x₂ (c ∪ c₁) env = .ok (tx₂, c₂) ∧ + typeOf x₃ c env = .ok (tx₃, c₃) ∧ + (tx₂.typeOf ⊔ tx₃.typeOf) = (.some tx.typeOf) ∧ c' = (c₁ ∪ c₂) ∩ c₃ := by simp [typeOf] at h₁ cases h₂ : typeOf x₁ c env <;> simp [h₂, typeOfIf] at * - simp [ResultType.typeOf, Except.map] rename_i res₁ split at h₁ <;> try { simp [ok, err] at h₁ } <;> rename_i c₁ hr₁ case ok.h_1 => - exists BoolType.tt, res₁.snd + exists res₁.fst, BoolType.tt, res₁.snd simp [hr₁] cases h₃ : typeOf x₂ (c ∪ res₁.snd) env <;> simp [h₃] at h₁ rename_i res₂ ; simp [ok] at h₁ have ⟨ht₂, hc₂⟩ := h₁ - exists res₂.fst, res₂.snd subst ht₂ hc₂ - simp [h₃, ←hr₁] + simp [h₃, ←hr₁, TypedExpr.typeOf] + exists res₂.snd case ok.h_2 => - exists BoolType.ff, res₁.snd + exists res₁.fst, BoolType.ff, res₁.snd simp [hr₁] - exact h₁ + cases h₃ : typeOf x₃ c env <;> simp [h₃] at h₁ + rename_i res₃ + simp [ok] at h₁ + replace ⟨hl₁, hr₁⟩ := h₁ + subst hl₁ hr₁ + exists res₃.fst, res₃.fst case ok.h_3 => - exists BoolType.anyBool, res₁.snd + exists res₁.fst, BoolType.anyBool, res₁.snd simp [hr₁] cases h₃ : typeOf x₂ (c ∪ res₁.snd) env <;> simp [h₃] at h₁ cases h₄ : typeOf x₃ c env <;> simp [h₄] at h₁ @@ -70,7 +77,9 @@ theorem type_of_ite_inversion {x₁ x₂ x₃ : Expr} {c c' : Capabilities} {env subst ht hc exists res₂.fst, res₂.snd simp only [←hr₁, h₃, Except.ok.injEq, true_and] - exists res₃.fst, res₃.snd + exists res₃.fst + simp [TypedExpr.typeOf] + exists res₃.snd theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) @@ -82,22 +91,21 @@ theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} GuardedCapabilitiesInvariant (Expr.ite x₁ x₂ x₃) c₂ request entities ∧ ∃ v, EvaluatesTo (Expr.ite x₁ x₂ x₃) request entities v ∧ InstanceOfType v ty.typeOf := by - have ⟨bty₁, rc₁, ty₂, rc₂, ty₃, rc₃, h₄, h₅⟩ := type_of_ite_inversion h₃ - split_type_of h₄ ; rename_i h₄ hl₄ hr₄ - specialize ih₁ h₁ h₂ h₄ + have ⟨ty₁, bty₁, rc₁, ty₂, rc₂, ty₃, rc₃, h₄, h₅, h₆, h₇⟩ := type_of_ite_inversion h₃ + specialize ih₁ h₁ h₂ h₅ have ⟨ih₁₁, v₁, ih₁₂, ih₁₃⟩ := ih₁ - simp [hl₄] at ih₁₃ + simp [h₆] at ih₁₃ have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃ subst hb₁ - cases bty₁ <;> simp at h₅ + cases bty₁ <;> simp at h₇ case anyBool => - have ⟨h₅, h₆, ht, hc⟩ := h₅ + have ⟨h₈, ht, hty, hc⟩ := h₇ cases b₁ case false => rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant] <;> try exact type_is_inhabited ty.typeOf - specialize ih₃ h₁ h₂ h₆ + specialize ih₃ h₁ h₂ ht have ⟨ih₃₁, v₃, ih₃₂, ih₃₃⟩ := ih₃ rcases ih₃₂ with ih₃₂ | ih₃₂ | ih₃₂ | ih₃₂ <;> simp [ih₃₂] <;> try exact type_is_inhabited ty.typeOf @@ -108,7 +116,7 @@ theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} apply capability_intersection_invariant simp [ih₃₁] case right => - apply instance_of_lub ht + apply instance_of_lub hty simp [ih₃₃] case true => rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> @@ -116,8 +124,7 @@ theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} try exact type_is_inhabited ty.typeOf simp [GuardedCapabilitiesInvariant, ih₁₂] at ih₁₁ have h₇ := capability_union_invariant h₁ ih₁₁ - subst rc₁ - specialize ih₂ h₇ h₂ h₅ + specialize ih₂ h₇ h₂ h₈ have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂ apply And.intro case left => @@ -130,10 +137,10 @@ theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} case right => rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;> simp [ih₂₂] <;> try exact type_is_inhabited ty.typeOf - apply instance_of_lub ht + apply instance_of_lub hty simp [ih₂₃] case tt => - have ⟨h₅, ht, hc⟩ := h₅ + replace ⟨h₇, ht, hc⟩ := h₇ rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant] <;> try exact type_is_inhabited ty.typeOf @@ -141,25 +148,26 @@ theorem type_of_ite_is_sound {x₁ x₂ x₃ : Expr} {c₁ c₂ : Capabilities} simp at hb₁ ; subst hb₁ ; simp only [ite_true] simp [GuardedCapabilitiesInvariant, ih₁₂] at ih₁₁ have h₆ := capability_union_invariant h₁ ih₁₁ - subst rc₁ - specialize ih₂ h₆ h₂ h₅ + specialize ih₂ h₆ h₂ h₇ have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂ rcases ih₂₂ with ih₂₂ | ih₂₂ | ih₂₂ | ih₂₂ <;> simp [ih₂₂] <;> try exact type_is_inhabited ty.typeOf - subst ht hc ; simp [ih₂₃] + subst hc + simp [ht, ih₂₃] intro h₇ ; subst h₇ simp [GuardedCapabilitiesInvariant, ih₂₂] at ih₂₁ exact capability_union_invariant ih₁₁ ih₂₁ case ff => - have ⟨h₅, ht, hc⟩ := h₅ + replace ⟨h₇, ht, hc⟩ := h₇ rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool, GuardedCapabilitiesInvariant] <;> try exact type_is_inhabited ty.typeOf have hb₁ := instance_of_ff_is_false ih₁₃ simp at hb₁ ; simp [hb₁] - specialize ih₃ h₁ h₂ h₅ + specialize ih₃ h₁ h₂ h₇ have ⟨ih₃₁, v₃, ih₃₂, ih₃₃⟩ := ih₃ - subst ht hc + subst hc + rw [ht] apply And.intro · simp [GuardedCapabilitiesInvariant] at ih₃₁ exact ih₃₁ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/LitVar.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/LitVar.lean index cbbb3a825..7ee5297fc 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/LitVar.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/LitVar.lean @@ -26,6 +26,15 @@ namespace Cedar.Thm open Cedar.Spec open Cedar.Validation +theorem type_of_lit_inversion + (h₁ : (typeOf (Expr.lit l) c₁ env) = Except.ok (tx, c₂)) : + ∃ ty, TypedExpr.lit l ty = tx +:= by + simp [typeOf, typeOfLit, ok, err] at h₁ + (split at h₁ <;> try split at h₁) <;> + try simp only [reduceCtorEq, Except.ok.injEq, Prod.mk.injEq] at h₁ <;> + simp [←h₁] + theorem type_of_lit_is_sound {l : Prim} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} (h₃ : (typeOf (Expr.lit l) c₁ env) = Except.ok (ty, c₂)) : GuardedCapabilitiesInvariant (Expr.lit l) c₂ request entities ∧ diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Or.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Or.lean index 7dae743fd..e60e73a1d 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Or.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Or.lean @@ -26,21 +26,24 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation -theorem type_of_or_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.or x₁ x₂) c env = Except.ok (ty, c')) : - ∃ bty₁ c₁, - (typeOf x₁ c env).typeOf = .ok (.bool bty₁, c₁) ∧ +theorem type_of_or_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.or x₁ x₂) c env = Except.ok (tx, c')) : + ∃ tx₁ bty₁ c₁, + typeOf x₁ c env = .ok (tx₁, c₁) ∧ + tx₁.typeOf = .bool bty₁ ∧ if bty₁ = BoolType.tt - then ty.typeOf = .bool BoolType.tt ∧ c' = ∅ - else ∃ bty₂ c₂, - (typeOf x₂ c env).typeOf = .ok (.bool bty₂, c₂) ∧ + then tx = tx₁ ∧ c' = ∅ + else ∃ bty tx₂ bty₂ c₂, + tx = (.or tx₁ tx₂ (.bool bty)) ∧ + typeOf x₂ c env = .ok (tx₂, c₂) ∧ + tx₂.typeOf = .bool bty₂ ∧ if bty₁ = BoolType.ff - then ty.typeOf = .bool bty₂ ∧ c' = c₂ + then bty = bty₂ ∧ c' = c₂ else if bty₂ = BoolType.tt - then ty.typeOf = .bool BoolType.tt ∧ c' = ∅ + then bty = BoolType.tt ∧ c' = ∅ else if bty₂ = BoolType.ff - then ty.typeOf = .bool BoolType.anyBool ∧ c' = c₁ - else ty.typeOf = .bool BoolType.anyBool ∧ c' = c₁ ∩ c₂ + then bty = BoolType.anyBool ∧ c' = c₁ + else bty = BoolType.anyBool ∧ c' = c₁ ∩ c₂ := by simp [typeOf] at h₁ cases h₂ : typeOf x₁ c env <;> simp [h₂] at * @@ -49,21 +52,23 @@ theorem type_of_or_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Env split at h₁ <;> simp [ok, err] at h₁ <;> rename_i hr₁ case ok.h_1 c₁ => - exists BoolType.tt, res₁.snd - simp [←h₁, hr₁, ResultType.typeOf, Except.map] + exists res₁.fst, BoolType.tt, res₁.snd + simp [←h₁, hr₁] case ok.h_2 c₁ => - cases h₃ : typeOf x₂ c env <;> simp [h₃] at * + cases h₃ : typeOf x₂ c env <;> simp [h₃] at h₁ rename_i res₂ split at h₁ <;> simp [ok, err] at h₁ rename_i bty₂ hr₂ have ⟨ht, hc⟩ := h₁ subst ht hc - exists BoolType.ff, res₁.snd - simp [hr₁, hr₂, ResultType.typeOf, Except.map] - simp [TypedExpr.typeOf] + exists res₁.fst, BoolType.ff, res₁.snd + simp only [hr₁, hr₂, true_and] + exists bty₂, res₂.fst + simp only [exists_eq_right_right', true_and] + exists bty₂, res₂.snd case ok.h_3 bty₁ hneq₁ hneq₂ => cases bty₁ <;> simp at hneq₁ hneq₂ - exists BoolType.anyBool, res₁.snd + exists res₁.fst, BoolType.anyBool, res₁.snd simp [hr₁] cases h₃ : typeOf x₂ c env <;> simp [h₃] at * rename_i res₂ @@ -71,13 +76,25 @@ theorem type_of_or_inversion {x₁ x₂ : Expr} {c c' : Capabilities} {env : Env rename_i hr₂ <;> have ⟨ht, hc⟩ := h₁ <;> subst ht hc <;> simp [hr₁, ResultType.typeOf, Except.map] case anyBool.ok.h_1 => + exists BoolType.tt, res₂.fst + simp only [hr₂, true_and] exists BoolType.tt, res₂.snd case anyBool.ok.h_2 => + exists BoolType.anyBool, res₂.fst + simp only [true_and] exists BoolType.ff, res₂.snd case anyBool.ok.h_3 bty₂ hneq₁ hneq₂ => + exists BoolType.anyBool, res₂.fst + simp exists bty₂, res₂.snd - simp [←hr₂, TypedExpr.typeOf] - cases bty₂ <;> simp at * + simp [←hr₂] + constructor + · intro heq + specialize hneq₁ heq + contradiction + · intro heq + specialize hneq₂ heq + contradiction theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) @@ -88,30 +105,30 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : GuardedCapabilitiesInvariant (Expr.or x₁ x₂) c₂ request entities ∧ ∃ v, EvaluatesTo (Expr.or x₁ x₂) request entities v ∧ InstanceOfType v ty.typeOf := by - have ⟨bty₁, rc₁, h₄, h₅⟩ := type_of_or_inversion h₃ - split_type_of h₄ ; rename_i h₄ hl₄ hr₄ + have ⟨tx₁, bty₁, rc₁, h₄, h₅, h₆⟩ := type_of_or_inversion h₃ specialize ih₁ h₁ h₂ h₄ have ⟨ih₁₁, v₁, ih₁₂, ih₁₃⟩ := ih₁ - rw [hl₄] at ih₁₃ + rw [h₅] at ih₁₃ have ⟨b₁, hb₁⟩ := instance_of_bool_is_bool ih₁₃ ; subst hb₁ - split at h₅ - case isTrue h₆ => - subst h₆ - have ⟨hty, hc⟩ := h₅ ; rw [hty] at * ; subst hc + split at h₆ + case isTrue h₇ => + subst h₇ + have ⟨hty, hc⟩ := h₆ ; rw [hty] at * ; subst hc apply And.intro empty_guarded_capabilities_invariant have h₇ := instance_of_tt_is_true ih₁₃ simp at h₇ ; subst h₇ simp [EvaluatesTo] at ih₁₂ + rw [h₅] + exists (.prim (.bool true)) rcases ih₁₂ with ih₁₂ | ih₁₂ | ih₁₂ | ih₁₂ <;> simp [EvaluatesTo, evaluate, Result.as, ih₁₂, Coe.coe, Value.asBool] <;> - try exact type_is_inhabited (CedarType.bool BoolType.tt) exact true_is_instance_of_tt case isFalse => - have ⟨bty₂, rc₂, h₅', h₇⟩ := h₅ - split_type_of h₅' ; rename_i h₅' hl₅ hr₅ - specialize ih₂ h₁ h₂ h₅' + have ⟨bty, tx₂, bty₂, rc₂, h₅', h₇, h₈, h₉⟩ := h₆ + subst ty + specialize ih₂ h₁ h₂ h₇ have ⟨ih₂₁, v₂, ih₂₂, ih₂₃⟩ := ih₂ - rw [hl₅] at ih₂₃ + rw [h₈] at ih₂₃ have ⟨b₂, hb₂⟩ := instance_of_bool_is_bool ih₂₃ subst hb₂ simp [EvaluatesTo] @@ -123,19 +140,21 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : case false.inr.inr.inr.inr.inr.inr => cases b₂ <;> simp [CoeT.coe, CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeTC.coe, Coe.coe] - case false h₆ _ _ => - cases bty₁ <;> simp at h₆ h₇ + case false h₉ => + cases bty₁ <;> simp at h₉ h₈ case anyBool => - cases bty₂ <;> simp at h₇ <;> - have ⟨h₇, _⟩ := h₇ <;> rw [h₇] at * <;> + cases bty₂ <;> simp at h₉ <;> + replace ⟨h₉, _⟩ := h₉ <;> rw [h₉] <;> try exact bool_is_instance_of_anyBool false exact ih₂₃ case ff => - rw [h₇.left] + rw [h₉.left] exact ih₂₃ - case true h₆ _ _ => - cases bty₁ <;> cases bty₂ <;> simp at h₆ h₇ <;> - have ⟨hty, hc⟩ := h₇ <;> simp [hty, hc] at * + case tt => + contradiction + case true h₉ => + cases bty₁ <;> cases bty₂ <;> simp at h₉ h₈ <;> + have ⟨hty, hc⟩ := h₉ <;> simp [hty, hc] at * case ff.ff => rcases ih₂₃ with ⟨_, _, ih₂₃⟩ simp [InstanceOfBoolType] at ih₂₃ @@ -150,12 +169,10 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : apply And.intro · simp [GuardedCapabilitiesInvariant, ih₂₂] at ih₂₁ apply capability_intersection_invariant - rw [←hr₅] simp [ih₂₁] · apply bool_is_instance_of_anyBool all_goals { simp [GuardedCapabilitiesInvariant, ih₂₂] at ih₂₁ - rw [←hr₅] simp [ih₂₁] first | apply true_is_instance_of_tt @@ -164,19 +181,17 @@ theorem type_of_or_is_sound {x₁ x₂ : Expr} {c₁ c₂ : Capabilities} {env : all_goals { simp [GuardedCapabilitiesInvariant] at ih₁₁ ih₂₁ simp [ih₁₂] at ih₁₁ ; simp [ih₂₂] at ih₂₁ - rename_i h₆ _ _ + rename_i h₁₀ rcases ih₁₃ with ⟨_, _, ih₁₃⟩ simp [InstanceOfBoolType] at ih₁₃ - cases bty₁ <;> simp at h₆ ih₁₃ h₇ - cases bty₂ <;> simp at h₇ <;> - have ⟨ht, hc⟩ := h₇ <;> simp [ht, hc] at * <;> - simp [true_is_instance_of_tt, bool_is_instance_of_anyBool] <;> + cases bty₁ <;> simp at h₁₀ ih₁₃ h₈ + cases bty₂ <;> simp at h₉ <;> + have ⟨ht, hc⟩ := h₉ <;> simp [ht, hc] at * <;> + simp [TypedExpr.typeOf, true_is_instance_of_tt, bool_is_instance_of_anyBool] <;> try { apply empty_capabilities_invariant } <;> - subst rc₁ rc₂ <;> try { assumption } apply capability_intersection_invariant simp [ih₁₁] } - end Cedar.Thm diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean index 178a665c9..f2bf76a64 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Record.lean @@ -28,22 +28,21 @@ open Cedar.Spec open Cedar.Validation def AttrValueHasAttrType (av : Attr × Value) (aqty : Attr × QualifiedType) : Prop := - av.fst = aqty.fst ∧ InstanceOfType av.snd (Qualified.getType aqty.snd) + av.fst = aqty.fst ∧ InstanceOfType av.snd aqty.snd.getType -def AttrExprHasAttrType (c : Capabilities) (env : Environment) (ax : Attr × Expr) (aqty : Attr × QualifiedType) : Prop := - ∃ ty' c', - aqty = (ax.fst, .required ty') ∧ - (typeOf ax.snd c env).typeOf = Except.ok (ty', c') +def AttrExprHasAttrType (c : Capabilities) (env : Environment) (ax : Attr × Expr) (atx : Attr × TypedExpr) : Prop := + ax.fst = atx.fst ∧ + ∃ c', (typeOf ax.snd c env) = Except.ok (atx.snd, c') -theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabilities} {env : Environment} {rty : List (Attr × TypedExpr)} - (h₁ : axs.mapM (λ x => (typeOf x.snd c env).map (λ (ty, _) => (x.fst, ty))) = Except.ok rty) : - List.Forall₂ (AttrExprHasAttrType c env) axs (List.map (fun x => (x.fst, Qualified.required x.snd.typeOf)) rty) +theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabilities} {env : Environment} {rtx : List (Attr × TypedExpr)} + (h₁ : axs.mapM (λ x => (typeOf x.snd c env).map (λ (ty, _) => (x.fst, ty))) = Except.ok rtx) : + List.Forall₂ (AttrExprHasAttrType c env) axs rtx := by cases axs case nil => simp [pure, Except.pure] at h₁ ; subst h₁ ; apply List.Forall₂.nil case cons hd tl => - cases rty + cases rtx case nil => simp [←List.mapM'_eq_mapM] at h₁ cases h₂ : Except.map (fun x => (hd.fst, x.fst)) (typeOf hd.snd c env) <;> simp [h₂] at h₁ @@ -62,8 +61,6 @@ theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabil rename_i _ r _ simp [AttrExprHasAttrType] exists r.snd - rename_i h₃ - simp [h₃, ResultType.typeOf, Except.map] } { apply type_of_record_inversion_forall @@ -73,24 +70,22 @@ theorem type_of_record_inversion_forall {axs : List (Attr × Expr)} {c : Capabil simp only [h₁] } -theorem type_of_record_inversion {axs : List (Attr × Expr)} {c c' : Capabilities} {env : Environment} {ty : TypedExpr} - (h₁ : typeOf (Expr.record axs) c env = Except.ok (ty, c')) : +theorem type_of_record_inversion {axs : List (Attr × Expr)} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.record axs) c env = Except.ok (tx, c')) : c' = ∅ ∧ - ∃ (rty : List (Attr × QualifiedType)), - ty.typeOf = .record (Map.make rty) ∧ - List.Forall₂ (AttrExprHasAttrType c env) axs rty + ∃ (atxs : List (Attr × TypedExpr)), + tx = .record atxs (.record (Map.make (atxs.map λ (a, tx) => (a, .required tx.typeOf)))) ∧ + List.Forall₂ (AttrExprHasAttrType c env) axs atxs := by simp [typeOf, ok] at h₁ cases h₂ : axs.mapM₂ fun x => Except.map (fun x_1 => (x.1.fst, x_1.fst)) (typeOf x.1.snd c env) <;> simp [h₂] at h₁ rename_i rty simp [h₁] - exists (List.map (fun x => (x.fst, Qualified.required x.snd.typeOf)) rty) ; simp [←h₁] - constructor - case left => simp [TypedExpr.typeOf] - case right => - simp [List.mapM₂, List.attach₂] at h₂ - simp [List.mapM_pmap_subtype (fun (x : Attr × Expr) => Except.map (fun x₁ : (TypedExpr × Capabilities) => (x.fst, x₁.fst)) (typeOf x.snd c env))] at h₂ - exact type_of_record_inversion_forall h₂ + exists rty + simp [←h₁] + simp [List.mapM₂, List.attach₂] at h₂ + simp [List.mapM_pmap_subtype (fun (x : Attr × Expr) => Except.map (fun x₁ : (TypedExpr × Capabilities) => (x.fst, x₁.fst)) (typeOf x.snd c env))] at h₂ + exact type_of_record_inversion_forall h₂ theorem mk_vals_instance_of_mk_types₁ {a : Attr} {avs : List (Attr × Value)} {rty : List (Attr × QualifiedType)} (h₁ : List.Forall₂ AttrValueHasAttrType avs rty) @@ -110,13 +105,13 @@ theorem mk_vals_instance_of_mk_types₁ {a : Attr} {avs : List (Attr × Value)} simp [Map.contains, Map.find?, Map.kvs, h₆] at h₇ exact h₇ -theorem mk_vals_instance_of_mk_types₂ {a : Attr} {v : Value} {qty : QualifiedType} {avs : List (Attr × Value)} {rty : List (Attr × QualifiedType)} - (h₁ : List.Forall₂ AttrValueHasAttrType avs rty) +theorem mk_vals_instance_of_mk_types₂ {a : Attr} {v : Value} {qty : QualifiedType} {avs : List (Attr × Value)} {rtx : List (Attr × QualifiedType)} + (h₁ : List.Forall₂ AttrValueHasAttrType avs rtx) (h₂ : Map.find? (Map.mk avs) a = some v) - (h₃ : Map.find? (Map.mk rty) a = some qty) : + (h₃ : (Map.mk rtx).find? a = some qty) : InstanceOfType v (Qualified.getType qty) := by - cases avs <;> cases rty <;> cases h₁ + cases avs <;> cases rtx <;> cases h₁ case nil => simp [Map.find?, List.find?] at h₂ case cons ahd atl rhd rtl h₄ h₅ => @@ -125,27 +120,27 @@ theorem mk_vals_instance_of_mk_types₂ {a : Attr} {v : Value} {qty : QualifiedT have ⟨hl₄, hr₄⟩ := h₄ ; simp [hl₄] at * cases h₆ : rhd.fst == a <;> simp [h₆] at h₂ h₃ case true => - subst h₂ h₃ + rw [←h₂, ←h₃] exact hr₄ case false => apply @mk_vals_instance_of_mk_types₂ a v qty atl rtl h₅ <;> simp [Map.find?, Map.kvs, h₂, h₃] -theorem mk_vals_instance_of_mk_types₃ {a : Attr} {qty : QualifiedType} {avs : List (Attr × Value)} {rty : List (Attr × QualifiedType)} - (h₁ : List.Forall₂ AttrValueHasAttrType avs rty) - (h₂ : Map.find? (Map.mk rty) a = some qty) : +theorem mk_vals_instance_of_mk_types₃ {a : Attr} {qty : QualifiedType} {avs : List (Attr × Value)} {rtx : List (Attr × QualifiedType)} + (h₁ : List.Forall₂ AttrValueHasAttrType avs rtx) + (h₂ : (Map.mk rtx).find? a = some qty) : Map.contains (Map.mk avs) a = true := by - cases avs <;> cases rty <;> cases h₁ + cases avs <;> cases rtx <;> cases h₁ case nil => simp [Map.find?, List.find?] at h₂ case cons ahd atl rhd rtl h₄ h₅ => simp [Map.contains, Map.find?, List.find?] simp [Map.find?, List.find?] at h₂ simp [AttrValueHasAttrType] at h₄ - have ⟨h₄, _⟩ := h₄ ; simp [h₄] at * - cases h₆ : rhd.fst == a <;> simp [h₆] at * - cases h₇ : List.find? (fun x => x.fst == a) rtl <;> simp [h₇] at h₂ + have ⟨h₄, _⟩ := h₄ ; simp [h₄] + cases h₆ : rhd.fst == a <;> simp [h₆] at h₂ ⊢ + cases h₇ : rtl.find? λ (a', _) => a' == a <;> simp [h₇] at h₂ have h₈ := @mk_vals_instance_of_mk_types₃ a qty atl rtl h₅ simp [Map.find?, List.find?, Map.kvs, h₇, h₂, Map.contains] at h₈ exact h₈ @@ -165,39 +160,73 @@ theorem mk_vals_instance_of_mk_types {avs : List (Attr × Value)} {rty : List (A intro a qty h₂ _ exact mk_vals_instance_of_mk_types₃ h₁ h₂ -theorem head_of_vals_instance_of_head_of_types {xhd : Attr × Expr} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rhd : Attr × QualifiedType} {vhd : Attr × Value} +theorem find_mk_xs_find_mk_txs {axs : List (Attr × Expr)} {atxs : List (Attr × TypedExpr)} + (h₁ : List.Forall₂ (AttrExprHasAttrType c env) axs atxs) + (h₂ : (Map.mk axs).find? a = some x) : + ∃ tx c', (Map.mk atxs).find? a = some tx ∧ typeOf x c env = .ok (tx, c') +:= by + cases axs <;> cases atxs <;> cases h₁ + case nil => + simp [Map.find?, List.find?] at h₂ + case cons axh axt atxh athl h₄ h₅ => + simp [Map.contains, Map.find?, List.find?] + simp [Map.find?, List.find?] at h₂ + simp [AttrExprHasAttrType] at h₄ + replace ⟨h₄, _, h₆⟩ := h₄ ; rw [←h₄] + cases h₇ : axh.fst == a <;> simp [h₇] at h₂ ⊢ + · cases h₈ : axt.find? λ (a', _) => a' == a <;> simp [h₈] at h₂ + subst h₂ + rename_i ax + have h₉ := @find_mk_xs_find_mk_txs c env a ax.snd axt athl h₅ + simp [h₈, Map.find?, List.find?, Map.kvs, Map.contains] at h₉ + exact h₉ + · subst h₂ + simp [h₆] + +theorem find_make_xs_find_make_txs {axs : List (Attr × Expr)} {atxs : List (Attr × TypedExpr)} + (h₁ : List.Forall₂ (AttrExprHasAttrType c env) axs atxs) + (h₂ : (Map.make axs).find? a = some x) : + ∃ tx c', (Map.make atxs).find? a = some tx ∧ typeOf x c env = .ok (tx, c') +:= by + apply @find_mk_xs_find_mk_txs _ _ _ _ (List.canonicalize Prod.fst axs) + · let p := fun (x : Expr) (tx : TypedExpr) => + ∃ c', (typeOf x c env) = Except.ok (tx, c') + have h₆ := List.canonicalize_preserves_forallᵥ p axs atxs + simp [p, List.Forallᵥ] at h₆ + apply h₆ h₁ + · simp only [Map.make] at h₂ + exact h₂ + +theorem head_of_vals_instance_of_head_of_types {xhd : Attr × Expr} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rhd : Attr × TypedExpr} {vhd : Attr × Value} (h₁ : TypeOfIsSound xhd.snd) (h₂ : CapabilitiesInvariant c₁ request entities) (h₃ : RequestAndEntitiesMatchEnvironment env request entities) (h₄ : AttrExprHasAttrType c₁ env xhd rhd) (h₅ : bindAttr xhd.fst (evaluate xhd.snd request entities) = Except.ok vhd) : - AttrValueHasAttrType vhd rhd + AttrValueHasAttrType vhd (rhd.fst, .required rhd.snd.typeOf) := by simp [TypeOfIsSound] at h₁ - have ⟨ty', c', h₄, h₆⟩ := h₄ ; subst h₄ - split_type_of h₆ ; rename_i h₆ hl₆ hr₆ + replace ⟨h₄, _, h₆⟩ := h₄ ; rw [←h₄] specialize h₁ h₂ h₃ h₆ have ⟨_, v, h₁, h₇⟩ := h₁ simp [bindAttr] at h₅ cases h₈ : evaluate xhd.snd request entities <;> simp [h₈] at h₅ simp [EvaluatesTo, h₈] at h₁ ; subst h₁ h₅ - simp only [true_and, AttrValueHasAttrType, Qualified.getType, h₇, hl₆] - rw [←hl₆] - exact h₇ + simp [AttrValueHasAttrType, Qualified.getType, h₇, h₆] -theorem vals_instance_of_types {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rty : List (Attr × QualifiedType)} {avs : List (Attr × Value)} +theorem vals_instance_of_types {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rtx : List (Attr × TypedExpr)} {avs : List (Attr × Value)} (ih : ∀ (axᵢ : Attr × Expr), axᵢ ∈ axs → TypeOfIsSound axᵢ.snd) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rty) + (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rtx) (h₄ : (axs.mapM fun x => bindAttr x.fst (evaluate x.snd request entities)) = Except.ok avs) : - List.Forall₂ AttrValueHasAttrType avs rty + List.Forall₂ AttrValueHasAttrType avs (rtx.map λ (a, tx) => (a, .required tx.typeOf)) := by cases h₃ case nil => simp [←List.mapM'_eq_mapM, pure, Except.pure] at h₄ subst h₄ - simp only [List.Forall₂.nil] + simp [List.map_nil] case cons xhd rhd xtl rtl h₅ h₆ => simp [List.mapM'_eq_mapM, pure, Except.pure] at h₄ cases h₇ : bindAttr xhd.fst (evaluate xhd.snd request entities) <;> simp [h₇] at h₄ @@ -214,26 +243,26 @@ theorem vals_instance_of_types {axs : List (Attr × Expr)} {c₁ : Capabilities} intro ax h₉ ; apply ih ; simp [h₉] } -theorem type_of_record_is_sound_ok {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rty : List (Attr × QualifiedType)} {avs : List (Attr × Value)} +theorem type_of_record_is_sound_ok {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rtx : List (Attr × TypedExpr)} {avs : List (Attr × Value)} (ih : ∀ (axᵢ : Attr × Expr), axᵢ ∈ axs → TypeOfIsSound axᵢ.snd) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rty) + (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rtx) (h₄ : (axs.mapM fun x => bindAttr x.fst (evaluate x.snd request entities)) = Except.ok avs) : - InstanceOfType (Value.record (Map.make avs)) (CedarType.record (Map.make rty)) + InstanceOfType (Value.record (Map.make avs)) (CedarType.record (Map.make (rtx.map λ (a, tx) => (a, .required tx.typeOf)))) := by apply mk_vals_instance_of_mk_types let p := fun (v : Value) (qty : QualifiedType) => InstanceOfType v qty.getType have h₅ := vals_instance_of_types ih h₁ h₂ h₃ h₄ - have h₆ := List.canonicalize_preserves_forallᵥ p avs rty + have h₆ := List.canonicalize_preserves_forallᵥ p avs (rtx.map λ (a, tx) => (a, .required tx.typeOf)) simp [List.Forallᵥ] at h₆ exact h₆ h₅ -theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rty : List (Attr × QualifiedType)} {err : Error} +theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabilities} {env : Environment} {request : Request} {entities : Entities} {rtx : List (Attr × TypedExpr)} {err : Error} (ih : ∀ (axᵢ : Attr × Expr), axᵢ ∈ axs → TypeOfIsSound axᵢ.snd) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rty) + (h₃ : List.Forall₂ (AttrExprHasAttrType c₁ env) axs rtx) (h₄ : (axs.mapM fun x => bindAttr x.fst (evaluate x.snd request entities)) = Except.error err) : err = Error.entityDoesNotExist ∨ err = Error.extensionError ∨ err = Error.arithBoundsError := by @@ -251,8 +280,7 @@ theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabili subst h₄ h₅ specialize ih hd simp only [List.mem_cons, true_or, TypeOfIsSound, forall_const] at ih - have ⟨ty', c', _, hh₃⟩ := hh₃ - split_type_of hh₃ ; rename_i hh₃ hhl₃ hhr₃ + replace ⟨h₄, c', hh₃⟩ := hh₃ specialize ih h₁ h₂ hh₃ have ⟨_, v, ih, _⟩ := ih simp [EvaluatesTo, h₆] at ih @@ -267,16 +295,16 @@ theorem type_of_record_is_sound_err {axs : List (Attr × Expr)} {c₁ : Capabili (by simp [List.mapM₂, List.attach₂, List.mapM_pmap_subtype, h₅]) -theorem type_of_record_is_sound {axs : List (Attr × Expr)} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} +theorem type_of_record_is_sound {axs : List (Attr × Expr)} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : typeOf (Expr.record axs) c₁ env = Except.ok (ty, c₂)) + (h₃ : typeOf (Expr.record axs) c₁ env = Except.ok (tx, c₂)) (ih : ∀ (axᵢ : Attr × Expr), axᵢ ∈ axs → TypeOfIsSound axᵢ.snd) : GuardedCapabilitiesInvariant (Expr.record axs) c₂ request entities ∧ - ∃ v, EvaluatesTo (Expr.record axs) request entities v ∧ InstanceOfType v ty.typeOf + ∃ v, EvaluatesTo (Expr.record axs) request entities v ∧ InstanceOfType v tx.typeOf := by - have ⟨h₆, rty, h₅, h₄⟩ := type_of_record_inversion h₃ - subst h₆ ; rw [h₅] + have ⟨h₆, rty, h₄, h₅⟩ := type_of_record_inversion h₃ + subst h₆ h₄ apply And.intro empty_guarded_capabilities_invariant simp only [EvaluatesTo, evaluate] simp only [do_ok, do_error] @@ -285,9 +313,11 @@ theorem type_of_record_is_sound {axs : List (Attr × Expr)} {c₁ c₂ : Capabil rw [List.mapM_pmap_subtype f] cases h₅ : (axs.mapM f) <;> simp [h₅] case error err => + rename_i h₄ simp [type_is_inhabited] exact type_of_record_is_sound_err ih h₁ h₂ h₄ h₅ case ok avs => + rename_i h₄ exact type_of_record_is_sound_ok ih h₁ h₂ h₄ h₅ end Cedar.Thm diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/Set.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/Set.lean index 4dba8458c..75fa602da 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/Set.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/Set.lean @@ -113,15 +113,16 @@ theorem type_of_set_tail subst h₆ exists ty' -theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {sty : TypedExpr} - (h₁ : typeOf (Expr.set xs) c env = Except.ok (sty, c')) : +theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.set xs) c env = Except.ok (tx, c')) : c' = ∅ ∧ - ∃ ty, - sty.typeOf = .set ty ∧ - ∀ xᵢ, xᵢ ∈ xs → - ∃ tyᵢ cᵢ, - (typeOf xᵢ c env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ - (tyᵢ ⊔ ty) = .some ty + ∃ txs ty, + tx = (.set txs (.set ty)) ∧ + ∀ xᵢ ∈ xs, + ∃ txᵢ cᵢ, + txᵢ ∈ txs ∧ + typeOf xᵢ c env = Except.ok (txᵢ, cᵢ) ∧ + (txᵢ.typeOf ⊔ ty) = .some ty := by simp [typeOf] at h₁ cases h₂ : List.mapM₁ xs fun x => justType (typeOf x.val c env) <;> @@ -134,7 +135,7 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi have ⟨hl₁, hr₁⟩ := h₁ subst hl₁ hr₁ simp only [List.empty_eq, true_and] - exists ty + exists (hd :: tl), ty apply And.intro ; case left => simp [TypedExpr.typeOf] intro x h₄ cases h₄ @@ -150,19 +151,26 @@ theorem type_of_set_inversion {xs : List Expr} {c c' : Capabilities} {env : Envi simp only [justType, Except.map] at h₅ split at h₅ <;> simp at h₅ rename_i res h₇ - exists hdty.typeOf, res.snd - apply And.intro + exists hdty, res.snd + and_intros + · simp · simp [←h₅, h₇, ResultType.typeOf, Except.map] · exact foldlM_of_lub_is_LUB h₃ case tail xhd xtl h₄ => have ⟨ty', h₅, h₆⟩ := type_of_set_tail h₂ h₃ h₄ - have h₇ := @type_of_set_inversion xtl c ∅ env (.set tl ty'.set) - simp only [h₅, List.empty_eq, TypedExpr.typeOf, CedarType.set.injEq, exists_and_right, exists_eq_left', true_and, true_implies] at h₇ - specialize h₇ x h₄ - have ⟨tyᵢ, ⟨c₁, h₇⟩, h₈⟩ := h₇ - exists tyᵢ, c₁ - simp only [true_and, h₇] - exact lub_trans h₈ h₆ + have h₇ := @type_of_set_inversion xtl c ∅ env (.set tl ty'.set) h₅ + simp only [List.empty_eq, exists_and_right, true_and] at h₇ + replace ⟨ txs, ty, h₇, h₈ ⟩ := h₇ + simp only [TypedExpr.set.injEq, CedarType.set.injEq] at h₇ + replace ⟨ h₇, h₉ ⟩ := h₇ + subst h₇ h₉ + specialize h₈ x h₄ + replace ⟨txᵢ, c₁, htl, htxᵢ, hlub ⟩ := h₈ + exists txᵢ, c₁ + and_intros + · exact List.Mem.tail _ htl + · exact htxᵢ + · exact lub_trans hlub h₆ theorem list_is_sound_implies_tail_is_sound {hd : Expr} {tl : List Expr} (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → TypeOfIsSound xᵢ) : @@ -173,8 +181,8 @@ theorem list_is_sound_implies_tail_is_sound {hd : Expr} {tl : List Expr} simp [h₂] theorem list_is_typed_implies_tail_is_typed {hd : Expr} {tl : List Expr} {c₁ : Capabilities} {env : Environment} {ty : CedarType} - (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty) : - ∀ (xᵢ : Expr), xᵢ ∈ tl → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty + (h₁ : ∀ (xᵢ : Expr), xᵢ ∈ hd :: tl → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty) : + ∀ (xᵢ : Expr), xᵢ ∈ tl → ∃ txᵢ cᵢ, typeOf xᵢ c₁ env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty := by intro xᵢ h₂ apply h₁ @@ -184,7 +192,7 @@ theorem type_of_set_is_sound_err {xs : List Expr} {c₁ : Capabilities} {env : E (ih : ∀ (xᵢ : Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₄ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty) + (h₄ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty) (h₅ : (xs.mapM fun x => evaluate x request entities) = Except.error err) : err = Error.entityDoesNotExist ∨ err = Error.extensionError ∨ @@ -199,7 +207,6 @@ theorem type_of_set_is_sound_err {xs : List Expr} {c₁ : Capabilities} {env : E have h₄ := h₄ hd simp only [h₆, List.mem_cons, true_or, forall_const] at h₄ have ⟨tyᵢ, cᵢ, h₇, _⟩ := h₄ - split_type_of h₇ ; rename_i h₇ hl₇ _ have h₉ := ih hd ; simp [h₆, TypeOfIsSound] at h₉ specialize (h₉ h₁ h₂ h₇) ; have ⟨_, v, h₉⟩ := h₉ simp [EvaluatesTo] at h₉ @@ -222,7 +229,7 @@ theorem type_of_set_is_sound_ok { xs : List Expr } { c₁ : Capabilities } { env (ih : ∀ (xᵢ : Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ) (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) - (h₃ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ tyᵢ cᵢ, (typeOf xᵢ c₁ env).typeOf = Except.ok (tyᵢ, cᵢ) ∧ (tyᵢ ⊔ ty) = some ty) + (h₃ : ∀ (xᵢ : Expr), xᵢ ∈ xs → ∃ txᵢ cᵢ, (typeOf xᵢ c₁ env) = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty) (h₄ : (xs.mapM fun x => evaluate x request entities) = Except.ok vs) (h₅ : v ∈ vs): InstanceOfType v ty @@ -248,14 +255,12 @@ theorem type_of_set_is_sound_ok { xs : List Expr } { c₁ : Capabilities } { env have ⟨tyᵢ, cᵢ, h₃, h₆⟩ := h₃ specialize ih hd simp [TypeOfIsSound] at ih - split_type_of h₃ ; rename_i h₃ hl₃ _ specialize ih h₁ h₂ h₃ have ⟨_, v', ihl, ihr⟩ := ih simp [EvaluatesTo] at ihl rcases ihl with ihl | ihl | ihl | ihl <;> simp [ihl] at h₇ subst h₇ - rw [hl₃] at ihr exact instance_of_lub_left h₆ ihr case tail h₉ => apply @type_of_set_is_sound_ok @@ -274,11 +279,15 @@ theorem type_of_set_is_sound {xs : List Expr} {c₁ c₂ : Capabilities} {env : GuardedCapabilitiesInvariant (Expr.set xs) c₂ request entities ∧ ∃ v, EvaluatesTo (Expr.set xs) request entities v ∧ InstanceOfType v sty.typeOf := by - have ⟨h₆, ty, h₄, h₅⟩ := type_of_set_inversion h₃ + have ⟨h₆, txs, ty, h₄, h₅⟩ := type_of_set_inversion h₃ subst h₆ ; rw [h₄] apply And.intro empty_guarded_capabilities_invariant simp only [EvaluatesTo, evaluate, List.mapM₁, List.attach_def, List.mapM_pmap_subtype (evaluate · request entities)] + replace h₅ : ∀ xᵢ ∈ xs, ∃ tx c', typeOf xᵢ c₁ env = .ok (tx, c') ∧ (tx.typeOf ⊔ ty) = some ty := by + intros x h₁ + replace ⟨txᵢ, cᵢ, h₅⟩ := h₅ x h₁ + simp [h₅] cases h₆ : xs.mapM fun x => evaluate x request entities <;> simp [h₆] case error err => diff --git a/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean b/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean index e6c7311a1..37fc11789 100644 --- a/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean +++ b/cedar-lean/Cedar/Thm/Validation/Typechecker/UnaryApp.lean @@ -26,6 +26,32 @@ open Cedar.Data open Cedar.Spec open Cedar.Validation +theorem type_of_unary_inversion {op : UnaryOp} {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {tx : TypedExpr} + (h₁ : typeOf (Expr.unaryApp op x₁) c₁ env = Except.ok (tx, c₂)) : + c₂ = ∅ ∧ + ∃ tx₁ ty c₁', + tx = .unaryApp op tx₁ ty ∧ + typeOf x₁ c₁ env = Except.ok (tx₁, c₁') ∧ + match op with + | .not => ∃ bty, ty = .bool bty.not ∧ tx₁.typeOf = .bool bty + | .neg => tx₁.typeOf = .int ∧ ty = .int + | .isEmpty => ty = .bool .anyBool ∧ ∃ ty₀, tx₁.typeOf = .set ty₀ + | .like _ => ty = .bool .anyBool ∧ tx₁.typeOf = .string + | .is ety₀ => ∃ ety₁, ty = .bool (if ety₀ = ety₁ then .tt else .ff) ∧ tx₁.typeOf = .entity ety₁ +:= by + cases h₂ : typeOf x₁ c₁ env <;> simp only [h₂, typeOf, Except.bind_err, Except.bind_ok, reduceCtorEq] at h₁ + rename_i res ; have ⟨ty₁, c₁'⟩ := res + simp only [typeOfUnaryApp, Function.comp_apply] at h₁ + split at h₁ <;> try contradiction + all_goals { + simp only [ok, Except.ok.injEq, Prod.mk.injEq] at h₁ + replace ⟨ h₁, hc ⟩ := h₁ + simp only [hc, List.empty_eq, true_and] + exists ty₁ + rename_i hty₁ _ + simp [h₁, hty₁] + } + theorem type_of_not_inversion {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} (h₁ : typeOf (Expr.unaryApp .not x₁) c₁ env = Except.ok (ty, c₂)) : c₂ = ∅ ∧ @@ -49,7 +75,6 @@ theorem type_of_not_inversion {x₁ : Expr} {c₁ c₂ : Capabilities} {env : En simp only [TypedExpr.typeOf] simp [ResultType.typeOf, Except.map, h'₁] - theorem type_of_not_is_sound {x₁ : Expr} {c₁ c₂ : Capabilities} {env : Environment} {ty : TypedExpr} {request : Request} {entities : Entities} (h₁ : CapabilitiesInvariant c₁ request entities) (h₂ : RequestAndEntitiesMatchEnvironment env request entities) diff --git a/cedar-lean/Cedar/Validation/Typechecker.lean b/cedar-lean/Cedar/Validation/Typechecker.lean index 35bfedfde..6a1cfb48f 100644 --- a/cedar-lean/Cedar/Validation/Typechecker.lean +++ b/cedar-lean/Cedar/Validation/Typechecker.lean @@ -76,8 +76,10 @@ def typeOfIf (r₁ : TypedExpr × Capabilities) (r₂ r₃ : ResultType) : Resul match r₁.fst.typeOf with | .bool .tt => do let (ty₂, c₂) ← r₂ - ok ty₂ (c₁ ∪ c₂) - | .bool .ff => r₃ + ok (.ite r₁.fst ty₂ ty₂ ty₂.typeOf) (c₁ ∪ c₂) + | .bool .ff => do + let (ty₃, c₃) ← r₃ + ok (.ite r₁.fst ty₃ ty₃ ty₃.typeOf) c₃ | .bool .anyBool => do let (ty₂, c₂) ← r₂ let (ty₃, c₃) ← r₃