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. 48 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..=8 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..=9 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-07 immediately before opening this PR:

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
...
Verification Time: 959.7045s
Complete - 48 successfully verified harnesses, 0 failures, 48 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. Several
harnesses pin #[kani::solver(kissat)] following the existing in-tree usage
(num/mod.rs, ptr/mod.rs).

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.

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.