In-place randomized quickselect on the word RAM

Iterative in-place 3-way randomized quickselect over Cslib.WordRAM.Basis.standard. Given an n-word slice starting at address base and a 0-indexed target rank k < n, the algorithm selects the k-th smallest element input.mergeSort[k] in place using zero auxiliary memory words (O(1) registers only).

The selection loop maintains a single active subarray [lo, hi) of length m = hi - lo containing the target address target = base + k (lo ≤ target < hi). When 2 ≤ m, each iteration samples a uniform pivot offset off ← rand (m - 1) with pivot value piv = mem (lo + off) and applies Dutch National Flag 3-way partitioning to split [lo, hi) into < piv on [lo, lt), = piv on [lt, gt), and > piv on [gt, hi):

1. Pathwise correctness and zero auxiliary space: Every execution path halts cleanly and returns input.mergeSort[k]. The final memory permutes [base, base + n) in place so that mem (base + k) = input.mergeSort[k], mem (base + i) ≤ mem (base + k) for i < k, and mem (base + k) ≤ mem (base + i) for k < i < n. All memory outside Finset.Ico base (base + n) is unchanged.
2. Strict worst-case bounds: Because the = piv region [lt, gt) contains the sampled pivot, lt < gt holds and each iteration strictly decreases m = hi - lo. Every execution path makes at most n - 1 rand calls and executes at most 10 * n ^ 2 + 15 instructions.
3. Unconditional linear expected running time (including duplicates): All copies of piv in [lo, hi) land in [lt, gt). When lt ≤ target < gt, the active range collapses immediately to length 1; otherwise, for a sampled pivot of sorted rank r < m in [lo, hi), the next active subarray has length at most max r (m - 1 - r). The identity 4 * ∑_{r < m} max r (m - 1 - r) ≤ 3 * m ^ 2 gives a (3 / 4)-shrinking linear potential 80 * m on the active subarray length m, proving expectedTime w program (.init (k :: input)) ≤ 80 * n + 15 uniformly over all k < n and all duplicate-key patterns.
4. Total out-of-range handling: On State.init (k :: input) satisfying InputFits w (k :: input) with n ≤ k, program skips selectSlice and halts deterministically in 8 instructions with output 0, 0 rand calls, and unchanged memory.

Main definitions

• Cslib.Algorithms.WordRAM.Quickselect.samplePivot, Cslib.Algorithms.WordRAM.Quickselect.narrowRange, Cslib.Algorithms.WordRAM.Quickselect.partitionAndNarrow, Cslib.Algorithms.WordRAM.Quickselect.selectStep, Cslib.Algorithms.WordRAM.Quickselect.selectSetup, Cslib.Algorithms.WordRAM.Quickselect.loadHeader: structured building blocks of the selection loop and Data.init header.
• Cslib.Algorithms.WordRAM.Quickselect.selectSlice: reusable 16-register structured subroutine selecting rank regs rk in [regs base, regs base + regs len) in place.
• Cslib.Algorithms.WordRAM.Quickselect.code, Cslib.Algorithms.WordRAM.Quickselect.program: structured and compiled 16-register randomized quickselect on State.init (k :: input).
• Cslib.Algorithms.WordRAM.Quickselect.worstCaseTime: quadratic worst-case step bound 10 * n ^ 2 + 15.
• Cslib.Algorithms.WordRAM.Quickselect.expectedTimeBound: linear expected step bound 80 * n + 15.

Main results

• Cslib.Algorithms.WordRAM.Quickselect.selectSlice_spec: ExecRandWithin and linear expectedCodeTime specification for selectSlice on an arbitrary slice [base, base + n).
• Cslib.Algorithms.WordRAM.Quickselect.loadHeader_spec, Cslib.Algorithms.WordRAM.Quickselect.code_spec, Cslib.Algorithms.WordRAM.Quickselect.code_out_of_range_spec: structured loadHeader and code specifications for k < input.length and input.length ≤ k.
• Cslib.Algorithms.WordRAM.Quickselect.quickselect_correct_and_bounds: joint certificate of RandHaltsWithin, RandCallsBounded (≤ n - 1), pathwise order-statistic output, in-place partition order, zero-auxiliary-memory Modifies frame, and O(n) expectedTime at word size w ≥ logWidth 2 input.length.
• Cslib.Algorithms.WordRAM.Quickselect.quickselect_out_of_range: deterministic 8-step halting when input.length ≤ k.

