One ranking, written once, and proved rather than sampled - #40
Conversation
`audit --for-publication`, `scan` and the coverage half of `check` each ranked the same two counts into the same three exit codes, in three copies. Three transcriptions of one decision is three places for it to drift, and the drift is silent: every copy still returns a valid `Exit`, so a copy that had stopped agreeing would report a number nobody could see was wrong. `error::verdict` is the one statement of it now, beside the `Exit` enum whose docstring already claimed the convention lived in one place. Then the proofs, because this is the function where an unknown becomes a number a caller acts on -- and `UNKNOWN -> PASS` is the failure this repository keeps finding one seam at a time. Four `#[cfg(kani)]` harnesses say, over every pair of counts a usize can hold: * a run that could not look never exits 0; * a violation outranks a surface that could not be read; * clean means read everything and found nothing, in both directions; * every answer is one of the three codes this tool documents. Worth a model checker here and nowhere else in this crate, and the measurement is what says so. Change `could_not_look > 0` to `could_not_look > 1` -- one character -- and all 197 in-crate unit tests still pass, including the four that test this function directly, because they name 3 and 0 and never 1. One CLI test catches it, by the luck of exercising a tree with exactly one unreadable seam. Kani refuses in 15 milliseconds with the counterexample, and that number is the argument for the tier: everything else in this crate reads files, runs git and formats reports, and CBMC has nothing to say about any of it. Not wired into a hook, for the same reason `cargo deny` is not: `cargo kani setup` fetches half a gigabyte, which is not something a commit waits for. The proofs themselves cost about a second each. CONTRIBUTING carries the command and the measurement. `cfg(kani)` is declared in `Cargo.toml` rather than allowed at the module, so the unexpected-cfg lint keeps working on every other name in the file.
|
Warning Review limit reached
Next review available in: 32 minutes You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. How can I continue?After more reviews become available, a review can be triggered using the To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews. How do review limits work?CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability. For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window. Please refer docs for additional details. Review details⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: 📒 Files selected for processing (6)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #40 +/- ##
=======================================
Coverage 89.44% 89.45%
=======================================
Files 31 31
Lines 9732 9727 -5
=======================================
- Hits 8705 8701 -4
+ Misses 1027 1026 -1 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
2 participants
Answers the Kani deliverable of #13: one proof over exit-state logic. It needed a function to be about, and finding one found three copies of it.
One ranking, three copies
audit --for-publication,scanand the coverage half ofcheckeach turned the same two counts -- what was found, what could not be read -- into the same three exit codes, in three separate places. Three transcriptions of one decision is three places for it to drift, and the drift is silent: every copy still returns a validExit, so a copy that had stopped agreeing reports a number nobody can see is wrong.error::verdictis the single statement of it now, beside theExitenum whose docstring already said the convention lived in one place.The proofs
Four
#[cfg(kani)]harnesses, over every pair of counts ausizecan hold:Why here and nowhere else in the crate
Measured rather than asserted. Change
could_not_look > 0tocould_not_look > 1-- one character -- and all 197 in-crate unit tests still pass, including the four that test this function directly, because they name 3 and 0 and never 1. One CLI test catches it, by the luck of exercising a tree with exactly one unreadable seam. Kani refuses in 15 milliseconds and hands back the counterexample.That is the whole argument for the tier and also its limit: everything else in this crate reads files, runs git and formats reports, and CBMC has nothing useful to say about any of it. This is the one function where an unknown becomes a number a caller acts on, which is the failure shape this repository keeps finding one seam at a time.
Cost, and where it runs
cargo kani setupfetches about half a gigabyte; the proofs then cost about a second each. Manual tier, documented in CONTRIBUTING, not wired into a hook -- the same decisioncargo denygot and for the same reason.cfg(kani)is declared inCargo.tomlrather than allowed at the module, so the unexpected-cfg lint keeps working on every other name in that file.Checks
cargo test,cargo clippy --all-targets,cargo fmt --check,scripts/coverage.sh(454 tests, 88.29%),uphold scan,uphold checkandcargo kaniall pass locally.