theorem Cedar.Thm.Opt.compileWithEffect.correctness (effect : Spec.Effect) (p : Spec.Policy) (εnv : SymCC.SymEnv) : SymCC.Opt.compileWithEffect effect p εnv = do let term ← SymCC.compileWithEffect effect p εnv have footprint : Data.Set SymCC.Term := SymCC.footprint p.toExpr εnv Except.ok (Option.map (fun (term : SymCC.Term) => { term := term, footprint := footprint }) term)

Correctness theorem for Opt.compileWithEffect:

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

theorem Cedar.Thm.Opt.satisfiedPolicies.correctness (effect : Spec.Effect) (ps : Spec.Policies) (εnv : SymCC.SymEnv) : SymCC.Opt.satisfiedPolicies effect ps εnv = do let term ← SymCC.satisfiedPolicies effect ps εnv have footprint : Data.Set SymCC.Term := SymCC.footprints (List.filterMap (fun (p : Spec.Policy) => if p.effect = effect then some p.toExpr else none) ps) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.satisfiedPolicies:

Opt.satisfiedPolicies produces the same term as SymCC.satisfiedPolicies, and Opt.satisfiedPolicies produces the same footprint as footprints applied to just the policies with the appropriate effect

theorem Cedar.Thm.Opt.isAuthorized.correctness (ps : Spec.Policies) (εnv : SymCC.SymEnv) : SymCC.Opt.isAuthorized ps εnv = do let term ← SymCC.isAuthorized ps εnv have footprint : Data.Set SymCC.Term := SymCC.footprints (List.map Spec.Policy.toExpr ps) εnv Except.ok { term := term, footprint := footprint }

Correctness theorem for Opt.isAuthorized:

Opt.isAuthorized produces the same term as SymCC.isAuthorized, and Opt.isAuthorized produces the same footprint as footprints