Fixed-code native sorting and multiplicity construction from machine input

The input is the ordinary native list of unsigned words. The code reads its length and the physical word width, and uses that width as an explicit key-bit bound. The lower-level deduplicateCode accepts a smaller caller-supplied bit bound when known. The standard-input wrapper's charged bound is O(n * w) for positive n and w.

The key array starts at 1+2n, the count array at 1+3n; the return value is their common logical length. The two sorting buffers occupy [1,1+2n). The implementation accepts repeated keys, zero keys and canonical signed integer encodings. Its order is unsigned encoding order.

Main definitions

• inputCode, program: the complete structured and flat native programs.
• layoutWidth: a logarithmic width sufficient for all four array blocks.

Main results

• input_exec: charged execution from ordinary native input, with exact key/count output.
• layout_fits: logarithmic-width layout fit, including empty input.

def Cslib.Algorithms.WordRAM.RadixSort.inputCode : WordRAM.Code WordRAM.Basis.standard 16

Read the native input header and width, then sort and construct both output arrays.

def Cslib.Algorithms.WordRAM.RadixSort.program : WordRAM.Program WordRAM.Basis.standard 16

The fixed native instruction list, returning the number of unique keys.

def Cslib.Algorithms.WordRAM.RadixSort.layoutWidth (n : ℕ) : ℕ

A logarithmic layout-width schedule; the key magnitude bound is independent.

theorem Cslib.Algorithms.WordRAM.RadixSort.layout_fits (n : ℕ) : WordRAM.Fits (layoutWidth n) (1 + 4 * n) ∧ WordRAM.Fits (layoutWidth n) 2

Four array blocks and both initialization constants fit at the layout-width threshold. This does not by itself bound input key magnitudes.

theorem Cslib.Algorithms.WordRAM.RadixSort.input_exec {w : ℕ} (xs : List ℕ) (hinput : WordRAM.InputFits w xs) (hfit : WordRAM.Fits w (1 + 4 * xs.length)) (h2 : WordRAM.Fits w 2) : ∃ (y : WordRAM.Data 16) (rs : List (ℕ × ℕ)) (steps : ℕ), WordRAM.Exec w inputCode (WordRAM.Data.init xs) y steps ∧ WordRAM.Executes w program (WordRAM.State.init xs) rs.length (steps + 1) ∧ steps + 1 ≤ deduplicateTime xs.length w + 6 ∧ WordRAM.Block.HoldsList (1 + 2 * xs.length) (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (1 + 3 * xs.length) (List.map Prod.snd rs) y.mem ∧ (List.map Prod.fst rs).Nodup ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 < x2) (List.map Prod.fst rs) ∧ (∀ (k : ℕ), k ∈ List.map Prod.fst rs ↔ k ∈ xs) ∧ (∀ p ∈ rs, 0 < p.2 ∧ List.count p.1 xs = p.2) ∧ WordRAM.Modifies { base := 1, length := 4 * xs.length }.footprint (WordRAM.Data.init xs).mem y.mem

Execute the complete finite native program on the standard input convention. The bound includes the final halt and every setup/address/control instruction. Input fit and the explicit 4n+1 layout fit are independent requirements. Empty and singleton inputs need no exceptions. The output words enumerate exactly the input set and each stored count is its full multiplicity.