Reasoning about what is unchanged on the heap

[kumom]

I am working on a semester project and have got stuck at verifying a method for over a month now. After trying all the tricks mentioned in this post and this section, I still encountered timeouts (> 5min). So I did some literature review, particularly reading this paper multiples times. The subsection "Existential Activation" could be the reason why I encountered timeouts, but I am not sure yet because I don't know how to inspect Z3 model efficiently.

Let me first briefly describe the problem I am encountering.

Consider a class Node with the following field:

  ghost var Repr: set<Node>
  ghost var ValueSetsVersions: seq<int>
  ghost var ValueSets: seq<set<int>> 
  
  var leftsVersions: seq<int>
  var lefts: seq<Node?>
  var rightsVersions: seq<int>
  var rights: seq<Node?>
  var valuesVersions: seq<int>
  var values: seq<int>

The specification predicates are rather sophisticated, so I'll just post what I considered relevant here for now.

There are three properties in total. BasicProp() contains some unquantified formulas and defines what Repr contains (standard definition, containing all reachable objects through lefts and right recursively and including itself). There are two other recursive predicates, let's call them Prop1() and Prop2(), which have the structure below:

  ghost predicate Prop1()
    reads Repr
    requires BasicProp() 
  {
    ... // some formula that only involves fields of `this`
    && (forall v <- lefts | v != null :: v.Prop1())
    && (forall v <- rights | v != null :: v.Prop1())
  }

This specification was validated for all functions, but hit timeouts when I tried to verify the method Insert. I first put assume false in all branches except one, i.e.,

method Insert(version: int, value: int) returns (res: Node?) 
  modifies Repr
  requires BasicProp() && Prop1() && Prop2()
  ensures BasicProp() && Prop1() && Prop2()
{
...
    if right == null {
            res := new Node.Init(version, value);        
            rights := rights + [res];
            rightsVersions := rightsVersions + [version];
    
            Repr := Repr + res.Repr;
            ValueSets := ValueSets + [ValueSet() + {value}];
            ValueSetsVersions := ValueSetsVersions + [version];
    }
...
}

After inspection, I realized I cannot verify the recursive calls from Prop1 (and similarly from Prop2)

&& (forall v <- lefts | v != null :: v.Prop1())
&& (forall v <- rights | v != null :: v.Prop1())

However, since they hold before calling the function, and the modification in this method (in this branch at least) should make this property hold still. To validate this statement, I wrote a twostate lemma which has the following predicate as the precondition:

  twostate predicate Unchanged() 
    reads Repr
    requires BasicProp() && old(BasicProp())
    requires old(ValueSetProp()) && old(BinarySearchProp())
    ensures ...
  {
    values == old(values)
    && valuesVersions == old(valuesVersions)
    && lefts == old(lefts)
    && leftsVersions == old(leftsVersions)
    && rights == old(rights)
    && rightsVersions == old(rightsVersions)
    && ValueSets == old(ValueSets)
    && ValueSetsVersions == old(ValueSetsVersions)
    && Repr == old(Repr)
    && (forall l <- old(lefts) | l != null :: l.Unchanged())
    && (forall r <- old(rights) | r != null :: r.Unchanged())
  }

Then in the twostate lemama, I used the predicate above and asserted what is changed and what is not on the heap as follows

twostate lemma InsertRight(new newNode: Node, version: int, value: int)
    requires old(BasicProp) && BasicProp() && old(Prop1()) && old(Prop2())
    // modifications
    requires Repr == old(Repr) + {newNode} 
    requires rights == old(rights) + [newNode]
    requires rightsVersions == old(rightsVersions) + [version]
    requires ValueSets == old(ValueSets) + [old(ValueSet()) + {value}]
    requires ValueSetsVersions == old(ValueSetsVersions) + [version]
    // unchanged part
    requires values == old(values)
              && valuesVersions == old(valuesVersions)
              && lefts == old(lefts)
              && leftsVersions == old(leftsVersions)
              && (forall node <- old(rights) | node != null :: node.Unchanged())
              && (forall node <- old(lefts) | node != null :: node.Unchanged())
ensures Prop1() && Prop2()
{}

If I put this lemma in the branch above, i.e.,

