Round-six lemma `corrLC_runs`
ProvedIntMul.Kappa.R6.IL2C.corrLC_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.R6IL2CCorrU):
theorem IntMul.Kappa.R6.IL2C.corrLC_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
{l : Lay} {K ρ G n L B : ℕ} (hB : 1 ≤ B)
(hV : KVal l K ρ G n L l.M (zsz ((l.M * B : ℕ) : ℤ) + 3))
(t : IState HS) (recs : ℕ → List ℤ) (hlen : ∀ m, (recs m).length = B)
(hbits : ∀ m, Bnd 1 (recs m)) (R0 : List Item) (h0 : t.G 0 = ints (flR recs l.M) ++ R0)
(hE : KEnv t l K ρ G n) {eB eM eA : Ex HS} {Bb : ℕ}
(hsz : ((corrPlC eB eM eA).map fun p => p.2.size + 1).sum ≤ 30)
(n1 : NoLow eB) (n2 : NoLow eM) (n3 : NoLow eA)
(E1 : ESp eB t Bb (B : ℤ)) (E2 : ESp eM t Bb (l.M : ℤ))
(E3 : ESp eA t Bb (zsz ((l.M * B : ℕ) : ℤ) : ℤ)) :
IRuns I iprog (corrLC eB eM eA) t
(t.upd 0 (ints (flR (fun d => recs (corrC l K ρ G n L d)) l.M) ++ R0))
(30 * 10 ^ 7 * (Bb + 2) ^ 2 + 1 +
400 * cCorrG (cKeyC (zsz ((l.M * B : ℕ) : ℤ) + 3) n) B l.M (zsz ((l.M * B : ℕ) : ℤ))
(nMv (keyC l K ρ G n L) l.M) (zsz ((l.M * B : ℕ) : ℤ) + 3) +
(3 * (2 * Bb + 2) + 1))
Context. Round six, compact controls (I2C): the register-driven correction
corrV kp is corrG kp B M A with B, M, A read from the registers 1, 2, 3;
corrVC = corrV keyProgC; corrLC eB eM eA pushes the three parameters and runs it.
corrLC_runs: on flR recs M (layout in the registers, KEnv), corrLC computes
flR (recs ∘ corrC) M, where corrC = stepP (Sfw ∘ TlS) inverts the key keyC.
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 NLogN NLogN.KFL NLogN.KIL NLogN.KFD NLogN.KFW NLogN.KFX IntMul NLogN.RS NLogN.KFW.RS AModel
theorem IntMul.Kappa.R6.IL2C.corrLC_runs {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp}
{l : Lay} {K ρ G n L B : ℕ} (hB : 1 ≤ B)
(hV : KVal l K ρ G n L l.M (zsz ((l.M * B : ℕ) : ℤ) + 3))
(t : IState HS) (recs : ℕ → List ℤ) (hlen : ∀ m, (recs m).length = B)
(hbits : ∀ m, Bnd 1 (recs m)) (R0 : List Item) (h0 : t.G 0 = ints (flR recs l.M) ++ R0)
(hE : KEnv t l K ρ G n) {eB eM eA : Ex HS} {Bb : ℕ}
(hsz : ((corrPlC eB eM eA).map fun p => p.2.size + 1).sum ≤ 30)
(n1 : NoLow eB) (n2 : NoLow eM) (n3 : NoLow eA)
(E1 : ESp eB t Bb (B : ℤ)) (E2 : ESp eM t Bb (l.M : ℤ))
(E3 : ESp eA t Bb (zsz ((l.M * B : ℕ) : ℤ) : ℤ)) :
IRuns I iprog (corrLC eB eM eA) t
(t.upd 0 (ints (flR (fun d => recs (corrC l K ρ G n L d)) l.M) ++ R0))
(30 * 10 ^ 7 * (Bb + 2) ^ 2 + 1 +
400 * cCorrG (cKeyC (zsz ((l.M * B : ℕ) : ℤ) + 3) n) B l.M (zsz ((l.M * B : ℕ) : ℤ))
(nMv (keyC l K ρ G n L) l.M) (zsz ((l.M * B : ℕ) : ℤ) + 3) +
(3 * (2 * Bb + 2) + 1)) := by sorry