This file contains theorems saying that compile succeeds
with the correct term type on well-typed expressions.
States the symbolic compiler succeeds on a typed expression tx and
produces a term t with the corresponding type.
Equations
- Cedar.Thm.CompileWellTyped tx εnv = ∃ (t : Cedar.SymCC.Term), Cedar.SymCC.compile tx.toExpr εnv = Except.ok t ∧ t.typeOf = (Cedar.SymCC.TermType.ofType tx.typeOf).option
Instances For
def
Cedar.Thm.CompileWellTypedCondition
(tx : Validation.TypedExpr)
(Γ : Validation.TypeEnv)
(εnv : SymCC.SymEnv)
:
A sufficient condition for CompileWellTyped to hold.
Equations
- Cedar.Thm.CompileWellTypedCondition tx Γ εnv = (εnv = Cedar.SymCC.SymEnv.ofEnv Γ ∧ Cedar.Thm.TypedExpr.WellTyped Γ tx ∧ εnv.WellFormedFor tx.toExpr)
Instances For
A stronger version of CompileWellTyped that
also includes well-formedness of the term
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Cedar.Thm.ofRecordType_preserves_attr
{rty : Validation.RecordType}
{attr : Spec.Attr}
{qty : Validation.Qualified Validation.CedarType}
{ty : Validation.CedarType}
(hattr_exists : Data.Map.find? rty attr = some qty)
(hattr_ty : qty.getType = ty)
:
∃ (attr_ty : SymCC.TermType), (Data.Map.mk (SymCC.TermType.ofRecordType rty.1)).find? attr = some attr_ty ∧ match attr_ty with
| attr_ty'.option => SymCC.TermType.ofType ty = attr_ty' ∧ ¬qty.isRequired = true
| x => SymCC.TermType.ofType ty = attr_ty ∧ qty.isRequired = true
If some attribute exists in a record type,
then it should still exist after applying TermType.ofRecordType
theorem
Cedar.Thm.isCedarRecordType_implies_isRecordType
{ty : SymCC.TermType}
(hty : ty.isCedarRecordType = true)
:
theorem
Cedar.Thm.compile_well_typed_lit
{p : Spec.Prim}
{tx : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(h : CompileWellTypedCondition (Validation.TypedExpr.lit p tx) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.lit p tx) εnv
theorem
Cedar.Thm.compile_well_typed_var
{v : Spec.Var}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(hcond : CompileWellTypedCondition (Validation.TypedExpr.var v ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.var v ty) εnv
theorem
Cedar.Thm.compile_well_typed_ite
{a b c : Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(iha : CompileWellTypedAndWF a εnv)
(ihb : CompileWellTypedAndWF b εnv)
(ihc : CompileWellTypedAndWF c εnv)
(hcond_ite : CompileWellTypedCondition (a.ite b c ty) Γ εnv)
:
CompileWellTyped (a.ite b c ty) εnv
theorem
Cedar.Thm.compile_well_typed_or_and
{a b : Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(iha : CompileWellTypedAndWF a εnv)
(ihb : CompileWellTypedAndWF b εnv)
:
(CompileWellTypedCondition (a.or b ty) Γ εnv → CompileWellTyped (a.or b ty) εnv) ∧ (CompileWellTypedCondition (a.and b ty) Γ εnv → CompileWellTyped (a.and b ty) εnv)
Combined case for or and and
theorem
Cedar.Thm.compile_well_typed_unaryApp
{op : Spec.UnaryOp}
{expr : Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihexpr : CompileWellTypedAndWF expr εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.unaryApp op expr ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.unaryApp op expr ty) εnv
theorem
Cedar.Thm.compile_binaryApp_wf_types
{op : Spec.BinaryOp}
{a b : Validation.TypedExpr}
{ty : Validation.CedarType}
{t tcomp_a tcomp_b : SymCC.Term}
{εnv : SymCC.SymEnv}
(hwf_ent : εnv.entities.WellFormed)
(hok_a : SymCC.compile a.toExpr εnv = Except.ok tcomp_a)
(hok_b : SymCC.compile b.toExpr εnv = Except.ok tcomp_b)
(hwf_get_comp_a : SymCC.Term.WellFormed εnv.entities (SymCC.Factory.option.get tcomp_a))
(hwf_get_comp_b : SymCC.Term.WellFormed εnv.entities (SymCC.Factory.option.get tcomp_b))
(hok : SymCC.compile (Validation.TypedExpr.binaryApp op a b ty).toExpr εnv = Except.ok t)
:
match op, hok with
| Spec.BinaryOp.add, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.BinaryOp.sub, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.BinaryOp.mul, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.BinaryOp.getTag, hok =>
∃ (ety : Spec.EntityType), ∃ (τs : SymCC.SymTags), (SymCC.Factory.option.get tcomp_a).typeOf = SymCC.TermType.entity ety ∧ εnv.entities.tags ety = some (some τs) ∧ t.typeOf = τs.vals.outType.option
| x, hok => t.typeOf = SymCC.TermType.bool.option
Similar to compileApp₂_wf_types, but for compile
theorem
Cedar.Thm.compile_ok_implies_compile_well_typed_binaryApp
{op : Spec.BinaryOp}
{a b : Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(iha : CompileWellTypedAndWF a εnv)
(ihb : CompileWellTypedAndWF b εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.binaryApp op a b ty) Γ εnv)
(hok : ∃ (t : SymCC.Term), SymCC.compile (Validation.TypedExpr.binaryApp op a b ty).toExpr εnv = Except.ok t)
:
CompileWellTyped (Validation.TypedExpr.binaryApp op a b ty) εnv
Since we have the nice lemma compileApp₂_wf_types,
it's enough to prove that compile of a binaryApp succeeds.
theorem
Cedar.Thm.compile_well_typed_binaryApp
{op : Spec.BinaryOp}
{a b : Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(iha : CompileWellTypedAndWF a εnv)
(ihb : CompileWellTypedAndWF b εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.binaryApp op a b ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.binaryApp op a b ty) εnv
theorem
Cedar.Thm.compile_well_typed_getAttr
{expr : Validation.TypedExpr}
{attr : Spec.Attr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihexpr : CompileWellTypedAndWF expr εnv)
(hcond : CompileWellTypedCondition (expr.getAttr attr ty) Γ εnv)
:
CompileWellTyped (expr.getAttr attr ty) εnv
theorem
Cedar.Thm.compile_well_typed_hasAttr
{expr : Validation.TypedExpr}
{attr : Spec.Attr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihexpr : CompileWellTypedAndWF expr εnv)
(hcond : CompileWellTypedCondition (expr.hasAttr attr ty) Γ εnv)
:
CompileWellTyped (expr.hasAttr attr ty) εnv
theorem
Cedar.Thm.compile_well_typed_set
{xs : List Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihxs : ∀ (x : Validation.TypedExpr), x ∈ xs → CompileWellTypedAndWF x εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.set xs ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.set xs ty) εnv
theorem
Cedar.Thm.compile_well_typed_record
{xs : List (Spec.Attr × Validation.TypedExpr)}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihxs : ∀ (a : Spec.Attr) (x : Validation.TypedExpr), (a, x) ∈ xs → CompileWellTypedAndWF x εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.record xs ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.record xs ty) εnv
theorem
Cedar.Thm.compile_well_typed_call
{xfn : Spec.ExtFun}
{xs : List Validation.TypedExpr}
{ty : Validation.CedarType}
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
(ihxs : ∀ (x : Validation.TypedExpr), x ∈ xs → CompileWellTypedAndWF x εnv)
(hcond : CompileWellTypedCondition (Validation.TypedExpr.call xfn xs ty) Γ εnv)
:
CompileWellTyped (Validation.TypedExpr.call xfn xs ty) εnv
@[irreducible]
theorem
Cedar.Thm.compile_well_typed_on_wf_expr
{Γ : Validation.TypeEnv}
{εnv : SymCC.SymEnv}
{tx : Validation.TypedExpr}
:
CompileWellTypedCondition tx Γ εnv → CompileWellTyped tx εnv
Compiling a well-typed expression should produce a term of the corresponding TermType,
assuming that the expression is well-formed in the symbolic environment.