The copy on managed states (round six, `cpyD_sp`)

Proved

IntMul.Kappa.R6.cpyD_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The copy on managed states.

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

theorem IntMul.Kappa.R6.cpyD_sp {Z X : Fin HS} (hZX : Z ≠ X) (hZ5 : Z.val < 56) (hX5 : X.val < 56)
    (hZy : Z ≠ yC) (hZc : Z ≠ cC) (hXy : X ≠ yC) (hXc : X ≠ cC) (hXd : X ≠ zDd) (hZd : Z ≠ zDd)
    (s : IState HS) (f : Fin HS → List ℤ) (desc : List ℤ) (hfZ : f Z = desc) (hfX : f X = [])
    (hfY : f yC = []) (hfC : f cC = []) (hfD : f zDd = []) (k c dv B : ℕ)
    (hdv : (encK s f).top zDd = dv) (hdi : (encK s f).IsInt zDd) (hlen : desc.length = k * dv + c)
    (hB1 : k * dv + c < 2 ^ B) (hB2 : dv < 2 ^ B) (hB : Bnd B desc) :
    Sp (cpyD Z X k c) (encK s f) (encK s (Function.update f X desc))
      (2 * (2 * k + 2) * 2000 * (B + 2) + desc.length * (40000 * (B + 2) + 30) + 64)

Context. Round-six machine: copying a stored descriptor

The setup leaves the descriptors of the interface calls on zPh, zLn, zCh (BaseOK6). Before a call, cpyD Z X k c copies the k d + c integers on top of Z onto the builder stack X and leaves Z as it was (d from zDd; scratch 40, counter 41): mvK Z 40 41 n moves them to 40 reversed, then a counted loop pushes each one back on Z and on X.

cpyD_sp: the specification on managed states.
cpyD_run: the form callW_I uses: from any state with the descriptor on top of Z.

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_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.KIL NLogN.RS

Formal statement

theorem IntMul.Kappa.R6.cpyD_sp {Z X : Fin HS} (hZX : Z ≠ X) (hZ5 : Z.val < 56) (hX5 : X.val < 56)
    (hZy : Z ≠ yC) (hZc : Z ≠ cC) (hXy : X ≠ yC) (hXc : X ≠ cC) (hXd : X ≠ zDd) (hZd : Z ≠ zDd)
    (s : IState HS) (f : Fin HS → List ℤ) (desc : List ℤ) (hfZ : f Z = desc) (hfX : f X = [])
    (hfY : f yC = []) (hfC : f cC = []) (hfD : f zDd = []) (k c dv B : ℕ)
    (hdv : (encK s f).top zDd = dv) (hdi : (encK s f).IsInt zDd) (hlen : desc.length = k * dv + c)
    (hB1 : k * dv + c < 2 ^ B) (hB2 : dv < 2 ^ B) (hB : Bnd B desc) :
    Sp (cpyD Z X k c) (encK s f) (encK s (Function.update f X desc))
      (2 * (2 * k + 2) * 2000 * (B + 2) + desc.length * (40000 * (B + 2) + 30) + 64) := 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.cpyD_sp`, Solutions/R6MCpy.lean (lines 101–211) of the round-six development.

View graph