Delayed packed-formula copies

An executable proof-carrying primitive that advances the rolling formula cursor and emits the corresponding packed-output copy gate.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_sound (sizePolynomial : Polynomial ℕ) : (emitPackedFormulaCopy sizePolynomial).Sound

Delayed packed-formula copy emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_spaceBoundByWidth (sizePolynomial : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hpolynomialCap : ∀ (inputLength : ℕ), 2 * TM.binaryPolynomialValueCap sizePolynomial (values inputLength Work.horizon) ≤ width inputLength) (hcursorResult : ∀ (inputLength : ℕ), values inputLength Work.gateCount + Polynomial.eval (values inputLength Work.horizon) sizePolynomial ≤ width inputLength) (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference₀ : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) (hpositive : ∀ (inputLength : ℕ), 0 < Polynomial.eval (values inputLength Work.horizon) sizePolynomial) : (emitPackedFormulaCopy sizePolynomial).SpaceBoundByWidthAt initialSpace values width

A delayed packed-formula copy has a pointwise width certificate when the evaluator cap, advanced cursor, wire frontier, and old reference fit the shared width, and the formula block is explicitly nonempty. The cursor-result bound also bounds the evaluated formula size.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_requires (sizePolynomial : Polynomial ℕ) (values : BinaryValues WorkCount) : (emitPackedFormulaCopy sizePolynomial).requires values ↔ values Work.temporary₃ = 0 ∧ values Work.polynomialScratch = 0 ∧ values Work.multiplyCounter = 0 ∧ values Work.addCounter = 0 ∧ values Work.copyCounter = 0 ∧ values Work.emitCounter = 0 ∧ 0 < Polynomial.eval (values Work.horizon) sizePolynomial

Exact zero-scratch and positive-formula-size domain.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_effect (sizePolynomial : Polynomial ℕ) (values : BinaryValues WorkCount) : (emitPackedFormulaCopy sizePolynomial).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + Polynomial.eval (values Work.horizon) sizePolynomial)) Work.available (values Work.available + 1)) Work.reference₀ 0) Work.temporary₃ 0

The rolling formula cursor and wire frontier each advance exactly once; the reference and polynomial scratch registers are restored to zero.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_emitted (sizePolynomial : Polynomial ℕ) (values : BinaryValues WorkCount) : (emitPackedFormulaCopy sizePolynomial).emitted values = (CircuitCode.RawGate.copy (values Work.gateCount + Polynomial.eval (values Work.horizon) sizePolynomial - 1)).encode

Exact non-negated copy gate for the output wire of the newly traversed formula block.