theorem
Cedar.Thm.slice_at_level_inner_well_formed
{entities : Spec.Entities}
{work : Data.Set Spec.EntityUID}
{n : Nat}
:
(Spec.Entities.sliceAtLevel.sliceAtLevel entities work n).WellFormed
theorem
Cedar.Thm.checked_eval_entity_in_slice
{request : Spec.Request}
{e : Spec.Expr}
{nmax : Nat}
{euid : Spec.EntityUID}
{n : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{entities : Spec.Entities}
{ed : Spec.EntityData}
(hc : CapabilitiesInvariant c request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf e c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax [])
(he : Spec.evaluate e request entities = Except.ok (Spec.Value.prim (Spec.Prim.entityUID euid)))
(hf : Data.Map.find? entities euid = some ed)
:
theorem
Cedar.Thm.not_entities_then_not_slice
{n : Nat}
{request : Spec.Request}
{uid : Spec.EntityUID}
{entities : Spec.Entities}
(hse : Data.Map.find? entities uid = none)
:
theorem
Cedar.Thm.checked_eval_entity_find_entities_eq_find_slice
{request : Spec.Request}
{e : Spec.Expr}
{euid : Spec.EntityUID}
{n nmax : Nat}
{c c' : Validation.Capabilities}
{tx : Validation.TypedExpr}
{env : Validation.TypeEnv}
{entities : Spec.Entities}
(hc : CapabilitiesInvariant c request entities)
(hr : InstanceOfWellFormedEnvironment request entities env)
(ht : Validation.typeOf e c env = Except.ok (tx, c'))
(hl : Validation.TypedExpr.EntityAccessAtLevel env tx n nmax [])
(he : Spec.evaluate e request entities = Except.ok (Spec.Value.prim (Spec.Prim.entityUID euid)))
:
If an expression checks at level n and then evaluates to an entity, then the
data for that entity in the slice will be the same as in the original entities.