From ba652d9d400c7e368bb7ded0d4e78250001dbdb3 Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jaybosamiya@gmail.com>
Date: Tue, 14 May 2024 11:45:57 -0400
Subject: [PATCH] Add CI

---
 .github/workflows/ci.yml | 41 ++++++++++++++++++++++++++++++++++++++++
 tools/ci-build-verus.sh  | 12 ++++++++++++
 tools/ci-setup-verus.sh  | 13 +++++++++++++
 3 files changed, 66 insertions(+)
 create mode 100644 .github/workflows/ci.yml
 create mode 100755 tools/ci-build-verus.sh
 create mode 100755 tools/ci-setup-verus.sh

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000..6c6b5f4
--- /dev/null
+++ b/.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
diff --git a/tools/ci-build-verus.sh b/tools/ci-build-verus.sh
new file mode 100755
index 0000000..b2decb3
--- /dev/null
+++ b/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"
diff --git a/tools/ci-setup-verus.sh b/tools/ci-setup-verus.sh
new file mode 100755
index 0000000..77adcba
--- /dev/null
+++ b/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)"