The tail (round six, `gen_tail`)

The tail: the r leftover digit interchanges, then the register file is removed.

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

theorem IntMul.Kappa.R6.IL.gen_tail {Pp : ℕ} {I : List Sym} {iprog : Fin Pp → IStmt HS Pp} (s : IState HS)
    {m q W T e P L M Bb : ℕ} {A B Cs : Shape} (hM : zsz (M : ℤ) ≤ Bb) (hq : 2 ≤ q)
    (hP : 1 ≤ P) (hL : 1 ≤ L)
    (hA : ∀ x ∈ A, 1 ≤ x) (hB : ∀ x ∈ B, 1 ≤ x) (hC : ∀ x ∈ Cs, 1 ≤ x)
    (hEB : EntB m q W T e P L (vol A) (vol B) (vol Cs) M)
    (hVM : vol (P :: L :: hdShape A B Cs e q) ≤ M)
    (R : List Item) (ys : List (ZMod 2)) (hys : ys.length = vol (P :: L :: hdShape A B Cs e q)) :
    IRuns I iprog (genTail q)
      (encK (s.upd 0 (ints (enc2 ys) ++ R))
        (regState (fDesc e P L (vol A) (vol B) (vol Cs))
          (vEnt m q W T e P L (vol A) (vol B) (vol Cs)) genD))
      (encK (s.upd 0 (ints (enc2 (Bit.tailSwaps (P :: L :: hdShape A B Cs e q)
          (A.length + 2 + m * (e / m)) (A.length + B.length + e + 2 + m * (e / m)) (e % m) ys)) ++ R))
        (fDesc e P L (vol A) (vol B) (vol Cs)))
      (cTail q (vol (P :: L :: hdShape A B Cs e q)) Bb (e % m))

Context. Round six, item language: the tail of the general procedure

After the level, the general procedure swaps the r = e mod m leftover digit pairs (KFE swapsF q, the registers set by tailA q) and removes its register file: gen_tail. The digit runs are those of Bit.tailSwaps in progH.

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