This file proves that typechecking of .binaryApp expressions is sound.

theorem Cedar.Thm.type_of_binaryApp_inversion {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {c c' : Validation.Capabilities} {env : Validation.TypeEnv} {tx : Validation.TypedExpr} (htx : Validation.typeOf (Spec.Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (tx, c')) : ∃ (tx₁ : Validation.TypedExpr), ∃ (c₁ : Validation.Capabilities), ∃ (tx₂ : Validation.TypedExpr), ∃ (c₂ : Validation.Capabilities), Validation.typeOf x₁ c env = Except.ok (tx₁, c₁) ∧ Validation.typeOf x₂ c env = Except.ok (tx₂, c₂) ∧ ∃ (ty : Validation.CedarType), tx = Validation.TypedExpr.binaryApp op₂ tx₁ tx₂ ty

theorem Cedar.Thm.type_of_binaryApp_is_sound {op₂ : Spec.BinaryOp} {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 op₂ x₁ x₂) c₁ env = Except.ok (ty, c₂)) (ih₁ : TypeOfIsSound x₁) (ih₂ : TypeOfIsSound x₂) : GuardedCapabilitiesInvariant (Spec.Expr.binaryApp op₂ x₁ x₂) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.binaryApp op₂ x₁ x₂) request entities v ∧ InstanceOfType env v ty.typeOf