opaque function called within lambda is not opaque!

[DavePearce]

Dafny version

4.0.0

Code to produce this issue

// Function want to verify something about
opaque function inc(x:nat) : nat { x + 1 }

// Intermediatary to force lambda
predicate Check(p: ()->bool) { p() }

method test() {
    assert Check(() => inc(1) == 2);
}

Command to run and resulting output

No response

What happened?

The assertion verifies when it should not because there is no specification of inc() and, furthermore, inc() is marked opaque. The problem persists when using the attribute syntax {:opaque} as well. Finally, observe that this assertion does not verify as expected:

assert inc(1) == 2;

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

Linux

[MikaelMayer]

I am investigating the problem. So far:

• The call of "inc" is not translated the same whether it's stand-alone or inside the lambda.
  Stand-alone:

(_module.__default.inc(StartFuel__module._default.inc, LitInt(1))

In the lambda:

            AtLayer((lambda $l#9#ly#0: LayerType :: 
              Handle0((lambda $l#9#heap#0: Heap :: 
                  $Box(_module.__default.inc($l#9#ly#0, LitInt(1)) == LitInt(2))), 
                (lambda $l#9#heap#0: Heap :: true), 
                (lambda $l#9#heap#0: Heap :: SetRef_to_SetBox((lambda $l#9#o#0: ref :: false))))), 
            $LS($LZ))

So our translation is somehow incorrect. The first construction (outside of the lambda) correct prevents the verifier from picking up the axiom of "inc" until Reveal is properly called.
In the lamdda however, it seems that the fuel used is the one captured by the lambda and hard-coded as 1, whereas it should depend on every function call, at least locally in the lambda. It is possible that this fuel is there to reset all other fuel types
I did another experiment, by adding two "inc" like functions, and they are each provided the same fuel as the lambda.

Another interesting experiment:

method test() {
    assert Check(() => assert inc(1) == 2;inc(1) == 2);
}

Here the check verifies, but not the inner assert. This is because the inner assert is checked as part of the well-formedness, and there it's using the correct fuel that can be revealed or not.
However, for the check, it's using a fuel of 1.

Looking at the difference between the two calls, in the stand-alone version, the "amount" is set to low = 1, whereas in the lambda, the amount is set to low = 0. Will investigate.

[MikaelMayer]

Another interesting case:

method test() {
    var l := () => assert inc(1) >= 2;inc(1) == 2;
    assert Check(l);  // Error on this one
}

In this one, it cannot prove the assertion inner to the definition of l because it's lacking fuel. However, it can still prove the assert on the line afterwards.
When looking at the definition of Check, we find that the definition of check does not have any fuel because Check is not opaque.

_module.__default.Check(p#0) == $Unbox(Apply0(TBool, $Heap, p#0)): bool);

Another interesting example

opaque const one: nat := 1

method test() {
    assert CheckThis(() => inc(one) == 2);  // Error on this one
}

Here, since constants have a slightly different reveal mechanism that does not involve fuel, the check fails. The fuel passed in the lambda cannot be used for the constant. Revealing the constant anywhere (except in the body of the lambda) makes the check to pass.

My take away is that we shouldn't rely on layer/fuel to "reveal". Opaqueness It should be a different mechanism. I think I found a better way. I'll write a write-up about this.

[MikaelMayer]

Another interesting example

method test() {
  var x := inc(1);
  assert CheckThis(() => x == 2);  // Error on this one
}

This one fails, although we just extracted inc(1) from the lambda.