Noop && operation changes verification time

[keyboardDrummer]

The program:

method Foo() {
  assert var x := 3; 
    x == 3;
}

and

method Foo() {
  assert && var x := 3; 
    x == 3;
}

have the same meaning, but the former takes 3149 RU to verify and the latter 3704, using Dafny 4.9.1

[MikaelMayer]

This is because && as a prefix acts as if it was true && . You can verify this by expliciting the "true" before the "&&" and verify it has the same resource count.

Let me analyze different configurations

Method body	Resource count
var x := 3; assert x == 3;	3053
assert var x := 3; x == 3;	3145
var x := assert true; 3; assert x == 3;	3412
assert true && var x := 3; x == 3;	3670
assert true && true && var x := 3; x == 3;	4201
assert true && true && true && var x := 3; x == 3;	4541
assert true && true && true && true && var x := 3; x == 3;	4889
assert && var x := 3; x == 3;	3670
assert var x := 3; assert true; x == 3;	3667
assert var x := assert true; 3; x == 3;	3517
assert var x := 3; x == assert true; 3;	3665
assert var x := 3; (assert true; x) == 3;	3665

The fact that it takes more resource count in the first one is expected. First, when trying to prove that x == 3, it will look at all available proved statements, and because we don't prune things, it seems that processing "true" will take an extra 300 RC for this proof goal. It's also likely because there is some special encoding for each assertion to prove in case it fails to be able to point the user to the failed assertion.

I've also seen instances where asserting true did have a huge impact on either increasing or decreasing resource count for obviously no reason other than a change of heuristic in the solver.
But in that case, it probably means that the solver got lucky in one case, and unlucky in the other one. For example, if it makes heuristic decisions based on index modulo something (I don't know), then adding one more or remove one less statement could dramatically change the resource count, but it's because the proof itself is likely brittle and lucky on the best case.

I'm still going to investigate all of that.

[keyboardDrummer]

Hey, thanks for investigating. I think it could be interesting to check what happens to the true && when it gets transformed to SMT. Based on the impact, it looks like it doesn't end up producing just true && at the SMT level, but something bigger.

Solving that might be more fruitful than adding a processing step that simplifies occurrences of true &&.

[MikaelMayer]

I edited my message shortly after publishing it, so you might not have seen my other hypothese but I think it matches your intuition.

"It's also likely because there is some special encoding for each assertion to prove in case it fails to be able to point the user to the failed assertion."