Execution seams for the streaming circuit evaluator #
The evaluator has three semantically named work tapes, while Cfg exposes work
tapes through Fin 3. This file packages that representation boundary once.
Later phase proofs can state exact configurations using named tape arguments and
reduce one machine step to the corresponding named CoreAction, without
reopening the finite-index projection plumbing.
Work-tape family assembled from the evaluator's three named tapes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Symbols read from the evaluator's three named work tapes.
Equations
- Complexity.CircuitCode.Machine.Internal.coreHeads code wires counter i = (Complexity.CircuitCode.Machine.Internal.coreWork code wires counter i).read
Instances For
Exact evaluator configuration with named work-tape arguments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Project the counter tape from a named evaluator work family.
Project the counter-head symbol from the named evaluator heads.
Reassembling all three named tapes recovers an arbitrary evaluator work family.
Reassembling the named fields of a configuration recovers the original configuration.
Writing a Boolean verdict at output cell one preserves its parked head and left-marker invariant and records the exact verdict cell.
Zero-verdict specialization of outputWriteBool_frame, matching every
controller rejection action.
A unary-prefix counter with its canonical left marker is the corresponding
binary cursor over true bits at its append frontier.
A rewound binary cursor of true bits is the public unary-counter shape.
One evaluator step on a named configuration applies the four named tape actions directly. This is the representation seam used by every phase proof.
Any controller branch selecting CoreAction.reject halts in one step,
writes zero at the current output head, and preserves the named work tapes.
In the code-rewind phase, an off-marker code cursor takes one ordinary left step while every framed tape remains unchanged.
On the left marker, the code rewind bounces to the first code bit and hands control to the wire-rewind phase.
Rewinding a code cursor takes exactly position + 2 steps and enters the
wire-rewind phase with the code head on its first bit.
In the wire-rewind phase, an off-marker wire cursor takes one ordinary left step while every framed tape remains unchanged.
On the left marker, the wire rewind bounces to the first wire and enters the family-tag phase.
Rewinding a wire cursor takes exactly position + 2 steps and enters the
family-tag phase with the wire head on its first bit.
From the two staged append frontiers, the evaluator reaches its first
family-tag read in exactly code.length + input.length + 4 steps, retaining
both canonical tape contents.
An empty-input family tagged with zero enters the explicit empty-answer branch and advances past the tag.
A nonempty input paired with a positive-family tag enters the unary gate count phase and advances past the tag.
Reading one unary gate-count mark advances the code cursor and extends the counter by one mark.
The zero delimiter ends unary gate-count construction and advances the code cursor to the first serialized gate.
Scanning a terminated unary gate count takes exactly remaining + 1
steps. It leaves the code at the gate stream and materializes all marks on the
counter tape.
In the counter-rewind phase, an off-marker counter cursor takes one ordinary left step while every framed tape remains unchanged.
On the left marker, the counter rewind bounces to its first mark and enters the initial gate-check phase.
Rewinding a counter cursor takes exactly position + 2 steps and enters
the first gate check with the counter at position zero.
A built unary prefix rewinds in exactly count + 2 steps to the public
counter shape expected by the gate loop.
A well-formed positive-family header builds and rewinds its declared unary
gate counter in exactly 2 * count + 4 steps, stopping at the first gate
check with the code cursor at the serialized gate stream.
A positive-family tag is invalid on the empty input and rejects in one step.
An empty-family tag is invalid on a nonempty input and rejects in one step.
A missing family tag rejects in one step for either input arity.
The empty-family answer phase consumes its Boolean answer bit, independently of the remaining serialized suffix.
At the exact end of an empty-family code, the controller writes the answer and halts.
A well-formed empty-input family code runs from its tag read to a halted configuration in exactly three steps.
From the staging frontiers, a well-formed empty-input family code reaches its exact halted verdict in nine steps. This is the first complete branch of the streaming controller's machine semantics.