Classical randomized selection (RANDOMIZED-SELECT) appears in [CLRS09], Section 9.2; see also [MU17], Section 3.5 (sampling-based median selection, related background). The 3-way Dutch National Flag word-RAM formulation, zero-auxiliary-memory frame, pure-ℕ linear drift potential 80 * m, and duplicate-key rank domination are original to this formalization.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Section 9.2.
• M. Mitzenmacher and E. Upfal, Probability and Computing, Section 3.5.

Expected-selection linear potential recurrence

Order-statistic characterization and word-size bound

Structured WordRAM quickselect program (r = 16)

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.ans : Fin 16

Output register (also 0 initially in Data.init).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.one : Fin 16

Constant 1 (Quicksort.Reg.one).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.rk : Fin 16

Target 0-indexed rank k.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.len : Fin 16

Slice length n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.base : Fin 16

Slice base address base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.target : Fin 16

Target cell address base + k.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.lo1 : Fin 16

Maintained value lo + 1 for the loop test lo + 1 < hi.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.lo : Fin 16

Active subarray start address lo (Quicksort.Reg.lo).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.hi : Fin 16

Active subarray exclusive end address hi (Quicksort.Reg.hi).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.lt : Fin 16

3-way partition < piv boundary lt (Quicksort.Reg.lt).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.cur : Fin 16

3-way partition scan cursor cur (Quicksort.Reg.cur).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.gt : Fin 16

3-way partition > piv boundary gt (Quicksort.Reg.gt).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.piv : Fin 16

Pivot value piv (Quicksort.Reg.piv).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.val : Fin 16

Element scratch val (Quicksort.Reg.val).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.val2 : Fin 16

Swap scratch val2 (Quicksort.Reg.val2).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quickselect.Reg.tmp : Fin 16

Offset / address scratch tmp (Quicksort.Reg.tmp).

def Cslib.Algorithms.WordRAM.Quickselect.samplePivot : WordRAM.Code WordRAM.Basis.standard 16

Sample a uniform pivot offset tmp ← rand (hi - (lo + 1)) (2 instructions, 1 rand call).

def Cslib.Algorithms.WordRAM.Quickselect.narrowRange : WordRAM.Code WordRAM.Basis.standard 16

Narrow [lo, hi) (alongside lo1 = lo + 1) to the unique 3-way partition region containing target (≤ 6 instructions, zero .sub/.div/.mod operations).

def Cslib.Algorithms.WordRAM.Quickselect.partitionAndNarrow : WordRAM.Code WordRAM.Basis.standard 16

Partition [lo, hi) around the pivot at lo + tmp and narrow [lo, hi) around target.

def Cslib.Algorithms.WordRAM.Quickselect.selectStep : WordRAM.Code WordRAM.Basis.standard 16

One iteration of the quickselect loop on [lo, hi) (lo + 1 < hi).

def Cslib.Algorithms.WordRAM.Quickselect.selectSetup : WordRAM.Code WordRAM.Basis.standard 16

Deterministic 5-instruction setup of selectSlice.

def Cslib.Algorithms.WordRAM.Quickselect.selectSlice : WordRAM.Code WordRAM.Basis.standard 16

Reusable structured in-place quickselect subroutine on [regs base, regs base + regs len): permutes the slice in place around rank regs rk and stores the selected element in ans.

def Cslib.Algorithms.WordRAM.Quickselect.loadHeader : WordRAM.Code WordRAM.Basis.standard 16

Deterministic 4-instruction header reading len = M[0] - 1 and rk = M[1] on Data.init (k :: input).

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

Structured 16-register quickselect on Data.init (k :: input): selects input.mergeSort[k] in [2, input.length + 2) when k < input.length, and sets ans ← 0 otherwise.

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

Compiled flat 16-register randomized quickselect program halting with ans.

def Cslib.Algorithms.WordRAM.Quickselect.worstCaseTime (n : ℕ) : ℕ

Quadratic worst-case instruction budget 10 * n ^ 2 + 15.

