Native stable-scatter stores

Main results

• Wanted.exec_scatterWrite: store one computed code and original position at the actual cursor, then increment that cursor and the original-input counter.

This is an internal implementation API. The scatter position is the existing counting-sort formula, whose range follows from the original input length, rather than an execution oracle.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_scatterWrite {w L m N Q n v : ℕ} (key : ℕ → ℕ) (hn : n < Q) (hk : key n < MatrixMultiplication.Schonhage.numBands L m N ^ 2) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hi : x.regs index = n) (ht : x.regs tile = key n) (hv : x.regs (packRegisters code) = v) (hc : x.mem (cursorAddressBase L m N Q + key n) = CountingSort.position key Q n) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w scatterWrite x y 9 ∧ Parameters L m N Q y ∧ y.regs index = n + 1 ∧ y.mem (codeAddress L m N Q + CountingSort.position key Q n) = v ∧ y.mem (originalAddress L m N Q + CountingSort.position key Q n) = n ∧ y.mem (cursorAddressBase L m N Q + key n) = CountingSort.position key Q n + 1 ∧ ∀ (a : ℕ), a ≠ cursorAddressBase L m N Q + key n → a ≠ codeAddress L m N Q + CountingSort.position key Q n → a ≠ originalAddress L m N Q + CountingSort.position key Q n → y.mem a = x.mem a

Three actual memory stores suffice for one stable occurrence. Address fits and separation follow from the original query length and the proved counting-sort position.