Merge remote-tracking branch 'origin/main' into iter-range-rs-contracts

Author: tautschnig

.github/workflows/kani-metrics.yml

@@ -14,6 +14,13 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
+    - name: Remove unnecessary software to free up disk space
+      run: |
+        # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+        df -h
+        sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+        df -h
+
     - name: Checkout Repository
       uses: actions/checkout@v4
       with:

.github/workflows/kani.yml

@@ -37,6 +37,14 @@ jobs:
       WORKER_TOTAL: 4
 
     steps:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -67,6 +75,14 @@ jobs:
       fail-fast: false
 
     steps:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -159,6 +175,14 @@ jobs:
       fail-fast: true
 
     steps:
+      - name: Remove unnecessary software to free up disk space
+        if: matrix.os == 'ubuntu-latest'
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4
@@ -253,6 +277,13 @@ jobs:
     name: Kani List
     runs-on: ubuntu-latest
     steps:
+      - name: Remove unnecessary software to free up disk space
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /usr/local/.ghcup
+          df -h
+
       # Step 1: Check out the repository
       - name: Checkout Repository
         uses: actions/checkout@v4

.github/workflows/update-subtree.yml

@@ -11,6 +11,7 @@ defaults:
 
 jobs:
   update-subtree-library:
+    if: github.repository == 'model-checking/verify-rust-std'
     # 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
@@ -85,6 +86,7 @@ jobs:
       if: ${{ env.SUBTREE_PR_EXISTS == 'no' }}
       run: |
         cd splitsh-lite
+        sudo apt-get update
         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
@@ -110,6 +112,10 @@ jobs:
         fi
 
         git checkout ${NEXT_COMMIT_HASH}
+        # Collect submodule commits; note that submodules (intentionally!)
+        # aren't initialized, hence lines will be prefixed with "-" (see git
+        # submodule --help).
+        git submodule status  -- library/ | sed 's/^-//' > ../submodule-heads
         /usr/bin/time -v ../splitsh-lite/splitsh-lite --progress --prefix=library --target subtree/library
         git checkout -b subtree/library subtree/library
 
@@ -165,6 +171,7 @@ jobs:
           fi
         fi
         git checkout main
+        git submodule foreach 'git fetch'
 
         # Tell git about the correct merge base to use, which is the subtree
         # head that we last merged from.
@@ -178,6 +185,8 @@ jobs:
             -c user.name=gitbot -c user.email=git@bot \
             merge -Xsubtree=library subtree/library; then
           echo "MERGE_CONFLICTS=yes" >> $GITHUB_ENV
+          # Ignore submodule conflicts, those are dealt with below.
+          for d in $(cat ../submodule-heads | cut -f2 -d" ") ; do git reset HEAD $d ; done
           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
@@ -187,6 +196,14 @@ jobs:
         NEW_SUBTREE_HEAD=$(git rev-parse subtree/library)
         echo "NEW_SUBTREE_HEAD=${NEW_SUBTREE_HEAD}" >> $GITHUB_ENV
 
+        # Set submodules to upstream versions
+        git submodule update --init
+        git submodule foreach 'grep $sm_path $toplevel/../submodule-heads | cut -f1 -d" " | xargs git checkout'
+        if ! git diff --quiet; then
+          git -c user.name=gitbot -c user.email=git@bot \
+            commit -m "Update submodules" library/
+        fi
+
         sed -i "s/^channel = \"nightly-.*\"/channel = \"nightly-${NEXT_TOOLCHAIN_DATE}\"/" rust-toolchain.toml
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update toolchain to ${NEXT_TOOLCHAIN_DATE}" rust-toolchain.toml
@@ -195,6 +212,22 @@ jobs:
         git -c user.name=gitbot -c user.email=git@bot \
           commit -m "Update Kani version to ${KANI_COMMIT_HASH}" tool_config/kani-version.toml
 
