Repository navigation
New challenge: Verify the safety of BinaryHeap functions - #747
Kieran-Hulsman wants to merge 2 commits into
Conversation
| - [27: Verify atomically reference-counted Cell implementation](./challenges/0027-arc.md) | ||
| - [28: Verify float to decimal conversion module](./challenges/0028-flt2dec.md) | ||
| - [29: Safety of `boxed`](./challenges/0029-boxed.md) | ||
| - [31: Verify the safety of `BinaryHeap` functions](./challenges/0031-binary-heap.md) |
There was a problem hiding this comment.
I’ll renumber the file, title and SUMMARY.md entry to the next free number once this is ready to merge.
feliperodri
left a comment
feliperodri
left a comment
There was a problem hiding this comment.
This is a well-targeted challenge. BinaryHeap moves elements with ptr::read and ptr::copy_nonoverlapping at positions picked by user-supplied Ord, so it's real unsafe code whose safety depends on code the library doesn't control. Requiring safety for any Ord, including inconsistent ones, is what makes it worth verifying. I checked the targets against library/alloc/src/collections/binary_heap/mod.rs on main: every listed function exists, the seven listed unsafe functions are all the unsafe fns apart from from_raw_vec/as_mut_slice (which you deliberately leave as correctness-only), and every function with an unsafe block is on the list. Nothing here overlaps an existing challenge or harness.
What blocks approval: the number 31 is also used by #595, and the UB list leaves out the intrinsic preconditions that Hole relies on. I'd also like the scope of panicking Ord stated, since it's what Hole's Drop exists for. Details inline.
What would flip this to approval:
- Renumber if #595 merges first (file name, title,
SUMMARY.md). - Add "Invoking undefined behavior via compiler intrinsics" to the UB list.
- Say whether the proofs must cover an
Ordthat panics (unwinding throughHole::drop), or that this is out of scope.
| |---------| | ||
| |Hole::new| | ||
| |Hole::get| | ||
| |Hole::move_to| |
There was a problem hiding this comment.
Praise: the Hole functions are the right core: Hole::new reads the element out with ptr::read, move_to and Drop write with ptr::copy_nonoverlapping, and every sift goes through them. Specifying their contracts first is what makes the safe methods tractable.
| |From<Vec<T>>| | ||
| |IntoIterSorted::next| | ||
| |DrainSorted::next| | ||
| |Drop for Hole| |
There was a problem hiding this comment.
Question: Hole restores the slice in drop so that a panic in Ord::cmp in the middle of a sift doesn't leave a duplicated or missing element. Line 70 requires safety for any Ord, but doesn't say whether that includes one that panics. Both approved tools stop at panics today: Kani reports a reachable panic as a failure and doesn't model unwinding, and VeriFast's proofs here run with -ignore_unwind_paths. Could you state whether unwinding through Hole::drop must be verified, or that panicking Ord is out of scope? Either is fine, but solutions need to know which.
There was a problem hiding this comment.
I think it should be out of scope. I've added this to the list of assumptions:
* A panicking `Ord` is out of scope: solutions need not verify unwinding through `Drop for Hole`.|
|
||
| The unsafe functions `from_raw_vec` and `as_mut_slice` require callers to keep the contents a max-heap. This is a correctness requirement, not a safety one, so the functions above must be safe even when the contents are not a max-heap. | ||
|
|
||
| The verification must be unbounded---it must hold for heaps of arbitrary length. |
There was a problem hiding this comment.
Praise: worth keeping. rebuild_tail branches on self.len() <= 2048, so bounded proofs would miss a whole code path.
|
|
||
| The verification must hold for generic type `T` (what satisfies this clause is to be decided in [issue #734](https://github.com/model-checking/verify-rust-std/issues/734)). | ||
|
|
||
| The verification must hold for any implementation of `Ord` for `T`, including ones that return inconsistent results. |
There was a problem hiding this comment.
Praise: this is the requirement that gives the challenge its value; a model of Ord that may return anything is exactly what a proof should assume.
| ### List of UBs | ||
|
|
||
| All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
|
||
| * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. | ||
| * Reading from uninitialized memory except for padding or unions. | ||
| * Producing an invalid value |
There was a problem hiding this comment.
Bug: Hole relies on ptr::copy_nonoverlapping and ptr::read, whose preconditions (non-overlapping, valid, aligned) are intrinsic UB rather than plain dangling accesses. Please add "Invoking undefined behavior via compiler intrinsics", as Challenges 2 and 29 (Box) do. Leaving out "mutating immutable bytes" is right here.
There was a problem hiding this comment.
updated! the list of UBs now has this line:
* Invoking undefined behavior via compiler intrinsics.| | Implementation | | ||
| |---------| | ||
| |TrustedLen for IntoIterSorted| | ||
| |TrustedLen for DrainSorted| |
There was a problem hiding this comment.
Question: IntoIter also has unsafe impls with safety obligations: TrustedFused, SourceIter (with unsafe fn as_inner), InPlaceIterable and AsVecIntoIter, which feed Vec's in-place collection. Are they in scope, or covered by the Vec challenges? A sentence saying which would prevent solutions from guessing.
There was a problem hiding this comment.
I think it should be out of scope, which is now said explicitly in the description
The other `unsafe impl`s on `IntoIter`
(`TrustedFused`, `SourceIter`, `InPlaceIterable`, `AsVecIntoIter`)
delegate to `vec::IntoIter` and are out of scope for this challenge.| ------------------- | ||
|
|
||
|
|
||
| ## Goal |
There was a problem hiding this comment.
Nit: the template has Description and Assumptions sections, which this proposal doesn't. A short Description and an Assumptions section (for example "Vec's own safety may be assumed") would match the other challenges. The path in parentheses could also be a link, as in other challenges.
There was a problem hiding this comment.
updated! i've added description & assumptions sections, and linked the path
feliperodri
added
the
Challenge Proposal
Proposes a challenge to verify the safety of
BinaryHeap: theHoleand sift functions,PeekMut, theTrustedLenimplementations of its sorted iterators, and the safe methods built on them.Adds the challenge document and its book entry.
Tracking issue: #746
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.