Delayed packed-formula copies -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_spaceBoundByWidth_internal (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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_requires_internal (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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPackedFormulaCopy_effect_internal (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

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

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