From b9e3e44f6d49e7a922f36d6377bca9e33200fd18 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@users.noreply.github.com>
Date: Mon, 2 Dec 2024 10:49:53 -0500
Subject: [PATCH] Add a workflow that runs Verus on each task (#25)

---
 .github/workflows/verus.yml | 52 +++++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 .github/workflows/verus.yml

diff --git a/.github/workflows/verus.yml b/.github/workflows/verus.yml
new file mode 100644
index 0000000..5efc68b
--- /dev/null
+++ b/.github/workflows/verus.yml
@@ -0,0 +1,52 @@
+name: verus
+
+on: [pull_request, workflow_dispatch]
+
+jobs:
+  verus:
+    runs-on: ubuntu-latest
+    steps:
+      - name: checkout
+        uses: actions/checkout@v4
+
+      - name: Install toolchain dependencies
+        shell: bash
+        run: |
+          curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --profile minimal --default-toolchain none -y
+          echo "${CARGO_HOME:-$HOME/.cargo}/bin" >> $GITHUB_PATH
+
+      - name: Install Rust toolchain
+        run: |
+          rustup update --no-self-update stable
+          rustup install 1.79.0-x86_64-unknown-linux-gnu
+
+      - name: Get the URL for the latest Verus release
+        id: verus-release-info
+        run: |
+          jq --version
+          echo "VERUS_URL=$(curl -s https://api.github.com/repos/verus-lang/verus/releases | jq -r '.[].assets[].browser_download_url' | grep x86-linux -)" >> $GITHUB_OUTPUT
+
+      - name: Download the latest Verus release
+        run: |
+          curl --proto '=https' --tlsv1.2 -LsSf ${{ steps.verus-release-info.outputs.VERUS_URL }} -o verus.zip; unzip verus.zip
+
+      - name: run Verus
+        working-directory: ./tasks
+        run: |
+          # Run `verus` on each file, collecting failures if any
+          ANYFAILED=""
+          for i in *.rs; do
+            echo -n "[verus] $i: "
+            if ../verus-x86-linux/verus "$i" >/dev/null 2>/dev/null; then
+              echo "success"
+            else 
+              echo "failed"
+              # Re-run `verus` on any failure just to display the actual output
+              ../verus-x86-linux/verus "$i" || true
+              ANYFAILED="$ANYFAILED $i"
+            fi
+          done
+          if [ -n "$ANYFAILED" ]; then
+            echo "Failed:$ANYFAILED"
+            exit 1
+          fi