Timeout in verification of lemmaCal invovling real numbers

[OlivierTOMATO]

Dafny version

4.6.0

Code to produce this issue

ghost function Pick<T>(s: set<T>): T
    requires |s| > 0
{
    var x :| x in s;
    x
}

ghost function cal(s: set<real>): real
requires |s| > 0
{
    var x := Pick(s);
    if |s| == 1 then x
    else cal(s-{x}) * |s| as real
}

lemma lemmaCal(s: set<real>)
requires |s| > 1
ensures cal(s) == cal(s-{Pick(s)}) * |s| as real // Comment: A time out
{
 //  assert cal(s) == cal(s-{Pick(s)}) * |s| as real;
}

ghost function cal2(s: set<real>): real
requires |s| > 0
{
    var x := Pick(s);
    if |s| == 1 then x
    else cal2(s-{x}) + |s| as real
}

lemma lemmaCal2(s: set<real>)
requires |s| > 1
ensures cal2(s) == cal2(s-{Pick(s)}) + |s| as real
{
}

Command to run and resulting output

dafny --verification-time-limit 5 code.dfy

What happened?

I am working on a simple example involving the following functions:

• Pick: Randomly selects a value from a set of real numbers.
• cal: Multiplies all the values in a set and returns a real number.
• cal2: Adds all the values in a set and returns a real number.

I have two lemmas:

• lemmaCal: A lemma that asserts certain properties related to the above functions when the size of the set is greater than 1.
• lemmaCal2: A similar lemma that also asserts properties when the set size is greater than 1.

Problem

1. lemmaCal2 successfully passes the verification, but lemmaCal runs into a timeout during verification.
2. If I add an assertion for the postcondition directly in lemmaCal and remove the postcondition, the verification passes.
3. If I change the real numbers to integers or replace the set with a sequence (seq), the verification also passes.

Ultimately, I am looking for a way to ensure that lemmaCal() can be verified without timing out. Any insights or suggestions would be greatly appreciated!

What type of operating system are you experiencing the problem on?

Mac

[OlivierTOMATO]

I tried the code in Dafny of versions 4.6.0, 4.7.0 and 4.8.0. None of them work as well.

[RustanLeino]

Thanks for the report. (I was unable to reproduce getting a proof when the assert is included, but can confirm the other behaviors.)

Workaround

Turn off automatic induction for lemmaCal:

lemma {:induction false} lemmaCal(s: set<real>)

Diagnosis

To prove the rather trivial postcondition of lemmaCal, the verifier needs to do a little bit of quantifier instantiation. In particular, the proof goal at the Boogie level is cal(2, s) == cal(2, sp) * ..., where I'm writing sp to denote s-{Pick(s)} and where I added a "fuel" number as the first parameter of cal. One application of the definition axiom for cal gives cal(2, s) == cal(1, sp) * .... After that, the synonym axiom (which says that the fuel value is irrelevant) needs to be applied to the two cal(..., sp) terms, which in essence gives cal(2, sp) == cal(0, sp) and cal(1, sp) == cal(0, sp), which completes the proof.

However, during this round of quantifier instantiations, it seems that the (automatic) induction hypothesis is invoked. Somehow, this is causing the verifier to time out. (The only way I see this happen is if the quantifier instantiations I mentioned in the previous paragraph never happen. That is, it seems that something in the handling of non-linear arithmetic causes the verifier never to return to the other quantifier instantiations.)

Four mitigations come to mind:

• We could turn off automatic induction by default. We may do this in the future, but using the issue reported here as the motivation for doing so seems rather weak.
• We could turn off non-linear arithmetic by default. We have discussed this numerous times, but never taken the bold step to do it. Then again, for this program, I'm guessing one would want to turn non-linear arithmetic on, if one is to make use of the product returned by cal.
• The verifier tries to find matching patterns for all quantifiers sent to Boogie/Z3. However, one glaring omission is in the automatically generated induction hypothesis. (I think @cpitclaudel is looking into fixing this.) It is possible that such a matching pattern would be enough to prevent a bad or unnecessary invocation of the induction hypothesis here.
• The fuel parameter is used as an argument to the function cal itself. This necessitates the use of a synonym axiom, among other things. I'd like us to move that fuel parameter into the cal#canCall function instead. This may reduce the quantifier instantiations enough that the induction hypothesis (and non-linear arithmetic) won't be a problem here.

Remark

cal(s) actually returns the factorial of the cardinality of s multiplied by an arbitrary real number in s. To compute the product of the numbers in s, change |s| as real to just s. An analogous remark applies to cal2.