Merge remote-tracking branch 'origin/main' into bedrock-library/alloc/src/alloc.rs

Author: tautschnig

.github/ISSUE_TEMPLATE/tool_application.md

@@ -0,0 +1,10 @@
+---
+name: Tool Application
+about: Submit a new tool application
+title: "[Tool Application] "
+labels: Tool Application
+---
+
+<!--
+Please see https://model-checking.github.io/verify-rust-std/tool_template.html for the application template.
+-->

.github/pull_requests.toml

@@ -12,5 +12,11 @@ members = [
     "jaisnan",
     "patricklam",
     "ranjitjhala",
-    "carolynzech"
+    "carolynzech",
+    "robdockins",
+    "HuStmpHrrr",
+    "Eh2406",
+    "jswrenn",
+    "havelund",
+    "jorajeev"
 ]

.github/workflows/book.yml

@@ -3,6 +3,7 @@
 name: Build Book
 on:
   workflow_dispatch:
+  merge_group:
   pull_request:
     branches: [ main ]
   push:

.github/workflows/kani.yml

@@ -1,38 +1,67 @@
-# This workflow is responsible for verifying the standard library with Kani.
-
 name: Kani
+
 on:
   workflow_dispatch:
+  merge_group:
   pull_request:
     branches: [ main ]
   push:
     paths:
       - 'library/**'
       - '.github/workflows/kani.yml'
-      - 'scripts/check_kani.sh'
+      - 'scripts/run-kani.sh'
 
 defaults:
   run:
     shell: bash
 
 jobs:
-  build:
+  check-kani-on-std:
+    name: Verify std library
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        # Kani does not support windows.
         os: [ubuntu-latest, macos-latest]
         include:
           - os: ubuntu-latest
             base: ubuntu
           - os: macos-latest
             base: macos
     steps:
-      - name: Checkout Library
+      # Step 1: Check out the repository
+      - name: Checkout Repository
         uses: actions/checkout@v4
         with:
           path: head
           submodules: true
 
-      - name: Run Kani Script
-        run: bash ./head/scripts/check_kani.sh ${{github.workspace}}/head
+      # Step 2: Run Kani on the std library (default configuration)
+      - name: Run Kani Verification
+        run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
+   
+  run-kani-list:
+    name: Kani List
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          path: head
+          submodules: true
+
+      # Step 2: Run list on the std library
+      - name: Run Kani List
+        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
+      
+      # Step 3: Add output to job summary
+      - 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.md', 'utf8');
+            await core.summary
+              .addHeading('Kani List Output', 2)
+              .addRaw(kaniOutput, false)
+              .write();

.github/workflows/pr_approval.yml

@@ -1,25 +1,33 @@
+# This workflow checks that the PR has been approved by 2+ members of the committee listed in `pull_requests.toml`.
+#
+# Run this action when a pull request review is submitted / dismissed.
+# Note that an approval can be dismissed, and this can affect the job status.
+# We currently trust that contributors won't make significant changes to their PRs after approval, so we accept
+# changes after approval.
+#
+# We still need to run this in the case of a merge group, since it is a required step. In that case, the workflow
+# is a NOP.
 name: Check PR Approvals
-
-# For now, the workflow gets triggered only when a review is submitted
-# This technically means, a PR with zero approvals can be merged by the rules of this workflow alone
-# To protect against that scenario, we can turn on number of approvals required to 2 in the github settings
-# of the repository
 on:
+  merge_group:
   pull_request_review:
-    types: [submitted]
+    types: [submitted, dismissed]
 
 jobs:
   check-approvals:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout repository
         uses: actions/checkout@v2
+        if: ${{ github.event_name != 'merge_group' }}
 
       - name: Install TOML parser
         run: npm install @iarna/toml
+        if: ${{ github.event_name != 'merge_group' }}
 
       - name: Check PR Relevance and Approvals
         uses: actions/github-script@v6
+        if: ${{ github.event_name != 'merge_group' }}
         with:
           script: |
             const fs = require('fs');
@@ -44,8 +52,11 @@ jobs:
               pull_number = context.issue.number;
             }
 
+            console.log(`owner is ${owner}`);
+            console.log(`pull_number is ${pull_number}`);
 
             // Get parsed data