def Cslib.Algorithms.WordRAM.Quickselect.expectedTimeBound (n : ℕ) : ℕ

Linear expected instruction budget 80 * n + 15.

Selection invariant and subroutine specifications

theorem Cslib.Algorithms.WordRAM.Quickselect.selectSlice_spec {w : ℕ} {x : WordRAM.Data 16} (hk : x.regs Reg.rk < x.regs Reg.len) (hfit : WordRAM.Fits w (x.regs Reg.base + x.regs Reg.len)) : let vbase := x.regs Reg.base; let n := x.regs Reg.len; let k := x.regs Reg.rk; let s₀ := Quicksort.memSlice vbase (vbase + n) x.mem; WordRAM.ExecRandWithin w selectSlice x (fun (y : WordRAM.Data 16) => y.regs Reg.ans = (s₀.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] ∧ (Quicksort.memSlice vbase (vbase + n) y.mem).Perm s₀ ∧ y.mem (vbase + k) = (s₀.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] ∧ (∀ i < k, y.mem (vbase + i) ≤ y.mem (vbase + k)) ∧ (∀ (i : ℕ), k < i → i < n → y.mem (vbase + k) ≤ y.mem (vbase + i)) ∧ WordRAM.Modifies (Finset.Ico vbase (vbase + n)) x.mem y.mem) (10 * n ^ 2 + 8) (n - 1) ∧ WordRAM.expectedCodeTime w selectSlice x ≤ ↑(80 * n + 8)

Specification of selectSlice on an arbitrary slice [vbase, vbase + n). When k = x.regs rk < x.regs len = n and Fits w (x.regs base + x.regs len):

1. selectSlice runs within 10 * n ^ 2 + 8 instructions and n - 1 rand calls, permuting [vbase, vbase + n) in place, placing the k-th sorted element in both y.mem (vbase + k) and y.regs ans, partitioning [vbase, vbase + n) around vbase + k, and modifying only Finset.Ico vbase (vbase + n);
2. Its expected instruction count satisfies expectedCodeTime w selectSlice x ≤ 80 * n + 8.

Top-level program specifications on State.init (k :: input)

theorem Cslib.Algorithms.WordRAM.Quickselect.loadHeader_spec {w k : ℕ} {input : List ℕ} (hfit : WordRAM.InputFits w (k :: input)) : ∃ (x_hdr : WordRAM.Data 16), WordRAM.Exec w loadHeader (WordRAM.Data.init (k :: input)) x_hdr 4 ∧ x_hdr.mem = (WordRAM.Data.init (k :: input)).mem ∧ x_hdr.regs Reg.one = 1 ∧ x_hdr.regs Reg.rk = k ∧ x_hdr.regs Reg.len = input.length

Deterministic 4-step execution of loadHeader on Data.init (k :: input).

theorem Cslib.Algorithms.WordRAM.Quickselect.code_out_of_range_spec {w k : ℕ} {input : List ℕ} (hk : input.length ≤ k) (hfit : WordRAM.InputFits w (k :: input)) : ∃ (y : WordRAM.Data 16), WordRAM.Exec w code (WordRAM.Data.init (k :: input)) y 7 ∧ y.regs Reg.ans = 0 ∧ y.mem = (WordRAM.Data.init (k :: input)).mem

Structured 7-step execution of code when input.length ≤ k.

theorem Cslib.Algorithms.WordRAM.Quickselect.quickselect_out_of_range {w k : ℕ} {input : List ℕ} (hk : input.length ≤ k) (hfit : WordRAM.InputFits w (k :: input)) : WordRAM.Executes w program (WordRAM.State.init (k :: input)) 0 8 ∧ WordRAM.RandHaltsWithin w program (WordRAM.State.init (k :: input)) (worstCaseTime input.length) ∧ WordRAM.RandCallsBounded w program (WordRAM.State.init (k :: input)) (worstCaseTime input.length) 0 ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w program (worstCaseTime input.length) (WordRAM.RandCfg.running (WordRAM.State.init (k :: input)))), ∃ (y : WordRAM.Data 16), cfg = WordRAM.RandCfg.halted 0 y ∧ WordRAM.Data.Bounded w y ∧ y.mem = (WordRAM.Data.init (k :: input)).mem) ∧ WordRAM.expectedTime w program (WordRAM.State.init (k :: input)) = 8

