The index updates and pops (round six, `keyTail_fsp`)

Proved

IntMul.Kappa.R6.IL2C.keyTail_fsp

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

complexity-theoryinteger-multiplicationkappa-improvement

The index updates and pops of keyProgC.

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

theorem IntMul.Kappa.R6.IL2C.keyTail_fsp {l : Lay} {K ρ G n L M Bb : ℕ} (hV : KVal l K ρ G n L M Bb)
    {s : IState HS} {G0 : Fin HS → List ℤ} {k : ℕ} (hk : k < M)
    {lm : List ℤ} (hm : G0 rm = (k : ℤ) :: lm) (hE : KEnv (encK s G0) l K ρ G n)
    {x t4 u2 y5 : ℕ} (hx : x < l.QL) (ht4 : t4 < l.QC) (hu2 : u2 < l.QC) (hy5 : y5 < l.QL) :
    FSp (.seq (.asg ky (scK kQL kSY ky rm)) (.seq (.asg ku (scK kQC kSU ku ky))
      (.seq (.push rK (scK kQC kST kt ku))
      (.seq (.pop ky) (.seq (.pop ku) (.seq (.pop kt) (.seq (.pop kx)
      (.seq (.pop IntMul.Kappa.R6.IL2C.pR) (.pop pN)))))))))
      (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t4 u2 y5))
      (encK s (Function.update G0 rK
        ((sc l.QC l.sT t4 (sc l.QC l.sU u2 (sc l.QL l.sY y5 k)) : ℕ) :: G0 rK))) (IntMul.Kappa.R6.IL2C.cTail Bb)

Context. Round six, compact controls (I2C): the run of the key program

keyProgC_fsp: keyProgC pushes keyC l K ρ G n L k on rK (all other registers restored). The pushes are keyPush_fsp (part A), the eleven updates keyMid_fsp (part B); here the index updates and pops (keyTail_fsp) and the assembly.

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_Defs21

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C
open NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul NLogN.RS

Formal statement

theorem IntMul.Kappa.R6.IL2C.keyTail_fsp {l : Lay} {K ρ G n L M Bb : ℕ} (hV : KVal l K ρ G n L M Bb)
    {s : IState HS} {G0 : Fin HS → List ℤ} {k : ℕ} (hk : k < M)
    {lm : List ℤ} (hm : G0 rm = (k : ℤ) :: lm) (hE : KEnv (encK s G0) l K ρ G n)
    {x t4 u2 y5 : ℕ} (hx : x < l.QL) (ht4 : t4 < l.QC) (hu2 : u2 < l.QC) (hy5 : y5 < l.QL) :
    FSp (.seq (.asg ky (scK kQL kSY ky rm)) (.seq (.asg ku (scK kQC kSU ku ky))
      (.seq (.push rK (scK kQC kST kt ku))
      (.seq (.pop ky) (.seq (.pop ku) (.seq (.pop kt) (.seq (.pop kx)
      (.seq (.pop IntMul.Kappa.R6.IL2C.pR) (.pop pN)))))))))
      (encK s (IntMul.Kappa.R6.IL2C.KS G0 n ((2 : ℤ) ^ G) x t4 u2 y5))
      (encK s (Function.update G0 rK
        ((sc l.QC l.sT t4 (sc l.QC l.sU u2 (sc l.QL l.sY y5 k)) : ℕ) :: G0 rK))) (IntMul.Kappa.R6.IL2C.cTail Bb) := 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 `IntMul.Kappa.R6.IL2C.keyTail_fsp`, Solutions/R6IL2CKeyRun.lean (lines 21–154) of the round-six development.

View graph