Lean model and proofs for batched-authorization

[john-h-kastner-aws]

Category

Lean formalization

Describe the feature you'd like to request

#836 added the model and proofs for the partial authorization algorithm and #725 added proofs for batched evaluation.

The Rust library also has has a batched authorization algorithm which is not modeled or proven correct.

https://github.com/cedar-policy/cedar/blob/b1611dcff61d3ba0a54f15c2f02bdfe4c9cfe190/cedar-policy-core/src/batched_evaluator.rs#L87

We should add a Lean model of this algorithm and prove that it is correct. Correctness theorem will be the same as for evaluation but showing that the authorization decision is the same rather than the result of evaluation.

Describe alternatives you've considered

.

Additional context

No response

Is this something that you'd be interested in working on?

• 👋 I may be able to implement this feature request
• ⚠️ This feature might incur a breaking change