New challenges for Rc, Arc, and related Weak implementations

doc/src/challenges/0026-rc.md

@@ -0,0 +1,129 @@
+# Challenge 26: Verify reference-counted Cell implementation
+
+- **Status:** Open
+- **Solution:** *Option field to point to the PR that solved this challenge.*
+- **Tracking Issue:** [#382](https://github.com/model-checking/verify-rust-std/issues/382)
+- **Start date:** *2025/06/01*
+- **End date:** *2025/12/31*
+- **Reward:** *5,000 USD*
+
+-------------------
+
+
+## Goal
+
+The goal of this challenge is to verify [Rc](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) (meaning "Reference counted") and its related [Weak](https://github.com/rust-lang/rust/blob/master/library/alloc/src/rc.rs) 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.
+
+## 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 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    |
+|  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.
+
+For functions taking inputs of generic type 'T', the proofs can be limited to primitive types only. Moreover, for functions taking allocators as input, the proofs can be limited to only the allocators implemented in the standard library (Global/System).
+
+## 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.

doc/src/challenges/0027-arc.md

@@ -0,0 +1,138 @@
+# Challenge 27: Verify atomically reference-counted Cell implementation
+
+- **Status:** Open
+- **Solution:** *Option field to point to the PR that solved this challenge.*
+- **Tracking Issue:** [#383](https://github.com/model-checking/verify-rust-std/issues/383)
+- **Start date:** *2025/06/01*
+- **End date:** *2025/12/31*
+- **Reward:** *5,000 USD*
+
+-------------------
+
+
+## Goal
+
+The goal of this challenge is to verify [Arc](https://github.com/rust-lang/rust/blob/master/library/alloc/src/sync.rs) (meaning "Atomically reference counted") and its related [Weak](https://github.com/rust-lang/rust/blob/master/library/alloc/src/sync.rs) 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.
+
+### 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.
+
+For functions taking inputs of generic type 'T', the proofs can be limited to primitive types o
+nly. Moreover, for functions taking allocators as input, the proofs can be limited to only the allocators implemented in the standard library (Global/System).
+
+Note that solving this challenge will in part require proving an absence of data races from methods using atomic types (in this case Arc). This is also one of the main difficulties of [Challenge 7](0007-atomic-types.md). It's likely that a technique to do this for one challenge could be used for the other, with some adaptation.
+
+## 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.