A call (round six, `callC_sp`)

Proved

J6Seg.PreT.callC_sp

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

complexity-theoryinteger-multiplicationkappa-improvement

A call.

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

theorem J6Seg.PreT.callC_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {d : Fin HS} (hd : d ∈ rg)
    {e16 e17 e18 e27 : Ex HS} (h16 : InRg e16) (h17 : InRg e17) (h18 : InRg e18) (h27 : InRg e27)
    (o16 : e16.ok (encK s (J6Seg.PreT.RF v c))) (o17 : e17.ok (encK s (J6Seg.PreT.RF v c)))
    (o18 : e18.ok (encK s (J6Seg.PreT.RF v c))) (o27 : e27.ok (encK s (J6Seg.PreT.RF v c)))
    {a16 a17 a18 a27 : ℕ} (v16 : e16.eval (encK s (J6Seg.PreT.RF v c)) = a16)
    (v17 : e17.eval (encK s (J6Seg.PreT.RF v c)) = a17) (v18 : e18.eval (encK s (J6Seg.PreT.RF v c)) = a18)
    (v27 : e27.eval (encK s (J6Seg.PreT.RF v c)) = a27)
    {prog : RS} {r : ℤ} {C : ℕ}
    (hprog : ∀ (t : IState HS) (L16 L17 L18 L27 : List Item), t.G 16 = .int a16 :: L16 →
      t.G 17 = .int a17 :: L17 → t.G 18 = .int a18 :: L18 → t.G 27 = .int a27 :: L27 →
      prog.ok t ∧ prog.run t = t.upd 19 (.int r :: t.G 19) ∧ prog.cost t ≤ C)
    {V : Fin HS → ℕ} {B : ℕ} (b16 : ∀ j ∈ e16.regs, |v j| ≤ V j) (b17 : ∀ j ∈ e17.regs, |v j| ≤ V j)
    (b18 : ∀ j ∈ e18.regs, |v j| ≤ V j) (b27 : ∀ j ∈ e27.regs, |v j| ≤ V j)
    (m16 : mg V e16 < 2 ^ B) (m17 : mg V e17 < 2 ^ B) (m18 : mg V e18 < 2 ^ B)
    (m27 : mg V e27 < 2 ^ B) (hr : zsz r ≤ B) (hvd : zsz (v d) ≤ B) :
    Sp (callC d e16 e17 e18 e27 prog) (encK s (J6Seg.PreT.RF v c)) (encK s (J6Seg.PreT.RF (Function.update v d r) c))
      (cCall e16 e17 e18 e27 B C)

Context. B-line IL, pre-tables (B5), part 3: calls of the library number programs

callC d e16 e17 e18 e27 prog: push the four inputs on 16, 17, 18, 27, run prog (which pushes its result on 19 and leaves everything else), move the result into register d ∈ rg, pop. callC_sp: generic; enC_sp / epC_sp: v d := expNeg n k j / expPos n k j σ.

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.PreT
open IntMul NLogN NLogN.KIL NLogN.RS IntMul.HvdH

Formal statement

theorem J6Seg.PreT.callC_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {d : Fin HS} (hd : d ∈ rg)
    {e16 e17 e18 e27 : Ex HS} (h16 : InRg e16) (h17 : InRg e17) (h18 : InRg e18) (h27 : InRg e27)
    (o16 : e16.ok (encK s (J6Seg.PreT.RF v c))) (o17 : e17.ok (encK s (J6Seg.PreT.RF v c)))
    (o18 : e18.ok (encK s (J6Seg.PreT.RF v c))) (o27 : e27.ok (encK s (J6Seg.PreT.RF v c)))
    {a16 a17 a18 a27 : ℕ} (v16 : e16.eval (encK s (J6Seg.PreT.RF v c)) = a16)
    (v17 : e17.eval (encK s (J6Seg.PreT.RF v c)) = a17) (v18 : e18.eval (encK s (J6Seg.PreT.RF v c)) = a18)
    (v27 : e27.eval (encK s (J6Seg.PreT.RF v c)) = a27)
    {prog : RS} {r : ℤ} {C : ℕ}
    (hprog : ∀ (t : IState HS) (L16 L17 L18 L27 : List Item), t.G 16 = .int a16 :: L16 →
      t.G 17 = .int a17 :: L17 → t.G 18 = .int a18 :: L18 → t.G 27 = .int a27 :: L27 →
      prog.ok t ∧ prog.run t = t.upd 19 (.int r :: t.G 19) ∧ prog.cost t ≤ C)
    {V : Fin HS → ℕ} {B : ℕ} (b16 : ∀ j ∈ e16.regs, |v j| ≤ V j) (b17 : ∀ j ∈ e17.regs, |v j| ≤ V j)
    (b18 : ∀ j ∈ e18.regs, |v j| ≤ V j) (b27 : ∀ j ∈ e27.regs, |v j| ≤ V j)
    (m16 : mg V e16 < 2 ^ B) (m17 : mg V e17 < 2 ^ B) (m18 : mg V e18 < 2 ^ B)
    (m27 : mg V e27 < 2 ^ B) (hr : zsz r ≤ B) (hvd : zsz (v d) ≤ B) :
    Sp (callC d e16 e17 e18 e27 prog) (encK s (J6Seg.PreT.RF v c)) (encK s (J6Seg.PreT.RF (Function.update v d r) c))
      (cCall e16 e17 e18 e27 B C) := 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.PreT.callC_sp`, Solutions/J6SegILPre3.lean (lines 44–125) of the round-six development.

View graph