Matching loops

Jun 24, 2013 at 11:56 PM
Hi all,

Z3 runs into a time-out when verifying the following Dafny program (I am only showing the relevant parts):
method createStudent(id: int) returns (element: StudentElement)
  ...
  ensures forall ex :: ex in this.top.extents ==> ex.Inv() &&
    forall e :: e in ex.elements ==> e.Inv(); // (1)
{
  ...
  assume forall ex :: ex in (this.top.extents - {this}) ==> ex.Inv() &&
    forall e :: e in ex.elements ==> e.Inv(); // (2)
  assert forall ex :: ex in this.top.extents ==> ex.Inv(); // (3)
  assert this in this.top.extents &&
    forall e :: e in this.elements ==> e.Inv(); // (4)
  assert forall ex :: ex in this.top.extents ==>
    forall e :: e in ex.elements ==> e.Inv(); // (5)
}
The problem is postcondition (1), which cannot be verified. To identify the bottleneck, I split up postcondition (1) into the assert statements (3), (4), and (5). Given the assume statement (2), the assert statements (3) and (4) can be verified, but not the assert statement (5). The latter causes the time-out. However, given assertion (3) and the verification of assert statements (3) and (4), I cannot possibly see why assert statement (5) is not verifiable?

I have browsed previous threads and am wondering whether assert statement (5) causes a matching loop problem. Unfortunately, I am not quite sure whether I understood the matching loop problem properly. Can anyone help?

Thanks a lot!

Stephanie
Jul 4, 2013 at 9:44 AM
Hi Stephanie,

Your steps toward debugging this issue are good (that is, adding various assume and assert statements). I agree with your assessment that it's odd that (5) does not seem to follow from (2), (3), and (4). Here are a few remarks.

The fact that you can prove (3) says that your ...'s establish that this.Inv() holds -- the rest of (3) follows from (2).

It must also be that your ...'s allow you to prove (4), since the assumption (2) does not help there.

Assuming (3) and (4), and adding some declarations to make the code snippet above compile, I am able to prove (5). See http://rise4fun.com/Dafny/YQOw. It may be that my program verifies because I give almost no details about Inv(). So, it could indeed be, as you conjecture, that something in your full example causes the SMT solver to get confused.

To continue your steps toward debugging the issue and/or finding a workaround, you can try a structure like:
    forall (ex | ex in this.top.extents)
      ensures ex.Inv() && forall e :: e in ex.elements ==> e.Inv();
    {
      forall (e | e in ex.elements)
        ensures e.Inv();
      {
        if ex == this {
          // ...
        } else {
          // ...
        }
      }
    }
which "zoom" into the various parts of the formula to be verified. If you're lucky, the way Dafny presents these proof obligations to the SMT solver may prevent the SMT solver from getting confused.

One other thing that comes to mind, but which may or may not help you, is the following. I'm guessing that your method is probably adding "this" to this.top.extents. If so, you may want to try adding a lemma like this one:
assert old(this.top.extents) == this.top.extents - {this};
If these things don't seem to help, maybe I could take a look at more of your example, in particular with the ...'s expanded.

Best wishes,
Rustan
Jul 5, 2013 at 10:09 PM
Hi Rustan,

Thank you very much for your reply!

My example is indeed more complex than the one you have come up with. In particular, there is a further layer of indirection: this is of type 'StudentExtent', which keeps its 'StudentElement' instances in its 'elements' field. Via 'top' an instance of 'StudentExtent' gets hold of a singleton instance 'StudentTop' that keeps all existing 'StudentExtent' instances in the set 'extents'. So the class structure looks like:
class StudentTop {
  var extents: set<StudentExtent>;
}
class StudentExtent {
  var elements: set<StudentElement>;
  var top: StudentTop;
  method createStudent(id: int) returns (element: StudentElement) ... {...} // see above
}
class StudentElement {
}
The invariant of 'StudentExtent' is actually trivial, the one for 'StudentElement' simple, and the one for 'StudentTop' a bit more involved. I am happy to provide the full code example if that's helpful for the discussion. Also note that in method 'createStudent()', 'this' is already contained in 'this.top.extents', i.e., it's added when it's created.

So I continued debugging my code using the 'parallel' construct (you meant PARALLEL rather than FORALL, correct?). Doing this, I was finally able to prove (5), but I came across a very strange, almost buggy behavior. Let me explain. Here is the new code excerpt that verifies:
method createStudent(id: int) returns (element: StudentElement)
  ...
  ensures forall ex :: ex in this.top.extents ==> ex.Inv() &&
    forall e :: e in ex.elements ==> e.Inv(); // (1)
{
  ...
  assume forall ex :: ex in this.top.extents ==> (ex != this ==> (ex.Inv() &&
    forall e :: e in ex.elements ==> e.Inv())); // (2) NOTE DIFFERENCE!
  assert forall ex :: ex in this.top.extents ==> ex.Inv(); // (3)
  assert this in this.top.extents &&
    forall e :: e in this.elements ==> e.Inv(); // (4)

  parallel (ex | ex in this.top.extents) // (6)
    ensures ex.Inv() && forall e :: e in ex.elements ==> e.Inv();
  {
    parallel (e | e in ex.elements)
      ensures e.Inv();
    {
      if (ex == this) {
      } else {
      }
    }
  }

  assert forall ex :: ex in this.top.extents ==>
    forall e :: e in ex.elements ==> e.Inv(); // (5)
}
Basically it looks like the if statement in the parallel block (6) enables the verification of (5), i.e., if I uncomment block (6), I get a time-out. However, note that to make the above code verifiable, I had to change (2) from
assume forall ex :: ex in (this.top.extents - {this}) ==> (ex.Inv() && forall e :: e in ex.elements ==> e.Inv()); // (2)
to
assume forall ex :: ex in this.top.extents ==> (ex != this ==> (ex.Inv() && forall e :: e in ex.elements ==> e.Inv())); // (2)
If I use the former instead, the above code results in a time-out. Likewise, if I remove the if statement from the parallel block, a time-pout occurs.

Do you have any idea what the problem is here? I am happy to provide the full program, if that would be helpful.

Thanks a lot,

Stephanie