Linked List insertion

[CodeNinja89]

So now I have started having bad dreams about this problem. I followed Rustan Leino's paper and implemented the linked list example from the same. The example clearly explains the concept of dynamic frames but inserting a node in the middle of the queue is not trivial.

In the paper, when the node is appended at the end of the list, the footprints of all the nodes in the list are updated to reflect that the new node is reachable from everywhere. A simple "forall" does the trick. However, Inserting in the middle is tricky because we have to tell Dafny that this new node is reachable "only from the nodes before it". I tried the following:

class Node {
    var data: int
    var next: Node?
    
    ghost var footprint: set<object>
    ghost var contents: seq<int>
    
    ghost predicate valid()
        reads this, footprint
    {
        this in footprint &&
        (next != null ==> next in footprint &&
            next.footprint <= footprint &&
            this !in next.footprint &&
            next.valid()) &&
        (next == null ==> |contents| == 0 &&
            next != null ==> next.contents == contents[1..])
    }
    
    constructor()
        modifies this
        ensures valid() && fresh(footprint - {this})
        ensures next == null
        ensures |contents| == 0
    {
        next := null;
        contents := [];
        footprint := {this};
    }
    
    method enqueueMid(d: int, pos: int)
        requires valid()
        requires 0 <= pos < |contents|
        modifies footprint
        ensures valid() && fresh(footprint - old(footprint))
    {
        var i: int := 0;
        var curr := this;
        
        while(i < pos && curr.next != null)
            invariant curr != null
            invariant curr != null ==> curr.valid()
            decreases if curr != null then curr.footprint else {}
        {
            i := i + 1;
            curr := curr.next;
        }
        
        var n := new Node();
        n.data := d;
        
        if(curr == null) {
            curr := n;
            contents := contents + [d]; // if current is null then we have reached the end of the list!
        } else {
            n.next := curr.next;
            n.footprint := n.footprint + curr.footprint - {curr}; // acyclicity!
            curr.footprint := curr.footprint + n.footprint;
            curr.next := n;
            contents := contents[ .. pos] + [d] + contents[pos ..];
        }
        
        footprint := footprint + n.footprint;
        assert(valid()); // could not prove: next.valid()
    }
}

The final assertion gives me an error. As I understood, this error asks me to show Dafny that next node following the new node remains valid. After a bit of reading and later a discussion on stackoverflow, I understood that after the insert operation, Dafny cannot reason about the validity of the nodes already present in the footprint.

To overcome this, the solution provided on SO was to collect the nodes parsed along the way and then update the footprint of each node. This is cool but again, Dafny cannot reason about the fact that the footprint of a node is a subset of the footprint of its previous node and therefore an assumption was made.

I think using a twostate lemma (or function (or method)) might solve the problem because it will allow me to reason about the fact that, between the updates, the footprint of a node is a subset of the footprint of its previous node holds. I may be wrong and that brings me to my question:

1. An explanation about the concept of twostate lemma (or function (or method)). I have read the Dafny documentation and also a discussion but did not understand it very clearly. An example of how (if it can be) can I use it in completing my linked list insertion would be really appreciated.
2. I made another attempt and it verifies but I don't think this is correct. For instance, when I try to implement a Main function and add the a node at position 0, the pre-condition of the enqueue method fails saying "cannot prove pos < |contents|". And that is expected because the linked list is initially empty.

[MikaelMayer]

This is an excellent problem.
I think you have a loss of information from your while loop, where curr is set to an object after the end of the while loop but since while loops are like mini-methods, the only postcondition available for the variables it modifies are the invariant and the negation of the guard.

So basically, after the while loop, Dafny can only prove about curr that

!(i < pos && curr.next != null)
&& curr != null;
&& curr.Valid()

which, as you can guess, is not useful in any way because curr has no relationship in this formula with the current "this".

The solution is to strengthen the invariant so that you know exactly what curr is. It's the i-th object of the collection, right?
The problem is, the footprint is a set in your model. Make it a sequence, and have your Valid() state that the footprint of every node in the sequence is itself plus the remaining nodes.
Now you can add the following invariant:

invariant curr == this.footprint[i]

and you don't have information loss.

