Stack-machine addition of two integer items is correct in linear time

Proved

NLogN.Runs.addInt

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $\sigma$ be a state of the stack machine with $S$ stacks, and let $q,i,j,k,t_1,t_2$ be stack indices such that $q,i,j,t_1,t_2$ are pairwise distinct and $k$ differs from $q,t_1,t_2$ (it may coincide with $i$ or $j$ ). Here $q$ is the control-state stack, $i,j$ hold the operands, $k$ receives the result and $t_1,t_2$ are scratch stacks. Assume

stack $i$ is the encoding of the integer item $z_1$ followed by $R_i$ , and stack $j$ the encoding of $z_2$ followed by $R_j$ , where neither $R_i$ nor $R_j$ starts with a bit symbol;
the tops of $t_1,t_2$ are not bit symbols, and the top of $t_1$ is not the flag symbol flagB.

Then the statement addInt q i j k t1 t2 runs from $\sigma$ to the state $\sigma'$ obtained by popping both operands and pushing their sum on $k$ :

\sigma' = \big((\sigma[i := R_i])[j := R_j]\big)\big[k := \mathrm{enc}(z_1+z_2) \mathbin{+\!\!+} (\text{current } k)\big],

with cost at most $\mathrm{addIntCost}(\max(|z_1|_2,|z_2|_2))$ , where $|z|_2$ = zsz z is the bit length of $|z|$ . addIntCost is an explicit affine function of the bit length, so signed addition costs $O(\max(|z_1|_2,|z_2|_2))$ steps. All other stacks, the input position and the output are unchanged.

This is the low-level implementation of the item-language instruction add; it is used (through the compiler correctness theorem) for every addition performed by the Schönhage–Strassen procedures.

Formalization Note. Machine states are St S records: stacks stk : Fin S → List Sym over the 16-letter alphabet Sym = Fin 16 (head = top), input position ip and output out; σ.set i L replaces stack i. An integer item is stored as (Item.int z).enc: a sign header followed by the minimal binary magnitude, least significant bit nearest the header; bitOf detects bit symbols, and the hypotheses bitOf (…).head? = none say that the following stack content does not start with a bit (so item boundaries are recognisable). Runs I prog p σ σ' c means p runs from σ to exactly σ' with some cost $c'\le c$ ; the procedures prog and input I are arbitrary.

Preamble

-- Schönhage–Strassen multitape-TM development (NLogN), generated by skeleton subtraction.

import Definitions.Def_IntMul_SS_Defs2

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}
variable {q i j k t1 t2 : Fin S} (hqi : q ≠ i) (hqj : q ≠ j) (hqt1 : q ≠ t1) (hqt2 : q ≠ t2)
  (hij : i ≠ j) (hit1 : i ≠ t1) (hit2 : i ≠ t2) (hjt1 : j ≠ t1) (hjt2 : j ≠ t2) (ht12 : t1 ≠ t2)
  (hqk : q ≠ k) (hkt1 : k ≠ t1) (hkt2 : k ≠ t2)
include hqi hqj hqt1 hqt2 hij hit1 hit2 hjt1 hjt2 ht12 hqk hkt1 hkt2

Formal statement

theorem NLogN.Runs.addInt (σ : St S) (z1 z2 : ℤ) (Ri Rj : List Sym)
    (hi : σ.stk i = (Item.int z1).enc ++ Ri) (hj : σ.stk j = (Item.int z2).enc ++ Rj)
    (hRi : bitOf Ri.head? = none) (hRj : bitOf Rj.head? = none)
    (ht1 : bitOf (σ.stk t1).head? = none) (ht1' : (σ.stk t1).head? ≠ some flagB)
    (ht2 : bitOf (σ.stk t2).head? = none) :
    NLogN.Runs I prog (NLogN.addInt q i j k t1 t2 : Stmt S P) σ
      (((σ.set i Ri).set j Rj).set k ((Item.int (z1 + z2)).enc ++ ((σ.set i Ri).set j Rj).stk k))
      (addIntCost (max (zsz z1) (zsz z2))) := by sorry

Source

A. Schönhage, V. Strassen, Schnelle Multiplikation großer Zahlen, Computing 7 (1971), 281–292 (main theorem: O(n log n log log n) multitape TM multiplication). Lemma `NLogN.Runs.addInt` of the Lean development NLogN/Arith.lean (lines 310–396), written for the prove2.me integer-multiplication campaign.

View graph