Timeouts on complex invariants

Feb 26, 2013 at 5:23 AM
Hello,

I'm continuing to work on the ArraySet example, which we've seen in a couple other posts. It involves threading a "free" list and a "used" list through an array and you can view it as a "toy" memory allocator. I use some ghost sequence variables to describe these elements.

I'm at the trickiest bit, which involves swapping an element from one list to another. I have a "swap" function that does the operation, and should preserve the invariant. However, I'm having difficulty with Dafny timing out; I can split the postconditions across two swap functions and get it to work, but if I put everything together it appears to run aground. Here are the two swap functions:
method swap1(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>) 
    modifies this;
    modifies nextArray;
    requires seqOk(hd, bs);
    requires |bs| > 0 ;
    requires 0 <= split < |bs| ;
    requires |bs| <= nextArray.Length; 
    requires 0 <= newSlot < nextArray.Length;
    requires newSlot !in bs;

    ensures |bs'| > 0 ; 

    // the properties I care about for seqOk
    ensures nextArray != null; 
    ensures (forall i, j :: (0 <= i < |bs'| && 0 <= j < |bs'| && i != j) ==> bs'[i] != bs'[j]);
    ensures (hd == -1 <==> |bs'| == 0) ;
    ensures (forall j :: j in bs' ==> (j >= 0 && j < nextArray.Length));        
    ensures (|bs'| > 0 ==> ((hd == bs'[0])));  

    // need to prove the 'ensures' below separately or I time out; see swap2.  The 
    // necessary assertions for proof are commented out below.
    //
    // ensures (nextArray[lastElem(bs')] == -1);

{

    var splitLoc := bs[split]; 

    nextArray[newSlot], nextArray[splitLoc] := nextArray[splitLoc], newSlot ;  
    //assert ((split == |bs|-1) ==> (nextArray[newSlot] == -1)); 
    bs' := bs[..split+1] + [newSlot] + bs[split+1..]; 
    //assert((split == |bs'|-1) ==> (nextArray[lastElem(bs')] == -1)); 
    //assert (|bs'| > 0 ==> (nextArray[lastElem(bs')] == -1)); 
    assert(bs'[split+1] == nextArray[bs'[split]]) ; 
    assert (forall j :: 1 <= j <= split ==> nextArray[bs'[j-1]] == bs'[j]);
    assert (forall j :: split+1 < j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]); 
    assert (forall j :: 1 <= j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]);
    assert (forall i, j :: (0 <= i < |bs'| && 0 <= j < |bs'| && i != j) ==> bs'[i] != bs'[j]);
    assert ((hd == -1) == (|bs'| == 0)) ;
    assert (forall j :: j in bs' ==> (j >= 0 && j < nextArray.Length));     
    assert (|bs'| > 0 ==> ((hd == bs'[0])));  
}


method swap2(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
    modifies this;
    modifies nextArray;
    requires seqOk(hd, bs);
    requires |bs| > 0 ;
    requires 0 <= split < |bs| ;
    requires |bs| <= nextArray.Length; 
    requires 0 <= newSlot < nextArray.Length;
    requires newSlot !in bs;

    ensures |bs'| > 0 ; 
    ensures nextArray != null;
    ensures 0 <= lastElem(bs') < nextArray.Length;

    // this is the one I actually care about.
    ensures (nextArray[lastElem(bs')] == -1);
{

    var splitLoc := bs[split]; 

    nextArray[newSlot], nextArray[splitLoc] := nextArray[splitLoc], newSlot ;  
    assert ((split == |bs|-1) ==> (nextArray[newSlot] == -1)); 
    bs' := bs[..split+1] + [newSlot] + bs[split+1..]; 
    assert((split == |bs'|-1) ==> (nextArray[lastElem(bs')] == -1)); 
    assert (|bs'| > 0 ==> (nextArray[lastElem(bs')] == -1)); 
    // yay!
}
The entire program is below. My guess is that as I add assertions for one conjunct, I'm accreting junk that is causing Dafny to go astray when trying to prove the other things. Is there any way to localize assertions as relevant only for one thread of proof?

Thanks again!

Mike

