Round-six lemma `rotR_runs`
ProvedIntMul.Kappa.R6.IL2C.rotR_runsAn 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.R6IL2CTab):
theorem IntMul.Kappa.R6.IL2C.rotR_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
{T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
(sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) (hfok : fok (tabGenR sgn T) = true)
{Q d1 d2 n : ℕ} {ru rv rw w0 : ℤ} (hv : TVal Q d1 d2 ru rv rw w0 Tm n Bb)
(P B w : ℕ) (zP : zsz (P : ℤ) ≤ Bb)
(t : IState HS) (xs : List ℤ) (R : List Item) (hlen : xs.length = P * Q * B)
(hbw : Bnd w xs) (h0 : t.G 0 = ints xs ++ R)
{eP eQ eB e1 e2 eu ev ew e0 en eR : Ex HS}
(hsz : ((rotPlR eP eQ eB e1 e2 eu ev ew e0 en eR).map fun p => p.2.size + 1).sum ≤ 200)
(hlow : ∀ p ∈ rotPlR eP eQ eB e1 e2 eu ev ew e0 en eR, KFX.NoLow p.2)
(EP : ESp eP t Bb (P : ℤ)) (EQ : ESp eQ t Bb (Q : ℤ)) (EB : ESp eB t Bb (B : ℤ))
(E1 : ESp e1 t Bb (d1 : ℤ)) (E2 : ESp e2 t Bb (d2 : ℤ)) (Eu : ESp eu t Bb ru)
(Ev : ESp ev t Bb rv) (Ew : ESp ew t Bb rw) (E0 : ESp e0 t Bb w0)
(En : ESp en t Bb (n : ℤ)) (ER : ESp eR t Bb Rv) :
IRuns I iprog (rotR sgn T eP eQ eB e1 e2 eu ev ew e0 en eR) t
(t.upd 0 (ints (pull [P, Q, B] [P, Q, B]
(KIL.rotAddr Q (tabE sgn tf ru rv rw w0 d1 d2 Q n)) 0 xs) ++ R))
(cRotR T Bb n P Q B w)
Context. Round six, compact controls (I2C): uniform offset tables and rotations
tabGenR sgn T pushes on stack 14 the table p ↦ (sgn · segSum tf ru rv rw w0 (p/d1) (p/d2) n) mod Q
(p = P-1, …, 0), all parameters on registers:
1: P, 2: Q, 3: d1, 5: d2, 6: ru, 7: rv, 8: rw, 9: w0, 10: n, 11: R (the term T may read R).
rotR pushes the parameters, runs the table generator and the record rotation KFC.rotF
(rotR_runs).
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_Defs21 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.IL2C open AModel NLogN NLogN.KFL NLogN.KIL NLogN.KFD IntMul NLogN.RS
theorem IntMul.Kappa.R6.IL2C.rotR_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
{T : Ex HS} {tf : ℤ → ℤ → ℤ} {Bb : ℕ} {Tm Rv : ℤ} (hT : SegTR T tf Bb Tm Rv)
(sgn : ℤ) (hs : sgn = 1 ∨ sgn = -1) (hfok : fok (tabGenR sgn T) = true)
{Q d1 d2 n : ℕ} {ru rv rw w0 : ℤ} (hv : TVal Q d1 d2 ru rv rw w0 Tm n Bb)
(P B w : ℕ) (zP : zsz (P : ℤ) ≤ Bb)
(t : IState HS) (xs : List ℤ) (R : List Item) (hlen : xs.length = P * Q * B)
(hbw : Bnd w xs) (h0 : t.G 0 = ints xs ++ R)
{eP eQ eB e1 e2 eu ev ew e0 en eR : Ex HS}
(hsz : ((rotPlR eP eQ eB e1 e2 eu ev ew e0 en eR).map fun p => p.2.size + 1).sum ≤ 200)
(hlow : ∀ p ∈ rotPlR eP eQ eB e1 e2 eu ev ew e0 en eR, KFX.NoLow p.2)
(EP : ESp eP t Bb (P : ℤ)) (EQ : ESp eQ t Bb (Q : ℤ)) (EB : ESp eB t Bb (B : ℤ))
(E1 : ESp e1 t Bb (d1 : ℤ)) (E2 : ESp e2 t Bb (d2 : ℤ)) (Eu : ESp eu t Bb ru)
(Ev : ESp ev t Bb rv) (Ew : ESp ew t Bb rw) (E0 : ESp e0 t Bb w0)
(En : ESp en t Bb (n : ℤ)) (ER : ESp eR t Bb Rv) :
IRuns I iprog (rotR sgn T eP eQ eB e1 e2 eu ev ew e0 en eR) t
(t.upd 0 (ints (pull [P, Q, B] [P, Q, B]
(KIL.rotAddr Q (tabE sgn tf ru rv rw w0 d1 d2 Q n)) 0 xs) ++ R))
(cRotR T Bb n P Q B w) := by sorry