+        # Try to automatically patch the VeriFast proofs
+        pushd verifast-proofs
+        if bash ./patch-verifast-proofs.sh; then
+          if ! git diff --quiet; then
+            git -c user.name=gitbot -c user.email=git@bot \
+              commit . -m "Update VeriFast proofs"
+          else
+            # The original files have not changed; no updates to the VeriFast proofs are necessary.
+            true
+          fi
+        else
+          # Patching the VeriFast proofs failed; requires manual intervention.
+          true
+        fi
+        popd
+
     - name: Create Pull Request without conflicts
       if: ${{ env.MERGE_CONFLICTS == 'no' && env.MERGE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7

doc/src/SUMMARY.md

@@ -36,4 +36,6 @@
   - [20: Verify the safety of char-related functions in str::pattern](./challenges/0020-str-pattern-pt1.md)
   - [21: Verify the safety of substring-related functions in str::pattern](./challenges/0021-str-pattern-pt2.md)
   - [22: Verify the safety of str iter functions](./challenges/0022-str-iter.md)
+  - [23: Verify the safety of Vec functions part 1](./challenges/0023-vec-pt1.md)
+  - [24: Verify the safety of Vec functions part 2](./challenges/0024-vec-pt2.md)
   - [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md)

doc/src/challenges/0023-vec-pt1.md

@@ -0,0 +1,78 @@
+# Challenge 23: Verify the safety of `Vec` functions part 1
+
+- **Status:** Open
+- **Tracking Issue:** [#284](https://github.com/model-checking/verify-rust-std/issues/284)
+- **Start date:** *2025-03-07*
+- **End date:** *2025-10-17*
+- **Reward:** *15000 USD*
+
+-------------------
+
+
+## Goal
+
+Verify the safety of `std::Vec` functions (library/alloc/src/vec/mod.rs).
+
+
+### Success Criteria
+
+Verify the safety of the following public functions in (library/alloc/src/vec/mod.rs):
+
+| Function |
+|---------|
+|from_raw_parts| 
+|from_nonnull|
+|from_nonnull_in|
+|into_raw_parts_with_alloc|
+|into_boxed_slice|
+|truncate|
+|set_len|
+|swap_remove|
+|insert|
+|remove|
+|retain_mut|
+|dedup_by|
+|push|
+|push_within_capacity|
+|pop|
+|append|
+|append_elements|
+|drain|
+|clear|
+|split_off|
+|leak|
+|spare_capacity_mut|
+|split_at_spare_mut|
+|split_at_spare_mut_with_len|
+|extend_from_within|
+|into_flattened|
+|extend_with|
+|spec_extend_from_within|
+|deref|
+|deref_mut|
+|into_iter|
+|extend_desugared|
+|extend_trusted|
+|extract_if|
+|drop|
+|try_from|
+
+
+
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must hold for generic type `T` (no monomorphization).
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.

doc/src/challenges/0024-vec-pt2.md

@@ -0,0 +1,67 @@
+# Challenge 24: Verify the safety of `Vec` functions part 2
+
+- **Status:** Open
+- **Tracking Issue:** [#285](https://github.com/model-checking/verify-rust-std/issues/285)
+- **Start date:** *2025/03/07*
+- **End date:** *2025/10/17*
+- **Reward:** *15000 USD*
+
+-------------------
+
+
+## Goal
+
+Continue from part 1 (Challenge 23), for this challenge, you need to verify the safety of `std::Vec` iterator functions in other files in (library/alloc/src/vec/).
+
+
+### Success Criteria
+
+Verify the safety of the following functions that in implemented for `IntoIter` in (library/alloc/src/vec/into_iter.rs):
+
+| Function |
+|---------|
+|as_slice|
+|as_mut_slice|
+|forget_allocation_drop_remaining|
+|into_vecdeque|
+|next|
+|size_hint|
+|advance_by|
+|next_chunk|
+|fold|
+|try_fold|
+|__iterator_get_unchecked|
+|next_back|
+|advance_back_by|
+|drop|
+
+and the following functions from other files: 
+
+| Function | in File|
+|---------|---------|
+|next| extract_if.rs|
+|spec_extend (for IntoIter) | spec_extend.rs |
+|spec_extend (for slice::Iter) | spec_extend.rs |
+|from_elem (for i8)| spec_from_elem.rs |
+|from_elem (for u8)| spec_from_elem.rs |
+|from_elem (for ())| spec_from_elem.rs |
+|from_iter| spec_from_iter.rs|
+|from_iter (default)| spec_from_iter_nested.rs|
+
+
+The verification must be unbounded---it must hold for slices of arbitrary length.
+
+The verification must hold for generic type `T` (no monomorphization).
+
+### List of UBs
+
+All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md):
+
+* Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer.
+* Reading from uninitialized memory except for padding or unions.
+* Mutating immutable bytes.
+* Producing an invalid value
+
+
+Note: All solutions to verification challenges need to satisfy the criteria established in the [challenge book](../general-rules.md)
+in addition to the ones listed above.