This file proves that typechecking of .binaryApp .less and binaryApp .lessEq expressions is sound.
theorem
Cedar.Thm.type_of_int_cmp_inversion
{op₂ : Spec.BinaryOp}
{x₁ x₂ : Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : op₂ = Spec.BinaryOp.less ∨ op₂ = Spec.BinaryOp.lessEq)
(h₂ : Validation.typeOf (Spec.Expr.binaryApp op₂ x₁ x₂) c env = Except.ok (ty, c'))
:
c' = ∅ ∧ ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool ∧ (((∃ (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₂)) ∨ ((∃ (c₁ : Validation.Capabilities), (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.datetime, c₁)) ∧ ∃ (c₂ : Validation.Capabilities), (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.datetime, c₂)) ∨ (∃ (c₁ : Validation.Capabilities), (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.duration, c₁)) ∧ ∃ (c₂ : Validation.Capabilities), (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.duration, c₂))
theorem
Cedar.Thm.type_of_int_cmp_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.less ∨ op₂ = Spec.BinaryOp.lessEq)
(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