Total out-of-range behavior (input.length ≤ k). Whenever InputFits w (k :: input) holds and input.length ≤ k, program executes deterministically in 8 instructions returning 0, making 0 rand calls and leaving memory completely unchanged.

theorem Cslib.Algorithms.WordRAM.Quickselect.code_spec {w k : ℕ} {input : List ℕ} (hk : k < input.length) (hw : WordRAM.logWidth 2 input.length ≤ w) (hfit : WordRAM.InputFits w (k :: input)) : WordRAM.ExecRandWithin w code (WordRAM.Data.init (k :: input)) (fun (y : WordRAM.Data 16) => y.regs Reg.ans = (input.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] ∧ (Quicksort.memSlice 2 (input.length + 2) y.mem).Perm input ∧ y.mem (2 + k) = (input.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] ∧ (∀ i < k, y.mem (2 + i) ≤ y.mem (2 + k)) ∧ (∀ (i : ℕ), k < i → i < input.length → y.mem (2 + k) ≤ y.mem (2 + i)) ∧ WordRAM.Modifies (Finset.Ico 2 (input.length + 2)) (WordRAM.Data.init (k :: input)).mem y.mem) (10 * input.length ^ 2 + 14) (input.length - 1) ∧ WordRAM.expectedCodeTime w code (WordRAM.Data.init (k :: input)) ≤ ↑(80 * input.length + 14)

Structured ExecRandWithin and linear expectedCodeTime specification for code when k < input.length.

theorem Cslib.Algorithms.WordRAM.Quickselect.quickselect_correct_and_bounds {w k : ℕ} {input : List ℕ} (hk : k < input.length) (hw : WordRAM.logWidth 2 input.length ≤ w) (hfit : WordRAM.InputFits w (k :: input)) : WordRAM.RandHaltsWithin w program (WordRAM.State.init (k :: input)) (worstCaseTime input.length) ∧ WordRAM.RandCallsBounded w program (WordRAM.State.init (k :: input)) (worstCaseTime input.length) (input.length - 1) ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w program (worstCaseTime input.length) (WordRAM.RandCfg.running (WordRAM.State.init (k :: input)))), ∃ (y : WordRAM.Data 16), cfg = WordRAM.RandCfg.halted (input.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] y ∧ WordRAM.Data.Bounded w y ∧ (Quicksort.memSlice 2 (input.length + 2) y.mem).Perm input ∧ y.mem (2 + k) = (input.mergeSort fun (a b : ℕ) => decide (a ≤ b))[k] ∧ (∀ i < k, y.mem (2 + i) ≤ y.mem (2 + k)) ∧ (∀ (i : ℕ), k < i → i < input.length → y.mem (2 + k) ≤ y.mem (2 + i)) ∧ WordRAM.Modifies (Finset.Ico 2 (input.length + 2)) (WordRAM.Data.init (k :: input)).mem y.mem) ∧ WordRAM.expectedTime w program (WordRAM.State.init (k :: input)) ≤ ↑(expectedTimeBound input.length)

In-place randomized quickselect: correctness, zero auxiliary space, worst-case bounds, rand-call bound, and linear expected running time.

For any input : List ℕ of length n, target rank k < n, and word size w ≥ logWidth 2 n with InputFits w (k :: input):

1. program halts without faulting within worstCaseTime n = 10 * n ^ 2 + 15 instructions on every execution path (RandHaltsWithin);
2. Every execution path makes at most n - 1 rand calls (RandCallsBounded);
3. On every supported halting configuration, program returns input.mergeSort[k] with y.Bounded w, permutes memSlice 2 (n + 2) y.mem in place so that y.mem (2 + k) = input.mergeSort[k] with y.mem (2 + i) ≤ y.mem (2 + k) for i < k and y.mem (2 + k) ≤ y.mem (2 + i) for k < i < n, and leaves all memory outside Finset.Ico 2 (n + 2) untouched (Modifies, zero auxiliary heap words);
4. The expected instruction count satisfies expectedTime w program (.init (k :: input)) ≤ expectedTimeBound n = 80 * n + 15 uniformly over all k < n and unconditionally across duplicate keys.