opaque and literals

[Chris-Hawblitzel]

The recent change to opaque ("Rewrite opaque using fuel", commit 01f90e6) causes a change in behavior with opaque functions. Here's an example:

function{:opaque} f(i:int):int { if i > 0 then 1 + f(i - 1) else 0 }

lemma L(x:int)
  requires 10 <= x <= 11 || 20 <= x <= 21;
{
  assert f(x) == x; // it's surprising that this verifies when opaque f is never revealed
}

This verifies even though f is never revealed, because the literals 10, 11, 20, and 21 trigger an axiom that doesn't respect opaque. I worry that this will make it harder to diagnose slow verification performance. Usually, with opaque, I'm confident that the body of an opaque function isn't the cause of slow verification, as long as the function's body is never revealed. With the special behavior for literals, I have to worry that slow performance might be due to the body of an opaque function after all, depending on what literals are in scope.

An alternative would be to make the axiom for literals for opaque functions require fuel, just like the axiom for non-literals for opaque functions, so that opaque behaves more consistently between literals and non-literals. Maybe the literal axiom could still run without consuming the fuel that it's given, but it would need non-zero fuel to get triggered in the first place.

[parno]

This was closed by commit a56aa9a.