class ArraySet {

var elementArray : array<int>;
var nextArray: array<int>;
var usedHd: int;
var freeHd: int;
ghost var usedSeq: seq<int> ;
ghost var freeSeq: seq<int> ;

// Invariant for array creating a simple store. You can think of it as a grossly simplified
// memory allocator. Each memory location (array slot) is either part of a "free list" or a
// "used list". Both lists are threaded through the structure of the array. We used a
// variant of this structure for a high-speed encryption application.

predicate index_ok(index: int)
reads this;
reads nextArray ; 
{
nextArray != null && index >= 0 && index < nextArray.Length
}

function lastElem(input: seq<int>) : int
requires |input| > 0; 
{
input[|input| - 1]
}

predicate seqOk(hd: int, theSeq: seq<int>)
reads this;
reads nextArray; 
{
nextArray != null &&
(forall i, j :: 0 <= i < j < |theSeq| ==> theSeq[i] != theSeq[j]) &&
(hd == -1 <==> |theSeq| == 0) &&
(forall j :: j in theSeq ==> j >= 0 && j < nextArray.Length) &&
(forall j :: 1 <= j < |theSeq| ==> nextArray[theSeq[j-1]] == theSeq[j]) && 
(|theSeq| > 0 ==> hd == theSeq[0] && nextArray[lastElem(theSeq)] == -1)
}

predicate arrayInv()
reads this;
reads nextArray; 
reads elementArray;
{
nextArray != null &&
elementArray != null && 
(forall j :: 0 <= j < nextArray.Length ==> -1 <= nextArray[j] < nextArray.Length) && 
-1 <= freeHd < nextArray.Length && 
-1 <= usedHd < nextArray.Length && 
nextArray.Length == elementArray.Length && 
nextArray != elementArray &&

// usedSeq & freeSeq are well formed and correctly mapped to the nextArray
seqOk(usedHd, usedSeq) && 
seqOk(freeHd, freeSeq) && 

// sequences contain no duplications, are disjoint, and exhaustive
(forall j :: 0 <= j < nextArray.Length ==> j in usedSeq || j in freeSeq) && 
(forall j :: j in usedSeq ==> j !in freeSeq) &&
(forall j :: j in freeSeq ==> j !in usedSeq) &&

true
}

method init(size: int)
modifies this; 
requires size > 0;
ensures nextArray != null;
ensures forall j :: 0 <= j < nextArray.Length ==> -1 <= nextArray[j] < nextArray.Length;
ensures arrayInv();
{
elementArray := new int[size];

nextArray := new int[size];
parallel (j | 0 <= j < nextArray.Length) {
  nextArray[j] := if j < nextArray.Length - 1 then j + 1 else -1;
}

usedHd := -1;
freeHd := 0;
usedSeq := []; 

var fs, i := [], 0;
while (i < nextArray.Length)
  invariant 0 <= i <= nextArray.Length;
  invariant |fs| == i;
  invariant forall j :: 0 <= j < i ==> fs[j] == j;
{
  fs, i := fs + [i], i + 1;
}
freeSeq := fs;
// lemma needed to make the postcondition go through:
assert forall j :: 0 <= j < nextArray.Length ==> freeSeq[j] == j ==> j in freeSeq;
}
method insertHd(n: int) returns (result: bool)
    modifies this;
    modifies nextArray;
    modifies elementArray;
    requires arrayInv();
    ensures arrayInv();
{
    var oldUsedHd : int;

    if (freeHd != -1) {
        // assign usedHd to freeHd; if I get rid of oldUsedHd (using parallel assignment), proof fails.  Why?
        oldUsedHd := usedHd; 
        usedHd, freeHd := freeHd, nextArray[freeHd];
        nextArray[usedHd] := oldUsedHd; 

        // assign the next pointer of the first used element to the previous head of the used list
        elementArray[usedHd] := n;

        usedSeq := [freeSeq[0]] + usedSeq;
        freeSeq := freeSeq[1..];
        assert (|usedSeq| > 1 ==> nextArray[usedSeq[0]] == usedSeq[1]) ; 
        result := true;
    } else {
        result := false;
    }
} 

/*
    swap: add the newSlot array location into the list represented by sequence bs.
        Steps: 
            Find the location for insert (splitLoc), 
            update the next pointers, and
            update the sequence to match.

        Swap should preserve the seqOk invariant, but it times out when I try to 
        prove the pieces all at once.  Temporarily, I am proving the conjuncts 
        separately with swap1 and swap2, but both these operations are destructive
        of the heap, so this won't work for "real"; Dafny is able to prove the 
        pieces, but when I put them together, I think it gets overloaded by the volume
        of information for each conjunct.  I'm looking for a way to separate the 
        proof into separate paths of execution here.
*/

method swap1(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
    // swap1 code HERE

method swap2(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
            // swap2 code HERE

method insertTl(n: int) returns (result: bool)
    modifies this; 
    modifies nextArray;
    modifies elementArray;
    requires arrayInv();
    requires usedHd != -1; 
{
    // array location and sequence location for insert.
    var al := usedHd; 
    ghost var sl := 0;

}

method insert(n: int) returns (result: bool)
    modifies this;
    modifies nextArray;
    modifies elementArray;
    requires arrayInv();
    ensures arrayInv();
{
    if (freeHd == -1) {
        result := false;
        return; 
    } else if (usedHd == -1 || n < elementArray[usedHd]) {
        result := insertHd(n) ;
        assert (arrayInv()); 
        return; 
    } else {
        // find location and perform a swap HERE.
        return;
    }
}
}
Feb 27, 2013 at 6:11 PM
FYI, I think I have it figured out.

Calc came to the rescue here for me. I am not entirely sure that I'm using it correctly, but it looks like I can factor intermediate results using calc to prevent Dafny from going into the weeds. Is this an appropriate way to use calc? I couldn't find much documentation, so I'm just using my gut here.

method swap(bs: seq<int>, newSlot: int, split: int, hd: int) returns (bs': seq<int>)
    modifies this;
    modifies nextArray;
    requires seqOk(hd, bs);
    requires |bs| > 0 ;
    requires 0 <= split < |bs| ;
    requires |bs| <= nextArray.Length; 
    requires 0 <= newSlot < nextArray.Length;
    requires newSlot !in bs;

    ensures |bs'| > 0 ; 

    // the properties I care about for seqOk
    ensures nextArray != null; 
    ensures seqOk(hd, bs'); 
{

    var splitLoc := bs[split]; 

    nextArray[newSlot] := nextArray[splitLoc] ;
    nextArray[splitLoc] := newSlot ;  
    assert ((split == |bs|-1) ==> (nextArray[newSlot] == -1)); 
    bs' := bs[..split+1] + [newSlot] + bs[split+1..]; 
    calc {
        (forall i, j :: (0 <= i < |bs'| && 0 <= j < |bs'| && i != j) ==> bs'[i] != bs'[j]);
        (forall i, j :: 0 <= i < j < |bs'| ==> bs'[i] != bs'[j]) ; 
    }
    assert ((hd == -1) <==> (|bs'| == 0)) ;
    calc {
        (bs'[split+1] == nextArray[bs'[split]]) ;
        (forall j :: 1 <= j <= split ==> nextArray[bs'[j-1]] == bs'[j]);
        (forall j :: split+1 < j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]);
        (forall j :: 1 <= j < |bs'| ==> nextArray[bs'[j-1]] == bs'[j]);
    }
    assert (forall j :: j in bs' ==> (j >= 0 && j < nextArray.Length));     
    calc {
        (|bs'| > 0 ==> ((hd == bs'[0])));  
        ((split == |bs'|-1) ==> (nextArray[lastElem(bs')] == -1)); 
        (|bs'| > 0 ==> (nextArray[lastElem(bs')] == -1)); 
        (|bs'| > 0 ==> ((hd == bs'[0]) && (nextArray[lastElem(bs')] == -1)));  
    }
    assert seqOk(hd, bs');
}
Mar 1, 2013 at 9:07 PM
I'd like to register my interest in this issue too!! Specifically...

I've been working on a sequence-based example (the longest upsequence), with heavy use of an "isSubsequence" function, and I've layered the code so that the actual program uses only ghost methods in the complicated reasoning about the subsequences, and only those ghost methods "know" just how isSubsequence is defined. Now here's the thing...

I can compile the ghost methods, on their own, with a variety of definitions of isSubsequence (altering the ghost methods' bodies accordingly), and all is fine. But when I add the main program back (which uses those ghost methods), most of my isSubsequence definitions either cause dafny to loop or general several minutes' worth of compilation time.

So encapsulating the isSubsequence definition would be a good idea. Is it possible?