Verified structured RAM decoded-gate evaluator #
This module exposes the mutable-data kernel used by the serialized-circuit evaluator. Given an already-decoded, topologically valid gate, it performs two indirect memo reads, evaluates the gate with branch-free Boolean arithmetic, and indirectly appends the result in exactly twenty RAM transitions.
theorem
Complexity.RAM.Structured.GateEval.routine_correct
{base : ℕ}
{gate : CircuitCode.RawGate}
{wires : List Bool}
{store : Store}
(hready : ReadyAt base gate wires store)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program store final stepCount cost space ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (base + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ final baseReg = base ∧ final wireCountReg = wires.length ∧ (∀ (index : ℕ) (hindex : index < wires.length), final (base + index) = Input.bitValue wires[index]) ∧ ∀ (index : ℕ), wireBase ≤ index → index ≠ base + wires.length → final index = store index
Evaluate a decoded gate in any store satisfying the routine ABI.
The memo may be located above an arbitrary base address; the result is appended there and every prior memo cell is preserved.
theorem
Complexity.RAM.Structured.GateEval.program_performance
(gate : CircuitCode.RawGate)
(wires : List Bool)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
(hgate : gate.WellFormedAt wires.length)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program (inputStore gate wires) final stepCount cost space ∧ cost ≤ timeBound wires.length ∧ space ≤ spaceBound wires.length ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (wireBase + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (wireBase + index) = Input.bitValue wires[index]
Source-level correctness with exact transitions and explicit resources.
theorem
Complexity.RAM.Structured.GateEval.compiled_performance
(gate : CircuitCode.RawGate)
(wires : List Bool)
(value0 value1 : Bool)
(hvalue0 : wires[gate.input₀]? = some value0)
(hvalue1 : wires[gate.input₁]? = some value1)
(hgate : gate.WellFormedAt wires.length)
:
∃ (final : Store) (cost : ℕ) (space : ℕ),
Exec program (inputStore gate wires) final stepCount cost space ∧ run compiled stepCount { pc := 0, regs := inputStore gate wires } = { pc := program.codeSize, regs := final } ∧ Halted compiled (run compiled stepCount { pc := 0, regs := inputStore gate wires }) ∧ logTimeUpto compiled stepCount { pc := 0, regs := inputStore gate wires } ≤ timeBound wires.length ∧ spaceUpto compiled stepCount { pc := 0, regs := inputStore gate wires } ≤ spaceBound wires.length ∧ final outputReg = Input.bitValue (gate.eval value0 value1) ∧ final (wireBase + wires.length) = Input.bitValue (gate.eval value0 value1) ∧ ∀ (index : ℕ) (hindex : index < wires.length), final (wireBase + index) = Input.bitValue wires[index]
End-to-end concrete RAM performance and decoded-gate correctness.
One decoded gate takes logarithmic time in the current memo length.
The explicit memo-space budget is quasilinear.