In-place randomized quicksort on the word RAM

Iterative in-place 3-way randomized quicksort over Cslib.WordRAM.Basis.standard, sorting an n-word input array in Block.mk 1 n using an explicit 2 * n-word range stack allocated at [n + 1, 3 * n + 1).

Using Dutch National Flag 3-way partitioning (< piv, = piv, > piv) around a uniformly sampled pivot off ← rand (hi - lo - 1) ensures that:

1. Pathwise correctness: every execution path halts cleanly with Block.mk 1 n holding input.mergeSort (a sorted permutation of input), modifying memory only within Finset.Ico 1 (3 * n + 1);
2. Strict worst-case bounds: only subranges of length ≥ 2 are pushed, and every partition strictly eliminates at least the sampled pivot, so stack potential ∑ (hi - lo - 1) drops on every iteration — bounding every path to at most n - 1 rand calls and 20 * n ^ 2 + 8 * n + 32 instructions;
3. Unconditional O(n log n) expected running time (including duplicates): equal elements fall into the middle = piv region and are never recursed on, so the left and right recursive sizes on sorted rank r are at most r and m - 1 - r regardless of duplicate keys. Bounding Mathlib's harmonic numbers via harmonic_le_log_add_one (harmonic n ≤ Nat.log 2 n + 1) yields expectedTime w program (.init input) ≤ 120 * n * (Nat.log 2 n + 1) + 32 without transcendental analysis.

Main definitions

• Cslib.Algorithms.WordRAM.Quicksort.code, Cslib.Algorithms.WordRAM.Quicksort.program: structured and compiled 16-register randomized quicksort program.
• Cslib.Algorithms.WordRAM.Quicksort.worstCaseTime: quadratic worst-case step bound 20 * n ^ 2 + 8 * n + 32.
• Cslib.Algorithms.WordRAM.Quicksort.expectedTimeBound: O(n log n) expected step bound 120 * n * (Nat.log 2 n + 1) + 32.

Main results

• Cslib.Algorithms.WordRAM.Quicksort.quicksort_correct_and_bounds: joint certificate of RandHaltsWithin, RandCallsBounded (≤ n - 1), pathwise sorted-array realization + Modifies frame, and O(n log n) expectedTime at word size w ≥ logWidth 3 input.length.

Classical background on randomized quicksort, equal-key partitioning and the expected-cost recurrence appears in [CLRS09], Section 7.3, Section 7.4.2 and Problems 7-2–7-3; [MU17], Section 2.5, gives additional expected-cost background. The word-RAM implementation and step constants, constant-56 explicit-stack potential, ranked-loop drift formulation and duplicate-key rank-domination proof are original to this formalization.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Section 7.3, Section 7.4.2 and Problems 7-2–7-3.
• M. Mitzenmacher and E. Upfal, Probability and Computing, Section 2.5.

Expected-partition potential recurrence

noncomputable def Cslib.Algorithms.WordRAM.Quicksort.subCost (m : ℕ) : ℝ

Potential contribution of a subarray of length m in the expected-time drift argument.

theorem Cslib.Algorithms.WordRAM.Quicksort.subCost_of_lt_two {m : ℕ} (h : m < 2) : subCost m = 0

theorem Cslib.Algorithms.WordRAM.Quicksort.subCost_nonneg (m : ℕ) : 0 ≤ subCost m

theorem Cslib.Algorithms.WordRAM.Quicksort.subCost_le_formula (m : ℕ) : subCost m ≤ 56 * (↑m + 1) * ↑(harmonic m)

theorem Cslib.Algorithms.WordRAM.Quicksort.subCost_mono {a b : ℕ} (hab : a ≤ b) : subCost a ≤ subCost b

theorem Cslib.Algorithms.WordRAM.Quicksort.subCost_recurrence {m : ℕ} (hm : 2 ≤ m) : 28 * ↑m + (∑ r ∈ Finset.range m, (subCost r + subCost (m - 1 - r))) / ↑m ≤ subCost m

Key expected-quicksort recurrence: for m ≥ 2, 28 * m plus the average over r < m of subCost r + subCost (m - 1 - r) is at most subCost m.

Memory slices, permutations, and 3-way partition rank bounds

def Cslib.Algorithms.WordRAM.Quicksort.memSlice (a b : ℕ) (mem : ℕ → ℕ) : List ℕ

Read the subarray mem[a .. b) as a list of length b - a.

