Merge remote-tracking branch 'origin/main' into layout-harnesses

.github/TOOL_REQUEST_TEMPLATE.md

@@ -0,0 +1,31 @@
+_The following form is designed to provide information for your tool that should be included in the effort to verify the Rust standard library. Please note that the tool will need to be **supported** if it is to be included._
+
+## Tool Name
+_Please enter your tool name here._
+
+## Description
+_Please enter a description for your tool and any information you deem relevant._
+
+## Tool Information
+
+* [ ] Does the tool perform Rust verification? 
+* [ ] Does the tool deal with *unsafe* Rust code? 
+* [ ] Does the tool run independently in CI? 
+* [ ] Is the tool open source?
+* [ ] Is the tool under development? 
+* [ ] Will you or your team be able to provide support for the tool?
+
+## Licenses
+_Please list the license(s) that are used by your tool, and if to your knowledge they conflict with the Rust standard library license(s)._
+
+## Steps to Use the Tool
+
+1. [First Step]
+2. [Second Step]
+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._
+
+## CI & Versioning
+_Please describe how you version the tool and how it will be supported in CI pipelines._

.github/pull_requests.toml

@@ -9,5 +9,8 @@ members = [
     "remi-delmas-3000",
     "qinheping",
     "tautschnig",
-    "jaisnan"
+    "jaisnan",
+    "patricklam",
+    "ranjitjhala",
+    "carolynzech"
 ]

.github/workflows/pr_approval.yml

@@ -7,16 +7,9 @@ name: Check PR Approvals
 on:
   pull_request_review:
     types: [submitted]
-  workflow_dispatch:
-
-# Without these permissions, we get a 403 error from github
-# for trying to modify the pull request for newer project.
-# Source: https://stackoverflow.com/a/76994510
-permissions: write-all
 
 jobs:
   check-approvals:
-    if: github.event.review.state == 'APPROVED' || github.event_name == 'workflow_dispatch'
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
@@ -51,22 +44,6 @@ jobs:
               pull_number = context.issue.number;
             }
 
-            // Get PR files
-            const files = await github.rest.pulls.listFiles({
-              owner,
-              repo,
-              pull_number
-            });
-
-            const relevantPaths = ['library/', 'doc/src/challenges/'];
-            const isRelevantPR = files.data.some(file =>
-              relevantPaths.some(path => file.filename.startsWith(path))
-            );
-
-            if (!isRelevantPR) {
-              console.log('PR does not touch relevant paths. Exiting workflow.');
-              return;
-            }
 
             // Get parsed data
             try {
@@ -117,45 +94,6 @@ jobs:
               text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
             };
 
-            // Get PR details
-            const pr = await github.rest.pulls.get({
-              owner,
-              repo,
-              pull_number
-            });
-
-            // Create or update check run
-            const checkRuns = await github.rest.checks.listForRef({
-              owner,
-              repo,
-              ref: pr.data.head.sha,
-              check_name: checkName
-            });
-
-            // Reuse the same workflow everytime there's a new review submitted
-            // instead of creating new workflows. Better efficiency and readability
-            // as the number of workflows is kept to a minimal number
-            if (checkRuns.data.total_count > 0) {
-              await github.rest.checks.update({
-                owner,
-                repo,
-                check_run_id: checkRuns.data.check_runs[0].id,
-                status: 'completed',
-                conclusion,
-                output
-              });
-            } else {
-              await github.rest.checks.create({
-                owner,
-                repo,
-                name: checkName,
-                head_sha: pr.data.head.sha,
-                status: 'completed',
-                conclusion,
-                output
-              });
-            }
-
             if (conclusion === 'failure') {
               core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
             }

README.md

@@ -7,7 +7,8 @@
 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.
+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
@@ -36,12 +37,14 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more
 ## License
 
 ### Kani
-
 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 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.
+
+## Introducing a New Tool
+
+Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.

doc/book.toml

@@ -12,6 +12,7 @@ build-dir = "../book"
 site-url = "/verify-rust-std/"
 git-repository-url = "https://github.com/model-checking/verify-rust-std"
 edit-url-template = "https://github.com/model-checking/verify-rust-std/edit/main/doc/{path}"
+no-section-label = true
 
 [output.html.playground]
 runnable = false

doc/src/SUMMARY.md

@@ -13,10 +13,16 @@
 ---
 
 - [Challenges](./challenges.md)
