add a few kani proofs #429
Conversation
There was a problem hiding this comment.
Pull request overview
This PR adds Kani model checker proofs to verify the correctness of the GlobalWeight implementation, which manages weight tracking for future queues. The proofs verify critical invariants such as capacity bounds, operation symmetry, and clamping behavior.
- Adds 5 Kani proof functions to verify GlobalWeight invariants
- Configures Cargo.toml to recognize the
kanicfg flag - Adds CI workflow job to run Kani verification on pull requests
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| src/global_weight.rs | Adds kani_proofs module with 5 verification proofs for weight management invariants |
| Cargo.toml | Adds lint configuration to suppress warnings for the kani cfg flag |
| .github/workflows/ci.yml | Adds Kani verification job to CI pipeline |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
src/global_weight.rs
Outdated
| let large_weight: usize = kani::any(); | ||
| kani::assume(large_weight > max); | ||
|
|
||
| // Both should have space (since weight gets clamped to max). |
There was a problem hiding this comment.
The comment is misleading. When large_weight > max and it gets clamped to max, has_space_for checks if current <= max - max, which is current <= 0. This is only true when current == 0, not in general. The conditional check on line 122 correctly handles this, but the comment incorrectly suggests that having space is guaranteed due to clamping.
| // Both should have space (since weight gets clamped to max). | |
| // If there is space for the clamped weight (max), both paths should behave the same. |
Time to start using a model checker on this somewhat tricky code.
Time to start using a model checker on this somewhat tricky code.