Triggerless Quantifier Instantiation

[DavePearce]

The following fails to verify for reasons unknown:

type nat is (int x)
where:
    x >= 0

define f_requires_0(int[] xs) is:
    |xs| > 0

assert "postcondition not satisfied":
    forall(nat[] xs):
        if:
            f_requires_0(xs)
        then:
            exists(int i):
                (0 <= i) && (i < |xs|)
                (xs[i] >= 0)

However, if we manually inline f_requires_0(xs) then it does indeed verify.

UPDATE: the problem here is that we end up with two forall quantifiers and no trigger. Something like this: forall(nat[] xs).(|xs| > 0 && forall(int i).(i < 0 || i >= |xs| || xs[i] < 0))

UPDATE: What we need is for |xs| > 0 to somehow trigger quantifier instantiation. For example, if it generated xs[0]=y for any y then we'd be close.

[DavePearce]

Here's a simpler example encountered by Lindsay:

function ordMin(int[] a) -> (int m)
requires |a| > 0
ensures some { k in 0..|a| | m == a[k] }:
    //
     return a[0]

This generates the following WyAL assertion:

assert "postcondition not satisfied":
    forall(int[] a):
        if:
            |a| > 0
        then:
            exists(int k).((0 <= k) && (k < |a|) && (a[0] == a[k])) 

The system does a proof-by-contradiction which begins by inverting to give this:

    some(int[] a):
         |a| > 0
         forall(int k).((0 > k) || (k > |a|) || (a[0] != a[k]))

The problem is that we need a "trigger" to instantiate the quantifier. That is a possible substitution for k. The tool doesn't generate these from scratch (like more SMT solvers, including Z3). Rather it generates them from the "triggers". In this case, a trigger is a ground clause containing an expression of the form a[e] for arbitrary expression e. The system will then substitute k:=e to instantiate the quantifier.

The problem with this assertion is that doesn't have a trigger. An interesting workaround is to artificially introduce one. For example, by rewriting the original program like this:

function ordMin(int[] a) -> (int m)
requires |a| > 0 && a[0] >= 0
ensures some { k in 0..|a| | m == a[k] }:
    //
    return a[0]

See that I've added a[0] >= 0 to the precondition. This then generates the following assertion (after inversion):

     some(int[] a):
         |a| > 0 && a[0] >= 0
         forall(int k).((0 > k) || (k > |a|) || (a[0] != a[k]))

Here we have the necessary trigger and verification does succeed. In fact, using this precondition also succeeds:

requires |a| > 0 && (a[0] >= 0 || a[0] <= 0)

Though using a[0] == a[0] does not, presumably because it simplifies away the trigger.

[DavePearce]

Found a better workaround, introduce a temporary variable:

function ordMin(int[] a) -> (int m)
requires |a| > 0
ensures some { k in 0..|a| | m == a[k] }:
    //
    int r = a[0]
    return r