Update exercises #1024
Update exercises #1024
Conversation
| @@ -4,11 4,11 @@ use creusot_contracts::*; | |||
| // Prove the following: | |||
| // 1. If we return Some(i) it is the first index containing `tgt` | |||
| // 2. If we return None, then there are no indices containing `tgt` | |||
| fn search<T: Ord>(v: &Vec<T>, tgt: &T) -> Option<usize> { | |||
| fn search<T: Ord DeepModel>(v: &[T], tgt: &T) -> Option<usize> { | |||
There was a problem hiding this comment.
Are you saying compilation/translation to Coma fails without this? Or did you have to add this to prove whichever spec you wanted to prove?
There was a problem hiding this comment.
Ok, this happened after adding the specification.
use creusot_contracts::*;
#[ensures(forall<i: usize> result == Some(i) ==> i@ < [email protected]() && forall<j: Int> 0 <= j && j < i@ ==> v@[j] != *tgt)]
#[ensures(result == None ==> forall<i: Int> 0 <= i && i < [email protected]() ==> v@[i] != *tgt)]
pub fn search<T: Ord>(v: &[T], tgt: &T) -> Option<usize> {
let mut i = 0;
#[invariant(forall<j: Int> 0 <= j && j < i@ ==> v@[j] != *tgt)]
while i < v.len() {
if v[i] == *tgt {
return Some(i);
}
i = 1
}
return None;
}For the code above, I get the following error message:
error[E0277]: the trait bound `T: creusot_contracts::DeepModel` is not satisfied
--> src/lib.rs:10:12
|
10 | if v[i] == *tgt {
| ^^^^^^^^^^^^ the trait `creusot_contracts::DeepModel` is not implemented for `T`
I can also use tgt@ instead of *tgt in the specifications, but then I get an additional message about ShallowModel not being implemented by T.
I’m on commit 917bcee1, if this is of interest.
There was a problem hiding this comment.
Indeed, you need to add this bound. I think my original intent was to have that be part of the exercise, but its probably best to provide that for the user.
There was a problem hiding this comment.
In fact, I started to wonder whether adding the DeepModel trait bound was intended to be part of the exercise once I read @sarsko’s comment 😅 I guess the actual issue is that DeepModel is not mentioned in the guide. Otherwise I would have felt more comfortable with the exercise. And if you have the page anyway, you could use #[diagnostic::on_unimplemented] and link the respective page, which would IMO be the best experience for newcomers 😉
| @@ -6,9 6,7 @@ use creusot_contracts::*; | |||
| pub fn all_zero(v: &mut Vec<u32>) { | |||
| let mut i = 0; | |||
| let old_v = snapshot! { v }; | |||
| // Until https://gitlab.inria.fr/why3/why3/-/merge_requests/667 is merged | |||
| // the following invariant is needed to allow Why3 to remember prophecies dont change | |||
| #[invariant(proph_const, ^v == ^old_v.inner())] | |||
There was a problem hiding this comment.
Keep in mind, this is actually now needed again by the change to coma. At least until 0.2 comes out (soon ish).
There was a problem hiding this comment.
Interesting, so that’s why I needed #[invariant(^*old_v == ^v)]? The old syntax with proph_const didn’t seem to work …
error: unexpected token
--> src/lib.rs:119:28
|
119 | #[invariant(proph_const, ^old_v.inner() == ^v)]
| ^
error: internal error: Cannot fetch THIR body
|
Hi Nils, Thanks for the PR, I think we'll merge it but there are a few remarks / questions I have for you:
Do you mean that Creusot panics? Returns an error? Or that it generates ill-formed Coma code? More generally, I would strongly recommend sticking to |
I just noticed ordinary error messages. So everything is fine 🙂 |
Before turning to a larger project, I thought it might be better to solve a few small exercises. Unfortunately, two of the provided ones have little bugs such that the compilation/translation to Coma already fails. I am not confident about the
DeepModeltrait bound (still learning Creusot …) but it seemed to be required.