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
This commit improves the visibility of the status of the verification
effort. More specifically, it makes the tools, challenges, and proofs
easier to find by listing the currently accepted tools and the
challenges, with their reward, status, and link to the proof (once
resolved) in a table in the repo README.
@@ -8,7 +8,7 @@ This repository is a fork of the official Rust programming
8
8
language repository, created solely to verify the Rust standard
9
9
library. It should not be used as an alternative to the official
10
10
Rust releases. The repository is tool agnostic and welcomes the addition of
11
-
new tools.
11
+
new tools. The currently accepted tools are [Flux](https://model-checking.github.io/verify-rust-std/tools/flux.html), [GOTO Transcoder (ESBMC)](https://model-checking.github.io/verify-rust-std/tools/goto-transcoder.html), [Kani](https://model-checking.github.io/verify-rust-std/tools/kani.html), and [VeriFast](https://model-checking.github.io/verify-rust-std/tools/verifast.html).
12
12
13
13
The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
14
14
1. Contributing to the core mechanism of verifying the rust standard library
@@ -21,8 +21,39 @@ memory safety and a subset of undefined behaviors in the Rust standard library.
21
21
Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
22
22
successful completion.
23
23
24
-
See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
25
-
and the list of existing challenges.
24
+
These are the challenges:
25
+
26
+
| Challenge | Reward | Status | Proof |
27
+
| --------- | ------ | ------ | ----- |
28
+
|[1: Verify core transmuting methods](https://model-checking.github.io/verify-rust-std/challenges/0001-core-transmutation.html)| N/A | Open ||
29
+
|[2: Verify the memory safety of core intrinsics using raw pointers](https://model-checking.github.io/verify-rust-std/challenges/0002-intrinsics-memory.html)| N/A | Open ||
30
+
|[3: Verifying Raw Pointer Arithmetic Operations](https://model-checking.github.io/verify-rust-std/challenges/0003-pointer-arithmentic.html)| N/A |[Resolved](https://github.com/model-checking/verify-rust-std/pull/212)|[Kani](https://github.com/model-checking/verify-rust-std/pull/212/files)|
31
+
|[4: Memory safety of BTreeMap's `btree::node` module](https://model-checking.github.io/verify-rust-std/challenges/0004-btree-node.html)| 10,000 USD | Open ||
32
+
|[5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)| 5,000 USD |[Resolved](https://github.com/model-checking/verify-rust-std/pull/238)|[VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/collections/linked_list.rs)|
33
+
|[6: Safety of `NonNull`](./challenges/0006-nonnull.md)| N/A |[Resolved](https://github.com/model-checking/verify-rust-std/pull/247)|[Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/ptr/non_null.rs)|
34
+
|[7: Safety of Methods for Atomic Types & Atomic Intrinsics](./challenges/0007-atomic-types.md)| 10,000 USD | Open ||
35
+
|[8: Contracts for SmallSort](./challenges/0008-smallsort.md)| 10,000 USD | Open ||
36
+
|[9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)| N/A |[Resolved](https://github.com/model-checking/verify-rust-std/pull/136)|[Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/time.rs)|
37
+
|[10: Memory safety of String](./challenges/0010-string.md)| N/A | Open ||
38
+
|[11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)| N/A |[Resolved](https://github.com/model-checking/verify-rust-std/issues/59)|[Kani](https://github.com/model-checking/verify-rust-std/tree/main/library/core/src/num)|
39
+
|[12: Safety of `NonZero`](./challenges/0012-nonzero.md)| N/A | Open ||
40
+
|[13: Safety of `CStr`](./challenges/0013-cstr.md)| N/A | Open ||
41
+
|[14: Safety of Primitive Conversions](./challenges/0014-convert-num.md)| TBD |[Resolved](https://github.com/model-checking/verify-rust-std/pull/247)|[Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/convert/num.rs)|
42
+
|[15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)|| Open ||
43
+
|[16: Verify the safety of Iterator functions](./challenges/0016-iter.md)| 10,000 USD | Open ||
44
+
|[17: Verify the safety of slice functions](./challenges/0017-slice.md)| 10,000 USD | Open ||
45
+
|[18: Verify the safety of slice iter functions](./challenges/0018-slice-iter.md)| 10,000 USD | Open ||
46
+
|[19: Safety of `RawVec`](./challenges/0019-rawvec.md)| 10,000 USD |[Resolved](https://github.com/model-checking/verify-rust-std/pull/422)|[VeriFast](https://github.com/model-checking/verify-rust-std/tree/main/verifast-proofs/alloc/raw_vec/mod.rs)|
47
+
|[20: Verify the safety of char-related functions in str::pattern](./challenges/0020-str-pattern-pt1.md)| 25,000 USD | Open ||
48
+
|[21: Verify the safety of substring-related functions in str::pattern](./challenges/0021-str-pattern-pt2.md)| 25,000 USD | Open ||
49
+
|[22: Verify the safety of str iter functions](./challenges/0022-str-iter.md)| 10,000 USD | Open ||
50
+
|[23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md)| 15,000 USD | Open ||
51
+
|[24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md)| 15,000 USD | Open ||
52
+
|[25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md)| 10,000 USD | Open ||
53
+
|[26: Verify reference-counted Cell implementation](./challenges/0026-rc.md)| 10,000 USD | Open ||
0 commit comments