Suggest changes to avoid brittleness due to use of difficult constructs

[atomb]

Summary

Help reduce brittleness by warning about the use of certain difficult constructs and providing guidance on how to restructure the code to avoid them.

Background and Motivation

Brittleness, where verification can alternate between success and failure after seemingly trivial changes, is a key challenge in Dafny. Combining certain particularly complex constructs can exacerbate the problem, and programs can generally be refactored to avoid those difficult combinations. We would like to help make that job easier.

Proposed Feature

Implement warnings, enabled with --warn-brittleness, for code that follows any of the following patterns:

• Quantifiers in contracts where the quantified variable could become an additional in or out parameter.
• Conversions between integers and bit vectors where arithmetic or logical operations appear on both sides of the conversion.
• Use of quantifiers and "complex" theories in the same context. In this case, complex theories include:
  • Non-linear integer or real arithmetic operations
  • Bit vector operations

For each of these cases, provide guidance on how to refactor the code to avoid the difficult construct and, therefore, the warning, as well.

Alternatives

This guidance could, in principle, be purely static, written in a document. However, automated warnings about existing code, potentially with pointers to such a document, will make it easier to detect and improve brittle code.

[keyboardDrummer]

Quantifiers in contracts where the quantified variable could become an additional in or out parameter.

Probably better as a suggestion, since the user might not want to refactor this.

Maybe this holds for the other two as well. Could you provide examples for those?

[atomb]

Quantifiers in contracts where the quantified variable could become an additional in or out parameter.

Probably better as a suggestion, since the user might not want to refactor this.

Maybe this holds for the other two as well. Could you provide examples for those?

If that's the case, then none of the patterns we've discussed so far would be warnings. All would be suggestions. I'm open to that possibility, but just wanted to double check that's what you had in mind.

And, yes, I can post some examples.

[atomb]

An example of both quantifiers that could become additional parameters and of the use of non-linear arithmetic along with quantifiers:

https://github.com/dafny-lang/dafny/blob/ca4bb03e0d9f519292acd643a83b8ad6d35b1ff4/Source/DafnyStandardLibraries/src/Std/Arithmetic/Internal/MulInternals.dfy#L70-L90

Note that, in this case, the combination of quantifiers and NL arithmetic isn't as much of a problem because the module has the {:disableNonlinearArithmetic} attribute, so those operations are treated as uninterpreted functions. However, the same code in a different module would be a nice example.

Some examples of code that Dafny can't easily prove because operations occur on both sides of an integer-to-bitvector conversion is here:

https://github.com/dafny-lang/dafny/issues/2174#issuecomment-1155812561

The exact code in that example verifies because all of the idx variables are bit vectors. If you make them integers, it stops verifying, at least last time I checked. But whether it verifies or not is inconsistent, and depends on the exact expression and the size of the bit vectors involved.

[keyboardDrummer]

If that's the case, then none of the patterns we've discussed so far would be warnings. All would be suggestions. I'm open to that possibility, but just wanted to double check that's what you had in mind.

If something is a warning then it must be addressable. If there are patterns where we think it is valid for a user to write lemma PForAll() ensures forall x :: P(x) { ... }, then we can't warn on it.

Alternatively, we could try to introduce a syntax that makes such lemma's unnecessary, and then we can warn on it. Here's an idea:

method Foo() {
  PForX(?) // ? means wrap this in a forall statement for that parameter
}
lemma PForX(x: X) ensures P(x) { ... }

We could then have a type based suggestion that suggests using a variable local to Foo as an argument to PForX

[keyboardDrummer]

An example of both quantifiers that could become additional parameters and of the use of non-linear arithmetic along with quantifiers:

Could you not just include the code that would give a warning/suggestion, but also what you think the code should be rewritten to?

[atomb]

After some recent discussion here's how I'm thinking we might more precisely define each pattern listed in the issue description:

• If any lemma has a postcondition with a top-level forall, or with a forall as a conjunct, and the body is not immediately a forall statement wrapped around another lemma call, suggest splitting it into a parameterized lemma and a quantified wrapper, and using the parameterized lemma whenever possible.
• Skip the one about integer/bit vector conversion for now, since it'll be a bit complex to detect.
• If any quantified expression, anywhere, contains non-linear arithmetic or bit vector operations, suggest refactoring the code so that the quantifier is no longer necessary, or move the body of the quantified expression to an opaque predicate to be revealed when needed. Don't look inside function/predicate calls when doing this.

And I'd add another one closely related to the last one above:

• If any quantified expression, anywhere, includes a call to a function/predicate that is not treated opaquely in the current context (as controlled by opacity of the declaration or a hide statement), suggest making the target of that call opaque or hiding it in the current context.

[keyboardDrummer]

@atomb could you create separate GH issues for the above? I'd like to discuss, but rather not different ideas in one thread.