From 70bd0215da3183db04796c93f070d805cc93343b Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 26 Jul 2024 11:04:59 -0700
Subject: [PATCH] Add two new CI workflows to check Kani against
 `verify-rust-std` (#3386)

This PR adds the following workflows:
1. `verify-std-check`: This workflow will run either in a PR or via
workflow call. It pulls the `main` branch of `verify-rust-std`
repository, and see if it can verify the repo with the new Kani version
from HEAD.
   - If verification succeeds, the workflow will succeed.
   - If the verification fails and this is a PR, the workflow will compare
the verification result against the base of the PR. The workflow will
succeed if the results match*.
2. `verify-std-update`: This workflow will run the `verify-std-check`
workflow. If it succeeds, it will update the `verify-rust-std` branch
from HEAD. This workflow will fail if `features/verify-rust-std` branch
diverges, and a merge is required.

The motivation for this PR is to help us identify any changes to Kani
that may break the Rust verification repository, and to keep the
`verify-rust-std` up to date as much as possible.

* The fallback logic is needed since toolchain upgrades can potentially
break the std verification. This will happen in cases where the new
toolchain version is incompatible with the library version from the
`verify-rust-std`. Those cases should not interfere with Kani
development, and they should be fixed when we update the
`verify-rust-std` repo.
---
 .github/workflows/verify-std-check.yml  | 86 +++++++++++++++++++++++++
 .github/workflows/verify-std-update.yml | 35 ++++++++++
 2 files changed, 121 insertions(+)
 create mode 100644 .github/workflows/verify-std-check.yml
 create mode 100644 .github/workflows/verify-std-update.yml

diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml
new file mode 100644
index 000000000000..667be6b340c5
--- /dev/null
+++ b/.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
+
diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml
new file mode 100644
index 000000000000..518f80ecd1b8
--- /dev/null
+++ b/.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
+