Add Verus CI job (closes #7)#19
Merged
Merged
Conversation
avrabe
added a commit
that referenced
this pull request
May 23, 2026
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) <noreply@anthropic.com>
This was referenced May 23, 2026
avrabe
added a commit
that referenced
this pull request
May 23, 2026
rules_rocq_rust (added in #17) calls rust_toolchain with `channel`, `iso_date`, and `version` attributes — newer-rules_rust APIs that wohl's pinned rules_rust commit (6281d27 via git_override) does not have. This blocks PR #19's Verus CI job at toolchain resolution. Match relay's pin: - bazel_dep rules_rust 0.61.0 -> 0.70.0 (from BCR) - drop the git_override to 6281d27 — that commit is now an ancestor of 0.70.0; the override was the old workaround for a Bazel API break that 0.61.0 had inherited (relay's MODULE.bazel comment documents this). - bazel_dep rules_wasm_component 0.1.0 -> 1.0.0 — rules_wasm_ component 1.0.0 also targets rules_rust 0.70.0; keep the local_ path_override so active rules_wasm_component dev still works. Validation - `bazel mod show_repo @rules_rust` resolves 0.70.0 from BCR cleanly. - `bazel mod show_repo @rules_wasm_component` resolves via the local override. - Existing CI (lint/test/kani/fuzz/rivet-validate) is cargo-based and does not exercise the bazel rules — so this PR's CI passes "trivially". The real bazel-side validation comes via PR #19's Verus job once rebased onto this. A future bazel build //:all CI job (tracked in #14 / #8) will be the standing gate for any rules_wasm_component API ripple through wohl's WASM components. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
May 24, 2026
Matches relay's pin. Drops the rules_rust git_override (commit 6281d27 is now an ancestor of 0.70.0). Unblocks rules_rocq_rust + the Verus CI job in #19, which calls rust_toolchain with channel/iso_date/version attrs that the old pin lacked.
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) <noreply@anthropic.com>
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) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Wires the Verus deductive-proof gate into CI. The Bazel target
//proofs/verus:alert_dedup_verifywas landed in Phase 2 Track D (#12); this PR adds the corresponding workflow job, completing the Verus CI loop.Closes #7.
What the job does
wohl(path: wohl).pulseengine/rules_wasm_componentat a pinned SHA (newRULES_WASM_COMPONENT_REFenv var,fbe2057).wohl/MODULE.bazeluseslocal_path_overrideforrules_wasm_componentso 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.bazel-contrib/setup-bazel@0.15.0withbazelisk-cache,disk-cache, andrepository-cacheenabled — keeps the Verus toolchain (~26 MB) and Bazel state cached across runs.bazel test //proofs/verus:alert_dedup_verify --test_output=summary.rules_verus's hermetic toolchain handles the Verus binary download via the pinned0.2026.02.15toolchain inMODULE.bazel— no manual install on the runner.Why bazel-contrib/setup-bazel
It's the maintained successor to
bazelbuild/setup-bazelisk, supports cache configuration directly, and is widely used in the Bazel community.Pairs with
RULES_WASM_COMPONENT_REFis now an explicit PR, same model asRELAY_REF/RIVET_REF..bazelignore) — orthogonal but related: would have been a hard blocker if anybazel build //...job traversed into.claude/worktrees/. This Verus job uses a specific target so it doesn't traverse, but the.bazelignoreis good hygiene for the next bazel job (the WASM-build job from WASM component build hygiene: no .bazelignore + wasm_component.rs escapes the CI lint gate #14).🤖 Generated with Claude Code