Polynomial recent-wire offsets -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePolynomialOffset_sound_internal (polynomial : Polynomial ℕ) (extra : ℕ) : (preparePolynomialOffset polynomial extra).Sound

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

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

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

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

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

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

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

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

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