Round-six lemma `sp_jloop`
ProvedIntMul.Kappa.R6.sp_jloopAn 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.R6SJ):
theorem IntMul.Kappa.R6.sp_jloop (P : Prm) (n : ℕ) (s : IState HS) (f : Fin HS → List ℤ) (Aa Bb : ℕ)
(l25 l33 l34 l36 : List ℤ) (h48 : f 48 = []) (h49 : f 49 = []) (h50 : f 50 = [])
(h25 : f 25 = (dP6 P n : ℤ) :: l25) (h33 : f 33 = (hN6 P n : ℤ) :: l33)
(h34 : f 34 = (dpN6 P n : ℤ) :: l34) (h36 : f 36 = 1 :: l36)
(hd : 1 ≤ dP6 P n) (hl : 2 ≤ ℓP6 P n) (hW : WinOK6 P n) (hAa : 2 ≤ Aa)
(hcA : 2 ^ ℓP6 P n * 2 ^ ℓP6 P n ≤ Aa) (hPA : 2 * 2 ^ (ℓP6 P n * dP6 P n) ≤ Aa)
(hsA : 8 * (dP6 P n + ℓP6 P n) ≤ Aa) (hB : Aa ^ 6 < 2 ^ Bb) :
Sp jR (encK s f)
(encK s (update (update (update f 36 ((PP6 P n (dP6 P n) : ℤ) :: l36)) 37
(saL P n (dP6 P n) ++ f 37)) 38 (maL P n (dP6 P n) ++ f 38)))
((dP6 P n * (cJ (2 ^ ℓP6 P n) + 1) + 1) * kU Bb)
Context. Round-six setup, part 4: the source loop
jR = rep 48 (reg 25) jB: for j = 0, …, d-1 (j = d - counter), the body computes
t_j = 2^{h + [d' ≤ j]} (39), w_j = t_j / (8d²) (40), A_j = t_j - 2 w_j (41), selects
s_j by the candidate loop (42), computes μ_j = P^{-1} mod s_j (46), pushes s_j on 37
and μ_j on 38, and multiplies the running product P (36) by s_j.
sp_jloop: from P = 1 the loop leaves P = ∏ s_j, 37 = [s_{d-1}, …, s_0] and
38 = [μ_{d-1}, …, μ_0] (above the old contents).
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_Defs69 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 open IntMul NLogN NLogN.KIL NLogN.KFM NLogN.RS Finset Function
theorem IntMul.Kappa.R6.sp_jloop (P : Prm) (n : ℕ) (s : IState HS) (f : Fin HS → List ℤ) (Aa Bb : ℕ)
(l25 l33 l34 l36 : List ℤ) (h48 : f 48 = []) (h49 : f 49 = []) (h50 : f 50 = [])
(h25 : f 25 = (dP6 P n : ℤ) :: l25) (h33 : f 33 = (hN6 P n : ℤ) :: l33)
(h34 : f 34 = (dpN6 P n : ℤ) :: l34) (h36 : f 36 = 1 :: l36)
(hd : 1 ≤ dP6 P n) (hl : 2 ≤ ℓP6 P n) (hW : WinOK6 P n) (hAa : 2 ≤ Aa)
(hcA : 2 ^ ℓP6 P n * 2 ^ ℓP6 P n ≤ Aa) (hPA : 2 * 2 ^ (ℓP6 P n * dP6 P n) ≤ Aa)
(hsA : 8 * (dP6 P n + ℓP6 P n) ≤ Aa) (hB : Aa ^ 6 < 2 ^ Bb) :
Sp jR (encK s f)
(encK s (update (update (update f 36 ((PP6 P n (dP6 P n) : ℤ) :: l36)) 37
(saL P n (dP6 P n) ++ f 37)) 38 (maL P n (dP6 P n) ++ f 38)))
((dP6 P n * (cJ (2 ^ ℓP6 P n) + 1) + 1) * kU Bb) := by sorry