verify* functions always succeed on well-formed inputs. -

theorem Cedar.Thm.verifyEvaluate_is_ok {φ : SymCC.Term → SymCC.Term} {p p' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') : ∃ (asserts : SymCC.Asserts), SymCC.verifyEvaluate φ p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyEvaluate succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyEvaluatePair_is_ok {φ : SymCC.Term → SymCC.Term → SymCC.Term} {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁') (hwt₂ : SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyEvaluatePair φ p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyEvaluatePair succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.compileWithEffect_is_ok (effect : Spec.Effect) {p p' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') : ∃ (asserts : Option SymCC.Term), SymCC.compileWithEffect effect p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

compileWithEffect succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.satisfiedPolicies_is_ok (effect : Spec.Effect) {ps ps' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') : ∃ (asserts : SymCC.Term), SymCC.satisfiedPolicies effect ps' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

satisfiedPolicies succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.isAuthorized_is_ok {ps ps' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') : ∃ (asserts : SymCC.Term), SymCC.isAuthorized ps' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

isAuthorized succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyIsAuthorized_is_ok (φ : SymCC.Term → SymCC.Term → SymCC.Term) {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁') (hwt₂ : SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyIsAuthorized φ ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyIsAuthorized succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyNeverErrors_is_ok {p p' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') : ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverErrors p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyNeverErrors succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyAlwaysMatches_is_ok {p p' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') : ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyAlwaysMatches succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyNeverMatches_is_ok {p p' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicy p Γ = Except.ok p') : ∃ (asserts : SymCC.Asserts), SymCC.verifyNeverMatches p' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyNeverMatches succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyMatchesEquivalent_is_ok {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁') (hwt₂ : SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesEquivalent p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyMatchesEquivalent succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyMatchesImplies_is_ok {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁') (hwt₂ : SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesImplies p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyMatchesImplies succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyMatchesDisjoint_is_ok {p₁ p₁' p₂ p₂' : Spec.Policy} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicy p₁ Γ = Except.ok p₁') (hwt₂ : SymCC.wellTypedPolicy p₂ Γ = Except.ok p₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyMatchesDisjoint p₁' p₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyMatchesDisjoint succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyImplies_is_ok {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁') (hwt₂ : SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyImplies ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyImplies succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.isAuthorized_allowAll_is_ok (Γ : Validation.TypeEnv) : SymCC.isAuthorized [SymCC.verifyAlwaysAllows.allowAll] (SymCC.SymEnv.ofEnv Γ) = Except.ok (SymCC.Term.prim (SymCC.TermPrim.bool true))

theorem Cedar.Thm.verifyAlwaysAllows_is_ok {ps ps' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') : ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysAllows ps' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyAlwaysAllows succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyAlwaysDenies_is_ok {ps ps' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt : SymCC.wellTypedPolicies ps Γ = Except.ok ps') : ∃ (asserts : SymCC.Asserts), SymCC.verifyAlwaysDenies ps' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyAlwaysDenies succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyEquivalent_is_ok {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁') (hwt₂ : SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyEquivalent ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyEquivalent succeeds on sufficiently well-formed inputs.

theorem Cedar.Thm.verifyDisjoint_is_ok {ps₁ ps₁' ps₂ ps₂' : Spec.Policies} {Γ : Validation.TypeEnv} (hwf : Γ.WellFormed) (hwt₁ : SymCC.wellTypedPolicies ps₁ Γ = Except.ok ps₁') (hwt₂ : SymCC.wellTypedPolicies ps₂ Γ = Except.ok ps₂') : ∃ (asserts : SymCC.Asserts), SymCC.verifyDisjoint ps₁' ps₂' (SymCC.SymEnv.ofEnv Γ) = Except.ok asserts

verifyDisjoint succeeds on sufficiently well-formed inputs.