class List
{
  var value:int;
  var next:List;
  
  predicate inv { acc(value) && acc(next) && (next!=null ==> next.inv) }
  
  function len():int
    requires inv;
  {
    unfolding inv in (next==null) ? 1 : (1+next.len())
  }
  
  predicate P { acc(value,50) }
  
  method skip()
    requires P; ensures P
  {}
  
  method goo()
    requires acc(value);
  {
    // mask: value=100, secmask: -
    fold P;
    // mask: value=50,p=100, secmask: value=50
    call skip();
    // mask: value=50,p=100, secmask: -
    fold P;
    // mask: value=0,p=200, secmask: value=50
    fork t:=skip();
    // mask: value=0,p=100, secmask: -
    assert unfolding P in value==old(value);
    // ERROR: Chalice currently cannot verify this example, as there is neither
    // primary nor secondary permission available to value directly before the
    // assertion
  }

}