fix(ci): Kani PR-smoke + Mutation shard + Verus log upload#209
Merged
Conversation
Three CI fixes in one workflow PR:
- Kani: split into PR-only --only-codegen smoke (~5 min) and main-only
full run. Resolves 45m15s timeout cancellations on PRs while keeping
full verification nightly. The workflow comment at line 400 already
named this as the planned approach.
- Mutation rivet-core: shard into 4 (rivet-core x {0,1,2,3}/4) so each
arm fits in ~15-20 min instead of timing out at 55+ min on the
3677-mutant corpus. rivet-cli stays single-arm.
- Verus: always-upload bazel test.log as `verus-test-log` artifact.
Required for debugging spec failures from the GitHub UI; without it
the test log is invisible and we have to guess at SMT errors.
Diagnosed by parallel research agents in REQ-004 follow-up sweep.
Trace: skip
The vertical-aligned `rivet-cli, shard:` tripped yamllint's `commas: too many spaces after comma` rule on line 316. Use a single space; we lose the column alignment but unblock the gate. Trace: skip
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
There was a problem hiding this comment.
⚠️ Performance Alert ⚠️
Possible performance regression was detected for benchmark 'Rivet Criterion Benchmarks'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.20.
| Benchmark suite | Current: 141305d | Previous: c7d5664 | Ratio |
|---|---|---|---|
validate/10000 |
15032857 ns/iter (± 1063041) |
11852513 ns/iter (± 526632) |
1.27 |
This comment was automatically generated by workflow using github-action-benchmark.
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
avrabe
added a commit
that referenced
this pull request
Apr 25, 2026
Verus's lemma_div_is_ordered signature requires int args: fn lemma_div_is_ordered(x: int, y: int, z: int) But `covered * 100` and `total * 100` are `nat * int` (since covered and total are nat), so the call failed with E0308: expected `int`, found `nat` at rivet-core/src/verus_specs.rs:249:13 (covered * 100, total * 100) Surfaced via the bazel test.log artifact upload (PR #209) — without it the Verus failure was just "FAIL in 0.4s" with no detail. Cast both products as int explicitly. The third argument `total as int` was already correctly cast. Verifies: REQ-004
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
Fix three CI jobs that were either failing or unobservable on run 24936025203:
pull_request-only--only-codegensmoke (~5 min) and apushtomain-only full run. The 27-harness full suite was overrunning the 45 min budget mid-CBMC-unwind on every PR. The workflow comment at line 400 already described this approach as the planned fix.rivet-corecorpus across 4 matrix arms (rivet-core x {0,1,2,3}/4). Each shard now has ~15-20 min of work inside the 45 min budget.rivet-clikeeps its single-arm hard-gate behaviour.bazel-testlogs/verus/rivet_specs_verify/test.logas theverus-test-logartifact viaif: always(). Without this we cannot see why the SMT obligations are failing from the GitHub UI.Changes
.github/workflows/ci.yml:mutants:matrix usesinclude:with explicitshardandshard_idfields (slash-freeshard_idkeeps cache key + artifact name valid).kani:step list gated bygithub.event_name/github.ref.verus:adds an always-onUpload Verus test logstep covering bothbazel-out/*/testlogs/...andbazel-testlogs/...paths withif-no-files-found: warn.Test plan
Kani Proofsjob completes in <10 min on this PR (smoke path only)Mutation Testingmatrix arms appear; rivet-cli is the hard gate, rivet-core arms arecontinue-on-errorverus-test-logartifact is downloadable from the run pageConstraints respected
Trace: skip