Fixed-code native unsigned radix sorter

Two stable scans per bit partition the source into zeros followed by ones in scratch. Swapping the pointers avoids a copy-back scan. Code and registers are independent of length and key width. The source pointer on exit identifies the sorted array; the other block is scratch.

Main definitions

• pass: two digit scans and pointer swap.
• code: the complete radix sorter with a register-supplied bit bound.
• timeBound: explicit instruction bound, excluding halt.

Main results

• exec: complete charged sorting, with permutation, sortedness and a two-array frame.

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

Exchange source and scratch, then advance to the next bit.

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

Exactly two stable scans per bit.

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

Complete unsigned radix sorter. Parameters are length, two disjoint array bases, and bits. The returned source register identifies the sorted block.

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

All instructions of radix sorting, excluding a final halt.

theorem Cslib.Algorithms.WordRAM.RadixSort.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 + 2 * xs.length)) (hbits : WordRAM.Fits w keyBits) (h2 : WordRAM.Fits w 2) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w code x y (timeBound xs.length keyBits) ∧ WordRAM.Block.HoldsList (y.regs src) (passes keyBits xs) y.mem ∧ (passes keyBits xs).Perm xs ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) (passes keyBits xs) ∧ (y.regs src = base ∨ y.regs src = base + xs.length) ∧ WordRAM.Modifies { base := base, length := 2 * xs.length }.footprint x.mem y.mem

Sort all keys below 2^keyBits in keyBits * (22n+15)+5 instructions. The two arrays have length n, are adjacent, and start at caller-supplied base. Only these 2n cells may change. The sorted block is returned in src; it is one of the two original blocks. This includes empty lists and zero bit bounds. The key-bit bound and both one-past-end addresses must fit; constant two must fit. No ordering contract is assumed.