Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extend typechecker inversion lemma for type annotation #569

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Extend typechecker inversion lemma for type annotation #569

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
102 changes: 53 additions & 49 deletions cedar-lean/Cedar/Thm/Validation/Typechecker/And.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 *
Expand All @@ -46,50 +49,56 @@ 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 *
rename_i res₂
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₇
Expand All @@ -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₁₂ <;>
Expand All @@ -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₁₃]
Expand All @@ -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₁₃]

Expand Down
22 changes: 22 additions & 0 deletions cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it ok to combine the two existential quantifiers? Btw, there's no detailed specification of ty, like other inversion theorems. Is it intended?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I realized that these inversion theorems essentially say that typedOf produces well-typed expressions and subsequent proofs are "Well typed programs cannot go wrong." I'm not sure if we can complete the TPE soundness proof using this inversion theorem. That being said, we can always expand the theorem later.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it ok to combine the two existential quantifiers?

I don't see why not

Btw, there's no detailed specification of ty

I don't actually care about ty for my proofs, so this is good enough. The inversion lemma for the specific binary operators do specify ty, but I wanted one inversion lemma for all binary operators to make my proofs simpler. We could extend this lemma to specify the types of tx tx\1 and tx\2 in a match on op\2. Then other inversion lemma could be done in terms of this one, but I didn't need to go that far.

I realized that these inversion theorems essentially say that typedOf produces well-typed expressions

Yeah, there's probably some overlap here. I expect that TPE will need something stronger than what I needed for levels, but we'll probably be able to end up with both proof using the same inversion theorems.

:= 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)
Expand Down
60 changes: 31 additions & 29 deletions cedar-lean/Cedar/Thm/Validation/Typechecker/BinaryApp/GetTag.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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₁
Expand All @@ -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₁ <;>
Expand All @@ -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']
Expand All @@ -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
49 changes: 49 additions & 0 deletions cedar-lean/Cedar/Thm/Validation/Typechecker/Call.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 ∧
Expand Down
Loading