Soundness of batched expression evaluation: batched evaluation of a single well-typed residual produces the same result as direct evaluation with the complete entity store.

theorem Cedar.Thm.batched_evaluate_loop_eq_evaluate {loader : TPE.EntityLoader} {iters : Nat} {x : Spec.Residual} {req : Spec.Request} (es : Spec.Entities) {current_store : TPE.PartialEntities} {env : Validation.TypeEnv} : EntityLoader.WellBehaved es loader → Residual.WellTyped env x → RequestAndEntitiesRefine req es req.asPartialRequest current_store → InstanceOfWellFormedEnvironment req es env → Except.toOption ((TPE.batchedEvaluateLoop env x req loader current_store iters).evaluate req es) = Except.toOption (x.evaluate req es)