Native counting of all valid subset masks

Main results

• BandPreparation.exec_countMasks: the complete binary-mask scan computes the binomial coefficient, with its inner population loops and all outer controls charged.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_countMasks {w : ℕ} (L m : ℕ) (x : WordRAM.Data 96) (hL : x.regs levels = L) (hm : x.regs inner = m) (hM : x.regs masks = 2 ^ L) (h1 : x.regs one = 1) (h2 : x.regs two = 2) (hfit : WordRAM.Fits w (2 ^ L + L + 4)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w countMasks x y ((6 * L + 11) * 2 ^ L + 4) ∧ y.regs count = MatrixMultiplication.Schonhage.K L m ∧ y.regs mask = 2 ^ L ∧ y.mem = x.mem ∧ ∀ (i : Fin 96), i ≠ mask → i ≠ count → i ≠ residue → i ≠ population → i ≠ counter → i ≠ digit → y.regs i = x.regs i

Scanning all masks computes K L m; neither that count nor a valid table is supplied as an input. Every mask-counter and accepted-counter fit follows from the scan range.