@[simp]

theorem Cslib.Algorithms.WordRAM.Quicksort.length_memSlice (a b : ℕ) (mem : ℕ → ℕ) : (memSlice a b mem).length = b - a

theorem Cslib.Algorithms.WordRAM.Quicksort.getElem_memSlice {a b : ℕ} {mem : ℕ → ℕ} {i : ℕ} (hi : i < b - a) : (memSlice a b mem)[i] = mem (a + i)

theorem Cslib.Algorithms.WordRAM.Quicksort.mem_memSlice_iff {a b v : ℕ} {mem : ℕ → ℕ} : v ∈ memSlice a b mem ↔ ∃ (addr : ℕ), a ≤ addr ∧ addr < b ∧ mem addr = v

theorem Cslib.Algorithms.WordRAM.Quicksort.memSlice_congr {a b : ℕ} {m₁ m₂ : ℕ → ℕ} (h : ∀ (addr : ℕ), a ≤ addr → addr < b → m₁ addr = m₂ addr) : memSlice a b m₁ = memSlice a b m₂

theorem Cslib.Algorithms.WordRAM.Quicksort.memSlice_append {a b c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) (mem : ℕ → ℕ) : memSlice a c mem = memSlice a b mem ++ memSlice b c mem

theorem Cslib.Algorithms.WordRAM.Quicksort.memSlice_swap_perm {a b p q : ℕ} (hp : a ≤ p ∧ p < b) (hq : a ≤ q ∧ q < b) (mem : ℕ → ℕ) : (memSlice a b (Function.update (Function.update mem p (mem q)) q (mem p))).Perm (memSlice a b mem)

Swapping two addresses inside [a, b) preserves List.Perm on memSlice a b.

theorem Cslib.Algorithms.WordRAM.Quicksort.partition_counts_and_lt {lo lt gt hi piv : ℕ} {mem₀ mem : ℕ → ℕ} (hbounds : lo ≤ lt ∧ lt ≤ gt ∧ gt ≤ hi) (hperm : (memSlice lo hi mem).Perm (memSlice lo hi mem₀)) (hlt : ∀ (a : ℕ), lo ≤ a → a < lt → mem a < piv) (heq : ∀ (a : ℕ), lt ≤ a → a < gt → mem a = piv) (hgt : ∀ (a : ℕ), gt ≤ a → a < hi → piv < mem a) (hpiv : piv ∈ memSlice lo hi mem₀) : lt < gt ∧ lt - lo = List.countP (fun (x : ℕ) => decide (x < piv)) (memSlice lo hi mem₀) ∧ hi - gt = List.countP (fun (x : ℕ) => decide (piv < x)) (memSlice lo hi mem₀)

At 3-way partition exit (cur = gt), < piv has exact count lt - lo, > piv has exact count hi - gt, and piv ∈ memSlice lo hi mem₀ implies lt < gt.

theorem Cslib.Algorithms.WordRAM.Quicksort.sorted_countP_bounds {zs : List ℕ} (hsorted : List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) zs) {r : ℕ} (hr : r < zs.length) : List.countP (fun (x : ℕ) => decide (x < zs[r])) zs ≤ r ∧ List.countP (fun (x : ℕ) => decide (zs[r] < x)) zs ≤ zs.length - 1 - r

On a sorted list zs (Pairwise (· ≤ ·)), at index r < zs.length, at most r elements are strictly less than zs[r] and at most zs.length - 1 - r elements are strictly greater than zs[r].

theorem Cslib.Algorithms.WordRAM.Quicksort.sum_subCost_pivot_le (u : List ℕ) : ∑ k : Fin u.length, (subCost (List.countP (fun (x : ℕ) => decide (x < u[↑k])) u) + subCost (List.countP (fun (x : ℕ) => decide (u[↑k] < x)) u)) ≤ ∑ r ∈ Finset.range u.length, (subCost r + subCost (u.length - 1 - r))

Expected child subCost summed over all m = u.length uniform pivot choices is bounded by ∑ r < m, (subCost r + subCost (m - 1 - r)), even in the presence of duplicate keys.

Word-size arithmetic (logWidth 3 n ≤ w) and work-stack invariants

theorem Cslib.Algorithms.WordRAM.Quicksort.fits_three_mul_add_three {n w : ℕ} (hw : WordRAM.logWidth 3 n ≤ w) : WordRAM.Fits w (3 * n + 3)

