Documentation

Cedar.Thm.BatchedEvaluator.Common

Shared definitions and lemmas for batched evaluator theorems.

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.environment?_schema {schema : Validation.Schema} {pty rty : Spec.EntityType} {act : Spec.EntityUID} {env : Validation.TypeEnv} (h : schema.environment? pty rty act = some env) :
    env.ets = schema.ets ∧ env.acts = schema.acts

    Schema.environment? carries the schema's entity and action types through unchanged.

    source
    theorem Cedar.Thm.actionEntities_refines {env : Validation.TypeEnv} {es : Spec.Entities} (hwf : env.WellFormed) (hinst : InstanceOfSchema es env) :
    EntitiesRefine es (TPE.actionEntities env.acts)
    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