Merge branch 'main' into rawvecchallenge

Author: tautschnig

.github/workflows/kani-metrics.yml

@@ -26,7 +26,9 @@ jobs:
         python-version: '3.x'
 
     - name: Compute Kani Metrics
-      run: ./scripts/run-kani.sh --run metrics --path ${{github.workspace}}
+      run: |
+        ./scripts/run-kani.sh --run metrics --with-autoharness --path ${{github.workspace}}
+        rm kani-list.json
 
     - name: Create Pull Request
       uses: peter-evans/create-pull-request@v7

.github/workflows/kani.yml

@@ -53,6 +53,193 @@ jobs:
       - name: Run Kani Verification
         run: head/scripts/run-kani.sh --path ${{github.workspace}}/head
 
+  kani_autoharness:
+    name: Verify std library using autoharness
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run Kani autoharness on the std library for selected functions.
+      # Uses "--include-pattern" to make sure we do not try to run across all
+      # possible functions as that may take a lot longer than expected. Instead,
+      # explicitly list all functions (or prefixes thereof) the proofs of which
+      # are known to pass.
+      - name: Run Kani Verification
+        run: |
+          scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern alloc::layout::Layout::from_size_align \
+            --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
+            --include-pattern char::convert::from_u32_unchecked \
+            --include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<isize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u8>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u16>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u32>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u64>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<u128>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<usize>::count_ones" \
+            --include-pattern "num::nonzero::NonZero::<i8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<i128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<isize>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u8>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u16>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u32>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u64>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<u128>::rotate_" \
+            --include-pattern "num::nonzero::NonZero::<usize>::rotate_" \
+            --include-pattern ptr::align_offset::mod_inv \
+            --include-pattern ptr::alignment::Alignment::as_nonzero \
+            --include-pattern ptr::alignment::Alignment::as_usize \
+            --include-pattern ptr::alignment::Alignment::log2 \
+            --include-pattern ptr::alignment::Alignment::mask \
+            --include-pattern ptr::alignment::Alignment::new \
+            --include-pattern ptr::alignment::Alignment::new_unchecked \
+            --include-pattern time::Duration::from_micros \
+            --include-pattern time::Duration::from_millis \
+            --include-pattern time::Duration::from_nanos \
+            --include-pattern time::Duration::from_secs \
+            --exclude-pattern time::Duration::from_secs_f \
+            --include-pattern unicode::unicode_data::conversions::to_ \
+            --exclude-pattern ::precondition_check \
+            --harness-timeout 10m \
+            --default-unwind 1000 \
+            --jobs=3 --output-format=terse | tee autoharness-verification.log
+          gzip autoharness-verification.log
+
+      - name: Upload Autoharness Verification Log
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+          path: autoharness-verification.log.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run_kani_metrics:
+    name: Kani Metrics
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: true
+
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # The Kani metrics collection uses a Python script (kani_std_analysis.py), so make sure Python is installed
+      - name: Set up Python
+        uses: actions/setup-python@v4
+        with:
+          python-version: '3.x'
+
+      # Step 2: Run list on the std library
+      - name: Run Kani Metrics
+        run: |
+          scripts/run-kani.sh --run metrics --with-autoharness
+          pushd /tmp/std_lib_analysis
+          tar czf results.tar.gz results
+          popd
+
+      - name: Upload kani-list.json
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+          path: kani-list.json
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+      - name: Upload scanner results
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+          path: /tmp/std_lib_analysis/results.tar.gz
+          if-no-files-found: error
+          # Aggressively short retention: we don't really need these
+          retention-days: 3
+
+  run-log-analysis:
+    name: Build JSON from logs
+    needs: [run_kani_metrics, kani_autoharness]
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest, macos-latest]
+        include:
+          - os: ubuntu-latest
+            base: ubuntu
+          - os: macos-latest
+            base: macos
+      fail-fast: false
+
+    steps:
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: false
+
+      - name: Download log
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-autoharness-verification.log.gz
+
+      - name: Download kani-list.json
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-kani-list.json
+
+      - name: Download scanner results
+        uses: actions/download-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.tar.gz
+
+      - name: Run log parser
+        run: |
+          gunzip autoharness-verification.log.gz
+          tar xzf results.tar.gz
+          python3 scripts/kani-std-analysis/log_parser.py \
+            --kani-list-file kani-list.json \
+            --analysis-results-dir results/ \
+            autoharness-verification.log \
+            -o results.json
+
+      - name: Upload JSON
+        uses: actions/upload-artifact@v4
+        with:
+          name: ${{ matrix.os }}-results.json
+          path: results.json
+          if-no-files-found: error
+
   run-kani-list:
     name: Kani List
     runs-on: ubuntu-latest
