This file proves that both compile and evaluate preserve well-formedness. #
theorem
Cedar.Thm.compileAttrsOf_wf
{t t₁ : SymCC.Term}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hok : SymCC.compileAttrsOf t₁ εs = Except.ok t)
:
SymCC.Term.WellFormed εs t ∧ ∃ (rty : Data.Map Spec.Attr SymCC.TermType), t.typeOf = SymCC.TermType.record rty ∧ (t₁.typeOf = SymCC.TermType.record rty ∨ ∃ (ety : Spec.EntityType), ∃ (fₐ : SymCC.UnaryFunction), t₁.typeOf = SymCC.TermType.entity ety ∧ εs.attrs ety = some fₐ ∧ fₐ.outType = SymCC.TermType.record rty)
theorem
Cedar.Thm.compileHasAttr_wf
{t t₁ : SymCC.Term}
{a : Spec.Attr}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hok : SymCC.compileHasAttr t₁ a εs = Except.ok t)
:
theorem
Cedar.Thm.compileGetAttr_wf
{t t₁ : SymCC.Term}
{a : Spec.Attr}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hok : SymCC.compileGetAttr t₁ a εs = Except.ok t)
:
theorem
Cedar.Thm.compileApp₁_wf_types
{op₁ : Spec.UnaryOp}
{t t₁ : SymCC.Term}
{εs : SymCC.SymEntities}
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hok : SymCC.compileApp₁ op₁ t₁ = Except.ok t)
:
SymCC.Term.WellFormed εs t ∧ match op₁, hok with
| Spec.UnaryOp.neg, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| x, hok => t.typeOf = SymCC.TermType.bool.option
theorem
Cedar.Thm.compileApp₁_wf
{op₁ : Spec.UnaryOp}
{t t₁ : SymCC.Term}
{εs : SymCC.SymEntities}
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hok : SymCC.compileApp₁ op₁ t₁ = Except.ok t)
:
theorem
Cedar.Thm.compileInₑ.isEq_wf
{t₁ t₂ : SymCC.Term}
{εs : SymCC.SymEntities}
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hw₂ : SymCC.Term.WellFormed εs t₂)
:
SymCC.Term.WellFormed εs (SymCC.compileInₑ.isEq t₁ t₂) ∧ (SymCC.compileInₑ.isEq t₁ t₂).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileInₑ.isIn_wf
{t₁ t₂ : SymCC.Term}
{ancs? : Option SymCC.UnaryFunction}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety₁)
(hw₂ : SymCC.Term.WellFormed εs t₂)
(hty₂ : t₂.typeOf = SymCC.TermType.entity ety₂)
(ha : ancs? = εs.ancestorsOfType ety₁ ety₂)
:
SymCC.Term.WellFormed εs (SymCC.compileInₑ.isIn t₁ t₂ ancs?) ∧ (SymCC.compileInₑ.isIn t₁ t₂ ancs?).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileInₑ_wf
{t₁ t₂ : SymCC.Term}
{ancs? : Option SymCC.UnaryFunction}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hty₁ : t₁.typeOf = SymCC.TermType.entity ety₁)
(hw₂ : SymCC.Term.WellFormed εs t₂)
(hty₂ : t₂.typeOf = SymCC.TermType.entity ety₂)
(ha : ancs? = εs.ancestorsOfType ety₁ ety₂)
:
SymCC.Term.WellFormed εs (SymCC.compileInₑ t₁ t₂ ancs?) ∧ (SymCC.compileInₑ t₁ t₂ ancs?).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileInₛ.isIn₁_wf
{t ts : SymCC.Term}
{εs : SymCC.SymEntities}
(hw₁ : SymCC.Term.WellFormed εs t)
(hw₂ : SymCC.Term.WellFormed εs ts)
:
SymCC.Term.WellFormed εs (SymCC.compileInₛ.isIn₁ t ts) ∧ (SymCC.compileInₛ.isIn₁ t ts).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileInₛ.isIn₂_wf
{t ts : SymCC.Term}
{ancs? : Option SymCC.UnaryFunction}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t)
(hty₁ : t.typeOf = SymCC.TermType.entity ety₁)
(hw₂ : SymCC.Term.WellFormed εs ts)
(hty₂ : ts.typeOf = (SymCC.TermType.entity ety₂).set)
(ha : ancs? = εs.ancestorsOfType ety₁ ety₂)
:
SymCC.Term.WellFormed εs (SymCC.compileInₛ.isIn₂ t ts ancs?) ∧ (SymCC.compileInₛ.isIn₂ t ts ancs?).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileInₛ_wf
{t ts : SymCC.Term}
{ancs? : Option SymCC.UnaryFunction}
{ety₁ ety₂ : Spec.EntityType}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t)
(hty₁ : t.typeOf = SymCC.TermType.entity ety₁)
(hw₂ : SymCC.Term.WellFormed εs ts)
(hty₂ : ts.typeOf = (SymCC.TermType.entity ety₂).set)
(ha : ancs? = εs.ancestorsOfType ety₁ ety₂)
:
SymCC.Term.WellFormed εs (SymCC.compileInₛ t ts ancs?) ∧ (SymCC.compileInₛ t ts ancs?).typeOf = SymCC.TermType.bool
theorem
Cedar.Thm.compileApp₂_wf_types
{op₂ : Spec.BinaryOp}
{t t₁ t₂ : SymCC.Term}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hw₂ : SymCC.Term.WellFormed εs t₂)
(hok : SymCC.compileApp₂ op₂ t₁ t₂ εs = Except.ok t)
:
SymCC.Term.WellFormed εs 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), t₁.typeOf = SymCC.TermType.entity ety ∧ εs.tags ety = some (some τs) ∧ t.typeOf = τs.vals.outType.option
| x, hok => t.typeOf = SymCC.TermType.bool.option
theorem
Cedar.Thm.compileApp₂_wf
{op₂ : Spec.BinaryOp}
{t t₁ t₂ : SymCC.Term}
{εs : SymCC.SymEntities}
(hwε : εs.WellFormed)
(hw₁ : SymCC.Term.WellFormed εs t₁)
(hw₂ : SymCC.Term.WellFormed εs t₂)
(hok : SymCC.compileApp₂ op₂ t₁ t₂ εs = Except.ok t)
:
theorem
Cedar.Thm.compileCall_wf_types
{f : Spec.ExtFun}
{ts : List SymCC.Term}
{εs : SymCC.SymEntities}
{t : SymCC.Term}
(hwf : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t)
(hok : SymCC.compileCall f ts = Except.ok t)
:
SymCC.Term.WellFormed εs t ∧ match f, hok with
| Spec.ExtFun.decimal, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.decimal).option
| Spec.ExtFun.ip, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.ipAddr).option
| Spec.ExtFun.datetime, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option
| Spec.ExtFun.offset, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option
| Spec.ExtFun.toDate, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.datetime).option
| Spec.ExtFun.toTime, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option
| Spec.ExtFun.duration, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option
| Spec.ExtFun.durationSince, hok => t.typeOf = (SymCC.TermType.ext Validation.ExtType.duration).option
| Spec.ExtFun.toMilliseconds, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.ExtFun.toSeconds, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.ExtFun.toMinutes, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.ExtFun.toHours, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| Spec.ExtFun.toDays, hok => t.typeOf = (SymCC.TermType.bitvec 64).option
| x, hok => t.typeOf = SymCC.TermType.bool.option
theorem
Cedar.Thm.compileCall_wf
{f : Spec.ExtFun}
{ts : List SymCC.Term}
{εs : SymCC.SymEntities}
{t : SymCC.Term}
(hwf : ∀ (t : SymCC.Term), t ∈ ts → SymCC.Term.WellFormed εs t)
(hok : SymCC.compileCall f ts = Except.ok t)
:
@[irreducible]
theorem
Cedar.Thm.compile_wf
{x : Spec.Expr}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
:
εnv.WellFormedFor x →
SymCC.compile x εnv = Except.ok t →
SymCC.Term.WellFormed εnv.entities t ∧ ∃ (ty : SymCC.TermType), t.typeOf = ty.option
theorem
Cedar.Thm.compile_option_get_wf
{x : Spec.Expr}
{εnv : SymCC.SymEnv}
{t : SymCC.Term}
:
εnv.WellFormedFor x →
SymCC.compile x εnv = Except.ok t →
∃ (ty : SymCC.TermType), (SymCC.Term.WellFormed εnv.entities t ∧ t.typeOf = ty.option) ∧ SymCC.Term.WellFormed εnv.entities (SymCC.Factory.option.get t) ∧ (SymCC.Factory.option.get t).typeOf = ty
@[irreducible]
theorem
Cedar.Thm.evaluate_wf
{x : Spec.Expr}
{env : Spec.Env}
{v : Spec.Value}
:
env.WellFormedFor x → Spec.evaluate x env.request env.entities = Except.ok v → Spec.Value.WellFormed env.entities v
theorem
Cedar.Thm.wf_value_uid_implies_exists_entity_data
{es : Spec.Entities}
{uid : Spec.EntityUID}
(hwf : Spec.Value.WellFormed es (Spec.Value.prim (Spec.Prim.entityUID uid)))
: