Add Skolem functions to QP framing axioms

[jwkai]

This modifies the axiom used to frame heap-dependent functions and predicates with Set arguments based on quantified permissions.

The following explanation also exists in #522. We noticed that in the existing generated axiom, the LHS quantified formula that will become a negated existential on the left of a disjunction. For example:

// ==================================================
// Function used for framing of quantified permission (forall a: Ref, i: Int :: { two(a, i) } (a in as) && (i in is) ==> acc(two(a, i), write)) in function foo_twos
// ==================================================

function  foo_twos#condqp(Heap: HeapType, vas_1_1: (Set Ref), vis_1_1: (Set int)): int;

axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, vas: (Set Ref), vis: (Set int) ::
  { foo_twos#condqp(Heap2Heap, vas, vis), foo_twos#condqp(Heap1Heap, vas, vis), succHeapTrans(Heap2Heap, Heap1Heap) }
  (forall a: Ref, i: int ::
    
    ((vas[a] && vis[i]) && NoPerm < FullPerm <==> (vas[a] && vis[i]) && NoPerm < FullPerm) && ((vas[a] && vis[i]) && NoPerm < FullPerm ==> 
      Heap2Heap[null, two(a, i)] == Heap1Heap[null, two(a, i)])
  ) ==> foo_twos#condqp(Heap2Heap, vas, vis) == foo_twos#condqp(Heap1Heap, vas, vis)
);

This generates new Skolemized indices for a: Ref and i: Int for each triggering of the outer quantified variables Heap2Heap: HeapType, Heap1Heap: HeapType, vas: (Set Ref), vis: (Set int).

However, there may be some prior equalities between the given heap-dependent term across other heaps. For example, if

foo_twos#condqp(Heap3Heap, vas, vis) == foo_twos#condqp(Heap2Heap, vas, vis)

then it is undesirable to generate distinct Skolemized indices for both triggerings of the QP axiom:

{ foo_twos#condqp(Heap3Heap, vas, vis), 
  foo_twos#condqp(Heap1Heap, vas, vis), 
  succHeapTrans(Heap3Heap, Heap1Heap) }

and

{ foo_twos#condqp(Heap2Heap, vas, vis), 
  foo_twos#condqp(Heap1Heap, vas, vis), 
  succHeapTrans(Heap2Heap, Heap1Heap) }

My modification defines a more general Skolem function for each quantified variable, taking applications of the heap-dependent function or predicate, in order to share witness indices. It substitutes these Skolem functions for the quantified variables in the LHS of the implication. For example:

// ==================================================
// Function used for framing of quantified permission (forall a: Ref, i: Int :: { two(a, i) } (a in as) && (i in is) ==> acc(two(a, i), write)) in function foo_twos
// ==================================================

