HvdH machine lemma ST.stepP_spec (The recursive step, part 9: the whole program `stepP K` (generic in th)

The following holds (Lean statement, in the scope of module NLogN.HSt9):

theorem NLogN.ST.stepP_spec (M : MulSpec) {K N a b Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu Bc Bd : ℕ}
    {BS BB : ℕ → ℕ} (hA : StepArgs M K N a b Φf Φm m mm Φ Bacc Qa Bq Bx CS CB Q Bs mu Bc Bd BS BB)
    (s : IState HS) (LA LB LN : List Item) (hsA : s.G Top.XA = .int a :: LA)
    (hsB : s.G Top.XB = .int b :: LB) (hsN : s.G Top.XN = .int N :: LN) :
    Spec M (stepP K) s (((s.upd Top.XA LA).upd Top.XB LB).upd Top.XR (.int (a * b : ℕ) :: s.G Top.XR))
      (stepCost K N Φf Φm Bs CS CB Bx Q Bc Bd)

Context. The lemma belongs to the part The recursive step, part 9: the whole program stepP K (generic in the numeric premises).

Formalization Note. This is a lemma of the Lean development NLogN, a multitape-Turing-machine implementation of the Harvey–van der Hoeven $O(n\log n)$ integer multiplication algorithm, used in the proof of NLogN.FIN.theorem_1_1_nlogn : IntMul.MulTimeBound fun n => n * Real.log n. All names refer to the definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8 (namespace NLogN), built on the platform model Def_IntMul_MultitapeModel and the published reference Def_IntMul_HvdH_MachineRef. The machine layer: IState HS is a state of 64 item stacks; RM programs have a semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s relative to a multiplication spec M : MulSpec; zsz z is the bit length of $|z|$.