Merge branch 'model-checking:main' into transmute

Author: AlexLB99

.github/pull_requests.toml

@@ -9,7 +9,6 @@ members = [
     "remi-delmas-3000",
     "qinheping",
     "tautschnig",
-    "jaisnan",
     "patricklam",
     "ranjitjhala",
     "carolynzech",
@@ -18,5 +17,7 @@ members = [
     "Eh2406",
     "jswrenn",
     "havelund",
-    "jorajeev"
+    "jorajeev",
+    "rajath-mk",
+    "thanhnguyen-aws"
 ]

.github/workflows/update-subtree.yml

@@ -11,7 +11,10 @@ defaults:
 
 jobs:
   update-subtree-library:
-    runs-on: ubuntu-latest
+    # Changing the host platform may alter the libgit2 version as used by
+    # splitsh-lite, which will require changing the version of git2go.
+    # See https://github.com/jeffWelling/git2go?tab=readme-ov-file#which-go-version-to-use
+    runs-on: ubuntu-24.04
 
     steps:
     - name: Checkout Repository
@@ -34,12 +37,6 @@ jobs:
         fetch-depth: 0
         path: rust-tmp
 
-    - name: Checkout git-filter-repo
-      uses: actions/checkout@v4
-      with:
-        repository: newren/git-filter-repo
-        path: git-filter-repo
-
     - name: Fetch toolchain versions
       run: |
         CURRENT_TOOLCHAIN_DATE=$(grep -oP 'channel = "nightly-\K\d{4}-\d{2}-\d{2}' verify-rust-std/rust-toolchain.toml)
@@ -77,6 +74,30 @@ jobs:
       env:
         GH_TOKEN: ${{ github.token }}
 
+    - name: Checkout splitsh-lite
+      if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
+      uses: actions/checkout@v4
+      with:
+        repository: splitsh/lite
+        path: splitsh-lite
+
+    - name: Build splitsh-lite
+      if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
+      run: |
+        cd splitsh-lite
+        sudo apt-get install -y golang libgit2-dev
+        # git2go upstream hasn't been updated to more recent versions of
+        # libgit2, so using a fork that does stay up to date
+        sed -i 's#github.com/libgit2/git2go#github.com/jeffwelling/git2go#' go.mod splitter/*
+        # may need to adjust "v37" to a higher number per
+        # https://github.com/jeffWelling/git2go?tab=readme-ov-file#which-go-version-to-use
+        # depening on the libgit2 version being installed
+        sed -i -e 's/v34/v37/g' go.mod splitter/*.go
+        # v37.0.0 had issues that weren't fully fixed until v37.0.4
+        sed -i 's/v37.0.0/v37.0.4/' go.mod
+        go mod tidy
+        go build -o splitsh-lite github.com/splitsh/lite
+
     - name: Update subtree/library locally
       if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
       run: |
@@ -89,15 +110,16 @@ jobs:
         fi
 
         git checkout ${NEXT_COMMIT_HASH}
-        ../git-filter-repo/git-filter-repo --subdirectory-filter library --force
-        git checkout -b subtree/library
+        /usr/bin/time -v ../splitsh-lite/splitsh-lite --progress --prefix=library --target subtree/library
+        git checkout -b subtree/library subtree/library
 
         cd ../verify-rust-std
         git remote add rust-filtered ../rust-tmp/
         git fetch rust-filtered
         git checkout -b subtree/library rust-filtered/subtree/library
-        # The filter-subtree operation adds an extraneous `library/` folder containing the submodules
-        # (c.f. https://github.com/model-checking/verify-rust-std/issues/249), so remove that before committing.
+        # The checkout still leaves behind the library folder with submodules.
+        # We need to remove this as we'd otherwise have the create-pull-request
+        # action create an extra commit.
         rm -rf library
         SUBTREE_HEAD_MSG=$(git log --format=%s -n 1 origin/subtree/library)
         UPSTREAM_FROM=$(git log --grep="${SUBTREE_HEAD_MSG}" -n 1 --format=%H rust-filtered/subtree/library)
@@ -107,7 +129,6 @@ jobs:
           echo "MERGE_CONFLICTS=noop" >> $GITHUB_ENV
         else
           git branch --set-upstream-to=origin/subtree/library
-          git -c user.name=gitbot -c user.email=git@bot rebase
           echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
         fi
 
@@ -130,12 +151,15 @@ jobs:
       if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
       run: |
         cd verify-rust-std
+        if ! git rev-parse --verify subtree/library; then
+          git checkout -t -b subtree/library origin/update-subtree/library
+        fi
         git checkout main
 
         # This command may fail, which will require human intervention.
         if ! git \
             -c user.name=gitbot -c user.email=git@bot \
-            subtree merge --prefix=library update-subtree/library --squash; then
+            subtree merge --prefix=library subtree/library --squash; then
           echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
           git -c user.name=gitbot -c user.email=git@bot commit -a -m "Merge from $NEXT_COMMIT_HASH with conflicts"
         else

doc/mdbook-metrics/src/main.rs

@@ -44,6 +44,25 @@ fn run_kani_metrics_script() -> Result<(), Error> {
     Command::new("python")
         .args(&[
             "kani_std_analysis.py",
+            "--crate",
+            "core",
+            "--metrics-file",
+            "metrics-data-core.json",
+            "--plot-only",
+            "--plot-dir",
+            &tools_path.to_string_lossy(),
+        ])
+        .stdout(std::process::Stdio::null())
+        .stderr(std::process::Stdio::null())
+        .status()?;
+
+    Command::new("python")
+        .args(&[
+            "kani_std_analysis.py",
+            "--crate",
+            "std",
+            "--metrics-file",
+            "metrics-data-std.json",
             "--plot-only",
             "--plot-dir",
             &tools_path.to_string_lossy(),
@@ -83,12 +102,19 @@ fn add_graphs(chapter: &mut Chapter) {
 
 Note that these metrics are for x86-64 architectures.
 
-## `core`
+### `core`
 ![Unsafe Metrics](core_unsafe_metrics.png)
 
 ![Safe Abstractions Metrics](core_safe_abstractions_metrics.png)
 
 ![Safe Metrics](core_safe_metrics.png)
+
+### `std`
+![Unsafe Metrics](std_unsafe_metrics.png)
+
+![Safe Abstractions Metrics](std_safe_abstractions_metrics.png)
+
+![Safe Metrics](std_safe_metrics.png)
 "#;
 
     chapter.content.push_str(new_content);

doc/src/challenges/0006-nonnull.md

@@ -1,11 +1,11 @@
 # Challenge 6: Safety of NonNull
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
 - **Start date:** *2024/08/16*
 - **End date:** *2025/04/10*
 - **Reward:** *N/A*
-
+- **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative)
 -------------------
 
 

doc/src/challenges/0008-smallsort.md

@@ -11,8 +11,7 @@
 
 ## Goal
 
-The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting
-algorithms optimized for slices with small lengths.
+The implementations of the traits `StableSmallSortTypeImpl`, `UnstableSmallSortTypeImpl`, and `UnstableSmallSortFreezeTypeImpl` in the `smallsort` [module](https://github.com/rust-lang/rust/blob/master/library/core/src/slice/sort/shared/smallsort.rs) of the Rust standard library are the sorting algorithms with optimized implementations for slices with small lengths.
 In this challenge, the goal is to, first prove the memory safety of the public functions in the `smallsort` module, and, second, write contracts for them to
 show that the sorting algorithms actually sort the slices.
 

doc/src/challenges/0012-nonzero.md

@@ -73,7 +73,6 @@ Verify the safety of the following functions and methods (all located within `co
 |  `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
 

doc/src/challenges/0014-convert-num.md

@@ -1,11 +1,11 @@
 # Challenge 14: Safety of Primitive Conversions
 
-- **Status:** Open
-- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/220
+- **Status:** Resolved
+- **Tracking Issue:** [#220](https://github.com/model-checking/verify-rust-std/issues/220)
 - **Start date:** 2024/12/15
 - **End date:** 2025/2/28
 - **Prize:** *TBD*
-
+- **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
 
 ## Goal

doc/src/challenges/0015-intrinsics-simd.md

@@ -3,7 +3,7 @@
 - **Status:** Open
 - **Reward:** 
 - **Solution:** 
-- **Tracking Issue:** https://github.com/model-checking/verify-rust-std/issues/173
+- **Tracking Issue:** [#173](https://github.com/model-checking/verify-rust-std/issues/173)
 - **Start date:** 2025/02/01
 - **End date:** 2025/08/01