Prusti proves `false` in `tests/verify_overflow/pass/extern-spec/linked-list.rs`

[vfukala]

prusti-tests/tests/verify_overflow/pass/extern-spec/linked-list.rs still passes even when prusti_assert!(false); is added to line 115.

The entire test case then looks like this:

use prusti_contracts::*;

use std::collections::LinkedList;
use std::option::Option;

#[extern_spec]
impl<T> std::option::Option<T> {
    #[pure]
    #[ensures(matches!(*self, Some(_)) == result)]
    pub fn is_some(&self) -> bool;

    #[pure]
    #[ensures(self.is_some() == !result)]
    pub fn is_none(&self) -> bool;

    #[requires(self.is_some())]
    pub fn unwrap(self) -> T;

    #[requires(self.is_some())]
    pub fn expect(self, msg: &str) -> T;
}

/// Ghost method for LinkedList used to access an index in the LinkedList
#[trusted]
#[pure]
#[requires(index < list.len())]
fn get<T: Copy>(list: &LinkedList<T>, index: usize) -> T {
    for (i, elem) in list.iter().enumerate() {
        if i == index {
            return *elem;
        }
    }
    unreachable!()
}

#[extern_spec]
impl<T> LinkedList<T>
    where T: Copy + PartialEq {
    #[ensures(result.is_empty())]
    pub fn new() -> LinkedList<T>;

    #[pure]
    #[ensures(result ==> self.len() == 0)]
    #[ensures(!result ==> self.len() > 0)]
    pub fn is_empty(&self) -> bool;

    #[pure]
    pub fn len(&self) -> usize;

    #[ensures(self.len() == 0)]
    pub fn clear(&mut self);

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(get(self, 0) == elt)]
    #[ensures(forall (|i: usize| (i < old(self.len())) ==>
        get(self, i + 1) == old(get(self, i))))]
    pub fn push_front(&mut self, elt: T);

    #[ensures(old(self.len()) == 0 ==> (self.len() == old(self.len())) && result.is_none())]
    #[ensures(old(self.len()) > 0 ==> self.len() == old(self.len()) - 1 && result.is_some())]
    #[ensures(old(self.len()) > 0 ==> forall (|i: usize| (i < self.len()) ==>
    get(self, i) == old(get(self, i + 1))))]
    pub fn pop_front(&mut self) -> Option<T>;

    #[ensures(self.len() == old(self.len()) + 1)]
    #[ensures(get(self, self.len() - 1) == elt)]
    #[ensures(forall (|i: usize| (i < old(self.len())) ==>
    get(self, i) == old(get(self, i))))]
    pub fn push_back(&mut self, elt: T);

    #[ensures(old(self.len()) == 0 ==> (self.len() == old(self.len())) && result.is_none())]
    #[ensures(old(self.len()) > 0 ==> self.len() == old(self.len()) - 1 && result.is_some())]
    #[ensures(old(self.len()) > 0 ==> forall (|i: usize| (i < self.len()) ==>
    get(self, i) == old(get(self, i))))]
    pub fn pop_back(&mut self) -> Option<T>;

    #[ensures(self.len() == old(self.len() + other.len()))]
    #[ensures(forall (|i: usize| (i < old(self.len())) ==>
        get(self, i) == old(get(self, i))))]
    #[ensures(forall (|j: usize| (old(self.len()) <= j && j < self.len()) ==>
        get(self, j) == old(get(other, j - self.len()))))]
    #[ensures(other.len() == 0)]
    pub fn append(&mut self, other: &mut LinkedList<T>);

    #[requires(at <= self.len())]
    #[ensures(result.len() == old(self.len()) - at)]
    #[ensures(self.len() == at)]
    #[ensures(forall (|i: usize| (i < self.len()) ==>
        get(self, i) == old(get(self, i))))]
    #[ensures(forall (|j: usize| (j < result.len()) ==>
        get(&result, j) == old(get(self, j + at))))]
    pub fn split_off(&mut self, at: usize) -> LinkedList<T>;
}

fn main() {
    let mut l = LinkedList::new();
    l.push_front(1);

    assert!(get(&l, 0) == 1);

    let mut ll2 = LinkedList::new();
    ll2.push_front(2);
    ll2.push_front(3);
    ll2.push_front(4);
    assert!(get(&ll2, 2) == 2);
    assert!(get(&ll2, 1) == 3);
    assert!(get(&ll2, 0) == 4);

    l.append(&mut ll2);
    assert!(l.len() == 4);

    assert!(get(&l, 3) == 2);
    assert!(get(&l, 2) == 3);
    assert!(get(&l, 1) == 4);

    prusti_assert!(false); // CHANGED HERE

    assert!(matches!(l.pop_front(), Some(1)));

    assert!(l.len() == 3);
}

This does not happen (the test case doesn't pass) when the prusti_assert!(false); is added before the three assert!(get... right above.

(equivalently:) The test case doesn't pass if instead, prusti_refute!(false); is added to line 115.

[vfukala]

A minimized example. This program verifies (with default flags) despite the prusti_assert!(false);:

use prusti_contracts::*;

struct List {
    sz: usize
}

impl List {
    #[trusted]
    #[ensures(result.sz == 0)]
    fn new() -> List { unreachable!() }

    #[trusted]
    #[requires(self.sz == 0)]
    #[ensures(self.sz == 1)]
    #[ensures(old(0 - self.sz) == 0)]
    fn add_to_empty(&mut self) { unreachable!() }
}

fn main() {
    let mut l = List::new();

    l.add_to_empty();

    prusti_assert!(false);
}

If any of the following conditions holds, the program (correctly) doesn't verify:

• passing CHECK_OVERFLOWS=false
• removing the #[ensures(self.sz == 1)] (line 14)
• removing the #[ensures(old(0 - self.sz) == 0)] (line 15)
• changing 0 - self.sz on line 15 to any of: 0, self.sz, or self.sz - 0

[fpoli]

Nice catch! It seems that overflow conditions of old expressions are encoded without an old(..) around them. That is, the postcondition old(0 - self.sz) == 0 is being encoded as self.sz == 0 && old(0 - self.sz) == 0 but it should be old(self.sz == 0) && old(0 - self.sz) == 0.