This file contains expression-kind-specific lemmas of the theorem typechecked_is_well_typed_after_lifting
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_lit
{p : Spec.Prim}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
:
Validation.typeOf (Spec.Expr.lit p) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_var
{v : Spec.Var}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
:
Validation.typeOf (Spec.Expr.var v) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_ite
{cond thenExpr elseExpr : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf cond c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(hᵢ₂ :
∀ (c₁_1 : Validation.Capabilities) {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf thenExpr (c₁ ∪ c₁_1) env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(hᵢ₃ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf elseExpr c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (cond.ite thenExpr elseExpr) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_and
{x₁ x₂ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(hᵢ₂ :
∀ (c : Validation.Capabilities) {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₂ (c₁ ∪ c) env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (x₁.and x₂) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_or
{x₁ x₂ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(hᵢ₂ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₂ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (x₁.or x₂) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_unary_app
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{op₁ : Spec.UnaryOp}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (Spec.Expr.unaryApp op₁ x₁) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_binary_app
{x₁ x₂ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{op₂ : Spec.BinaryOp}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(hᵢ₂ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₂ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (Spec.Expr.binaryApp op₂ x₁ x₂) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_has_attr
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{attr : Spec.Attr}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (x₁.hasAttr attr) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_get_attr_in_record
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{attr : Spec.Attr}
{tc : Validation.TypedExpr × Validation.Capabilities}
{rty : Data.Map Spec.Attr (Validation.Qualified Validation.CedarType)}
{a : Validation.CedarType}
(h₃ : Validation.getAttrInRecord tc.fst.typeOf rty x₁ attr c₁ = Except.ok (a, c₂))
:
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_get_attr
{x₁ : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{attr : Spec.Attr}
(hᵢ₁ :
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (x₁.getAttr attr) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_call_arg
{c₁ : Validation.Capabilities}
{env : Validation.TypeEnv}
{xs : List Spec.Expr}
{tys : List Validation.TypedExpr}
(hᵢ :
List.Forall₂
(fun (x : Spec.Expr) (y : Validation.TypedExpr) => Validation.justType (Validation.typeOf x c₁ env) = Except.ok y)
xs tys)
(hᵢ₁ :
∀ (x₁ : Spec.Expr),
x₁ ∈ xs →
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
(x : Validation.TypedExpr)
:
(x ∈ tys.map₁ fun (x : { x : Validation.TypedExpr // x ∈ tys }) => x.val.liftBoolTypes) → TypedExpr.WellTyped env x
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_call
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{xfn : Spec.ExtFun}
{xs : List Spec.Expr}
(hᵢ₁ :
∀ (x₁ : Spec.Expr),
x₁ ∈ xs →
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (Spec.Expr.call xfn xs) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.foldM_lub_some
{x y : Validation.CedarType}
{xs : List Validation.CedarType}
:
List.foldlM Validation.lub? x xs = some y → ∀ (t : Validation.CedarType), t ∈ xs → (t ⊑ y) = true
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_set
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{xs : List Spec.Expr}
(hᵢ₁ :
∀ (x₁ : Spec.Expr),
x₁ ∈ xs →
∀ {c₂ : Validation.Capabilities} {ty : Validation.TypedExpr},
Validation.typeOf x₁ c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (Spec.Expr.set xs) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.record_lifting_make
{tys : List (Spec.Attr × Validation.TypedExpr)}
:
Validation.RecordType.liftBoolTypes
(Data.Map.make
(List.map (fun (x : Spec.Attr × Validation.TypedExpr) => (x.fst, Validation.Qualified.required x.snd.typeOf))
tys)) = Data.Map.make
(List.map (fun (x : Spec.Attr × Validation.TypedExpr) => (x.fst, Validation.Qualified.required x.snd.typeOf))
(List.map (fun (x : Spec.Attr × Validation.TypedExpr) => (x.fst, x.snd.liftBoolTypes)) tys))
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting_record
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
{axs : List (Spec.Attr × Spec.Expr)}
(hᵢ₁ :
∀ (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₂) → TypedExpr.WellTyped env ty.liftBoolTypes)
:
Validation.typeOf (Spec.Expr.record axs) c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
theorem
Cedar.Thm.typechecked_is_well_typed_after_lifting
{e : Spec.Expr}
{c₁ c₂ : Validation.Capabilities}
{env : Validation.TypeEnv}
{ty : Validation.TypedExpr}
:
Validation.typeOf e c₁ env = Except.ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes
The type checker produces typed expressions that are well-typed after type lifting. TODO: move this around after the proof is fixed