VeriFast freezes due to matching loop

[elKei24]

Hi Bart,

when trying to verify something like in the following example, VeriFast gets stuck and will not respond until killed and opened again:

fixpoint bool bar1(int f);
fixpoint int bar2(int f);

predicate pred(int f; ) = bar1(f) == true;     
    
lemma_auto void lemma_1(int f); // not a auto-lemma: works
  requires bar1(f) == true;
  ensures bar1(bar2(f)) == true; // without bar2: works
    
lemma void lemma_2()
  requires pred(?f);
  ensures pred(f);
{
  open pred(f); // without this line: works
}

Best regards,
Elias

[btj]

This is due to a so-called matching loop in the SMT solver, caused by the autolemma. The declaration of the autolemma causes VeriFast to emit the SMT solver axiom forall f. bar1(f) == true ==> bar1(bar2(f)) == true, with trigger bar1(f). The SMT solver deals with this as follows: whenever a new term that matches bar1(X) is constructed, the axiom is instantiated and bar1(X) == true ==> bar1(bar2(X)) == true is assumed. Notice, however, that this again causes a new term bar1(bar(X)) to be constructed, causing another quantifier instantiation, and so on indefinitely. The opening of pred(f) constructs the initial term bar1(f) and kicks off the loop.

The solution, therefore, is to change the autolemma so that it no longer causes matching loops.

You can specify a trigger explicitly using lemma_auto(trigger) syntax. See bin/list.gh for examples.

It would also be nice if VeriFast detected matching loops and generated an informative error message instead of freezing, so I will leave this issue open to record that.

[btj]

When the VeriFast IDE freezes, it is useful to run the command-line tool with the -verbose X option, where X is either 1, 2, or a larger number, to control the amount of diagnostic output. E.g.:

verifast -verbose 10 myfile.c

Another useful command-line option is -stats, which, among other things, reports how often each axiom (= pure autolemma) was instantiated.

[elKei24]

Ah, thanks for the hint, I have noticed those triggers before, but did not know what they are used for.
I also have tried the -verbose switch before, but only with X ≤ 4 as described in the usage message of the command. With X = 10 it is indeed a lot easier to find the reason for the freeze 👍