This file proves two key auxiliary lemmas used to show the soundness and completeness of Cedar's symbolic compiler.

@[irreducible]

theorem Cedar.Thm.compile_evaluate {x : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} : env ∼ εnv → env.WellFormedFor x → εnv.WellFormedFor x → SymCC.compile x εnv = Except.ok t → Spec.evaluate x env.request env.entities ∼ t

The lemma shows that the symbolic compiler (compile) behaves like the concrete evaluator (evaluate) on literal inputs.

In particular, let x be an expression, εnv a well-formed symbolic environment for x, and env a well-formed concrete environment for x that is equivalent to εnv. Then, the result produced by the symbolic compiler on x and εnv is equivalent to the result produced by the concrete evaluator x and env.

@[irreducible]

theorem Cedar.Thm.compile_interpret {x : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {t : SymCC.Term} : I.WellFormed εnv.entities → εnv.WellFormedFor x → SymCC.compile x εnv = Except.ok t → SymCC.compile x (SymCC.SymEnv.interpret I εnv) = Except.ok (SymCC.Term.interpret I t)

The lemma shows that interpret and compile can be applied in any order to get the same result. In particular, let x be an expression, εnv a well-formed symbolic environment for x, and I a well-formed interpretion for εnv. Then, compiling x with respect to (εnv.interpret I) gives the same result as interpreting the output of compiling x with respect to εnv.

theorem Cedar.Thm.compile_bisimulation {x : Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {t : SymCC.Term} {I : SymCC.Interpretation} : εnv.WellFormedFor x → env.WellFormedFor x → I.WellFormed εnv.entities → env ∼ SymCC.SymEnv.interpret I εnv → SymCC.compile x εnv = Except.ok t → Spec.evaluate x env.request env.entities ∼ SymCC.Term.interpret I t