Prove2Me

The forward pass (round six, `fwd_runs`)

Proved
J6Seg.Src.fwd_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

The forward pass.

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

theorem J6Seg.Src.fwd_runs (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iL : Fin HS} (fS : Free iS)
    (fT : Free iT) (fL : Free iL) {s t lam A : ℕ} {LS LT LL : List ℤ}
    (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGL : G iL = (lam : ℤ) :: LL)
    (h43 : G 43 = []) (hs : 0 < s) (hl : 0 < lam) (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A)
    (hlA : lam ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (.rep 43 (.reg iS) (fwdB iS iT iL)) (encK s0 (fwS G s t lam 0)) (encK s0 (fwS G s t lam s))
      ((s + 1) * (401 * uC A DD + uC A DD))

Context. B-line IL, source-table producers, part 3: ljP, the forward pass

ljP iS iT iL iW (inputs s, t, λ, w on the tops of the free stacks iS, iT, iL, iW):

  1. push the sentinel 0 on 14;
  2. forward pass rep 43 s fwdB: at step k push stF k on 14 (stE: k if k = 0, k % λ = 0 or rrZ k ≠ rrZ (k-1) + 1, else the previous top);
  3. push s on 15 (the block end eB), 0 on 31 (the count);
  4. backward pass rep 43 s bwdB (part 4): at step k (j = s - 1 - k) pop stF j from 14, push it on 32, push eB j - stF j on 33, push j on 30 and count it on 31 if nearB j, update 15 to eB (j - 1);
  5. pop 15 and the sentinel.

Here: the expressions, their values, and fwd_runs.

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_Defs65

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Src
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg
Formal statement
theorem J6Seg.Src.fwd_runs (s0 : IState HS) (G : Fin HS → List ℤ) {iS iT iL : Fin HS} (fS : Free iS)
    (fT : Free iT) (fL : Free iL) {s t lam A : ℕ} {LS LT LL : List ℤ}
    (hGS : G iS = (s : ℤ) :: LS) (hGT : G iT = (t : ℤ) :: LT) (hGL : G iL = (lam : ℤ) :: LL)
    (h43 : G 43 = []) (hs : 0 < s) (hl : 0 < lam) (hsA : s ≤ 2 ^ A) (htA : t ≤ 2 ^ A)
    (hlA : lam ≤ 2 ^ A) (hA : 2 ≤ A) :
    Sp (.rep 43 (.reg iS) (fwdB iS iT iL)) (encK s0 (fwS G s t lam 0)) (encK s0 (fwS G s t lam s))
      ((s + 1) * (401 * uC A DD + uC A DD)) := 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.Src.fwd_runs`, Solutions/J6SegILSrc3.lean (lines 178–237) of the round-six development.

View graph