Direct-unrolling read-formula generator

A stack-free proof-carrying routine that emits the exact numeric gate schedule for reading one symbol from a bounded encoded configuration.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_sound (stateCount tapeCount : ℕ) : (emitReadFormula stateCount tapeCount).Sound

Complete read-formula emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadConnector_spaceBoundByWidth {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (havailablePositive : ∀ (inputLength : ℕ), 1 ≤ values inputLength Work.available) (hreference₀ : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) (hreference₁ : ∀ (inputLength : ℕ), values inputLength Work.reference₁ ≤ width inputLength) : emitReadConnector.SpaceBoundByWidthAt initialSpace values width

One reverse-fold connector has a pointwise width certificate when its frontier and both reference registers fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_spaceBoundByWidth (stateCount tapeCount : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), ReadFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.available + (4 * (values inputLength Work.horizon + 1) + 1) ≤ width inputLength) (hheadCap : ∀ (inputLength position : ℕ), position ≤ values inputLength Work.horizon → transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) position + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 ≤ width inputLength) (hcellCap : ∀ (inputLength position : ℕ), position ≤ values inputLength Work.horizon → transitionCellRef stateCount tapeCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) position (values inputLength Work.symbolIndex) + (values inputLength Work.tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + tapeCount + values inputLength Work.tapeIndex + 4 ≤ width inputLength) : (emitReadFormula stateCount tapeCount).SpaceBoundByWidthAt initialSpace values width

Complete read-formula emission has a pointwise width certificate when the wire frontier and every head- and cell-reference intermediate fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_requires (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).requires values

The clean-entry contract suffices for every arithmetic, loop, reference, and raw-gate leaf in complete read-formula emission.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_effect (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).effect values = Function.update values Work.available (values Work.available + (4 * (values Work.horizon + 1) + 1))

Complete read-formula emission restores all owned scratch and only advances the wire frontier, by four gates per possible head position plus the false identity gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitReadFormula_emitted (stateCount tapeCount : ℕ) (values : BinaryValues WorkCount) (hclean : ReadFormulaClean values) : (emitReadFormula stateCount tapeCount).emitted values = List.flatMap CircuitCode.RawGate.encode (readFormulaSchedule stateCount tapeCount (values Work.horizon) (values Work.configBase) (values Work.available) (values Work.tapeIndex) (values Work.symbolIndex))

Complete read-formula emission produces exactly the canonical serialized read-formula schedule at the current horizon and wire frontier.