-
Notifications
You must be signed in to change notification settings - Fork 97
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Call check_proof_attribute
for contract harnesses
#3522
Call check_proof_attribute
for contract harnesses
#3522
Conversation
Note that we should merge model-checking/verify-rust-std#86 first to avoid breaking the standard library. |
Merging this shouldn't break the std repository, right? BTW, you could leave it as draft for now too since you don't think this is ready to be merged. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks
It will break our harnesses in the std repository--see the new error messages in the logs:
|
Modifies the `check_cast` harness to: - Be a proof instead of a proof for contract - Remove the generic type parameter Currently, Kani doesn't run this harness. (See the [log](https://github.com/model-checking/verify-rust-std/actions/runs/10887990165/job/30211482361?pr=85) from a recent PR). It doesn't run the harness because it has a generic type parameter, and Kani's error handling for contract proofs doesn't check for this condition. (PR to fix is [here](model-checking/kani#3522)). Once we remove the generic type parameter so that the harness runs, Kani complains that we can't run it as a proof for contract because there are no contracts, so we make it a regular proof instead. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
dd26362
Modifies the `check_cast` harness to: - Be a proof instead of a proof for contract - Remove the generic type parameter Currently, Kani doesn't run this harness. (See the [log](https://github.com/model-checking/verify-rust-std/actions/runs/10887990165/job/30211482361?pr=85) from a recent PR). It doesn't run the harness because it has a generic type parameter, and Kani's error handling for contract proofs doesn't check for this condition. (PR to fix is [here](model-checking/kani#3522)). Once we remove the generic type parameter so that the harness runs, Kani complains that we can't run it as a proof for contract because there are no contracts, so we make it a regular proof instead. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Kani enforces that
[kani::proof]
attribute is not applied to generic functions. We do not currently enforce this restriction on contract harnesses. When the compiler searches for harnesses to verify, it only looks at monomorphized functions. Thus, currently a user can write this code:and get
"No proof harnesses (functions with #[kani::proof]) were found to verify."
In the case where a user is running many harnesses, they may not notice that Kani skipped the harness. For example, we currently have this harness in the standard library, which doesn't actually run. (PR to fix is here). After this PR merges, the code snippet above would instead error with:
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.