The entry computes the register file (round six, `genE_sp`)

The entry computes the register file.

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

theorem IntMul.Kappa.R6.IL.genE_sp (s : IState HS) {m q W T e P L a b c M Bb : ℕ} (hM : zsz (M : ℤ) ≤ Bb)
    (h : EntB m q W T e P L a b c M) :
    Sp (genE m q W T) (encK s (fDesc e P L a b c))
      (encK s (regState (fDesc e P L a b c) (vEnt m q W T e P L a b c) genD))
      (cGenE m q W T e Bb)

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

The general procedure reads the descriptor DescG (dT = e, dP, dL, dA, dB, dC) and creates a register file genD holding f = e / m, r = e mod m, N = q ^ f, q ^ r, N ^ m, L' = L / W, vol A, and the level volumes vol (P :: L' :: A), q ^ r vol B, q ^ r vol Cs, v = vol (P :: L' :: hdShape A B' C' m N), (T + W) v, T v (genE_sp).

• desc_split: a state with the descriptor is a managed state over the descriptor values;
• vEnt: the valuation after the entry, with its values (vEnt_vals) and bounds.

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