-
Notifications
You must be signed in to change notification settings - Fork 16
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
Challenge 11: Safety of Methods for Numeric Primitive Types #59
Comments
Hello! We are CMU Team 2 and will be working on this challenge :) Our team:
|
Hello, this is Team 2 :) We have a question regarding how to write proofs. Per Part 1 of the challenge, we will need to write proofs for unchecked_* methods. We referred to other harnesses in the repo and found that all of them use the
Thank you for any guidance and clarifications! @rahulku @feliperodri |
@Yenyun035 Good question! We recommend writing contracts and applying them directly to the functions. So, close to what you have for option 1, but omitting the wrapper. For example: // your contracts go here!
pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { ... } You can then go ahead and write harnesses for the methods directly, e.g. #[kani::proof_for_contract(i8::unchecked_add)]
fn harness() {...} It seems like you have a good handle on how contracts work, but if you are looking for more resources, we recommend looking at the contracts section of our tutorial. |
@carolynzech Appreciate it for your response! I just tried to add contracts and write a corresponding harness as you stated. However, I encountered this error:
How could this be resolved? |
@Yenyun035 Ensure that you're running Kani from the |
Link to challenge: https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html
The text was updated successfully, but these errors were encountered: