The pass on the pair lane (round six, `passP_runs`)

Proved

J6Seg.Slab.passP_runs

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

complexity-theoryinteger-multiplicationkappa-improvement

The pass on the pair lane.

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

theorem J6Seg.Slab.passP_runs
    (H : UnitsOK (I := I) (iprog := iprog) linP OkU OkA KG g dr rd it bk cdr crd cit cbk)
    (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ℤ × ℤ)) (l l₂ : List ℤ)
    (hF0 : F 0 = xs.map Prod.fst ++ l) (hFZ : F rZ = xs.map Prod.snd ++ l₂)
    (hK : ∀ C CU OP ARG ACC, KG (skS (update (update F 0 l) rZ l₂) C CU OP ARG ACC))
    (hA : F lA = []) (hC : F lC = []) (hD : F lD = []) (cs : List (ℤ × ℤ)) (RC : List ℤ)
    (hFC : F rC = flatC cs ++ RC) (hACC : F rACC = [])
    {m : ℕ} {LM : List ℤ} (hM : F rM = (m : ℤ) :: LM) {LN : List ℤ}
    (hN : F rNC = (cs.length : ℤ) :: LN) {Ba : ℕ} (hcs : CmdsOK OkA Ba cs) (n : ℕ)
    (hV : VC n cs 0) (hND : nDrop cs = n) (pre : ℕ) {LB : List ℤ}
    (hB : F rNB = (pre : ℤ) :: LB) (hxs : xs.length = pre * (n * m)) (hok : ∀ u ∈ xs, OkU u)
    {LT : List ℤ} (hT : F rTOT = ((passOut m g cs n pre xs).length : ℤ) :: LT) {Bo : ℕ}
    (hBo : ∀ y ∈ passOut m g cs n pre xs, zsz y ≤ Bo) :
    IRuns I iprog (J6Seg.Slab.passP dr rd it bk) (encK s F)
      (encK s (update (update F 0 (passOut m g cs n pre xs ++ l)) rZ l₂))
      (passC pre cs.length m Ba (cdr + crd + cit + cbk) (passOut m g cs n pre xs).length Bo)

Context. B-line IL, B1 (streaming slab pass) §7: the passes on plain register states

passZ_runs (integer lane): from encK s F with F 0 = xs ++ l and the skeleton inputs (rC the control list flatC cs ++ RC, rACC empty, the counts on rNB rNC rM rTOT, the rptX counters empty) the pass leaves passOut … ++ l on stack 0, everything else as it was.
passP_runs (pair lane): the same with F 0 = xs.map fst ++ l, F rZ = xs.map snd ++ l₂; stack rZ ends as l₂.
mem_slabPass, length_slabPass: the entries and the length of a slab pass.
blockC_le, passC_le: the cost bounds blockC ≤ 20000 (L+1)(m+1)(cu+Ba+1).

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_Defs64

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.Slab
set_option maxRecDepth 20000
open IntMul NLogN NLogN.KIL Function
open NLogN.KFUU (lA lC lD cU)
open NLogN.KFT (cf3 rptX)
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
  {OkU : ℤ × ℤ → Prop} {OkA : ℤ → Prop} {KG : (Fin HS → List ℤ) → Prop} {g : ℤ → ℤ × ℤ → ℤ}
  {dr rd it bk : IStmt HS P} {cdr crd cit cbk : ℕ}

Formal statement

theorem J6Seg.Slab.passP_runs
    (H : UnitsOK (I := I) (iprog := iprog) linP OkU OkA KG g dr rd it bk cdr crd cit cbk)
    (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ℤ × ℤ)) (l l₂ : List ℤ)
    (hF0 : F 0 = xs.map Prod.fst ++ l) (hFZ : F rZ = xs.map Prod.snd ++ l₂)
    (hK : ∀ C CU OP ARG ACC, KG (skS (update (update F 0 l) rZ l₂) C CU OP ARG ACC))
    (hA : F lA = []) (hC : F lC = []) (hD : F lD = []) (cs : List (ℤ × ℤ)) (RC : List ℤ)
    (hFC : F rC = flatC cs ++ RC) (hACC : F rACC = [])
    {m : ℕ} {LM : List ℤ} (hM : F rM = (m : ℤ) :: LM) {LN : List ℤ}
    (hN : F rNC = (cs.length : ℤ) :: LN) {Ba : ℕ} (hcs : CmdsOK OkA Ba cs) (n : ℕ)
    (hV : VC n cs 0) (hND : nDrop cs = n) (pre : ℕ) {LB : List ℤ}
    (hB : F rNB = (pre : ℤ) :: LB) (hxs : xs.length = pre * (n * m)) (hok : ∀ u ∈ xs, OkU u)
    {LT : List ℤ} (hT : F rTOT = ((passOut m g cs n pre xs).length : ℤ) :: LT) {Bo : ℕ}
    (hBo : ∀ y ∈ passOut m g cs n pre xs, zsz y ≤ Bo) :
    IRuns I iprog (J6Seg.Slab.passP dr rd it bk) (encK s F)
      (encK s (update (update F 0 (passOut m g cs n pre xs ++ l)) rZ l₂))
      (passC pre cs.length m Ba (cdr + crd + cit + cbk) (passOut m g cs n pre xs).length Bo) := 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.Slab.passP_runs`, Solutions/J6SegILSlab7.lean (lines 71–118) of the round-six development.

View graph