logWidth 3 n ≤ w suffices to fit every address and temporary up to 3 * n + 3 for all n : ℕ (including n = 0).

def Cslib.Algorithms.WordRAM.Quicksort.IntervalDisjoint (p q : ℕ × ℕ) : Prop

Two half-open intervals [a₁, b₁) and [a₂, b₂) are disjoint.

theorem Cslib.Algorithms.WordRAM.Quicksort.IntervalDisjoint.symm {p q : ℕ × ℕ} (h : IntervalDisjoint p q) : IntervalDisjoint q p

def Cslib.Algorithms.WordRAM.Quicksort.ValidStack (n : ℕ) (S : List (ℕ × ℕ)) : Prop

Every interval (a, b) ∈ S satisfies 1 ≤ a, a + 2 ≤ b, and b ≤ n + 1, and the intervals in S are pairwise disjoint.

theorem Cslib.Algorithms.WordRAM.Quicksort.ValidStack.sum_len_le {n : ℕ} {S : List (ℕ × ℕ)} (hS : ValidStack n S) : (List.map (fun (p : ℕ × ℕ) => p.2 - p.1) S).sum ≤ n

Sum of lengths ∑ (b - a) of intervals in S is at most n when ValidStack n S holds.

theorem Cslib.Algorithms.WordRAM.Quicksort.ValidStack.two_mul_length_le {n : ℕ} {S : List (ℕ × ℕ)} (hS : ValidStack n S) : 2 * S.length ≤ n

Twice S.length is at most n when ValidStack n S holds.

def Cslib.Algorithms.WordRAM.Quicksort.NoExternalInversions (n : ℕ) (mem : ℕ → ℕ) (S : List (ℕ × ℕ)) : Prop

Global cross-interval order invariant: every pair 1 ≤ i < j < n + 1 not jointly contained in any active stack interval (a, b) ∈ S is already ordered (mem i ≤ mem j).

Structured WordRAM quicksort program (r = 16)

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quicksort.Reg.zero : Fin 16

Constant 0.

@[reducible, inline]

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

Constant 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quicksort.Reg.two : Fin 16

Constant 2.

@[reducible, inline]

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

Input array length n.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quicksort.Reg.stackLo : Fin 16

Base address n + 1 of the lo work-stack array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quicksort.Reg.stackHi : Fin 16

Base address 2 * n + 1 of the hi work-stack array.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Quicksort.Reg.sp : Fin 16

Current stack pointer (S.length).

@[reducible, inline]

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

Active subarray start address lo.

@[reducible, inline]

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

Active subarray exclusive end address hi.

@[reducible, inline]

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

3-way partition < piv boundary lt.

@[reducible, inline]

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

3-way partition scan cursor cur (and alloc scratch during setup).

@[reducible, inline]

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

3-way partition > piv boundary gt (and alloc frontier during setup).

@[reducible, inline]

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

Pivot value piv.

@[reducible, inline]

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

Element scratch val.

@[reducible, inline]

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

Swap scratch val2.

@[reducible, inline]

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

Address / offset scratch tmp.

def Cslib.Algorithms.WordRAM.Quicksort.swapCells (a b v1 v2 : Fin 16) : WordRAM.Code WordRAM.Basis.standard 16

Swap memory cells *a and *b using scratch registers v1, v2 (4 instructions).

def Cslib.Algorithms.WordRAM.Quicksort.partStep : WordRAM.Code WordRAM.Basis.standard 16

One Dutch National Flag 3-way partition step at cursor cur (≤ 9 instructions).

def Cslib.Algorithms.WordRAM.Quicksort.pushIfNonTrivial (a b : Fin 16) : WordRAM.Code WordRAM.Basis.standard 16

Push [regs a, regs b) onto (stackLo, stackHi) if regs a + 2 ≤ regs b.

def Cslib.Algorithms.WordRAM.Quicksort.popPrefix : WordRAM.Code WordRAM.Basis.standard 16

Deterministic prefix of popAndSample: decrement sp, load lo and hi, and compute tmp = hi - lo - 1 (7 instructions).

def Cslib.Algorithms.WordRAM.Quicksort.popAndSample : WordRAM.Code WordRAM.Basis.standard 16

Pop the top range [lo, hi) from the stack and sample tmp ← rand (hi - lo - 1).

def Cslib.Algorithms.WordRAM.Quicksort.partInit : WordRAM.Code WordRAM.Basis.standard 16

