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

theorem Cedar.Thm.verifyEvaluateOpt_eqv_verifyEvaluate_ok {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} {φ : SymCC.Term → SymCC.Term} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → SymCC.verifyEvaluate φ wp (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyEvaluateOpt φ cp)

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

theorem Cedar.Thm.verifyEvaluatePairOpt_eqv_verifyEvaluatePair_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} {φ : SymCC.Term → SymCC.Term → SymCC.Term} : 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.verifyEvaluatePair φ wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyEvaluatePairOpt φ cp₁ cp₂)

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

theorem Cedar.Thm.verifyIsAuthorizedOpt_eqv_verifyIsAuthorized_ok {ps₁ ps₂ wps₁ wps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} {φ : SymCC.Term → SymCC.Term → SymCC.Term} : 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.verifyIsAuthorized φ wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyIsAuthorizedOpt φ cpset₁ cpset₂)

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

theorem Cedar.Thm.verifyNeverErrorsOpt_eqv_verifyNeverErrors_ok {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → SymCC.verifyNeverErrors wp (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyNeverErrorsOpt cp)

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

theorem Cedar.Thm.verifyAlwaysMatchesOpt_eqv_verifyAlwaysMatches_ok {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → SymCC.verifyAlwaysMatches wp (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyAlwaysMatchesOpt cp)

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

theorem Cedar.Thm.verifyNeverMatchesOpt_eqv_verifyNeverMatches_ok {p wp : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicy.compile p Γ = Except.ok cp → SymCC.wellTypedPolicy p Γ = Except.ok wp → SymCC.verifyNeverMatches wp (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyNeverMatchesOpt cp)

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

theorem Cedar.Thm.verifyMatchesEquivalentOpt_eqv_verifyMatchesEquivalent_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.verifyMatchesEquivalent wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyMatchesEquivalentOpt cp₁ cp₂)

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

theorem Cedar.Thm.verifyMatchesImpliesOpt_eqv_verifyMatchesImplies_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.verifyMatchesImplies wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyMatchesImpliesOpt cp₁ cp₂)

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

theorem Cedar.Thm.verifyMatchesDisjointOpt_eqv_verifyMatchesDisjoint_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.verifyMatchesDisjoint wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyMatchesDisjointOpt cp₁ cp₂)

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

theorem Cedar.Thm.verifyImpliesOpt_eqv_verifyImplies_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.verifyImplies wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyImpliesOpt cpset₁ cpset₂)

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

theorem Cedar.Thm.verifyAlwaysAllowsOpt_eqv_verifyAlwaysAllows_ok {ps wps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → SymCC.wellTypedPolicies ps Γ = Except.ok wps → SymCC.verifyAlwaysAllows wps (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyAlwaysAllowsOpt cpset)

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

theorem Cedar.Thm.verifyAlwaysDeniesOpt_eqv_verifyAlwaysDenies_ok {ps wps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → SymCC.wellTypedPolicies ps Γ = Except.ok wps → SymCC.verifyAlwaysDenies wps (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyAlwaysDeniesOpt cpset)

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

theorem Cedar.Thm.verifyEquivalentOpt_eqv_verifyEquivalent_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.verifyEquivalent wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyEquivalentOpt cpset₁ cpset₂)

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

theorem Cedar.Thm.verifyDisjointOpt_eqv_verifyDisjoint_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.verifyDisjoint wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ) ~ Except.ok (SymCC.verifyDisjointOpt cpset₁ cpset₂)

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