From stack-machine executions to the platform Turing-machine multiplication predicate

Proved

NLogN.multipliesAt_of_exec

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let prog be a stack-machine program with $S$ stacks and $P>0$ procedures (procedure $0$ is the main program), let $n\in\mathbb N$ and $T\in\mathbb R$ . Suppose that for all bit strings $x,y$ of length $n$ there are a final state $\sigma'$ and a cost $c$ such that

procedure $0$ , started from the initial state (all stacks empty, input position $0$ , empty output) on the input word $x\#y$ (inputCodes x y), executes to $\sigma'$ with exact cost $c$ ;
the output of $\sigma'$ is $\mathrm{bin}_{2n}(\mathrm{val}(x)\cdot\mathrm{val}(y))$ ;
$2c+1\le T$ .

Then the compiled multitape Turing machine machineOf prog hP satisfies the platform predicate

\mathrm{MultipliesAt}(\mathrm{machineOf}\ prog\ hP,\ n,\ T),

i.e. on every input $x\#y$ with $|x|=|y|=n$ it halts within $T$ steps with output tape $\mathrm{bin}_{2n}(\mathrm{val}\,x\cdot\mathrm{val}\,y)$ .

This is the bridge from the program-level semantics to the machine model of Def_IntMul_MultitapeModel: each flat instruction is simulated by at most two Turing machine steps, plus one step to halt.

Formalization Note. machineOf compiles the structured program to flat code with jumps and calls, then to a MultitapeTM with $S+3$ tapes: the input tape, the output tape, a control tape holding return addresses, and one tape per stack. Exec is the big-step semantics with exact cost; bin and val are the platform's definitions.

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
open IntMul IntMul.Mach
variable {S P : ℕ}

Formal statement

theorem NLogN.multipliesAt_of_exec (prog : Fin P → Stmt S P) (hP : 0 < P) (n : ℕ) (T : ℝ)
    (h : ∀ x y : List Bool, x.length = n → y.length = n → ∃ σ' c,
      Exec (inputCodes x y) prog (prog ⟨0, hP⟩) (St.init S) σ' c ∧
        σ'.out = bin (2 * n) (val x * val y) ∧ (2 * c + 1 : ℝ) ≤ T) :
    MultipliesAt (machineOf prog hP) n T := 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.multipliesAt_of_exec` of the Lean development NLogN/Top.lean (lines 111–138), written for the prove2.me integer-multiplication campaign.

View graph