Counted loop with an item-language body (round six, `irep`)

Proved

NLogN.KIL.IRuns.irep

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

complexity-theoryinteger-multiplicationkappa-improvement

Counted loop with an item-language body (managed states, as Sp.rep).

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

theorem NLogN.KIL.IRuns.irep {C : Fin HS} {n : Ex HS} {body : IStmt HS Pp} {s : IState HS}
    {F : ℕ → Fin HS → List ℤ} {N B c : ℕ} (hB1 : 1 ≤ B) (hC5 : C.val < 56) (hC : ∀ k, F k C = [])
    (hnc : n.Clean) (hno : n.ok (encK s (F 0))) (hnl : n.Lin) (hnb : n.Bnd (encK s (F 0)) B)
    (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, IRuns I iprog body (encK s (Function.update (F k) C [(N : ℤ) - k]))
      (encK s (Function.update (F (k + 1)) C [(N : ℤ) - k])) c) :
    IRuns I iprog (NLogN.KIL.irep C n body) (encK s (F 0)) (encK s (F N))
      ((n.size + 1) * 2000 * (B + 2) + N * (c + 8000 * (B + 2) + 30) + (2 * B + 32))

Context. KIL6: counted loops whose body is item-language code (with procedure calls)

irep C n body is the item-language counterpart of RS.rep C n b for an arbitrary IStmt body (which may contain .calls): push the count n on the counter stack C, run body; C := C - 1 while the top of C is nonzero, pop C. IRuns.irep is the analogue of Sp.rep on managed states.

Also: Sp.asgQ (assignment of a general expression, quadratic cost) and the conversion of a stack-0 specification on t.upd 0 … states to managed states (Sp.top0).

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_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
import Definitions.Def_IntMul_HvdH_M_Defs8
import Definitions.Def_IntMul_MultitapeModel

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KIL
open IntMul NLogN.RS AModel AModelL12
variable {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}

Formal statement

theorem NLogN.KIL.IRuns.irep {C : Fin HS} {n : Ex HS} {body : IStmt HS Pp} {s : IState HS}
    {F : ℕ → Fin HS → List ℤ} {N B c : ℕ} (hB1 : 1 ≤ B) (hC5 : C.val < 56) (hC : ∀ k, F k C = [])
    (hnc : n.Clean) (hno : n.ok (encK s (F 0))) (hnl : n.Lin) (hnb : n.Bnd (encK s (F 0)) B)
    (hn : n.eval (encK s (F 0)) = N)
    (hb : ∀ k < N, IRuns I iprog body (encK s (Function.update (F k) C [(N : ℤ) - k]))
      (encK s (Function.update (F (k + 1)) C [(N : ℤ) - k])) c) :
    IRuns I iprog (NLogN.KIL.irep C n body) (encK s (F 0)) (encK s (F N))
      ((n.size + 1) * 2000 * (B + 2) + N * (c + 8000 * (B + 2) + 30) + (2 * B + 32)) := 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 `NLogN.KIL.IRuns.irep`, Solutions/KIL6Loop.lean (lines 49–107) of the round-six development.

View graph