Skip to content

Commit fac264f

Browse files
thanhnguyen-awsthanhnguyen-aws
committed
Merge branch 'memchrinvariant' of https://github.com/thanhnguyen-aws/verify-rust-std into memchrinvariant
2 parents a96b095 + b4a38b9 commit fac264f

File tree

33 files changed

+4337
-68
lines changed

33 files changed

+4337
-68
lines changed

‎.github/workflows/kani-metrics.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ defaults:
1111

1212
jobs:
1313
update-kani-metrics:
14+
if: github.repository == 'model-checking/verify-rust-std'
1415
runs-on: ubuntu-latest
1516

1617
steps:

‎.github/workflows/verifast-negative.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -30,16 +30,16 @@ jobs:
3030
- name: Install VeriFast
3131
run: |
3232
cd ~
33-
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
34-
# https://github.com/verifast/verifast/attestations/4911733
35-
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
36-
tar xf verifast-25.02-linux.tar.gz
33+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
34+
# https://github.com/verifast/verifast/attestations/8998468
35+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
36+
tar xf verifast-25.07-linux.tar.gz
3737
3838
- name: Install the Rust toolchain used by VeriFast
39-
run: rustup toolchain install nightly-2024-11-23
39+
run: rustup toolchain install nightly-2025-04-09
4040

4141
- name: Run VeriFast Verification
4242
run: |
43-
export PATH=~/verifast-25.02/bin:$PATH
43+
export PATH=~/verifast-25.07/bin:$PATH
4444
cd verifast-proofs
4545
bash check-verifast-proofs-negative.sh

‎.github/workflows/verifast.yml

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -27,17 +27,17 @@ jobs:
2727
- name: Install VeriFast
2828
run: |
2929
cd ~
30-
curl -OL https://github.com/verifast/verifast/releases/download/25.02/verifast-25.02-linux.tar.gz
31-
# https://github.com/verifast/verifast/attestations/4911733
32-
echo '5d5c87d11b3d735f44c3f0ca52aebc89e3c4d1119d98ef25188d07cb57ad65e8 verifast-25.02-linux.tar.gz' | shasum -a 256 -c
33-
tar xf verifast-25.02-linux.tar.gz
30+
curl -OL https://github.com/verifast/verifast/releases/download/25.07/verifast-25.07-linux.tar.gz
31+
# https://github.com/verifast/verifast/attestations/8998468
32+
echo '48d2c53b4a6e4ba6bf03bd6303dbd92a02bfb896253c06266b29739c78bad23b verifast-25.07-linux.tar.gz' | shasum -a 256 -c
33+
tar xf verifast-25.07-linux.tar.gz
3434
3535
- name: Install the Rust toolchain used by VeriFast
36-
run: rustup toolchain install nightly-2024-11-23
36+
run: rustup toolchain install nightly-2025-04-09
3737

3838
- name: Run VeriFast Verification
3939
run: |
40-
export PATH=~/verifast-25.02/bin:$PATH
40+
export PATH=~/verifast-25.07/bin:$PATH
4141
cd verifast-proofs
4242
bash check-verifast-proofs.sh
4343

‎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/0019-rawvec.md

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
1-
# Challenge 25: Verify the safety of `RawVec` functions
1+
# Challenge 19: Verify the safety of `RawVec` functions
22

3-
- **Status:** Open
3+
- **Status:** Resolved
44
- **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
55
- **Start date:** *2025-03-07*
6-
- **End date:** *2025-10-17*
6+
- **End date:** *2025-08-12*
77
- **Reward:** *10000 USD*
8+
- **Contributors:** [Bart Jacobs](https://github.com/btj)
89

910
-------------------
1011

‎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)