The block loop (round six, `loopB2_runs`)

Proved

J6Seg.KR.loopB2_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

The block loop.

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

theorem J6Seg.KR.loopB2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b pk φD B BH : ℕ} {φT : ℕ → ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ n, ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT n)
    (hb : 1 ≤ b) (P : ℕ) (s : IState HS) (G : Fin HS → List ℤ) (hG : GOK P pk b G)
    (tdi : TB (2 ^ pk) (G TDI)) (tgi : TB (2 ^ pk) (G TGI)) (tga : TB (2 ^ pk) (G TGA))
    (tdd : TB (2 ^ pk) (G TDD))
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B) (dt : List ℤ) :
    ∀ (ds : List (ℕ × List ℤ × List ℤ)) (z : List GI) (r0 o du : List ℤ),
      (∀ d ∈ ds, 1 ≤ d.1 ∧ d.2.1.length = d.1 ∧ d.2.2.length = d.1 ∧ d.1 ≤ (G TDI).length ∧
        d.1 ≤ (G TGI).length ∧ d.1 ≤ (G TGA).length ∧ d.1 ≤ (G TDD).length ∧ TB (2 ^ pk) d.2.1 ∧
        TB (2 ^ pk) d.2.2 ∧ 2 * (2 * d.1) * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧
        zsz ((2 * d.1 : ℕ) : ℤ) ≤ B ∧ (∀ v ∈ blkHdr2 d.1 b, zsz v ≤ BH)) →
      zsz (ds.length : ℤ) ≤ BH → J6Seg.KR.sumN ds ≤ z.length → chunkOK P (2 ^ pk) (G TDI) (G TGI) (G TGA) (G TDD) ds z →
      IRuns I iprog (.loop BC isPos (blkI2 pM))
        (encK s (BF G (gflat z ++ r0) [] [] o (dsEnc2 b ds ++ dt) du [] [] [] [] []
          [(ds.length : ℤ)]))
        (encK s (BF G (gflat (z.drop (J6Seg.KR.sumN ds)) ++ r0) [] [] (gflat (chunkB P (G TDI) (G TGI) (G TGA) (G TDD) ds z).reverse ++ o)
          dt ((dsEnc2 b ds).reverse ++ du) [] [] [] [] [] [0]))
        (cLoop2 pk b φD φT B BH ds)

Context. B3′, part 4: the block loop with in-kernel constants (loopB2_runs, cost cLoop2).

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_Defs66

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.KR
open IntMul NLogN NLogN.KIL NLogN.KFD NLogN.KFB NLogN.KFV
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem J6Seg.KR.loopB2_runs {M : MulSpec} {pM : Fin Pp} (hM : MulOK I iprog pM M) (hdom : ∀ x y, M.dom x y)
    {b pk φD B BH : ℕ} {φT : ℕ → ℕ} (hΦD : ∀ x y : ℤ, zsz x ≤ B → zsz y ≤ B → M.Φ x y ≤ φD)
    (hΦT : ∀ n, ∀ x y : ℤ, zsz x ≤ b * (2 * n) + 2 → zsz y ≤ b * (2 * n) + 2 → M.Φ x y ≤ φT n)
    (hb : 1 ≤ b) (P : ℕ) (s : IState HS) (G : Fin HS → List ℤ) (hG : GOK P pk b G)
    (tdi : TB (2 ^ pk) (G TDI)) (tgi : TB (2 ^ pk) (G TGI)) (tga : TB (2 ^ pk) (G TGA))
    (tdd : TB (2 ^ pk) (G TDD))
    (hBb : b + 4 ≤ B) (hBp : 2 * pk + 4 ≤ B) (hPB : P + 3 ≤ B) (dt : List ℤ) :
    ∀ (ds : List (ℕ × List ℤ × List ℤ)) (z : List GI) (r0 o du : List ℤ),
      (∀ d ∈ ds, 1 ≤ d.1 ∧ d.2.1.length = d.1 ∧ d.2.2.length = d.1 ∧ d.1 ≤ (G TDI).length ∧
        d.1 ≤ (G TGI).length ∧ d.1 ≤ (G TGA).length ∧ d.1 ≤ (G TDD).length ∧ TB (2 ^ pk) d.2.1 ∧
        TB (2 ^ pk) d.2.2 ∧ 2 * (2 * d.1) * 2 ^ (2 * pk) < 2 ^ (b - 1) ∧
        zsz ((2 * d.1 : ℕ) : ℤ) ≤ B ∧ (∀ v ∈ blkHdr2 d.1 b, zsz v ≤ BH)) →
      zsz (ds.length : ℤ) ≤ BH → J6Seg.KR.sumN ds ≤ z.length → chunkOK P (2 ^ pk) (G TDI) (G TGI) (G TGA) (G TDD) ds z →
      IRuns I iprog (.loop BC isPos (blkI2 pM))
        (encK s (BF G (gflat z ++ r0) [] [] o (dsEnc2 b ds ++ dt) du [] [] [] [] []
          [(ds.length : ℤ)]))
        (encK s (BF G (gflat (z.drop (J6Seg.KR.sumN ds)) ++ r0) [] [] (gflat (chunkB P (G TDI) (G TGI) (G TGA) (G TDD) ds z).reverse ++ o)
          dt ((dsEnc2 b ds).reverse ++ du) [] [] [] [] [] [0]))
        (cLoop2 pk b φD φT B BH ds) := 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.KR.loopB2_runs`, Solutions/J6SegKs4.lean (lines 22–83) of the round-six development.

View graph