Strange Bug with Macro Substitution?

[DavePearce]

There is a very strange problem with the following (from the resize example):

define unchanged(int[] xs, int n, int[] ys) is:
    forall(int j):
        if:
            (0 <= j) && (j < |xs|)
        then:
            (j >= n) || (xs[j] == ys[j])

define resize_ensures_2(int[] xs, nat n, int v, int[] ys) is:
    forall(int i).(((|xs| <= i) && (i < n)) ==> (ys[i] == v))

define resize_loopinvariant_31(int[] xs, nat n, int[] rs, nat i) is:
    |rs| == n

define resize_loopinvariant_35(int[] xs, nat n, int v, int[] rs, nat i) is:
    unchanged(xs, i, rs)

define resize_loopinvariant_45(int[] xs, nat n, int v, int[] rs) is:
    forall(int j):
        if:
            ((|xs| <= j) && (j < n))
        then:
            rs[j] == v

assert "postcondition not satisfied":
    forall(int v, int[] xs, nat n, int[] rs, int i):
        if:
            resize_loopinvariant_31(xs, n, rs, i)
            resize_loopinvariant_35(xs, n, v, rs, i)
            resize_loopinvariant_45(xs, n, v, rs)
        then:
            resize_ensures_2(xs, n, v, rs)

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

Basically, if you do just about anything to this (e.g. inline one of the macros) then it will verify. And. ss far as I'm aware, it is indeed correct.

[DavePearce]

Right, so when it fails it does so because of the classic "counting" problem. This may be arising from the fact that it infers this (recursive) formula:

rs[i] == rs[5 + rs[i]] 

This term is being generated from instantiating this quantifier:

forall(int m).((rs[l] == rs[m]) || (m >= |rs|) || (|xs| >= (1 + m)))

against:

|rs| >= (1 + rs[l]) 

to give (where m == 1 + rs[l]):

(rs[l] == rs[1 + rs[l]]) || (|xs| >= (2 + rs[l])) || ((1 + rs[l]) >= |rs|)

It seems a little odd that this example is triggering quantifier instantiation.

[DavePearce]

UPDATE: have fixed quantifier instantiation to properly look for triggers, which was something it wasn't previously doing.

This now resolves the counting issue but most importantly does not resolve the actual issue itself. In particular, original assertion not verifying but with any slight modification it is.

[DavePearce]

Right, the problem is (as always) to do with representation:

┌──────────────────────────────────────────────────────────┐
│ 460. rs[l] == xs[l]                           (Or-E 462) │
│┌─────────────────────────────────────────────────────────┤
││ 464. v >= (1 + rs[l])                        (Or-E 467) │
││ 472. v >= (1 + xs[l])                    (Eq-S 464,460) │
││ 476. (v == rs[l]) || (l >= |rs|) ||  (Forall-I 433,460) │
││┌────────────────────────────────────────────────────────┤
│││ 473. v == rs[l]                             (Or-E 476) │
│││ 479. forall(int m).((rs[l] == rs[m]) || (Eq-S 433,473) │
│││ 480. rs[l] >= (1 + xs[l])               (Eq-S 472,473) │
│││ 482. true                           (Forall-I 479,473) │

480. rs[l] >= (1 + xs[l]) is not in normal form since already have 460. rs[l] == xs[l]. Proper representation would be e.g. 480. xs[l] >= (1 + xs[l]) which automatically reduces to false.

UPDATE: The problem seems to be really that 473. v == rs[l] is not in normal form which arises from the quantifier instantiation 476. The problem is that the term generated from the instantiation is not in normal form.