[Tiramisu-Cake]

This PR verifies the smallsort module (#56) with Kani on the real implementations, within explicit bounds: memory
safety of the three small_sort trait entries and the helpers behind them at lengths that reach every dispatch
boundary up to N32; sorting correctness (sortedness plus full-value multiset preservation) on the general, fallback
and network routes; and requires/modifies contracts on five real helpers, proved and then used at real call sites.
235 harnesses run SUCCESSFUL on each OS in the repository's unchanged Kani workflow, and 13 negative controls check
that the oracles and contracts reject what they should. Function bodies, signatures, workflows and tool pins are
unchanged.

Highlights

• Memory safety on the real routes. All three trait entries (stable, unstable, unstable-Freeze) and the general,
  fallback and network routes behind them run as-is, at representative lengths that include every dispatch boundary up
  to N32. Comparators return arbitrary answers or mutate through a Cell; element types include a Drop type, a ZST
  and sizes of 1, 8, 16, 17, 85 and 86 bytes, which select every size-dependent branch.
• Sorting correctness with a full-value oracle. Sortedness plus multiset preservation, stated for an arbitrary
  symbolic value: it occurs as often after the sort as before. Some families sort by a key (x >> 1) under which
  distinct values tie, so a key-only oracle would miss payload corruption; the network and logical-model families use
  the ordinary <. Covered on the general and stable routes at u8 and u64 N0..9, on the fallback route at N0..6, and
  on the network route (sortedness up to N13, multiset preservation below the network width, and permutation of
  distinct tags at N9 and N13 for an arbitrary comparator).
• Contracts on the real helpers. requires/modifies on swap_if_less, insert_tail,
  insertion_sort_shift_left, sort4_stable and bidirectional_merge, proved by 16 proof_for_contract harnesses
  with an arbitrary-answer comparator, and used by four stub_verified consumers at real call sites with the same
  element type, comparator and allocation as the proof (the u8 networks at N9, N13 and N32; u64 sort8_stable).
• Sorting contracts where this Kani accepts them. ensures (model-sorted output, preserved full-value count) on
  proof-owned profiles of the helpers and on wrappers of the three trait entries at N2. Contracts directly on the
  trait methods are blocked by two Kani issues we reported with reproducers (Limitations).
• Calibrated negative controls. Thirteen harnesses: a mutant swap_if_less, payload corruptions, wrong
  comparators, requires violations, a comparator writing outside the write set, a duplicated tag. Each fails exactly
  its designated check on this library tree with the pinned Kani.

Challenge criteria

Criterion	In this PR
No UB: the three small_sort trait entries	real routes at representative lengths up to N32 on the type matrix below, Kani default checks
No UB: swap_if_less, insertion_sort_shift_left, sort4_stable, has_efficient_in_place_swap	contracts proved on the listed domains (first three); real bodies with arbitrary comparators; insertion_sort_shift_left body at every offset for u64 N1..20; predicate on 12 types
Contracts showing that small_sort sorts	ensures on N2 wrappers of each entry; sorting proved by harness oracles at the lengths below; contracts on the trait methods themselves await kani#5116 and kani#4908
Lengths	bounded as listed; correctness to N9 (general, stable), N13 (network sortedness), N6 (fallback)
UB classes	dangling, misaligned and out-of-bounds accesses on every path above; see Limitations for the rest

What is checked (235 harnesses, organizer flags including --no-assert-contracts)

Group	Harnesses	Route / function	T, N	Property
General / stable entries	25	general route (small_sort_general*)	u8, u64; N0..9	key order + full-value count
Fallback insertion	7	small_sort_fallback	u8, u64; N0..6	key order + full-value count
Network entry	16	small_sort_network	u8 N0..7, 9..13; u64 N0..7, 9	order; count only for N < 9
Insertion phase	5	insertion_sort_shift_left from offset 9 or 13	u8 N10, 11, 14; u64 N10, 14	whole-array count, any input
Safety	92	all routes and dispatch	u64, u8, [u8; 16/17/85/86], a Drop type, ZST (stable trait entry, ()), Cell; dispatch to N32; insertion at every offset for u64 N1..20 and Cell N1..5, N20; stable route with minimal scratch at N2	Kani default checks up to normal return
Drop / tag	19	fallback, insertion, general and network routes	selected N; fixed distinct u8 tags on network N9, N13	drop counts and tag permutation at normal return
Trait entries, logical model	6	small_sort	Cell<u8>, Drop key	logical order + count
Helpers	9	has_efficient_in_place_swap, sort4_stable, swap_if_less at equal positions, helper pairs	type matrix; N2, N4, N10	predicate; safety + value preservation
Contract proofs on profiles	36	swap_if_less 14, sort4_stable 2, insert_tail 5, bidirectional_merge 12, N2 forwarding wrappers 3	exact listed allocations	order contract on the executed domain
Contracts on the real helpers	20	proof_for_contract 16, stub_verified consumers 4	see Contracts	requires and modifies on the executed domain

Full-value multiset preservation uses an independent symbolic probe on the listed integer and byte-array fixtures;
Cell and Drop fixtures use their logical models. The tag harnesses sort fixed distinct u8 tags with an arbitrary
comparator; that this carries over to arbitrary values (data moves only by comparator answers) is a source-level
argument.

Contracts

On the real helpers. Safety contracts: requires on pointer validity and allocation geometry, modifies on the
element or destination memory. Executed domains:

• swap_if_less: u8, u64 and [u8; 17] in a 4-element allocation; u8 in 9- and 13-element allocations; u8 and u64
  in a 32-element allocation with any base and any two positions, equal positions included.
• insert_tail: u64, tail 1..4 in a 5-element allocation, and tail 1..15 from the start of a 17-element allocation.
• insertion_sort_shift_left: u64 arrays of lengths 2 and 3, every valid offset. The body itself is also checked
  directly at every offset for lengths 1 through 20.
• sort4_stable: u64, disjoint 4-element source and destination.
• bidirectional_merge: u64 of length 2 and 4, and of length 8 at the geometry of the 48-element stable scratch.

Each consumer replaces the real call with the proved contract through stub_verified, with the same element type,
comparator and allocation domain as the contract proof: the unstable u8 network at N9, N13 and N32 with
swap_if_less, and u64 sort8_stable with bidirectional_merge. The same routes are also checked with their real
bodies. Proofs on the real helpers use one comparator function item per harness that returns an arbitrary answer, so
no ordering law is assumed. Only the executed domains are claimed.

On profiles. Sorting contracts (ensures: model-sorted output, preserved full-value count) are checked on
proof-owned profiles that forward a fixed element type and one canonical function-pointer comparator to the real
helpers (a guard rejects any other comparator), and on three N2 wrappers that call the trait entry points.

Negative controls (13, behind cfg(kani_smallsort_controls), which CI never sets)

• a negated swap_if_less copy;
• two checks that the oracle sees a changed payload;
• the canonical-comparator guard of the wrappers;
• four consumers that use a profile contract with a wrong comparator, so the comparator precondition must fail;
• three calls that violate a real helper's requires: out-of-allocation swap_if_less, insert_tail with
  begin == tail, and bidirectional_merge into an overlapping destination;
• a swap_if_less contract proof with a comparator that increments a captured counter, which must fail the write-set
  check;
• a duplicated tag on the network N9 tag harness.

We ran all thirteen on this library tree with the pinned Kani (cd355b0b), outside GitHub Actions: each fails exactly
one check, the designated one (report).

CI

We ran the upstream workflows unchanged on this commit in our fork via workflow_dispatch (fork runs, not upstream PR
checks):

• Kani run 42363378063: success on Ubuntu and macOS, including all 8 partition jobs, autoharness and
  Build JSON from logs, in attempt 1.
• Rust Tests, Flux, RAPx, KMIR, VeriFast, VeriFast (negative), GOTO Transcoder, Book and Testable SIMD: success in attempt 1.

In the autoharness runs all 235 SmallSort harnesses are SUCCESSFUL on each OS, with zero failed checks and
978/978 satisfied covers (counted from the logs; the workflow does not enforce covers). No warning comes from
the SmallSort files. SmallSort's summed verification time is 7,802 s on Ubuntu and 10,534 s on macOS, 65.9% and 70.3%
of the job's manual-harness total; the longest proof takes 246 s on Ubuntu and 340 s on macOS, below the 600 s
timeout (per-harness timings). The harnesses are independent: any of them can be split or moved behind the
opt-in cfg without touching the rest.

At this base the autoharness job runs on a pull request only with the run-autoharness label (or in the merge queue
or on dispatch); we would appreciate the label on this PR.

Limitations

Several of the remaining gaps come from Kani limitations that we reported or reproduced upstream; they are linked
below.

• Scope. Results hold for the listed types, comparators, lengths and allocation layouts. The write sets list
  element and destination memory only, since Kani cannot state the footprint of an arbitrary FnMut; the contracts
  are claimed for comparators that write nowhere else (a comment above swap_if_less says so, and the counter control
  checks it).
• Contracts on the trait methods. A contract on a specialization default fn is not accepted on the current pin
  (kani#5116), nor is a proof_for_contract on a trait method
  with its own generic F (kani#4908);
  the N2 wrappers are the nearest contract-form statement this Kani verifies. Kani main has since fixed the second
  case (kani#5135), which is not yet in the repository's pin; it
  opens direct contracts on the non-default small_sort implementations, which we intend to add here once the pin
  includes it.
• Lengths. Wider domains are limited by verification time; an extended u64 N10 composition on an earlier research
  tree also ran into kani-driver memory use (kani#5117).
• Panics. Seventy-one ordinary harnesses replace panic_on_ord_violation with an assume(false) stub; the other
  164 do not replace that function. Comparator panics and unwind recovery are not verified.
• UB classes. As in the repository's Kani profile, there is no uninitialized-memory or value-validity
  instrumentation on these routes: -Z uninit-checks reports unsupported operations here
  (kani#3300) and -Z valid-value-checks does not yet support
  copy_nonoverlapping (kani#3762), which these routes use.
  Writes to immutable bytes and aliasing beyond Kani's pointer checks are not modelled.
• Model trust. The array-select reproducer from kani#5104
  still fails on the organizer Kani pin cd355b0b
  (pin-check report);
  the four array-valued fixtures network::swap_contract_bytes16_n2, network::swap_contract_bytes17_n2,
  merge::sort4_contract_bytes16_n4 and merge::sort4_arbitrary_comparator_bytes16_n4 retain that model caveat.
• ZST and geometry. ZST coverage consists of direct stable SmallSort trait-entry checks on (). The public sort
  entry points short-circuit ZSTs, and select_nth_unstable skips selection work for them after validating the
  index. ZST comparators read with ptr::read, since read_volatile on a ZST gives spurious dereference failures
  (kani#5072). The stable Freeze route is checked with a separate
  48-element scratch and with the minimal scratch at N2. Tie stability is not proved separately.

Beyond this PR: wider domains (longer networks, more insertion lengths) need more verification time or tool support;
we left them out rather than stretch the CI budget, and can propose them separately.

Note for maintainers. The sort4_stable contract makes source/destination non-overlap explicit. The existing
SAFETY comment mentions validity for four reads and writes but does not state this condition; the implementation uses
copy_nonoverlapping.

Source. One commit on main at 233f96f66a (it merges cleanly with the current main): 17 files under library/, +3941/−0. The harnesses
live in core::slice::sort::shared::smallsort::verify (verify.rs opens with a module map). smallsort.rs gains only
the contract attributes, a comment on their write sets, three cfg(kani) geometry predicates used by the contracts and
the mod verify registration; library/core/Cargo.toml gets a check-cfg entry for the controls cfg.

This contribution was prepared with the help of AI assistants.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT
licenses.