Dafny: function unrolling

Apr 23, 2013 at 12:21 AM
I thought that Dafny would unroll function definitions on "known" input. But it does not. Here an example:

Take the predicate subsequence for lists -- as in the end of this message.

Then,, I was stuck in the following:
      var xs:= Cons(1,Cons(2, Nil));
      var ys:= Cons(2,Cons(1, Cons(1, Nil)));
     assert ! (subsequence(xs, ys))  ;    //Dafny  does not verify
I could force the above to verify by “calculations”, as follows:
      calc {
        subsequence(xs,ys);
        ==>
        subsequence(Cons(1,Cons(2, Nil)), Cons(1,Cons(1, Nil)));
        ==>
        subsequence(Cons(2, Nil), Cons(1,Cons(1, Nil)));
        ==>
        subsequence(Cons(2, Nil), Cons(1, Nil));
        ==>
        subsequence(Cons(2, Nil), Nil);
        ==
        false;
      }
      assert ! (subsequence(xs, ys))  ;    // verifies
But I would have thought that Dafny sould have unrolled the definition of “subsequence”, since it know that it terminates on finite inputs.

Cheers,

Sophia

PS And here the definitions
 predicate subsequence<T>(xs: list<T>, ys: list<T>)
{
    match xs
          case Nil => true
          case Cons(x, xs') =>
                 match ys
                     case Nil => false
                      case Cons(y, ys') =>
                                if (x == y)
                               then subsequence(xs', ys')
                               else subsequence(xs, ys')
    }
Apr 23, 2013 at 12:40 AM
Related to previous:

I tried to reason with quantifiers and induction, but several proofs which I expected should go through, did not.
I think it is has to do with the treatment of constant terms, that they are “unrolled” only one level deep.

I defined, for lists the following predicates
  • predicate elem<T>(n: T, xs: list<T>) – recursively
  • predicate subset<T>(xs: list<T>, ys: list<T>) – through universal quantifiers
    I attach the definitions at the end of this posting.
I could easily prove that subset => subsequence, quite easily,

But then, I was stuck in the following:
      var xs:= Cons(1,Cons(2, Nil));
      var ys:= Cons(2,Cons(1, Cons(1, Nil)));
     assert subset(xs,ys);   // does not verify
I then tried unrolling the definitions, and after a lot of unrolling, I could verify.

First I added
       assert forall x:: ( (elem(x,xs)) ==> (x==1 || x==2) );  // does not verify
      assert subset(xs,ys);                                                        // does not verify   
The I added
      var us:= Cons(1,Nil);
      var xs:= Cons(1,Cons(2, Nil));
      var ys:= Cons(2,Cons(1, Cons(1, Nil)));
      assert forall x:: (  elem(x,us)  ==> (x==1 )  ) ;                       // verifies
      assert forall x:: ( (elem(x,xs)) ==> (x==1 || x==2) );        // verifies
       assert subset(xs,ys);   // still does not verify
I then added some more:
      assert forall x:: (  elem(x,us)  ==> (x==1 )  ) ;
       assert forall x:: ( (elem(x,xs)) ==> (x==1 || x==2) );
      assert subset(xs,zs);
      assert subset(xs,vs);
      assert elem(2,ys);
      assert elem(1,ys);    
      assert subset(xs,ys);      // verifies
Also, instead I unrolled the definition of xs, and it worked too:
      var vs:= Cons(2,Cons(1, Nil));  
     assert subset(xs,vs);
     assert subset(xs,ys);

And here the definitions

predicate elem<T>(n: T, xs: list<T>)
{
match xs
     case Nil => false
case Cons(y, ys) => n == y || elem(n, ys)
}

predicate subset<T>(xs: list<T>, ys: list<T>)
{
forall x :: elem(x, xs) ==> elem(x, ys)
}

predicate subsequence<T>(xs: list<T>, ys: list<T>)
{
match xs
    case Nil => true
     case Cons(x, xs') =>
        match ys
                case Nil => false
                case Cons(y, ys') =>
                    if (x == y)
                   then subsequence(xs', ys')
                   else subsequence(xs, ys')
}
Coordinator
Apr 25, 2013 at 12:12 AM
Hi Sophia,

Re your first post above: Dafny applies the same rule to all uses of functions, regardless of if the arguments are given as literals. That is, they are subject to the same unwind limits. One way to change this (which I'm not currently planning on doing, but perhaps it should be done) would be to let users manually set the unwinding depth (perhaps in an attribute attached to an assert statement). A solution that would do this automatically would be nicer, but this is tricky--the function call is not known to terminate until the verifier has checked it to terminate (for example, what if the definition of subset was written to recurse forever), so one needs to invoke the verifier before one can determine if it is safe to (without any limits) partially evaluate calls.

Re your second post: You say you can prove subset ==> subsequence. Did you perhaps mean subsequence ==> subset?

In conclusion: Your various manual unrollings, asserts, and calculations are--however awkward--currently the way to prove such properties.

Rustan