Add Kani regression

.github/workflows/book.yml

@@ -11,9 +11,11 @@ on:
   pull_request:
     paths:
       - 'doc/**'
+      - '.github/workflows/book.yml'
   push:
     paths:
       - 'doc/**'
+      - '.github/workflows/book.yml'
 
 jobs:
   build:

.github/workflows/kani.yml

@@ -0,0 +1,51 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This workflow is responsible for verifying the standard library with Kani.
+
+name: Kani
+on:
+  workflow_dispatch:
+  pull_request:
+    paths:
+      - 'library/**'
+      - '.github/workflows/kani.yml'
+  push:
+    paths:
+      - 'library/**'
+      - '.github/workflows/kani.yml'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          path: verify-rust-std
+
+      # We currently build Kani from a branch that tracks a rustc version compatible with this library version.
+      - name: Checkout `Kani`
+        uses: actions/checkout@v4
+        with:
+          repository: model-checking/kani
+          path: kani
+          branch: features/verify-rust-std
+
+      - name: Build `Kani`
+        working-directory: kani
+        run: |
+          cargo build-dev --release
+          echo "$(pwd)/scripts" >> $GITHUB_PATH
+
+      - name: Run tests
+        working-directory: verify-rust-std
+        env:
+          RUST_BACKTRACE: 1
+        run: |
+          kani verify-std -Z unstable-options ./library --target-dir "target"
+          

.github/workflows/rustc.yml

@@ -4,7 +4,7 @@
 # This workflow is responsible for building the standard library using the bootstrap script
 # and executing the Rust regression.
 
-name: Check Rust bootstrap
+name: Rust Tests
 on:
   workflow_dispatch:
   pull_request: