Regression with List::append example

[fpoli]

The following program, from Alex's presentation, no longer verifies. It still verifies using the latest GithHub release, which is a few months old.

error: [Prusti: verification error] postcondition might not hold.
  --> tmp/program.rs:32:15
   |
32 |     #[ensures(self.len() == old(self.len()) + 1)]
   |               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
note: the error originates here
  --> tmp/program.rs:39:5
   |
39 | /     fn append(&mut self, v: i32) {
40 | |         match self.next {
41 | |             None => self.next = Some(box List { val: v, next: None }),
42 | |             Some(box ref mut tail) => tail.append(v),
43 | |         }
44 | |     }
   | |_____^

#![feature(box_patterns, box_syntax)]
use prusti_contracts::*;

struct List {
    val: i32,
    next: Option<Box<List>>
}

impl List {
    #[pure]
    #[ensures(result > 0)]
    fn len(&self) -> usize {
        match self.next {
            None => 1,
            Some(box ref tail) => 1 + tail.len(),
        }
    }

    #[pure]
    #[requires(0 <= i && i < self.len())]
    fn get(&self, i: usize) -> i32 {
        if i == 0 {
            self.val
        } else {
            match self.next {
                Some(box ref tail) => tail.get(i - 1),
                None => unreachable!(),
            }
        }
    }

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(self.get(self.len() - 1) == v)]
    #[ensures(
        forall(|i:usize|
            0 <= i && i < self.len() - 1 ==> self.get(i) == old(self.get(i))
        )
    )]
    fn append(&mut self, v: i32) {
        match self.next {
            None => self.next = Some(box List { val: v, next: None }),
            Some(box ref mut tail) => tail.append(v),
        }
    }
}

fn client(a: &mut List, b: &mut List) {
    let old_len = b.len();
    a.append(42);
    assert!(b.len() == old_len);
}

fn main(){}

[Aurel300]

We have versions of this test in the test suite. They were disabled with the latest snapshot changes, as discussed, due to pure recursive functions no longer being unfolded automatically by the verifier. See #543.

[fpoli]

I see, thanks. I'll close as this is included in #543.