Repository navigation
Challenge 8: Contracts for SmallSort #56
Description
Link to PR: #57
Link to challenge: https://github.com/model-checking/verify-rust-std/blob/main/doc/src/challenges/0008-smallsort.md
SmallSort #56Link to PR: #57
Link to challenge: https://github.com/model-checking/verify-rust-std/blob/main/doc/src/challenges/0008-smallsort.md
Activity
[-]Tracking issue for verification of SmallSort[/-][+]Challenge 8: Contracts for `SmallSort`[/+]BusyBeaver-42 commentedon Jan 9, 2025
Hi, I have a few questions about this challenge.
Missing safety requirement
I believe
merge_downis missing a requirement in theSAFETYcomment. Specifically,dst.sub(1)is called, but theSAFETYcomment does not guarantee that the resulting pointer remains within the same allocated object. This is not a significant issue since it's a private function, and when it is called,dst.sub(1)is indeed within the same allocated object.EDIT: I've opened the following issue: rust-lang#135984.
Can the absence of "invalid values" be verified with a separate tool?
"Invalid values" refer to the following scenario: If the input array is
[1, 2, 3]and the output array is[1, 1, 1], then although the output array is sorted, an "invalid value" is created. In this example, it is not a safety concern, but it could become one for non-Copytypes.I believe this requires a separate tool because verifying with
kanithat the multiset (like a set but counting repetitions) of inputs matches the multiset of outputs is extremely slow. For example,sort4_stablealready takes approximately 6 minutes to verify.How arbitrary does
is_lesshave to be when verifying correctness?To verify safety, since the sorting methods are safe and are called with a user-provided
is_less, verification has to be done with a function that returns a random boolean (kani::any()).However, what
is_lessshould be used when verifying correctness? For example, is it sufficient to verify correctness only for the default ordering of integers? Alternatively, should verification be conducted on a custom type with 32 distinct values, allowing for testing of any weak total ordering on these 32 values? This second approach is likely to perform poorly.Additionally, what types
Tshould be tested?What is the limit for memory and runtime?
I need to use
stub_verifiedonsort13_optimalbecause the code thatkanianalyzes becomes too large when verifying the sorting methods. However, verifyingsort13_optimalis very resource-intensive due to the large number of statements it contains, as explained in this comment. It requires 50 GB of memory and takes 40 minutes (38 GB of this is swap memory, which might explain the lengthy runtime on my laptop).qinheping commentedon Jan 24, 2025
Thank you. The safety comments should be updated in the upstream if the proof shows that the current comments is actually not enough.
Yes, other tools are welcome.
The ultimate goal is to prove the correctness for arbitrary types and arbitrary ordering. However, we understand that model arbitrary ordering itself is very challenging. So proofs for primitive types with default ordering will be considered as a solid solutions.
qinheping commentedon Jan 24, 2025
We expect to run all proof on CI. So ideally the running time of a single proof should be less than ~2 minutes on a GitHub standard runner. However, if the proof is running into the limitation of Kani/CBMC, we suggest you to open a PR with the proof so that we could merge it once we have made performance improvements that get the CI time down to a reasonable amount.
Challenge 8: Verify safety and sorting correctness of SmallSort
TheodorNEngoy commentedon Sep 5, 2026
I'm assessing a possible contribution to Challenge 8. Before investing in a complete solution, could you clarify:
i32coverage for every length up to each SmallSort variant's threshold, including sortedness and multiset preservation, satisfy the intended sorting-correctness scope? Forinsertion_sort_shift_leftas a standalone helper, is proof beyond those thresholds required?I have a local draft harness with tested assertion helpers, but have not yet run the Kani proof and am not claiming a completed solution.
docs: provisional submission minimum per maintainer practice (PR mode…
Tiramisu-Cake commentedon Oct 23, 2026
Hi!
We are working on a Challenge 8 solution and want to make sure we target the right domain before submitting. The challenge text asks for verification "for all possible slices with arbitrary valid length"; the review on #678 clarifies that length means up to the specialization thresholds (16 for the fallback path, 32 for the general/network paths) and that
sort13_optimal,bidirectional_mergeand contract-form correctness are expected. Two points are still unclear to us:Element types. Is coverage by a set of representative element types that exercises every specialization (Freeze / non-Freeze, Copy / non-Copy,
size_of <= 16and> 16, ZST, interior mutability) sufficient for acceptance, or is a proof that is generic overT(e.g. with a deductive tool) required for the memory-safety part?Comparator behavior. For the no-UB criterion, is it sufficient to verify with a pure, total, non-panicking
is_less, or must the proofs also cover comparators that may panic or keep state (theCopyOnDrop-style unwind recovery paths ininsert_tail/small_sort_general)? If panicking comparators are required, is a proof of "no UB on unwind" enough, without any functional guarantee after a panic?A short answer on these two points would let us scope the submission correctly. Thank you.
docs(ch8): apply coordinator review 837c2e6 to plan revisions 4-5
docs(ch8): minimal plan revision 6 — wave 1 outcome and wave 2 work o…
docs(ch8): revise plan revision 6 per review — rationale, budget, mac…
docs(ch8): apply review corrections to plan revision 7