NonZero (unchecked_mul & unchecked_add) Proof for Contracts #338
Conversation
Added contract and placeholder harness
Corrected issues from Pull Request
Restored previous cargo files
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Zyad Hassan <[email protected]>
|
|
||
| macro_rules! nonzero_check_add { | ||
| ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => { | ||
| #[kani::proof_for_contract(<$t>::unchecked_add)] |
There was a problem hiding this comment.
| #[kani::proof_for_contract(<$t>::unchecked_add)] | |
| #[kani::proof_for_contract(<$nonzero_type>::unchecked_add)] |
There was a problem hiding this comment.
No, that would not produce the right type. We want something like <i8>::unchecked_add, not <NonZeroI8>::unchecked_add.
There was a problem hiding this comment.
But taking u8 as my example, won't that produce a proof for https://doc.rust-lang.org/std/primitive.u8.html#method.unchecked_add instead of https://doc.rust-lang.org/std/num/struct.NonZero.html#method.unchecked_add?
|
|
||
| macro_rules! check_mul_unchecked_intervals { | ||
| ($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => { | ||
| #[kani::proof_for_contract(<$t>::unchecked_mul)] |
There was a problem hiding this comment.
| #[kani::proof_for_contract(<$t>::unchecked_mul)] | |
| #[kani::proof_for_contract(<$nonzero_type>::unchecked_mul)] |
|
|
||
| macro_rules! check_mul_unchecked_small { | ||
| ($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_mul_for:ident) => { | ||
| #[kani::proof_for_contract(<$t>::unchecked_mul)] |
There was a problem hiding this comment.
| #[kani::proof_for_contract(<$t>::unchecked_mul)] | |
| #[kani::proof_for_contract(<$nonzero_type>::unchecked_mul)] |
| // TODO: not sure how to refer to a parameter that is a mutable reference | ||
| // #[requires({ | ||
| // let size = core::mem::size_of::<T>(); | ||
| // let ptr = n as *const T as *const u8; | ||
| // let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; | ||
| // !slice.iter().all(|&byte| byte == 0) | ||
| // })] |
There was a problem hiding this comment.
I would vote removing this (and its harnesses) from this PR entirely. I think these contracts will need simplification before getting merged upstream. My hunch is that the Rust community will need to land on some canonical way of talking about the memory behind references in contracts (at least an experimental one), rather than twist ourselves into knots writing unsafe contracts.
In the meantime, I don't think there's much value-add in merging this in; there's already a similar contract in new_unchecked.
There was a problem hiding this comment.
Ack, will put in a PR of its own where we can discuss this properly. Also, is unrelated to the PR description.
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Co-authored-by: Carolyn Zech <[email protected]>
Towards #71
These are the changes contributed by SahithiMV in #184 plus the proposed changes in that PR.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.