Compilation of `:| assume` omitted

[RustanLeino]

Dafny version

4.4.0

Code to produce this issue

method Main() {
  var y;
  y :| y == 2;
  print y, " ";
  y :| assume {:axiom} y == 3;
  print y, "\n";
}

Command to run and resulting output

% dafny run test.dfy

Dafny program verifier finished with 1 verified, 0 errors
2 2

What happened?

The :| assume construct should be different from :| only in that it omits the proof obligation that a value exists. So, if the compiler does compile the program, then, in the event that the value actually does exist, the code should find it.

In other words,

y :| assume {:axiom} P(y);

should behave like

assume {:axiom} exists z :: P(z);
y :| P(y);

However, it seems the compiler emits no code for the :| assume statement, which is wrong.

Additional test case

method Main() {
  var y;
  
  y :| y == 2;
  print y, " ";

  assume {:axiom} exists z :: z == 3 && P(z);
  y :| y == 3 && P(y);
  print y, " ";

  y :| assume {:axiom} y == 4 && P(y);
  print y, "\n";
}

opaque predicate P(x: int) { true }

Currently, this gives:

% dafny run test.dfy

Dafny program verifier finished with 1 verified, 0 errors
2 3 3

but it should have printed 2 3 4.

What type of operating system are you experiencing the problem on?

Mac

[robin-aws]

After waffling a bit :) I feel this deserves the during 4: execution of correct program soundness issue label. If nothing else we hadn't defined correct program behavior in this case, but I don't think the current behavior (don't assign the variable anything at all!) could be correct. I think the correct behavior should be to search for a satisfying value just as we do without the assume, the caveat just being that the program may not terminate if no such value exists.

Note the followed program creates a runtime target language compiler crash from the same root cause, because the variable isn't assigned anything:

method Main() {
  var y :| assume {:axiom} y == 4 && P(y);
  print y, "\n";
}

opaque predicate P(x: int) { true }

% dafny run src/Scratch.dfy

Dafny program verifier finished with 1 verified, 0 errors
Errors compiling program into Scratch
(5051,28): error CS0165: Use of unassigned local variable '_0_y'

[robin-aws]

More specifically (since the lack of :| expect came up in #5165), I'd suggest both of these options:

var y :| expect P(y);             // Only allowed if the domain to search is provably finite
                                  // Always terminates but will halt if no such satisfying `y` exists
var y2 :| assume {:axiom} P(y);   // Allowed even if the search may be infinite, may not terminate at runtime

Edit: In both cases compilation should fail as it does now if the heuristics can't figure out how to compile the search at all.