New failure on small linked list example

[alexanderjsummers]

The following example previously worked on a Prusti install I have here, but after running "Prusti: update dependencies" I get a failure for the postcondition on push:

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

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

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

  #[ensures(self.len() == old(self.len()) + 1)]
  fn push(&mut self, v:i32) {
    match self.next {
      None => self.next = Some(box List { val : v, next : None}),
      Some(box ref mut tail) => tail.push(v)
    }
  }
}

[alexanderjsummers]

Interestingly, if one removes the val field from the program, the analogous program verifies. I guess this must either be a back-end issue or an issue with the snapshots encoding:

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

struct List {
  next : Option<Box<List>>
}

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

  #[ensures(self.len() == old(self.len()) + 1)]
  fn push(&mut self) {
    match self.next {
      None => self.next = Some(box List { next : None}),
      Some(box ref mut tail) => tail.push()
    }
  }
}

[fpoli]

This might be the same thing that happened in #583. Aurel explained:

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.

[alexanderjsummers]

Thanks for the speedy response! As far as I can tell this doesn't seem to be an example in which triggering unfoldings of function definitions should be particularly problematic; the convenient strategy from Viper only makes a difference over limited functions (which should still be working) if one needs unfolding to more than depth 1, and that doesn't seem to arise in this example.

[JonasAlaif]

After a bit of playing around with the Viper I've reduced the example to:

domain Snap$Option {
  function List_next_disc(self: Snap$Option): Bool
  
  function Snap_None(): Snap$Option
  
  function Snap_Some(_0: Snap$List): Snap$Option
  
  function snap_Option_Some(self: Snap$Option): Snap$List
  
  axiom Snap$Option$0$discriminant_axiom {
    !List_next_disc(Snap_None())
  }
  
  axiom Snap$Option$1$discriminant_axiom {
    (forall _0: Snap$List :: { Snap_Some(_0) } List_next_disc(Snap_Some(_0)))
  }
  
  axiom Snap$Option$1$field$f$0$axiom {
    (forall _0: Snap$List :: { snap_Option_Some(Snap_Some(_0)) } snap_Option_Some(Snap_Some(_0)) == _0)
  }
}

domain Snap$List {
  function Snap_List(_0: Int, _1: Snap$Option): Snap$List

  function snap_List_next(self: Snap$List): Snap$Option
  
  axiom Snap$List$0$field$next$axiom {
    (forall _0: Int, _1: Snap$Option :: { snap_List_next(Snap_List(_0, _1)) } snap_List_next(Snap_List(_0, _1)) == _1)
  }
}

field is_some: Bool
field enum_Some: Ref
field next: Ref
field val: Int

function get_is_some(self: Ref): Bool
  requires acc(Option(self), read())
  ensures List_next_disc(to_snap_OptBoxList(self)) == result
{
  unfolding acc(Option(self), read()) in self.is_some
}

function len(_1: Snap$List): Int
{
  !List_next_disc(snap_List_next(_1)) ? 1 : 1 + len(snap_Option_Some(snap_List_next(_1)))
}

function to_snap_OptBoxList(self: Ref): Snap$Option
  requires acc(Option(self), read())
{
  unfolding acc(Option(self), read()) in (self.is_some ? Snap_Some(to_snap_List(self.enum_Some)) : Snap_None())
}

function to_snap_List(self: Ref): Snap$List
  requires acc(List(self), read())
{
  unfolding acc(List(self), read()) in Snap_List(self.val, to_snap_OptBoxList(self.next))
}

function read(): Perm
  ensures none < result
  ensures result < write


predicate Option(self: Ref) {
  acc(self.is_some, write) && acc(self.enum_Some, write) && (self.is_some ==> acc(List(self.enum_Some), write))
}

predicate List(self: Ref) {
  acc(self.val, write) && acc(self.next, write) && acc(Option(self.next), write)
}

method m_push(l: Ref) returns ()
  requires acc(List(l), write) && unfolding acc(List(l), write) in !get_is_some(l.next)
{
  var l2: Ref

  inhale acc(Option(l2), write)
  inhale get_is_some(l2)

  unfold acc(Option(l2), write)
  inhale acc(List(l2.enum_Some), write)
  unfold acc(List(l2.enum_Some), write)
  inhale acc(Option(l2.enum_Some.next), write)

  inhale !get_is_some(l2.enum_Some.next)

  fold acc(List(l2.enum_Some), write)

  //assert len(to_snap_List(l2.enum_Some)) == 1

  fold acc(Option(l2), write)

  unfold acc(List(l), write)
  l.next := l2
  fold acc(List(l), write)

  assert len(to_snap_List(l)) == old(len(to_snap_List(l))) + 1
}

This fails on the final assert, but if one un-comments the assert a few lines before, then verification succeeds. Seems to be a Viper issue, probably something with triggering? Also noticed the same, with that if the val field is removed then it always succeeds for some reason.