New challenges for Rc, Arc, and related Weak implementations #367
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,130 @@ | ||
| # Challenge XXXX[^challenge_id]: Verify reference-counted Cell implementation | ||
|
|
||
| - **Status:** Open | ||
| - **Solution:** *Option field to point to the PR that solved this challenge.* | ||
| - **Tracking Issue:** *Link to issue* | ||
| - **Start date:** 2025/06/01 | ||
| - **End date:** 2025/12/31 | ||
| - **Reward:** *TBD*[^reward] | ||
|
There was a problem hiding this comment. Actually, please do propose a reward - it will still be reviewed the by reward committee and they may propose changes, but they do want an initial proposal. Thank you! |
||
|
|
||
| ------------------- | ||
|
|
||
|
|
||
| ## Goal | ||
|
|
||
| The goal of this challenge is to verify Rc and its related Weak implementation. Rc is the library-provided building block that enables safe multiple ownership of data through reference counting for single-threaded cases, as opposed to the usual ownership types used by Rust. A related challenge verifies the Arc implementation, which is atomic multi-threaded. | ||
|
There was a problem hiding this comment. Please include source-code pointers as |
||
|
|
||
| ## Motivation | ||
|
|
||
| The Rc (for single-threaded code) and Arc (atomic multi-threaded) cell types are widely used in Rust programs to enable shared ownership of data through reference counting. Since shared ownership is generally not permitted by Rust's type system, these implementations use unsafe code to bypass Rust's usual compile-time checks. Verifying the Rust standard library thus fundamentally requires verification of these types. | ||
|
There was a problem hiding this comment. In terms of reading it is a bit awkward that only the second paragraph explains what |
||
|
|
||
| ## Description | ||
|
|
||
| This challenge verifies a number of Rc methods that encapsulate unsafety, as well as providing contracts for unsafe methods that impose safety conditions on their callers for correct use. | ||
|
|
||
| A key part of the Rc implementation is the Weak struct, which allows keeping a temporary reference to an Rc without creating circular references and without protecting the inner value from being dropped. | ||
|
|
||
| ### Assumptions | ||
|
|
||
| Some properties needed for safety are beyond the ability of the Rust type system to express. This is true for all challenges, but we point out some of the properties that are relevant for this challenge. | ||
|
|
||
| * It may be possible to use a new construct analogous to the [can_dereference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html). Our new construct would track that a pointer indeed originates from `into_raw`. | ||
|
|
||
| * It is unclear how to show the reference count is greater than 0 when it is being decremented; the proposed `linked_list` [challenge](0005-linked-list.md) solution does not appear to check list length before performing operations either. | ||
|
|
||
| * Showing that something is initialized, as required by `assume_init`, appears to be beyond the current state of the art for type systems, so it may be impossible to express the full safety property required there. | ||
|
|
||
| ### Success Criteria | ||
|
|
||
| All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified: | ||
|
|
||
| | Function | Location | | ||
| |---------|---------| | ||
| | Rc<mem::MaybeUninit<T>,A>::assume_init | alloc::rc | | ||
|
There was a problem hiding this comment. Can you please include guidance in the challenge on what level of completeness you expect with regard to generics? |
||
| | Rc<[mem::MaybeUninit<T>],A>::assume_init | alloc::rc | | ||
| | Rc<T:?Sized>::from_raw | alloc::rc | | ||
| | Rc<T:?Sized>::increment_strong_count | alloc::rc | | ||
| | Rc<T:?Sized>::decrement_strong_count | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::from_raw_in | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::increment_strong_count_in | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::decrement_strong_count_in | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::get_mut_unchecked | alloc::rc | | ||
| | Rc<dyn Any,A:Allocator>::downcast_unchecked | alloc::rc | | ||
| | Weak<T:?Sized>::from_raw | alloc::rc | | ||
| | Weak<T:?Sized,A:Allocator>::from_raw_in | alloc::rc | | ||
|
|
||
| These (not necessarily public) functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added. | ||
|
|
||
| | Function | Location | | ||
| |---------|---------| | ||
| | Rc<T:?Sized, A:Allocator>::inner | alloc::rc | | ||
| | Rc<T:?Sized, A:Allocator>::into_inner_with_allocator | alloc::rc | | ||
| | Rc<T>::new | alloc::rc | | ||
| | Rc<T>::new_uninit | alloc::rc | | ||
| | Rc<T>::new_zeroed | alloc::rc | | ||
| | Rc<T>::try_new | alloc::rc | | ||
| | Rc<T>::try_new_uninit | alloc::rc | | ||
| | Rc<T>::try_new_zeroed | alloc::rc | | ||
| | Rc<T>::pin | alloc::rc | | ||
| | Rc<T,A:Allocator>::new_uninit_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::new_zeroed_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::new_cyclic_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::try_new_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::try_new_uninit_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::try_new_zeroed_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::pin_in | alloc::rc | | ||
| | Rc<T,A:Allocator>::try_unwrap | alloc::rc | | ||
| | Rc<[T]>::new_uninit_slice | alloc::rc | | ||
| | Rc<[T]>::new_zeroed_slice | alloc::rc | | ||
| | Rc<[T]>::into_array | alloc::rc | | ||
| | Rc<[T],A:Allocator>::new_uninit_slice_in | alloc::rc | | ||
| | Rc<[T],A:Allocator>::new_zeroed_slice_in | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::as_ptr | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::get_mut | alloc::rc | | ||
| | Rc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut | alloc::rc | | ||
| | Rc<dyn Any,A:Allocator>::downcast | alloc::rc | | ||
| | Rc<T:?Sized,A:Allocator>::from_box_in | alloc::rc | | ||
| | RcFromSlice<T: Clone>::from_slice | alloc::rc | | ||
| | RcFromSlice<T: Copy>::from_slice | alloc::rc | | ||
| | Drop<T: ?Sized, A:Allocator>::drop for Rc | alloc::rc | | ||
| | Clone<T: ?Sized, A:Allocator>::clone for Rc | alloc::rc | | ||
| | Default<T:Default>::default | alloc::rc | | ||
| | Default<str>::default | alloc::rc | | ||
| | From<&Str>::from | alloc::rc | | ||
| | From<Vec<T,A:Allocator>>::from | alloc::rc | | ||
| | From<Rc<str>>::from | alloc::rc | | ||
| | TryFrom<Rc[T],A:Allocator>::try_from | alloc::rc | | ||
| | ToRcSlice<T, I>::to_rc_slice | alloc::rc | | ||
| | Weak<T:?Sized,A:Allocator>::as_ptr | alloc::rc | | ||
| | Weak<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::rc | | ||
| | Weak<T:?Sized,A:Allocator>::upgrade | alloc::rc | | ||
| | Weak<T:?Sized,A:Allocator>::inner | alloc::rc | | ||
| | Drop<T:?Sized, A:Allocator>::drop for Weak | alloc::rc | | ||
| | RcInnerPtr::inc_strong | alloc::rc | | ||
| | RcInnerPtr::inc_weak | alloc::rc | | ||
| | UniqueRc<T:?Sized,A:Allocator>::into_rc | alloc::rc | | ||
| | UniqueRc<T:?Sized,A:Allocator+Clone>::downgrade | alloc::rc | | ||
| | Deref<T:?Sized,A:Allocator>::deref | alloc::rc | | ||
| | DerefMut<T:?Sized,A:Allocator>::deref_mut | alloc::rc | | ||
| | Drop<T:?Sized, A:Allocator>::drop for UniqueRc | alloc::rc | | ||
| | UniqueRcUninit<T:?Sized, A:Allocator>::new | alloc::rc | | ||
| | UniqueRcUninit<T:?Sized, A:Allocator>::data_ptr | alloc::rc | | ||
| | Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit | alloc::rc | | ||
|
|
||
| This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions. | ||
|
|
||
| ## List of UBs | ||
|
|
||
| In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](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. | ||
| * Invoking undefined behavior via compiler intrinsics. | ||
| * Mutating immutable bytes. | ||
| * Producing an invalid value. | ||
|
|
||
| Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) | ||
| in addition to the ones listed above. | ||
|
|
||
| [^challenge_id]: The number of the challenge sorted by publication date. | ||
| [^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,138 @@ | ||
| # Challenge XXXY[^challenge_id]: Verify atomically reference-counted Cell implementation | ||
|
There was a problem hiding this comment. Do you forsee any overlap/interaction with Challenge 7 (Safety of Methods for Atomic Types and |
||
|
|
||
| - **Status:** Open | ||
| - **Solution:** *Option field to point to the PR that solved this challenge.* | ||
| - **Tracking Issue:** *Link to issue* | ||
| - **Start date:** 2025/06/01 | ||
| - **End date:** 2025/12/31 | ||
| - **Reward:** *TBD*[^reward] | ||
|
|
||
| ------------------- | ||
|
|
||
|
|
||
| ## Goal | ||
|
|
||
| The goal of this challenge is to verify Arc and its related Weak implementation. Arc is the library-provided building block that enables safe multiple ownership of data through reference counting for multi-threaded code, as opposed to the usual ownership types used by Rust. The Rc implementation is the subject of a related challenge. | ||
|
|
||
| ## Motivation | ||
|
|
||
| The Rc (for single-threaded code) and Arc (atomic multi-threaded) cell types are widely used in Rust programs to enable shared ownership of data through reference counting. Since shared ownership is generally not permitted by Rust's type system, these implementations use unsafe code to bypass Rust's usual compile-time checks. Verifying the Rust standard library thus fundamentally requires verification of these types. | ||
|
|
||
| ## Description | ||
|
|
||
| This challenge verifies a number of Arc methods that encapsulate unsafety, as well as providing contracts for unsafe methods that impose safety conditions on their callers for correct use. | ||
|
|
||
| A key part of the Arc implementation is the Weak struct, which allows keeping a temporary reference to an Arc without creating circular references and without protecting the inner value from being dropped. | ||
|
|
||
| ### Assumptions | ||
|
|
||
| Some properties needed for safety are beyond the ability of the Rust type system to express. This is true for all challenges, but we point out some of the properties that are relevant for this challenge. | ||
|
|
||
| * It may be possible to use a new construct analogous to the [can_dereference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html). Our new construct would track that a pointer indeed originates from `into_raw`. | ||
|
|
||
| * It is unclear how to show that the reference count is greater than 0 when it is being decremented; the proposed `linked_list` [challenge](0005-linked-list.md) solution does not appear to check list length before performing operations either. | ||
|
|
||
| * Showing that something is initialized, as required by `assume_init`, appears to be beyond the current state of the art for type systems, so it may be impossible to express the full safety property required there. | ||
|
|
||
| * In general, Kani does not support verifying concurrent code, but it may still be possible to verify the memory-related safety properties here, assuming that the atomicity declarations are sufficient. | ||
|
There was a problem hiding this comment. The challenges should not prescribe a particular verification tool, so I don't think you should consider Kani's limitations a constraint. |
||
|
|
||
| ### Success Criteria | ||
|
|
||
| All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified: | ||
|
|
||
| | Function | Location | | ||
| |---------|---------| | ||
| | Arc<mem::MaybeUninit<T>,A>::assume_init | alloc::sync | | ||
| | Arc<[mem::MaybeUninit<T>],A>::assume_init | alloc::sync | | ||
| | Arc<T:?Sized>::from_raw | alloc::sync | | ||
| | Arc<T:?Sized>::increment_strong_count | alloc::sync | | ||
| | Arc<T:?Sized>::decrement_strong_count | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::from_raw_in | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::increment_strong_count_in | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::decrement_strong_count_in | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::get_mut_unchecked | alloc::sync | | ||
| | Arc<dyn Any+Send+Sync,A:Allocator>::downcast_unchecked | alloc::sync | | ||
| | Weak<T:?Sized>::from_raw | alloc::sync | | ||
| | Weak<T:?Sized,A:Allocator>::from_raw_in | alloc::sync | | ||
|
|
||
| These (not necessarily public) functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added. | ||
|
|
||
| | Function | Location | | ||
| |---------|---------| | ||
| | Arc<T:?Sized, A:Allocator>::into_inner_with_allocator | alloc::sync | | ||
| | Arc<T>::new | alloc::sync | | ||
| | Arc<T>::new_uninit | alloc::sync | | ||
| | Arc<T>::new_zeroed | alloc::sync | | ||
| | Arc<T>::pin | alloc::sync | | ||
| | Arc<T>::try_pin | alloc::sync | | ||
| | Arc<T>::try_new | alloc::sync | | ||
| | Arc<T>::try_new_uninit | alloc::sync | | ||
| | Arc<T>::try_new_zeroed | alloc::sync | | ||
| | Arc<T,A:Allocator>::new_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::new_uninit_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::new_zeroed_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::new_cyclic_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::pin_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::try_pin_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::try_new_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::try_new_uninit_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::try_new_zeroed_in | alloc::sync | | ||
| | Arc<T,A:Allocator>::try_unwrap | alloc::sync | | ||
| | Arc<T,A:Allocator>::into_inner | alloc::sync | | ||
| | Arc<[T]>::new_uninit_slice | alloc::sync | | ||
| | Arc<[T]>::new_zeroed_slice | alloc::sync | | ||
| | Arc<[T]>::into_array | alloc::sync | | ||
| | Arc<[T],A:Allocator>::new_uninit_slice_in | alloc::sync | | ||
| | Arc<[T],A:Allocator>::new_zeroed_slice_in | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::as_ptr | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::inner | alloc::sync | | ||
| | Arc<T:?Sized,A:Allocator>::from_box_in | alloc::sync | | ||
| | ArcFromSlice<T: Clone>::from_slice | alloc::sync | | ||
| | ArcFromSlice<T: Copy>::from_slice | alloc::sync | | ||
| | Clone<T: ?Sized, A:Allocator>::clone for Arc | alloc::sync | | ||
| | Arc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut | alloc::sync | | ||
| | Arc<T:?Sized, A:Allocator>::get_mut | alloc::sync | | ||
| | Drop<T: ?Sized, A:Allocator>::drop for Arc | alloc::sync | | ||
| | Arc<dyn Any+Send+Sync,A:Allocator>::downcast | alloc::sync | | ||
| | Weak<T:?Sized,A:Allocator>::as_ptr | alloc::sync | | ||
| | Weak<T:?Sized,A:Allocator>::into_raw_with_allocator | alloc::sync | | ||
| | Weak<T:?Sized,A:Allocator>::upgrade | alloc::sync | | ||
| | Weak<T:?Sized,A:Allocator>::inner | alloc::sync | | ||
| | Drop<T:?Sized, A:Allocator>::drop for Weak | alloc::sync | | ||
| | Default<T:Default>::default | alloc::sync | | ||
| | Default<str>::default | alloc::sync | | ||
| | Default<core::ffi::CStr>::default | alloc::sync | | ||
| | Default<[T]>::default | alloc::sync | | ||
| | From<&Str>::from | alloc::sync | | ||
| | From<Vec<T,A:Allocator+Clone>>::from | alloc::sync | | ||
| | From<Arc<str>>::from | alloc::sync | | ||
| | TryFrom<Arc[T],A:Allocator>::try_from | alloc::sync | | ||
| | ToArcSlice<T, I>::to_arc_slice | alloc::sync | | ||
| | UniqueArcUninit<T:?Sized, A:Allocator>::new | alloc::sync | | ||
| | UniqueArcUninit<T:?Sized, A:Allocator>::data_ptr | alloc::sync | | ||
| | Drop<T:?Sized, A:Allocator>::drop for UniqueArcUninit | alloc::sync | | ||
| | UniqueArc<T:?Sized,A:Allocator>::into_arc | alloc::sync | | ||
| | UniqueArc<T:?Sized,A:Allocator+Clone>::downgrade | alloc::sync | | ||
| | Deref<T:?Sized,A:Allocator>::deref | alloc::sync | | ||
| | DerefMut<T:?Sized,A:Allocator>::deref_mut | alloc::sync | | ||
| | Drop<T:?Sized, A:Allocator>::drop for UniqueArc | alloc::sync | | ||
|
|
||
|
|
||
| This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions. | ||
|
|
||
| ## List of UBs | ||
|
|
||
| In addition to any properties called out as SAFETY comments in the source code, all proofs must automatically ensure the absence of the following [undefined behaviors](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): | ||
|
|
||
| * Data races. | ||
| * Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. | ||
| * Invoking undefined behavior via compiler intrinsics. | ||
| * Mutating immutable bytes. | ||
| * Producing an invalid value. | ||
|
|
||
| Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md) | ||
| in addition to the ones listed above. | ||
|
|
||
| [^challenge_id]: The number of the challenge sorted by publication date. | ||
| [^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee. | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We knowingly have a chicken&egg problem here; please create an issue now, put its link in here, and eventually update the issue once this PR is merged.