Merge branch 'main' into new_challenge_convert_num

Author: sgpthomas

.github/pull_requests.toml

@@ -16,5 +16,7 @@ members = [
     "robdockins",
     "HuStmpHrrr",
     "Eh2406",
-    "jswrenn"
+    "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

@@ -2,6 +2,7 @@ name: Kani
 
 on:
   workflow_dispatch:
+  merge_group:
   pull_request:
     branches: [ main ]
   push:
@@ -37,18 +38,10 @@ jobs:
       # Step 2: Run Kani on the std library (default configuration)
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
-
-  test-kani-script:
-    name: Test Kani script
-    runs-on: ${{ matrix.os }}
-    strategy:
-      matrix:
-        os: [ubuntu-latest, macos-latest]
-        include:
-          - os: ubuntu-latest
-            base: ubuntu
-          - os: macos-latest
-            base: macos
+   
+  run-kani-list:
+    name: Kani List
+    runs-on: ubuntu-latest
     steps:
       # Step 1: Check out the repository
       - name: Checkout Repository
@@ -57,25 +50,18 @@ jobs:
           path: head
           submodules: true
 
-      # Step 2: Test Kani verification script with specific arguments
-      - name: Test Kani script (Custom Args)
-        run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse
-
-      # Step 3: Test Kani verification script in the repository directory
-      - name: Test Kani script (In Repo Directory)
-        working-directory: ${{github.workspace}}/head
-        run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse
-      
-      # Step 4: Run list on the std library and add output to job summary
+      # 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.txt', 'utf8');
+            const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
             await core.summary
-              .addRaw(kaniOutput)
-              .write();
+              .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');

.github/workflows/rustc.yml

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

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

@@ -24,29 +24,29 @@ Annotate Rust core::intrinsics functions that manipulate raw pointers with their
 
 Intrinsic functions to be annotated with safety contracts
 
-| Function | Location |
-|---------|---------|
-|typed_swap | core::intrisics |
-|vtable_size| core::intrisics |
-|vtable_align| core::intrisics |
-|copy_nonoverlapping| core::intrisics |
-|copy| core::intrisics |
-|write_bytes| core::intrisics |
-|size_of_val| core::intrisics |
-|arith_offset| core::intrisics |
-|volatile_copy_nonoverlapping_memory| core::intrisics |
-|volatile_copy_memory| core::intrisics |
-|volatile_set_memory| core::intrisics |
-|volatile_load| core::intrisics |
-|volatile_store| core::intrisics |
-|unaligned_volatile_load| core::intrisics |
-|unaligned_volatile_store| core::intrisics |
-|compare_bytes| core::intrisics |
-|min_align_of_val| core::intrisics |
-|ptr_offset_from| core::intrisics |
-|ptr_offset_from_unsigned| core::intrisics |
-|read_via_copy| core::intrisics |
-|write_via_move| core::intrisics |
+| Function                            | Location        |
+|-------------------------------------|-----------------|
+| typed_swap                          | core::intrisics |
+| vtable_size                         | core::intrisics |
+| vtable_align                        | core::intrisics |
+| copy_nonoverlapping                 | core::intrisics |
+| copy                                | core::intrisics |
+| write_bytes                         | core::intrisics |
+| size_of_val                         | core::intrisics |
+| arith_offset                        | core::intrisics |
+| volatile_copy_nonoverlapping_memory | core::intrisics |
+| volatile_copy_memory                | core::intrisics |
+| volatile_set_memory                 | core::intrisics |
+| volatile_load                       | core::intrisics |
+| volatile_store                      | core::intrisics |
+| unaligned_volatile_load             | core::intrisics |
+| unaligned_volatile_store            | core::intrisics |
+| compare_bytes                       | core::intrisics |
+| min_align_of_val                    | core::intrisics |
+| ptr_offset_from                     | core::intrisics |
+| ptr_offset_from_unsigned            | core::intrisics |
+| read_via_copy                       | core::intrisics |
+| write_via_move                      | core::intrisics |
 
 
 All the following usages of intrinsics were proven safe:

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

@@ -88,7 +88,7 @@ At least 3 of the following usages were proven safe:
 
 | Function          | Location      |
 |-------------------|---------------|
-| \[u8\]::is_asc_ii | core::slice   |
+| \[u8\]::is_ascii | core::slice   |
 | String::remove    | alloc::string |
  | Vec::swap_remove | alloc::vec |
  | Option::as_slice | core::option |

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

@@ -1,11 +1,12 @@
 # Challenge 11: Safety of Methods for Numeric Primitive Types
 
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
 - **Start date:** *2024/08/20*
-- **End date:** *2025/04/10*
+- **End date:** *2024/12/04*
 - **Reward:** *N/A*
+- **Contributors**: [Rajath M Kotyal](https://github.com/rajathkotyal), [Yen-Yun Wu](https://github.com/Yenyun035), [Lanfei Ma](https://github.com/lanfeima), [Junfeng Jin](https://github.com/MWDZ)
 
 -------------------
 

doc/src/tools.md

@@ -4,7 +4,7 @@ The verification tool ecosystem for Rust is rapidly growing, and we welcome the
 In this chapter, you can find a list of tools that have already been approved for new solutions,
 what is their CI current status, as well as more details on how to use them.
 
-If the tool you would like to add a new tool to the list of tool applications,
+If you would like to add a new tool to the list of tool applications,
 please see the [Tool Application](general-rules.md#tool-applications) section.
 
 ## Approved tools:

library/Cargo.lock

@@ -10,7 +10,7 @@ edition = "2021"
 
 [dependencies]
 core = { path = "../core" }
-compiler_builtins = { version = "0.1.123", features = ['rustc-dep-of-std'] }
+compiler_builtins = { version = "=0.1.138", features = ['rustc-dep-of-std'] }
 safety = { path = "../contracts/safety" }
 
 [dev-dependencies]

library/alloc/Cargo.toml

@@ -61,7 +61,7 @@ pub use std::alloc::Global;
 /// of the allocator registered with the `#[global_allocator]` attribute
 /// if there is one, or the `std` crate’s default.
 ///
-/// This function is expected to be deprecated in favor of the `alloc` method
+/// This function is expected to be deprecated in favor of the `allocate` method
 /// of the [`Global`] type when it and the [`Allocator`] trait become stable.
 ///
 /// # Safety
@@ -106,7 +106,7 @@ pub unsafe fn alloc(layout: Layout) -> *mut u8 {
 /// of the allocator registered with the `#[global_allocator]` attribute
 /// if there is one, or the `std` crate’s default.
 ///
-/// This function is expected to be deprecated in favor of the `dealloc` method
+/// This function is expected to be deprecated in favor of the `deallocate` method
 /// of the [`Global`] type when it and the [`Allocator`] trait become stable.
 ///
 /// # Safety
@@ -125,7 +125,7 @@ pub unsafe fn dealloc(ptr: *mut u8, layout: Layout) {
 /// of the allocator registered with the `#[global_allocator]` attribute
 /// if there is one, or the `std` crate’s default.
 ///
-/// This function is expected to be deprecated in favor of the `realloc` method
+/// This function is expected to be deprecated in favor of the `grow` and `shrink` methods
 /// of the [`Global`] type when it and the [`Allocator`] trait become stable.
 ///
 /// # Safety
@@ -145,7 +145,7 @@ pub unsafe fn realloc(ptr: *mut u8, layout: Layout, new_size: usize) -> *mut u8
 /// of the allocator registered with the `#[global_allocator]` attribute
 /// if there is one, or the `std` crate’s default.
 ///
-/// This function is expected to be deprecated in favor of the `alloc_zeroed` method
+/// This function is expected to be deprecated in favor of the `allocate_zeroed` method
 /// of the [`Global`] type when it and the [`Allocator`] trait become stable.
 ///
 /// # Safety
@@ -155,11 +155,14 @@ pub unsafe fn realloc(ptr: *mut u8, layout: Layout, new_size: usize) -> *mut u8
 /// # Examples
 ///
 /// ```
-/// use std::alloc::{alloc_zeroed, dealloc, Layout};
+/// use std::alloc::{alloc_zeroed, dealloc, handle_alloc_error, Layout};
 ///
 /// unsafe {
 ///     let layout = Layout::new::<u16>();
 ///     let ptr = alloc_zeroed(layout);
+///     if ptr.is_null() {
+///         handle_alloc_error(layout);
+///     }
 ///
 ///     assert_eq!(*(ptr as *mut u16), 0);
 ///