Feature request: explicit language features for verification debugging

[robin-aws]

Follow-up from #1354.

It is a fairly well-established idiom amongst Dafny programmers to temporarily insert assume false; or assert false; in various places when trying to determine why their program doesn't verify. The effect is to "turn off verification" for a region of code, in order to gain more precise feedback on what specific proof obligations are not met, or to find regions with a high verification cost (by observing that the verifier takes a very long time to flag the violation from an assert false;). Doing so creates an invalid Dafny program, so as long as the verifier raises at least one violation it is still sound, but the effectiveness of this technique depends on the somewhat undefined behavior of how the verifier behaves in the presence of existing logical inconsistencies.

1354 improves the effectiveness of this mechanism by making the effects of something like assume false; more useful for verification debugging, but it's still a fragile situation. I propose that a better solution would be a more explicit way to tell the verifier "don't verify this section", which would therefore have concrete and well-defined semantics. For example (without actually suggesting this syntax is ideal):

method JustVerifyThisAlreadyDammit(n: nat) { // error, "body contains unverified blocks"
  var i := 0;
  while i < n {
    unverified { // Temporarily inserted
      SomeCodeThatWontVerifyYet(i);
    }
    i := i + 1;
  }
  assert n == 0; // error, because the unverified block never hides the loop from Boogie
}

The current technique reminds me of what I used to do in languages that had limited debugging support: I'd add this snippet in random places just so I had a statement to attach a breakpoint to.

int breakpoint = 42;
breakpoint++;

There could be other solutions to this problem, so don't take my suggestion too literally. The key point is I think it's time for SOMETHING better. :)

[tjhance]

The effect is to "turn off verification" for a region of code, in order to gain more precise feedback on what specific proof obligations are not met, or to find regions with a high verification cost (by observing that the verifier takes a very long time to flag the violation from an assert false;)

I do this a lot too, but it seems to me there could be much more direct language support for this common developer scenario, e.g., if dafny had a way to print out a detailed breakdown of how much time it is spending at the granularity of assertions & preconditions.

[robin-aws]

Absolutely, and we're investigating improvements in that area as well. I don't even intend this issue to take a strong stance on which solution is the best bang for the buck yet.

[kjx]

(assuming this is still live)

I quite like (unverified) tag within code, although I guess quite close to {:verify false} on the declaration.

I do wonder if there are other linguistic things that can help verification by making more things explicit, or by restricting the scope of code or changes (and thus proofs?)

one recently example is the "by" clauses to everything - especially if you add the "by" back into forall v <- r ensures e by c

other ideas: guarantee (e) within {code} // rely-guarantee guarantee reads (locations) within {code} // code only reads those locations, not any others footprint(e) // all locations required to evaluate e