@@ -66,8 +253,14 @@ jobs:
 
       # Step 2: Run list on the std library
       - name: Run Kani List
-        run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head
-      
+        run: |
+          head/scripts/run-kani.sh --run list --with-autoharness --path ${{github.workspace}}/head
+          # remove duplicate white space to reduce file size (GitHub permits at
+          # most one 1MB)
+          ls -l ${{github.workspace}}/head/kani-list.md
+          perl -p -i -e 's/ +/ /g' ${{github.workspace}}/head/kani-list.md
+          ls -l ${{github.workspace}}/head/kani-list.md
+
       # Step 3: Add output to job summary
       - name: Add Kani List output to job summary
         uses: actions/github-script@v6
@@ -79,3 +272,30 @@ jobs:
               .addHeading('Kani List Output', 2)
               .addRaw(kaniOutput, false)
               .write();
+
+  run-autoharness-analyzer:
+    name: Kani Autoharness Analyzer
+    runs-on: ubuntu-latest
+    steps:
+      # Step 1: Check out the repository
+      - name: Checkout Repository
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+
+      # Step 2: Run autoharness analyzer on the std library
+      - name: Run Autoharness Analyzer
+        run: scripts/run-kani.sh --run autoharness-analyzer
+
+      # Step 3: Add output to job summary
+      - name: Add Autoharness Analyzer output to job summary
+        run: |
+          echo "# Autoharness Failure Summary" >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate core, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/core_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, all functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"
+          echo "## Crate std, unsafe functions" >> "$GITHUB_STEP_SUMMARY"
+          cat autoharness_analyzer/std_unsafe_autoharness_data.md >> "$GITHUB_STEP_SUMMARY"

.github/workflows/pr_approval.yml

@@ -73,6 +73,21 @@ jobs:
               return;
             }
 
+            // Get the list of changed files
+            const { data: changedFiles } = await github.rest.pulls.listFiles({
+              owner,
+              repo,
+              pull_number,
+            });
+
+            // Check if any files in doc/, library/ or verifast-proofs/ are modified
+            const affectsDocs = changedFiles.some(file => file.filename.startsWith('doc/'));
+            const affectsLibrary = changedFiles.some(file => file.filename.startsWith('library/'));
+            const affectsVerifast = changedFiles.some(file => file.filename.startsWith('verifast-proofs/'));
+            // Require two approvals iff one of the above folders are modified; otherwise, one is sufficient.
+            const requiresTwoApprovals = affectsDocs || affectsLibrary || affectsVerifast;
+            const requiredApprovals = requiresTwoApprovals ? 2 : 1;
+
             // Get all reviews with pagination
             async function getAllReviews() {
               let allReviews = [];
@@ -113,23 +128,27 @@ jobs:
                 .map(review => review.user.login)
             );
 
-            const requiredApprovals = 2;
             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 conclusion = (currentCountfromCommittee >= 2) ? 'success' : 'failure';
+            // Check if we have enough approvals
+            const conclusion = (currentCountfromCommittee >= requiredApprovals) ? 'success' : 'failure';
 
             console.log('PR Approval Status');
