-
Notifications
You must be signed in to change notification settings - Fork 109
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
Cannot use PartialOrd in specifications despite marking them as #[pure] using external spec feature #1436
Comments
Thank you for the bug report. The panic is due to an prusti-dev/prusti-interface/src/environment/query.rs Lines 273 to 320 in 863cd59
In other words, Prusti fails to find the method that implements the declared As a workaround, I'd try to define and use in the specifications a method like impl Frame {
#[pure]
#[trusted]
#[ensures(result == (self.number >= other.number))] // i.e. the implementation of `#[derive(PartialOrd)]`
pub fn ge(&self, other: &Self) -> bool { *self >= *other }
} |
Sorry for the delay in responding! There is no core limitation here, just various bits and pieces that are not done "yet". I'll start with providing the modified file that does verify, then comment on some parts of it: use prusti_contracts::*;
#[derive(PartialEq, Eq, Copy, Clone, PartialOrd, Ord)]
struct Frame {
number: usize
}
// (1)
#[extern_spec]
trait PartialOrd<Rhs> {
#[pure]
fn partial_cmp(&self, other: &Rhs) -> Option<core::cmp::Ordering>;
#[pure]
#[ensures(result == matches!(self.partial_cmp(other), Some(core::cmp::Ordering::Greater)))]
fn gt(&self, other: &Rhs) -> bool;
#[pure]
#[ensures(result == matches!(self.partial_cmp(other), Some(core::cmp::Ordering::Greater | core::cmp::Ordering::Equal)))]
fn ge(&self, other: &Rhs) -> bool;
}
#[extern_spec]
impl PartialOrd<usize> for usize {
#[pure]
#[ensures(if *self > *other {
result === Some(core::cmp::Ordering::Greater)
} else if *self < *other {
result === Some(core::cmp::Ordering::Less)
} else {
result === Some(core::cmp::Ordering::Equal)
})]
fn partial_cmp(&self, other: &usize) -> Option<core::cmp::Ordering>;
}
// (2)
#[extern_spec]
impl PartialOrd for Frame {
#[pure]
#[ensures(result == self.number.partial_cmp(&other.number))]
fn partial_cmp(&self, other: &Frame) -> Option<core::cmp::Ordering>;
}
impl Frame {
#[ensures(result >= *a && result >= *b)]
fn max(a: &Frame, b: &Frame) -> Frame {
assert!(matches!( // (4)
a.partial_cmp(a),
Some(core::cmp::Ordering::Greater | core::cmp::Ordering::Equal)
));
if *a > *b { // (3)
*a
} else {
*b
}
}
}
#[trusted]
fn main() {}
|
Thanks @Aurel300, the explanation was very helpful. |
I'm trying to use the basic comparison operators for a type in my specifications, and following advice I found from other issues, I've marked the Ord and PartialOrd required methods as pure using the external spec feature. This still leads to a Prusti error:
[Prusti: invalid specification] use of impure function "std::cmp::PartialOrd::ge" in pure code is not allowed
When I add the ge() method to my external spec and mark it as pure, I get an unexpected error.
I'm wondering if I'm missing something when trying to use external spec for trait methods, or if this actually is an issue for now.
This is the code:
This is the Prusti assistant output when I try to set the ge() method as pure:
The text was updated successfully, but these errors were encountered: