The block loop (new header) (round six, `blkL2_sp`)

Proved

J6Seg.PreT.blkL2_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The block loop (new header).

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

theorem J6Seg.PreT.blkL2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {K Cs Cb : Fin HS}
    (hK : K ∉ rg) (hK5 : K.val < 56) (hKC : K ≠ Cu) (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56)
    (hKs : K ≠ Cs) (hCb : Cb ∉ rg) (hCb5 : Cb.val < 56) (hKb : K ≠ Cb) (hbs : Cb ≠ Cs)
    (hbu : Cb ≠ Cu) (hwb : Cb ∉ (blkB2 K Cs).writes)
    (hcs : c Cs = []) (hcu : c Cu = []) (hcb : c Cb = [])
    {P R sN tN lam aN A b q : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A)
    (h28 : v 28 = b) (h4l : 4 * lam ≤ 2 ^ A)
    (h6 : v 6 = q) (hl : 1 ≤ lam) (hsA : sN ≤ 2 ^ A) (hqA : q * lam ≤ 2 ^ A) :
    Sp (blkL2 K Cs Cb)
      (encK s (J6Seg.PreT.RF (bS P R sN tN lam aN v (min sN (q * lam + lam)) (q * lam) 0) c))
      (encK s (J6Seg.PreT.RF (bS P R sN tN lam aN v (min sN (q * lam + lam)) (q * lam) lam)
        (Function.update c K ((J6Seg.KR.dsEnc2 b
          (J6Seg.descsOf sN tN lam (mkTables P R sN tN aN) q)).reverse ++ c K))))
      (cBL2 A lam)

Context. B-line IL, pre-tables (B5′, tabK2 layout), part 23: the block loop and chunk part A

blkL2, partA2 are blkL, partA with blkB2; the descriptors are dsEnc2 b, all at width BW A (no BH/BD, no M).

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_Defs68

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.blkL2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {K Cs Cb : Fin HS}
    (hK : K ∉ rg) (hK5 : K.val < 56) (hKC : K ≠ Cu) (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56)
    (hKs : K ≠ Cs) (hCb : Cb ∉ rg) (hCb5 : Cb.val < 56) (hKb : K ≠ Cb) (hbs : Cb ≠ Cs)
    (hbu : Cb ≠ Cu) (hwb : Cb ∉ (blkB2 K Cs).writes)
    (hcs : c Cs = []) (hcu : c Cu = []) (hcb : c Cb = [])
    {P R sN tN lam aN A b q : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A)
    (h28 : v 28 = b) (h4l : 4 * lam ≤ 2 ^ A)
    (h6 : v 6 = q) (hl : 1 ≤ lam) (hsA : sN ≤ 2 ^ A) (hqA : q * lam ≤ 2 ^ A) :
    Sp (blkL2 K Cs Cb)
      (encK s (J6Seg.PreT.RF (bS P R sN tN lam aN v (min sN (q * lam + lam)) (q * lam) 0) c))
      (encK s (J6Seg.PreT.RF (bS P R sN tN lam aN v (min sN (q * lam + lam)) (q * lam) lam)
        (Function.update c K ((J6Seg.KR.dsEnc2 b
          (J6Seg.descsOf sN tN lam (mkTables P R sN tN aN) q)).reverse ++ c K))))
      (cBL2 A lam) := 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 `J6Seg.PreT.blkL2_sp`, Solutions/J6SegILPre23.lean (lines 25–182) of the round-six development.

View graph