An executable model of execution authority with a bounded state search
The model met 14 of 14 corpus cases; a bounded breadth-first search of 200,000 states and 693,029 transitions stopped at depth 9 with no violation, and witnesses reached 22 of 22 required events.
Prediction heldDoes it work?Working note
- Designed for
- Built to test whether an executable model of the guard's execution authority (grant, admission, send, recovery) with an independent verifier meets fixed obligations over a fixed corpus, as a basis for integrating it into the guard.
What was tested
We built a Python model of the guard’s execution authority with its own provider and world, a resource automaton, a closed compiler and wire format, and an independent verifier, then checked it against a fixed corpus, with a budgeted breadth-first search and with executable witnesses. Requirements and cases were fixed beforehand within this cycle.
What we observed
All 14 of 14 corpus cases ended with their expected outcomes. The search covered 200,000 states and 693,029 transitions and stopped on its resource limit at depth 9 with no violation. Witnesses reached 22 of 22 required events and completed 12 positive traces; the search alone reached 21 of 22.
What this means for Heimdall
Within the searched prefix and the witnesses no violation appeared: a bounded basis for an integration plan, not a verification.
Limits
The state space was truncated and overall progress was not established; “fixed beforehand” means within this work cycle, not an independent prediction; outputs were not kept; a model, which the shipped path did not implement.
What remains open
Keep or regenerate the run outputs before citing the counts.