viperproject
List tutorial fails to verify
I am trying to verify (using the prusti-rustc binary) the basic stack proposed in the tutorial:
#![feature(box_patterns)]
use prusti_contracts::*;
use std::mem;
pub enum TrustedOption {
Some(i32),
None,
}
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()
}
#[ensures(result.len() == 0)]
pub fn new() -> Self {
List {
head: Link::Empty,
}
}
}
impl Link {
#[pure]
#[ensures(!self.is_empty() ==> result > 0)]
#[ensures(result >= 0)]
fn len(&self) -> usize {
match self {
Link::Empty => 0,
Link::More(box node) => 1 + node.next.len(),
}
}
#[pure]
fn is_empty(&self) -> bool {
match self {
Link::Empty => true,
Link::More(box node) => false,
}
}
}
fn main(){}
which produces this verification error in the method List.new():
error: [Prusti: verification error] postcondition might not hold. #[ensures(result.len() == 0)]
I can solve it adding the following postcondition to the Link.len() method:
#[ensures(self.is_empty() ==> result == 0)]
But this postcondition can be derived by the current one !self.is_empty() ==> result > 0 && result >= 0.
My questions are:
- Does the tutorial fails to verify on purpose?
- Is it ok to add this new postcondition or should it be deduced by Prusti?
Thanks for reporting that. Which version of Prusti are you using? Using the latest version of the master branch this program verifies for me, without the redundant ... result == 0 postcondition.
Does the tutorial fails to verify on purpose?
No, it seems an (unintended) incompleteness that has been fixed in the meantime. We should add the examples of that tutorial to the test suite to avoid more regressions.
Is it ok to add this new postcondition or should it be deduced by Prusti?
It should be deduced, but it's also ok to add that postcondition because it's anyway going to be checked when verifying the implementation of len.
I tried the last nightly release without luck. What I am doing is unzipping the binaries for Ubuntu, giving execution permissions to all binaries and executing:
./prusti-rustc --edition=2021 list.rs
The errors continue. Should I build directly from source?
No need to compile from source; the last nightly release should be enough. I actually found that I had check_overflows=false in my Prusti.toml; my bad. With overflow checks enabled I can reproduce the issue.
(You also get that 1 + node.next.len() might overflow, I expect.)
Exactly, I have two errors.
If I consider the whole example, I have even more errors (5 to be exact). Thanks for confirming this.
#![feature(box_patterns)]
use prusti_contracts::*;
use std::mem;
pub enum TrustedOption {
Some(i32),
None,
}
impl TrustedOption {
#[pure]
pub fn is_none(&self) -> bool {
match self {
TrustedOption::Some(_) => false,
TrustedOption::None => true,
}
}
#[pure]
pub fn is_some(&self) -> bool {
!self.is_none()
}
#[pure]
#[requires(self.is_some())]
pub fn peek(&self) -> i32 {
match self {
TrustedOption::Some(val) => *val,
TrustedOption::None => unreachable!(),
}
}
}
pub struct List {
head: Link,
}
enum Link {
Empty,
More(Box<Node>),
}
struct Node {
elem: i32,
next: Link,
}
#[trusted]
#[requires(src.is_empty())]
#[ensures(dest.is_empty())]
#[ensures(old(dest.len()) == result.len())]
#[ensures(forall(|i: usize| (0 <= i && i < result.len()) ==>
old(dest.lookup(i)) == result.lookup(i)))]
fn replace(dest: &mut Link, src: Link) -> Link {
mem::replace(dest, src)
}
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)]
#[ensures(forall(|i: usize| (1 <= i && i < self.len()) ==>
old(self.lookup(i-1)) == self.lookup(i)))]
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);
}
#[ensures(old(self.len()) == 0 ==> result.is_none())]
#[ensures(old(self.len()) > 0 ==> result.is_some())]
#[ensures(old(self.len()) == 0 ==> self.len() == 0)]
#[ensures(old(self.len()) > 0 ==> self.len() == old(self.len()-1))]
#[ensures(old(self.len()) > 0 ==> result.peek() == old(self.lookup(0)))]
#[ensures(old(self.len()) > 0 ==>
forall(|i: usize| (0 <= i && i < self.len()) ==>
old(self.lookup(i+1)) == self.lookup(i)))]
pub fn pop(&mut self) -> TrustedOption {
match replace(&mut self.head, Link::Empty) {
Link::Empty => {
TrustedOption::None
}
Link::More(node) => {
self.head = node.next;
TrustedOption::Some(node.elem)
}
}
}
}
impl Link {
#[pure]
#[ensures(!self.is_empty() ==> result > 0)]
#[ensures(self.is_empty() ==> result == 0)]
#[ensures(result >= 0)]
fn len(&self) -> usize {
match self {
Link::Empty => 0,
Link::More(box node) => 1 + node.next.len(),
}
}
#[pure]
fn is_empty(&self) -> bool {
match self {
Link::Empty => true,
Link::More(box node) => false,
}
}
#[pure]
#[requires(0 <= index && index < self.len())]
pub fn lookup(&self, index: usize) -> i32 {
match self {
Link::Empty => unreachable!(),
Link::More(box node) => {
if index == 0 {
node.elem
} else {
node.next.lookup(index - 1)
}
}
}
}
}
fn main(){}
@fpoli should it be harmful to use the check_overflows=false flag? I am not interested in checking overflows for now. I see that the postconditions are still checked and the code verifies.
@fpoli should it be harmful to use the
check_overflows=falseflag? I am not interested in checking overflows for now. I see that the postconditions are still checked and the code verifies.
That flag is well tested and it even used to be the default, so there should be no issues with that.