This file proves that typechecking of .call expressions is sound.
theorem
Cedar.Thm.type_of_call_args_inversion
{xs : List Spec.Expr}
{txs : List Validation.TypedExpr}
{c : Validation.Capabilities}
{env : Validation.TypeEnv}
(htxs :
(xs.mapM₁ fun (x : { x : Spec.Expr // x ∈ xs }) => Validation.justType (Validation.typeOf x.val c env)) = Except.ok txs)
:
List.Forall₂
(fun (xᵢ : Spec.Expr) (txᵢ : Validation.TypedExpr) =>
∃ (cᵢ : Validation.Capabilities), Validation.typeOf xᵢ c env = Except.ok (txᵢ, cᵢ))
xs txs
theorem
Cedar.Thm.type_of_call_inversion
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(htx : Validation.typeOf (Spec.Expr.call xfn xs) c env = Except.ok (tx, c'))
:
∃ (txs : List Validation.TypedExpr), (∃ (ty : Validation.CedarType), tx = Validation.TypedExpr.call xfn txs ty) ∧ List.Forall₂
(fun (xᵢ : Spec.Expr) (txᵢ : Validation.TypedExpr) =>
∃ (cᵢ : Validation.Capabilities), Validation.typeOf xᵢ c env = Except.ok (txᵢ, cᵢ))
xs txs
theorem
Cedar.Thm.type_of_call_decimal_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.decimal xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.decimal ∧ c' = ∅ ∧ ∃ (s : String), xs = [Spec.Expr.lit (Spec.Prim.string s)] ∧ (Spec.Ext.Decimal.decimal s).isSome = true
theorem
Cedar.Thm.type_of_call_decimal_is_sound
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.decimal xs) c₁ env = Except.ok (ty, c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.decimal xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.decimal xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_datetime_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.datetime xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.datetime ∧ c' = ∅ ∧ ∃ (s : String), xs = [Spec.Expr.lit (Spec.Prim.string s)] ∧ (Spec.Ext.Datetime.parse s).isSome = true
theorem
Cedar.Thm.type_of_call_datetime_is_sound
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.datetime xs) c₁ env = Except.ok (ty, c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.datetime xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.datetime xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_duration_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.duration xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.duration ∧ c' = ∅ ∧ ∃ (s : String), xs = [Spec.Expr.lit (Spec.Prim.string s)] ∧ (Spec.Ext.Datetime.duration s).isSome = true
theorem
Cedar.Thm.type_of_call_duration_is_sound
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.duration xs) c₁ env = Except.ok (ty, c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.duration xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.duration xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_ip_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.ip xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr ∧ c' = ∅ ∧ ∃ (s : String), xs = [Spec.Expr.lit (Spec.Prim.string s)] ∧ (Spec.Ext.IPAddr.ip s).isSome = true
theorem
Cedar.Thm.type_of_call_ip_is_sound
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.ip xs) c₁ env = Except.ok (ty, c₂))
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.ip xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.ip xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.typeOf_of_binary_call_inversion
{xs : List Spec.Expr}
{c : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty₁ ty₂ : Validation.TypedExpr}
(h₁ :
(xs.mapM₁ fun (x : { x : Spec.Expr // x ∈ xs }) => Validation.justType (Validation.typeOf x.val c env)) = Except.ok [ty₁, ty₂])
:
Equations
- Cedar.Thm.IsDecimalComparator Cedar.Spec.ExtFun.lessThan = True
- Cedar.Thm.IsDecimalComparator Cedar.Spec.ExtFun.lessThanOrEqual = True
- Cedar.Thm.IsDecimalComparator Cedar.Spec.ExtFun.greaterThan = True
- Cedar.Thm.IsDecimalComparator Cedar.Spec.ExtFun.greaterThanOrEqual = True
- Cedar.Thm.IsDecimalComparator x✝ = False
Instances For
theorem
Cedar.Thm.type_of_call_decimal_comparator_inversion
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₀ : IsDecimalComparator xfn)
(h₁ : Validation.typeOf (Spec.Expr.call xfn xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool ∧ c' = ∅ ∧ ∃ (x₁ : Spec.Expr), ∃ (x₂ : Spec.Expr), ∃ (c₁ : Validation.Capabilities), ∃ (c₂ : Validation.Capabilities), xs = [x₁, x₂] ∧ (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.decimal, c₁) ∧ (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.decimal, c₂)
theorem
Cedar.Thm.type_of_call_decimal_comparator_is_sound
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₀ : IsDecimalComparator xfn)
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.call xfn xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call xfn xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call xfn xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_isInRange_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.isInRange xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool ∧ c' = ∅ ∧ ∃ (x₁ : Spec.Expr), ∃ (x₂ : Spec.Expr), ∃ (c₁ : Validation.Capabilities), ∃ (c₂ : Validation.Capabilities), xs = [x₁, x₂] ∧ (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.ipAddr, c₁) ∧ (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.ipAddr, c₂)
theorem
Cedar.Thm.type_of_call_isInRange_comparator_is_sound
{xs : List 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.call Spec.ExtFun.isInRange xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.isInRange xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.isInRange xs) request entities v ∧ InstanceOfType env v ty.typeOf
Equations
Instances For
theorem
Cedar.Thm.typeOf_of_unary_call_inversion
{xs : List Spec.Expr}
{c : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty₁ : Validation.TypedExpr}
(h₁ :
(xs.mapM₁ fun (x : { x : Spec.Expr // x ∈ xs }) => Validation.justType (Validation.typeOf x.val c env)) = Except.ok [ty₁])
:
theorem
Cedar.Thm.type_of_call_toTime_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.toTime xs) c env = Except.ok (ty, c'))
:
theorem
Cedar.Thm.type_of_call_toTime_is_sound
{xs : List 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.call Spec.ExtFun.toTime xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.toTime xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.toTime xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_toDate_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.toDate xs) c env = Except.ok (ty, c'))
:
theorem
Cedar.Thm.type_of_call_toDate_is_sound
{xs : List 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.call Spec.ExtFun.toDate xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.toDate xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.toDate xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_offset_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.offset xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.datetime ∧ c' = ∅ ∧ ∃ (x₁ : Spec.Expr), ∃ (x₂ : Spec.Expr), ∃ (c₁ : Validation.Capabilities), ∃ (c₂ : Validation.Capabilities), xs = [x₁, x₂] ∧ (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.datetime, c₁) ∧ (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.duration, c₂)
theorem
Cedar.Thm.type_of_call_offset_is_sound
{xs : List 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.call Spec.ExtFun.offset xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.offset xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.offset xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_durationSince_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.call Spec.ExtFun.durationSince xs) c env = Except.ok (ty, c'))
:
ty.typeOf = Validation.CedarType.ext Validation.ExtType.duration ∧ c' = ∅ ∧ ∃ (x₁ : Spec.Expr), ∃ (x₂ : Spec.Expr), ∃ (c₁ : Validation.Capabilities), ∃ (c₂ : Validation.Capabilities), xs = [x₁, x₂] ∧ (Validation.typeOf x₁ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.datetime, c₁) ∧ (Validation.typeOf x₂ c env).typeOf = Except.ok (Validation.CedarType.ext Validation.ExtType.datetime, c₂)
theorem
Cedar.Thm.type_of_call_durationSince_is_sound
{xs : List 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.call Spec.ExtFun.durationSince xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call Spec.ExtFun.durationSince xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call Spec.ExtFun.durationSince xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_ipAddr_recognizer_inversion
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₀ : IsIpAddrRecognizer xfn)
(h₁ : Validation.typeOf (Spec.Expr.call xfn xs) c env = Except.ok (ty, c'))
:
theorem
Cedar.Thm.type_of_call_ipAddr_recognizer_is_sound
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₀ : IsIpAddrRecognizer xfn)
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.call xfn xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call xfn xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call xfn xs) request entities v ∧ InstanceOfType env v ty.typeOf
Equations
- Cedar.Thm.IsDurationConverter Cedar.Spec.ExtFun.toMilliseconds = True
- Cedar.Thm.IsDurationConverter Cedar.Spec.ExtFun.toSeconds = True
- Cedar.Thm.IsDurationConverter Cedar.Spec.ExtFun.toMinutes = True
- Cedar.Thm.IsDurationConverter Cedar.Spec.ExtFun.toHours = True
- Cedar.Thm.IsDurationConverter Cedar.Spec.ExtFun.toDays = True
- Cedar.Thm.IsDurationConverter x✝ = False
Instances For
theorem
Cedar.Thm.type_of_call_duration_converter_inversion
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(h₀ : IsDurationConverter xfn)
(h₁ : Validation.typeOf (Spec.Expr.call xfn xs) c env = Except.ok (ty, c'))
:
theorem
Cedar.Thm.type_of_call_duration_converter_is_sound
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₀ : IsDurationConverter xfn)
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.call xfn xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call xfn xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call xfn xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_call_is_sound
{xfn : Spec.ExtFun}
{xs : List 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.call xfn xs) c₁ env = Except.ok (ty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.call xfn xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.call xfn xs) request entities v ∧ InstanceOfType env v ty.typeOf
theorem
Cedar.Thm.type_of_preserves_evaluation_results_call
{xfn : Spec.ExtFun}
{ty : Validation.TypedExpr}
{c₂ : Validation.Capabilities}
{request : Spec.Request}
{entities : Spec.Entities}
{xs : List Spec.Expr}
{tys : List Validation.TypedExpr}
:
Validation.typeOfCall xfn tys xs = Except.ok (ty, c₂) →
List.mapM (fun (x : Spec.Expr) => Spec.evaluate x request entities) xs = List.mapM (fun (y : Validation.TypedExpr) => Spec.evaluate y.toExpr request entities) tys →
Spec.evaluate (Spec.Expr.call xfn xs) request entities = Spec.evaluate ty.toExpr request entities