Charged native binary-mask population scans

Main results

• BandPreparation.exec_population: the actual remainder/division loop computes the population in 6L+5 instructions, preserves memory and changes only its four local registers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.BandPreparation.exec_population {w : ℕ} (L a : ℕ) (x : WordRAM.Data 96) (hl : x.regs levels = L) (ha : x.regs mask = a) (ho : x.regs one = 1) (ht : x.regs two = 2) (hfit : WordRAM.Fits w (a + L + 2)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w populationCode x y (6 * L + 5) ∧ y.regs population = MatrixMultiplication.Schonhage.MaskTable.population L a ∧ y.mem = x.mem ∧ ∀ (i : Fin 96), i ≠ residue → i ≠ population → i ≠ counter → i ≠ digit → y.regs i = x.regs i

Popcount is a native loop, with a fit derived for each arithmetic operation from a bound on its original mask and depth. No memory cell is touched.