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

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.