Simplify pr workflow to require 2 approvals on all PR's

.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/src/SUMMARY.md

@@ -22,3 +22,4 @@
   - [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 NonZero](./challenges/0012-nonzero.md)

doc/src/challenges/0012-nonzero.md

@@ -0,0 +1,87 @@
+# Challenge 12: Safety of `NonZero`
+
+- **Status:** Open
+- **Tracking Issue:** [Link to issue](https://github.com/model-checking/verify-rust-std/issues/71)
+- **Start date:** *2024-08-23*
+- **End date:** *2024-12-10*
+
+-------------------
+
+## Goal
+
+Verify the safety of `NonZero` in `core::num`.
+
+### Assumptions
+
+`new` and `get` leverage `transmute_unchecked`, so verifying the safety of these methods would require verifying that transmutations are safe. This task is out of scope for this challenge (instead, it's work for [Challenge 1](0001-core-transmutation.md)). For this challenge, for a transmutation from type `T` to type `U`, it suffices to write and verify a contract that `T` and `U` have the same size.
+
+You may assume that each `NonZeroInner` type upholds the safety conditions of the `ZeroablePrimitive` trait. Specifically, you need not verify that the integer primitives which implement `ZeroablePrimitive` are valid when 0, or that transmutations to the `Option` type are sound.
+
+### Success Criteria
+
+#### Part 1: `new` and `new_unchecked`
+
+Verify the safety and correctness of `NonZero::new` and `NonZero::new_unchecked`.
+
+Specifically, write and verify contracts specifying the following:
+1. The preconditions specified by the `SAFETY` comments are upheld. 
+2. For an input `n`:  
+    a. A `NonZero` object is created if and only if the input was nonzero.  
+    b. The value of the `NonZeroInner` object equals `n`.
+
+#### Part 2: Other Uses of `unsafe`
+
+Verify the safety of the following functions and methods (all located within `core::num::nonzero`):
+
+| Function |
+|--------- |
+|  `max`   |
+|  `min`   |
+|  `clamp`   |
+|  `bitor`  (all 3 implementations) |
+|  `count_ones`   |
+|  `rotate_left`   |
+|  `rotate_right`   |
+|  `swap_bytes`   |
+|  `reverse_bits`   |
+|  `from_be`   |
+|  `from_le`   |
+|  `to_be`   |
+|  `to_le`   |
+|  `checked_mul`   |
+|  `saturating_mul`   |
+|  `unchecked_mul`   |
+|  `checked_pow`   |
+|  `saturating_pow`   |
+|  `neg`   |
+|  `checked_add`   |
+|  `saturating_add`   |
+|  `unchecked_add`   |
+|  `checked_next_power_of_two`   |
+|  `midpoint`   |
+|  `isqrt`   |
+|  `abs`   |
+|  `checked_abs`   |
+|  `overflowing_abs`   |
+|  `saturating_abs`   |
+|  `wrapping_abs`   |
+|  `unsigned_abs`   |
+|  `checked_neg`   |
+|  `overflowing_neg`   |
+|  `wrapping_neg` |
+|  `from_mut`   |
+|  `from_mut_unchecked` |
+
+You are not required to write correctness contracts for these methods (e.g., for `max`, ensuring that the `result` is indeed the maximum of the inputs), but it would be great to do so!
+
+### 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 [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Invoking undefined behavior via compiler intrinsics.
+* Reading from uninitialized memory.
+* 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.