Round-six lemma `slUp_runs`

Proved

J6A.SL.slUp_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module Solutions.J6AIL15):

theorem J6A.SL.slUp_runs {P1 : RS} {Rn Rn' : Fin HS} (hRn : Rn ∈ rg) (hRn' : Rn' ∈ rg)
    (dR : Rn ≠ 20 ∧ Rn ≠ 21) (dR' : Rn' ≠ 20 ∧ Rn' ≠ 21 ∧ Rn' ≠ 38 ∧ Rn' ≠ 44 ∧ Rn' ≠ 45)
    (d3 : Rn' ≠ 37 ∧ Rn' ≠ 39)
    (s : IState HS) (F : Fin HS → List ℤ) (h44 : F 44 = []) (h43 : F 43 = []) (h34 : F 34 = [])
    (h35 : F 35 = []) (h36 : F 36 = []) (hρ : ∀ i, F (ρS i) = []) (hrg : ∀ j ∈ rg, F j = [])
    {n n' pre post W C1 : ℕ} {src : ℕ → Option ℕ} (hs : J6Seg.MonoSrc n n' src) (hW : 2 ≤ W)
    (h1 : ∃ v, BV W v ∧ v 1 = pre ∧ v 2 = post ∧ v Rn = n ∧ v Rn' = n' ∧
      ∀ s, Sp P1 (encK s F) (encK s (J6Seg.PJ.RF v (update F 44 (srcTab src (fun _ => 0) n')))) C1)
    (hT : pre * (n' * (2 * post)) ≤ 2 ^ W) (hp2 : 2 * post ≤ 2 ^ W) :
    IRuns I iprog (slUp P1 Rn Rn') (encK s F)
      (encK s (extend ρS (slabV (J6Seg.ctlOf n n' src (fun _ => 0)) pre post n' [] []) F))
      (C1 + ctlPhC W n n' + cTail W)

Context. A lines, IL side 15: the gather and compress slab set-ups

slUp P1 Rn Rn': a register-file prologue P1 (ending with the source table on 44, n on Rn, n' on Rn', pre, post on 1, 2), then B1's ctlPh Rn Rn', then cntP 1 2 Rn' and finiP rg. slUp_runs: it takes F to extend ρS (slabV (ctlOf n n' src 0) pre post n' [] []) F.
slDn: dropP 38 45 2; popL [38, 37, 39, 40], back (slDn_sp).
The prologues gP1 X (gather: parAX X, n' = 8 (M · 8H) on 12, n = 32 t on 7, gthP 3 4 8 9 10 11 12) and cP1 X (compress: n = M · 8 · 8H on 7, cmpP 8 11 4, n' = t on 4) with gP1_sp / cP1_sp.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs67

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6A J6A.SL
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PJ J6A.PA J6A.ST
open J6Seg.Slab (srcTab flatC)
open J6Seg.Src (ctlPh ctlPhC cntP cntOut dropP popL uC DD regOut)
open J6Seg.Ax (ρS slabV)
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem J6A.SL.slUp_runs {P1 : RS} {Rn Rn' : Fin HS} (hRn : Rn ∈ rg) (hRn' : Rn' ∈ rg)
    (dR : Rn ≠ 20 ∧ Rn ≠ 21) (dR' : Rn' ≠ 20 ∧ Rn' ≠ 21 ∧ Rn' ≠ 38 ∧ Rn' ≠ 44 ∧ Rn' ≠ 45)
    (d3 : Rn' ≠ 37 ∧ Rn' ≠ 39)
    (s : IState HS) (F : Fin HS → List ℤ) (h44 : F 44 = []) (h43 : F 43 = []) (h34 : F 34 = [])
    (h35 : F 35 = []) (h36 : F 36 = []) (hρ : ∀ i, F (ρS i) = []) (hrg : ∀ j ∈ rg, F j = [])
    {n n' pre post W C1 : ℕ} {src : ℕ → Option ℕ} (hs : J6Seg.MonoSrc n n' src) (hW : 2 ≤ W)
    (h1 : ∃ v, BV W v ∧ v 1 = pre ∧ v 2 = post ∧ v Rn = n ∧ v Rn' = n' ∧
      ∀ s, Sp P1 (encK s F) (encK s (J6Seg.PJ.RF v (update F 44 (srcTab src (fun _ => 0) n')))) C1)
    (hT : pre * (n' * (2 * post)) ≤ 2 ^ W) (hp2 : 2 * post ≤ 2 ^ W) :
    IRuns I iprog (slUp P1 Rn Rn') (encK s F)
      (encK s (extend ρS (slabV (J6Seg.ctlOf n n' src (fun _ => 0)) pre post n' [] []) F))
      (C1 + ctlPhC W n n' + cTail W) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `J6A.SL.slUp_runs`, Solutions/J6AIL15.lean (lines 88–133) of the round-six development.

View graph