The input-scaling loop (round six, `loopA`)
ProvedJ6Seg.ATab.Rn.loopAThe input-scaling loop.
The following holds (Lean statement, in the scope of module Solutions.J6AILTab2):
theorem J6Seg.ATab.Rn.loopA {W p s t α H q : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
(h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h3 : v0 3 = s) (h4 : v0 4 = t)
(h7 : v0 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)) (h10 : v0 10 = ((2 * J6A.WA p α H : ℕ) : ℤ))
(h12 : v0 12 = 2 ^ J6A.QA p)
(h25 : v0 25 = (t : ℤ) * (J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H) -
s * J6A.kcB H (J6A.kkA H q))
(hpW : 2 * p ≤ W + 1) (hN : 2 * J6A.WA p α H < 2 ^ W)
(hb1 : ∀ i < 2 * J6A.WA p α H, (J6A.aNum s t H (J6A.kkA H q)
(J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H + i) : ℤ) ≤ 2 ^ W)
(hb2 : ∀ i < 2 * J6A.WA p α H, |fA p s t α H q i| ≤ 2 ^ W) :
Rn J6Seg.ATab.loopA v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
(update c0 sS (PreT.rv (fA p s t α H q) (2 * J6A.WA p α H) ++ c0 sS))
(cFor W (2 * J6A.WA p α H) (cBodyA W))
Context. A lines, table set-up, part 2: the input-scaling table loop
The register file during the table loop (LV):
1 = 2p 2 = p/2 3 = s 4 = t 5 = 2^(2p) 6 = β = betaT (2p) α 7 = t³α²
8 = H 9 = W 11 = t²α² 12 = 2^Q 20 = 2^pk 21 = 2^b 22 = jA 23 = b·2r
(10 the loop count, 24 the block index, 25 the block offset A0 = t (j_c - W) - s k_c,
26 the loop index, 28, 29 scratch).
loopA: for i < 2W: 28 := (t-s)⁺ (A0 + t i)²; 29 := expNeg 2p (t³α²) 28; push 2^Q · 29,
i.e. it pushes aTabA … q (Rn.loopA).
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 J6Seg J6Seg.ATab open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH Function
theorem J6Seg.ATab.Rn.loopA {W p s t α H q : ℕ} {v0 : Vr} {c0 : Cs} (hv0 : BV W v0) (hc0 : c0 cI = [])
(h1 : v0 1 = ((2 * p : ℕ) : ℤ)) (h3 : v0 3 = s) (h4 : v0 4 = t)
(h7 : v0 7 = ((t ^ 3 * α ^ 2 : ℕ) : ℤ)) (h10 : v0 10 = ((2 * J6A.WA p α H : ℕ) : ℤ))
(h12 : v0 12 = 2 ^ J6A.QA p)
(h25 : v0 25 = (t : ℤ) * (J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H) -
s * J6A.kcB H (J6A.kkA H q))
(hpW : 2 * p ≤ W + 1) (hN : 2 * J6A.WA p α H < 2 ^ W)
(hb1 : ∀ i < 2 * J6A.WA p α H, (J6A.aNum s t H (J6A.kkA H q)
(J6A.jcB s t H (J6A.kkA H q) - J6A.WA p α H + i) : ℤ) ≤ 2 ^ W)
(hb2 : ∀ i < 2 * J6A.WA p α H, |fA p s t α H q i| ≤ 2 ^ W) :
Rn J6Seg.ATab.loopA v0 c0 (fun v' => (∀ j, j ∉ ([26, 28, 29] : List (Fin HS)) → v' j = v0 j) ∧ BV W v')
(update c0 sS (PreT.rv (fA p s t α H q) (2 * J6A.WA p α H) ++ c0 sS))
(cFor W (2 * J6A.WA p α H) (cBodyA W)) := by sorry