The output item (round six, `itO_ok`)
ProvedJ6Seg.Slab.itO_okThe output item.
The following holds (Lean statement, in the scope of module Solutions.J6SegILSlab6):
theorem J6Seg.Slab.itO_ok {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) (Bu Ba k₁ k₂ : ℕ) :
ItOK (I := I) (iprog := iprog) linP (OkP Bu) (fun a => zsz a ≤ Ba) (KO k₁ k₂)
(outG k₁ k₂) (itO pM) (cItO (Bu + Ba + 2) k₁ k₂)
Context. B-line IL, B1 (streaming slab pass) §6: the pair lane and the output item (pass 7)
The pair lane linP inp tmp G (units (y, y₂) : ℤ × ℤ, the zipped input): first components
on stack 0 / temps rT = 50, second components on rZ = 53 / temps rT2 = 51. Units:
rdP = mv 0 rT; mv rZ rT2, bkP (reverse), drP = drop 0; drop rZ.
The output item itO pM (constants 2^k₁ on rK1 = 41, 2^k₂ on rK2 = 42, scratch
43, 46, 54, multiplication via mulC pM / ARGM = 55):
g a (y, y₂) = (a * ((y - y₂) / 2^k₁)).tdiv (2^k₂) (outG), i.e. outE with a = d̃_l,
k₁ = P - p, k₂ = p. The floor division is the truncating split corrected by the sign of
the remainder; the cost is O(cU Z) with Z = Bu + Ba + 2 (one multiplication).
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_R6_Defs64
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.Slab
set_option maxRecDepth 20000
set_option maxHeartbeats 1000000
open IntMul NLogN NLogN.KIL Function
open NLogN.KFUU (lA lC lD cU)
open NLogN.KFT (cf3 rptX)
variable {P : ℕ} {I : List Sym} {iprog : Fin P → IStmt HS P}
theorem J6Seg.Slab.itO_ok {pM : Fin P} (hM : MulOK I iprog pM NLogN.KFUU.MS) (Bu Ba k₁ k₂ : ℕ) :
ItOK (I := I) (iprog := iprog) linP (OkP Bu) (fun a => zsz a ≤ Ba) (KO k₁ k₂)
(outG k₁ k₂) (itO pM) (cItO (Bu + Ba + 2) k₁ k₂) := by sorry