[orbitingflea]

Part of #1124.

This PR adds iterative in-place three-way randomized quickselect over Cslib.WordRAM.Basis.standard (the standard word-RAM instruction basis). Given State.init (k :: input) with an n-word array stored at memory addresses M[2 .. n + 2), the program selects the 0-indexed k-th smallest element input.mergeSort[k] in place using zero auxiliary memory words.

• In-range correctness and bounds (k < n): Suppose the word bit-width w satisfies logWidth 2 n ≤ w (meaning 2 * (Nat.log 2 n + 1) ≤ w) and InputFits w (k :: input) holds (meaning the input length and every element are below 2 ^ w). Every execution path halts within 10 * n ^ 2 + 15 instructions (RandHaltsWithin) and makes at most n - 1 rand calls (RandCallsBounded). Every halting configuration returns input.mergeSort[k]. The final memory permutes M[2 .. n + 2) in place so that M[2 + k] = input.mergeSort[k], M[2 + i] ≤ M[2 + k] for i < k, and M[2 + k] ≤ M[2 + i] for k < i < n. All memory outside Finset.Ico 2 (n + 2) is unchanged (Modifies). The expected instruction count (expectedTime) is at most 80 * n + 15 across duplicate keys.
• Out-of-range behavior (n ≤ k): When InputFits w (k :: input) and n ≤ k, the program halts deterministically in 8 instructions, returns 0, makes 0 rand calls, and leaves memory unchanged.
• Reuse and public surface: The implementation reuses Quicksort's three-way partition step, slice helpers, and rank-count bounds directly. The selection loop invariant and linear potential are marked private because quickselect tracks a single active subarray rather than Quicksort's two-sided range stack. Quickselect keeps the slice subroutine, top-level program, time bounds, register aliases, and Basis.standard structured step pieces public so that RandomizedWordRAMBridge can lift the program to Basis.exact (the exact arithmetic basis without saturating subtraction).

Scope

This PR covers in-place randomized quickselect on the word RAM, its uncatalogued formal abstract in RandomizedWordRAMAbstract alongside quicksort, and unit and abstract tests.

Validation: all six scripts/check.sh gates and python3 -B scripts/build_abstracts.py --check pass (see the PR Checks tab for hosted CI results).

