Merge branch 'main' into int-mut-tests

.github/workflows/verify-std-check.yml

@@ -0,0 +1,86 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to build and run the `verify-rust-std` repository.
+#
+# This check should be optional, but it has been added to help provide
+# visibility to when a PR may break the `verify-rust-std` repository.
+#
+# We expect toolchain updates to potentially break this workflow in cases where
+# the version tracked in the `verify-rust-std` is not compatible with newer
+# versions of the Rust toolchain.
+#
+# Changes unrelated to the toolchain should match the current status of main.
+
+name: Check Std Verification
+on:
+  pull_request:
+  workflow_call:
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  verify-std:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Kani does not support windows.
+        os: [ ubuntu-22.04, macos-14 ]
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          repository: model-checking/verify-rust-std
+          path: verify-rust-std
+          submodules: true
+
+      - name: Checkout `Kani`
+        uses: actions/checkout@v4
+        with:
+          path: kani
+
+      - name: Setup Kani Dependencies
+        uses: ./kani/.github/actions/setup
+        with:
+          os: ${{ matrix.os }}
+          kani_dir: kani
+
+      - name: Build Kani
+        working-directory: kani
+        run: |
+          cargo build-dev
+          echo "$(pwd)/scripts" >> $GITHUB_PATH
+
+      - name: Run verification with HEAD
+        id: check-head
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      # If the head failed, check if it's a new failure.
+      - name: Checkout base
+        working-directory: kani
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        run: |
+          BASE_REF=${{ github.event.pull_request.base.sha }}
+          git checkout ${BASE_REF}
+          cargo build-dev
+
+      - name: Run verification with BASE
+        id: check-base
+        if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request'
+        working-directory: verify-rust-std
+        continue-on-error: true
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
+            -Z mem-predicates -Z ptr-to-ref-cast-checks
+
+      - name: Compare PR results
+        if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output
+        run: |
+          echo "New failure introduced by this change"
+          exit 1
+

.github/workflows/verify-std-update.yml

@@ -0,0 +1,35 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+#
+# This workflow will try to update the verify std branch.
+
+name: Update "features/verify-rust-std"
+on:
+  schedule:
+    - cron: "30 3 * * *" # Run this every day at 03:30 UTC
+  workflow_dispatch:     # Allow manual dispatching.
+
+env:
+  RUST_BACKTRACE: 1
+
+jobs:
+  # First ensure the HEAD is compatible with the `verify-rust-std` repository.
+  verify-std:
+    name: Verify Std
+    permissions: { }
+    uses: ./.github/workflows/verify-std-check.yml
+
+  # Push changes to the features branch.
+  update-branch:
+    needs: verify-std
+    permissions:
+      contents: write
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Kani
+        uses: actions/checkout@v4
+
+      - name: Update feature branch
+        run: |
+          git push origin HEAD:features/verify-rust-std
+