Horner layers: polynomial register evaluation

The reduction emitter's variable indices are mixed-radix numerals (flatVar), and its time budget is p.eval n — both are computed by iterating the single Horner layer tmp := tmp · X + c over unary registers. This file builds that layer from the Arith register calculus and folds it into polyEvalTM.

To keep the time accounting sane across long seqTM chains, every stage bound is rounded up to the single monotone budget opBudget M, where M bounds every register value in play. Only the polynomial shape of the final bound matters (FP quantifies the degree existentially), so all budgets are deliberately loose.

Main definitions

• TM.opBudget — the uniform per-operation time budget
• TM.setConstTM — q := c
• TM.hornerLayerRegTM — tmp := tmp · X + comp (register addend)
• TM.hornerLayerConstTM — tmp := tmp · X + c (constant addend)

Main results

• the _hoareTime specification of each machine

def Complexity.TM.opBudget (M : ℕ) : ℕ

One budget bounds every register operation whose values are at most M: increments, clears, copies, additions, multiply-accumulates, and literal emissions. Cubic in M because mulAddIntoTM's bound is (product value) × (per-mark sweep length).

Equations

• Complexity.TM.opBudget M = 32 * ((M + 2) * (M + 2) * (M + 2))

theorem Complexity.TM.le_opBudget_of_le {a M : ℕ} (h : a ≤ 6 * (M + 2) * (M + 2)) : a ≤ opBudget M

Anything at most quadratic in M + 2 (with constant 6) fits in opBudget M.

theorem Complexity.TM.incRegTM_le_opBudget {d M : ℕ} (h : d ≤ M) : 2 * d + 4 ≤ opBudget M

incRegTM fits the budget.

theorem Complexity.TM.clearRegTM_le_opBudget {d M : ℕ} (h : d ≤ M) : 2 * d + 4 ≤ opBudget M

clearRegTM fits the budget.

theorem Complexity.TM.one_le_opBudget {M : ℕ} : 1 ≤ opBudget M

skipTM fits the budget.

theorem Complexity.TM.addIntoTM_le_opBudget {a b M : ℕ} (ha : a ≤ M) (hab : b + a ≤ M) : a * (2 * (b + a) + 4 + 2) + (a + 2) ≤ opBudget M

addIntoTM fits the budget.

theorem Complexity.TM.iterTM_incRegTM_le_opBudget {c d M : ℕ} (h : d + c ≤ M) : c * (2 * (d + c) + 5) + 1 ≤ opBudget M

iterTM (incRegTM q) c fits the budget.

theorem Complexity.TM.copyIntoTM_le_opBudget {a b M : ℕ} (ha : a ≤ M) (hb : b ≤ M) : 2 * b + 4 + 1 + (a * (2 * (0 + a) + 4 + 2) + (a + 2)) ≤ opBudget M

copyIntoTM fits the budget.

theorem Complexity.TM.setConstTM_le_opBudget {c d M : ℕ} (hc : c ≤ M) (hd : d ≤ M) : 2 * d + 4 + 1 + (c * (2 * c + 5) + 1) ≤ opBudget M

setConstTM fits the budget.

theorem Complexity.TM.emitLitTM_le_opBudget {v M : ℕ} (h : v ≤ M) : 3 * v + 9 ≤ opBudget M

emitLitTM fits the budget.

theorem Complexity.TM.mulAddIntoTM_le_opBudget {a b d M : ℕ} (ha : a ≤ M) (hb : b ≤ M) (hd : d + a * b ≤ M) : a * (mulAddBound a b d + 2) + (a + 2) ≤ opBudget M

mulAddIntoTM fits the budget, provided the accumulated product stays below M.

def Complexity.TM.setConstTM {n : ℕ} (q : Fin n) (c : ℕ) : TM n

q := c (clear, then increment c times).

Equations

• Complexity.TM.setConstTM q c = (Complexity.TM.clearRegTM q).seqTM ((Complexity.TM.incRegTM q).iterTM c)

theorem Complexity.TM.setConstTM_hoareTime {n : ℕ} (q : Fin n) (c d : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hq : work₀ q = regTape d) : (setConstTM q c).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update work₀ q (regTape c)) ys) (2 * d + 4 + 1 + (c * (2 * c + 5) + 1))

