The native set-up (round six, `natUp_sp`)
ProvedJ6Seg.ATab.natUp_spThe native set-up.
The following holds (Lean statement, in the scope of module Solutions.J6AILTab10):
theorem J6Seg.ATab.natUp_sp {W k pre post s t p α d pkA pkC bA bC B : ℕ} (st : IState HS)
(Zn : Fin HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
(hO : ∀ i, (oN i).val < 31 ∨ (oN i).val = 55) (hZ : Zn.val = 49 ∨ Zn.val = 55)
(hZo : ∀ i, oN i ≠ Zn)
(hdL : ∀ x ∈ J6A.PA.dL k pre post s t p α d, |x| < 2 ^ W) (hp1 : 1 ≤ p) (hα1 : 1 ≤ α)
(hmW : sWidth p α + 4 ≤ W) (hP : PBnd W p t α pkA pkC bA bC) (hA : ABnd W p s t α)
(hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W)
(hdB : Bnd B (J6A.PA.dL k pre post s t p α d)) (h8 : zsz 8 ≤ B)
(hvB : ∀ a ∈ vsA (p + 2) (pkA * p + pkC + 1) (Nat.log 2 (sWidth p α) + 3) pre (ncA p t α)
post, zsz a ≤ B)
(hlB : zsz ((tabA p s t α (pkA * p + pkC) (bA * p + bC)).length : ℤ) ≤ B)
(hTB : Bnd B (tabA p s t α (pkA * p + pkC) (bA * p + bC))) :
Sp (natUp pkA pkC bA bC Zn oN) (encK st (F0 Zn (J6A.PA.dL k pre post s t p α d)))
(encK st (extend oN (kerV p s t α (pkA * p + pkC) (bA * p + bC) pre post)
(F0 Zn (J6A.PA.dL k pre post s t p α d))))
(cNat W p t α pkA pkC bA bC B (tabA p s t α (pkA * p + pkC) (bA * p + bC)).length)
Context. A lines, table set-up, part 10: the native set-up program
natUp Zn oN: move the descriptor Zn → 54 → 31, run the core (J6AILTab9), move the table
43 → 41, distribute with B5's distAll oN, move the descriptor back 31 → 54 → Zn.
natUp_sp: from the descriptor alone on Zn to the A register file kerV … on oN,
for any layout with oN i < 31 or = 55 (injective) and Zn ∈ {49, 55}, Zn ∉ range oN
(the layout of B5's nativeLayout).
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.natUp_sp {W k pre post s t p α d pkA pkC bA bC B : ℕ} (st : IState HS)
(Zn : Fin HS) (oN : Fin 19 → Fin HS) (hinj : Injective oN)
(hO : ∀ i, (oN i).val < 31 ∨ (oN i).val = 55) (hZ : Zn.val = 49 ∨ Zn.val = 55)
(hZo : ∀ i, oN i ≠ Zn)
(hdL : ∀ x ∈ J6A.PA.dL k pre post s t p α d, |x| < 2 ^ W) (hp1 : 1 ≤ p) (hα1 : 1 ≤ α)
(hmW : sWidth p α + 4 ≤ W) (hP : PBnd W p t α pkA pkC bA bC) (hA : ABnd W p s t α)
(hrW : 2 * (4 * J6A.WA p α (HAx p α) + 4 * HAx p α) < 2 ^ W)
(hdB : Bnd B (J6A.PA.dL k pre post s t p α d)) (h8 : zsz 8 ≤ B)
(hvB : ∀ a ∈ vsA (p + 2) (pkA * p + pkC + 1) (Nat.log 2 (sWidth p α) + 3) pre (ncA p t α)
post, zsz a ≤ B)
(hlB : zsz ((tabA p s t α (pkA * p + pkC) (bA * p + bC)).length : ℤ) ≤ B)
(hTB : Bnd B (tabA p s t α (pkA * p + pkC) (bA * p + bC))) :
Sp (natUp pkA pkC bA bC Zn oN) (encK st (F0 Zn (J6A.PA.dL k pre post s t p α d)))
(encK st (extend oN (kerV p s t α (pkA * p + pkC) (bA * p + bC) pre post)
(F0 Zn (J6A.PA.dL k pre post s t p α d))))
(cNat W p t α pkA pkC bA bC B (tabA p s t α (pkA * p + pkC) (bA * p + bC)).length) := by sorry