The descriptor program

The descriptor program.

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

theorem NLogN.KFW.descP_run (s : IState HS) (f : Fin HS → List ℤ) (w u p q : ℕ) (sh : List ℕ) (rest : List ℤ)
    (hsh : ∀ a ∈ sh, 1 ≤ a) (hpq : p < q) (hq : q < sh.length)
    (hpu : sh.getD p 0 = 2 ^ u) (hqu : sh.getD q 0 = 2 ^ u)
    (hfD : f NLogN.KFW.dS = (w : ℤ) :: (u : ℤ) :: (p : ℤ) :: (q : ℤ) :: (sh.length : ℤ) ::
      (sh.map (fun a : ℕ => (a : ℤ)) ++ rest))
    (hfe : ∀ j ∈ [sT, NLogN.KFW.sW, sU, NLogN.KFW.sP, sG, sS, sN, xp, xq, xL, NLogN.KFW.aS, cC], f j = []) :
    FSp descP (encK s f) (encK s (regsSw f w u p q sh))
      (25 * xD sh.length (Nat.size sh.prod + w + u + 8) (Nat.size sh.prod + w + u + 8 + zsz (sh.length : ℤ)))

Context. The lemma belongs to the part KFW: reading the swap descriptor: The descriptor descSw w u p q sh = [w, u, p, q, |sh|, sh_0, …] sits on the managed stack dS. descP reads it into the registers of swWU (w, u, vol Pre, vol G, vol Suf · (w+1), N for the Gaussian array of shape sh ++ [2]) by moving it item by item to a temporary stack and back, with unary-counted loops (rep); descP_fsp.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs22.