Level checking rules out entityDoesNotExist errors (issue #642) #
level_based_slicing_is_sound_expr already proves that evaluating against the
full store agrees with evaluating against the level-n slice. Issue #642 asks
for the additional guarantee that a level-checked, well-typed expression never
produces Error.entityDoesNotExist at all, given a store that is closed up to
that level.
Note this is genuinely a NEW hypothesis, not a consequence of well-formedness:
InstanceOfSchema (Typechecker/Types.lean) only constrains entries that are
present in the store; nothing forces an entity-typed attribute value to point
at a uid that is itself a key in entities. So principal.manager.name can
type- and level-check while principal.manager's uid is absent, and the second
getAttr errors with entityDoesNotExist. That is exactly the gap #642 closes,
and the reason we introduce EntitiesClosedAtLevel.
Per @john-h-kastner-aws on the issue (2026-05-21), the property is stated as a standalone validation pass, independent of slicing:
validatesAtLevel ∧ EntitiesClosedAtLevel → NoEntitiesErrors
with the sliced variant following trivially from the existing semantic-equivalence soundness theorem.
The DNE surface #
Error.entityDoesNotExist is produced in exactly three places, all in
Spec/Entities.lean: Entities.attrs, Entities.tags, Entities.ancestors
(each findOrErr uid .entityDoesNotExist). In the evaluator these are reached
only via:
.getAttron an entity value (getAttr→attrsOf v es.attrs→Entities.attrs).binaryApp .getTag(getTag uid tag es→Entities.tags)
Every other operator either short-circuits or uses the infallible *OrEmpty
lookups (hasAttr/hasTag/mem), so for them the result follows from the
inductive hypotheses alone. Hence only level_based_no_dne_get_attr and the
.getTag branch of level_based_no_dne_binary_app carry real content.
The crux (checked_eval_entity_exists) #
checked_eval_entity_reachable (Slice/Reachable.lean) already places a
level-checked entity at ReachableIn … (n + 1), and with its entities.contains
hypothesis dropped upstream it does so without presupposing existence. Composing
that with EntitiesClosedAtLevel gives checked_eval_entity_exists, the single
lemma consumed by the two dereferencing cases (getAttr on an entity, .getTag).
Everything else is plumbing.
entities is closed for request up to level: every entity reachable from
the request roots (request.sliceEUIDs) within level dereferences is present
in the store. This is the closure condition #642 adds.
Phrased relative to the request because that is what checked_eval_entity_reachable
and friends produce (ReachableIn entities request.sliceEUIDs euid (n + 1)).
Entities.closedAtLevel (Spec/Slice.lean) is the executable algorithm that
decides this predicate, and closedAtLevel_iff proves the two equivalent, so the
guarantees below can be discharged by running the check on a concrete store.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Entities.closedAtLevel (the executable check) agrees with the
EntitiesClosedAtLevel predicate. Entities.closedAtLevel reuses the reachable
set computed by the slicing algorithm (Entities.sliceAtLevel.sliceAtLevel), and
membership in that set coincides with ReachableIn (reachable_then_mem_slice /
reachable_of_mem_slice), so the algorithm checks contains on exactly the
entities the predicate quantifies over.
Per-expression inductive hypothesis, parallel to TypedAtLevelIsSound: a
level-checked, well-typed e evaluated against a store closed at its level does
not produce entityDoesNotExist.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The crux: a reachable, level-checked entity exists #
KEY LEMMA (the crux of #642). If a level-checked, well-typed entity-access
expression evaluates to (a value yielding, via path) euid, and the store is
closed at level n + 1, then euid is present in the store.
checked_eval_entity_reachable (Slice/Reachable.lean) supplies
ReachableIn entities request.sliceEUIDs euid (n + 1) without assuming euid
exists (its entities.contains hypothesis was dropped upstream), and
EntitiesClosedAtLevel turns that reachability into membership. This is the one
lemma the two dereferencing cases (getAttr on an entity, .getTag) consume.
Per-operation "never DNE" helpers #
The generic bind_ne_error workhorse (monadic bind preserves "not this error")
lives in Thm/Data/Control.lean; the lemmas below cover the individual
operators.
apply₁ only ever yields a value, a typeError, or an arithBoundsError (via
intOrErr); it never produces entityDoesNotExist.
hasAttr reads attributes via the infallible attrsOrEmpty lookup, so it never
produces entityDoesNotExist (at worst typeError for a non-record/entity
receiver).
Coercing a result to Bool (Result.as Bool) never introduces an
entityDoesNotExist: on success it runs Value.asBool (at worst typeError),
on failure it preserves the existing error. Used for the boolean-guard
operators (and, or, ite).
Inversion for the boolean coercion: if Result.as Bool r = .ok b, then r was
already .ok (.prim (.bool b)). Lets the guard operators recover the underlying
value (needed to fire GuardedCapabilitiesInvariant).
Per-operator lemmas #
Trivial (IH plumbing only): lit, var, and, or, ite, unaryApp, hasAttr, set,
call, record, and the non-dereferencing / *OrEmpty branches of binaryApp.
Meaty (use checked_eval_entity_exists): get_attr (entity branch) and the
.getTag branch of binary_app.
The boolean-guard operators coerce their final Result Bool back to
Result Value via (Value.prim ∘ Prim.bool) <$> ·. That functor map never
turns a non-entityDoesNotExist result into one.
Meaty (.getTag branch). For op = .getTag the evaluator calls
getTag uid tag es which dereferences Entities.tags and can DNE; that branch
mirrors get_attr below (checked_eval_entity_exists shows the entity is
present). All other binary operators are non-dereferencing or use *OrEmpty
(.mem, .hasTag), so they follow from the inductive hypotheses.
Entity branch. getAttr (entity euid) a es = es.attrs euid >>= (·.findOrErr a attrDoesNotExist),
which DNEs iff euid ∉ es. By soundness e evaluates to an entity (or errors,
in which case the IH rules out a DNE error and the remaining error kinds are not
entityDoesNotExist). When it evaluates to entity euid, checked_eval_entity_exists
shows euid is present in the store, so the outer lookup yields at worst
attrDoesNotExist, never entityDoesNotExist.
Record branch. No entity is dereferenced, so the outer lookup is a record
projection (attrDoesNotExist at worst). Only the inner expression e could
DNE, and the IH rules that out.
Meaty case. Dispatches on whether the receiver has entity or record type
(type_of_getAttr_inversion); the entity branch is where entityDoesNotExist
can fire and where EntitiesClosedAtLevel is consumed.
Top-level theorem #
Mirrors level_based_slicing_is_sound_expr: structural recursion on e
dispatching to the per-operator lemmas, with the same sizeOf bookkeeping for
the set/call/record inductive-hypothesis builders.
Policy- and validator-level wrappers #
Mirror typecheck_policy_with_level_is_sound /
validate_with_level_is_sound_wf, threading EntitiesClosedAtLevel through to
the top-level expression theorem. Stubbed until the expression theorem is
complete.