Proofs that the optimized interface in SymCCOpt is equivalent to the unoptimized interface in SymCC.

theorem Cedar.Thm.satisfiedPolicies_eq_error {e : SymCC.Error} {effect : Spec.Effect} {ps : Spec.Policies} {εnv : SymCC.SymEnv} : SymCC.satisfiedPolicies effect ps εnv = Except.error e → ∃ (p : Spec.Policy), p ∈ ps ∧ SymCC.compile p.toExpr εnv = Except.error e

If SymCC.satisfiedPolicies fails, that must be because SymCC.compile failed with that error on some policy

theorem Cedar.Thm.isAuthorized_eq_error {e : SymCC.Error} {ps : Spec.Policies} {εnv : SymCC.SymEnv} : SymCC.isAuthorized ps εnv = Except.error e → ∃ (p : Spec.Policy), p ∈ ps ∧ SymCC.compile p.toExpr εnv = Except.error e

If SymCC.isAuthorized fails, that must be because SymCC.compile failed with that error on some policy

theorem Cedar.Thm.compile_ok_iff_welltypedpolicy_ok {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → ((SymCC.CompiledPolicy.compile p Γ).isOk = true ↔ (SymCC.wellTypedPolicy p Γ).isOk = true)

CompiledPolicy.compile succeeds iff wellTypedPolicy succeeds

Note: Γ.WellFormed is technically only required for the reverse direction

theorem Cedar.Thm.compile_ok_iff_welltypedpolicies_ok {ps : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → ((SymCC.CompiledPolicySet.compile ps Γ).isOk = true ↔ (SymCC.wellTypedPolicies ps Γ).isOk = true)

CompiledPolicySet.compile succeeds iff wellTypedPolicies succeeds

Note: Γ.WellFormed is technically only required for the reverse direction

theorem Cedar.Thm.compile_ok_then_exists_wtp {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp

If CompiledPolicy.compile succeeds, then wellTypedPolicy succeeds

Note: Can be proved without Γ.WellFormed

theorem Cedar.Thm.compile_ok_then_exists_wtps {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → ∃ (wps : Spec.Policies), SymCC.wellTypedPolicies ps Γ = Except.ok wps

If CompiledPolicySet.compile succeeds, then wellTypedPolicies succeeds

Note: Can be proved without Γ.WellFormed

theorem Cedar.Thm.cp_satAssertsOpt?_eqv_satAsserts?_ok {asserts : SymCC.Asserts} {ps wps : Spec.Policies} {cps : List SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : List.length ps = cps.length → cps ≠ [] → List.mapM (fun (x : Spec.Policy) => SymCC.CompiledPolicy.compile x Γ) ps = Except.ok cps → List.mapM (fun (x : Spec.Policy) => SymCC.wellTypedPolicy x Γ) ps = Except.ok wps → SymCC.satAsserts? wps asserts (SymCC.SymEnv.ofTypeEnv Γ) = SymCC.satAssertsOpt? (List.map SymCC.CompiledPolicies.policy cps) asserts

This theorem covers the "happy path" -- showing that if optimized policy compilation with CompiledPolicy.compile succeeds, then satAsserts? and satAssertsOpt? are equivalent.

theorem Cedar.Thm.cpset_satAssertsOpt?_eqv_satAsserts?_ok {asserts : SymCC.Asserts} {pss wpss : List Spec.Policies} {cpsets : List SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : pss.length = cpsets.length → cpsets ≠ [] → List.mapM (fun (x : Spec.Policies) => SymCC.CompiledPolicySet.compile x Γ) pss = Except.ok cpsets → List.mapM (fun (x : Spec.Policies) => SymCC.wellTypedPolicies x Γ) pss = Except.ok wpss → SymCC.satAsserts? wpss.flatten asserts (SymCC.SymEnv.ofTypeEnv Γ) = SymCC.satAssertsOpt? (List.map SymCC.CompiledPolicies.pset cpsets) asserts

This theorem covers the "happy path" -- showing that if optimized policy compilation with CompiledPolicySet.compile succeeds, then satAsserts? and satAssertsOpt? are equivalent.

theorem Cedar.Thm.neverErrorsOpt?_eqv_neverErrors?_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.neverErrorsOpt? cp = SymCC.neverErrors? wp (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and neverErrors? and neverErrorsOpt? are equivalent.

theorem Cedar.Thm.alwaysMatchesOpt?_eqv_alwaysMatches?_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.alwaysMatchesOpt? cp = SymCC.alwaysMatches? wp (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and alwaysMatches? and alwaysMatchesOpt? are equivalent.

theorem Cedar.Thm.neverMatchesOpt?_eqv_neverMatches?_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.neverMatchesOpt? cp = SymCC.neverMatches? wp (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and neverMatches? and neverMatchesOpt? are equivalent.

theorem Cedar.Thm.matchesEquivalentOpt?_eqv_matchesEquivalent?_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.matchesEquivalentOpt? cp₁ cp₂ = SymCC.matchesEquivalent? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and matchesEquivalent? and matchesEquivalentOpt? are equivalent.

theorem Cedar.Thm.matchesImpliesOpt?_eqv_matchesImplies?_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.matchesImpliesOpt? cp₁ cp₂ = SymCC.matchesImplies? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and matchesImplies? and matchesImpliesOpt? are equivalent.

theorem Cedar.Thm.matchesDisjointOpt?_eqv_matchesDisjoint?_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.matchesDisjointOpt? cp₁ cp₂ = SymCC.matchesDisjoint? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicy succeeds and matchesDisjoint? and matchesDisjointOpt? are equivalent.

theorem Cedar.Thm.neverErrorsOpt?_eqv_neverErrors? {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.neverErrorsOpt? cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.neverErrors? wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for neverErrors? and neverErrorsOpt?, including both the .ok and .error cases

theorem Cedar.Thm.alwaysMatchesOpt?_eqv_alwaysMatches? {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.alwaysMatchesOpt? cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.alwaysMatches? wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for alwaysMatches? and alwaysMatchesOpt?, including both the .ok and .error cases

theorem Cedar.Thm.neverMatchesOpt?_eqv_neverMatches? {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.neverMatchesOpt? cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.neverMatches? wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for neverMatches? and neverMatchesOpt?, including both the .ok and .error cases

theorem Cedar.Thm.matchesEquivalentOpt?_eqv_matchesEquivalent? {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.matchesEquivalentOpt? cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.matchesEquivalent? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for matchesEquivalent? and matchesEquivalentOpt?, including both the .ok and .error cases

theorem Cedar.Thm.matchesImpliesOpt?_eqv_matchesImplies? {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.matchesImpliesOpt? cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.matchesImplies? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for matchesImplies? and matchesImpliesOpt?, including both the .ok and .error cases

theorem Cedar.Thm.matchesDisjointOpt?_eqv_matchesDisjoint? {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.matchesDisjointOpt? cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.matchesDisjoint? wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for matchesDisjoint? and matchesDisjointOpt?, including both the .ok and .error cases

theorem Cedar.Thm.impliesOpt?_eqv_implies?_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.impliesOpt? cpset₁ cpset₂ = SymCC.implies? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and implies? and impliesOpt? are equivalent.

theorem Cedar.Thm.impliesOpt?_eqv_implies? {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.impliesOpt? cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.implies? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for implies? and impliesOpt?, including both the .ok and .error cases

theorem Cedar.Thm.alwaysAllowsOpt?_eqv_alwaysAllows?_ok {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → ∃ (wps : Spec.Policies), SymCC.wellTypedPolicies ps Γ = Except.ok wps ∧ SymCC.alwaysAllowsOpt? cpset = SymCC.alwaysAllows? wps (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and alwaysAllows? and alwaysAllowsOpt? are equivalent.

theorem Cedar.Thm.alwaysAllowsOpt?_eqv_alwaysAllows? {ps : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset ← SymCC.CompiledPolicySet.compile ps Γ pure (SymCC.alwaysAllowsOpt? cpset)) = do let wps ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps Γ) pure (SymCC.alwaysAllows? wps (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for alwaysAllows? and alwaysAllowsOpt?, including both the .ok and .error cases

theorem Cedar.Thm.alwaysDeniesOpt?_eqv_alwaysDenies?_ok {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → ∃ (wps : Spec.Policies), SymCC.wellTypedPolicies ps Γ = Except.ok wps ∧ SymCC.alwaysDeniesOpt? cpset = SymCC.alwaysDenies? wps (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and alwaysDenies? and alwaysDeniesOpt? are equivalent.

theorem Cedar.Thm.alwaysDeniesOpt?_eqv_alwaysDenies? {ps : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset ← SymCC.CompiledPolicySet.compile ps Γ pure (SymCC.alwaysDeniesOpt? cpset)) = do let wps ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps Γ) pure (SymCC.alwaysDenies? wps (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for alwaysDenies? and alwaysDeniesOpt?, including both the .ok and .error cases

theorem Cedar.Thm.equivalentOpt?_eqv_equivalent?_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.equivalentOpt? cpset₁ cpset₂ = SymCC.equivalent? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.equivalentOpt?_eqv_equivalent? {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.equivalentOpt? cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.equivalent? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for equivalent? and equivalentOpt?, including both the .ok and .error cases

theorem Cedar.Thm.disjointOpt?_eqv_disjoint?_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.disjointOpt? cpset₁ cpset₂ = SymCC.disjoint? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and disjoint? and disjointOpt? are equivalent.

theorem Cedar.Thm.disjointOpt?_eqv_disjoint? {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.disjointOpt? cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.disjoint? wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for disjoint? and disjointOpt?, including both the .ok and .error cases

theorem Cedar.Thm.checkNeverErrorsOpt_eqv_checkNeverErrors_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.checkNeverErrorsOpt cp = SymCC.checkNeverErrors wp (SymCC.SymEnv.ofTypeEnv Γ)

This theorem covers the "happy path" -- showing that if optimized policy compilation succeeds, then wellTypedPolicies succeeds and checkNeverErrors and checkNeverErrorsOpt? are equivalent.

theorem Cedar.Thm.checkAlwaysMatchesOpt_eqv_checkAlwaysMatches_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.checkAlwaysMatchesOpt cp = SymCC.checkAlwaysMatches wp (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkNeverMatchesOpt_eqv_checkNeverMatches_ok {p : Spec.Policy} {cp : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicy.compile p Γ = Except.ok cp → ∃ (wp : Spec.Policy), SymCC.wellTypedPolicy p Γ = Except.ok wp ∧ SymCC.checkNeverMatchesOpt cp = SymCC.checkNeverMatches wp (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkMatchesEquivalentOpt_eqv_checkMatchesEquivalent_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.checkMatchesEquivalentOpt cp₁ cp₂ = SymCC.checkMatchesEquivalent wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkMatchesImpliesOpt_eqv_checkMatchesImplies_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.checkMatchesImpliesOpt cp₁ cp₂ = SymCC.checkMatchesImplies wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkMatchesDisjointOpt_eqv_checkMatchesDisjoint_ok {p₁ p₂ wp₁ wp₂ : Spec.Policy} {cp₁ cp₂ : SymCC.CompiledPolicy} {Γ : Validation.TypeEnv} : Γ.WellFormed → 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.checkMatchesDisjointOpt cp₁ cp₂ = SymCC.checkMatchesDisjoint wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkNeverErrorsOpt_eqv_checkNeverErrors {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.checkNeverErrorsOpt cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.checkNeverErrors wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkNeverErrorsandcheckNeverErrorsOpt, including both the .okand.error` cases

theorem Cedar.Thm.checkAlwaysMatchesOpt_eqv_checkAlwaysMatches {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.checkAlwaysMatchesOpt cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.checkAlwaysMatches wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkAlwaysMatches and checkAlwaysMatchesOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkNeverMatchesOpt_eqv_checkNeverMatches {p : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp ← SymCC.CompiledPolicy.compile p Γ pure (SymCC.checkNeverMatchesOpt cp)) = do let wp ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p Γ) pure (SymCC.checkNeverMatches wp (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkNeverMatches and checkNeverMatchesOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkMatchesEquivalentOpt_eqv_checkMatchesEquivalent {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.checkMatchesEquivalentOpt cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.checkMatchesEquivalent wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkMatchesEquivalent and checkMatchesEquivalentOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkMatchesImpliesOpt_eqv_checkMatchesImplies {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.checkMatchesImpliesOpt cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.checkMatchesImplies wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkMatchesImplies and checkMatchesImpliesOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkMatchesDisjointOpt_eqv_checkMatchesDisjoint {p₁ p₂ : Spec.Policy} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cp₁ ← SymCC.CompiledPolicy.compile p₁ Γ let cp₂ ← SymCC.CompiledPolicy.compile p₂ Γ pure (SymCC.checkMatchesDisjointOpt cp₁ cp₂)) = do let wp₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₁ Γ) let wp₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicy p₂ Γ) pure (SymCC.checkMatchesDisjoint wp₁ wp₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkMatchesDisjoint and checkMatchesDisjointOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkImpliesOpt_eqv_checkImplies_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.checkImpliesOpt cpset₁ cpset₂ = SymCC.checkImplies wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkImpliesOpt_eqv_checkImplies {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.checkImpliesOpt cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.checkImplies wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkImplies and checkImpliesOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkAlwaysAllowsOpt_eqv_checkAlwaysAllows_ok {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → ∃ (wps : Spec.Policies), SymCC.wellTypedPolicies ps Γ = Except.ok wps ∧ SymCC.checkAlwaysAllowsOpt cpset = SymCC.checkAlwaysAllows wps (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkAlwaysAllowsOpt_eqv_checkAlwaysAllows {ps : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset ← SymCC.CompiledPolicySet.compile ps Γ pure (SymCC.checkAlwaysAllowsOpt cpset)) = do let wps ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps Γ) pure (SymCC.checkAlwaysAllows wps (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkAlwaysAllows and checkAlwaysAllowsOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkAlwaysDeniesOpt_eqv_checkAlwaysDenies_ok {ps : Spec.Policies} {cpset : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps Γ = Except.ok cpset → ∃ (wps : Spec.Policies), SymCC.wellTypedPolicies ps Γ = Except.ok wps ∧ SymCC.checkAlwaysDeniesOpt cpset = SymCC.checkAlwaysDenies wps (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkAlwaysDeniesOpt_eqv_checkAlwaysDenies {ps : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset ← SymCC.CompiledPolicySet.compile ps Γ pure (SymCC.checkAlwaysDeniesOpt cpset)) = do let wps ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps Γ) pure (SymCC.checkAlwaysDenies wps (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkAlwaysDenies and checkAlwaysDeniesOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkEquivalentOpt_eqv_checkEquivalent_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.checkEquivalentOpt cpset₁ cpset₂ = SymCC.checkEquivalent wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkEquivalentOpt_eqv_checkEquivalent {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.checkEquivalentOpt cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.checkEquivalent wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkEquivalent and checkEquivalentOpt, including both the .ok and .error cases

theorem Cedar.Thm.checkDisjointOpt_eqv_checkDisjoint_ok {ps₁ ps₂ : Spec.Policies} {cpset₁ cpset₂ : SymCC.CompiledPolicySet} {Γ : Validation.TypeEnv} : Γ.WellFormed → SymCC.CompiledPolicySet.compile ps₁ Γ = Except.ok cpset₁ → SymCC.CompiledPolicySet.compile ps₂ Γ = Except.ok cpset₂ → ∃ (wps₁ : Spec.Policies), ∃ (wps₂ : Spec.Policies), SymCC.wellTypedPolicies ps₁ Γ = Except.ok wps₁ ∧ SymCC.wellTypedPolicies ps₂ Γ = Except.ok wps₂ ∧ SymCC.checkDisjointOpt cpset₁ cpset₂ = SymCC.checkDisjoint wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ)

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

theorem Cedar.Thm.checkDisjointOpt_eqv_checkDisjoint {ps₁ ps₂ : Spec.Policies} {Γ : Validation.TypeEnv} : Γ.WellFormed → (do let cpset₁ ← SymCC.CompiledPolicySet.compile ps₁ Γ let cpset₂ ← SymCC.CompiledPolicySet.compile ps₂ Γ pure (SymCC.checkDisjointOpt cpset₁ cpset₂)) = do let wps₁ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₁ Γ) let wps₂ ← Except.mapError SymCC.CompiledPolicyError.validationError (SymCC.wellTypedPolicies ps₂ Γ) pure (SymCC.checkDisjoint wps₁ wps₂ (SymCC.SymEnv.ofTypeEnv Γ))

Full equivalence for checkDisjoint and checkDisjointOpt, including both the .ok and .error cases