Add Rust tests and Kani workflow (#9)

Create two new workflows:
  - Rust Tests: Run the Rust repository tests for the standard library.
- Kani: Run `kani verify-std` to verify the standard library. Note that
we don't have any harness yet to verify.

.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:
@@ -27,8 +29,9 @@ jobs:
           cargo install mdbook --version "^0.4" --locked
           echo "${HOME}/.cargo/bin" >> $GITHUB_PATH
 
+      # Removed --locked for now since it is broken due to old proc_macro feature.
       - name: Install linkchecker
-        run: cargo install mdbook-linkcheck --version "^0.7" --locked
+        run: cargo install mdbook-linkcheck --version "^0.7"
 
       - name: Build Documentation
         run: mdbook build doc

.github/workflows/kani.yml

@@ -0,0 +1,56 @@
+# 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: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Kani does not support windows.
+        os: [ubuntu-latest, macos-latest]
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          path: verify-rust-std
+          submodules: true
+
+      # 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
+          ref: 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

@@ -0,0 +1,66 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This workflow is responsible for building the standard library using the bootstrap script
+# and executing the Rust regression.
+
+name: Rust Tests
+on:
+  workflow_dispatch:
+  pull_request:
+    paths:
+      - 'library/**'
+      - 'rust-toolchain.toml'
+      - '.github/workflows/rustc.yml'
+  push:
+    paths:
+      - 'library/**'
+      - 'rust-toolchain.toml'
+      - '.github/workflows/rustc.yml'
+
+defaults:
+  run:
+    shell: bash
+
+jobs:
+  build:
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        # Note windows-latest is currently failing.
+        os: [ubuntu-latest, macos-latest]
+    steps:
+      - name: Checkout Library
+        uses: actions/checkout@v4
+        with:
+          path: head
+
+      - name: Checkout `upstream/master`
+        uses: actions/checkout@v4
+        with:
+          repository: rust-lang/rust
+          path: upstream
+          fetch-depth: 0
+          submodules: true
+
+      # Run rustc twice in case the toolchain needs to be installed.
+      # Retrieve the commit id from the `rustc --version`. Output looks like:
+      # `rustc 1.80.0-nightly (84b40fc90 2024-05-27)`
+      - name: Checkout matching commit
+        run: |
+          cd head
+          rustc --version
+          COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/")
+          cd ../upstream
+          git checkout ${COMMIT_ID}
+
+      - name: Copy Library
+        run: |
+          rm -rf upstream/library
+          cp -r head/library upstream
+
+      - name: Run tests
+        working-directory: upstream
+        run: |
+          ./configure --set=llvm.download-ci-llvm=true
+          ./x test --stage 0 library/std

rust-toolchain.toml

@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# This version should be updated whenever we update the version of the Rust
+# standard library we currently track.
+
+[toolchain]
+channel = "nightly-2024-05-23"
+components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]