Feature request: identifying individual assertions in Dafny code

[robin-aws]

This feature request (which may need refining and/or substantial splitting up) depends on the following proposed definition.

Assertion: An individual boolean expression, derived from an element of Dafny code, which must be true for the program to be valid.

An explicit assert statement creates an assertion, but isn’t the only way:

• Applying a function/invoking a method creates an assertion for each requires clause
• Each return statement creates an assertion for each ensures clause on the current method
• Each a[i] expression creates a 0 <= i < |a| assertion
• Extending a trait and implementing a method creates an assertion that the method’s ensures clauses are at least as strong as those in the trait
• A subset type declaration with a witness creates an assertion that the witness satisfies the type’s predicate
• Writing to an object field creates an assertion that the object is an element of the current method’s modifies clause
• etc.

These are the elements that ideally the IDE would provide UX for identifying and verifying individually in the future. A single line of Dafny code, or even a single token position, can create multiple assertions. This is similar to the way a single line of code can contain multiple potential breakpoints when debugging.

This is something of a blocker for providing good "profiling" feedback based on techniques like the proposed /vcsSplitOnEveryAssert Boogie feature (boogie-org/boogie#465), since a Dafny source location isn't enough to uniquely and clearly identify the source of a Boogie assertion.