Use proof dependencies for more thorough brittleness reduction warnings

[atomb]

Summary

Issues #5253 and issue #5259 describe features to help guide Dafny programmers toward reducing brittleness in the verification of their code. This issue describes additional features that extend that capability by building on proof dependencies.

Background and Motivation

Brittleness, where verification can alternate between success and failure after seemingly trivial changes, is a key challenge in Dafny. In general, one of the more effective techniques for reducing brittleness is to limit the information available to the solver. Proof dependency analysis can help us understand what facts are necessary for what proof goals, and therefore suggest ways to refactor the code to reduce brittleness.

Proposed Feature

Implement new warnings that identify instance of the following patterns:

• Lemma calls or assert statements that are needed only to help discharge one assertion, and therefore could be moved into a by block of an assert statement (or a method call, when #5192 is complete).
• Preconditions on functions that are necessary only to prove postconditions and not internal goals, and therefore could be moved (alongside the associated postcondition(s)) to a separate lemma.

Alternatives

Like #5253 and #5253, these suggestions could be static, in a document. But, like those issue, direct, active feedback, would help accelerate the process. In addition, it automates a dependency analysis process that is difficult to perform manually.

[keyboardDrummer]

Nice feature

Nitpick: in the user facing messages, I think we should talk about performance instead of brittleness. Addressing these warnings will improve verification performance, even if the user is not having any issues with brittleness.

[keyboardDrummer]

Do we know whether by clauses works as advertised in the sense that anything in a by clause does not affect the SMT generated by the rest of the callable? If not, shouldn't we fix that as well?

[keyboardDrummer]

Also, suppose you have a sequence of assertions,

assert A;
assert B;
assert C;

where each is used to prove the next one, then it seems the feature described in this issue would guide the user to write this as a nesting of by blocks

assert C by {
  assert B by {
    assert A;
  }
}

Syntactically that looks much worse. Are we missing a language construct here?

[atomb]

Do we know whether by clauses works as advertised in the sense that anything in a by clause does not affect the SMT generated by the rest of the callable? If not, shouldn't we fix that as well?

Unfortunately, using by clauses does not entirely insulate the encapsulated proof from that of the enclosing method. I agree that it should, but I also think it won't be any easy thing to change. Right now, the encoding works in such a way that aims to allow the solver to quickly conclude that the hidden part is irrelevant, because it can't affect the main goal, and ignore it. However, with particularly brittle goals, logical independence doesn't guarantee predictable performance, because these "irrelevant" parts of the SMT term are still in memory, and still affect things like the shape of internal solver data structure, ordering of variable indices, and such things. (They also may affect things like the ability of the solver to know that certain theories aren't required. For instance, if you have non-linear arithmetic in a by block, but not in the outer method's verification conditions, the solver might adjust its heuristics to favor being able to reason about non-linear arithmetic for the entire goal.)

[atomb]

assert C by {
  assert B by {
    assert A;
  }
}

Syntactically that looks much worse. Are we missing a language construct here?

Yeah, I agree. I suspect there may be a language construct that would make it nicer. I'll mull that over, but feel free to suggest something if it comes to mind!

[keyboardDrummer]

Do we know whether by clauses works as advertised in the sense that anything in a by clause does not affect the SMT generated by the rest of the callable? If not, shouldn't we fix that as well?

Unfortunately, using by clauses does not entirely insulate the encapsulated proof from that of the enclosing method. I agree that it should, but I also think it won't be any easy thing to change.

Currently when use you --isolate-assertions, at the Boogie level when it runs a particular assertions, it will turn all other assertions into assumes. I'm thinking we can add an optimization that removes assume clauses that occur at the end of a conditional block, such as the end of an if branch, combined with an optimization that removes empty conditional blocks.

That way, if you have

assert X by { Y; }
assert Z;

and we translate it into this Boogie:

if * {
  assert Y;
  assert X;
}
assume X;
assert Z;

Then with --isolate-assertions it becomes three VCs, that at the Boogie level look like:

if * {
  assert Y;
}

if * {
  assume Y;
  assert X;
}

assume X;
assert Z;

Note that Y does not occur in the last block, so the Dafny by clause no longer affects the proving of anything after assert X by