This file proves that typechecking of .binaryApp .containsAny and .binaryApp .containsAll expressions is sound.

theorem Cedar.Thm.type_of_containsA_inversion {op₂ : Spec.BinaryOp} {x₁ x₂ : Spec.Expr} {c c' : Validation.Capabilities} {env : Validation.TypeEnv} {ty : Validation.TypedExpr} (h₁ : op₂ = Spec.BinaryOp.containsAll ∨ op₂ = Spec.BinaryOp.containsAny) (h₂ : Validation.typeOf (Spec.Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (ty, c')) : c' = ∅ ∧ ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool ∧ ∃ (ty₁ : Validation.CedarType), ∃ (ty₂ : Validation.CedarType), (ty₁ ⊔ ty₂).isSome = true ∧ (∃ (c₁ : Validation.Capabilities), (Validation.typeOf x₁ c env).typeOf = Except.ok (ty₁.set, c₁)) ∧ ∃ (c₂ : Validation.Capabilities), (Validation.typeOf x₂ c env).typeOf = Except.ok (ty₂.set, c₂)

theorem Cedar.Thm.type_of_containsA_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.containsAll ∨ op₂ = Spec.BinaryOp.containsAny) (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