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.