Challenge 8: Verify SmallSort with Kani

[v3risec]

Summary

This PR adds Kani verification coverage for Challenge 8 (smallsort). The verification targets all seven functions listed by the challenge, with the main focus on the three specialized small_sort trait APIs:

• StableSmallSortTypeImpl::small_sort

• UnstableSmallSortTypeImpl::small_sort

• UnstableSmallSortFreezeTypeImpl::small_sort

• swap_if_less

• insertion_sort_shift_left

• sort4_stable

• has_efficient_in_place_swap

For the three small_sort APIs, the end-to-end harnesses check:

• execution of the real implementation without introducing unverified stubs or path pruning,

• sortedness under a valid ordering,

• preservation of the input multiset,

• symbolic slice lengths up to the threshold selected by the corresponding specialization.

Specialization coverage

The harnesses exercise the relevant smallsort dispatch paths.

Stable small sort

The stable implementation covers:

• non-Freeze fallback sorting up to length 16,

• Freeze general sorting up to length 32,

• the size_of::<T>() <= 16 general path using the 8-element presort primitive,

• the size_of::<T>() > 16 general path using the 4-element presort primitive.

The non-Freeze path is split into separate memory-safety, sortedness, and permutation proofs to keep solver cost manageable.

Unstable small sort

The unstable implementations cover:

• non-Freeze fallback,

• Freeze + Copy network sorting,

• Freeze + Copy general sorting for both small and larger element sizes,

• Freeze + Copy oversized fallback,

• Freeze + !Copy general sorting,

• Freeze + !Copy oversized fallback.

Equivalent specialization coverage is included for UnstableSmallSortFreezeTypeImpl directly.

The general route is instantiated with both element sizes at or below the 16-byte presort cutoff and element sizes above that cutoff, ensuring both general-sort presort strategies are exercised.

Helper functions

swap_if_less and sort4_stable have explicit safety contracts and dedicated proof_for_contract harnesses.

insertion_sort_shift_left is exercised with symbolic length and offset over the range used by the current small-sort implementations.

has_efficient_in_place_swap is checked across representative zero-sized, small, large, and interior-mutable element types.

Current limitations

Some full-domain proofs still exceed the current 10-minute per-harness verification budget. The length-32 Freeze/general/network paths inline several expensive operations into a single SAT instance, including presorting, insertion extension, and bidirectional merge. An full-domain Stable Freeze experiment required more than 20 minutes locally.

The next step is to investigate modular verification of the expensive internal primitives so the top-level proofs can reuse verified summaries instead of repeatedly expanding the complete implementations.

The sorting properties of the three specialized small_sort methods are currently expressed as end-to-end harness assertions rather than reusable Kani function postcondition contracts. Direct contracts on these specialized methods are currently limited by specialization and generic old-state handling in the pinned toolchain.

No assume(false) path pruning or unverified behavioral stubs are used to make the sorting proofs succeed.

Resolves #56

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