Misleading "verified" gutter icon

[MikaelMayer]

Context and issue

After one year of writing Dafny and looking at how people write Dafny code in everyday's life, I came to realize that many of us use assume false for temporary verification debugging. And this is an accepted way of debugging when verification is slow, for example. When I designed the gutter icons, I did not realize this would cause a conflict, but there is one now that I realized.

It occurred several times that I got the feedback that a user was editing a quite long method, and forgot they had added "assume false" in some places, and the function suddenly verifies.
So they are happy and move on to something else. But...
only later, when they want to compile (if they have the chance to, some never get to this stage and only use Dafny as a model checker), will they realize that they had forgotten one case. That latency is a source of frustration. Having gutter icons telling them the method is "verified" when it had some yet unproven assumptions feels not supportive.
This is not really a bug, this was only a design choice that was missing an element.

Example

For example, let's say, after fixing case 1 => , the whole gutter icons turn green below:

The user is happy and moves on to something else
They might have forgotten, after hours of writing y := 4, that there is still an assumption in their code that wouldn't compile.
The fact that we show "green line" is thus misleading.

Recommended solution for gutter icons

I strongly suggest we consider a new set of icons that, in addition to all the others existing icons,

• Conveys immediately the notion that the entire method is conditionally verified, i.e. some assume remain in its body.
• Indicate in the gutter where the assumptions are (but only when the method is fully verified, not when there are errors elsewhere).
• Is of course accessible (does not rely only on color, but also on shape)

This should hold not only for statements like assume {:false}, but also for any declarations that can have expressions to verify, because one could insert "assume false;" in these expressions as well. Hence, this needs to be done for

• Constant declaration with righ-hand-side
• Datatype constructors with default values
• Functions and methods, and by-method bodies of functions
• Right-hand side of subset types and newtypes
  The only place where we would not report assumptions are assume true, as in assume {:split_here} true

We might have other design ideas (i.e. warnings in diagnostics, exposing all compiler issues and not just verification issues, etc.) , but gutter icons are de facto one of the most important source of visual verification feedback for our users, so any other approach would be complementary.

[cpitclaudel]

I recently changed the way assume false looks in the Emacs mode:

… this might be an easy improvement to make on top of the changes you suggest.

[MikaelMayer]

This is nice, but what about assume {:split_here} true that is used by some of our users?

[dijkstracula]

Is it possible that this could be extended to annotating precondition contradictions as well? I was recently bitten by a super-silly precondition, essentially of the form requires x < x for some x: int, and only much later did I realise I had, somewhere, tied myself in a knot[1]. By this point, the contradition was in a totally different module that I had paged out of my mind, so it took awhile to find.

[1]: power dafny user lesson 1: if your code is consistently passing the verifier and you're starting to think, "boy, am I ever good at writing correct programs", be wary ;-)

[MikaelMayer]

Is it possible that this could be extended to annotating precondition contradictions as well? I was recently bitten by a super-silly precondition, essentially of the form requires x < x for some x: int, and only much later did I realise I had, somewhere, tied myself in a knot[1]. By this point, the contradition was in a totally different module that I had paged out of my mind, so it took awhile to find.

This is a very interesting idea that indeed deserves to be studied on its own. It has its own challenges:

• Trying to prove "false" when it's not possible can be extremely expensive for a verifier. How to ensure we can do both? Maybe caching down the road?

This issue is different, it's about the usual construct assume false that developers add to their code to verify fast a portion of it, to help them verify a portion of it.
Would this help in your case if, besides "false", we also added the following patterns that are statically easy to recognize, not only for assumes, but also for requires?

x < x    where x is a variable
x > x
x != x
x == x.field  where x is a datatype.
exists x :: E where can be easily inferred to be always false
!E where E can be easily inferred to be always true
E && B   if E or B are always false.
E || B   if E and B are always false.

[dijkstracula]

Trying to prove "false" when it's not possible can be extremely expensive for a verifier.

This makes a lot of sense; I wasn't sure whether solving this particular issue was a matter of statically checking for "assert <expression that the solver, through its solver magic, can conclude will always be false>". It does make sense that that's a potentially-expensive computation.

Happy to split this conversation out into its issue so this one doesn't get cluttered up :-)

[RustanLeino]

A user should never write assume {:split_here} true. They should write assert {:split_here} true. So, there's no reason to ignore certain assume statements.

[MikaelMayer]

A user should never write assume {:split_here} true. They should write assert {:split_here} true. So, there's no reason to ignore certain assume statements.

Are you saying that assume {:split_here} true does not do the assertion splitting, or that it is bad practice? I have seen it in user codebases.

Agreed to not ignore assume statements in general. Another problem we encountered by changing the background color of elements is the impression that things are "selected", when they are not. So in that sense it's also good to decouple visual feedback.