Merge branch 'main' into morechallenges

Author: thanhnguyen-aws

.github/workflows/update-subtree.yml

@@ -117,6 +117,10 @@ jobs:
         git remote add rust-filtered ../rust-tmp/
         git fetch rust-filtered
         git checkout -b subtree/library rust-filtered/subtree/library
+        # 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)
         UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
@@ -133,11 +137,14 @@ jobs:
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
-        body: |
+        body: >
           This is an automated PR to update the subtree/library branch to the changes
-          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
-          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
-          **Do not merge this PR using the merge queue. Instead, use the rebase strategy.**
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}), inclusive.
+
+          **Review this PR as usual, but do not merge this PR using the GitHub web interface.
+          Instead, once it is approved, use `git push` to literally push the changes to `subtree/library`
+          without any rebase or merge.**
         branch: update-subtree/library
         delete-branch: true
         base: subtree/library
@@ -147,20 +154,36 @@ jobs:
       if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
       run: |
         cd verify-rust-std
-        if ! git rev-parse --verify subtree/library; then
+        # create-pull-request resets branches locally, implying that
+        # `subtree/library` no longer is what the above instructions created.
+        if [ "${SUBTREE_PR_EXISTS}" = "yes" ]; then
           git checkout -t -b subtree/library origin/update-subtree/library
+        else
+          git checkout subtree/library
+          git reset --hard origin/update-subtree/library
         fi
         git checkout main
 
+        # Tell git about the correct merge base to use, which is the subtree
+        # head that we last merged from.
+        PREV_SUBTREE_HEAD=$(git log --grep="^git-subtree-split:" | egrep '^[[:space:]]+git-subtree-split:' | awk '{print $2;exit}')
+        echo "Previous subtree head: ${PREV_SUBTREE_HEAD}"
+        git replace --graft subtree/library ${PREV_SUBTREE_HEAD}
+        git replace --graft main ${PREV_SUBTREE_HEAD}
+
         # This command may fail, which will require human intervention.
         if ! git \
             -c user.name=gitbot -c user.email=git@bot \
-            subtree merge --prefix=library subtree/library --squash; then
+            merge -Xsubtree=library subtree/library; 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
           echo "MERGE_CONFLICTS=no" >> $GITHUB_ENV
         fi
+        git replace -d subtree/library
+        git replace -d main~1
+        NEW_SUBTREE_HEAD=$(git rev-parse subtree/library)
+        echo "NEW_SUBTREE_HEAD=${NEW_SUBTREE_HEAD}" >> $GITHUB_ENV
 
         sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
         git -c user.name=gitbot -c user.email=git@bot \
@@ -169,16 +192,22 @@ jobs:
         sed -i "s/commit = .*/commit = \"${KANI_COMMIT_HASH}\"/" tool_config/kani-version.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
+
     - name: Create Pull Request without conflicts
       if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
-        body: |
+        body: >
           This is an automated PR to merge library subtree updates
-          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
-          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}), inclusive.
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}), inclusive.
           This is a clean merge, no conflicts were detected.
+          **Do not remove or edit the following annotations:**
+
+          git-subtree-dir: library
+
+          git-subtree-split: ${{ env.NEW_SUBTREE_HEAD }}
         branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
         delete-branch: true
         base: main
@@ -189,12 +218,17 @@ jobs:
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Merge subtree update for toolchain nightly-${{ env.NEXT_TOOLCHAIN_DATE }}'
-        body: |
+        body: >
           This is an automated PR to merge library subtree updates
-          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (${{ env.CURRENT_COMMIT_HASH }})
-          to ${{ env.NEXT_TOOLCHAIN_DATE }} (${{ env.NEXT_COMMIT_HASH }}) (inclusive)
+          from ${{ env.CURRENT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.CURRENT_COMMIT_HASH }})
+          to ${{ env.NEXT_TOOLCHAIN_DATE }} (rust-lang/rust@${{ env.NEXT_COMMIT_HASH }}) (inclusive)
           into main. `git merge` resulted in conflicts, which require manual resolution.
           Files were commited with merge conflict markers.
+          **Do not remove or edit the following annotations:**
+
+          git-subtree-dir: library
+
+          git-subtree-split: ${{ env.NEW_SUBTREE_HEAD }}
         branch: sync-${{ env.NEXT_TOOLCHAIN_DATE }}
         delete-branch: true
         base: main

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