This file proves key lemmas for the strong well-formedness assumptions for
policies, generated by the enforce function in Cedar.SymCC.Enforcer. #
theorem
Cedar.Thm.swf_implies_enforce_satisfiedBy
{ps : Spec.Policies}
{env : Spec.Env}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{assumes : SymCC.Asserts}
:
env ∼ SymCC.SymEnv.interpret I εnv →
I.WellFormed εnv.entities →
εnv.StronglyWellFormedForPolicies ps →
env.StronglyWellFormedForPolicies ps →
SymCC.enforce (List.map Spec.Policy.toExpr ps) εnv = Data.Set.mk assumes →
SymCC.Asserts.satisfiedBy I assumes = true
theorem
Cedar.Thm.enforce_satisfiedBy_implies_exists_swf_extract?
{ps : Spec.Policies}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{assumes : SymCC.Asserts}
:
εnv.StronglyWellFormedForPolicies ps →
I.WellFormed εnv.entities →
SymCC.enforce (List.map Spec.Policy.toExpr ps) εnv = Data.Set.mk assumes →
SymCC.Asserts.satisfiedBy I assumes = true →
∃ (I' : SymCC.Interpretation), ∃ (env : Spec.Env), some env = SymCC.SymEnv.extract? (List.map Spec.Policy.toExpr ps) I εnv ∧ I'.WellFormed εnv.entities ∧ env ∼ SymCC.SymEnv.interpret I' εnv ∧ env.StronglyWellFormedForPolicies ps ∧ ∀ (p : Spec.Policy) (t : SymCC.Term),
p ∈ ps →
SymCC.compile p.toExpr εnv = Except.ok t → SymCC.Term.interpret I t = SymCC.Term.interpret I' t
theorem
Cedar.Thm.enforce_satisfiedBy_implies_exists_swf
{ps : Spec.Policies}
{εnv : SymCC.SymEnv}
{I : SymCC.Interpretation}
{assumes : SymCC.Asserts}
:
εnv.StronglyWellFormedForPolicies ps →
I.WellFormed εnv.entities →
SymCC.enforce (List.map Spec.Policy.toExpr ps) ε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.StronglyWellFormedForPolicies ps ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ∀ (p : Spec.Policy) (t : SymCC.Term),
p ∈ ps →
SymCC.compile p.toExpr εnv = Except.ok t → SymCC.Term.interpret I t = SymCC.Term.interpret I' t