Add Verus CI job (closes #7)

.github/workflows/ci.yml

@@ -23,6 +23,11 @@ env:
   # resolve under actions/checkout's default shallow strategy.
   RELAY_REF: 178ffd479ad863c91ece4f580379a9207c36a530
   RIVET_REF: 78f001e23d595ba816f7a7be59282194dedfdc12
+  # Pinned rules_wasm_component for Bazel-running jobs (verus, future
+  # bazel build //...). wohl's MODULE.bazel uses local_path_override
+  # for local dev; CI checks out the pinned ref into a sibling path so
+  # the override resolves.
+  RULES_WASM_COMPONENT_REF: fbe20571eee9bd05687c95e7a43f6c236d9b2428
 
 jobs:
   lint:
@@ -182,3 +187,30 @@ jobs:
       - name: rivet validate
         working-directory: wohl
         run: rivet validate
+
+  verus:
+    name: Verus (bazel test //proofs/verus)
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          path: wohl
+      - uses: actions/checkout@v4
+        with:
+          repository: pulseengine/rules_wasm_component
+          path: rules_wasm_component
+          ref: ${{ env.RULES_WASM_COMPONENT_REF }}
+          fetch-depth: 0
+      # rules_rocq_rust's module extension eagerly creates a
+      # nixpkgs-backed rocq_toolchains repo at Bazel analysis time,
+      # so every Bazel job needs nix-build on PATH (see MODULE.bazel
+      # comment). Pinned to cachix/install-nix-action v31.10.6.
+      - uses: cachix/install-nix-action@8aa03977d8d733052d78f4e008a241fd1dbf36b3
+      - uses: bazel-contrib/setup-bazel@0.15.0
+        with:
+          bazelisk-cache: true
+          disk-cache: ${{ github.workflow }}-verus
+          repository-cache: true
+      - name: bazel test //proofs/verus:alert_dedup_verify
+        working-directory: wohl
+        run: bazel test //proofs/verus:alert_dedup_verify --test_output=summary

MODULE.bazel

@@ -39,6 +39,28 @@ git_override(
     commit = "e4660cc1b06fc4c0aefb49401fa2e2184cf804e3",
 )
 
+# rules_rocq_rust's module extension unconditionally creates the
+# rocq_toolchains repo via a nixpkgs package, even before any rocq rule
+# is loaded. That requires `nix-build` on PATH (local dev: install nix;
+# CI: see the install step in the verus job). The nixpkgs commit below
+# mirrors rivet — keep them in lock-step until we have a reason to
+# diverge.
+bazel_dep(name = "rules_nixpkgs_core", version = "0.13.0")
+
+nix_repo = use_extension(
+    "@rules_nixpkgs_core//extensions:repository.bzl",
+    "nix_repo",
+)
+nix_repo.github(
+    name = "nixpkgs",
+    org = "NixOS",
+    repo = "nixpkgs",
+    # nixos-unstable with Rocq 9.0.1 (matches pulseengine/rivet's pin).
+    commit = "aca4d95fce4914b3892661bcb80b8087293536c6",
+    sha256 = "",
+)
+use_repo(nix_repo, "nixpkgs")
+
 local_path_override(
     module_name = "rules_wasm_component",
     path = "../rules_wasm_component",