Native radix sorting followed by unique-key/multiplicity array construction

This composes the complete native sorter and adjacent-run builder. Two length-n sorting buffers are followed by length-n key and count output buffers. All four blocks lie in one explicit frame. The returned keys are in unsigned encoding order; decoding signed keys does not turn that order into signed integer order.

Main definitions

• deduplicateCode: fixed 16-register sorting and multiplicity program.
• deduplicateTime: complete structured instruction bound.

Main results

• deduplicate_exec: exact set enumeration and full multiplicities, with no sorting premise.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.RadixSort.origin : Fin 16

Original base retained while radix sorting swaps its two pointers.

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

Install the two output pointers after the two sorting buffers.

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

Complete sorting and deduplication; Deduplicate.out returns the number of unique words.

def Cslib.Algorithms.WordRAM.RadixSort.deduplicateTime (n keyBits : ℕ) : ℕ

All instructions, including pointer construction and both complete algorithms, excluding only the final halt. For positive n and key-bit bound this is O(n * keyBits).

theorem Cslib.Algorithms.WordRAM.RadixSort.deduplicate_exec {w base keyBits : ℕ} (xs : List ℕ) (x : WordRAM.Data 16) (hn : x.regs len = xs.length) (hs : x.regs src = base) (hd : x.regs dst = base + xs.length) (hb : x.regs bits = keyBits) (hmem : WordRAM.Block.HoldsList base xs x.mem) (hkeys : ∀ v ∈ xs, v < 2 ^ keyBits) (hwords : ∀ v ∈ xs, WordRAM.Fits w v) (hfit : WordRAM.Fits w (base + 4 * xs.length)) (hbits : WordRAM.Fits w keyBits) (h2 : WordRAM.Fits w 2) : ∃ (y : WordRAM.Data 16) (rs : List (ℕ × ℕ)), WordRAM.ExecWithin w deduplicateCode x y (deduplicateTime xs.length keyBits) ∧ y.regs Deduplicate.out = rs.length ∧ WordRAM.Block.HoldsList (base + 2 * xs.length) (List.map Prod.fst rs) y.mem ∧ WordRAM.Block.HoldsList (base + 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 := base, length := 4 * xs.length }.footprint x.mem y.mem

Complete fixed-code radix sorting and adjacent deduplication, with full multiplicities. Keys below 2^keyBits may repeat arbitrarily. Only the four length-n buffers change. The conditions constrain arithmetic/address fit, not sorting or deduplication behavior.