Counterexample Generation Timeouts

[DavePearce]

For some reasons, counterexample generation seems to timeout quite easily. Not sure what's going on there. This is the smallest example I've found so far:

type nat is (int n) where n >= 0

function zeroOut(int[] ns) -> (int[] rs):
    //
    nat i = 0
    int len = |ns|
    //
    while i < |ns|
    where all { k in 0..i | ns[k] == 0 }:
        ns[i] = 1
        i = i + 1
    //
    return ns

The offending verification condition is:

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

define zeroOut_loopinvariant_229(int[] ns, nat i) is:
    forall(int k).(((0 <= k) && (k < i)) ==> (ns[k] == 0))

assert "loop invariant not restored":
    forall(int len, int[] ns, int[] ns$2, int[] ns$1, nat i, nat i$1, nat i$2):
        if:
            i == 0
            len == |ns|
            zeroOut_loopinvariant_229(ns$1, i$1)
            i$1 < |ns$1|
            ns$2 == ns$1[i$1:=1]
            i$2 == (i$1 + 1)
        then:
            zeroOut_loopinvariant_229(ns$2, i$2)

This can then be reduced to this whilst preserving the timeout:

assert:
    forall(int len, int[] ns, int[] ns$2, int[] ns$1, nat i, nat i$1, nat i$2):
        if:
            i$1 < |ns$1|
        then:
            forall(int k):
                if:
                    (0 <= k) && (k < i$2)
                then:
                    ns[k] == 0

One of the obvious things to note here is the number of quantifier parameters. That is despite the fact that most of them are not even used!

[DavePearce]

Further reducing the verification to this does help, though it still takes a while to get through them all:

assert:
    forall(int[] ns, int[] ns$1, nat i$1, nat i$2):
        if:
            i$1 < |ns$1|
        then:
            forall(int k):
                if:
                    (0 <= k)
                    (k < i$2)
                then:
                    ns[k] == 0

This definitely suggests that a better approach to handling the state space is required.

[DavePearce]

IDEA 1: One idea here is to instantiate variables for iteration lazily. That is, at the point of use of a variable we then (somehow) instantiate an iteration space for that variable. This would be very helpful for functions as well (#142) since they don't have explicit declaration points where we can iterate.

IDEA 2: The other obvious idea is to perform integer range analysis on declared types to determine upper and lower bounds. This would be particularly good for e.g. nat types which are common.

Note that idea 1 may have some advantages with situations like this:

forall(int i, int j):
   if:
      i == j + 1
   then:
     ...

Here, we don't want to iterate all of i's space as it is fully determined by j's.