HvdH machine lemma permP_spec (Permuting a list of records by a list of target indices)

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

theorem NLogN.permP_spec (d n kb : ℕ) (Kl : List ℕ) (D : List (List ℤ)) (Rest RK : List Item)
    (s : IState HS) (hKl : Kl.length = n) (hK : Kl.Perm (List.range n)) (hD : D.length = n)
    (hDw : ∀ r ∈ D, r.length = d) (hN : n ≤ 2 ^ kb) (L1 L2 : List Item)
    (h0 : s.G 0 = ints D.flatten ++ Rest) (h1 : s.G 1 = .int n :: L1)
    (h2 : s.G 2 = .int kb :: L2) (h3 : s.G 3 = natInts Kl ++ RK) :
    (permP d).ok s ∧ (permP d).run s = s.upd 0 (ints (permL Kl D).flatten ++ Rest)

Context. The lemma belongs to the part Permuting a list of records by a list of target indices: Stack 0 holds n records of d integers, n is on 1, the number of key bits kb (n ≤ 2^kb) on 2, and stack 3 holds the target indices Kl (a permutation of 0, …, n-1). permP d moves record p to position Kl[p]; the index list on 3 is restored. Scratch: 40, 41, 43, 45, 51, 54 and those of sortP.

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|$.