-  - [Core Transmutation](./challenges/0001-core-transmutation.md)
-  - [Memory safety of core intrinsics](./challenges/0002-intrinsics-memory.md)
-  - [Pointer Arithmetic](./challenges/0003-pointer-arithmentic.md)
-  - [Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
-  - [Inductive data type](./challenges/0005-linked-list.md)
-  - [Contracts for SmallSort](./challenges/0008-smallsort.md)
-  - [Memory safety of String](./challenges/0010-string.md)
+  - [1: Verify core transmuting methods](./challenges/0001-core-transmutation.md)
+  - [2: Verify the memory safery of core intrinsics using raw pointers](./challenges/0002-intrinsics-memory.md)
+  - [3: Verifying Raw Pointer Arithmetic Operations](./challenges/0003-pointer-arithmentic.md)
+  - [4: Memory safety of BTreeMap's `btree::node` module](./challenges/0004-btree-node.md)
+  - [5: Verify functions iterating over inductive data type: `linked_list`](./challenges/0005-linked-list.md)
+  - [6: Safety of `NonNull`](./challenges/0006-nonnull.md)
+  - [8: Contracts for SmallSort](./challenges/0008-smallsort.md)
+  - [9: Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
+  - [10: Memory safety of String](./challenges/0010-string.md)
+  - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
+  - [12: Safety of `NonZero`](./challenges/0012-nonzero.md)
+
+

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

@@ -1,7 +1,7 @@
 # Challenge 1: Verify `core` transmuting methods
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/19)
+- **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** 2024-06-12
 - **End date:** 2024-12-10
 

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

@@ -1,7 +1,7 @@
 # Challenge 2: Verify the memory safery of core intrinsics using raw pointers
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/16)
+- **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
 - **Start date:** *24/06/12*
 - **End date:** *24/12/10*
 

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

@@ -2,7 +2,7 @@
 
 - **Status:** Open
 - **Solution:**
-- **Tracking Issue:** <https://github.com/model-checking/verify-rust-std/issues/21>
+- **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
 - **Start date:** 24/06/24
 - **End date:** 24/12/10
 

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

@@ -1,7 +1,7 @@
 # Challenge 4: Memory safety of BTreeMap's `btree::node` module
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/25)
+- **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
 - **Start date:** *2024-07-01*
 - **End date:** *2024-12-10*
 

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

@@ -1,7 +1,7 @@
 # Challenge 5: Verify functions iterating over inductive data type: `linked_list`
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/29)
+- **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *24/07/01*
 - **End date:** *24/12/10*
 

doc/src/challenges/0006-nonnull.md

@@ -0,0 +1,84 @@
+# Challenge 6: Safety of NonNull
+
+- **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*
+
+-------------------
+
+
+## Goal
+
+Verify absence of undefined behavior of the [`ptr::NonNull` module](https://github.com/rust-lang/rust/blob/master/library/core/src/ptr/non_null.rs).
+Most of its functions are marked `unsafe`, yet they are used in 62 other modules
+of the standard library.
+
+### Success Criteria
+
+Prove absence of undefined behavior of the following 48 public functions. You
+may wish to do so by attaching pre- and postconditions to these, and then (if
+needed by the tooling that you choose to use) adding verification harnesses.
+
+1. `NonNull<T>::add`
+2. `NonNull<T>::addr`
+3. `NonNull<T>::align_offset`
+4. `NonNull<T>::as_mut<'a>`
+5. `NonNull<T>::as_mut_ptr`
+6. `NonNull<T>::as_non_null_ptr`
+7. `NonNull<T>::as_ptr`
+8. `NonNull<T>::as_ref<'a>`
+9. `NonNull<T>::as_uninit_mut<'a>`
+10. `NonNull<T>::as_uninit_ref<'a>`
+11. `NonNull<T>::as_uninit_slice<'a>`
+12. `NonNull<T>::as_uninit_slice_mut<'a>`
+13. `NonNull<T>::byte_add`
+14. `NonNull<T>::byte_offset_from<U: ?Sized>`
+15. `NonNull<T>::byte_offset`
+16. `NonNull<T>::byte_sub`
+17. `NonNull<T>::cast<U>`
+18. `NonNull<T>::copy_from_nonoverlapping`
+19. `NonNull<T>::copy_from`
+20. `NonNull<T>::copy_to_nonoverlapping`
+21. `NonNull<T>::copy_to`
+22. `NonNull<T>::dangling`
+23. `NonNull<T>::drop_in_place`
+24. `NonNull<T>::from_raw_parts`
+25. `NonNull<T>::get_unchecked_mut<I>`
+26. `NonNull<T>::is_aligned_to`
+27. `NonNull<T>::is_aligned`
+28. `NonNull<T>::is_empty`
+29. `NonNull<T>::len`
+30. `NonNull<T>::map_addr`
+31. `NonNull<T>::new_unchecked`
+32. `NonNull<T>::new`
+33. `NonNull<T>::offset_from`
+34. `NonNull<T>::offset`
+35. `NonNull<T>::read_unaligned`
+36. `NonNull<T>::read_volatile`
+37. `NonNull<T>::read`
+38. `NonNull<T>::replace`
+39. `NonNull<T>::slice_from_raw_parts`
+40. `NonNull<T>::sub_ptr`
+41. `NonNull<T>::sub`
+42. `NonNull<T>::swap`
+43. `NonNull<T>::to_raw_parts`
+44. `NonNull<T>::with_addr`
+45. `NonNull<T>::write_bytes`
+46. `NonNull<T>::write_unaligned`
+47. `NonNull<T>::write_volatile`
+48. `NonNull<T>::write`
+
+### List of UBs
+
+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):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/challenges/0008-smallsort.md

