Skip to content

Commit cd5e611

Browse files
AlexLB99patricklam
AlexLB99
and
patricklam
authored
New challenges for Rc, Arc, and related Weak implementations (#367)
This PR proposes two new challenges, namely: - A challenge for Rc and its related Weak implementation - A challenge for Arc and its related Weak implementation Any feedback is greatly appreciated! By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Patrick Lam <[email protected]>
1 parent 9e522b6 commit cd5e611

File tree

3 files changed

+265
-0
lines changed

3 files changed

+265
-0
lines changed

‎doc/src/SUMMARY.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,3 +40,5 @@
4040
- [23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md)
4141
- [24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md)
4242
- [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md)
43+
- [26: Verify reference-counted Cell implementation](./challenges/0026-rc.md)
44+
- [27: Verify atomically reference-counted Cell implementation](./challenges/0027-arc.md)

‎doc/src/challenges/0026-rc.md

Lines changed: 127 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,127 @@
1+
# Challenge 26: Verify reference-counted Cell implementation
2+
3+
- **Status:** Open
4+
- **Solution:** *Option field to point to the PR that solved this challenge.*
5+
- **Tracking Issue:** [#382](https://github.com/model-checking/verify-rust-std/issues/382)
6+
- **Start date:** *2025/06/01*
7+
- **End date:** *2025/12/31*
8+
- **Reward:** *10,000 USD*
9+
10+
-------------------
11+
12+
13+
## Goal
14+
15+
The goal of this challenge is to verify [Rc](https://doc.rust-lang.org/std/rc/struct.Rc.html) (meaning "Reference counted") and its related [Weak](https://doc.rust-lang.org/std/rc/struct.Weak.html) 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.
16+
17+
## Motivation
18+
19+
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.
20+
21+
## Description
22+
23+
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.
24+
25+
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.
26+
27+
### Assumptions
28+
29+
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.
30+
31+
* You are not required to check that the reference count is greater than 0 when it is being decremented.
32+
33+
* 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.
34+
35+
### Success Criteria
36+
37+
All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:
38+
39+
| Function | Location |
40+
|---------|---------|
41+
| `Rc<mem::MaybeUninit<T>,A>::assume_init` | `alloc::rc` |
42+
| `Rc<[mem::MaybeUninit<T>],A>::assume_init` | `alloc::rc` |
43+
| `Rc<T:?Sized>::from_raw` | `alloc::rc` |
44+
| `Rc<T:?Sized>::increment_strong_count` | `alloc::rc` |
45+
| `Rc<T:?Sized>::decrement_strong_count` | `alloc::rc` |
46+
| `Rc<T:?Sized,A:Allocator>::from_raw_in` | `alloc::rc` |
47+
| `Rc<T:?Sized,A:Allocator>::increment_strong_count_in` | `alloc::rc` |
48+
| `Rc<T:?Sized,A:Allocator>::decrement_strong_count_in` | `alloc::rc` |
49+
| `Rc<T:?Sized,A:Allocator>::get_mut_unchecked` | `alloc::rc` |
50+
| `Rc<dyn Any,A:Allocator>::downcast_unchecked` | `alloc::rc` |
51+
| `Weak<T:?Sized>::from_raw` | `alloc::rc` |
52+
| `Weak<T:?Sized,A:Allocator>::from_raw_in` | `alloc::rc` |
53+
54+
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.
55+
56+
| Function | Location |
57+
|---------|---------|
58+
| `Rc<T:?Sized, A:Allocator>::inner` | `alloc::rc` |
59+
| `Rc<T:?Sized, A:Allocator>::into_inner_with_allocator` | `alloc::rc` |
60+
| `Rc<T>::new` | `alloc::rc` |
61+
| `Rc<T>::new_uninit` | `alloc::rc` |
62+
| `Rc<T>::new_zeroed` | `alloc::rc` |
63+
| `Rc<T>::try_new` | `alloc::rc` |
64+
| `Rc<T>::try_new_uninit` | `alloc::rc` |
65+
| `Rc<T>::try_new_zeroed` | `alloc::rc` |
66+
| `Rc<T>::pin` | `alloc::rc` |
67+
| `Rc<T,A:Allocator>::new_uninit_in` | `alloc::rc` |
68+
| `Rc<T,A:Allocator>::new_zeroed_in` | `alloc::rc` |
69+
| `Rc<T,A:Allocator>::new_cyclic_in` | `alloc::rc` |
70+
| `Rc<T,A:Allocator>::try_new_in` | `alloc::rc` |
71+
| `Rc<T,A:Allocator>::try_new_uninit_in` | `alloc::rc` |
72+
| `Rc<T,A:Allocator>::try_new_zeroed_in` | `alloc::rc` |
73+
| `Rc<T,A:Allocator>::pin_in` | `alloc::rc` |
74+
| `Rc<T,A:Allocator>::try_unwrap` | `alloc::rc` |
75+
| `Rc<[T]>::new_uninit_slice` | `alloc::rc` |
76+
| `Rc<[T]>::new_zeroed_slice` | `alloc::rc` |
77+
| `Rc<[T]>::into_array` | `alloc::rc` |
78+
| `Rc<[T],A:Allocator>::new_uninit_slice_in` | `alloc::rc` |
79+
| `Rc<[T],A:Allocator>::new_zeroed_slice_in` | `alloc::rc` |
80+
| `Rc<T:?Sized,A:Allocator>::into_raw_with_allocator` | `alloc::rc` |
81+
| `Rc<T:?Sized,A:Allocator>::as_ptr` | `alloc::rc` |
82+
| `Rc<T:?Sized,A:Allocator>::get_mut` | `alloc::rc` |
83+
| `Rc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut` | `alloc::rc` |
84+
| `Rc<dyn Any,A:Allocator>::downcast` | `alloc::rc` |
85+
| `Rc<T:?Sized,A:Allocator>::from_box_in` | `alloc::rc` |
86+
| `RcFromSlice<T: Clone>::from_slice` | `alloc::rc` |
87+
| `RcFromSlice<T: Copy>::from_slice` | `alloc::rc` |
88+
| `Drop<T: ?Sized, A:Allocator>::drop for Rc` | `alloc::rc` |
89+
| `Clone<T: ?Sized, A:Allocator>::clone for Rc` | `alloc::rc` |
90+
| `Default<T:Default>::default` | `alloc::rc` |
91+
| `Default<str>::default` | `alloc::rc` |
92+
| `From<&Str>::from` | `alloc::rc` |
93+
| `From<Vec<T,A:Allocator>>::from` | `alloc::rc` |
94+
| `From<Rc<str>>::from` | `alloc::rc` |
95+
| `TryFrom<Rc[T],A:Allocator>::try_from` | `alloc::rc` |
96+
| `ToRcSlice<T, I>::to_rc_slice` | `alloc::rc` |
97+
| `Weak<T:?Sized,A:Allocator>::as_ptr` | `alloc::rc` |
98+
| `Weak<T:?Sized,A:Allocator>::into_raw_with_allocator` | `alloc::rc` |
99+
| `Weak<T:?Sized,A:Allocator>::upgrade` | `alloc::rc` |
100+
| `Weak<T:?Sized,A:Allocator>::inner` | `alloc::rc` |
101+
| `Drop<T:?Sized, A:Allocator>::drop for Weak` | `alloc::rc` |
102+
| `RcInnerPtr::inc_strong` | `alloc::rc` |
103+
| `RcInnerPtr::inc_weak` | `alloc::rc` |
104+
| `UniqueRc<T:?Sized,A:Allocator>::into_rc` | `alloc::rc` |
105+
| `UniqueRc<T:?Sized,A:Allocator+Clone>::downgrade` | `alloc::rc` |
106+
| `Deref<T:?Sized,A:Allocator>::deref` | `alloc::rc` |
107+
| `DerefMut<T:?Sized,A:Allocator>::deref_mut` | `alloc::rc` |
108+
| `Drop<T:?Sized, A:Allocator>::drop for UniqueRc` | `alloc::rc` |
109+
| `UniqueRcUninit<T:?Sized, A:Allocator>::new` | `alloc::rc` |
110+
| `UniqueRcUninit<T:?Sized, A:Allocator>::data_ptr` | `alloc::rc` |
111+
| `Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit` | `alloc::rc` |
112+
113+
This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions.
114+
115+
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).
116+
117+
## List of UBs
118+
119+
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):
120+
121+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
122+
* Invoking undefined behavior via compiler intrinsics.
123+
* Mutating immutable bytes.
124+
* Producing an invalid value.
125+
126+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
127+
in addition to the ones listed above.

‎doc/src/challenges/0027-arc.md

Lines changed: 136 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,136 @@
1+
# Challenge 27: Verify atomically reference-counted Cell implementation
2+
3+
- **Status:** Open
4+
- **Solution:** *Option field to point to the PR that solved this challenge.*
5+
- **Tracking Issue:** [#383](https://github.com/model-checking/verify-rust-std/issues/383)
6+
- **Start date:** *2025/06/01*
7+
- **End date:** *2025/12/31*
8+
- **Reward:** *10,000 USD*
9+
10+
-------------------
11+
12+
13+
## Goal
14+
15+
The goal of this challenge is to verify [Arc](https://doc.rust-lang.org/std/sync/struct.Arc.html) (meaning "Atomically reference counted") and its related [Weak](https://doc.rust-lang.org/std/sync/struct.Weak.html) 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.
16+
17+
## Motivation
18+
19+
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.
20+
21+
## Description
22+
23+
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.
24+
25+
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.
26+
27+
### Assumptions
28+
29+
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.
30+
31+
* You are not required to check that the reference count is greater than 0 when it is being decremented.
32+
33+
* 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.
34+
35+
### Success Criteria
36+
37+
All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:
38+
39+
| Function | Location |
40+
|---------|---------|
41+
| `Arc<mem::MaybeUninit<T>,A>::assume_init` | `alloc::sync` |
42+
| `Arc<[mem::MaybeUninit<T>],A>::assume_init` | `alloc::sync` |
43+
| `Arc<T:?Sized>::from_raw` | `alloc::sync` |
44+
| `Arc<T:?Sized>::increment_strong_count` | `alloc::sync` |
45+
| `Arc<T:?Sized>::decrement_strong_count` | `alloc::sync` |
46+
| `Arc<T:?Sized,A:Allocator>::from_raw_in` | `alloc::sync` |
47+
| `Arc<T:?Sized,A:Allocator>::increment_strong_cobunt_in` | `alloc::sync` |
48+
| `Arc<T:?Sized,A:Allocator>::decrement_strong_count_in` | `alloc::sync` |
49+
| `Arc<T:?Sized,A:Allocator>::get_mut_unchecked` | `alloc::sync` |
50+
| `Arc<dyn Any+Send+Sync,A:Allocator>::downcast_unchecked` | `alloc::sync` |
51+
| `Weak<T:?Sized>::from_raw` | `alloc::sync` |
52+
| `Weak<T:?Sized,A:Allocator>::from_raw_in` | `alloc::sync` |
53+
54+
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.
55+
56+
| Function | Location |
57+
|---------|---------|
58+
| `Arc<T:?Sized, A:Allocator>::into_inner_with_allocator | alloc::sync |
59+
| `Arc<T>::new` | `alloc::sync` |
60+
| `Arc<T>::new_uninit` | `alloc::sync` |
61+
| `Arc<T>::new_zeroed` | `alloc::sync` |
62+
| `Arc<T>::pin` | `alloc::sync` |
63+
| `Arc<T>::try_pin` | `alloc::sync` |
64+
| `Arc<T>::try_new` | `alloc::sync` |
65+
| `Arc<T>::try_new_uninit` | `alloc::sync` |
66+
| `Arc<T>::try_new_zeroed` | `alloc::sync` |
67+
| `Arc<T,A:Allocator>::new_in` | `alloc::sync` |
68+
| `Arc<T,A:Allocator>::new_uninit_in` | `alloc::sync` |
69+
| `Arc<T,A:Allocator>::new_zeroed_in` | `alloc::sync` |
70+
| `Arc<T,A:Allocator>::new_cyclic_in` | `alloc::sync` |
71+
| `Arc<T,A:Allocator>::pin_in` | `alloc::sync` |
72+
| `Arc<T,A:Allocator>::try_pin_in` | `alloc::sync` |
73+
| `Arc<T,A:Allocator>::try_new_in` | `alloc::sync` |
74+
| `Arc<T,A:Allocator>::try_new_uninit_in` | `alloc::sync` |
75+
| `Arc<T,A:Allocator>::try_new_zeroed_in` | `alloc::sync` |
76+
| `Arc<T,A:Allocator>::try_unwrap]` | `alloc::sync` |
77+
| `Arc<T,A:Allocator>::into_inner` | `alloc::sync` |
78+
| `Arc<[T]>::new_uninit_slice` | `alloc::sync` |
79+
| `Arc<[T]>::new_zeroed_slice` | `alloc::sync` |
80+
| `Arc<[T]>::into_array` | `alloc::sync` |
81+
| `Arc<[T],A:Allocator>::new_uninit_slice_in` | `alloc::sync` |
82+
| `Arc<[T],A:Allocator>::new_zeroed_slice_in` | `alloc::sync` |
83+
| `Arc<T:?Sized,A:Allocator>::into_raw_with_allocator` | `alloc::sync` |
84+
| `Arc<T:?Sized,A:Allocator>::as_ptr` | `alloc::sync` |
85+
| `Arc<T:?Sized,A:Allocator>::inner` | `alloc::sync` |
86+
| `Arc<T:?Sized,A:Allocator>::from_box_in` | `alloc::sync` |
87+
| `ArcFromSlice<T: Clone>::from_slice` | `alloc::sync` |
88+
| `ArcFromSlice<T: Copy>::from_slice` | `alloc::sync` |
89+
| `Clone<T: ?Sized, A:Allocator>::clone for Arc` | `alloc::sync` |
90+
| `Arc<T:?Sized+CloneToUninit, A:Allocator+Clone>::make_mut` | `alloc::sync` |
91+
| `Arc<T:?Sized, A:Allocator>::get_mut` | `alloc::sync` |
92+
| `Drop<T: ?Sized, A:Allocator>::drop for Arc` | `alloc::sync` |
93+
| `Arc<dyn Any+Send+Sync,A:Allocator>::downcast` | `alloc::sync` |
94+
| `Weak<T:?Sized,A:Allocator>::as_ptr` | `alloc::sync` |
95+
| `Weak<T:?Sized,A:Allocator>::into_raw_with_allocator` | `alloc::sync` |
96+
| `Weak<T:?Sized,A:Allocator>::upgrade` | `alloc::sync` |
97+
| `Weak<T:?Sized,A:Allocator>::inner` | `alloc::sync` |
98+
| `Drop<T:?Sized, A:Allocator>::drop for Weak` | `alloc::sync` |
99+
| `Default<T:Default>::default` | `alloc::sync` |
100+
| `Default<str>::default` | `alloc::sync` |
101+
| `Default<core::ffi::CStr>::default` | `alloc::sync` |
102+
| `Default<[T]>::default` | `alloc::sync` |
103+
| `From<&Str>::from` | `alloc::sync` |
104+
| `From<Vec<T,A:Allocator+Clone>>::from` | `alloc::sync` |
105+
| `From<Arc<str>>::from` | `alloc::sync` |
106+
| `TryFrom<Arc[T],A:Allocator>::try_from` | `alloc::sync` |
107+
| `ToArcSlice<T, I>::to_arc_slice` | `alloc::sync` |
108+
| `UniqueArcUninit<T:?Sized, A:Allocator>::new]` | `alloc::sync` |
109+
| `UniqueArcUninit<T:?Sized, A:Allocator>::data_ptr` | `alloc::sync` |
110+
| `Drop<T:?Sized, A:Allocator>::drop for UniqueArcUninit` | `alloc::sync` |
111+
| `UniqueArc<T:?Sized,A:Allocator>::into_arc` | `alloc::sync` |
112+
| `UniqueArc<T:?Sized,A:Allocator+Clone>::downgrade` | `alloc::sync` |
113+
| `Deref<T:?Sized,A:Allocator>::deref` | `alloc::sync` |
114+
| `DerefMut<T:?Sized,A:Allocator>::deref_mut` | `alloc::sync` |
115+
| `Drop<T:?Sized, A:Allocator>::drop for UniqueArc` | `alloc::sync` |
116+
117+
118+
This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions.
119+
120+
For functions taking inputs of generic type 'T', the proofs can be limited to primitive types o
121+
nly. Moreover, for functions taking allocators as input, the proofs can be limited to only the allocators implemented in the standard library (Global/System).
122+
123+
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.
124+
125+
## List of UBs
126+
127+
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):
128+
129+
* Data races.
130+
* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
131+
* Invoking undefined behavior via compiler intrinsics.
132+
* Mutating immutable bytes.
133+
* Producing an invalid value.
134+
135+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
136+
in addition to the ones listed above.

0 commit comments

Comments
 (0)