Merge branch 'main' into align-offset-contracts

.github/workflows/pr_approval.yml

@@ -7,12 +7,6 @@ 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:
@@ -51,22 +45,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 +95,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}`);
             }

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

@@ -18,5 +18,9 @@
   - [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)
+  - [Safety of NonNull](./challenges/0006-nonnull.md)
   - [Contracts for SmallSort](./challenges/0008-smallsort.md)
+  - [Safe abstractions for `core::time::Duration`](./challenges/0009-duration.md)
   - [Memory safety of String](./challenges/0010-string.md)
+  - [Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md)
+  - [Safety of NonZero](./challenges/0012-nonzero.md)

doc/src/challenges/0006-nonnull.md

@@ -0,0 +1,84 @@
+# Challenge 6: Safety of NonNull
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](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/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.

doc/src/challenges/0011-floats-ints.md

@@ -0,0 +1,59 @@
+# Challenge 11: Safety of Methods for Numeric Primitive Types
+
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/59)
+- **Start date:** *2024-08-20*
+- **End date:** *2024-12-10*
+
+-------------------
+
+## Goal
+
+Verify the safety of public unsafe methods for floats and integers in `core::num`.
+
+To find the documentation for these methods, navigate first to the [`core::num` documentation](https://doc.rust-lang.org/core/num/index.html), then click on the appropriate primitive type in the left-side menu bar. For example, for `i8::unchecked_add`, click on `i8`.
+
+## Success Criteria
+
+### Part 1: Unsafe Integer Methods
+
+Prove the absence of arithmetic overflow/underflow and undefined behavior in the following methods for each of the listed integer types, given that their safety preconditions are satisfied:
+
+| Method              | Integer Types |
+| :---           |     :---
+| `unchecked_add`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `unchecked_sub`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `unchecked_mul`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `unchecked_shl`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `unchecked_shr`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `unchecked_neg`  |  `i8`, `i16`, `i32`, `i64`, `i128` |
+
+
+### Part 2: Safe API Verification
+
+Now, verify some of the safe APIs that leverage the unsafe integer methods from Part 1. Verify the absence of arithmetic overflow/underflow and undefined behavior of the following methods for each of the listed integer types:
+
+| Method              | Integer Types |
+| :---           |     :---
+| `wrapping_shl`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `wrapping_shr`  |  `i8`, `i16`, `i32`, `i64`, `i128`, `u8`, `u16`, `u32`, `u64`, `u128` |
+| `widening_mul`  |  `u8`, `u16`, `u32`, `u64` |
+| `carrying_mul`  |  `u8`, `u16`, `u32`, `u64` |
+
+
+### Part 3: Float to Integer Conversion
+
+Verify the absence of arithmetic overflow/underflow and undefined behavior in `to_int_unchecked` for `f16`, `f32`, `f64`, and `f128`.
+
+
+## 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):
+
+* Invoking undefined behavior via compiler intrinsics.
+* 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.