You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
-**Solution:***Option field to point to the PR that solved this challenge.*
5
+
-**Tracking Issue:***Link to issue*
6
+
-**Start date:** 2025/06/01
7
+
-**End date:** 2025/12/31
8
+
-**Reward:***TBD*[^reward]
9
+
10
+
-------------------
11
+
12
+
13
+
## Goal
14
+
15
+
The goal of this challenge is to verify Rc and its related Weak implementation. Rc is the library-provided building blocks that enable 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
+
* It may be possible to use something analogous to the [can_reference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html), which we introduce, to track that a pointer indeed originates from `into_raw`.
32
+
33
+
* It is unclear how we will show that the reference count is greater than 0 when it is being decremented; the proposed `linked_list`[challenge](0005-linked-list.html) solution does not appear to check list length before performing operations either.
34
+
35
+
* 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.
36
+
37
+
### Success Criteria
38
+
39
+
All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:
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.
| Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit | alloc::rc |
114
+
115
+
This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions.
116
+
117
+
All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
118
+
119
+
*List of UBs*
120
+
121
+
Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](general-rules.md)
122
+
in addition to the ones listed above.
123
+
124
+
[^challenge_id]: The number of the challenge sorted by publication date.
125
+
[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee.
Copy file name to clipboardExpand all lines: doc/src/challenges/XXXY-arc.md
+15-80Lines changed: 15 additions & 80 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -12,42 +12,36 @@
12
12
13
13
## Goal
14
14
15
-
The goal of this challenge is to verify the Rc, Arc, and their related Weak implementations. Rc and Arc are the library-provided building blocks that enable safe multiple ownership of data through reference counting, as opposed to the usual ownership types used by Rust.
15
+
The goal of this challenge is to verify Arc and its related Weak implementation. Arc is the library-provided building blocks that enable 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
16
17
17
## Motivation
18
18
19
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
20
21
-
The verification includes verification of a number of Rc and Arc methods that encapsulate unsafety, as well as providing contracts for unsafe methods that impose safety conditions on their callers for correct use.
22
-
23
-
A key part of the Rc and Arc implementations is the Weak struct, which allows keeping a temporary reference to an Rc or Arc without creating circular references and without protecting the inner value from being dropped.
24
-
25
21
## Description
26
22
27
-
*Describe the challenge in more details.*
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.
28
26
29
27
### Assumptions
30
28
31
-
*Mention any assumption that users may make. Example, "assuming the usage of Stacked Borrows".*
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
+
* It may be possible to use something analogous to the [can_reference API](https://model-checking.github.io/kani/crates/doc/kani/mem/fn.can_dereference.html), which we introduce, to track that a pointer indeed originates from `into_raw`.
32
+
33
+
* It is unclear how we will show that the reference count is greater than 0 when it is being decremented; the proposed `linked_list`[challenge](0005-linked-list.html) solution does not appear to check list length before performing operations either.
34
+
35
+
* 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.
36
+
37
+
* 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.
32
38
33
39
### Success Criteria
34
40
35
41
All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:
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. From alloc::rc:
| Drop<T:?Sized, A:Allocator>::drop for UniqueRcUninit | alloc::rc |
122
-
123
-
And from alloc::sync:
58
+
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.
124
59
125
60
| Function | Location |
126
61
|---------|---------|
@@ -184,7 +119,7 @@ And from alloc::sync:
184
119
| Drop<T:?Sized, A:Allocator>::drop for UniqueArc | alloc::sync |
185
120
186
121
187
-
(I haven't included non-public unsafe functions here, though I do include non-public functions that contain unsafe. Is that a problem? Also, need to add the Arc variants of all these.)
122
+
This list excludes non-public unsafe functions; relevant ones should be called from public unsafe functions.
188
123
189
124
All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
0 commit comments