Add CI workflow, README, and align CLAUDE.md with Kani-BMC reality#6
Merged
Conversation
Foundation PR 1b of the Phase 1 effort. Closes #1. CI workflow (.github/workflows/ci.yml) - jobs: lint (fmt + clippy -D warnings), test (workspace), kani (all 6 components), fuzz-smoke (60s per target on nightly), rivet-validate - cross-repo checkout for relay + rivet siblings (path = "../relay/..." and path = "../rivet/...") - Rust 1.85.0 stable, edition 2024; rust-cache + dedicated Kani cache - Concurrency group cancels in-progress runs on same ref Root README.md - tagline, components table, architecture summary, build instructions, verification status table, CI badge, links to PulseEngine/Relay/Rivet - License section notes Apache-2.0 SPDX in Cargo.toml; root LICENSE file pending separately CLAUDE.md drift fix - Was: "Verified core logic in src/core.rs (Verus-annotated)" — wrong path AND wrong verification tool - Now: "crates/wohl-*/plain/src/lib.rs (Kani BMC harnesses on engine.rs)" - Removed bazel test //:verus (not active), replaced with the cargo kani / cargo test / cargo fuzz / rivet validate commands that actually work - Verus mentioned as planned for wohl-alert dispatcher dedup invariant After this PR merges: - main branch protection can require CI green (currently only PR-required) - Phase 2 tracks (B: STM32G0 + door firmware, C: OTA core, D: Verus + fuzz deepening) start in parallel Verification (local, macOS-aarch64) - cargo fmt --all --check: clean - cargo clippy --workspace --all-targets -- -D warnings: clean - cargo test --workspace: 92/92 pass - YAML parse: OK Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
9 tasks
Round 2 of reviewer feedback on PR #6. Architect-flagged blockers - README.md Rivet validation status: was "0 errors / 20 warnings" — the 20 was lifecycle-gap count, actual warning count is 5. Fixed to "PASS, 5 warnings". (rivet validate confirms.) - CLAUDE.md / README.md said "Verus planned (separate tracking issue)" but no such issue existed. Filed issue #7 (Track D Verus on wohl-alert) and linked both files to it. - README "Build" section removed the `bazel build //...` line since CI does not exercise it; the bazel path is tracked for follow-up in #8. Bonus: root LICENSE file - Apache-2.0, matches sibling repo (relay) verbatim, including "Copyright 2026 pulseengine contributors" attribution. - README License section updated to reference LICENSE file. CI follow-ups (architect non-blocking, deferred) - Filed issue #8 for: Kani matrix split, pinned relay/rivet refs, cargo-deny job, bazel build job, nightly long-fuzz, fuzz coverage for the other 4 components, Kani cache key tightening, declaring required vs advisory jobs. No behavior change. cargo fmt + clippy + test still pass. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
User feedback: "dont add any numbers in the readme, they will be in the
next round again false." The previous revision had "PASS (20 harnesses)"
and "PASS, 5 warnings" — both will drift the moment a harness is added
or rivet validate is re-run.
Changes:
- Verification table: replace specific counts with "gated by CI" /
"active in spar/" / "planned" — status words that don't drift.
- Toolchain section: link to Cargo.toml's rust-version rather than
restating "1.85.0" (which would drift when Cargo.toml bumps).
- Links section: remove "this PR closes" qualifier on #1 since the PR
now refs rather than closes it (nightly long-fuzz remaining).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Architect re-reviewer caught this: `cargo fmt --all --check` reaches into local path-dependencies (relay/, rivet/ siblings) and inherits their fmt drift. The lint job would have gone red on first push even though every wohl crate is formatted correctly. Switch to a per-package loop over the 8 workspace members. Locally: before: cargo fmt --all --check → exit 1 (relay diff) after: cargo fmt -p <each> --check → exit 0 for all 8 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
Foundation PR 1b of the Phase 1 effort. Partial completion of #1 — nightly long-fuzz + fuzz coverage for the other 4 components are tracked in #8 (per architect-reviewer recommendation).
Lands four things that turn the cleaned-up baseline (#2) into a real ASPICE-grade merge gate:
.github/workflows/ci.yml— actual CI on every PR and main pushREADME.md— public-facing project description with CI badgeCLAUDE.mddrift fix — replaces stale Verus claims with current Kani-BMC realityLICENSE(Apache-2.0) — matches sibling repo (relay) patternCI workflow
lintcargo fmt -p $c --checkfor each workspace member +cargo clippy --workspace --all-targets -- -D warningstestcargo test --workspace --all-features(covers proptest)kanicargo kani -p $cratefor all monitors (serial loop; matrix split tracked in #8)fuzz-smokecargo fuzz runwith-max_total_time=60on nightly toolchainrivet-validaterivet validateagainstartifacts/*Why per-crate fmt:
cargo fmt --allreaches into local path-dependencies and would inherit drift inrelay//rivet/siblings. The per-package loop scopes the gate to this workspace's 8 members.Cross-repo checkout:
relayandrivetare checked out as siblings (matching the localpath = "../relay/..."layout). Currently pins to theirmainbranches — pinning to SHAs is tracked in #8.Caching:
Swatinem/rust-cache@v2per-job, plus a dedicatedactions/cache@v4for the Kani install.Reviewer feedback addressed (round 1 → 2 → 3)
Closes #1would auto-close while nightly-long-fuzz unmetcargo fmt --allreaches into../relay/and would fail CIc8e9f67); locally exit 0 across all 8 membersCLAUDE.md drift fix
Replaces stale paths and Verus claims with current Kani-BMC reality. Links to issue #7 for the planned Verus work on
wohl-alert.Local verification
cargo fmt -p $c --check× 8cargo clippy --workspace --all-targets -- -D warningscargo test --workspace --all-featuresrivet validateCI runs the full matrix end-to-end on this PR.
After this PR merges
main: require CI green (PR-only is already on)lint,test,kani,rivet-validaterequired;fuzz-smokeadvisory — tracked in CI follow-ups: matrix split, pinned siblings, cargo-deny, bazel build, nightly long-fuzz #8)crates/wohl-ota/no_std core with Kani harnesseswohl-alert(#7) + CI hygiene (#8)🤖 Generated with Claude Code