+            console.log('Modified folders:');
+            console.log(`- doc/: ${affectsDocs ? 'yes' : 'no'}`);
+            console.log(`- library/: ${affectsLibrary ? 'yes' : 'no'}`);
+            console.log(`- verifast-proofs/: ${affectsVerifast ? 'yes' : 'no'}`);
+            console.log(`Required approvals from committee: ${requiredApprovals}`);
             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 2 approvals from committee members, but it has ${currentCountfromCommittee}`);
+              core.setFailed(`PR needs ${requiredApprovals} approval${requiredApprovals > 1 ? 's' : ''} from committee members, but it has ${currentCountfromCommittee}`);
             } else {
               core.info('PR approval check passed successfully.');
             }

.github/workflows/update-subtree.yml

@@ -126,14 +126,14 @@ jobs:
         UPSTREAM_HEAD=$(git log --format=%H -n 1 rust-filtered/subtree/library)
         if [ "${UPSTREAM_HEAD}" = "${UPSTREAM_FROM}" ]; then
           echo "Nothing to do, ${UPSTREAM_FROM} matches ${UPSTREAM_HEAD} (${SUBTREE_HEAD_MSG})"
-          echo "MERGE_CONFLICTS=noop" >> $GITHUB_ENV
+          echo "SUBTREE_PR_REQUIRED=no" >> $GITHUB_ENV
         else
           git branch --set-upstream-to=origin/subtree/library
-          echo "MERGE_CONFLICTS=maybe" >> $GITHUB_ENV
+          echo "SUBTREE_PR_REQUIRED=yes" >> $GITHUB_ENV
         fi
 
     - name: Create Pull Request to update subtree/library
-      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.SUBTREE_PR_EXISTS == 'no' }}
+      if: ${{ env.SUBTREE_PR_REQUIRED == 'yes' && env.SUBTREE_PR_EXISTS == 'no' }}
       uses: peter-evans/create-pull-request@v7
       with:
         title: 'Update subtree/library to ${{ env.NEXT_TOOLCHAIN_DATE }}'
@@ -151,7 +151,7 @@ jobs:
         path: verify-rust-std
 
     - name: Merge subtree/library changes
-      if: ${{ env.MERGE_CONFLICTS != 'noop' && env.MERGE_PR_EXISTS == 'no' }}
+      if: ${{ env.CURRENT_TOOLCHAIN_DATE != env.NEXT_TOOLCHAIN_DATE && env.MERGE_PR_EXISTS == 'no' }}
       run: |
         cd verify-rust-std
         # create-pull-request resets branches locally, implying that
@@ -160,7 +160,9 @@ jobs:
           git checkout -t -b subtree/library origin/update-subtree/library
         else
           git checkout subtree/library
-          git reset --hard origin/update-subtree/library
+          if [ "${SUBTREE_PR_REQUIRED}" = "yes" ]; then
+            git reset --hard origin/update-subtree/library
+          fi
         fi
         git checkout main
 

.github/workflows/verifast-negative.yml

@@ -42,4 +42,4 @@ jobs:
         run: |
           export PATH=~/verifast-25.02/bin:$PATH
           cd verifast-proofs
-          mysh check-verifast-proofs-negative.mysh
+          bash check-verifast-proofs-negative.sh

.github/workflows/verifast.yml

@@ -39,4 +39,29 @@ jobs:
         run: |
           export PATH=~/verifast-25.02/bin:$PATH
           cd verifast-proofs
-          mysh check-verifast-proofs.mysh
+          bash check-verifast-proofs.sh
+
+  notify-btj:
+    name: Notify @btj
+    runs-on: ubuntu-latest
+    needs: check-verifast-on-std
+    if: failure()
+    permissions:
+      id-token: write
+    
+    steps:
+      - name: Get GitHub OIDC token
+        id: get_token
+        uses: actions/github-script@v7
+        with:
+          script: |
+            const audience = 'notify-bart-jacobs';
+            return await core.getIDToken(audience);
+          result-encoding: string
+
+      - name: Call notification endpoint
+        run: |
+          curl -X POST "https://verify-rust-std-verifast-monitor.bart-jacobs.workers.dev/" \
+            -H "Authorization: Bearer ${{ steps.get_token.outputs.result }}" \
+            -H "Content-Type: application/json" \
+            -d '{}'

doc/src/SUMMARY.md

@@ -31,5 +31,8 @@
   - [15: Contracts and Tests for SIMD Intrinsics](./challenges/0015-intrinsics-simd.md)
   - [16: Verify the safety of Iterator functions](./challenges/0016-iter.md)
   - [17: Verify the safety of slice functions](./challenges/0017-slice.md)
-  - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter-pt1.md)
+  - [18: Verify the safety of slice iter functions](./challenges/0018-slice-iter.md)
   - [19: Safety of `RawVec`](./challenges/0019-rawvec.md)
+  - [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)