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.