AI assistance: Gemini agents (under Renfei Zhou's direction) wrote the Lean definitions, proofs, tests, formal abstract, and PR description. No human has reviewed this PR yet.

[Copilot]

Copilot was unable to review this pull request because the user who requested the review has insufficient remaining quota.

An organization owner can choose the repository organization as the billing source for reviews requested by members with a paid Copilot license. Learn about Copilot code review billing.

[SamuelSchlesinger]

reviewer-jetski-5208-1339 for coordinator-jetski-5208b1c7 (agent review, not human approval): CHANGES REQUESTED at 131eeb946dc28bfcb866eb080a3f632fae74103f

Thank you, @orbitingflea, for another clean contribution. The mathematics and the Lean statements look right to me. What I'm requesting is a small correction to a citation plus two additions to the PR description.

What is proved. quickselect_correct_and_bounds uses one fixed 16-register Basis.standard program and the start state init (k :: input), so M[0] = n + 1, M[1] = k and M[2 .. n + 2) = input. It assumes k < n, InputFits w (k :: input) and logWidth 2 n ≤ w. Under these hypotheses every coin path halts without faulting within 10n² + 15 steps and makes at most n - 1 rand calls. Every halting configuration returns input.mergeSort[k], permutes [2, n + 2) around 2 + k, and leaves every other cell unchanged, so no auxiliary memory is used. Finally, expectedTime ≤ 80n + 15. expectedTime is the tail sum ∑ₜ Pr[running at t] over the algorithm's coins for a fixed input. The theorem quantifies over every k < n and every input, including duplicate keys, so this is the usual guarantee: expected time over the coins, worst case over inputs. For n ≤ k, quickselect_out_of_range gives deterministic halting in 8 steps with output 0. The width hypothesis is a conventional sufficient condition (it makes n + 2 fit in a word), not a tight one, and the docstrings say so.

Source mapping. CLRS (3rd ed.) §9.2 RANDOMIZED-SELECT returns the i-th smallest element (1-indexed), recurses, uses Lomuto two-way partitioning, and proves E[T(n)] = O(n) assuming distinct elements. Here k = i − 1, the loop is iterative, partitioning is three-way, and the bound is an explicit step count that also covers duplicate keys. This is a faithful and somewhat stronger version, and the module correctly labels the explicit constants and the duplicate-key argument as original.

Checked instances and edge cases. For n = 1, k = 0, setup makes lo + 1 = hi, so the loop is skipped and no rand call is made. The abstract test on [7] confirms this. The out-of-range branch is exercised at w = 1 on init [0] (empty input). There are duplicate-heavy tests on [4,2,4,0,2,1] for all k < 6, and a selectSlice test on a non-default slice. The hypotheses are satisfiable.

Abstract. RandomizedWordRAMAbstract.quickselect matches the library theorem. One program p is fixed before w, k and input; the output is input.mergeSort.getD k 0; the frame a < 2 ∨ n + 2 ≤ a covers M[0] and M[1]; and the out-of-range clause includes expectedTime = 8. The group is still not in catalogue.json, consistent with the earlier decision on #1142. The Formal abstract PDFs job is green, but the rendered page was not inspected as part of this review.

Requested changes

1. Citation (inline). The module docstring cites [MitzenmacherUpfal2017], "Section 2.5 (Theorem 2.5 / LazySelect background)". In the 2nd edition, §2.5 is the expected run time of quicksort. The randomized median algorithm is in §3.5, and it is a sampling algorithm, not RANDOMIZED-SELECT. I could not match "Theorem 2.5" to selection. Please either drop the M&U reference or cite §3.5 as related background. (A coordinator could also push this documentation fix directly.)
2. PR description. Please name the AI tool(s) used and what they were used for, as CONTRIBUTING.md asks; "Implemented with AI assistance" alone is thin. Please also add one sentence on the existing notions considered for the new public definitions (expSubCost, IsCut, SelectInv, the potentials), for example that they are specific to this algorithm and that Quicksort.subCost/PartInv don't fit.

Nits (non-blocking)

• sum_max_pivot_le and list_map_sum_nat_eq_sum_range repeat Quicksort.sum_subCost_pivot_le and its private list_map_sum_eq_sum_range almost line for line. A shared rank-domination lemma in Quicksort, valid for any g monotone in both arguments, would serve both algorithms. This is fine as a follow-up.
• Several public declarations are proof scaffolding: IsCut, SelectInv, stepPotential, callPotential, expPotential, and expSubCost with its lemmas. They could be private, unless you want them as API (Quicksort makes similar declarations public).
• eq_mergeSort_getElem_of_perm_of_partitioned is a general fact about lists and could later move to a list module.
• "Hoare's FIND" is named without a reference; a Hoare1961 bib key would credit it.
• Tests use non-terminal by simp [dup6]; omega; simp only would follow the hygiene convention.

Scope of this review: I read every public statement and definition, the abstract and bridge statements, and the tests, and sampled the proofs. CI (ci-checks) is green on this head and the PR is mergeable. I did not build locally.

[SamuelSchlesinger]

Requested: in Mitzenmacher–Upfal (2nd ed.), §2.5 is "Application: The Expected Run-Time of Quicksort". The randomized median algorithm is §3.5 (Chapter 3), and it is a sampling-based algorithm rather than RANDOMIZED-SELECT. I couldn't match "Theorem 2.5" to selection. Could you drop this reference, or change it to something like [MitzenmacherUpfal2017], Section 3.5 (sampling-based median selection, related background)? Please update the ## References entry on line 73 to match.

[SamuelSchlesinger]

nit: this proof (and list_map_sum_nat_eq_sum_range above) repeats Quicksort.sum_subCost_pivot_le and its private list_map_sum_eq_sum_range almost line for line; only g differs. A single lemma in Quicksort would cover both. It could say that for any g : ℕ → ℕ → α monotone in both arguments, ∑ k : Fin u.length, g (u.countP (· < u[k])) (u.countP (u[k] < ·)) ≤ ∑ r ∈ range u.length, g r (u.length - 1 - r). Fine as a follow-up.

[SamuelSchlesinger]

nit: SelectInv, IsCut, the three potentials and expSubCost look like proof scaffolding for selectSlice_spec. Consider making them private, unless you intend them as reusable API.

[SamuelSchlesinger]

nit: each conjunct here has its own ∃ p, so this is weaker than "the quickselect program returns 0, 2, 2, 4". Taking one p from quickselect and stating all four facts about it would make the test match its docstring.

[orbitingflea]

Fixed in 91790fc (with upstream/main merged in dcfdac5):

• Citation (Complexity/Algorithms/WordRAM/Quickselect.lean): Changed [MitzenmacherUpfal2017] from Section 2.5 to Section 3.5 (sampling-based median selection, related background) and removed the uncited (Hoare's FIND) attribution.
• Public surface and register aliases (Complexity/Algorithms/WordRAM/Quickselect.lean): Marked internal proof scaffolding private (four_mul_sum_max_le, expSubCost*, sum_max_pivot_le, eq_mergeSort_getElem_of_perm_of_partitioned, fits_add_two, IsCut, SelectInv, SelectInv.exit_post, stepPotential, callPotential, expPotential, narrowRange_spec, partitionAndNarrow_spec, selectStep_spec, and selectSetup_spec), aligned ## Main definitions and ## Main results with the remaining public declarations, and aliased shared registers in Quickselect.Reg to Quicksort.Reg.*.
• Bridge factoring (abstracts/ComplexityAbstracts/RandomizedWordRAMBridge.lean): Simplified Exec.toExact_loadHeader to reuse Quickselect.loadHeader_spec and factored ExecRand.toExact_loop (shared by ExecRand.toExact_partLoop and ExecRand.toExact_selectLoop).
• Tests (ComplexityTests/WordRAMQuickselect.lean, ComplexityTests/Abstracts/RandomizedWordRAMTests.lean): Moved ∃ p : Program 16 outside the rank quantifier in quickselect_dup6_rank and quickselect_dup6_concrete_ranks so one program is tested across all ranks k = 0, 2, 3, 5, included the untouched-memory postcondition in the out-of-range test theorems, and replaced non-terminal simp with simp only.
• PR description: Updated the PR body to include the AI disclosure, the public-surface rationale, the uncatalogued status of RandomizedWordRAMAbstract, and validation details.

[SamuelSchlesinger]

reviewer-jetski-5208-1339b for coordinator-jetski-5208b1c7 (agent review, not human approval): APPROVED at 91790fc3fbd9f3964adb1c6b17a081b12a543a9b

Thanks @orbitingflea for the quick and thorough follow-up. This is a delta re-review against the previous review at 131eeb94. It covers the fix commit 91790fc3; the merge commit dcfdac52 only brings in upstream main and touches none of this PR's files.

Earlier blockers, all resolved

1. Citation. The module docstring and ## References now cite [MitzenmacherUpfal2017], Section 3.5, as related background on sampling-based median selection. CLRS §9.2 stays the primary source for RANDOMIZED-SELECT. The unsourced "Hoare's FIND" attribution was also dropped.
2. AI disclosure. The PR body now names the tool and its role: Gemini agents, working under your direction, wrote the definitions, proofs, tests, abstract and description.
3. Existing notions. The definitions in question (IsCut, SelectInv, expSubCost, the three potentials) and the scaffolding lemmas are now private. The PR body explains that they differ from Quicksort's two-sided stack invariant because quickselect tracks a single active subarray. The public surface left is the structured program pieces, selectSlice, code/program, the time budgets, and their specs, which the Basis.exact bridge needs. Each has a docstring.

Delta check. No public statement changed meaning. quickselect_correct_and_bounds, quickselect_out_of_range and the abstract RandomizedWordRAMAbstract.quickselect are textually unchanged apart from docstring rewording. The rewording still matches the statements: k < n, InputFits w (k :: input) and 2 * (Nat.log 2 n + 1) ≤ w give 10n² + 15 steps, at most n - 1 rand calls, output input.mergeSort.getD k 0, an in-place partition around 2 + k, frame [2, n + 2), and expectedTime ≤ 80n + 15; n ≤ k gives 8 deterministic steps, output 0 and expectedTime = 8. The Quickselect.Reg aliases now point to Quicksort.Reg.* and keep the same indices, since the proofs and bridge still check. The bridge refactor is proof-only: it adds a private generic ExecRand.toExact_loop, and Exec.toExact_loadHeader now goes through loadHeader_spec. The tests are stronger. quickselect_dup6_rank and quickselect_dup6_concrete_ranks now fix one program p for all ranks; for example, on [4,2,4,0,2,1] with k = 3 that single p returns 2 at M[5]. The out-of-range tests now include the unchanged-memory postcondition. The non-terminal simp calls are now simp only. I found no sorry, native_decide or heartbeat overrides.

Abstract impact. Only the docstrings of RandomizedWordRAMAbstract changed, and they match the unchanged statements. The group is still uncatalogued, as before.

CI. ci-checks and the Formal abstract PDFs job are green on this exact head, and the PR is mergeable. I did not build locally or inspect the rendered PDF.

Nit (follow-up, non-blocking). The earlier suggestion still stands: sum_max_pivot_le and Quicksort.sum_subCost_pivot_le could share one rank-domination lemma in Quicksort covering any g monotone in both arguments. Both are now private, so this is purely internal cleanup.