theorem Cedar.Thm.Opt.compile.correctness.lit (p : Spec.Prim) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.lit p) εnv = do let term ← SymCC.compile (Spec.Expr.lit p) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.lit p) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- lit case

theorem Cedar.Thm.Opt.compile.correctness.var (v : Spec.Var) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.var v) εnv = do let term ← SymCC.compile (Spec.Expr.var v) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.var v) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- var case

theorem Cedar.Thm.Opt.compile.correctness.ite (x₁ x₂ x₃ : Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (x₁.ite x₂ x₃) εnv = do let term ← SymCC.compile (x₁.ite x₂ x₃) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (x₁.ite x₂ x₃) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- ite case

theorem Cedar.Thm.Opt.compile.correctness.andor (x₁ x₂ : Spec.Expr) (εnv : SymCC.SymEnv) : (SymCC.Opt.compile (x₁.and x₂) εnv = do let term ← SymCC.compile (x₁.and x₂) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (x₁.and x₂) εnv Except.ok { term := term, footprint := footprint }) ∧ SymCC.Opt.compile (x₁.or x₂) εnv = do let term ← SymCC.compile (x₁.or x₂) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (x₁.or x₂) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- and and or cases

theorem Cedar.Thm.Opt.compile.correctness.unaryApp (op : Spec.UnaryOp) (x : Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.unaryApp op x) εnv = do let term ← SymCC.compile (Spec.Expr.unaryApp op x) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.unaryApp op x) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- unaryApp case

theorem Cedar.Thm.Opt.compile.correctness.binaryApp (op : Spec.BinaryOp) (x₁ x₂ : Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.binaryApp op x₁ x₂) εnv = do let term ← SymCC.compile (Spec.Expr.binaryApp op x₁ x₂) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.binaryApp op x₁ x₂) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- binaryApp case

theorem Cedar.Thm.Opt.compile.correctness.getAttr (expr : Spec.Expr) (attr : Spec.Attr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (expr.getAttr attr) εnv = do let term ← SymCC.compile (expr.getAttr attr) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (expr.getAttr attr) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- getAttr case

theorem Cedar.Thm.Opt.compile.correctness.hasAttr (expr : Spec.Expr) (attr : Spec.Attr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (expr.hasAttr attr) εnv = do let term ← SymCC.compile (expr.hasAttr attr) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (expr.hasAttr attr) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- hasAttr case

theorem Cedar.Thm.Opt.compile.correctness.extHasAttr (expr : Spec.Expr) (attr : Spec.Attr) (attrs : List Spec.Attr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (expr.extHasAttr attr attrs) εnv = do let term ← SymCC.compile (expr.extHasAttr attr attrs) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (expr.extHasAttr attr attrs) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- extHasAttr case

theorem Cedar.Thm.Opt.compile.correctness.set (ls : List Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.set ls) εnv = do let term ← SymCC.compile (Spec.Expr.set ls) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.set ls) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- set case

theorem Cedar.Thm.Opt.compile.correctness.record (m : List (Spec.Attr × Spec.Expr)) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.record m) εnv = do let term ← SymCC.compile (Spec.Expr.record m) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.record m) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- record case

theorem Cedar.Thm.Opt.compile.correctness.call (xfn : Spec.ExtFun) (args : List Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile (Spec.Expr.call xfn args) εnv = do let term ← SymCC.compile (Spec.Expr.call xfn args) εnv have footprint : Data.Set SymCC.Term := SymCC.footprint (Spec.Expr.call xfn args) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile -- call case

theorem Cedar.Thm.Opt.compile.correctness (x : Spec.Expr) (εnv : SymCC.SymEnv) : SymCC.Opt.compile x εnv = do let term ← SymCC.compile x εnv have footprint : Data.Set SymCC.Term := SymCC.footprint x εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.compile:

Opt.compile produces the same term as SymCC.compile, and Opt.compile produces the same footprint as footprint