Skip to content

Commit e2db435

Browse files
Add reward information to the repository and challenges (#176)
I also postponed the end date of all challenges, and fixed the date format. Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>
1 parent 406b1c1 commit e2db435

16 files changed

+64
-41
lines changed

README.md

Lines changed: 9 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -7,24 +7,23 @@
77
This repository is a fork of the official Rust programming
88
language repository, created solely to verify the Rust standard
99
library. It should not be used as an alternative to the official
10-
Rust releases. The repository is tool agnostic and welcomes the addition of
10+
Rust releases. The repository is tool agnostic and welcomes the addition of
1111
new tools.
1212

1313
The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
1414
1. Contributing to the core mechanism of verifying the rust standard library
1515
2. Creating new techniques to perform scalable verification
1616
3. Apply techniques to verify previously unverified parts of the standard library.
1717

18-
## [Kani](https://github.com/model-checking/kani)
18+
For that we are launching a contest that includes a series of challenges that focus on verifying
19+
memory safety and a subset of undefined behaviors in the Rust standard library.
20+
Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
21+
successful completion.
1922

20-
The Kani Rust Verifier is a bit-precise model checker for Rust.
21-
Kani verifies:
22-
* Memory safety (e.g., null pointer dereferences)
23-
* User-specified assertions (i.e `assert!(...)`)
24-
* The absence of panics (eg., `unwrap()` on `None` values)
25-
* The absence of some types of unexpected behavior (e.g., arithmetic overflows).
23+
See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
24+
and the list of existing challenges.
2625

27-
You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani).
26+
We welcome everyone to participate!
2827

2928
## Contact
3029

@@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
4039
Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
4140
See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details.
4241

43-
## Rust
42+
### Rust
4443
Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.
4544

4645
See [the Rust repository](https://github.com/rust-lang/rust) for details.

doc/src/challenge_template.md

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,9 @@
33
- **Status:** *One of the following: \[Open | Resolved | Expired\]*
44
- **Solution:** *Option field to point to the PR that solved this challenge.*
55
- **Tracking Issue:** *Link to issue*
6-
- **Start date:** *YY/MM/DD*
7-
- **End date:** *YY/MM/DD*
6+
- **Start date:** *YYYY/MM/DD*
7+
- **End date:** *YYYY/MM/DD*
8+
- **Reward:** *TBD*[^reward]
89

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

@@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta
4950
in addition to the ones listed above.
5051

5152
[^challenge_id]: The number of the challenge sorted by publication date.
53+
[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee.

doc/src/challenges/0001-core-transmutation.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
5-
- **Start date:** 2024-06-12
6-
- **End date:** 2024-12-10
5+
- **Start date:** *2024/06/12*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

doc/src/challenges/0002-intrinsics-memory.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
5-
- **Start date:** *24/06/12*
6-
- **End date:** *24/12/10*
5+
- **Start date:** *2024/06/12*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

doc/src/challenges/0003-pointer-arithmentic.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
# Challenge 3: Verifying Raw Pointer Arithmetic Operations
22

33
- **Status:** Open
4-
- **Solution:**
54
- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
6-
- **Start date:** 24/06/24
7-
- **End date:** 24/12/10
5+
- **Start date:** *2024/06/24*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
88

99
-------------------
1010

doc/src/challenges/0004-btree-node.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
5-
- **Start date:** *2024-07-01*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/07/01*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

doc/src/challenges/0005-linked-list.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
5-
- **Start date:** *24/07/01*
6-
- **End date:** *24/12/10*
5+
- **Start date:** *2024/07/01*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *5,000 USD*
78

89
-------------------
910

doc/src/challenges/0006-nonnull.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
5-
- **Start date:** *2024-08-16*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/16*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *N/A*
78

89
-------------------
910

doc/src/challenges/0007-atomic-types.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83)
5-
- **Start date:** *2024-10-30*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/10/30*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

doc/src/challenges/0008-smallsort.md

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,9 @@
22

33
- **Status:** Open
44
- **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
5-
- **Start date:** *2024-08-17*
6-
- **End date:** *2024-12-10*
5+
- **Start date:** *2024/08/17*
6+
- **End date:** *2025/04/10*
7+
- **Reward:** *10,000 USD*
78

89
-------------------
910

0 commit comments

Comments
 (0)