model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.03k stars 85 forks source link

Ensure that `Arbitrary` respects `Invariant` somehow #3265

Open adpaco-aws opened 2 weeks ago

adpaco-aws commented 2 weeks ago

The #[derive(Invariant)] macro introduced in #3250 allows the derived Arbitrary to generate values which don't respect the invariant, as explained in this comment. We should figure how to check for these cases, although that might become clearer once we've finished adding the remaining features for type invariant.