setConstTM Hoare specification.

def Complexity.TM.hornerLayerRegTM {n : ℕ} (X comp tmp tmp2 : Fin n) : TM n

One Horner layer with a register addend: tmp := tmp · X + comp (scratch tmp2 ends holding the same value).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.hornerLayerConstTM {n : ℕ} (X tmp tmp2 : Fin n) (c : ℕ) : TM n

One Horner layer with a constant addend: tmp := tmp · X + c (scratch tmp2 ends holding the same value).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.layerBudget (M : ℕ) : ℕ

The (uniform) time budget of one Horner layer.

Equations

• Complexity.TM.layerBudget M = 4 * Complexity.TM.opBudget M + 3

theorem Complexity.TM.hornerLayerRegTM_hoareTime {n : ℕ} {X comp tmp tmp2 : Fin n} (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (hct2 : comp ≠ tmp2) (M x v w u : ℕ) (hx : x ≤ M) (hv : v ≤ M) (hu : u ≤ M) (hres : v * x + w ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hX : work₀ X = regTape x) (hc : work₀ comp = regTape w) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (hornerLayerRegTM X comp tmp tmp2).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update (Function.update work₀ tmp2 (regTape (v * x + w))) tmp (regTape (v * x + w))) ys) (layerBudget M)

hornerLayerRegTM Hoare specification. From tmp = v, X = x, comp = w (and any tmp2 = u), reach tmp = tmp2 = v·x + w with all other tapes untouched, within layerBudget M steps, provided every value in play is at most M.

theorem Complexity.TM.hornerLayerConstTM_hoareTime {n : ℕ} {X tmp tmp2 : Fin n} (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (M x v c u : ℕ) (hx : x ≤ M) (hv : v ≤ M) (hu : u ≤ M) (hres : v * x + c ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hX : work₀ X = regTape x) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (hornerLayerConstTM X tmp tmp2 c).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update (Function.update work₀ tmp2 (regTape (v * x + c))) tmp (regTape (v * x + c))) ys) (layerBudget M)

hornerLayerConstTM Hoare specification. From tmp = v, X = x (and any tmp2 = u), reach tmp = tmp2 = v·x + c.

def Complexity.TM.hornerFold (x : ℕ) : List ℕ → ℕ → ℕ

Horner accumulator over a coefficient list (highest degree first).

Equations

• Complexity.TM.hornerFold x [] x✝ = x✝
• Complexity.TM.hornerFold x (c :: cs) x✝ = Complexity.TM.hornerFold x cs (x✝ * x + c)

@[simp]

theorem Complexity.TM.hornerFold_nil (x a : ℕ) : hornerFold x [] a = a

hornerFold over the empty coefficient list returns the accumulator.

theorem Complexity.TM.hornerFold_cons (x c a : ℕ) (cs : List ℕ) : hornerFold x (c :: cs) a = hornerFold x cs (a * x + c)

Unfolding lemma: one Horner layer replaces the accumulator a by a * x + c.

theorem Complexity.TM.hornerFold_reverse_range (f : ℕ → ℕ) (x k a : ℕ) : hornerFold x (List.map f (List.range k)).reverse a = a * x ^ k + ∑ i ∈ Finset.range k, f i * x ^ i

The Horner fold of a reversed coefficient window is the polynomial sum.

theorem Complexity.TM.hornerFold_le (x : ℕ) (cs : List ℕ) (a : ℕ) : hornerFold x cs a ≤ (a + cs.sum) * (x + 1) ^ cs.length

Crude but monotone bound on the Horner accumulator.

theorem Complexity.TM.hornerFold_take_le (x : ℕ) (cs : List ℕ) (k : ℕ) : hornerFold x (List.take k cs) 0 ≤ (cs.sum + 1) * (x + 1) ^ cs.length

Every prefix of the Horner fold is bounded by the full coefficient sum times the dominating power — the hypothesis-discharger for hornerLayersTM_hoareTime's value cap.

def Complexity.TM.hornerLayersTM {n : ℕ} (X tmp tmp2 : Fin n) (cs : List ℕ) : TM n

Fold Horner layers (constant addends, highest first) over a register.

Equations

