Challenge 26: Verify reference-counted Cell implementation
- Status: Open
- Solution: Option field to point to the PR that solved this challenge.
- Tracking Issue: #382
- Start date: 2025/06/01
- End date: 2025/12/31
- Reward: 10,000 USD
Goal
The goal of this challenge is to verify Rc (meaning "Reference counted") 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.
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.
-
You are not required to check that the reference count is greater than 0 when it is being decremented.
-
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:
- 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 in addition to the ones listed above.