This file proves that typechecking of .binaryApp .eq expressions is sound.
theorem
Cedar.Thm.type_of_eq_inversion
{x₁ x₂ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.binaryApp Spec.BinaryOp.eq x₁ x₂) c env = Except.ok (ty, c'))
:
c' = ∅ ∧ match x₁, x₂, h₁ with
| Spec.Expr.lit p₁, Spec.Expr.lit p₂, h₁ =>
if p₁ = p₂ then ty.typeOf = Validation.CedarType.bool Validation.BoolType.tt
else ty.typeOf = Validation.CedarType.bool Validation.BoolType.ff
| x, x_1, h₁ =>
∃ (ty₁ : Validation.TypedExpr), ∃ (c₁ : Validation.Capabilities), ∃ (ty₂ : Validation.TypedExpr), ∃ (c₂ : Validation.Capabilities), Validation.typeOf x₁ c env = Except.ok (ty₁, c₁) ∧ Validation.typeOf x₂ c env = Except.ok (ty₂, c₂) ∧ match ty₁.typeOf ⊔ ty₂.typeOf with
| some val => ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool
| none =>
ty.typeOf = Validation.CedarType.bool Validation.BoolType.ff ∧ ∃ (ety₁ : Spec.EntityType), ∃ (ety₂ : Spec.EntityType), ty₁.typeOf = Validation.CedarType.entity ety₁ ∧ ty₂.typeOf = Validation.CedarType.entity ety₂
theorem
Cedar.Thm.no_entity_type_lub_implies_not_eq
{env : Validation.TypeEnv}
{v₁ v₂ : Spec.Value}
{ety₁ ety₂ : Spec.EntityType}
(h₁ : InstanceOfType env v₁ (Validation.CedarType.entity ety₁))
(h₂ : InstanceOfType env v₂ (Validation.CedarType.entity ety₂))
(h₃ : (Validation.CedarType.entity ety₁ ⊔ Validation.CedarType.entity ety₂) = none)
:
theorem
Cedar.Thm.type_of_eq_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 (Spec.Expr.binaryApp Spec.BinaryOp.eq x₁ x₂) c₁ env = Except.ok (ty, c₂))
(ih₁ : TypeOfIsSound x₁)
(ih₂ : TypeOfIsSound x₂)
:
GuardedCapabilitiesInvariant (Spec.Expr.binaryApp Spec.BinaryOp.eq x₁ x₂) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.binaryApp Spec.BinaryOp.eq x₁ x₂) request entities v ∧ InstanceOfType env v ty.typeOf