The opaque keyword does not always hide the body of functions

[keyboardDrummer]

Example:

function FibDef(n: nat): nat {
  if n < 2 then n else FibDef(n-1) + FibDef(n-2)
}

opaque function Hidden(): nat {
  3
}

opaque function Hidden2(): nat {
  FibDef(10)
}

function Visible(): nat {
  FibDef(10)
}

method User() { // Resource usage 3.74K RU
  var x := Hidden();
  assert 3 == 3;
}

method User2() { // Resource usage 5.86K RU
  var x := Hidden2();
  assert 3 == 3;
}

method User3() { // Resource usage 5.68K RU
  var x := Visible();
  assert 3 == 3;
}

You would expect User and User2 to have the same resource usage, and User3 to have a higher usage.

[keyboardDrummer]

Relevant boogie code for the above program:

// function declaration for _module._default.Hidden2
function _module.__default.Hidden2($reveal: bool) : int
uses {
// consequence axiom for _module.__default.Hidden2
axiom 1 <= $FunctionContextHeight
   ==> (forall $reveal: bool :: 
    { _module.__default.Hidden2($reveal) } 
    _module.__default.Hidden2#canCall() || 1 < $FunctionContextHeight
       ==> LitInt(0) <= _module.__default.Hidden2($reveal));
// definition axiom for _module.__default.Hidden2 (revealed)
axiom 1 <= $FunctionContextHeight
   ==> 
  _module.__default.Hidden2#canCall() || 1 < $FunctionContextHeight
   ==> _module.__default.FibDef#canCall(LitInt(10))
     && _module.__default.Hidden2(true)
       == LitInt(_module.__default.FibDef($LS($LZ), LitInt(10)));
// definition axiom for _module.__default.Hidden2 for all literals (revealed)
axiom 1 <= $FunctionContextHeight
   ==> 
  _module.__default.Hidden2#canCall() || 1 < $FunctionContextHeight
   ==> _module.__default.FibDef#canCall(LitInt(10))
     && _module.__default.Hidden2(true)
       == LitInt(_module.__default.FibDef($LS($LZ), LitInt(10)));
}

[MikaelMayer]

The opaque keyword provides the feature of not being able to prove something about the function's body. As such, it is working as intended. I did not expect the same resource unit thought, since there are many factors that can influence the number of resource units. For example, the shape of axioms we provide, which here is different when a function is opaque than when it's not.

My expectation there is only that making something opaque makes proofs go faster, but only at scale. On low verification, the noise is too big for me to expect anything.

[keyboardDrummer]

While this issue only shows a tiny example, I saw cases where the leakiness of an opaque function increased proof resource count to >1M RU. It seems like there's no bound to how much verification performance can be lost through leakiness of the opacity feature.

[keyboardDrummer]

Lowering severity since this is by design so it's a lack of documentation.

[keyboardDrummer]

Currently opaque is implemented by adding an additional reveal: bool parameter to opaque functions, and only defining the body when true is passed for this parameter. The trigger for the quantifier also requires the parameter to be true.

An option would be to leverage the Boogie pruning mechanic so it removes any assertions that are not revealed. The most direct way of doing that would be to add a pruning mode where, when building the usage graph that's used for pruning, references from a Boogie implementation to a function/const are not traversed unless that function/const is revealed. Revealing would happen at the Boogie command level, so if you have:

// --isolate-assertions 

if (*) {
  reveal P;
  assert P(2) == 2;
  assume false;
}
assume P(2) == 2;
assert P(2) + 1 == 3;

This would only bring the definition and contract of P in scope when proving assert P(2) == 2, but not when proving assert P(2) + 1 == 3. This assumes the Boogie level optimizations from https://github.com/dafny-lang/dafny/issues/5536 are implemented.

There is already an attribute to mark top level declaration so they and their reachables do not get pruned, which can be useful for the Dafny prelude.

This approach would also have the (desirable?) side-effect that not-revealing a function also hides its ensures clauses.

[MikaelMayer]

Yes indeed, that would sound like a good idea. Any sound pruning would make the SMT be less brittle.