This file proves that typechecking of .and expressions is sound.
theorem
Cedar.Thm.type_of_and_inversion
{x₁ x₂ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (x₁.and x₂) c env = Except.ok (tx, c'))
:
∃ (tx₁ : Validation.TypedExpr), ∃ (bty₁ : Validation.BoolType), ∃ (c₁ : Validation.Capabilities), Validation.typeOf x₁ c env = Except.ok (tx₁, c₁) ∧ tx₁.typeOf = Validation.CedarType.bool bty₁ ∧ if bty₁ = Validation.BoolType.ff then tx = tx₁ ∧ c' = ∅
else ∃ (bty : Validation.BoolType), ∃ (tx₂ : Validation.TypedExpr), ∃ (bty₂ : Validation.BoolType), ∃ (c₂ : Validation.Capabilities), tx = tx₁.and tx₂ (Validation.CedarType.bool bty) ∧ Validation.typeOf x₂ (c ∪ c₁) env = Except.ok (tx₂, c₂) ∧ tx₂.typeOf = Validation.CedarType.bool bty₂ ∧ if bty₂ = Validation.BoolType.ff then bty = Validation.BoolType.ff ∧ c' = ∅
else bty = Validation.lubBool bty₁ bty₂ ∧ c' = c₁ ∪ c₂
theorem
Cedar.Thm.type_of_and_is_sound
{x₁ x₂ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (x₁.and x₂) c₁ env = Except.ok (tx, c₂))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
GuardedCapabilitiesInvariant (x₁.and x₂) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.and x₂) request entities v ∧ InstanceOfType env v tx.typeOf