Opaque Functions

Opaque Functions

Opaque pure functions let you hide implementation details from the current proof scope. This can improve proof stability and performance when inlining function bodies causes heavy solver load.

Core idea

• Mark a pure function as opaque.
• Calls to that function do not automatically expose the body.
• If you need body-level reasoning at a specific point, use reveal.

An Opaque function body is hidden by default.

opaque pure bool f(){
  return true;
}

void test(){
  assert f();
}

The assertion fails because the body is hidden.

You can use reveal to reason with the body

opaque pure bool f(){
  return true;
}

void test(){
  assert reveal f();
}

When to use opaque

Use opaque when:

• callers only need the contract/summary of a pure function
• inlining the function body leads to brittle or slow proofs
• the function is used frequently and body details are irrelevant in most call sites.

As example consider a function which precisely describes the functional correctness of an algorithm, but the algorithm consists of many branches and loops. In that case only innermost loop when the correctness of such a function is determined needs to reveal its body, and most other call sites do not need to know this. See the following example, where we only need reveal ones twice, and can use it twice without knowing its body.

  requires 0 <= n && n <= |a|;
opaque pure int ones(seq<int> a, int n) =
  n == 0 ? 0 : ones(a, n - 1) + (a[n - 1] == 1 ? 1 : 0);

  requires 0 <= n && n <= |a|;
  ensures \result == ones(a, n);
int countOnes(seq<int> a, int n)
{
  int i = 0;
  int c = 0;
  assert reveal ones(a, i) == 0;

   loop_invariant 0 <= i && i <= n;
   loop_invariant c == ones(a, i);
  while (i < n)  {
    int add = (a[i] == 1 ? 1 : 0);

    // Only here we need the body of ones:
    // unfold ones(a, i + 1) into ones(a, i) + add
    assert reveal ones(a, i + 1) == ones(a, i) + add;

    c = c + add;
    i = i + 1;
  }

  return c;
}

Trade-offs and limitations

• You lose automatic body-level facts at call sites.
• Assertions that rely on body details can fail unless you reveal.
• Revealing too much can re-introduce the same proof-scope explosion you were trying to avoid.

A common strategy is: keep functions opaque by default, and reveal only in small local proof points.