Mentioning recursive function body in its postcondition leads to a matching loop

[viper-admin]

Created by @vakaras on 2018-07-25 09:14 Last updated on 2018-08-15 10:00

The functions fib3 and fib4 below cause matching loops as illustrated with asserts in the methods test3 and test4 (to verify these methods, the verifier would need to unroll the functions 4 times on its own, which means that it is very likely that the verifier would try to unroll the functions arbitrary number of times, which means that we have a matching loop):

#!silver

function fib3(n: Int): Int
    ensures result == (n < 2 ? 1 : fib3(n-1) + fib3(n-2))
{ (n < 2 ? 1 : fib3(n-1) + fib3(n-2)) }

method test3() {
    // assert fib3(0) == 1
    // assert fib3(1) == 1
    // assert fib3(2) == 2
    // assert fib3(3) == 3
    // Verifies: we have a matching loop.
    assert fib3(4) == 5
}

function fib4(n: Int): Int
    ensures fib4(n) == (n < 2 ? 1 : fib4(n-1) + fib4(n-2))
{ (n < 2 ? 1 : fib4(n-1) + fib4(n-2)) }

method test4() {
    // assert fib4(0) == 1
    // assert fib4(1) == 1
    // assert fib4(2) == 2
    // assert fib4(3) == 3
    // Verifies: we have a matching loop.
    assert fib4(4) == 5
}

A work around would be to remove the postcondition because it is implied by the function body.

[viper-admin]

@vakaras commented on 2018-07-25 09:15

Carbon issue.

[viper-admin]

@mschwerhoff commented on 2018-08-07 14:01

@vakaras @alexanderjsummers Did you look at Z3's axiom instantiation statistics to confirm your matching loop theory ? It could also be that Z3's macro finder optimisation — an optimisation that affects axioms that (recursively) define mathematical functions, and that can probably be turned off for the purpose of debugging/exploring this issue — kicks in here.

[viper-admin]

@vakaras commented on 2018-08-15 10:00

@mschwerhoff

I have added the following method:

#!silver
method test3a(n: Int) {
    assert fib3(n) > 0
}

Executed Silicon with Z3 logging enabled:

#!bash

> silicon test.vpr --z3Args '"TRACE=true"'
Silicon 1.1-SNAPSHOT (<https://github.com/viperproject/silicon/commit/caf6da66fa6286347edaf0bc154103745cb91bc8>)
(c) Copyright ETH Zurich 2012 - 2017
Silicon found 1 error in 39,24s:
  [0] Assert might fail. Assertion fib3(n) > 0 might not hold. (test.vpr@28.5)

And imported the resulting log into the axiom profiler. In the axiom profiler I can see a very long chain of fib3%limited instantiations.

Does this answer your question?