Load pivot at lo + tmp and initialize lt ← lo, cur ← lo, gt ← hi (5 instructions).

def Cslib.Algorithms.WordRAM.Quicksort.partitionAndPush : WordRAM.Code WordRAM.Basis.standard 16

Read the sampled pivot at lo + tmp, 3-way partition [lo, hi), and push non-trivial subranges [lo, lt) and [gt, hi).

def Cslib.Algorithms.WordRAM.Quicksort.outerBody : WordRAM.Code WordRAM.Basis.standard 16

One iteration of the outer work-stack loop.

def Cslib.Algorithms.WordRAM.Quicksort.setup : WordRAM.Code WordRAM.Basis.standard 16

Allocate stackLo and stackHi of capacity n and push [1, n + 1) if n ≥ 2.

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

Structured in-place 3-way randomized quicksort over 16 registers.

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

Compiled flat randomized quicksort program halting with 0 (in zero).

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

Quadratic worst-case instruction budget 20 * n ^ 2 + 8 * n + 32.

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

O(n log n) expected instruction budget 120 * n * (⌊log₂ n⌋ + 1) + 32.

Subroutine executions and partition invariants

def Cslib.Algorithms.WordRAM.Quicksort.swapMem (mem : ℕ → ℕ) (p q : ℕ) : ℕ → ℕ

Swap two memory cells at addresses p and q.

@[simp]

theorem Cslib.Algorithms.WordRAM.Quicksort.swapMem_right (mem : ℕ → ℕ) (p q : ℕ) : swapMem mem p q q = mem p

@[simp]

theorem Cslib.Algorithms.WordRAM.Quicksort.swapMem_left (mem : ℕ → ℕ) (p q : ℕ) : swapMem mem p q p = mem q

theorem Cslib.Algorithms.WordRAM.Quicksort.swapMem_of_ne {mem : ℕ → ℕ} {p q a : ℕ} (hap : a ≠ p) (haq : a ≠ q) : swapMem mem p q a = mem a

theorem Cslib.Algorithms.WordRAM.Quicksort.modifies_swapMem {lo hi p q : ℕ} (hp : lo ≤ p ∧ p < hi) (hq : lo ≤ q ∧ q < hi) (mem : ℕ → ℕ) : WordRAM.Modifies (Finset.Ico lo hi) mem (swapMem mem p q)

theorem Cslib.Algorithms.WordRAM.Quicksort.swapCells_exec {w : ℕ} {a b v1 v2 : Fin 16} {x : WordRAM.Data 16} (ha1 : a ≠ v1) (hb1 : b ≠ v1) (ha2 : a ≠ v2) (hb2 : b ≠ v2) (hv : v1 ≠ v2) : WordRAM.Exec w (swapCells a b v1 v2) x { regs := Function.update (Function.update x.regs v1 (x.mem (x.regs a))) v2 (x.mem (x.regs b)), mem := swapMem x.mem (x.regs a) (x.regs b) } 4

swapCells a b v1 v2 executes in 4 instructions, swapping mem (regs a) and mem (regs b) and writing only scratch registers v1, v2.

structure Cslib.Algorithms.WordRAM.Quicksort.PartInv (w vlo vhi vpiv : ℕ) (mem₀ : ℕ → ℕ) (x : WordRAM.Data 16) : Prop

Dutch National Flag 3-way partition loop invariant on [lo, hi).

• one_eq : x.regs Reg.one = 1

  Register one holds 1.

• lo_eq : x.regs Reg.lo = vlo

  Register lo holds vlo.

• hi_eq : x.regs Reg.hi = vhi

  Register hi holds vhi.

• piv_eq : x.regs Reg.piv = vpiv

  Register piv holds vpiv.

• fits_hi : WordRAM.Fits w vhi

  vhi fits in w bits.

• lo_le_lt : vlo ≤ x.regs Reg.lt

  vlo ≤ lt.

• lt_le_cur : x.regs Reg.lt ≤ x.regs Reg.cur

  lt ≤ cur.

• cur_le_gt : x.regs Reg.cur ≤ x.regs Reg.gt

  cur ≤ gt.

• gt_le_hi : x.regs Reg.gt ≤ vhi

  gt ≤ vhi.

• perm : (memSlice vlo vhi x.mem).Perm (memSlice vlo vhi mem₀)

  mem[vlo .. vhi) is a permutation of mem₀[vlo .. vhi).

