Round-six lemma `dnCore_sp`
ProvedJ6Seg.Src.dnCore_spAn 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.J6SegILSrc18):
theorem J6Seg.Src.dnCore_sp (s0 : IState HS) (F : Fin HS → List ℤ) {Cm : Fin HS} (hC5 : Cm.val < 56)
(hCm : Cm ≠ 37 ∧ Cm ≠ 38 ∧ Cm ≠ 39 ∧ Cm ≠ 40 ∧ Cm ≠ 41 ∧ Cm ≠ 42 ∧ Cm ≠ 45) (hFC : F Cm = [])
(h37 : F 37 = []) (h38 : F 38 = []) (h39 : F 39 = []) (h40 : F 40 = []) (h45 : F 45 = [])
(cs : List (ℤ × ℤ)) (pre post n' : ℕ) (K1 K2 : List ℤ) {A : ℕ}
(hcs : ∀ y ∈ flatC cs, |y| ≤ 2 ^ A) (hm : cs.length ≤ 2 ^ A) (hpre : pre ≤ 2 ^ A)
(hpost : 2 * post ≤ 2 ^ A) (htot : pre * (n' * (2 * post)) ≤ 2 ^ A) :
Sp (dnCore Cm) (encK s0 (regOut F cs pre post n' K1 K2))
(encK s0 (update (update F 41 (K1 ++ F 41)) 42 (K2 ++ F 42))) (dnC A cs.length)
Context. B-line IL, source-table producers, part 18: the tear-down
dnCore Cm: pop rNB = 37, rM = 39, rTOT = 40, pop 2 |cs| entries of rC = 45 (loop on
rNC = 38, counter Cm), pop 38. dn0 Cm = dnCore Cm; dn7 Cm also pops rK1 = 41, rK2 = 42.
From regOut F cs pre post n' K1 K2 (with empty registers in F) back to F
(dn0_sp, dn7_sp).
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_Defs70 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg open J6Seg.PreT hiding rg RF RF_in RF_out upd_RF_in upd_RF_out cE InRg open J6Seg.Slab (flatC)
theorem J6Seg.Src.dnCore_sp (s0 : IState HS) (F : Fin HS → List ℤ) {Cm : Fin HS} (hC5 : Cm.val < 56)
(hCm : Cm ≠ 37 ∧ Cm ≠ 38 ∧ Cm ≠ 39 ∧ Cm ≠ 40 ∧ Cm ≠ 41 ∧ Cm ≠ 42 ∧ Cm ≠ 45) (hFC : F Cm = [])
(h37 : F 37 = []) (h38 : F 38 = []) (h39 : F 39 = []) (h40 : F 40 = []) (h45 : F 45 = [])
(cs : List (ℤ × ℤ)) (pre post n' : ℕ) (K1 K2 : List ℤ) {A : ℕ}
(hcs : ∀ y ∈ flatC cs, |y| ≤ 2 ^ A) (hm : cs.length ≤ 2 ^ A) (hpre : pre ≤ 2 ^ A)
(hpost : 2 * post ≤ 2 ^ A) (htot : pre * (n' * (2 * post)) ≤ 2 ^ A) :
Sp (dnCore Cm) (encK s0 (regOut F cs pre post n' K1 K2))
(encK s0 (update (update F 41 (K1 ++ F 41)) 42 (K2 ++ F 42))) (dnC A cs.length) := by sorry