This file proves a key auxiliary lemma used to show the completeness of Cedar's symbolic compiler: for every symbolic environment εnv that is well-formed for an expression x, and for interpretation I that is well-formed for εnv, there is concrete environment env that is well-formed with respect to x and that corresponds to the interpretation of εnv under I. The concrete environment env is obtained by concretizing εnv.interpret I with respect to x.

theorem Cedar.Thm.exists_wf_env {x : Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormedFor x → I.WellFormed εnv.entities → ∃ (env : Spec.Env), env ∼ SymCC.SymEnv.interpret I εnv ∧ env.WellFormedFor x

theorem Cedar.Thm.exists_wf_env_for_policies {ps : Spec.Policies} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} : εnv.WellFormedForPolicies ps → I.WellFormed εnv.entities → ∃ (env : Spec.Env), env ∼ SymCC.SymEnv.interpret I εnv ∧ env.WellFormedForPolicies ps