Try with the following much stronger invariant:

    ghost var footprint: seq<Node>
    ghost var contents: seq<int>
    
    ghost predicate valid()
        reads this, footprint
        decreases |footprint|
    {
        (forall i | 0 <= i < |footprint| ::
          && footprint[i].footprint == footprint[i..])
        && (forall i | 0 < i < |footprint| ::
          && footprint[i].valid())
        && if next == null then
             && contents == []
             && footprint == [this]
           else
             && |footprint| >= 2 && footprint[1] == next
             && footprint == [this] + next.footprint
             && contents == [next.data] + next.contents
    }

To convert a seq to a set, use (set x <- your_seq) if you need

[CodeNinja89]

Hi Mikael, thanks for your help!

I tried it with your invariant. The verification times out. Here is my attempt.

class Node {
    var data: int
    var next: Node?


    ghost var contents: seq<int>
    ghost var footprint: seq<Node>

    ghost predicate valid()
        reads this, footprint
        decreases |footprint|
    {
        (forall i | 0 <= i < |footprint| ::
            footprint[i].footprint == footprint[i ..]) &&
        (forall i | 0 < i < |footprint| ::
            footprint[i].valid()) &&
        if next == null then
            contents == [] && footprint == [this]
        else
            |footprint| >= 2 && footprint[1] == next &&
            footprint == [this] + next.footprint &&
            contents == [next.data] + next.contents
    }

    constructor(d: int)
        ensures valid()
        ensures footprint == [this]
        ensures contents == []
        ensures data == d && next == null
    {
        data := d;
        next := null;
        footprint := [this]; // sentinel node
        contents := [];
    }

