Native stable digit-selection scan

The scan appends a stable digit-selected subsequence to a disjoint destination array. Both orders of the two disjoint blocks are allowed, so consecutive radix passes can swap pointers. All loads, address calculations, stores and loop control are native instructions.

Main definitions

• Scan.body: read, test, conditionally append, and advance.
• Scan.code: reset the input cursor and scan the array.

Main results

• Scan.exec: stable selection with a linear instruction bound and memory frame.

@[reducible, inline]

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

Array length.

@[reducible, inline]

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

Source pointer; the sorter returns the final sorted pointer here.

@[reducible, inline]

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

Scratch pointer.

@[reducible, inline]

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

Current bit index.

@[reducible, inline]

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

Digit selected by the current scan.

@[reducible, inline]

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

Constant one.

@[reducible, inline]

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

Constant two.

@[reducible, inline]

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

Input cursor.

@[reducible, inline]

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

Output cursor.

@[reducible, inline]

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

Address temporary.

@[reducible, inline]

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

Loaded key.

@[reducible, inline]

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

Current key digit.

@[reducible, inline]

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

Number of key bits, supplied by the caller.

@[reducible, inline]

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

Temporary used to swap the two pointers.

def Cslib.Algorithms.WordRAM.RadixSort.Scan.body : WordRAM.Code WordRAM.Basis.standard 16

One stable-selection iteration, with every address and counter operation charged.

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

Reset the input cursor, then perform one stable-selection scan.

theorem Cslib.Algorithms.WordRAM.RadixSort.Scan.exec {w s d b t : ℕ} (xs acc : List ℕ) (x : WordRAM.Data 16) (hn : x.regs len = xs.length) (hs : x.regs src = s) (hd : x.regs dst = d) (hb : x.regs bit = b) (ht : x.regs tag = t) (ho : x.regs one = 1) (h2 : x.regs two = 2) (hout : x.regs out = acc.length) (hsrc : WordRAM.Block.HoldsList s xs x.mem) (hacc : WordRAM.Block.HoldsList d acc x.mem) (hwords : ∀ v ∈ xs, WordRAM.Fits w v) (hcap : (acc ++ select b t xs).length ≤ xs.length) (hdisj : s + xs.length ≤ d ∨ d + xs.length ≤ s) (hsfit : WordRAM.Fits w (s + xs.length)) (hdfit : WordRAM.Fits w (d + xs.length)) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w code x y (11 * xs.length + 3) ∧ WordRAM.Block.HoldsList d (acc ++ select b t xs) y.mem ∧ WordRAM.Block.HoldsList s xs y.mem ∧ y.regs out = (acc ++ select b t xs).length ∧ WordRAM.Modifies { base := d, length := xs.length }.footprint x.mem y.mem

Append a stable digit-selected subsequence in 11n+3 instructions. The destination has capacity n; source and destination blocks are disjoint, in either order. The caller's existing destination prefix is retained. Only destination cells may change.