The call of `expPosP` (round six, `callB_sp`)

Proved

J6Seg.Src.callB_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

The call of expPosP.

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

theorem J6Seg.Src.callB_sp (s0 : IState HS) (F : Fin HS → List ℤ) {e16 e17 e18 e27 : Ex HS}
    {n k jj σ A : ℕ} (hA : 2 ≤ A) (c16 : CIn s0 F A e16 n) (c17 : CIn s0 F A e17 k)
    (c18 : CIn s0 F A e18 jj) (c27 : CIn s0 F A e27 σ) (hvA : |expPos n k jj σ| ≤ 2 ^ A) :
    Sp (callB e16 e17 e18 e27) (encK s0 F) (encK s0 (update F 44 (expPos n k jj σ :: F 44)))
      ((e16.size + e17.size + e18.size + e27.size + 12) * uC A DD +
        expPosCost n (A * DD + 1) (A * DD + 1) σ)

Context. B-line IL, source-table producers, part 7: a call of expPosP

callB e16 e17 e18 e27: push the four inputs on 16, 17, 18, 27, run the library program expPosP (NLogN, output on 19), push its result on 44, pop 19, 27, 18, 17, 16. callB_sp: on encK s0 F, with the expressions' registers outside 16, 17, 18, 19, 27, 44, the result is update F 44 (expPos n k j σ :: F 44); every other stack (including 16–19, 27) is unchanged.

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 IntMul.HvdH

Formal statement

theorem J6Seg.Src.callB_sp (s0 : IState HS) (F : Fin HS → List ℤ) {e16 e17 e18 e27 : Ex HS}
    {n k jj σ A : ℕ} (hA : 2 ≤ A) (c16 : CIn s0 F A e16 n) (c17 : CIn s0 F A e17 k)
    (c18 : CIn s0 F A e18 jj) (c27 : CIn s0 F A e27 σ) (hvA : |expPos n k jj σ| ≤ 2 ^ A) :
    Sp (callB e16 e17 e18 e27) (encK s0 F) (encK s0 (update F 44 (expPos n k jj σ :: F 44)))
      ((e16.size + e17.size + e18.size + e27.size + 12) * uC A DD +
        expPosCost n (A * DD + 1) (A * DD + 1) σ) := 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.callB_sp`, Solutions/J6SegILSrc7.lean (lines 123–182) of the round-six development.

View graph