Extending a trait with an opaque function causes error, but only on the commandline and not on VSCode.

[EkanshdeepGupta]

Dafny version

4.1.0

Code to produce this issue

trait T {
  opaque function bar(): (r: int)
}

class F extends T {
  constructor() {}
  opaque function bar(): (r: int) {
    1
  }
}

Command to run and resulting output

$ ./Binaries/Dafny verify  ~/test/git-issue-549.dfy
git-issue-549.dfy(2,18): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
git-issue-549.dfy(2,18): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
git-issue-549.dfy(6,18): Error: wrong number of arguments to function: _module.F.bar (2 instead of 3)
git-issue-549.dfy(2,18): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
git-issue-549.dfy(6,18): Error: wrong number of arguments to function: _module.F.bar (2 instead of 3)
5 type checking errors detected in /var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl(2958,6): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl(2959,8): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl(2959,29): Error: wrong number of arguments to function: _module.F.bar (2 instead of 3)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl(2962,11): Error: wrong number of arguments to function: _module.T.bar (1 instead of 2)
/var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl(2962,34): Error: wrong number of arguments to function: _module.F.bar (2 instead of 3)
5 type checking errors detected in /var/folders/v7/dtr5626966sf_f5665tczxpw0000gr/T/git-issue-549__module.bpl

What happened?

In the Boogie translation, the override axiom for _module.T.bar in class _module.F seems to have the reveal argument missing.

Lines 2955 to 2962 of boogie_print.bpl:

// override axiom for _module.T.bar in class _module.F
axiom 0 <= $FunctionContextHeight
   ==> (forall this: ref :: 
    { _module.T.bar(this), $Is(this, Tclass._module.F()) } 
      { _module.T.bar(this), _module.F.bar($LZ, this) } 
    _module.F.bar#canCall(this)
         || (0 < $FunctionContextHeight && this != null && $Is(this, Tclass._module.F()))
       ==> _module.T.bar(this) == _module.F.bar($LZ, this));

Whereas, lines 2810-2811:

// function declaration for _module.T.bar
function _module.T.bar($reveal: bool, this: ref) : int;```


Interestingly, this example still verifies on the VSCode extension, but not on the command-line.

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

Mac

[MikaelMayer]

I was able to look at the generated boogie code from the language server and the CLI. Here are the differences:

VSCode => CLI

 implementation {:verboseName "F.bar (override check)"} OverrideCheck$$_module.F.bar(this: ref)
 {
   var F_$_Frame: <beta>[ref,Field beta]bool;
 
     // initialize fuel constant
     assume AsFuelBottom(StartFuel__module.F.bar) == StartFuel__module.F.bar;
     assume AsFuelBottom(StartFuelAssert__module.F.bar) == StartFuelAssert__module.F.bar;
     assert true;
-    F_$_Frame := lambda#0(null, $Heap, alloc, false);
+    F_$_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: 
+      $o != null && read($Heap, $o, alloc) ==> false);
     assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> false);
 }

Also, in a lot of other places, I see diffs like this, where VSCode emits an equivalence sign, and CLI emits an ==. @RustanLeino any insights on why that might be the case?
VSCode => CLI

 // #requires axiom for _module.F.bar
 axiom (forall $ly: LayerType, this: ref :: 
   { _module.F.bar#requires($ly, this) } 
   this != null && $Is(this, Tclass._module.F())
-     ==> (_module.F.bar#requires($ly, this) <==> true));
+     ==> _module.F.bar#requires($ly, this) == true);

[MikaelMayer]

But the problem is not in the comparison above. The CLI generates an extra boogie file that VSCode does not, which is suffixed with _module. I guess it's the exported version of the module.

// function declaration for _module.T.bar
function _module.T.bar($reveal: bool, this: ref) : int;
....
// override axiom for _module.T.bar in class _module.F
axiom 0 <= $FunctionContextHeight
   ==> (forall this: ref :: 
    { _module.T.bar(this), $Is(this, Tclass._module.F()) } 
      { _module.T.bar(this), _module.F.bar($LZ, this) }     // Here is the missing reveal argument
    _module.F.bar#canCall(this)
         || (0 < $FunctionContextHeight && this != null && $Is(this, Tclass._module.F()))
       ==> _module.T.bar(this) == _module.F.bar($LZ, this));