• Complexity.TM.hornerLayersTM X tmp tmp2 cs = Complexity.TM.bigSeqTM (List.map (Complexity.TM.hornerLayerConstTM X tmp tmp2) cs)

theorem Complexity.TM.hornerLayersTM_hoareTime {n : ℕ} (X tmp tmp2 : Fin n) (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (M x : ℕ) (hx : x ≤ M) (inp₀ : Tape) (hinp₀ : Parked inp₀) (c : ℕ) (cs : List ℕ) (v u : ℕ) (work₀ : Fin n → Tape) (ys : List Bool) : (∀ k ≤ (c :: cs).length, hornerFold x (List.take k (c :: cs)) v ≤ M) → u ≤ M → (∀ (i : Fin n), Parked (work₀ i)) → work₀ X = regTape x → work₀ tmp = regTape v → work₀ tmp2 = regTape u → (hornerLayersTM X tmp tmp2 (c :: cs)).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update (Function.update work₀ tmp2 (regTape (hornerFold x (c :: cs) v))) tmp (regTape (hornerFold x (c :: cs) v))) ys) ((c :: cs).length * (layerBudget M + 1) + 1)

hornerLayersTM Hoare specification (nonempty coefficient list). From tmp = v, reach tmp = tmp2 = hornerFold x (c :: cs) v, provided every intermediate accumulator value is at most M.

def Complexity.TM.polyCoeffs (p : Polynomial ℕ) : List ℕ

The coefficient list of p, highest degree first.

Equations

• Complexity.TM.polyCoeffs p = (List.map p.coeff (List.range (p.natDegree + 1))).reverse

theorem Complexity.TM.polyCoeffs_ne_nil (p : Polynomial ℕ) : polyCoeffs p ≠ []

The coefficient list of a polynomial is never empty (it has natDegree + 1 entries).

@[simp]

theorem Complexity.TM.polyCoeffs_length (p : Polynomial ℕ) : (polyCoeffs p).length = p.natDegree + 1

polyCoeffs p has exactly p.natDegree + 1 entries.

theorem Complexity.TM.hornerFold_polyCoeffs (p : Polynomial ℕ) (x : ℕ) : hornerFold x (polyCoeffs p) 0 = Polynomial.eval x p

The Horner fold computes p.eval.

def Complexity.TM.polyEvalTM {n : ℕ} (X tmp tmp2 : Fin n) (p : Polynomial ℕ) : TM n

tmp := p.eval x, reading x from register X (Horner's rule over the hardwired coefficient list; tmp2 is scratch and ends equal to tmp).

Equations

• Complexity.TM.polyEvalTM X tmp tmp2 p = (Complexity.TM.setConstTM tmp 0).seqTM (Complexity.TM.hornerLayersTM X tmp tmp2 (Complexity.TM.polyCoeffs p))

theorem Complexity.TM.polyEvalTM_hoareTime {n : ℕ} (X tmp tmp2 : Fin n) (hXt : X ≠ tmp) (hXt2 : X ≠ tmp2) (htt2 : tmp ≠ tmp2) (p : Polynomial ℕ) (M x v u : ℕ) (hx : x ≤ M) (hv : v ≤ M) (hu : u ≤ M) (hpre : ∀ k ≤ p.natDegree + 1, hornerFold x (List.take k (polyCoeffs p)) 0 ≤ M) (inp₀ : Tape) (work₀ : Fin n → Tape) (ys : List Bool) (hinp₀ : Parked inp₀) (hwork₀ : ∀ (i : Fin n), Parked (work₀ i)) (hX : work₀ X = regTape x) (ht : work₀ tmp = regTape v) (ht2 : work₀ tmp2 = regTape u) : (polyEvalTM X tmp tmp2 p).HoareTime (EmitPred inp₀ work₀ ys) (EmitPred inp₀ (Function.update (Function.update work₀ tmp2 (regTape (Polynomial.eval x p))) tmp (regTape (Polynomial.eval x p))) ys) (opBudget M + 1 + ((p.natDegree + 1) * (layerBudget M + 1) + 1))

polyEvalTM Hoare specification. From X = x (and any tmp = v, tmp2 = u), reach tmp = tmp2 = p.eval x, provided M caps x, the starting scratch values, and every Horner prefix value.