This file proves the soundness and completeness of the verification queries in Cedar.SymCC.Verifier, which are based on Cedar's reduction to SMT. For soundness, we show that if the result of a query is unsatisfiable, then the property checked by the query holds for all strongly well-formed concrete environments env that are represented by a given strongly well-formed symbolic environment εnv. For completeness, we show that if the result of the query is satisfiable, then there is a strongly-well formed concrete environment env represented by εnv for which the queried property is violated.

An environment is strongly well-formed if (1) it is free of dangling entity references, and (2) its ancestor relation is the transitive closure of a DAG. Cedar verification queries (dis)prove properties with respect to strongly well-formed environments.

theorem Cedar.Thm.verifyNeverErrors_is_sound {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverErrors p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → Except.isOk (Spec.evaluate p.toExpr env.request env.entities) = true

The verifyNeverError analysis is sound: if the assertions verifyNeverErrors p εnv are unsatisfiable for the policy p and the strongly well-formed symbolic environment εnv, then the evaluator will not error when applied to p and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyNeverErrors_is_complete {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverErrors p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬Except.isOk (Spec.evaluate p.toExpr env.request env.entities) = true

The verifyNeverError analysis is complete: if the assertions verifyNeverErrors p εnv are satisfiable for the policy p and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the evaluator will error when applied to p and env.

theorem Cedar.Thm.verifyAlwaysMatches_is_sound {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyAlwaysMatches p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → Spec.evaluate p.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyAlwaysMatches analysis is sound: if the assertions verifyAlwaysMatches p εnv are unsatisfiable for the policy p and the strongly well-formed symbolic environment εnv, then the evaluator will return .ok true when applied to p and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyAlwaysMatches_is_sound' {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyAlwaysMatches p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies

Alternate definition of soundness for alwaysMatches:

For a singleton policyset, if symcc says the policy alwaysMatches, then the spec authorizer should say it always appears in determiningPolicies

theorem Cedar.Thm.verifyAlwaysMatches_is_complete {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyAlwaysMatches p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ Spec.evaluate p.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyAlwaysMatches analysis is complete: if the assertions verifyAlwaysMatches p εnv are satisfiable for the policy p and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the evaluator will not return .ok true when applied to p and env.

theorem Cedar.Thm.verifyAlwaysMatches_is_complete' {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyAlwaysMatches p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies

Alternate definition of completeness for alwaysMatches:

For a singleton policyset, if symcc says the policy does not alwaysMatch, then there exists a concrete environment where the policy does not appear in determiningPolicies.

theorem Cedar.Thm.verifyNeverMatches_is_sound {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverMatches p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → Spec.evaluate p.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyNeverMatches analysis is sound: if the assertions verifyNeverMatches p εnv are unsatisfiable for the policy p and the strongly well-formed symbolic environment εnv, then the evaluator will never return .ok true when applied to p and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyNeverMatches_is_sound' {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverMatches p εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p → ¬p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies

Alternate definition of soundness for neverMatches:

For a singleton policyset, if symcc says the policy neverMatches, then the spec authorizer should say it never appears in determiningPolicies.

theorem Cedar.Thm.verifyNeverMatches_is_complete {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverMatches p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ Spec.evaluate p.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyNeverMatches analysis is complete: if the assertions verifyNeverMatches p εnv are satisfiable for the policy p and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the evaluator will return .ok true when applied to p and env.

theorem Cedar.Thm.verifyNeverMatches_is_complete' {p : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p → SymCC.verifyNeverMatches p εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p ∧ SymCC.Env.EnumCompleteFor env εnv ∧ p.id ∈ (Spec.isAuthorized env.request env.entities [p]).determiningPolicies

Alternate definition of completeness for neverMatches:

For a singleton policyset, if symcc says the policy does not neverMatch, then there exists a concrete environment where the policy appears in determiningPolicies.

theorem Cedar.Thm.verifyMatchesEquivalent_is_sound {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesEquivalent p₁ p₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p₁ → env.StronglyWellFormedForPolicy p₂ → (Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))) = (Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

The verifyMatchesEquivalent analysis is sound: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies will have the same matching behavior (both match or both don't match) when applied to any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyMatchesEquivalent_is_complete {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesEquivalent p₁ p₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p₁ ∧ env.StronglyWellFormedForPolicy p₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ (Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))) ≠ (Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

The verifyMatchesEquivalent analysis is complete: if the assertions verifyMatchesEquivalent p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the policies will have different matching behavior (one matches and the other doesn't) when applied to env.

theorem Cedar.Thm.verifyMatchesImplies_is_sound {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesImplies p₁ p₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p₁ → env.StronglyWellFormedForPolicy p₂ → Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) → Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyMatchesImplies analysis is sound: if the assertions verifyMatchesImplies p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then if p₁ matches in any strongly well-formed concrete environment env ∈ᵢ εnv, then p₂ also matches.

theorem Cedar.Thm.verifyMatchesImplies_is_complete {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesImplies p₁ p₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p₁ ∧ env.StronglyWellFormedForPolicy p₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities ≠ Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyMatchesImplies analysis is complete: if the assertions verifyMatchesImplies p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that p₁ matches but p₂ does not match in env.

theorem Cedar.Thm.verifyMatchesDisjoint_is_sound {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesDisjoint p₁ p₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicy p₁ → env.StronglyWellFormedForPolicy p₂ → ¬(Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)))

The verifyMatchesDisjoint analysis is sound: if the assertions verifyMatchesDisjoint p₁ p₂ εnv are unsatisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then the policies cannot both match in any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyMatchesDisjoint_is_complete {p₁ p₂ : Spec.Policy} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicy p₁ → εnv.StronglyWellFormedForPolicy p₂ → SymCC.verifyMatchesDisjoint p₁ p₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicy p₁ ∧ env.StronglyWellFormedForPolicy p₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ Spec.evaluate p₁.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true)) ∧ Spec.evaluate p₂.toExpr env.request env.entities = Except.ok (Spec.Value.prim (Spec.Prim.bool true))

The verifyMatchesDisjoint analysis is complete: if the assertions verifyMatchesDisjoint p₁ p₂ εnv are satisfiable for the policies p₁ and p₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that both policies match in env.

theorem Cedar.Thm.verifyEquivalent_is_sound {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyEquivalent ps₁ ps₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → env.StronglyWellFormedForPolicies ps₂ → bothAllowOrBothDeny (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyEquivalent analysis is sound: if the assertions verifyEquivalent ps₁ ps₂ εnv are unsatisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then the authorizer will produce the same authorization decision when applied to ps₁, ps₂, and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyEquivalent_is_complete {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyEquivalent ps₁ ps₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ env.StronglyWellFormedForPolicies ps₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬bothAllowOrBothDeny (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyEquivalent analysis is complete: if the assertions verifyEquivalent ps₁ ps₂ εnv are satisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will produce different authorization decisions when applied to ps₁, ps₂, and env.

theorem Cedar.Thm.verifyDisjoint_is_sound {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyDisjoint ps₁ ps₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → env.StronglyWellFormedForPolicies ps₂ → atLeastOneDenies (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyDisjoint analysis is sound: if the assertions verifyDisjoint ps₁ ps₂ εnv are unsatisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then the authorizer will not produce two allow decisions when applied to ps₁, ps₂, and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyDisjoint_is_complete {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyDisjoint ps₁ ps₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ env.StronglyWellFormedForPolicies ps₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬atLeastOneDenies (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyDisjoint analysis is complete: if the assertions verifyDisjoint ps₁ ps₂ εnv are satisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will produce two allow decisions when applied to ps₁, ps₂, and env.

theorem Cedar.Thm.verifyImplies_is_sound {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyImplies ps₁ ps₂ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → env.StronglyWellFormedForPolicies ps₂ → ifFirstAllowsSoDoesSecond (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyImplies analysis is sound: if the assertions verifyImplies ps₁ ps₂ εnv are unsatisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then if the authorizer returns allow for ps₁, it also returns allow for ps₂ in any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyImplies_is_complete {ps₁ ps₂ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → εnv.StronglyWellFormedForPolicies ps₂ → SymCC.verifyImplies ps₁ ps₂ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ env.StronglyWellFormedForPolicies ps₂ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬ifFirstAllowsSoDoesSecond (Spec.isAuthorized env.request env.entities ps₁) (Spec.isAuthorized env.request env.entities ps₂) = true

The verifyImplies analysis is complete: if the assertions verifyImplies ps₁ ps₂ εnv are satisfiable for the policies ps₁ and ps₂ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will produce allow for ps₁ but deny for ps₂ in env.

theorem Cedar.Thm.verifyAlwaysDenies_is_sound {ps₁ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → SymCC.verifyAlwaysDenies ps₁ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → denies (Spec.isAuthorized env.request env.entities ps₁) = true

The verifyAlwaysDenies analysis is sound: if the assertions verifyAlwaysDenies ps₁ εnv are unsatisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then the authorizer will return deny when applied to ps₁ and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyAlwaysDenies_is_complete {ps₁ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → SymCC.verifyAlwaysDenies ps₁ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬denies (Spec.isAuthorized env.request env.entities ps₁) = true

The verifyAlwaysDenies analysis is sound: if the assertions verifyAlwaysDenies ps₁ εnv are satisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will not return deny when applied to ps₁ and env.

theorem Cedar.Thm.verifyAlwaysAllows_is_sound {ps₁ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → SymCC.verifyAlwaysAllows ps₁ εnv = Except.ok asserts → εnv ⊭ asserts → ∀ (env : Spec.Env), env∈ᵢεnv → env.StronglyWellFormedForPolicies ps₁ → allows (Spec.isAuthorized env.request env.entities ps₁) = true

The verifyAlwaysAllows analysis is sound: if the assertions verifyAlwaysAllows ps₁ εnv are unsatisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then the authorizer will return allow when applied to ps₁ and any strongly well-formed concrete environment env ∈ᵢ εnv.

theorem Cedar.Thm.verifyAlwaysAllows_is_complete {ps₁ : Spec.Policies} {εnv : SymCC.SymEnv} {asserts : SymCC.Asserts} : εnv.StronglyWellFormedForPolicies ps₁ → SymCC.verifyAlwaysAllows ps₁ εnv = Except.ok asserts → εnv ⊧ asserts → ∃ (env : Spec.Env), env∈ᵢεnv ∧ env.StronglyWellFormedForPolicies ps₁ ∧ SymCC.Env.EnumCompleteFor env εnv ∧ ¬allows (Spec.isAuthorized env.request env.entities ps₁) = true

The verifyAlwaysAllows analysis is sound: if the assertions verifyAlwaysAllows ps₁ εnv are satisfiable for the policies ps₁ and the strongly well-formed symbolic environment εnv, then there exists a strongly well-formed concrete environment env ∈ᵢ εnv such that the authorizer will not return allow when applied to ps₁ and env.