This file proves that typechecking of .ite expressions is sound.
theorem
Cedar.Thm.type_of_ite_inversion
{x₁ x₂ x₃ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (x₁.ite x₂ x₃) c env = Except.ok (tx, c'))
:
∃ (tx₁ : Validation.TypedExpr), ∃ (bty₁ : Validation.BoolType), ∃ (c₁ : Validation.Capabilities), ∃ (tx₂ : Validation.TypedExpr), ∃ (c₂ : Validation.Capabilities), ∃ (tx₃ : Validation.TypedExpr), ∃ (c₃ : Validation.Capabilities), tx = tx₁.ite tx₂ tx₃ tx.typeOf ∧ Validation.typeOf x₁ c env = Except.ok (tx₁, c₁) ∧ tx₁.typeOf = Validation.CedarType.bool bty₁ ∧ match bty₁, c₂, c₃ with
| Validation.BoolType.ff, c₂, c₃ =>
Validation.typeOf x₃ c env = Except.ok (tx₃, c₃) ∧ tx.typeOf = tx₃.typeOf ∧ c' = c₃
| Validation.BoolType.tt, c₂, c₃ =>
Validation.typeOf x₂ (c ∪ c₁) env = Except.ok (tx₂, c₂) ∧ tx.typeOf = tx₂.typeOf ∧ c' = c₁ ∪ c₂
| Validation.BoolType.anyBool, c₂, c₃ =>
Validation.typeOf x₂ (c ∪ c₁) env = Except.ok (tx₂, c₂) ∧ Validation.typeOf x₃ c env = Except.ok (tx₃, c₃) ∧ (tx₂.typeOf ⊔ tx₃.typeOf) = some tx.typeOf ∧ c' = (c₁ ∪ c₂) ∩ c₃
theorem
Cedar.Thm.type_of_ite_is_sound
{x₁ x₂ x₃ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (x₁.ite x₂ x₃) c₁ env = Except.ok (ty, c₂))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
(ih₃ : TypeOfIsSound x₃)
:
GuardedCapabilitiesInvariant (x₁.ite x₂ x₃) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.ite x₂ x₃) request entities v ∧ InstanceOfType env v ty.typeOf