Moving a list of integers between stacks (register-held count)

Proved

NLogN.FW.spec_mv

by xuanji · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

harvey-van-der-hoeven-tminteger-multiplicationturing-machines

Let $i,j,c$ be registers below 55 with $i\ne j$ and $c\ne i,j$ , let stack $i$ start with the integer list $l$ and register $r<55$ hold $|l|$ . If $|l|$ and all entries of $l$ have bit length $\le B$ , the program mvList i j c (reg r) moves $l$ reversed onto stack $j$ within cost $|l|(14000(B+2)+30) + 4000(B+2) + 32$ .

Formalization Note. The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$ . MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$ . Register names (GU, CR, KB, XN, …) are fixed stack indices.

Preamble

-- Harvey–van der Hoeven multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_HvdH_M_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

set_option linter.unusedSimpArgs false
set_option linter.unusedVariables false
open NLogN
open NLogN.FW
open IntMul NLogN

Formal statement

theorem NLogN.FW.spec_mv (M : MulSpec) (i j c r : Fin HS) (s : IState HS) (l : List ℤ)
    (Ri Lr : List Item) (hij : i ≠ j) (hci : c ≠ i) (hcj : c ≠ j) (hi : s.G i = ints l ++ Ri)
    (hr : s.G r = .int (l.length : ℤ) :: Lr)
    (hi55 : i.val < 55) (hj55 : j.val < 55) (hc55 : c.val < 55) (hr55 : r.val < 55)
    (B : ℕ) (hlB : zsz (l.length : ℤ) ≤ B) (hB : ∀ x ∈ l, zsz x ≤ B) :
    Spec M (RM.rs (mvList i j c (.reg r))) s ((s.upd i Ri).upd j (ints l.reverse ++ s.G j))
      (l.length * (14000 * (B + 2) + 30) + 4000 * (B + 2) + 32) := by sorry

Source

D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Ann. of Math. 193 (2021), 563–617 (Theorem 1.1: multitape Turing machine multiplication in O(n log n)). Lemma `NLogN.FW.spec_mv` of the Lean development NLogN/HFW1.lean (lines 122–134), written for the prove2.me integer-multiplication campaign.

View graph