Stack-machine input reading: parse a binary word and its length ruler

Proved

NLogN.Runs.readR

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

integer-multiplicationschonhage-strassen-tmturing-machines

Let $q,i,j,t_1,t_2,t_3$ be pairwise distinct stacks of a state $\sigma$ , and let stop be a symbol different from the bit codes $0$ and $1$ . Let $W$ be a list of bits such that the input word $I$ contains, starting at the current input position $\sigma.\mathrm{ip}$ , the codes of the bits of $W$ (most significant first) followed by stop (positions past the end of $I$ read as codeEnd). Assume the tops of $t_1,t_2,t_3$ are not bit symbols. Then readR q i j t1 t2 t3 stop runs from $\sigma$ to the state in which

i \mathrel{+}= \mathrm{enc}(\mathrm{val}(W)),\qquad j \mathrel{+}= \mathrm{enc}(2^{|W|}),\qquad \mathrm{ip} := \sigma.\mathrm{ip}+|W|+1,

(pushing onto the existing contents of $i$ and $j$ ), with cost at most $\mathrm{readRCost}(|W|)$ , which is linear in $|W|$ . Here $\mathrm{val}(W)$ is the platform's big-endian value of a bit list.

This is how the top-level program reads its two inputs $x$ (terminated by the separator #) and $y$ (terminated by the end of input), together with the rulers $2^n$ used later for output.

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
open IntMul
variable {S P : ℕ} {I : List Sym} {prog : Fin P → Stmt S P}

Formal statement

theorem NLogN.Runs.readR {q i j t1 t2 t3 : Fin S} (hqi : q ≠ i) (hqj : q ≠ j) (hqt1 : q ≠ t1)
    (hqt2 : q ≠ t2) (hqt3 : q ≠ t3) (hij : i ≠ j) (hit1 : i ≠ t1) (hit2 : i ≠ t2) (hit3 : i ≠ t3)
    (hjt1 : j ≠ t1) (hjt2 : j ≠ t2) (hjt3 : j ≠ t3) (ht12 : t1 ≠ t2) (ht13 : t1 ≠ t3)
    (ht23 : t2 ≠ t3) {stop : Sym} (hs0 : stop ≠ 0) (hs1 : stop ≠ 1) (σ : St S) (W : List Bool)
    (hk : ∀ k (hk : k < W.length), I.getD (σ.ip + k) codeEnd = codeBit W[k])
    (hstop : I.getD (σ.ip + W.length) codeEnd = stop)
    (ht1 : bitOf (σ.stk t1).head? = none) (ht2 : bitOf (σ.stk t2).head? = none)
    (ht3 : bitOf (σ.stk t3).head? = none) :
    Runs I prog (NLogN.readR q i j t1 t2 t3 stop : Stmt S P) σ
      (((σ.set i ((Item.int (val W : ℤ)).enc ++ σ.stk i)).set j
        ((Item.int ((2 : ℤ) ^ W.length)).enc ++ σ.stk j)).setIp (σ.ip + W.length + 1))
      (readRCost W.length) := 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.readR` of the Lean development NLogN/Prims.lean (lines 102–164), written for the prove2.me integer-multiplication campaign.

View graph