method Insert(version: int, value: int) returns (res: Node?) 
  modifies Repr
  requires BasicProp() && Prop1() && Prop2()
  ensures BasicProp() && Prop1() && Prop2()
{
...
    if right == null {
            res := new Node.Init(version, value);        
            rights := rights + [res];
            rightsVersions := rightsVersions + [version];
    
            Repr := Repr + res.Repr;
            ValueSets := ValueSets + [ValueSet() + {value}];
            ValueSetsVersions := ValueSetsVersions + [version];

            // ADDING:

            assume (forall node <- old(rights) | node != null :: node.Unchanged());
            assume (forall node <- old(lefts) | node != null :: node.Unchanged());
            InsertRight(res, version, value);
    }
...
}

This branch gets verified now. However, the problem is that the two assumptions above cannot be turned into assertions, because they are defined recursively, and twostate predicate cannot be used in the precondition of Insert.

Other trials I did:

1. Asserting old(Repr) == Repr does not assert "everything reachable in the set Repr stays unchanged" according to my experiment. It simply says the field Repr stays unchanged.

2. Asserting forall node <- Repr :: node == old(node) also does not work, because it will say Argument to 'old' does not dereference the mutable heap, so this use of 'old' has no effect.

3. Even after changing the modifies clause to this (this branch does not involve recursive call to Insert so it is fine), the recursive calls to Prop1 or Prop2 still cannot be verified.

My question now is: how can I state the fact that "everything that was on the heap stays unchanged" for a recursive data structure in Dafny?

My more advanced question would be: Would the timeout have to do with a similar situation that is described in the "Existential Activation" part mentioned in this paper? That is, in reasoning about the heap, there is a new skolem constant introduced by Z3, but a term involving this new skolem constant is not selected as part of the trigger by Z3 (but it should). As a user, I cannot add such a trigger myself, because I would not know what skolem constant is introduced. Are there any workarounds in Dafny when we encounter such a situation?

[keyboardDrummer]

"how can I state the fact that "everything that was on the heap stays unchanged" for a recursive data structure in Dafny?'

Can you remove modifies Repr from your Insert function? Isn't that what's telling Dafny that every field of every element in the set Repr can be changed, meaning your entire data structure can change? Have you considered using modifies this ?

What does the Insert function do? Does it only modify the Node on which it is called, or can it change any node accessible from the current one?

[kumom]

Even after changing the modifies clause to this (this branch does not involve recursive call to Insert so it is fine), the recursive calls to Prop1 or Prop2 still cannot be verified.

I tried changing to modifies this during the iteration, but it would not be correct for other branches. Basically, I am trying to verify a partially persistent binary search tree implemented with the fat node method (based on this paper). You can imagine the Insert conceptually works like insertion on usual (more precisely, ephemeral) binary search trees, except that we need to recurse on the subtree with the right version.

By replacing the recursive predicate Unchanged with forall node <- Repr | node != this && old(allocated(node)) :: unchanged(node), we managed to verify the branch in the example. However, in other branches, where I need to recursively call right.Insert(version, value) (right is a node in the sequence rights), I still encounter timeouts because of an assertion forall r <- rights, l <- lefts | r != null && l != null ensures l != r && l.Repr !! r.Repr.

My more advanced question would be: Would the timeout have to do with a similar situation that is described in the "Existential Activation" part mentioned in this paper? That is, in reasoning about the heap, there is a new skolem constant introduced by Z3, but a term involving this new skolem constant is not selected as part of the trigger by Z3 (but it should). As a user, I cannot add such a trigger myself, because I would not know what skolem constant is introduced. Are there any workarounds in Dafny when we encounter such a situation?

Do you have any ideas about this question? I tried looking around online for relevant information, but maybe I didn't even know the right keywords to begin with. Since that paper was published in 2009, I am just curious whether there has been changes in Dafny or Z3 to work around situations like this. In that paper, they said "This pattern was crucial in verification of recursive data structures in VCC". Since I am also dealing with a recursive data structure with complex sharing situation, I am wondering whether this situation also happened in my case.

[jtristan]

Without access to your code, I can only make guesses, but I do not think that the solution to your problem should involve using triggers or existential activation. In my limited experience, when I find myself wondering thinking that I need to state that "everything reachable in the set Repr stays unchanged", it is a sign that the invariant that captures the structure of the Repr is not precise enough. I think it can be very difficult to define an invariant appropriately when your Repr is a set of objects, and I would suggest defining a Repr that explicitly captures the structure of your objects. Here's an example for concreteness.