    method enqueue(d: int, pos: nat)
        requires valid()
        requires 0 <= pos < |footprint| // not contents?
        modifies this, footprint
        ensures valid()
    {
        /* ghost */ var i: nat := 0;
        var curr := this; // start at the head

        while(i < pos && curr.next != null)
            invariant 0 <= i < |footprint|
            invariant curr != null
            invariant curr.valid()
            invariant curr == this.footprint[i]
            decreases if curr != null then curr.footprint else [] // or |footprint| - i but proving termination this way is not... "explainable"?
        {
            curr := curr.next;
            i := i + 1;
        }

        var n := new Node(d);
        n.next := curr.next;

        if curr.next != null {
            n.footprint := [n] + curr.next.footprint;
            n.contents := [curr.next.data] + curr.next.contents;
        }

        assert curr == footprint[i] && curr.valid();
        // assert n.valid();

        curr.next := n;
        // assert curr == footprint[i];
        assert curr.next.data == n.data;
        assert curr.next.footprint == n.footprint;

        footprint := footprint[.. i + 1] + [n] + footprint[i + 1 ..];
        assert n in footprint;

        // here we roll back all the way to the head to update the footprints and contents of all the nodes
        // IMO, we don't need to reason about the footprints and contents of the successor nodes of n
        // because they are not updated.
        // logically this loop seems ok but the verification times out.

        while i >= 0
            invariant i < |footprint|
            invariant footprint[i].valid()
            invariant footprint[i] != null
            decreases i
        {
            footprint[i].footprint := [footprint[i]] + footprint[i].next.footprint;
            footprint[i].contents := [footprint[i].next.data] + footprint[i].next.contents;
            i := i - 1;
        }
    }
}`

[MikaelMayer]

Whenever verification times out, the following annotation on the method will be your friend:

    method {:vcs_split_on_every_assert} {:rlimit 200} enqueue(d: int, pos: nat)

This will isolate every assertion and assign an arbitrary resource limit to each of them, so that you will quickly see in the gutter which assertions are timing out exactly, and work on them

After doing that, it looks like the assertion it can't prove is the following:

assert curr == footprint[i] && curr.valid();

One thing you can do to iterate faster is to use the {:only} attribute like this

    assert {:only} curr == footprint[i] && curr.valid();

so now, everything else will be assumed.
You can now copy-paste this assertion in places before where it's supposed to hold.
And you'll discover that this assertion unexpectedly fails after the assignment to n.footprint.
Hovering over the two constructs, you see that the first one is proved, but the second one curr.valid() is not longer proved. Does not mean it's wrong, just Dafny needs some hints.
Since curr.valid reads curr and curr.footprint, we need to ensure n is not in curr.footprint and n is not curr. So you add

    assert {:only} curr != n;
    assert {:only} n !in curr.footprint;

Then you realize on hovering that it can prove both things, so you turn back on hovering curr.valid() and try to understand why it fails. It fails at proving a sub-portion
This is where you can use the opaque trick. By making the valid() predicate opaque, you ensure Dafny does not try to prove sub-components of things you know are true, because the problem is, when assuming valid(), Dafny assumes each individual component, and when proving valid(), it tries to prove each individual components.

So transforming valid() to:

opaque ghost predicate valid()

solves the issue you were facing and now you just need to prove the validity by using reveal valid(); in places where you can't prove validity other than just looking at the definition

But let's say you don't want to make validopaque. You want to get to the gist of it and help Dafny to prove what it wants. When you hover over the failing curr.valid(), Dafny tells you exactly what it cannot prove. You'll get:

forall i | 0 < i < |curr.footprint| :: curr.footprint[i].valid()

To prove this, you add a forall statement just before:

    forall i | 0 < i < |curr.footprint| ensures curr.footprint[i].valid() {
    }

Because there is no {:only} on ensures yet, you convert the first {:only} to {:only "after"} and the last {:only} to {:only "before"} and remove all intermediates only.

You also realize that valid() was true before the assignment, but for it to be true after the assignment, you need to prove that n was not part of the footprint of curr.footprint[i]:

        assert n != curr.footprint[i];
        assert n !in curr.footprint[i].footprint;

but that's useless, because the thing it cannot prove is actually a ... sub-component of curr.footprint[i].valid(). Stupid proving engine.
So you're back now to making valid() opaque.

But oh, you can also do something else: Make functions opaque and revealed by default. This has the nice side-effect that Dafny won't try to be clever by inlining the content of the function for proving it.

So create a dfyconfig.toml and add in it

[options]
default-function-opacity="autoRevealDependencies"

and let me know how it goes!

[CodeNinja89]

What an answer! Crisp and clear explanation of the problem. It seems I was on the right track since I first attempted the problem. From what I understood, the trick with the opaque predicate basically tells Dafny "this part is obviously true, so don't bother".

[CodeNinja89]

I implemented the opaque valid and now I have some more questions. My implementation is here.

It seems to work and I checked with a Main method. But, the last while loop where I update the footprints of all the previous nodes becomes spurious. I think it is needed because otherwise how do I prove that the validity of the Queue is preserved? After all the whole predicate is based on footprint.

Also, if I remove the statement assert {:only} curr == footprint[i] && curr.valid(); or remove the ":only" from this assert, the verification breaks. I think it is the lack of understanding of opaque predicates but I'd rather ask and be judged.

Moreover, it doesn't matter where I place the reveal valid() inside the enqueue method, it always verifies... even without the last while loop. And that is what bothers me. Because I don't see how the validity holds even when the old footprints are not updated. In fact, I had to add ensures fresh(footprint)to get the main method work. But since I'm now not updating the footprints explicitly, how is the footprint "fresh"?

It will be a good lesson in Dafny if you can clarify these doubts.

[MikaelMayer]

{:only} focuses verification, so it's ok that verification breaks elsewhere when you remove it. You even get a warning saying that other assertions will be ignored. And of course, when you remove it, it no longer will pretend to prove valid() because you indeed have to modify all the other footprints

You might want to create a recursive ghost method to update all the footprints, it might be easier to specify, but otherwise you can also use a forall statement to update all the footprints at once.

When function or a predicate is opaque, it's jus that, for the solver, there is an axiom to get the definition only if it knows that a "reveal" parameter is true. When you call reveal, you just assume this parameter is true, so you only need to do this before the first time you need the body of the function to be revealed.

[CodeNinja89]

Ok... that makes a lot of sense. From what I read in the documentation it seemed that {:only "after"} solved the issue by asserting everything that follows "only after" the current assertion. That's not the case though, is it?

For example, in this update, after removing the "only"'s, I saw that current.footprint := [curr] + n.footprint; from my previous version is wrong (error: "value of expression (of type 'seq<Node?>') is not known to be an instance of type 'seq'"). The correct statements should be: current.footprint := [n] + curr.footprint;

It wasn't caught in the previous version because the "only after" assumes the rest of the assertions to focus the verification.

In this update, I have removed all the "only" assertions and seemed to progress much further. The final hurdle though is to update all the footprints. As you suggested, I tried to update the footprints using a forall statement like this:

forall j | 0 <= j < |footprint| {
    footprint[j].footprint := footprint[j ..];
}

I get an error: left-hand sides for different forall-statement bound variables might refer to the same location. Googling doesn't shed any light on this error.

Thank you for this discussion. I have learned more through this discussion than going through all kinds of papers and documentation.