Verified structured RAM iterable serialized-gate step #
This module exposes the split-layout gate routine used by the serialized-circuit experiment. Code and mutable memo occupy disjoint regions, so the exact same routine can be invoked again at the returned cursor.
theorem
Complexity.RAM.Structured.GateStreamStep.routine_correct
{gateStart base : ℕ}
{gate : CircuitCode.RawGate}
{tail wires : List Bool}
{store : Store}
(hready : Ready gateStart base gate tail wires store)
(hbound : Internal.StoreEnvelope (codeEnd gateStart gate tail) (codeEnd gateStart gate tail) store)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec routine store final (stepCount gate) cost space ∧ final UnaryDecode.pointerReg = gateStart + gate.encode.length ∧ final UnaryDecode.remainingReg = tail.length ∧ final memoBaseReg = base ∧ final wireCountMetaReg = wires.length + 1 ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ (∀ (index : ℕ) (hindex : index < wires.length), final (base + index) = Input.bitValue wires[index]) ∧ ∀ (delta : ℕ),
final (gateStart + gate.encode.length + delta) = match tail[delta]? with
| some bit => Input.bitValue bit
| none => 0
Consume and evaluate one gate while preserving the unread code tail and advancing the independent mutable memo.
theorem
Complexity.RAM.Structured.GateStreamStep.compiled_correct
{gateStart base : ℕ}
{gate : CircuitCode.RawGate}
{tail wires : List Bool}
{store : Store}
(hready : Ready gateStart base gate tail wires store)
(hbound : Internal.StoreEnvelope (codeEnd gateStart gate tail) (codeEnd gateStart gate tail) store)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec routine store final (stepCount gate) cost space ∧ run compiled (stepCount gate) { pc := 0, regs := store } = { pc := routine.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount gate) { pc := 0, regs := store }) ∧ logTimeUpto compiled (stepCount gate) { pc := 0, regs := store } = cost ∧ spaceUpto compiled (stepCount gate) { pc := 0, regs := store } = space ∧ final UnaryDecode.pointerReg = gateStart + gate.encode.length ∧ final UnaryDecode.remainingReg = tail.length ∧ final memoBaseReg = base ∧ final wireCountMetaReg = wires.length + 1 ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ (∀ (index : ℕ) (hindex : index < wires.length),
final (base + index) = Input.bitValue wires[index]) ∧ ∀ (delta : ℕ),
final (gateStart + gate.encode.length + delta) = match tail[delta]? with
| some bit => Input.bitValue bit
| none => 0
Structural compilation transfers the exact iterable-gate execution, including its logarithmic cost and peak-space measurements.