Compilation of item-language operations to the stack machine is correct

Proved

NLogN.IOp.Step.runs

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

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

Let $o$ be an item-language operation on $S$ item stacks (add, neg, dup, drop, move, constant, mark, unmark, shift, split, read, write, cat) and suppose $o$ steps from item state $s$ to $s'$ with cost $c$ (o.Step I s s' c). Then its compiled stack-machine statement o.stmt (over $S+4$ symbol stacks) runs from the encoding encI s to encI s' within cost $c$ , for any procedure table and input.

Formalization Note. encI writes each item stack as a symbol stack using the sign–magnitude binary item encoding and adds four scratch stacks. This is the per-operation correctness of the compiler from the item language to the symbol stack machine of IntMul_HvdH_M_Defs1 (it combines the primitive runs for addition, duplication, shifting, splitting, concatenation, reading and writing).

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

open NLogN
open IntMul
variable {S P : ℕ}
variable {I : List Sym} {prog : Fin P → Stmt (S + 4) P}

Formal statement

theorem NLogN.IOp.Step.runs {o : IOp S} {s s' : IState S} {c : ℕ} (h : o.Step I s s' c) :
    Runs I prog (o.stmt : Stmt (S + 4) P) (encI s) (encI s') c := 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.IOp.Step.runs` of the Lean development NLogN/ILang.lean (lines 179–277), written for the prove2.me integer-multiplication campaign.

View graph