Verified structured RAM serialized-gate step

This module is the first end-to-end composition of the structured RAM parser and mutable-data APIs. One fixed program consumes a canonical gate encoding, invokes the same cursor loop for both unary references, discovers the following memo base at runtime, evaluates the decoded gate, and appends its result.

theorem Complexity.RAM.Structured.GateStep.program_correct (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]

Source correctness and exact transition count for one canonical gate.

theorem Complexity.RAM.Structured.GateStep.program_performance (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ cost ≤ timeBound gate wires ∧ space ≤ spaceBound gate wires ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]

Source correctness, exact transitions, and closed-form logarithmic resource bounds for one serialized gate and its current memo.

theorem Complexity.RAM.Structured.GateStep.compiled_correct (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ run compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount gate) { pc := 0, regs := inputStore gate wires }) ∧ logTimeUpto compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = cost ∧ spaceUpto compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = space ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]

Compilation preserves the exact serialized-gate run and its memo result.

theorem Complexity.RAM.Structured.GateStep.compiled_performance (gate : CircuitCode.RawGate) (wires : List Bool) (value0 value1 : Bool) (hvalue0 : wires[gate.input₀]? = some value0) (hvalue1 : wires[gate.input₁]? = some value1) : ∃ (final : Store) (cost : ℕ) (space : ℕ), Exec program (inputStore gate wires) final (stepCount gate) cost space ∧ cost ≤ timeBound gate wires ∧ space ≤ spaceBound gate wires ∧ run compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled (stepCount gate) { pc := 0, regs := inputStore gate wires }) ∧ logTimeUpto compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = cost ∧ spaceUpto compiled (stepCount gate) { pc := 0, regs := inputStore gate wires } = space ∧ final GateEval.outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (memoBase gate + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (memoBase gate + index) = Input.bitValue wires[index]

Compilation transfers the serialized-gate result and both source resource bounds exactly to the concrete logarithmic-cost RAM.