Say that I want to define a linked list. I could define it starting with something like:

  class LL<T(!new)> ... {

    ghost var Repr: set<object>

    ghost predicate Invariant()
      reads this, Repr
      decreases Repr
    {
      && (this in Repr)
      && (next != null ==> next in Repr
         && this !in next.Repr
         && next.Repr < Repr
         && next.Invariant())
    }

  }

but is is easy for me to miss on subtle aliasing that make my mental model of the data structure differ from the possible layouts (for example with cycles I did not think about).

To make my life simpler, I would instead define my linked list as:

  class Cell<T(!new)> {

    var next: Cell?<T>
    var value: T

    constructor(value: T)
      ensures this.value == value
      ensures this.next == null
    {
      this.value := value;
      next := null;
    }

  }

and

  class LL<T(!new)> {

    var length: nat
    ghost var Repr: seq<Cell<T>>      // <-- Using seq
    var hd: Cell?<T>

    ghost predicate Invariant()
      reads this, Repr
    {
      && (length == |Repr|)
      && (length == 0 <==> hd == null)
      && (length > 0 ==> Repr[0] == hd)
      && (length > 0 ==> Repr[length-1].next == null)
      && (forall idx: nat :: idx < length - 1 ==>
          Repr[idx].next != null
          && Repr[idx].next == Repr[idx+1]
         )
    }

  }

Note that I defined my Repr as a sequence of objects, rather than a set, because it is the intended layout of my data structures.
This way, I can describe the layout of my structure in a simpler way.

In your case, you cannot simply use a seq, but since the data structure you are implementing is meant to behave as if it
was purely functional, I would use an algebraic data type to implement the slow version of the structure, and then define
the Repr as a tree of objects, and therefore make the invariant more explicit (that would relate the purely functional
data structure to the persistent one).

In conclusion, I doubt that refining triggers or diving deeper into Z3 will help. The data structure that you are trying to
verify seems very challenging, and my guess is that the invariant on the layout of the Repr is complex and that structuring it
might help. If the code was public, I would be interested in taking a closer look, it seems like an interesting case study.
(In fact, if you pull it off, I would really appreciate if you could let me know about it).

[kumom]

I just got back from the exam season. The project is now public and available here. Yeah, defining Repr in a smarter way is a challenge throughout the whole project. I am not sure the way you suggested applies, because the data structure is just "meant to be" functional to the outside, but it is not functional under the hood. In fact, the functional way to achieve persistence, called path copying method, has been verified in a previous course project. The verification was almost automatic.

I will take a pause from the project first, but if you have any ideas for this problem, I will be really interested to hear as well.

[MikaelMayer]

Let me suggest you the following:

• Right after creating res, can you prove that res.Prop1() ?
• Also, at the same point, can you prove that fresh(res.Repr)? Dafny does not do clever tracing, so unless explicitly stated, your new object might have a Repr that includes "this" and creates a circular data structure.

Not sure how much it is relevant but also:

• You can also apply the techniques of this section when verification fails to also identify what Dafny really has a hard time proving. You can also use the method/function attribute {:rlimit 3000} to force Dafny to stop after a certain resource limit, and {:vcs_split_on_every_assert} to let Dafny isolate every assertion separatedly. I found this extremely useful to isolate timeouts, because you can hover on assertions and see which ones take the most resource units, while ensuring this number does not exceed an arbitrary threshold.
• To prove an assert forall x <-C :: x.A() when C has been increasing, you normally write a forall statement with an ensures x.A(), and since you are increasing collection, you'd typically introduce the disjunction inside like if x in old(C) { assert x.A(); } else { assert x.A(); }

[kjx]

a more concrete suggestion (although I'm sure the original problem must be long solved).
when I've had similar problems, rather than just make a big predicate that does everything
I've made a much smaller (recursive) predicate that collects up the "footprint" of everything I care about:

function allTheEnvsSet(s : Region) : set<Object>
{
 if (s.Frame?)
     then {s.env} + allTheEnvsSet(s.prev)
     else {}
}

and then I can use that in reads or modifies clauses directly:

   reads allTheEnvsSet(s)