Challenge 8 (partial): no-UB proofs and sorting-correctness harnesses for smallsort

[samiam713]

Summary

This is a partial contribution — it does not close Challenge 8. The challenge's
success criteria cover arbitrary valid lengths; the harnesses here verify the
smallsort module per concrete length with fully symbolic contents up to a measured
model-checking tractability frontier, and past that frontier coverage is per-callee
rather than end-to-end (the exact gap is itemized below). Whether and how a partial
result counts toward the challenge is entirely the maintainers' call; this PR only
reports what was proven — and, quantitatively, what resisted proof.

Two things are offered for Challenge 8
(tracking issue #56):

1. 46 Kani harnesses, verified from a pristine clone: absence-of-UB proofs plus
   sorting correctness asserted as sortedness AND multiset-permutation of the
   input, per concrete length, with every specialization body steered via distinct
   element types. The dual oracle is directly responsive to the Challenge 8: Verify safety and sorting correctness of SmallSort #576 review
   (2026-08-16): the degenerate constant-overwrite "sort" that review described
   passes a sortedness-only check and is caught only by the permutation oracle
   (demonstrated by mutation, below). One file changed; everything added lives in a
   #[cfg(kani)] mod verify block — zero production lines change, zero verification
   escape hatches (no stubs; the only kani::assumes are documented preconditions,
   itemized in the Verification section).

2. A measured tractability frontier — where, concretely, bounded model checking of
   this module stops being feasible, per path, element width, and SAT solver. This is
   the quantified form of the wall Add contracts for SmallSort #234 hit ("out of memory or several tens of
   minutes") before being abandoned: the wall is now measured rather than merely hit.
   It is offered as information bearing on what a bounded model checker can reach on
   this module as currently specified — not as an argument about the challenge.

Correctness oracle. Every correctness harness asserts both properties: the output is
non-decreasing under the comparator, and for every input value its multiplicity is
preserved (multiset equality — a degenerate "sort" that overwrote the slice with a
constant could not pass). Contents are fully symbolic (kani::any()); no value
constraints anywhere.

What is covered, and how far. The small-sort API is bounded by design
(SMALL_SORT_FALLBACK_THRESHOLD = 16, SMALL_SORT_GENERAL_THRESHOLD =
SMALL_SORT_NETWORK_THRESHOLD = 32). Verification is one harness per concrete length
with symbolic contents. Model-checking cost turned out to be the binding constraint (as
#234 found before us; measurements below), so coverage has three tiers:

1. Insertion-path domains — the two default (non-Freeze) small_sort impl
   bodies (insertion-sort paths, threshold 16) are verified at lengths 0..=3 and 7
   via Cell<i32> instantiations, and insertion_sort_shift_left at lengths 1..=4
   with offset symbolic over its full accepted range (longer lengths exceed the
   budget once the insertion loops' data-dependent path conditions compound —
   sharply: len 4 verifies in seconds, len 8 exceeds 25 minutes; measurements
   below).
2. To the tractability frontier — the Freeze bodies end-to-end:
   small_sort_general_with_scratch (stable, via i32 at every length 0..=8 with the
   caller-shaped 48-slot scratch, plus u128 and non-Copy / oversized element types
   steering every specialization branch), and small_sort_network (via i32 at every
   length 0..=8 and u8 at 9). This exercises the len < 2 no-ops, copy-1,
   sort4_stable-pair, insertion, and sort9_optimal-region branches, and the
   threshold/has_efficient_in_place_swap/MAX_STACK_ARRAY_SIZE dispatch in all
   three trait impls.
3. Beyond the frontier, per-callee — for lengths whose composed proof exceeds any
   reasonable CI budget (measured: stable general ≥ ~10, network ≥ ~9 at 32-bit width;
   no width or SAT-solver choice moves the wall materially), each callee the long
   lengths execute is verified directly, at full i32 width, at its exact call-site
   shape and under its documented precondition: sort4_stable (criterion 6),
   sort8_stable at its only call shape (8),
   swap_if_less with symbolic in-bounds positions (criterion 4), and the
   sort9_optimal network at its guard length (8-bit elements — 32-bit is
   intractable there). The gap this leaves is stated plainly: the end-to-end
   composition at long lengths is not model-checked, and two branches resisted even
   direct verification at any width or solver tried — sort13_optimal (its 45-swap
   chain) and bidirectional_merge at lengths ≥ 16 (even with sorted halves
   assumed). Those two, plus the composed long lengths, are the precise unverified
   remainder.

Remaining criteria functions: swap_if_less (pair ordered + preserved, rest
untouched; distinctness of the two positions deliberately not assumed),
sort4_stable (sorted permutation, destination fully initialized),
insertion_sort_shift_left (permutation unconditional; sortedness under the documented
sorted-prefix premise, asserted as an implication so the unsorted-prefix case is still
explored for UB), has_efficient_in_place_swap.

Measured tractability (why the frontier is where it is)

On a 20-thread / 31 GiB box with the repo-pinned toolchain, single harness per run:

Proof	Wall clock
network path, i32, len 9	~1030 s
network path, i32, len 15	1207 s (minisat) / >1500 s (kissat, killed)
network path, u8, len 9	258 s
network path, u8, len 10–13	>420 s each (capped)
stable general, i32, len 12–17	>420 s each (capped)
stable general, i32, len 32	>3600 s (timeout)
stable general, u8/u128/20-byte elements, len 16+	>420–600 s each (capped)
symbolic-offset insertion, i32, len 8 / 12	>1500 s each
symbolic-offset insertion len 16+; Cell<i32> insertion paths len 15+; u128 general len 8	stuck >30 min each
everything in this PR	worst kept proofs: sort8_stable 513 s, sort9_optimal 270 s, network u8 len 9 258 s; the rest are seconds to a few minutes

The cost driver is CBMC's symbolic-pointer case-splitting (swap_if_less /
sort4_stable select pointers via hint::select_unpredictable; the merge loops
advance pointers by data-dependent amounts), which compounds per step — element width
and solver choice barely move it. This is the quantified form of what #234 reported
("out of memory or several tens of minutes") before being abandoned.

Verification

From a pristine clone at current main (2bd54c9) plus only this change, with the
repo-pinned toolchain (Kani 0.67.0 built at d4df833c, nightly-2025-11-25),
re-verified 2026-09-09 after the CI-budget adjustment (addendum below):

kani verify-std -Z unstable-options ./library \
  -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi \
  -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts \
  --harness check_ss_ --jobs=8 --output-format=terse \
  --cbmc-args --object-bits 12
...
Complete - 46 successfully verified harnesses, 0 failures, 46 total.  (--jobs=8)

Assertion liveness was checked by mutation: negating the sortedness oracle makes the
harnesses FAIL, and a production-side degenerate mutation (merge output overwritten with
copies of one element — exactly the "constant overwrite" scenario from the #576 review)
passes sortedness but fails the permutation oracle, which is the property that
review found missing.

Loops are covered with generous #[kani::unwind] bounds (len + 2); unwinding
assertions stay enabled, so a too-small bound fails the proof rather than masking
exploration. The only kani::assumes are documented preconditions (index bounds,
offset range). No stubs. Harnesses pin a SAT
backend explicitly, following existing in-tree practice (num/mod.rs,
ptr/mod.rs): #[kani::solver(cadical)] — Kani's own default — on eleven,
and #[kani::solver(kissat)] on the two where CI measured kissat faster
(check_ss_sort9_optimal, check_ss_unstable_u8_len_9). The setting is
per-harness because the measurements are; see the CI addenda below.

Scope and known limits

• The long-length composed proofs are the stated gap (tier 3 above): past the
  measured frontiers, end-to-end model checking exceeds any per-proof CI budget by an
  order of magnitude (table above). Coverage there is per-callee, plus branch coverage
  of the dispatch logic. If the committee prefers, the frontier harnesses can be
  extended on bigger iron — the harness shapes accept any length by macro invocation.
• The comparator is a fixed strict order on the element key (a < b). UB-freedom under
  an adversarial comparator (arbitrary results / panics) is not modeled.
• Correctness is asserted in harnesses rather than as #[ensures] attributes on the
  trait impls: the permutation property needs the pre-state of a generic &mut [T]
  behind specialized trait methods with closure parameters, which function-contract
  syntax cannot currently express there.
• Stability of the stable variant is not asserted (not among the challenge's criteria).
• Element instantiations are concrete (i32, Cell<i32>, u128, a non-Copy
  wrapper, [u64; 11], u8), chosen to steer every specialization/dispatch branch.

CI addendum (2026-09-09). The first CI run failed two ways, both fixed in the
second commit: the verify module was not rustfmt-formatted
(./scripts/check_rustc.sh --bless applied — formatting only), and four harnesses
exceeded the "Verify std library using autoharness" job's 10-minute per-harness
budget on the standard GitHub runners ("CBMC timed out"):
check_ss_stable_i32_len_9 and check_ss_unstable_noncopy_len_9 (both OSes),
check_ss_unstable_cell_len_8 (both OSes), and check_ss_stable_cell_len_8
(ubuntu; macOS passed it at 596.2 s of the 600 s cap). Those four are stepped back
one length — the two len-9 harnesses dropped (their families stay dense 0..=8) and
the two Cell len-8 harnesses moved to len 7 — taking the count from 48 to 46;
no production changes. The practical frontier is therefore set by the standard
runners (2–3× slower than the 20-thread box the tables above were measured on),
not by local iron. The slowest kept harnesses still run close to the cap in CI
(ubuntu: check_ss_unstable_i32_len_8 583.2 s, check_ss_sort8_stable 534.6 s,
check_ss_unstable_noncopy_len_8 523.2 s; macOS: check_ss_stable_i32_len_8
493.4 s), which is a known flake risk on a slow runner day.

CI addendum, second iteration (2026-09-09). The following run still timed out on
both runners, on two harnesses that had passed the run before
(check_ss_sort8_stable, check_ss_unstable_i32_len_8) — runner variance against
thin margins rather than a new wall. The fix is the SAT backend, not the scope: the
13 solver pins move from kissat to cadical — revised once more below, where
the right setting turned out to be per-harness rather than global.
Measured single-run A/B on one machine, one harness per invocation, identical load:

harness	kissat	kissat, tightened unwind	cadical	minisat
check_ss_sort8_stable	578.2 s	551.7 s	297.7 s	>1500 s (killed)
check_ss_unstable_i32_len_8	643.3 s	674.5 s	438.5 s	>1500 s (killed)

Tightening the unwind bounds below len + 2 measured as noise in both directions
(-4.6% / +4.9%), so the generous bounds stay. Re-running the whole suite
sequentially under cadical: 46 successfully verified harnesses, 0 failures, 46
total — slowest 407 s, next-slowest 285 s, against the 600 s per-harness cap.
Nothing was stepped back or dropped to achieve this: the harness count, the
lengths, the element types, the fully symbolic inputs, both oracles and the unwind
bounds are all unchanged from the run above; only the SAT engine differs.

CI addendum, third iteration (2026-09-09). The blanket move to cadical did fix
the two harnesses that had been timing out — on the ubuntu runner
check_ss_unstable_i32_len_8 went 583.2 s → 339.1 s and check_ss_sort8_stable
534.6 s → 313.1 s, and the macOS autoharness job passed all 46 — but it pushed two
different harnesses over the cap: check_ss_sort9_optimal and
check_ss_unstable_u8_len_9, which kissat had been solving in 276.8 s and 380.5 s,
both hit the 600 s timeout. So solver choice here is per-harness, not global: the two
u8/len-9 proofs are the ones kissat wins. The pins are split accordingly — cadical
on the eleven harnesses where it measured faster, kissat retained on those two. That
is the only change; the harness count, lengths, element types, fully symbolic inputs,
both oracles and the unwind bounds are untouched.

Being plain about what this does and does not buy: it moves every harness off the cap
by a measured margin rather than by scope reduction, but the margins on the slowest few
are still a few minutes on a shared runner, so a slow runner day remains a flake risk —
the same caveat as the first addendum, not a new one.

Relationship to #576: that PR covers the same challenge; its review (2026-08-16) found
two blockers — correctness asserted sortedness only (no permutation check), and every
harness pinned [i32; 4]. This PR is an independent implementation built to that
review's direction: sortedness ∧ permutation everywhere, and per-length sweeps plus
callee proofs in place of a single pinned shape, with the genuine cost wall measured and
disclosed rather than papered over. Also noting #234 (closed 2025 after hitting exactly
this wall) and #640 (withdrawn unreviewed, 2026-08-26).

AI disclosure: these harnesses were developed with substantial AI assistance (Claude,
Anthropic), with human direction and review; the commit carries a Co-authored-by
trailer accordingly. All proofs were re-verified from a pristine checkout before
submission.

Toward #56.