Skip to content

Update exercises #1024

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.

Sign up for GitHub

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

Merged
xldenis merged 1 commit into from
Jun 21, 2024
Merged

Update exercises #1024

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions exercises/02_linear_search.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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> {
Copy link
Copy Markdown
Contributor

@sarsko sarsko Jun 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Copy Markdown
Contributor Author

@nhusung nhusung Jun 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Collaborator

@xldenis xldenis Jun 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor Author

@nhusung nhusung Jun 21, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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 😉

let mut i = 0;

while i < v.len() {
if v[i] == tgt {
if v[i] == *tgt {
Comment thread
xldenis marked this conversation as resolved.
return Some(i);
}

Expand Down
4 changes: 1 addition & 3 deletions exercises/04_all_zero.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())]
Copy link
Copy Markdown
Collaborator

@xldenis xldenis Jun 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Copy Markdown
Contributor Author

@nhusung nhusung Jun 21, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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


while i < v.len() {
v[i] = 0;
i += 1;
Expand Down