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.