claimroutine
Guarded deterministic finite graph keeps designated paths
Guarded graph is finite and deterministic and keeps designated paths
basic well-definedness of the local graph
Statement (paper)
The graph whose states are the cursor and delimited words with the specified finite tags, with the guards checked as described and with the edge omitted at a state with an unavailable instruction, is finite and deterministic, and its designated paths pass all guards. Guards may create additional dead ends, but they cannot create a new path from a canonical initiation to a success state.
In plain English
The graph whose states are the cursor and delimited words with the specified finite tags, with guards checked and the edge omitted at a state whose instruction is unavailable, is finite and deterministic, and every designated path passes all guards. Guards can only add dead ends; they cannot create a new path from a canonical initiation to a success state.
Why it's here
This is the basic well-definedness step of the guarded local graph lemma: outdegree at most one and the preservation of designated paths give the claim that designated executions are exactly the prescribed terminal ones. Designated executions satisfy the allowance and clock bounds from the controller allowance definition, so those guards never cut them. The later claims on predecessors and probe-copy sizes build on this graph.
Classified routine:
A bookkeeping well-definedness check: determinism and finiteness follow directly from the construction. Guards only delete edges, and designated executions meet the bounds in the controller allowance definition, so no guard cuts them.
Uses
Used by
Sources
PaperOpen
- Section
- §11.2 Program states and record bounds
- Page
- —
- Label
—- Line
sections/implementation.tex:341
Leannot aligned
Phase 2 aligns this node to a Lean declaration.