Merge branch 'model-checking:main' into unchecked_mull_add

aa-luna · web-flow · commit dcbf4f5bef66 · 2024-11-24T17:29:48.000-05:00
diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml
@@ -15,5 +15,6 @@ members = [
     "carolynzech",
     "robdockins",
     "HuStmpHrrr",
-    "Eh2406"
+    "Eh2406",
+    "jswrenn"
 ]
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
@@ -65,3 +65,17 @@ jobs:
       - name: Test Kani script (In Repo Directory)
         working-directory: ${{github.workspace}}/head
         run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
+      
+      # Step 4: Run list on the std library and add output to job summary
+      - name: Run Kani List
+        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
+
+      - name: Add Kani List output to job summary
+        uses: actions/github-script@v6
+        with:
+          script: |
+            const fs = require('fs');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
+            await core.summary
+              .addRaw(kaniOutput)
+              .write();
diff --git a/README.md b/README.md
@@ -7,24 +7,23 @@
 This repository is a fork of the official Rust programming
 language repository, created solely to verify the Rust standard
 library. It should not be used as an alternative to the official
-Rust releases. The repository is tool agnostic and welcomes the addition of 
+Rust releases. The repository is tool agnostic and welcomes the addition of
 new tools.
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
-## [Kani](https://github.com/model-checking/kani)
+For that we are launching a contest that includes a series of challenges that focus on verifying
+memory safety and a subset of undefined behaviors in the Rust standard library.
+Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its
+successful completion.
 
-The Kani Rust Verifier is a bit-precise model checker for Rust.
-Kani verifies:
-* Memory safety (e.g., null pointer dereferences)
-* User-specified assertions (i.e `assert!(...)`)
-* The absence of panics (eg., `unwrap()` on `None` values)
-* The absence of some types of unexpected behavior (e.g., arithmetic overflows).
+See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules
+and the list of existing challenges.
 
-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).
+We welcome everyone to participate!
 
 ## Contact
 
@@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0).
 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.
 
-## Rust
+### Rust
 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.
 
 See [the Rust repository](https://github.com/rust-lang/rust) for details.
diff --git a/doc/src/challenge_template.md b/doc/src/challenge_template.md
@@ -3,8 +3,9 @@
 - **Status:** *One of the following: \[Open | Resolved | Expired\]*
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** *Link to issue*
-- **Start date:** *YY/MM/DD*
-- **End date:** *YY/MM/DD*
+- **Start date:** *YYYY/MM/DD*
+- **End date:** *YYYY/MM/DD*
+- **Reward:** *TBD*[^reward]
 
 -------------------
 
@@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta
 in addition to the ones listed above.
 
 [^challenge_id]: The number of the challenge sorted by publication date.
+[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee.
diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
-- **Start date:** 2024-06-12
-- **End date:** 2024-12-10
+- **Start date:** *2024/06/12*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
-- **Start date:** *24/06/12*
-- **End date:** *24/12/10*
+- **Start date:** *2024/06/12*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md
@@ -1,10 +1,10 @@
 # Challenge 3: Verifying Raw Pointer Arithmetic Operations
 
 - **Status:** Open
-- **Solution:**
 - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
-- **Start date:** 24/06/24
-- **End date:** 24/12/10
+- **Start date:** *2024/06/24*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
-- **Start date:** *2024-07-01*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/07/01*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
-- **Start date:** *24/07/01*
-- **End date:** *24/12/10*
+- **Start date:** *2024/07/01*
+- **End date:** *2025/04/10*
+- **Reward:** *5,000 USD*
 
 -------------------
 
@@ -23,7 +24,7 @@ The memory safety of the following public functions that iterating over the inte
 
 | Function | Location |
 |---------|---------|
-|clearn | alloc::collections::linked_list |
+|clear| alloc::collections::linked_list |
 |contains| alloc::collections::linked_list |
 |split_off| alloc::collections::linked_list |
 |remove| alloc::collections::linked_list |
diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
-- **Start date:** *2024-08-16*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/16*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83)
-- **Start date:** *2024-10-30*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/10/30*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
-- **Start date:** *2024-08-17*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/17*
+- **End date:** *2025/04/10*
+- **Reward:** *10,000 USD*
 
 -------------------
 
diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72)
-- **Start date:** *2024-08-20*
-- **End date:** *2024-12-20*
+- **Start date:** *2024/08/20*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
-- **Start date:** *2024-08-19*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/19*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
@@ -3,8 +3,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
-- **Start date:** *2024-08-20*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/20*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md
@@ -2,8 +2,9 @@
 
 - **Status:** Open
 - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71)
-- **Start date:** *2024-08-23*
-- **End date:** *2024-12-10*
+- **Start date:** *2024/08/23*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 
diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md
@@ -3,8 +3,9 @@
 - **Status:** Open
 - **Solution:**
 - **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150)
-- **Start date:** 2024/11/04
-- **End date:** 2025/01/31
+- **Start date:** *2024/11/04*
+- **End date:** *2025/04/10*
+- **Reward:** *N/A*
 
 -------------------
 ## Goal
diff --git a/doc/src/intro.md b/doc/src/intro.md
@@ -6,12 +6,22 @@ library](https://doc.rust-lang.org/std/). The goal of this is
 to provide automated verification that can be used to verify that a
 given Rust standard library implementation is safe.
 
+Verifying the Rust libraries is difficult because:
+1. Lack of a specification,
+2. Lack of an existing verification mechanism in the Rust ecosystem,
+3. The large size of the verification problem,
+4. The unknowns of scalable verification.
+
+Given the magnitude and scope of the effort, we believe this should be a community owned effort.
+For that, we are launching a contest that includes a series of challenges that focus on verifying
+memory safety and a subset of undefined behaviors in the Rust standard library.
+
 Efforts are largely classified in the following areas:
 
 1. Contributing to the core mechanism of verifying the rust standard library
 2. Creating new techniques to perform scalable verification
 3. Apply techniques to verify previously unverified parts of the standard library.
 
+There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion.
 
-We encourage everyone to watch this repository to be notified of any
-changes.
+We encourage everyone to watch this repository to be notified of any changes.
diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md
@@ -25,7 +25,7 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 3. \[and so on...\]
 
 ## Artifacts
-_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._
+_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
 
 ## CI & Versioning
 _Please describe how you version the tool and how it will be supported in CI pipelines._
diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh

Original file line number	Diff line number	Diff line change
`@@ -15,5 +15,6 @@ members = [`
`15`	`15`	`"carolynzech",`
`16`	`16`	`"robdockins",`
`17`	`17`	`"HuStmpHrrr",`
`18`		`- "Eh2406"`
	`18`	`+ "Eh2406",`
	`19`	`+ "jswrenn"`
`19`	`20`	`]`