Merge branch 'main' into usage_proofs

.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/workflows/pr_approval.yml

@@ -52,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);
@@ -70,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.');
             }

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

@@ -1,4 +1,4 @@
-# Challenge 2: Verify the memory safery of core intrinsics using raw pointers
+# Challenge 2: Verify the memory safety of core intrinsics using raw pointers
 
 - **Status:** Open
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
@@ -61,7 +61,7 @@ All the following usages of intrinsics were proven safe:
 
 
 
-Annotate and verify all the functions that below that expose intrinsics with safety contracts
+Annotate and verify all the functions below that expose intrinsics with safety contracts
 
 | Function | Location |
 |---------|---------|

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

@@ -11,7 +11,7 @@
 
 ## Goal
 
-Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate the its internal inductive-defined data type.
+Verify the memory safety of [`alloc::collections::linked_list` functions](https://github.com/rust-lang/rust/blob/c290e9de32e8ba6a673ef125fde40eadd395d170/library/alloc/src/collections/linked_list.rs) that iterate over its internal inductive-defined data type.
 
 ### Details
 

doc/src/challenges/0009-duration.md

@@ -1,14 +1,13 @@
 # Challenge 9: Safe abstractions for `core::time::Duration`
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72)
 - **Start date:** *2024/08/20*
-- **End date:** *2025/04/10*
+- **End date:** *2024/12/10*
 - **Reward:** *N/A*
-
+- **Contributors**: [Samuel Thomas](https://github.com/sgpthomas) and [Cole Vick](https://github.com/cvick32)
 -------------------
 
-
 ## Goal
 
 Write function contracts for `core::time::Duration` that can be used as safe abstractions.

doc/src/general-rules.md

@@ -69,20 +69,17 @@ Follow the following steps to create a new proposal:
 
 ## Tool Applications
 
-Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools):
-
-* Any new tool that participants want to enable will require an application using the [tool application template](./tool_template.md).
-* The tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS
-* A new tool application should clearly specify the differences to existing techniques and provide sufficient background
-  of why this is needed.
-* The tool application should also include mechanisms to audit its implementation and correctness.
-* Once the tool is approved, the participant needs to create a PR that creates a new action that runs the
-  std library verification using the new tool, as well as an entry to the “Approved Tools” section of this book.
-* Once the PR is merged, the tool is considered integrated.
-* The repository will be updated periodically, which can impact the tool capacity to analyze the new version of the repository.
-  I.e., the action may no longer pass after an update.
-  This will not impact the approval status of the tool, however,
-  new solutions that want to employ the tool may need to ensure the action is passing first.
+Solutions must be automated using one of the tools previously approved and listed [here](tools.md#approved-tools).
+To use a new tool, participants must first submit an application for it.
+
+* To submit a tool application, open a new issue in this repository using the "Tool Application" issue template.
+* The committee will review the application. Once a committee member approves the application, the participant needs to create a PR with:
+  * A new workflow that runs the tool against the standard library.
+  * A new entry to the “Approved Tools” section of this book.
+* Once this PR is merged, the tool is considered integrated, and the tool application issue will be closed.
+
+The repository will be updated periodically, which can impact a tool's capacity to analyze the new version of the repository (i.e., the workflow may no longer pass after an update).
+If it is determined that the tool requires changes and such changes cannot be provided in a timely fashion the tool's approval may be revoked.
 
 ## Committee Applications
 

doc/src/tool_template.md

@@ -15,6 +15,9 @@ _Please enter a description for your tool and any information you deem relevant.
 * [ ] Is the tool under development? 
 * [ ] Will you or your team be able to provide support for the tool?
 
+## Comparison to Other Approved Tools
+_Describe how this tool compares to the other approved tools. For example, are there certain properties that this tool can prove that the other tools cannot? The comparison does not need to be exhaustive; the purpose of this section is for the committee to understand the salient differences, and how this tool would fit into the larger effort._
+
 ## 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)._
 
@@ -24,8 +27,12 @@ _Please list the license(s) that are used by your tool, and if to your knowledge
 2. \[Second Step\]
 3. \[and so on...\]
 
-## Artifacts
-_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._
+## Artifacts & Audit Mechanisms
+_If there are noteworthy examples of using the tool to perform verification, please include them in this section. Links, papers, etc._
+_Also include mechanisms for the committee to audit the implementation and correctness of this tool (e.g., regression tests)._
+
+## Versioning
+_Please describe how you version the tool._
 
-## CI & Versioning
-_Please describe how you version the tool and how it will be supported in CI pipelines._
+## CI
+_If your tool is approved, you will be responsible merging a workflow into this repository that runs your tool against the standard library. For an example, see the Kani workflow (.github/workflows/kani.yml). Describe, at a high level, how your workflow will operate. (E.g., how will you package the tool to run in CI, how will you identify which proofs to run?)._

library/core/src/ffi/c_str.rs

@@ -9,8 +9,11 @@ use crate::marker::PhantomData;
 use crate::ptr::NonNull;
 use crate::slice::memchr;
 use crate::{fmt, ops, slice, str};
+use safety::{requires, ensures};
 
 use crate::ub_checks::Invariant;
+#[allow(unused_imports)]
+use crate::ub_checks::can_dereference;
 
 #[cfg(kani)]
 use crate::kani;
@@ -229,6 +232,25 @@ impl Invariant for &CStr {
     }
 }
 
+// Helper function
+#[cfg(kani)]
+#[requires(!ptr.is_null())]
+fn is_null_terminated(ptr: *const c_char) -> bool {
+    let mut next = ptr;
+    let mut found_null = false;
+    while can_dereference(next) {
+        if unsafe { *next == 0 } {
+            found_null = true;
+            break;
+        }
+        next = next.wrapping_add(1);
+    }
+    if (next.addr() - ptr.addr()) >= isize::MAX as usize {
+        return false;
+    }
+    found_null
+}
+
 impl CStr {
     /// Wraps a raw C string with a safe C string wrapper.
     ///
@@ -296,6 +318,8 @@ impl CStr {
     #[must_use]
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0")]
+    #[requires(!ptr.is_null() && is_null_terminated(ptr))]
+    #[ensures(|result: &&CStr| result.is_safe())]
     pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr {
         // SAFETY: The caller has provided a pointer that points to a valid C
         // string with a NUL terminator less than `isize::MAX` from `ptr`.
@@ -1017,6 +1041,16 @@ mod verify {
         assert_eq!(bytes, &slice[..end_idx]);
         assert!(c_str.is_safe());
     }
+
+    #[kani::proof_for_contract(CStr::from_ptr)]
+    #[kani::unwind(33)]
+    fn check_from_ptr_contract() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let ptr = string.as_ptr() as *const c_char;
+
+        unsafe { CStr::from_ptr(ptr); }
+    }
 
     #[kani::proof]
     #[kani::unwind(33)]