This file proves that typechecking of .set expressions is sound.
theorem
Cedar.Thm.type_of_set_tail
{x xhd : Spec.Expr}
{xtl : List Spec.Expr}
{c : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.CedarType}
{hd : Validation.TypedExpr}
{tl : List Validation.TypedExpr}
(h₁ :
((xhd :: xtl).mapM₁ fun (x : { x : Spec.Expr // x ∈ xhd :: xtl }) =>
Validation.justType (Validation.typeOf x.val c env)) = Except.ok (hd :: tl))
(h₂ : List.foldlM Validation.lub? hd.typeOf (List.map Validation.TypedExpr.typeOf tl) = some ty)
(h₃ : List.Mem x xtl)
:
theorem
Cedar.Thm.type_of_set_inversion
{xs : List Spec.Expr}
{c c' : Validation.Capabilities}
{env : Validation.TypeEnv}
{tx : Validation.TypedExpr}
(h₁ : Validation.typeOf (Spec.Expr.set xs) c env = Except.ok (tx, c'))
:
c' = ∅ ∧ ∃ (txs : List Validation.TypedExpr), ∃ (ty : Validation.CedarType), tx = Validation.TypedExpr.set txs ty.set ∧ ∀ (xᵢ : Spec.Expr),
xᵢ ∈ xs →
∃ (txᵢ : Validation.TypedExpr), ∃ (cᵢ : Validation.Capabilities), txᵢ ∈ txs ∧ Validation.typeOf xᵢ c env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty
theorem
Cedar.Thm.list_is_sound_implies_tail_is_sound
{hd : Spec.Expr}
{tl : List Spec.Expr}
(h₁ : ∀ (xᵢ : Spec.Expr), xᵢ ∈ hd :: tl → TypeOfIsSound xᵢ)
(xᵢ : Spec.Expr)
:
xᵢ ∈ tl → TypeOfIsSound xᵢ
theorem
Cedar.Thm.list_is_typed_implies_tail_is_typed
{hd : Spec.Expr}
{tl : List Spec.Expr}
{c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.CedarType}
(h₁ :
∀ (xᵢ : Spec.Expr),
xᵢ ∈ hd :: tl →
∃ (txᵢ : Validation.TypedExpr), ∃ (cᵢ : Validation.Capabilities), Validation.typeOf xᵢ c₁ env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty)
(xᵢ : Spec.Expr)
:
theorem
Cedar.Thm.type_of_set_is_sound_err
{xs : List Spec.Expr}
{c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.CedarType}
{request : Spec.Request}
{entities : Spec.Entities}
{err : Spec.Error}
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₄ :
∀ (xᵢ : Spec.Expr),
xᵢ ∈ xs →
∃ (txᵢ : Validation.TypedExpr), ∃ (cᵢ : Validation.Capabilities), Validation.typeOf xᵢ c₁ env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty)
(h₅ : List.mapM (fun (x : Spec.Expr) => Spec.evaluate x request entities) xs = Except.error err)
:
theorem
Cedar.Thm.type_of_set_is_sound_ok
{xs : List Spec.Expr}
{c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{request : Spec.Request}
{entities : Spec.Entities}
{ty : Validation.CedarType}
{v : Spec.Value}
{vs : List Spec.Value}
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ :
∀ (xᵢ : Spec.Expr),
xᵢ ∈ xs →
∃ (txᵢ : Validation.TypedExpr), ∃ (cᵢ : Validation.Capabilities), Validation.typeOf xᵢ c₁ env = Except.ok (txᵢ, cᵢ) ∧ (txᵢ.typeOf ⊔ ty) = some ty)
(h₄ : List.mapM (fun (x : Spec.Expr) => Spec.evaluate x request entities) xs = Except.ok vs)
(h₅ : v ∈ vs)
:
InstanceOfType env v ty
theorem
Cedar.Thm.type_of_set_is_sound
{xs : List Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{sty : Validation.TypedExpr}
{request : Spec.Request}
{entities : Spec.Entities}
(h₁ : CapabilitiesInvariant c₁ request entities)
(h₂ : InstanceOfWellFormedEnvironment request entities env)
(h₃ : Validation.typeOf (Spec.Expr.set xs) c₁ env = Except.ok (sty, c₂))
(ih : ∀ (xᵢ : Spec.Expr), xᵢ ∈ xs → TypeOfIsSound xᵢ)
:
GuardedCapabilitiesInvariant (Spec.Expr.set xs) c₂ request entities ∧ ∃ (v : Spec.Value), EvaluatesTo (Spec.Expr.set xs) request entities v ∧ InstanceOfType env v sty.typeOf
theorem
Cedar.Thm.type_of_ok_attr_list
{c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{atys : List (Spec.Attr × Validation.TypedExpr)}
{request : Spec.Request}
{entities : Spec.Entities}
{axs : List (Spec.Attr × Spec.Expr)}
:
List.Forall₂
(fun (x : Spec.Attr × Spec.Expr) (y : Spec.Attr × Validation.TypedExpr) =>
Except.map (fun (x_1 : Validation.TypedExpr × Validation.Capabilities) => (x.fst, x_1.fst))
(Validation.typeOf x.snd c₁ env) = Except.ok y)
axs atys →
(∀ (a₁ : Spec.Attr) (x₁ : Spec.Expr),
sizeOf (a₁, x₁).snd < 1 + sizeOf axs →
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) →
Spec.evaluate x₁ request entities = Spec.evaluate ty.toExpr request entities) →
List.Forall₂
(fun (x : Spec.Attr × Spec.Expr) (y : Spec.Attr × Validation.TypedExpr) =>
Spec.bindAttr x.fst (Spec.evaluate x.snd request entities) = Spec.bindAttr y.fst (Spec.evaluate y.snd.toExpr request entities))
axs atys