Round-six lemma `dot_body`
ProvedJ6Seg.JK.dot_bodyAn auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.
The following holds (Lean statement, in the scope of module Solutions.J6SegILJKer3):
theorem J6Seg.JK.dot_body {M : MulSpec} {Xb Φm Bx : ℕ} (hMB : MulBnd M Xb Φm) (hX : XOK X)
(s : IState HS) {lp lp1 : List ℤ} (hPX : F PX = []) (hrP : F rP = 2 ^ P :: lp)
(hrP1 : F rP1 = 2 ^ (P + 1) :: lp1) (N k : ℕ) (hk : k < cs.length)
(hca : cs.length ≤ acc.length) (hc : zsz cs[k] ≤ Xb) (ha : zsz (acc[k]'(by omega)) ≤ Xb)
(hXB : 2 * Xb + 3 ≤ Bx) (hPB : P + 3 ≤ Bx) (hS0 : zsz (S0 + dotF P (cs.take k) acc) ≤ Bx)
(hS1 : zsz (S0 + dotF P (cs.take (k + 1)) acc) ≤ Bx) :
MSp M (kD X) (encK s (update (J6Seg.JK.dSt P F X cs acc R T0 S0 Ls k) CD [(N : ℤ) - k]))
(encK s (update (J6Seg.JK.dSt P F X cs acc R T0 S0 Ls (k + 1)) CD [(N : ℤ) - k]))
(Φm + 10 ^ 5 * (Bx + 2))
Context. B-line IL, the J kernel (B4), part 3: the dot loop
dotP X: with the count c = |cs| on top of CNT, the coefficients cs ++ R on the
table stack dTJ and the accumulator acc (c ≤ |acc|) on X, it adds dotF P cs acc to
the top of SUM, moves cs (reversed) onto the consumed-table stack TT and leaves X as it
was (dotP_spec). Every product goes through the multiplication procedure (RM.mul); the
rounding rs P is linear work (rsE: ⌊(2x + 2^P) / 2^{P+1}⌋ by tdiv / tmod and a sign
test, with the rulers 2^P, 2^{P+1} on rP, rP1). Cost: (c + 1) · uC Φm Bx Bc.
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_Defs66
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6Seg J6Seg.JK
open IntMul NLogN NLogN.KIL Function
variable (P : ℕ) (F : Fin HS → List ℤ) (X : Fin HS) (cs acc R T0 : List ℤ) (S0 : ℤ) (Ls : List ℤ)
variable {P F X cs acc R T0 S0 Ls}
theorem J6Seg.JK.dot_body {M : MulSpec} {Xb Φm Bx : ℕ} (hMB : MulBnd M Xb Φm) (hX : XOK X)
(s : IState HS) {lp lp1 : List ℤ} (hPX : F PX = []) (hrP : F rP = 2 ^ P :: lp)
(hrP1 : F rP1 = 2 ^ (P + 1) :: lp1) (N k : ℕ) (hk : k < cs.length)
(hca : cs.length ≤ acc.length) (hc : zsz cs[k] ≤ Xb) (ha : zsz (acc[k]'(by omega)) ≤ Xb)
(hXB : 2 * Xb + 3 ≤ Bx) (hPB : P + 3 ≤ Bx) (hS0 : zsz (S0 + dotF P (cs.take k) acc) ≤ Bx)
(hS1 : zsz (S0 + dotF P (cs.take (k + 1)) acc) ≤ Bx) :
MSp M (kD X) (encK s (update (J6Seg.JK.dSt P F X cs acc R T0 S0 Ls k) CD [(N : ℤ) - k]))
(encK s (update (J6Seg.JK.dSt P F X cs acc R T0 S0 Ls (k + 1)) CD [(N : ℤ) - k]))
(Φm + 10 ^ 5 * (Bx + 2)) := by sorry