Evaluation of bounded-trace acceptance circuits #
This internal module composes the complete trace evaluator with the final
halt-and-output AND gate. The resulting raw circuit's last wire is exactly the
Boolean acceptance predicate used by NTM.acceptCount.
theorem
Complexity.CircuitUnrolling.evalAux?_acceptanceRawCircuit_internal
{k : ℕ}
(tm : NTM k)
(T n available : ℕ)
[NeZero available]
(layout : InputWires T n available)
(x : BitString n)
(choices : Fin T → Bool)
(wires : Array Bool)
(hsize : wires.size = available)
(hdata : ∀ (j : Fin n), wires[↑(layout.data j)]? = some (x j))
(hchoices : ∀ (j : Fin T), wires[↑(layout.choice j)]? = some (choices j))
:
∃ (traceResult : Array Bool),
(acceptanceRawCircuit tm T n available layout).evalAux? wires = some
(traceResult.push
(decide
((tm.trace T choices (tm.initCfg x.toList)).state = tm.qhalt ∧ (tm.trace T choices (tm.initCfg x.toList)).output.cells 1 = Γ.one))) ∧ traceResult.size = wires.size + traceFragmentSize tm T n available layout ∧ (∀ i < wires.size, traceResult[i]? = wires[i]?) ∧ EncodesConfig tm T (traceOutputBase tm T n available layout) traceResult
(tm.trace T choices (tm.initCfg x.toList))
Evaluating the acceptance circuit appends the Boolean acceptance predicate to the successfully evaluated trace array.
theorem
Complexity.CircuitUnrolling.eval?_acceptanceRawCircuit_internal
{k : ℕ}
(tm : NTM k)
(T n available : ℕ)
[NeZero available]
(layout : InputWires T n available)
(x : BitString n)
(choices : Fin T → Bool)
(input : BitString available)
(hdata : ∀ (j : Fin n), input (layout.data j) = x j)
(hchoices : ∀ (j : Fin T), input (layout.choice j) = choices j)
:
On a fixed-length primary input, raw single-output evaluation returns the acceptance predicate of the represented bounded trace.