One block (new header) (round six, `blk2_sp`)

One block (new header).

The following holds (Lean statement, in the scope of module Solutions.J6SegILPre22):

theorem J6Seg.PreT.blk2_sp (s : IState HS) (v : Fin HS → ℤ) (c : Fin HS → List ℤ) {K Cs : Fin HS}
    (hK : K ∉ rg) (hK5 : K.val < 56) (hKC : K ≠ Cu) (hCs : Cs ∉ rg) (hCs5 : Cs.val < 56)
    (hKs : K ≠ Cs) (hcs : c Cs = []) (hcu : c Cu = []) {P R sN tN lam aN A b st nb sn : ℕ}
    (hi : StIn2 v P R sN tN lam aN A) (hPA : P ≤ A) (TB : J6Seg.PreT.TabB P R sN tN aN lam A)
    (h28 : v 28 = b) (h4l : 4 * lam ≤ 2 ^ A)
    (h1 : v 1 = st) (h7 : v 7 = nb) (h8 : v 8 = sn) (hl : 1 ≤ lam)
    (hst : st + (1 + J6Seg.enF sN tN lam st) ≤ 2 ^ A) (hnb : nb + 1 ≤ 2 ^ A)
    (hsn : sn + (1 + J6Seg.enF sN tN lam st) ≤ 2 ^ A) :
    Sp (blkB2 K Cs) (encK s (J6Seg.PreT.RF v c))
      (encK s (J6Seg.PreT.RF (zr (Function.update (Function.update (Function.update v 1
          ((st + (1 + J6Seg.enF sN tN lam st) : ℕ) : ℤ)) 7 ((nb + 1 : ℕ) : ℤ)) 8
          ((sn + (1 + J6Seg.enF sN tN lam st) : ℕ) : ℤ)))
        (Function.update c K ((J6Seg.KR.encD2 b (dscOf P R sN tN lam aN st)).reverse ++ c K))))
      (cBlk2 A lam)

Context. B-line IL, pre-tables (B5′, tabK2 layout), part 22: the new block header and one block

• hdrP2 K Cs pushes blkHdr2 n b = [n, 2n, clog₂(2n), 2nb] (reading order, i.e. K gains its reverse) for n on 2, b on 28. clog₂(2n) is computed by λ rounds (counter Cs) of if p < 2n then (p := 2p; j := j + 1) with j on 3, p on 4. Everything is at width BW A (needs 4λ ≤ 2^A, since p = 2^j < 4n).
• blkB2 K Cs is blkB K Cs with hdrP2 in place of hdrP; blk2_sp needs no M.

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*).