+            let requiredApprovers;
             try {
               const tomlContent = fs.readFileSync('.github/pull_requests.toml', 'utf8');
               console.log('TOML content:', tomlContent);
@@ -62,38 +73,63 @@ jobs:
               return;
             }
 
-            // Get all reviews
-            const reviews = await github.rest.pulls.listReviews({
-              owner,
-              repo,
-              pull_number
-            });
+            // Get all reviews with pagination
+            async function getAllReviews() {
+              let allReviews = [];
+              let page = 1;
+              let page_limit = 100;
+              
+              while (page < page_limit) {
+                const response = await github.rest.pulls.listReviews({
+                  owner,
+                  repo,
+                  pull_number,
+                  per_page: 100,
+                  page
+                });
+                
+                allReviews = allReviews.concat(response.data);
+                
+                if (response.data.length < 100) {
+                  break;
+                }
+                
+                page++;
+              }
+
+              if (page == page_limit) {
+                console.log(`WARNING: Reached page limit of ${page_limit} while fetching reviews data; approvals count may be less than the real total.`)
+              }
+              
+              return allReviews;
+            }
+
+            const reviews = await getAllReviews();
 
             // Example: approvers = ["celina", "zyad"]
             const approvers = new Set(
-              reviews.data
+              reviews
                 .filter(review => review.state === 'APPROVED')
                 .map(review => review.user.login)
             );
 
             const requiredApprovals = 2;
-            const currentCountfromCommittee = Array.from(approvers)
-              .filter(approver => requiredApprovers.includes(approver))
-              .length;
-
-            // TODO: Improve logging and messaging to the user
-            console.log('PR Approvers:', Array.from(approvers));
-            console.log('Required Approvers:', requiredApprovals);
+            const committeeApprovers = Array.from(approvers)
+              .filter(approver => requiredApprovers.includes(approver));
+            const currentCountfromCommittee = committeeApprovers.length;
 
             // Core logic that checks if the approvers are in the committee
-            const checkName = 'PR Approval Status';
-            const conclusion = (approvers.size >= requiredApprovals && currentCountfromCommittee >= 2) ? 'success' : 'failure';
-            const output = {
-              title: checkName,
-              summary: `PR has ${approvers.size} total approvals and ${requiredApprovals} required approvals.`,
-              text: `Approvers: ${Array.from(approvers).join(', ')}\nRequired Approvers: ${requiredApprovers.join(', ')}`
-            };
+            const conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
 
+            console.log('PR Approval Status');
+            console.log(`PR has ${approvers.size} total approvals and ${currentCountfromCommittee} required approvals from the committee.`);
+            
+            console.log(`Committee Members: [${requiredApprovers.join(', ')}]`);
+            console.log(`Committee Approvers: ${committeeApprovers.length === 0 ? 'NONE' : `[${committeeApprovers.join(', ')}]`}`);
+            console.log(`All Approvers: ${approvers.size === 0 ? 'NONE' : `[${Array.from(approvers).join(', ')}]`}`);
+            
             if (conclusion === 'failure') {
-              core.setFailed(`PR needs at least ${requiredApprovals} total approvals and 2 required approvals. Current approvals: ${approvers.size}, Required approvals: ${requiredApprovals}`);
+              core.setFailed(`PR needs 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
+            } else {
+              core.info('PR approval check passed successfully.');
             }

.github/workflows/rustc.yml

@@ -4,6 +4,7 @@
 name: Rust Tests
 on:
   workflow_dispatch:
+  merge_group:
   pull_request:
     branches: [ main ]
   push:

.gitignore

@@ -19,6 +19,7 @@ Session.vim
 ## Build
 /book/
 /build/
+/kani_build/
 /target
 library/target
 *.rlib

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,11 +39,11 @@ 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.
 
 ## Introducing a New Tool
 
-Please use the [template available in this repository](.github/TOOL_REQUEST_TEMPLATE.md) to introduce a new verification tool.
+Please use the [template available in this repository](./doc/src/tool_template.md) to introduce a new verification tool.

doc/src/SUMMARY.md

@@ -14,15 +14,16 @@
 
 - [Challenges](./challenges.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)
+  - [2: Verify the memory safety 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)
+  - [7: Safety of Methods for Atomic Types & Atomic Intrinsics](./challenges/0007-atomic-types.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)
-
+  - [13: Safety of `CStr`](./challenges/0013-cstr.md)
 

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.

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*
 
 -------------------