Update exercises

[nhusung]

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 DeepModel trait bound (still learning Creusot …) but it seemed to be required.

[sarsko]

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?

[nhusung]

Ok, this happened after adding the specification.

use creusot_contracts::*;

#[ensures(forall<i: usize> result == Some(i) ==> i@ < v@.len() && forall<j: Int> 0 <= j && j < i@ ==> v@[j] != *tgt)]
#[ensures(result == None ==> forall<i: Int> 0 <= i && i < v@.len() ==> 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.

[xldenis]

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.

[nhusung]

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 😉

[xldenis]

Keep in mind, this is actually now needed again by the change to coma. At least until 0.2 comes out (soon ish).

[nhusung]

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

[xldenis]

Hi Nils,

Thanks for the PR, I think we'll merge it but there are a few remarks / questions I have for you:

Unfortunately, two of the provided ones have little bugs such that the compilation/translation to Coma already fails.

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 v0.1, which is our first "stable" version and still uses MLCFG. The current Coma branch on master has some regressions compared to 0.1 though by 0.2 it will supersede it.

[nhusung]

Do you mean that Creusot panics? Returns an error? Or that it generates ill-formed Coma code?

I just noticed ordinary error messages. So everything is fine 🙂