This file proves that typechecking of .binaryApp .add, binaryApp .sub, and binaryApp .mul expressions is sound.

theorem Cedar.Thm.type_of_int_arith_inversion {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {c c' : Validation.Capabilities} {env : Validation.TypeEnv} {ty : Validation.TypedExpr} (h₁ : op₂ = Spec.BinaryOp.add ∨ op₂ = Spec.BinaryOp.sub ∨ op₂ = Spec.BinaryOp.mul) (h₂ : Validation.typeOf (Spec.Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (ty, c')) : c' = ∅ ∧ ty.typeOf = Validation.CedarType.int ∧ (∃ (c₁ : Validation.Capabilities), (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.int, c₁)) ∧ ∃ (c₂ : Validation.Capabilities), (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.int, c₂)

theorem Cedar.Thm.type_of_int_arith_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₀ : op₂ = Spec.BinaryOp.add ∨ op₂ = Spec.BinaryOp.sub ∨ op₂ = Spec.BinaryOp.mul) (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