Heap-dependent function with QPs generates triggerless axiom

[jwkai]

While considering performance issues for heap-dependent functions, we found that the following function definition in Viper:

field f: Bool

function heapFun(refs: Set[Ref]): Map[Ref, Bool]
    requires (forall ref: Ref ::
        { ref in refs }
        ( ref in refs ) ==> acc(ref.f))

will generate this axiom in the Boogie translation using Carbon:

// ==================================================
// Function used for framing of quantified permission (forall ref: Ref :: { (ref in refs) } (ref in refs) ==> acc(ref.f, write)) in function heapFun
// ==================================================

function  heapFun#condqp1(Heap: HeapType, refs_1_1: (Set Ref)): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, refs: (Set Ref) ::
  { heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs), succHeapTrans(Heap2Heap, Heap1Heap) }
  (forall ref: Ref ::
    
    (refs[ref] && NoPerm < FullPerm <==> refs[ref] && NoPerm < FullPerm) && (refs[ref] && NoPerm < FullPerm ==> Heap2Heap[ref, f_7] == Heap1Heap[ref, f_7])
  ) ==> heapFun#condqp1(Heap2Heap, refs) == heapFun#condqp1(Heap1Heap, refs)
);

The inner quantifier (forall ref: Ref :: ...) is missing a trigger, presumably because in the context of the outer implication, it will become an existential that the solver uses to generate a Skolemized term with the bound variable ref replaced.

@alexanderjsummers and I discussed two changes:

1. Add a trigger with a dummy function application to the inner quantifier (forall ref: Ref :: ...) to at indicate (at least to anyone reading this Boogie code) that this quantifier shouldn't be triggered.
2. Consider replacing this inner quantifier with a Boolean-valued "Skolem function" taking heapFun#condqp1(Heap2Heap, refs) and heapFun#condqp1(Heap1Heap, refs) as arguments. This could potentially reduce the number of Map#Equal obligations arising from the quantifier body of the Skolemized (forall ref: Ref :: ...) terms in the situation where heapFun must be framed across many heaps (so that this axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, refs: (Set Ref) :: ...) gets triggered on many pairs of HeapType objects, and we lose progress on input values for which heapFun has previously been shown to be equal).

[jwkai]

After some testing, it seems that an equivalent Skolemized formula can perform much better in place of the quantified LHS here. Continuing the above example, this would look like:

// ==================================================
// Function used for framing of quantified permission (forall ref: Ref :: { (ref in refs) } (ref in refs) ==> acc(ref.f, write)) in function heapFun
// ==================================================

// Skolem function representing the existential (negated universal) quantified variable
function sk#condqp1(i1: int, i2: int): Ref 

function heapFun#condqp1(Heap: HeapType, refs_1_1: (Set Ref)): int;
axiom (forall Heap2Heap: HeapType, Heap1Heap: HeapType, refs: (Set Ref) ::
  { heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs), succHeapTrans(Heap2Heap, Heap1Heap) }

  (
    (refs[sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs))] && NoPerm < FullPerm 
     <==> 
     refs[sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs))] && NoPerm < FullPerm) 
  
    && 

    (refs[sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs))] && NoPerm < FullPerm 
     ==> 
     Heap2Heap[sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs)), f_7] ==
     Heap1Heap[sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs)), f_7]) 
  )
  ==> heapFun#condqp1(Heap2Heap, refs) == heapFun#condqp1(Heap1Heap, refs)
);

where the inner (LHS) quantifier is dropped, and sk#condqp1(heapFun#condqp1(Heap2Heap, refs), heapFun#condqp1(Heap1Heap, refs)) is substituted for the universally quantified variable ref: Ref in its body.

Preliminary tests indicate that only one member of each equivalence class of heap-based function applications that produce identical outputs will appear as a trigger of this axiom for subsequent heaps. So, if heapFun#condqp1(_, refs) does not differ across heaps H0 and H1, but does differ on H2, then it would not be necessary to prove both:

• heapFun#condqp1(H0, refs) != heapFun#condqp1(H2, refs)
• heapFun#condqp1(H1, refs) != heapFun#condqp1(H2, refs)

(whereas, in the original axiom, this would potentially be proved twice, for "Skolem constant" sk(H0, H2) and sk(H1, H2) resulting from the negated universal in each instance of the outer quantifier)

I am working on a pull request to generate the Skolemized form of the axiom.

[jackstodart]

It looks like this change has introduced a slowdown in my case.

I'm verifying the two attached files (changed to .txt so I could attach) which are almost the same, except for one loop invariant inv_optimal. In BF6_Variation.txt this is verified automatically in the usual way, but in BF6_VariationManual.txt it is handled manually and not as a Viper quantifier. The invariant in question is not a QP itself but all of the loops use QPs.

At commit 098c706, just before this change was merged, both files verify in similar time, but at commit d14a703 which merged this changed, BF6_Variation.vpr is 3-4x slower, while BF6_VariationManual.vpr is only about 10-20% slower. Rough times:

Commit	BF6_Variation.vpr	BF6_VariationManual.vpr
098c706	~17s	~13s
d14a703	~58s	~17s

The slower times persist in the most recent master commit of carbon. I'm using an Apple Silicon Mac, but we could reproduce the same timing ratios on a Windows machine.