Documentation

Cedar.Thm.BatchedEvaluator

This file defines theorems related to the batched evaluator

source
@[reducible, inline]
abbrev Cedar.Thm.EntityLoader.WellBehaved (store : Spec.Entities) (loader : TPE.EntityLoader) :
Prop

A well behaved entity loader

  1. Loads all the requested entities, returning none for missing entities
  2. Refines the backing entity store

The first condition is required for convergence of batched evaluation, which has not been proven. It is unused in the code base at the moment.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cedar.Thm.as_partial_request_refines {req : Spec.Request} :
    RequestRefines req req.asPartialRequest
    source
    theorem Cedar.Thm.any_refines_empty_entities {es : Spec.Entities} :
    EntitiesRefine es Data.Map.empty
    source
    theorem Cedar.Thm.entities_refine_append (es : Spec.Entities) (m1 m2 : TPE.PartialEntities) :
    EntitiesRefine es m1 → EntitiesRefine es m2 → EntitiesRefine es (m2 ++ m1)
    source
    theorem Cedar.Thm.direct_request_and_entities_refine (req : Spec.Request) (es : Spec.Entities) :
    RequestAndEntitiesRefine req es req.asPartialRequest es.asPartial
    source
    @[irreducible]
    theorem Cedar.Thm.batched_eval_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.batchedEvalLoop x req loader current_store iters).evaluate req es) = Except.toOption (x.evaluate req es)
    source
    theorem Cedar.Thm.batched_eval_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 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.