function  foo_twos#condqp(Heap: HeapType, vas_1_1: (Set Ref), vis_1_1: (Set int)): int;
function  sk_foo_twos#condqp48(fnAppH1: int, fnAppH2: int): Ref;
function  sk_foo_twos#condqp48_1(fnAppH1: int, fnAppH2: int): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, vas: (Set Ref), vis: (Set int) ::
  { foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis), succHeapTrans(Heap2Heap, Heap1Heap) }
  ((vas[sk_foo_twos#condqp48(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))] && vis[sk_foo_twos#condqp48_1(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))]) && NoPerm < FullPerm <==> (vas[sk_foo_twos#condqp48(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))] && vis[sk_foo_twos#condqp48_1(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))]) && NoPerm < FullPerm) && ((vas[sk_foo_twos#condqp48(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))] && vis[sk_foo_twos#condqp48_1(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis))]) && NoPerm < FullPerm ==> 
      Heap2Heap[null, two(sk_foo_twos#condqp48(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis)), sk_foo_twos#condqp48_1(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis)))] == Heap1Heap[null, two(sk_foo_twos#condqp48(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis)), sk_foo_twos#condqp48_1(foo_twos#condqp48(Heap2Heap, vas, vis), foo_twos#condqp48(Heap1Heap, vas, vis)))]
  ) ==> foo_twos#condqp48(Heap2Heap, vas, vis) == foo_twos#condqp48(Heap1Heap, vas, vis)
);

We tested this on examples with heap-modifying statements both relevant and irrelevant to a given heap-dependent function application. We found that the verification times scale roughly with the number of relevant heap-modifying statements, whereas the original axiom scales with the total (relevant and irrelevant) number of heap-modifying statements.

[marcoeilers]

Hi, thank you for your contribution and sorry it took so very long to get a response.
It took me a bit to understand both why the change helps and why the rewriting is equivalent, but I'm convinced now, and the code looks good to me as well.
Out of curiosity, do you have a "real" (as in, not artificial) example for which this leads to a significant speedup? I'd be interested in having a look at one if you do.

[jwkai]

Hi Marco,

No worries, I admit it took me a while to understand (and even longer to implement) as well! Alex Summers is really to credit for this idea.

Below is a "real" example of Viper code that led to this axiom modification. There is a Viper source (arrayTestChainIrrel3.viper), the Boogie file generated by Carbon (arrayTestChainIrrel3_sk.bpl) and the modified Boogie file with Skolemization (arrayTestChainIrrel3_nosk.bpl)

It's rather unreadable, but I believe the Viper should verify (under Carbon only, not Silicon, since it relies on heap-dependent triggers). And the Skolemized Boogie code should verify faster than the original. Please let me know if otherwise, this was all automatically generated code (even the Viper, by a plug-in that I'm working on).

The basic idea is: we increment the values of an array a at indices contained in two sets is: Set[Int] and js: Set[Int]. Each of these increment statements defines a new Heap in Boogie. Finally, we assume that is and js are disjoint, and then sum the array over only the indices contained in js, using the heap-dependent function __snap_Int_Int_Int_val(..., js).

So every increment statement of some index in the set is is "irrelevant" to our final assertion. By using this "relaxed Skolem function" for the heap framing axiom, we should avoid having to produce multiple framing arguments that __snap_Int_Int_Int_val(..., js) is unchanged across the intermediate heaps generated by loc(a, i_).val := loc(a, i_).val + 1 statements. I ran several examples where I added more and more "relevant" and "irrelevant" statements, and my benchmarks seem to indicate that that the verification times scale roughly with the "relevant" statements only.

Here's a "schematic" version of the code (you can interpret hfold[add()](arrayRec(a).val | js) as a heap-dependent function over the set js) :

method test1(a:Array)
    requires access_array(a, 0, len(a))
    requires len(a) > 10
{
    var js: Set[Int]
    var is: Set[Int]

    assume js subset allInt(0, len(a))
    assume is subset allInt(0, len(a))

    var j1 : Int
    assume j1 in js
    var j2 : Int
    assume j2 in js
    var j3 : Int
    assume j3 in js

    var i1 : Int
    assume i1 in is
    var i2 : Int
    assume i2 in is
    var i3 : Int
    assume i3 in is
    var i4 : Int
    assume i4 in is
    var i5 : Int
    assume i5 in is
    var i6 : Int
    assume i6 in is

    loc(a,i1).val := loc(a,i1).val + 1
    loc(a,j1).val := loc(a,j1).val + 1
    loc(a,i2).val := loc(a,i2).val + 1

    loc(a,i3).val := loc(a,i3).val + 1
    loc(a,j2).val := loc(a,j2).val + 1
    loc(a,i4).val := loc(a,i4).val + 1

    loc(a,i5).val := loc(a,i5).val + 1
    loc(a,j3).val := loc(a,j3).val + 1
    loc(a,i6).val := loc(a,i6).val + 1

    assume (js intersection is) == Set[Int]()
    assert hfold[add()](arrayRec(a).val | js) ==
        old(hfold[add()](arrayRec(a).val | js)) + 3
}

arrayTestChainIrrel3.vpr.txt
arrayTestChainIrrel3_nosk.bpl.txt
arrayTestChainIrrel3_sk.bpl.txt

[marcoeilers]

Thanks!