[Kieran-Hulsman]

Proposes a challenge to verify the safety of BinaryHeap: the Hole and sift functions, PeekMut, the TrustedLen implementations 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.

[feliperodri]

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:

1. Renumber if #595 merges first (file name, title, SUMMARY.md).
2. Add "Invoking undefined behavior via compiler intrinsics" to the UB list.
3. Say whether the proofs must cover an Ord that panics (unwinding through Hole::drop), or that this is out of scope.

[feliperodri]

Thanks, all four points are addressed: the intrinsics item is in the UB list, panicking Ord is explicitly out of scope, the other IntoIter unsafe impls are explicitly excluded, and the Description and Assumptions sections match the template. I re-checked the new text against binary_heap/mod.rs on main and it matches the code.

Approving. The one thing left is the number: #595 also uses 31, so whichever merges second takes the next free number (file name, title and SUMMARY.md), as you said you'd do.

[feliperodri]

@DiuDiu777 could you help us with a review on this challenge proposal as well?