This file proves key auxiliary lemmas for the strong well-formedness assumptions generated by the enforce function in Cedar/SymCC/Enforcer.lean.

theorem Cedar.Thm.enforce_satisfiedBy_swf {xs : List Spec.Expr} {env : Spec.Env} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {assumes : SymCC.Asserts} : env ∼ SymCC.SymEnv.interpret I εnv → I.WellFormed εnv.entities → εnv.StronglyWellFormedForAll xs → env.StronglyWellFormedForAll xs → SymCC.enforce xs εnv = Data.Set.mk assumes → SymCC.Asserts.satisfiedBy I assumes = true

theorem Cedar.Thm.enforce_satisfiedBy_implies_swf_extract? {xs : List Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {assumes : SymCC.Asserts} : εnv.StronglyWellFormedForAll xs → I.WellFormed εnv.entities → SymCC.enforce xs εnv = Data.Set.mk assumes → SymCC.Asserts.satisfiedBy I assumes = true → ∃ (I' : SymCC.Interpretation), ∃ (env : Spec.Env), some env = SymCC.SymEnv.extract? xs I εnv ∧ I'.WellFormed εnv.entities ∧ env ∼ SymCC.SymEnv.interpret I' εnv ∧ env.StronglyWellFormedForAll xs ∧ ∀ (x : Spec.Expr) (t : SymCC.Term), x ∈ xs → SymCC.compile x εnv = Except.ok t → SymCC.Term.interpret I t = SymCC.Term.interpret I' t

theorem Cedar.Thm.enforce_satisfiedBy_implies_swf {xs : List Spec.Expr} {εnv : SymCC.SymEnv} {I : SymCC.Interpretation} {assumes : SymCC.Asserts} : εnv.StronglyWellFormedForAll xs → I.WellFormed εnv.entities → SymCC.enforce xs εnv = Data.Set.mk assumes → SymCC.Asserts.satisfiedBy I assumes = true → ∃ (I' : SymCC.Interpretation), ∃ (env : Spec.Env), I'.WellFormed εnv.entities ∧ env ∼ SymCC.SymEnv.interpret I' εnv ∧ env.StronglyWellFormedForAll xs ∧ ∀ (x : Spec.Expr) (t : SymCC.Term), x ∈ xs → SymCC.compile x εnv = Except.ok t → SymCC.Term.interpret I t = SymCC.Term.interpret I' t