@@ -1,7 +1,7 @@
 # Challenge 8: Contracts for SmallSort
 
 - **Status:** Open
-- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/56)
+- **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
 - **Start date:** *2024-08-17*
 - **End date:** *2024-12-10*
 

doc/src/challenges/0009-duration.md

@@ -0,0 +1,72 @@
+# Challenge 9: Safe abstractions for `core::time::Duration`
+
+- **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*
+
+-------------------
+
+
+## Goal
+
+Write function contracts for `core::time::Duration` that can be used as safe abstractions.
+Even though the majority of `Duration` methods are safe, many of them are safe abstractions over unsafe code.
+
+For instance, the `new` method is implemented as follows in v1.3.0:
+```rust
+pub const fn new(secs: u64, nanos: u32) -> Duration {
+    if nanos < NANOS_PER_SEC {
+        // SAFETY: nanos < NANOS_PER_SEC, therefore nanos is within the valid range
+        Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
+    } else {
+        let secs = match secs.checked_add((nanos / NANOS_PER_SEC) as u64) {
+            Some(secs) => secs,
+            None => panic!("overflow in Duration::new"),
+        };
+        let nanos = nanos % NANOS_PER_SEC;
+        // SAFETY: nanos % NANOS_PER_SEC < NANOS_PER_SEC, therefore nanos is within the valid range
+        Duration { secs, nanos: unsafe { Nanoseconds(nanos) } }
+    }
+}
+```
+
+### Success Criteria
+
+Write a [type invariant](https://model-checking.github.io/kani/crates/doc/kani/derive.Invariant.html) for the struct `Duration`. Write function contracts for the following public functions.
+
+1. `Duration::new(secs: u64, nanos: u32) -> Duration`
+2. `Duration::from_secs(secs: u64) -> Duration`
+3. `Duration::from_millis(millis: u64) -> Duration`
+4. `Duration::from_micros(micros: u64) -> Duration`
+5. `Duration::from_nanos(nanos: u64) -> Duration`
+
+6. `Duration::as_secs(&self) -> u64`
+7. `Duration::as_millis(&self) -> u128`
+8. `Duration::as_micros(&self) -> u128`
+9. `Duration::as_nanos(&self) -> u128`
+10. `Duration::subsec_millis(&self) -> u32`
+11. `Duration::subsec_micros(&self) -> u32`
+12. `Duration::subsec_nanos(&self) -> u32`
+
+13. `Duration::checked_add(&self, rhs: Duration) -> Option<Duration>`
+14. `Duration::checked_sub(&self, rhs: Duration) -> Option<Duration>`
+15. `Duration::checked_mul(&self, rhs: u32) -> Option<Duration>`
+16. `Duration::checked_div(&self, rhs: u32) -> Option<Duration>`
+
+The memory safety and the contracts of the above listed functions must be verified
+for all possible input values.
+
+### List of UBs
+
+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):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.