viperproject
Checking preconditions of postconditions
Hi there !
I was trying to follow Prusti's user guide, and I ran into an issue on part 4.3, trying to prove the second invariant of linked lists (namely "After push(elem) the first element of the list stores the value elem.")
To avoid issues related to arithmetic overflows in the len function, I created a Prusti.toml file containing
check_overflows = false
@fpoli helped me add some invariants to get rid of some errors, but we still get this error :
[Prusti: verification error] precondition of pure function call might not hold.
list.rs[34,30] the failing assertion is here
with the following code :
use prusti_contracts::*;
use std::mem;
#[trusted]
#[requires(src.is_empty())]
#[ensures(dest.is_empty())]
#[ensures(old(dest.len()) == result.len())]
fn replace(dest: &mut Link, src: Link) -> Link {
mem::replace(dest, src)
}
pub struct List {
head: Link,
}
enum Link {
Empty,
More(Box<Node>),
}
struct Node {
elem: i32,
next: Link,
}
impl List {
#[pure]
pub fn len(&self) -> usize {
self.head.len()
}
#[pure]
#[requires(0 <= index && index < self.len())]
pub fn lookup(&self, index: usize) -> i32 {
self.head.lookup(index)
}
#[ensures(result.len() == 0)]
pub fn new() -> Self {
List {
head: Link::Empty,
}
}
#[ensures(self.lookup(0) == elem)]
pub fn push(&mut self, elem: i32) {
let new_node = Box::new(Node {
elem: elem,
next: replace(&mut self.head, Link::Empty),
});
self.head = Link::More(new_node);
debug_assert!(0 < self.head.len());
debug_assert!(self.lookup(0) == elem);
}
}
impl Link {
#[pure]
fn is_empty(&self) -> bool {
match self {
Link::Empty => true,
Link::More(_) => false,
}
}
#[pure]
#[ensures(result >= 0)]
#[ensures(!self.is_empty() ==> result >= 1)]
fn len(&self) -> usize {
match &self {
Link::Empty => 0,
Link::More(x) => x.next.len() + 1
}
}
#[pure]
#[requires(0 <= index && index < self.len())]
pub fn lookup(&self, index: usize) -> i32 {
match self {
Link::More(node) => {
if index == 0 {
node.elem
} else {
node.next.lookup(index - 1)
}
},
Link::Empty => unreachable!(),
}
}
}
fn main() {
let mut l = List::new();
//println!("l.len() = {}", l.len());
l.push(4);
//println!("l.len() = {}", l.len());
l.push(4);
//println!("l.len() = {}", l.len());
}
This is odd because a call self.lookup(0) on the result of a push operation should always be correct.
Is anything wrong with this code or is there something wrong with the verifier ?
Thanks in advance !
The Viper dump of the failing List::push verifies in Silicon. So, this is either an incompleteness of Viper or an issue in the way Prusti sends the program to be verified to Viper.
The error actually comes from the verification of the main function. However, a successful verification of List::push should ensure that the postcondition can be used at the call site without raising verification errors. It's not an unsoundness; it's just confusing for the user because working on main makes Prusti report errors in the already-verified List::push.
Encoding of l.push(4) in main:
// [mir] _2 = List::push(move _3, const 4_i32) -> [return: bb2, unwind: bb5]
label l3
_t6 := builtin$havoc_ref()
inhale acc(i32(_t6), write)
assert true
exhale acc(_3.val_ref, write) && (acc(struct$m_List(_3.val_ref), write) && acc(i32(_t6), write))
_2 := builtin$havoc_ref()
inhale acc(struct$m_List(old[l3](_3.val_ref)), write)
inhale acc(tuple0$(_2), write)
inhale true
inhale m_lookup__$TY$__(snap$__$TY$__Snap$struct$m_List$(old[l3](_3.val_ref)), 0) == old[l3](4) // ERROR
label l4
The program lacks a postcondition. Since List::push takes &mut self, it should ensure that the length of the list doesn't decrease. The lookup call in the postcondition of List::push requires that.
This verifies:
use prusti_contracts::*;
use std::mem;
#[trusted]
#[requires(src.is_empty())]
#[ensures(dest.is_empty())]
#[ensures(old(dest.len()) == result.len())]
fn replace(dest: &mut Link, src: Link) -> Link {
mem::replace(dest, src)
}
pub struct List {
head: Link,
}
enum Link {
Empty,
More(Box<Node>),
}
struct Node {
elem: i32,
next: Link,
}
impl List {
#[pure]
pub fn len(&self) -> usize {
self.head.len()
}
#[pure]
#[requires(0 <= index && index < self.len())]
pub fn lookup(&self, index: usize) -> i32 {
self.head.lookup(index)
}
#[ensures(result.len() == 0)]
pub fn new() -> Self {
List {
head: Link::Empty,
}
}
#[ensures(self.len() == old(self.len()) + 1)]
#[ensures(self.lookup(0) == elem)]
pub fn push(&mut self, elem: i32) {
let new_node = Box::new(Node {
elem: elem,
next: replace(&mut self.head, Link::Empty),
});
self.head = Link::More(new_node);
}
}
impl Link {
#[pure]
fn is_empty(&self) -> bool {
match self {
Link::Empty => true,
Link::More(_) => false,
}
}
#[pure]
#[ensures(result >= 0)]
#[ensures(!self.is_empty() ==> result >= 1)]
fn len(&self) -> usize {
match &self {
Link::Empty => 0,
Link::More(x) => x.next.len() + 1
}
}
#[pure]
#[requires(0 <= index && index < self.len())]
pub fn lookup(&self, index: usize) -> i32 {
match self {
Link::More(node) => {
if index == 0 {
node.elem
} else {
node.next.lookup(index - 1)
}
},
Link::Empty => unreachable!(),
}
}
}
fn main() {
let mut l = List::new();
//println!("l.len() = {}", l.len());
l.push(4);
//println!("l.len() = {}", l.len());
l.push(4);
//println!("l.len() = {}", l.len());
}