Add CI

.github/workflows/ci.yml

@@ -0,0 +1,41 @@
+name: CI
+
+on:
+  push:
+    branches:
+      - main
+  pull_request:
+  workflow_dispatch:
+  schedule:
+    - cron: '0 0 * * 1'  # Run every Monday night at midnight UTC
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build:
+    name: Verify
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+    steps:
+      - uses: actions/checkout@v3
+      - name: Set up Verus
+        run: ./tools/ci-setup-verus.sh
+      - name: Rust cache
+        uses: Swatinem/rust-cache@v2
+        with:
+          workspaces: |
+            ${{ github.workspace }}/verus/source -> target
+            ${{ github.workspace }}/verus/tools/vargo -> target
+          cache-directories: ${{ github.workspace }}/verus/source/target-verus
+      - name: Verus cache
+        uses: actions/cache@v3
+        with:
+          path: ${{ github.workspace }}/verus
+          key: ${{ runner.os }}-verus-${{ hashFiles('verus/.git/refs/heads/main') }}
+      - name: Build Verus
+        run: ./tools/ci-build-verus.sh
+      - name: Verify ironsht
+        run: |
+          verus --crate-type=dylib --expand-errors --time --no-report-long-running ironsht/src/lib.rs

tools/ci-build-verus.sh

@@ -0,0 +1,12 @@
+#!/bin/bash
+
+set -eu
+
+cd verus/source
+if [ -f z3 ]; then echo "Z3 already exists"; else ./tools/get-z3.sh; fi
+# shellcheck disable=SC1091
+source ../tools/activate
+env VERUS_Z3_PATH="$PWD/z3" vargo build --release
+
+# make verus binary accessible
+echo "$PWD/target-verus/release" >>"$GITHUB_PATH"

tools/ci-setup-verus.sh

@@ -0,0 +1,13 @@
+#!/bin/bash
+
+set -e
+
+git clone \
+  --depth 1 \
+  --recurse-submodules --shallow-submodules \
+  https://github.com/verus-lang/verus
+cd verus/source
+# trigger toolchain installation
+rustc --version
+echo "Verus is at $PWD"
+echo "Verus is at git revision: $(git rev-parse HEAD)"