Change the implementation of reveal/opaque to binary trigger, not fuel

[MikaelMayer]

How opaque is currently implemented

To ensure recursive functions do not unroll indefinitely, Dafny uses a "fuel" attribute, which is set to 2 in the context of an assert, and 1 in the context of an assume. It ensures the axioms of the function do not unroll the function more than required.
For example:

function inc(i: nat): nat {
  if i == 0 then 0 else inc(i-1) + 1
}

method Test(i: nat)
  requires i >= 3
{
  assert inc(i) == inc(i-3) + 3;
}

Dafny is unable to prove the assertion. However, if we replace the 3s by 2s, Dafny would succeed.

The amount of fuel that can be used is currently an annotation on the function {:fuel <lowfuel>,<highfuel>}.
Interestingly, if we set up this fuel to 0,0 or unknown constants, the function body is never available. This insight made it possible to figure out an opaque mechanism: Pretend the fuel is an unknown constant. To reveal it, assume this unknown constant is 1+another constant for assumptions or 1+(1+another constant) for assertions, which let the axioms unfold the function as usual.

For opaque functions, the attribute {:fuel } actually sets up the increase from another constant. It's just that these values are revealed only when passed to reveal().

Problems with opaque = assumption of non-zero fuel

• In opaque function called within lambda is not opaque! #3719, the problem is that opaque functions are provided with constant non-zero fuel that comes from a lambda expression. Looking at the code, it looks like it's by design, as a lambda expression starts a built-in function AtLayer which automatically provides a global fuel for the expressions below
• The notion of opaqueness is binary, either we reveal something or we don't, whereas here we need to maintain the value of constants
• It's not possible to set up the fuel for solving an assert at the time of the assertion.

Proposed solution

Currently, fuel is encoded as unary numbers: 0 = $LZ and 1 + fuel = $LS(<fuel>) and uninterpreted variables for opaque functions.
I suggest that the opaqueness of functions be not related to the fuel, so that there is no interference. Whenever we have an opaque function call P(<fuel>, x), we would thus have as first fuel argument the following expression:

P(CanRevealFuel(<contextFuel>, is_revealed_p), x)

is_revealed_p is a bool constant

The axiom is that

CanRevealFuel($LS(ly), true) == $LS(CanRevealFuel(ly, true))

meaning that without knowing is_revealed_p, it's never possible to extract fuel from a CanRevealFuel() expression.
And the reveal() call would do nothing else than assuming is_revealed_p

[RustanLeino]

Thank you for the clear write-up and the clever suggestion. It would be very nice to, as you state, divorce the opaqueness encoding from the fuel encoding.

I presume CanRevealFuel(..., is_revealed_p) would only be used if function p is opaque.

I have but one concern, which is what happens when this encoding is used inside a quantifier. Suppose a user writes a Dafny expression

forall x :: 10 <= x < 20 ==> P(x)

This would be translate into Boogie as

(forall x: int ::
    { P(CanRevealFuel($LS($LZ), is_revealed_P), x) }
    10 <= x && x < 20 ==> P(CanRevealFuel($LS($LZ), is_revealed_P), x))

I have filled in the trigger in the way that Dafny's auto-trigger would. Note that a trigger does not get massaged by the SMT solver. So, even if is_revealed_P is known to be true in the context, there has to be a term

P(CanRevealFuel($LS($LZ), true), E)

floating around in order for the SMT solver to instantiate the quantifier with x := E. That is, it's not enough if the context has a term P($LS(...), E).

It would be good to:

• Experimentally confirm what I said (by manually editing a Boogie program and checking whether or not the SMT solver is willing to instantiate the quantifier in a context where is_revealed_P is true and the term P($LS(...), E) is present).
• Consider updating the proposal to erase CanRevealFuel wrappers in triggers. That is, if auto-triggers would want to use the (translation of a) Dafny expression ... P(E) ... in a trigger, then instead of emitting that trigger as ... P(CanRevealFuel(X, ...), E) ..., it would erase the CanRevealFuel wrapper and instead emit the trigger as ... P(X, E) .... Would this still have the benefits that the proposal is trying to provide?

[MikaelMayer]

That is, it's not enough if the context has a term P($LS(...), E)

That's a very good observation. The thing I envision is that, for every call to P translated to Boogie, I'm using this CanBeRevealed wrapper.
So it's normally actually equivalent to adding one more boolean "reveal" argument between the fuel and the first argument. You could say, it's another kind of fuel, perhaps the oxygen, that is not turned on by default for opaque functions.

Experimentally confirm what I said (by manually editing a Boogie program and checking whether or not the SMT solver is willing to instantiate the quantifier in a context where is_revealed_P is true and the term P($LS(...), E) is present).

So I wrote the following Dafny program

opaque predicate P(x: int) {
  0 <= x
}

method test() {
  assume forall x :: 10 <= x < 20 ==> P(x);
  reveal P();
  assert P(12);
}

And I manually changed P(12) so that it does not use CanRevealFuel, and indeed, even if I comment out reveal P(); it no longer verifies, like you say because it cannot instantiate the axiom. But in practice this should not happen if every call to P has this CanRevealFuel as first argument.

Consider updating the proposal to erase CanRevealFuel wrappers in triggers. That is, if auto-triggers would want to use the (translation of a) Dafny expression ... P(E) ... in a trigger, then instead of emitting that trigger as ... P(CanRevealFuel(X, ...), E) ..., it would erase the CanRevealFuel wrapper and instead emit the trigger as ... P(X, E) .... Would this still have the benefits that the proposal is trying to provide?

Because of the observation above, erasing CanRevealFuel does not seem necessary, unless you see a context in which CanRevealFuel would not be added in the first argument (i.e. if we are translating function calls different ways which are not all in sync); in which case I would instead argue to add one more argument besides the fuel to the functions, to flatten the list of arguments.