Polynomial recent-wire offsets

Proof-carrying evaluation and raw-gate emission for recent-wire offsets that are fixed polynomials in the run-time tableau horizon.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_sound (polynomial : Polynomial ℕ) (extra : ℕ := 0) : (preparePolynomialOffset polynomial extra).Sound

Fixed-polynomial offset preparation is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_requires (polynomial : Polynomial ℕ) (extra : ℕ) (values : BinaryValues WorkCount) : (preparePolynomialOffset polynomial extra).requires values ↔ values Work.temporary₃ = 0 ∧ values Work.polynomialScratch = 0 ∧ values Work.multiplyCounter = 0 ∧ values Work.addCounter = 0

Exact zero-scratch domain for fixed-polynomial offset preparation.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_effect (polynomial : Polynomial ℕ) (extra : ℕ) (values : BinaryValues WorkCount) : (preparePolynomialOffset polynomial extra).effect values = Function.update values Work.temporary₃ (Polynomial.eval (values Work.horizon) polynomial + extra)

Exact evaluated polynomial offset.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_emitted (polynomial : Polynomial ℕ) (extra : ℕ) (values : BinaryValues WorkCount) : (preparePolynomialOffset polynomial extra).emitted values = []

Polynomial-offset preparation emits no circuit-code bits.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_spaceBoundByWidth (polynomial : Polynomial ℕ) (extra : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hpolynomialCap : ∀ (inputLength : ℕ), 2 * TM.binaryPolynomialValueCap polynomial (values inputLength Work.horizon) ≤ width inputLength) (hoffset : ∀ (inputLength : ℕ), Polynomial.eval (values inputLength Work.horizon) polynomial + extra ≤ width inputLength) : (preparePolynomialOffset polynomial extra).SpaceBoundByWidthAt initialSpace values width

Fixed-polynomial offset preparation has a pointwise width certificate when both its explicit Horner-prefix cap and final evaluated offset fit the shared width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPolynomialRecentGate_sound (polynomial : Polynomial ℕ) (extra : ℕ) (op : AndOrOp) (negated₀ negated₁ : Bool) (fixedOffset₁ : ℕ) : (emitPolynomialRecentGate polynomial extra op negated₀ negated₁ fixedOffset₁).Sound

Polynomial recent-gate emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPolynomialRecentGate_spaceBoundByWidth (polynomial : Polynomial ℕ) (extra : ℕ) (op : AndOrOp) (negated₀ negated₁ : Bool) (fixedOffset₁ : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hpolynomialCap : ∀ (inputLength : ℕ), 2 * TM.binaryPolynomialValueCap polynomial (values inputLength Work.horizon) ≤ width inputLength) (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference₀ : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) (hreference₁ : ∀ (inputLength : ℕ), values inputLength Work.reference₁ ≤ width inputLength) (hloop : ∀ (inputLength : ℕ), values inputLength Work.loop₃ = 0) (hoffsetAvailable : ∀ (inputLength : ℕ), Polynomial.eval (values inputLength Work.horizon) polynomial + extra ≤ values inputLength Work.available) (hfixedOffset₁ : ∀ (inputLength : ℕ), fixedOffset₁ ≤ values inputLength Work.available) : (emitPolynomialRecentGate polynomial extra op negated₀ negated₁ fixedOffset₁).SpaceBoundByWidthAt initialSpace values width

Polynomial recent-gate emission has a pointwise width certificate when the evaluator cap, width-bounded wire frontier and old references, zero loop controller, and both valid offsets are supplied explicitly.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPolynomialRecentGate_requires (polynomial : Polynomial ℕ) (extra : ℕ) (op : AndOrOp) (negated₀ negated₁ : Bool) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) : (emitPolynomialRecentGate polynomial extra op negated₀ negated₁ fixedOffset₁).requires values ↔ values Work.temporary₃ = 0 ∧ values Work.polynomialScratch = 0 ∧ values Work.multiplyCounter = 0 ∧ values Work.addCounter = 0 ∧ values Work.copyCounter = 0 ∧ values Work.loop₃ = 0 ∧ Polynomial.eval (values Work.horizon) polynomial + extra ≤ values Work.available ∧ fixedOffset₁ ≤ values Work.available ∧ values Work.emitCounter = 0

Exact zero-scratch and valid-offset domain for polynomial recent-gate emission.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPolynomialRecentGate_effect (polynomial : Polynomial ℕ) (extra : ℕ) (op : AndOrOp) (negated₀ negated₁ : Bool) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) (hloop : values Work.loop₃ = 0) : (emitPolynomialRecentGate polynomial extra op negated₀ negated₁ fixedOffset₁).effect values = Function.update (Function.update (Function.update (Function.update (Function.update values Work.loop₃ 0) Work.available (values Work.available + 1)) Work.reference₀ 0) Work.reference₁ 0) Work.temporary₃ 0

Polynomial recent-gate emission advances available once and restores its offset, controller, and reference scratch registers.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPolynomialRecentGate_emitted (polynomial : Polynomial ℕ) (extra : ℕ) (op : AndOrOp) (negated₀ negated₁ : Bool) (fixedOffset₁ : ℕ) (values : BinaryValues WorkCount) (hloop : values Work.loop₃ = 0) : (emitPolynomialRecentGate polynomial extra op negated₀ negated₁ fixedOffset₁).emitted values = { op := op, input₀ := values Work.available - (Polynomial.eval (values Work.horizon) polynomial + extra), input₁ := values Work.available - fixedOffset₁, negated₀ := negated₀, negated₁ := negated₁ }.encode

Exact raw gate emitted from the polynomial and fixed recent-wire offsets.