Documentation

Cedar.Thm.SymCC.Env.Soundness

This file contains the soundness theorems of Sym.ofEnv

source
theorem Cedar.Thm.env_symbolize?_wf {Γ : Validation.TypeEnv} {env : Spec.Env} (hwf_env : env.StronglyWellFormed) (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) :
(env.symbolize? Γ).WellFormed (SymCC.SymEnv.ofEnv Γ).entities
source
theorem Cedar.Thm.env_symbolize?_same {Γ : Validation.TypeEnv} {env : Spec.Env} (hwf_env : env.StronglyWellFormed) (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) :
env ∼ SymCC.SymEnv.interpret (env.symbolize? Γ) (SymCC.SymEnv.ofEnv Γ)
source
theorem Cedar.Thm.ofEnv_soundness {Γ : Validation.TypeEnv} {env : Spec.Env} (hwf_env : env.StronglyWellFormed) (hinst : InstanceOfWellFormedEnvironment env.request env.entities Γ) :
env∈ᵢSymCC.SymEnv.ofEnv Γ