This file proves that typechecking of .or expressions is sound.
theorem
Cedar.Thm.type_of_or_inversion
{x₁ x₂ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (x₁.or 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.tt then tx = tx₁ ∧ c' = ∅
else ∃ (bty : Validation.BoolType), ∃ (tx₂ : Validation.TypedExpr), ∃ (bty₂ : Validation.BoolType), ∃ (c₂ : Validation.Capabilities), tx = tx₁.or tx₂ (Validation.CedarType.bool bty) ∧ Validation.typeOf x₂ c env = Except.ok (tx₂, c₂) ∧ tx₂.typeOf = Validation.CedarType.bool bty₂ ∧ if bty₁ = Validation.BoolType.ff then bty = bty₂ ∧ c' = c₂
else if bty₂ = Validation.BoolType.tt then bty = Validation.BoolType.tt ∧ c' = ∅
else if bty₂ = Validation.BoolType.ff then bty = Validation.BoolType.anyBool ∧ c' = c₁
else bty = Validation.BoolType.anyBool ∧ c' = c₁ ∩ c₂
theorem
Cedar.Thm.type_of_or_is_sound
{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₁.or x₂) c₁ env = Except.ok (ty, c₂))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
GuardedCapabilitiesInvariant (x₁.or x₂) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (x₁.or x₂) request entities v ∧ InstanceOfType env v ty.typeOf