From f25fd50ddc1167dea2921123f89139c5caf87b9c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 23 May 2026 13:22:38 +0200 Subject: [PATCH 1/2] Add Verus CI job (bazel test //proofs/verus:alert_dedup_verify) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Wires the Verus deductive-proof gate into CI. The bazel target was landed in Phase 2 Track D (#12 / SWARCH-WOHL-006's verification chain); this PR adds the corresponding workflow job, completing the Verus CI loop and closing issue #7. What the job does - Checks out wohl (path: wohl). - Checks out pulseengine/rules_wasm_component at a pinned SHA (new env var RULES_WASM_COMPONENT_REF). wohl's MODULE.bazel uses local_path_override for rules_wasm_component so local dev iterates against a sibling checkout; CI provides the same sibling layout from a pinned commit so module resolution succeeds without breaking the local-dev pattern. - Sets up Bazelisk via bazel-contrib/setup-bazel@0.15.0 with bazelisk-cache, disk-cache, and repository-cache enabled — keeps the Verus toolchain (~26 MB) and Bazel state cached across runs. - Runs `bazel test //proofs/verus:alert_dedup_verify`. rules_verus's hermetic toolchain handles the Verus binary download via the pinned 0.2026.02.15 toolchain in MODULE.bazel — no manual install. Closes #7. Pairs with #17 (sibling pinning) — this is the first CI job that actually runs Bazel; the pinning makes its behavior deterministic. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/workflows/ci.yml | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6c93a7c..7a56472 100644 --- a/.github/workflows/ci.yml +++ b/.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,25 @@ 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 + - 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 From 18f5059afb46c0699d54ca58b2aca33077bf69fc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 23 May 2026 14:21:20 +0200 Subject: [PATCH 2/2] Verus CI: install Nix + mirror rivet's nix_repo pin MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR #19's first CI run failed because rules_rocq_rust (added in #17) unconditionally creates a nixpkgs-backed `rocq_toolchains` repo at Bazel module-resolution time — that needs `nix-build` on PATH, even though no rocq rule is actually loaded by //proofs/verus. Per the architect's direction ("install Nix in CI, but pin"): - MODULE.bazel: add rules_nixpkgs_core (0.13.0) + nix_repo.github pinned to NixOS/nixpkgs commit aca4d95 (matches rivet's pin exactly — keep wohl and rivet in lock-step on the nixpkgs ref until there is a reason to diverge). Without nix_repo, rules_ rocq_rust falls back to behavior that varies by tool version. - ci.yml (verus job): add cachix/install-nix-action pinned to SHA 8aa03977 (v31.10.6) BEFORE the setup-bazel step. Pinning by SHA, not tag — tags can move; SHAs cannot. Local devs need nix installed for `bazel test //proofs/verus:...` too (a side-effect of #17's rules_rocq_rust addition). Mac: `brew install nix`; Linux: official installer or distro package. Co-Authored-By: Claude Opus 4.7 (1M context) --- .github/workflows/ci.yml | 5 +++++ MODULE.bazel | 22 ++++++++++++++++++++++ MODULE.bazel.lock | 12 +++++++----- 3 files changed, 34 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7a56472..ad4274b 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -201,6 +201,11 @@ jobs: 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 diff --git a/MODULE.bazel b/MODULE.bazel index dcf9ebe..4b8582b 100644 --- a/MODULE.bazel +++ b/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", diff --git a/MODULE.bazel.lock b/MODULE.bazel.lock index 5f665ee..46abca8 100644 --- a/MODULE.bazel.lock +++ b/MODULE.bazel.lock @@ -339,7 +339,7 @@ "@@rules_nixpkgs_core+//extensions:repository.bzl%nix_repo": { "general": { "bzlTransitiveDigest": "dTTtWNdwe7E4j77oKh1mHI1qtdxfaVSGSZa1oPf2QjU=", - "usagesDigest": "ZjI2xoiQBaRz3qc721Gc+tXJ9FrSWkJDOJeEXWOvz4Q=", + "usagesDigest": "+xvGwqDhVmiuZ2ymH5G9SDGZMpTkU5ccxmwXBQjvdtY=", "recordedInputs": [ "REPO_MAPPING:rules_nixpkgs_core+,bazel_skylib bazel_skylib+" ], @@ -348,15 +348,17 @@ "repoRuleId": "@@rules_nixpkgs_core+//:nixpkgs.bzl%_nixpkgs_http_repository", "attributes": { "unmangled_name": "nixpkgs", - "url": "https://github.com/NixOS/nixpkgs/archive/refs/tags/24.05.tar.gz", - "strip_prefix": "nixpkgs-24.05", + "url": "https://github.com/NixOS/nixpkgs/archive/aca4d95fce4914b3892661bcb80b8087293536c6.tar.gz", + "strip_prefix": "nixpkgs-aca4d95fce4914b3892661bcb80b8087293536c6", "integrity": "", - "sha256": "911314b81780f26fdaf87e17174210bdbd40c86bac1795212f257cdc236a1e78" + "sha256": "" } } }, "moduleExtensionMetadata": { - "explicitRootModuleDirectDeps": [], + "explicitRootModuleDirectDeps": [ + "nixpkgs" + ], "explicitRootModuleDirectDevDeps": [], "useAllRepos": "NO", "reproducible": false