• modifies : WordRAM.Modifies (Finset.Ico vlo vhi) mem₀ x.mem

  Only Finset.Ico vlo vhi has been modified since mem₀.

• lt_zone (a : ℕ) : vlo ≤ a → a < x.regs Reg.lt → x.mem a < vpiv

  [vlo, lt) holds elements < vpiv.

• eq_zone (a : ℕ) : x.regs Reg.lt ≤ a → a < x.regs Reg.cur → x.mem a = vpiv

  [lt, cur) holds elements = vpiv.

• gt_zone (a : ℕ) : x.regs Reg.gt ≤ a → a < vhi → vpiv < x.mem a

  [gt, vhi) holds elements > vpiv.

theorem Cslib.Algorithms.WordRAM.Quicksort.partLoop_spec {w vlo vhi vpiv : ℕ} {x : WordRAM.Data 16} (hI : PartInv w vlo vhi vpiv x.mem x) (_hlt_init : x.regs Reg.lt = vlo) (hcur_init : x.regs Reg.cur = vlo) (hgt_init : x.regs Reg.gt = vhi) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w (WordRAM.Code.loop (WordRAM.Cond.lt Reg.cur Reg.gt) partStep) x y (11 * (vhi - vlo) + 2) ∧ PartInv w vlo vhi vpiv x.mem y ∧ y.regs Reg.cur = y.regs Reg.gt

Full 3-way partition loop executes within 11 * (vhi - vlo) + 2 instructions and exits with cur = gt.

Work-stack representation and pushIfNonTrivial

def Cslib.Algorithms.WordRAM.Quicksort.readStack (n : ℕ) (x : WordRAM.Data 16) : List (ℕ × ℕ)

Read the active work-stack directly from (x.regs sp, x.mem) at base addresses n + 1 and 2 * n + 1.

@[simp]

theorem Cslib.Algorithms.WordRAM.Quicksort.length_readStack (n : ℕ) (x : WordRAM.Data 16) : (readStack n x).length = x.regs Reg.sp

theorem Cslib.Algorithms.WordRAM.Quicksort.readStack_congr {n : ℕ} {x y : WordRAM.Data 16} (hsp : y.regs Reg.sp = x.regs Reg.sp) (hmem : ∀ (a : ℕ), n + 1 ≤ a → y.mem a = x.mem a) : readStack n y = readStack n x

theorem Cslib.Algorithms.WordRAM.Quicksort.pushIfNonTrivial_spec {w n : ℕ} {a b : Fin 16} {x : WordRAM.Data 16} (ha_tmp : a ≠ Reg.tmp) (hb_tmp : b ≠ Reg.tmp) (hone : x.regs Reg.one = 1) (htwo : x.regs Reg.two = 2) (hsLo : x.regs Reg.stackLo = n + 1) (hsHi : x.regs Reg.stackHi = 2 * n + 1) (hfit_all : WordRAM.Fits w (3 * n + 3)) (hvb : x.regs a ≤ n + 1 ∧ x.regs b ≤ n + 1) (hcap : x.regs a + 2 ≤ x.regs b → x.regs Reg.sp < n) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w (pushIfNonTrivial a b) x y 8 ∧ (readStack n y = if x.regs a + 2 ≤ x.regs b then readStack n x ++ [(x.regs a, x.regs b)] else readStack n x) ∧ WordRAM.Modifies (Finset.Ico (n + 1) (3 * n + 1)) x.mem y.mem

pushIfNonTrivial a b runs within 8 instructions, appending (va, vb) to readStack n iff va + 2 ≤ vb, and modifying memory only inside Finset.Ico (n + 1) (3 * n + 1).

Global outer-loop invariant and preservation across 3-way partition

structure Cslib.Algorithms.WordRAM.Quicksort.OuterInv (w : ℕ) (input : List ℕ) (x : WordRAM.Data 16) : Prop

Full outer-loop machine invariant for in-place randomized quicksort.

• hw : WordRAM.logWidth 3 input.length ≤ w

  Word size meets logWidth 3 input.length ≤ w.

• zero_eq : x.regs Reg.zero = 0

  Register zero holds 0.

• one_eq : x.regs Reg.one = 1

  Register one holds 1.

• two_eq : x.regs Reg.two = 2

  Register two holds 2.

• len_eq : x.regs Reg.len = input.length

  Register len holds input.length.

• stackLo_eq : x.regs Reg.stackLo = input.length + 1

  Register stackLo holds input.length + 1.

