This is a tracking issue for fixing the known quantifiers limitation that the ranges must be usizes.
I tried this code:
#[kani::requires(min != 0 && max != 0)]
#[kani::ensures(|result| *result != 0 && max % *result == 0 && min % *result == 0)]
#[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
#[kani::recursion]
fn gcd(mut max: u8, mut min: u8) -> u8 {
if min > max {
std::mem::swap(&mut max, &mut min);
}
let rest = max % min;
if rest == 0 { min } else { gcd(max, rest) }
}
#[kani::proof_for_contract(gcd)]
fn check_gcd() {
let max: u8 = kani::any();
let min: u8 = kani::any();
gcd(max, min);
}using the following command line invocation:
cargo kani -Z function-contracts
with Kani version: 0.62.0
I expected to see this happen: verification success
Instead, this happened:
cmzech@80a9971b5e20 playground % cargo kani -Z function-contracts
Kani Rust Verifier 0.62.0 (cargo plugin)
Compiling playground v0.1.0 (/Users/cmzech/playground)
error[E0308]: mismatched types
--> src/lib.rs:3:49
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| -----------------------^^^^^^^---------------------------------------------------
| | |
| | expected `usize`, found `u8`
| expected due to this
|
help: you can convert a `u8` to a `usize`
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX.into())| !(max % i == 0 && min % i == 0) || *result >= i))]
| +++++++
error[E0631]: type mismatch in closure arguments
--> src/lib.rs:3:26
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| expected due to this
| found signature defined here
| required by a bound introduced by this call
|
= note: expected closure signature `fn(usize) -> _`
found closure signature `fn(u8) -> _`
note: required by a bound in `kani::internal::kani_forall`
--> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
|
55 | kani_core::kani_lib!(kani);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| required by a bound in this function
| required by this bound in `kani_forall`
= note: this error originates in the macro `kani::forall` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider wrapping the function in a closure
--> /Users/cmzech/kani/library/kani_core/src/lib.rs:203:71
|
203| kani::internal::kani_forall(lower_bound, upper_bound, |arg0: usize| predicate(/* u8 */))
| +++++++++++++ ++++++++++
error[E0308]: mismatched types
--> src/lib.rs:3:49
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| -----------------------^^^^^^^---------------------------------------------------
| | |
| | expected `usize`, found `u8`
| expected due to this
|
help: you can convert a `u8` to a `usize`
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX.into())| !(max % i == 0 && min % i == 0) || *result >= i))]
| +++++++
error[E0631]: type mismatch in closure arguments
--> src/lib.rs:3:26
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| expected due to this
| found signature defined here
| required by a bound introduced by this call
|
= note: expected closure signature `fn(usize) -> _`
found closure signature `fn(u8) -> _`
note: required by a bound in `kani::internal::kani_forall`
--> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
|
55 | kani_core::kani_lib!(kani);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| required by a bound in this function
| required by this bound in `kani_forall`
= note: this error originates in the macro `kani::forall` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider wrapping the function in a closure
--> /Users/cmzech/kani/library/kani_core/src/lib.rs:203:71
|
203| kani::internal::kani_forall(lower_bound, upper_bound, |arg0: usize| predicate(/* u8 */))
| +++++++++++++ ++++++++++
error[E0308]: mismatched types
--> src/lib.rs:3:49
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| -----------------------^^^^^^^---------------------------------------------------
| | |
| | expected `usize`, found `u8`
| expected due to this
|
help: you can convert a `u8` to a `usize`
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX.into())| !(max % i == 0 && min % i == 0) || *result >= i))]
| +++++++
error[E0631]: type mismatch in closure arguments
--> src/lib.rs:3:26
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| expected due to this
| found signature defined here
| required by a bound introduced by this call
|
= note: expected closure signature `fn(usize) -> _`
found closure signature `fn(u8) -> _`
note: required by a bound in `kani::internal::kani_forall`
--> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
|
55 | kani_core::kani_lib!(kani);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| required by a bound in this function
| required by this bound in `kani_forall`
= note: this error originates in the macro `kani::forall` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider wrapping the function in a closure
--> /Users/cmzech/kani/library/kani_core/src/lib.rs:203:71
|
203| kani::internal::kani_forall(lower_bound, upper_bound, |arg0: usize| predicate(/* u8 */))
| +++++++++++++ ++++++++++
error[E0308]: mismatched types
--> src/lib.rs:3:49
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| -----------------------^^^^^^^---------------------------------------------------
| | |
| | expected `usize`, found `u8`
| expected due to this
|
help: you can convert a `u8` to a `usize`
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX.into())| !(max % i == 0 && min % i == 0) || *result >= i))]
| +++++++
error[E0631]: type mismatch in closure arguments
--> src/lib.rs:3:26
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| expected due to this
| found signature defined here
| required by a bound introduced by this call
|
= note: expected closure signature `fn(usize) -> _`
found closure signature `fn(u8) -> _`
note: required by a bound in `kani::internal::kani_forall`
--> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
|
55 | kani_core::kani_lib!(kani);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| required by a bound in this function
| required by this bound in `kani_forall`
= note: this error originates in the macro `kani::forall` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider wrapping the function in a closure
--> /Users/cmzech/kani/library/kani_core/src/lib.rs:203:71
|
203| kani::internal::kani_forall(lower_bound, upper_bound, |arg0: usize| predicate(/* u8 */))
| +++++++++++++ ++++++++++
error[E0308]: mismatched types
--> src/lib.rs:3:49
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| -----------------------^^^^^^^---------------------------------------------------
| | |
| | expected `usize`, found `u8`
| expected due to this
|
help: you can convert a `u8` to a `usize`
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX.into())| !(max % i == 0 && min % i == 0) || *result >= i))]
| +++++++
error[E0631]: type mismatch in closure arguments
--> src/lib.rs:3:26
|
3 | #[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX)| !(max % i == 0 && min % i == 0) || *result >= i))]
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| expected due to this
| found signature defined here
| required by a bound introduced by this call
|
= note: expected closure signature `fn(usize) -> _`
found closure signature `fn(u8) -> _`
note: required by a bound in `kani::internal::kani_forall`
--> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
|
55 | kani_core::kani_lib!(kani);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| required by a bound in this function
| required by this bound in `kani_forall`
= note: this error originates in the macro `kani::forall` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: consider wrapping the function in a closure
--> /Users/cmzech/kani/library/kani_core/src/lib.rs:203:71
|
203| kani::internal::kani_forall(lower_bound, upper_bound, |arg0: usize| predicate(/* u8 */))
| +++++++++++++ ++++++++++
Some errors have detailed explanations: E0308, E0631.
For more information about an error, try `rustc --explain E0308`.
error: could not compile `playground` (lib) due to 10 previous errors
error: Failed to execute cargo (exit status: 101). Found 10 compilation errors.
I had to change the quantifier to this:
#[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX as usize)| !(max as usize % (i as usize) == 0 && min as usize % (i as usize) == 0) || (*result as usize) >= (i as usize)))]
This is quite cumbersome. The error message is very confusing (and repetitive), so short of fixing the problem, we can at least try to improve that.
This is a tracking issue for fixing the known quantifiers limitation that the ranges must be usizes.
I tried this code:
using the following command line invocation:
with Kani version: 0.62.0
I expected to see this happen: verification success
Instead, this happened:
I had to change the quantifier to this:
#[kani::ensures(|result| kani::forall!(|i in (1,u8::MAX as usize)| !(max as usize % (i as usize) == 0 && min as usize % (i as usize) == 0) || (*result as usize) >= (i as usize)))]This is quite cumbersome. The error message is very confusing (and repetitive), so short of fixing the problem, we can at least try to improve that.