Cache verification in the LSP server

[keyboardDrummer]

Boogie has an advanced caching mechanism that can prevent verification tasks that haven't changed from being verified again, but can also makes verification tasks easier to compute if only part of them has been previously changed.

These are known bugs in Boogie's caching mechanism:

• Inconsistent results with and without caching, on a single snapshot #1878

There are also two architectural concerns:

• Boogie's caching mechanism depends on checksums computed by Dafny, so there can be a difference between how Boogie computes the checksum and how it translates to Boogie. Ideally Boogie would compute these checksums so there's no chance of an error by the client. The reason it works like it currently does may be that the Dafny to Boogie translation used to unstable in the sense that it depended on source code location and on global counters, a problem which has now been resolved.
• The dependency computation in Boogie may compute too many dependencies due to function references in axioms being bidirectional, leading to caching that is not granular.

Change

• Test verification caching at the Dafny LSP server level. We should have tests for
  • Caching of an unchanged method, when an unrelated method has been added above it.
  • Caching behaviour of an unchanged method, where one of its dependencies has changed.
  • Caching of an unchanged method, where a dependent of that method's dependency has changed.
  • Caching of assertions that occur before other assertions in a statement block.
  • Caching of verification of branches such as if-then-else or match statement.
  • Caching over different types of verifiables, such as constants, datatype constructors with default values, subset types and iterators.
  • ... Try to come up with more :-)
• Record limitations in the granularity of Boogie's caching
• Resolve bugs in Dafny's and Boogie's verification caching

Not in scope

• Parse or resolution caching
• Computation of verification priority

Prerequisites

None

Enables

• When an open file is changed, also update diagnostics and other IDE state for dependent files #2328
• On change, only cancel compilation tasks whose inputs have changed #2332

Implementation hints

Boogie caching mechanism is described in these two papers:

• Coarse-grained caching is described in http://leino.science/papers/krml236.pdf
• Fine-grained caching: http://leino.science/papers/krml245.pdf

[cpitclaudel]

As far as we're aware there are no issues with this caching mechanism, but we don't have LSP server tests that exercise the caching mechanism.

Unfortunately, we actually have identified a number of cases where the caching mechanism disagrees with the command line; see #1878