• stackHi_eq : x.regs Reg.stackHi = 2 * input.length + 1

  Register stackHi holds 2 * input.length + 1.

• valid_stack : ValidStack input.length (readStack input.length x)

  Active work-stack intervals are valid and pairwise disjoint.

• no_ext_inv : NoExternalInversions input.length x.mem (readStack input.length x)

  All inversions lie strictly inside active work-stack intervals.

• perm : (memSlice 1 (input.length + 1) x.mem).Perm input

  mem[1 .. n + 1) is a permutation of input.

• modifies : WordRAM.Modifies (Finset.Ico 1 (3 * input.length + 1)) (WordRAM.Data.init input).mem x.mem

  Only Finset.Ico 1 (3 * n + 1) has been modified since Data.init input.

theorem Cslib.Algorithms.WordRAM.Quicksort.partitionAndPush_spec {w : ℕ} {input : List ℕ} {vlo vhi : ℕ} {S₀ : List (ℕ × ℕ)} {x : WordRAM.Data 16} (k : Fin (vhi - vlo)) (hktmp : x.regs Reg.tmp = ↑k) (hzero : x.regs Reg.zero = 0) (hone : x.regs Reg.one = 1) (htwo : x.regs Reg.two = 2) (hlen : x.regs Reg.len = input.length) (hsLo : x.regs Reg.stackLo = input.length + 1) (hsHi : x.regs Reg.stackHi = 2 * input.length + 1) (hlo : x.regs Reg.lo = vlo) (hhi : x.regs Reg.hi = vhi) (hw : WordRAM.logWidth 3 input.length ≤ w) (hread : readStack input.length x = S₀) (hS : ValidStack input.length (S₀ ++ [(vlo, vhi)])) (hinv₀ : NoExternalInversions input.length x.mem (S₀ ++ [(vlo, vhi)])) (hperm₀ : (memSlice 1 (input.length + 1) x.mem).Perm input) (hmod₀ : WordRAM.Modifies (Finset.Ico 1 (3 * input.length + 1)) (WordRAM.Data.init input).mem x.mem) : let u := memSlice vlo vhi x.mem; have m₁ := List.countP (fun (x_1 : ℕ) => decide (x_1 < u[↑k])) u; have m₂ := List.countP (fun (x_1 : ℕ) => decide (u[↑k] < x_1)) u; have S₁ := if 2 ≤ m₁ then S₀ ++ [(vlo, vlo + m₁)] else S₀; have S₂ := if 2 ≤ m₂ then S₁ ++ [(vhi - m₂, vhi)] else S₁; ∃ (y : WordRAM.Data 16) (t : ℕ), WordRAM.Exec w partitionAndPush x y t ∧ t ≤ 11 * (vhi - vlo) + 23 ∧ OuterInv w input y ∧ readStack input.length y = S₂

Deterministic execution of partitionAndPush after popAndSample has popped (vlo, vhi) leaving stack S₀ and sampled offset k < vhi - vlo into tmp.

Randomized popAndSample, outerBody, setup, and headline bounds

theorem Cslib.Algorithms.WordRAM.Quicksort.outerBody_spec {w : ℕ} {input : List ℕ} {x : WordRAM.Data 16} (hI : OuterInv w input x) (hc : (WordRAM.Cond.lt Reg.zero Reg.sp).Holds x) : ∃ (S₀ : List (ℕ × ℕ)) (vlo : ℕ) (vhi : ℕ), readStack input.length x = S₀ ++ [(vlo, vhi)] ∧ ∃ (x_1 : vlo + 2 ≤ vhi) (y : Fin (vhi - vlo - 1 + 1) → WordRAM.Data 16) (t : Fin (vhi - vlo - 1 + 1) → ℕ), WordRAM.ExecRand w outerBody x ((fun (k : Fin (vhi - vlo - 1 + 1)) => (y k, 8 + t k)) <$> ProbComp.unifFin (vhi - vlo - 1)) ∧ ∀ (k : Fin (vhi - vlo - 1 + 1)), t k ≤ 11 * (vhi - vlo) + 23 ∧ OuterInv w input (y k) ∧ let u := memSlice vlo vhi x.mem; have m₁ := List.countP (fun (x_2 : ℕ) => decide (x_2 < u[↑k])) u; have m₂ := List.countP (fun (x_2 : ℕ) => decide (u[↑k] < x_2)) u; have S₁ := if 2 ≤ m₁ then S₀ ++ [(vlo, vlo + m₁)] else S₀; readStack input.length (y k) = if 2 ≤ m₂ then S₁ ++ [(vhi - m₂, vhi)] else S₁

