Some lemmas about CompiledPolicy, CompiledPolicySet, and CompiledPolicies.

theorem Cedar.Thm.intoCompiledPolicySet_correctness {p : Spec.Policy} {Γ : Validation.TypeEnv} : (do let cp ← SymCC.CompiledPolicy.compile p Γ pure cp.intoCompiledPolicySet) = SymCC.CompiledPolicySet.compile [p] Γ

Toplevel theorem about the correctness of CompiledPolicy.intoCompiledPolicySet

Compiling to a CompiledPolicy and then using intoCompiledPolicySet should give exactly the same result as compiling with CompiledPolicySet.compile directly

theorem Cedar.Thm.cp_compile_produces_the_right_policy {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → cp.policy = wp

The .policy of a CompiledPolicy is exactly the policy produced by wellTypedPolicy

theorem Cedar.Thm.cpset_compile_produces_the_right_policies {ps wps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → SymCC.wellTypedPolicies ps Γ = Except.ok wps → cpset.policies = wps

The .policies of a CompiledPolicySet is exactly the policies produced by wellTypedPolicies

theorem Cedar.Thm.cp_compile_produces_the_right_env {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → cp.εnv = SymCC.SymEnv.ofTypeEnv Γ

theorem Cedar.Thm.cpset_compile_produces_the_right_env {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → cpset.εnv = SymCC.SymEnv.ofTypeEnv Γ

theorem Cedar.Thm.cp_compile_produces_the_right_term {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → Except.ok cp.term = SymCC.compile wp.toExpr (SymCC.SymEnv.ofTypeEnv Γ)

theorem Cedar.Thm.cpset_compile_produces_the_right_term {ps wps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → SymCC.wellTypedPolicies ps Γ = Except.ok wps → Except.ok cpset.term = SymCC.isAuthorized wps (SymCC.SymEnv.ofTypeEnv Γ)

theorem Cedar.Thm.cp_compile_produces_the_right_footprint {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → cp.footprint = SymCC.footprint cp.policy.toExpr cp.εnv

theorem Cedar.Thm.cpset_compile_produces_the_right_footprint {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → cpset.footprint = SymCC.footprints (List.map Spec.Policy.toExpr cpset.policies) cpset.εnv

theorem Cedar.Thm.cp_compile_produces_the_right_acyclicity {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → cp.acyclicity = Data.Set.map (fun (x : SymCC.Term) => SymCC.acyclicity x cp.εnv.entities) cp.footprint

theorem Cedar.Thm.cpset_compile_produces_the_right_acyclicity {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → cpset.acyclicity = Data.Set.map (fun (x : SymCC.Term) => SymCC.acyclicity x cpset.εnv.entities) cpset.footprint

theorem Cedar.Thm.flatMap_allPolicies_policy {cps : List SymCC.CompiledPolicy} : List.flatMap SymCC.CompiledPolicies.allPolicies (List.map SymCC.CompiledPolicies.policy cps) = List.map SymCC.CompiledPolicy.policy cps

theorem Cedar.Thm.flatMap_allPolicies_policies {cpsets : List SymCC.CompiledPolicySet} : List.flatMap SymCC.CompiledPolicies.allPolicies (List.map SymCC.CompiledPolicies.pset cpsets) = List.flatMap SymCC.CompiledPolicySet.policies cpsets