One native tile-prefix update

Main results

• Wanted.exec_prefixStep: load the actual bucket count, store its immutable start and mutable cursor, and advance the running sum with every instruction charged.

This stage lemma is an internal implementation API for the complete grouping execution.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_prefixStep {w L m N Q t : ℕ} (key : ℕ → ℕ) (ht : t < MatrixMultiplication.Schonhage.numBands L m N ^ 2) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hi : x.regs index = t) (hs : x.regs total = Nat.count (fun (k : ℕ) => key k < t) Q) (hc : x.mem (countAddress L Q + t) = Nat.count (fun (k : ℕ) => key k = t) Q) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w prefixStep x y 8 ∧ Parameters L m N Q y ∧ y.regs index = t + 1 ∧ y.regs total = Nat.count (fun (k : ℕ) => key k < t + 1) Q ∧ y.mem (offsetAddress L m N Q + t) = Nat.count (fun (k : ℕ) => key k < t) Q ∧ y.mem (cursorAddressBase L m N Q + t) = Nat.count (fun (k : ℕ) => key k < t) Q ∧ ∀ (a : ℕ), a ≠ offsetAddress L m N Q + t → a ≠ cursorAddressBase L m N Q + t → y.mem a = x.mem a

One actual prefix update; the two stored cells are the only possible memory changes.