Round-six lemma `lgB_step`
ProvedJ6A.PA.lgB_stepAn 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.J6AIL8):
theorem J6A.PA.lgB_step {v : Vr} {c : Cs} (hv : BV W v) {m k : ℕ} (hm : 1 ≤ m) (hmW : m ≤ W)
(hv7 : v 7 = m) (hv20 : v 20 = 2 ^ k) (hv8 : v 8 = 2 ^ min k (Nat.log 2 m))
(hv22 : v 22 = ((min k (Nat.log 2 m) : ℕ) : ℤ)) (hk : k < m) :
Rn lgB v c (· = Function.update (Function.update (Function.update v 20 (2 ^ (k + 1))) 8
(2 ^ min (k + 1) (Nat.log 2 m))) 22 ((min (k + 1) (Nat.log 2 m) : ℕ) : ℤ)) c (cLg W)
Context. A lines, IL side 8: the parameter block parA
From the axis descriptor [k, pre, post, s, t, p, α, d] on dA = 31 the register file gets
1 = pre, 2 = post, 3 = s, 4 = t, 5 = p, 6 = α, 7 = m = sWidth p α,
8 = H = 2^⌊log₂ m⌋, 9 = W = H + m + 3, 10 = t / 16H, 11 = 8H, 12 = ⌊log₂ m⌋ + 3
(m by a counting loop for ⌊√p⌋, H and ⌊log₂ m⌋ by a doubling loop). Rn.parA.
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_Defs63
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open J6A J6A.PA
open IntMul NLogN NLogN.KIL NLogN.RS J6Seg.PJ IntMul.HvdH
variable {W : ℕ}
theorem J6A.PA.lgB_step {v : Vr} {c : Cs} (hv : BV W v) {m k : ℕ} (hm : 1 ≤ m) (hmW : m ≤ W)
(hv7 : v 7 = m) (hv20 : v 20 = 2 ^ k) (hv8 : v 8 = 2 ^ min k (Nat.log 2 m))
(hv22 : v 22 = ((min k (Nat.log 2 m) : ℕ) : ℤ)) (hk : k < m) :
Rn lgB v c (· = Function.update (Function.update (Function.update v 20 (2 ^ (k + 1))) 8
(2 ^ min (k + 1) (Nat.log 2 m))) 22 ((min (k + 1) (Nat.log 2 m) : ℕ) : ℤ)) c (cLg W) := by sorry