One iteration outerBody from an active state (0 < sp) pops (vlo, vhi), samples a uniform pivot k ← unifFin (vhi - vlo - 1) (1 rand call), and runs partitionAndPush in at most 11 * (vhi - vlo) + 31 total instructions.

def Cslib.Algorithms.WordRAM.Quicksort.stepPotential (n : ℕ) (x : WordRAM.Data 16) : ℕ

Quadratic worst-case step potential ∑_{(a,b) ∈ S} 20 * (b - a) ^ 2.

def Cslib.Algorithms.WordRAM.Quicksort.callPotential (n : ℕ) (x : WordRAM.Data 16) : ℕ

rand-call potential ∑_{(a,b) ∈ S} (b - a - 1).

noncomputable def Cslib.Algorithms.WordRAM.Quicksort.expPotential (n : ℕ) (x : WordRAM.Data 16) : ENNReal

Expected-time potential ENNReal.ofReal (∑_{(a,b) ∈ S} subCost (b - a)).

theorem Cslib.Algorithms.WordRAM.Quicksort.setup_spec {w : ℕ} {input : List ℕ} (hw : WordRAM.logWidth 3 input.length ≤ w) : ∃ (x_init : WordRAM.Data 16) (t_s : ℕ), WordRAM.Exec w setup (WordRAM.Data.init input) x_init t_s ∧ t_s ≤ 8 * input.length + 29 ∧ OuterInv w input x_init ∧ readStack input.length x_init = if 2 ≤ input.length then [(1, input.length + 1)] else []

setup executes deterministically from Data.init input within 8 * input.length + 29 instructions, establishing OuterInv with initial stack [(1, n + 1)] (if 2 ≤ n) or [].

theorem Cslib.Algorithms.WordRAM.Quicksort.quicksort_correct_and_bounds {w : ℕ} {input : List ℕ} (hw : WordRAM.logWidth 3 input.length ≤ w) (hfit : WordRAM.InputFits w input) : WordRAM.RandHaltsWithin w program (WordRAM.State.init input) (worstCaseTime input.length) ∧ WordRAM.RandCallsBounded w program (WordRAM.State.init input) (worstCaseTime input.length) (input.length - 1) ∧ (∀ cfg ∈ OracleComp.support (WordRAM.runRand w program (worstCaseTime input.length) (WordRAM.RandCfg.running (WordRAM.State.init input))), ∃ (y : WordRAM.Data 16), cfg = WordRAM.RandCfg.halted 0 y ∧ WordRAM.Data.Bounded w y ∧ (memSlice 1 (input.length + 1) y.mem).Perm input ∧ List.Pairwise (fun (x1 x2 : ℕ) => x1 ≤ x2) (memSlice 1 (input.length + 1) y.mem) ∧ ({ base := 1, length := input.length }.Realizes y.mem fun (i : Fin { base := 1, length := input.length }.length) => (input.mergeSort fun (a b : ℕ) => decide (a ≤ b))[↑i]) ∧ WordRAM.Modifies (Finset.Ico 1 (3 * input.length + 1)) (WordRAM.Data.init input).mem y.mem) ∧ WordRAM.expectedTime w program (WordRAM.State.init input) ≤ ↑(expectedTimeBound input.length)

In-place randomized quicksort: correctness, worst-case bounds, rand-call bound, and O(n log n) expected running time.

For any input : List ℕ of length n and word size w ≥ logWidth 3 n with InputFits w input:

1. program halts without faulting within worstCaseTime n = 20 * n ^ 2 + 8 * n + 32 instructions on every execution path (RandHaltsWithin);
2. Every execution path makes at most n - 1 rand calls (RandCallsBounded);
3. On every supported halting configuration .halted 0 y, y.Bounded w holds, memSlice 1 (n + 1) y.mem is a sorted permutation of input, Block.mk 1 n realizes input.mergeSort, and memory outside Finset.Ico 1 (3 * n + 1) is untouched (Modifies);
4. The expected instruction count satisfies expectedTime w program (.init input) ≤ expectedTimeBound n = 120 * n * (⌊log₂ n⌋ + 1) + 32 unconditionally (even when input contains duplicate elements).