This file contains the top-level correctness properties for the Cedar validator. We show that if validation succeeds for a set of policies, then for any request consistent with the schema, evaluating a policy in this set either produces a boolean value, or throws one of the errors in the set of valid errors.

theorem Cedar.Thm.validation_is_sound (policies : Spec.Policies) (schema : Validation.Schema) (request : Spec.Request) (entities : Spec.Entities) : schema.validateWellFormed = Except.ok () → Validation.validate policies schema = Except.ok () → Validation.validateRequest schema request = Except.ok () → Validation.validateEntities schema entities = Except.ok () → AllEvaluateToBool policies request entities

If a set of policies is well-typed (valid) with respect to the schema according to the validator, and the input request and entities are consistent with the schema, then evaluating a policy in this set either produces a boolean value, or throws an error of type entityDoesNotExist, extensionError, or arithBoundsError. These errors cannot be protected against at validation time, as they depend on runtime information.

theorem Cedar.Thm.validate_with_level_is_sound {ps : Spec.Policies} {schema : Validation.Schema} {n : Nat} {request : Spec.Request} {entities : Spec.Entities} (hwf : schema.validateWellFormed = Except.ok ()) (hr : Validation.validateRequest schema request = Except.ok ()) (he : Validation.validateEntities schema entities = Except.ok ()) (htl : Validation.validateWithLevel ps schema n = Except.ok ()) : Spec.isAuthorized request entities ps = Spec.isAuthorized request (entities.sliceAtLevel request n) ps

If a set of policies is well-typed and validates at a level n, then any authorization request made using a slice of entities obtained by slicing at level n will return the same response as authorizing using the original entities.

theorem Cedar.Thm.validate_with_level_no_dne {ps : Spec.Policies} {schema : Validation.Schema} {n : Nat} {request : Spec.Request} {entities : Spec.Entities} (hwf : schema.validateWellFormed = Except.ok ()) (hr : Validation.validateRequest schema request = Except.ok ()) (he : Validation.validateEntities schema entities = Except.ok ()) (hcl : entities.closedAtLevel request n = true) (htl : Validation.validateWithLevel ps schema n = Except.ok ()) (p : Spec.Policy) : p ∈ ps → Spec.evaluate p.toExpr request entities ≠ Except.error Spec.Error.entityDoesNotExist

End-to-end statement of issue #642 for a validated policy set, phrased over the executable closure check Entities.closedAtLevel: if ps validates at level n and the store passes entities.closedAtLevel request n, then no policy evaluates to entityDoesNotExist. These are exactly the evaluations isAuthorized performs, so this is the per-policy guarantee isAuthorized inherits: the authorizer surfaces evaluation results only through the kind-agnostic errorPolicies / satisfiedPolicies and never raises entityDoesNotExist of its own. Mirrors validate_with_level_is_sound, with the runtime closure obligation discharged by running Entities.closedAtLevel (closedAtLevel_iff bridges it to the EntitiesClosedAtLevel predicate).

theorem Cedar.Thm.error_of_mem_erroringPolicies {ps : Spec.Policies} {request : Spec.Request} {entities : Spec.Entities} {pid : Spec.PolicyID} (h : pid ∈ (Spec.isAuthorized request entities ps).erroringPolicies) : ∃ (p : Spec.Policy), p ∈ ps ∧ p.id = pid ∧ ∃ (e : Spec.Error), Spec.evaluate p.toExpr request entities = Except.error e

Bridge from Response.erroringPolicies membership back to the evaluator: if a policy id appears in the erroring set produced by isAuthorized, then some policy in ps with that id genuinely errored on evaluation. Because policy ids need not be unique, this recovers a policy with the id, not necessarily a specific one.

theorem Cedar.Thm.validate_with_level_no_dne_response {ps : Spec.Policies} {schema : Validation.Schema} {n : Nat} {request : Spec.Request} {entities : Spec.Entities} (hwf : schema.validateWellFormed = Except.ok ()) (hr : Validation.validateRequest schema request = Except.ok ()) (he : Validation.validateEntities schema entities = Except.ok ()) (hcl : entities.closedAtLevel request n = true) (htl : Validation.validateWithLevel ps schema n = Except.ok ()) (p : Spec.Policy) : p ∈ ps → p.id ∈ (Spec.isAuthorized request entities ps).erroringPolicies → Spec.evaluate p.toExpr request entities ≠ Except.error Spec.Error.entityDoesNotExist

Response-level form of validate_with_level_no_dne (issue #642): for a policy set that validates at level n over a store closed at that level, no policy in the authorizer's erroringPolicies errored with entityDoesNotExist. The erroringPolicies membership premise is not needed for soundness — no policy evaluates to entityDoesNotExist at all (validate_with_level_no_dne) — but it phrases the guarantee at the isAuthorized Response level.

theorem Cedar.Thm.validation_is_sound_response (policies : Spec.Policies) (schema : Validation.Schema) (request : Spec.Request) (entities : Spec.Entities) (huniq : PolicyIdsUnique policies) (hwf : schema.validateWellFormed = Except.ok ()) (hv : Validation.validate policies schema = Except.ok ()) (hr : Validation.validateRequest schema request = Except.ok ()) (he : Validation.validateEntities schema entities = Except.ok ()) (p : Spec.Policy) : p ∈ policies → p.id ∈ (Spec.isAuthorized request entities policies).erroringPolicies → Spec.evaluate p.toExpr request entities = Except.error Spec.Error.entityDoesNotExist ∨ Spec.evaluate p.toExpr request entities = Except.error Spec.Error.extensionError ∨ Spec.evaluate p.toExpr request entities = Except.error Spec.Error.arithBoundsError

Response-level form of validation_is_sound: for a validated policy set with unique policy ids, every policy in the authorizer's erroringPolicies errored with one of the three errors validation cannot rule out (entityDoesNotExist, extensionError, arithBoundsError). Uniqueness of ids (PolicyIdsUnique, as in determining_erroring_disjoint_when_unique_ids) is required: an id in erroringPolicies only witnesses that some policy with that id errored, so without uniqueness it need not be the policy p quantified over.