Round-six lemma `cntP_sp`
ProvedJ6Seg.Src.cntP_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.J6SegILSrc6):
theorem J6Seg.Src.cntP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iPre iPost iN : Fin HS}
(h1 : iPre.val < 56) (h2 : iPost.val < 56) (h3 : iN.val < 56)
(d1 : iPre ≠ 37 ∧ iPre ≠ 39) (d2 : iPost ≠ 37 ∧ iPost ≠ 39) (d3 : iN ≠ 37 ∧ iN ≠ 39)
{pre post n' A : ℕ} {L1 L2 L3 : List ℤ}
(hG1 : F iPre = (pre : ℤ) :: L1) (hG2 : F iPost = (post : ℤ) :: L2) (hG3 : F iN = (n' : ℤ) :: L3)
(hpA : pre ≤ 2 ^ A) (hqA : post ≤ 2 ^ A) (hnA : n' ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (cntP iPre iPost iN) (encK s0 F) (encK s0 (cntOut F pre post n')) (30 * uC A DD)
Context. B-line IL, source-table producers, part 6: the table loop, pass 1, the counts
Table loop (tab_loop): rep 43 (reg iN) b with n' on iN, the body at step k (index
j = n' - 1 - k, i.e. 43 holds j + 1) pushing argOf j then J6Seg.Slab.code (src j) on 44; the loop
leaves srcTab src argOf n' ++ G 44 on 44 (the table is produced last entry first).
enc_base, enc_base44: rebasing the empty-43 precondition away.
Pass 1 (selP iS iT iK iN): src = selSrc s t, argOf = fun _ => K (the caller passes
K = 2^(P'-p-1) on iK), n' on iN.
Inputs: s on iS, t on iT, K on iK, n' on iN (all Free); 0 < s,
s, t, n' ≤ 2^A, |K| ≤ 2^A, 2 ≤ A. Output: 44 := srcTab (selSrc s t) (fun _ => K) n' ++ F 44,
everything else unchanged (43 is the loop counter, restored). Theorem selP_sp, cost
(n' + 1) * (30 * uC A DD).
Counts (cntP iPre iPost iN): pushes pre on 37 (rNB), 2 post on 39 (rM),
pre * (n' * (2 post)) on 40 (rTOT). Inputs pre on iPre, post on iPost, n' on iN
(registers < 56, distinct from 37, 39, 40), all ≤ 2^A. Theorem cntP_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_Defs65 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.Src set_option maxRecDepth 20000 open IntMul NLogN NLogN.KIL Function NLogN.RS J6Seg.PreT J6Seg open J6Seg.Slab (srcTab)
theorem J6Seg.Src.cntP_sp (s0 : IState HS) (F : Fin HS → List ℤ) {iPre iPost iN : Fin HS}
(h1 : iPre.val < 56) (h2 : iPost.val < 56) (h3 : iN.val < 56)
(d1 : iPre ≠ 37 ∧ iPre ≠ 39) (d2 : iPost ≠ 37 ∧ iPost ≠ 39) (d3 : iN ≠ 37 ∧ iN ≠ 39)
{pre post n' A : ℕ} {L1 L2 L3 : List ℤ}
(hG1 : F iPre = (pre : ℤ) :: L1) (hG2 : F iPost = (post : ℤ) :: L2) (hG3 : F iN = (n' : ℤ) :: L3)
(hpA : pre ≤ 2 ^ A) (hqA : post ≤ 2 ^ A) (hnA : n' ≤ 2 ^ A) (hA : 2 ≤ A) :
Sp (cntP iPre iPost iN) (encK s0 F) (encK s0 (cntOut F pre post n')) (30 * uC A DD) := by sorry