Proofs that the optimized functions in SymCCOpt.Enforcer are equivalent to the unoptimized ones in SymCC.Enforcer.

theorem Cedar.Thm.enforce_eq_map_union {xs : List Spec.Expr} {εnv : SymCC.SymEnv} : SymCC.enforce xs εnv = Data.Set.map (fun (x : SymCC.Term) => SymCC.acyclicity x εnv.entities) (SymCC.footprints xs εnv) ∪ Data.Set.map (fun (x : SymCC.Term × SymCC.Term) => match x with | (t₁, t₂) => SymCC.transitivity t₁ t₂ εnv.entities) ((SymCC.footprints xs εnv).product (SymCC.footprints xs εnv))

Rephrases the unoptimized enforce as the union of the acyclicity and transitivity constraints using the Set.map/Set.product/∪ operations that the optimized enforce*CompiledPolicy* functions are defined with.

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

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then enforce and enforceCompiledPolicy are equivalent.

theorem Cedar.Thm.enforcePairCompiledPolicy_eqv_enforce_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p₁ Γ = Except.ok cp₁ → SymCC.CompiledPolicy.compile p₂ Γ = Except.ok cp₂ → SymCC.wellTypedPolicy p₁ Γ = Except.ok wp₁ → SymCC.wellTypedPolicy p₂ Γ = Except.ok wp₂ → SymCC.enforce [wp₁.toExpr, wp₂.toExpr] (SymCC.SymEnv.ofTypeEnv Γ) = SymCC.enforcePairCompiledPolicy cp₁ cp₂

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then enforce and enforcePairCompiledPolicy are equivalent.

theorem Cedar.Thm.enforcePairCompiledPolicySet_eqv_enforce_ok {ps₁ ps₂ wps₁ wps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ → SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ → SymCC.enforce (List.map Spec.Policy.toExpr wps₁ ++ List.map Spec.Policy.toExpr wps₂) (SymCC.SymEnv.ofTypeEnv Γ) = SymCC.enforcePairCompiledPolicySet cpset₁ cpset₂

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then enforce and enforcePairCompiledPolicySet are equivalent.