This file defines the main theorems for batched authorization and evaluation.
theorem
Cedar.Thm.batched_evaluate_eq_evaluate
{loader : TPE.EntityLoader}
{iters : Nat}
{x : Validation.TypedExpr}
{req : Spec.Request}
{es : Spec.Entities}
{env : Validation.TypeEnv}
:
EntityLoader.WellBehaved es loader →
TypedExpr.WellTyped env x →
InstanceOfWellFormedEnvironment req es env →
Except.toOption ((TPE.batchedEvaluate env x req loader iters).evaluate req es) = Except.toOption (Spec.evaluate x.toExpr req es)
The main correctness theorem for batched evaluation: Batched evaluation with an entity loader produces the same result as normal evaluation with the complete entity store.
theorem
Cedar.Thm.batched_authorize_ok_equiv
{loader : TPE.EntityLoader}
{iters : Nat}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{response : TPE.Response}
:
EntityLoader.WellBehaved es loader →
schema.validateWellFormed = Except.ok () →
Validation.validateEntities schema es = Except.ok () →
TPE.batchedAuthorize schema policies req loader iters = Except.ok response →
∃ (rps : List TPE.ResidualPolicy), response = TPE.isAuthorizedFromResiduals rps ∧ ResidualPoliciesEquiv policies rps req es
A successful batched authorization returns isAuthorizedFromResiduals of a list equivalent to the
policies, so any property of it transfers to the batched path without a second induction.
theorem
Cedar.Thm.batched_authorize_decision_eq_authorize
{loader : TPE.EntityLoader}
{iters : Nat}
{schema : Validation.Schema}
{policies : List Spec.Policy}
{req : Spec.Request}
{es : Spec.Entities}
{response : TPE.Response}
{d : Spec.Decision}
:
EntityLoader.WellBehaved es loader →
schema.validateWellFormed = Except.ok () →
Validation.validateEntities schema es = Except.ok () →
TPE.batchedAuthorize schema policies req loader iters = Except.ok response →
response.decision = some d → (Spec.isAuthorized req es policies).decision = d
The main correctness theorem for batched authorization: If the batched authorizer reaches a definitive decision, that decision agrees with the concrete authorizer.