Structured RAM iterable serialized-gate step — definitions #
Unlike the compact GateStep benchmark, this routine keeps the code cursor and
mutable wire memo physically separate. Registers 7 and 8 carry the memo base
and current wire count while the parser consumes a gate from a higher code
region. Two fixed continuation cells lie between the evaluator's control prefix
and the memo, so cursor state survives gate evaluation without aliasing either
mutable wires or unread code.
Physical base of the mutable wire memo.
Instances For
Number of semantic entries currently in the wire memo.
Instances For
Address of the current gate's first header bit.
Instances For
First decoded reference retained across the second unary decode.
Instances For
Fixed spill cell for the next code pointer.
Instances For
Fixed spill cell for the unread-code count.
Instances For
Initialize parser scratch and remember the current gate start.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Consume the fixed three-bit gate header without copying it. The header is loaded from its saved code address only after both references are decoded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Save the first reference and restart the unary accumulator.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Spill the continuation cursor, load the saved header, and marshal the gate
and independent memo metadata into GateEval's calling convention.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recover the next code cursor and rebuild persistent memo metadata after the gate kernel has appended its result.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Parse and evaluate one gate while retaining an independent code cursor and memo base for the next call.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Concrete compiled iterable gate routine.
Equations
Instances For
Exact transition count on one canonical gate.
Equations
Instances For
Serialized bits beginning at the current gate and continuing with unread code.
Equations
- Complexity.RAM.Structured.GateStreamStep.codeBits gate tail = gate.encode ++ tail
Instances For
Absolute address immediately after all code visible to this invocation.
Equations
- Complexity.RAM.Structured.GateStreamStep.codeEnd gateStart gate tail = gateStart + (Complexity.RAM.Structured.GateStreamStep.codeBits gate tail).length
Instances For
Unary-decoder input length corresponding to the absolute code region.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Calling convention at the beginning of an iterable gate invocation.
The memo lies strictly above the fixed continuation cells.
The append cell lies strictly before the current gate.
The parser cursor points at the current gate header.
The parser sees the complete current gate followed by unread code.
Persistent physical memo base.
Persistent semantic memo length.
- code_eq (delta : ℕ) : store (gateStart + delta) = match (codeBits gate tail)[delta]? with | some bit => Input.bitValue bit | none => 0
Current gate and unread tail are encoded at the cursor.
- wire_eq (index : ℕ) : store (base + index) = match wires[index]? with | some bit => Input.bitValue bit | none => 0
Existing memo contents.
Instances For
Calling convention immediately before marshalOps, after both references
have been decoded successfully.
The memo lies strictly above the fixed continuation cells.
The append cell lies strictly before unread gate code.
The second unary decoder recorded success.
The second decoded reference remains in the accumulator.
The next unread code address.
Number of unread code bits.
The second unary loop is inactive.
Persistent physical memo base.
Persistent semantic memo length.
Saved address of the current gate header.
Retained first decoded reference.
Operation header bit at the saved gate address.
First-negation header bit.
Second-negation header bit.
- wire_eq (index : ℕ) : store (base + index) = match wires[index]? with | some bit => Input.bitValue bit | none => 0
Existing memo contents.