Define backwards compatibility constraints for verification changes

[robin-aws]

A tricky thing about Dafny is that verification performance can change pretty dramatically with small changes in either Dafny source or the translation heuristics. Seemingly innocuous changes in Dafny can "break" existing code because it makes verification take slightly longer, to the point where builds time out and fail.

Dafny cannot commit to never making verification slower in any case, but at what point does an optimization with tradeoffs have to be off by default or bump the major version number?