Time-traveling triggers

[fpoli]

Thanks to @bkragl and @gauravpartha, I noticed that since #3233 with Z3 versions >4.8.5 Dafny will no longer set the smt.case_split=3 option. I recently found that without that option it is possible for quantifier triggers to "travel back in time". For example, on the following program the only way to prove (2) is to instantiate the quantifier (1) matching its trigger on a statement that comes later (3). Without the smt.case_split=3 option Dafny will accept the following program, but with smt.case_split=3 it will not. To reproduce this, it's enough to run Z3 on the /proverLog manually adding/removing the (set-option :smt.case_split 3) option from the log. Having the verification of a statement depend on code that comes later can be surprising. I'm opening this discussion just to make you aware of this behavior.

To be precise, even with smt.case_split=3 there is no guarantee that triggers will not travel back in time with Boogie, but at least it becomes much more difficult to build examples like the following.

(CC @Aurel300)

class Functions {
  function Foo(x: int): int
  function Bar(x: int): int
}

method Test(f: Functions, x: int) {
  assume forall x {:trigger f.Bar(x) } :: f.Foo(x) == 42 && f.Bar(x) > 0; // (1)
  assert f.Foo(x) == 42; // (2)
  assert f.Bar(x) > 0;   // (3)
}

[MikaelMayer]

@atomb You might be interested

[atomb]

Yeah, that's definitely counter-intuitive behavior! I'm somewhat reconsidering the overall decision of removing those flags for newer Z3 versions. On the arithmetic solver side, it initially seemed as though relying on the default solver in newer versions tended to perform better, but I've now come across a bunch of regressions, as well. And I think the regressions may outweigh the benefits. I'm going to investigate further.

[atomb]

I now have a draft PR to go back to setting those options unconditionally, #3385. In particular, the libraries code had a number of verification regressions with newer Z3 versions after that change.

[RustanLeino]

Thanks for reporting this and for the small repro. I agree that such behavior is quite counter-intuitive. It would be great if Boogie could guarantee that such behavior would never take place. (Making such a guarantee would probably necessitate a collaboration between a Z3 author and a Boogie author, or someone who knows the details of both.)

[shazqadeer]

@RustanLeino shared this discussion with me. I am afraid I am the odd voice out here. I don't find the behavior counter-intuitive but I realize that I know a lot more about the inner details of how Dafny programs get verified than the typical Dafny user. Perhaps it would help if I see an explanation of what a Dafny programmer expects from triggers (as opposed to what an SMT2 user expects from triggers).