Call-side opaque

[vkuncak]

We had an example where we need to assume a recursive function to be opaque while we verify it, but later we want to see its body to prove an inductive lemma. Thus, we want to control opaqueness at the call site level. This can be encoded along these lines: transform

def f(x: A): B = {
  E(opaque(f(t(x)))))
}

into:

def f(x: A): B = {
  E(f2(t(x)))))
}
@opaque def f2(x) = {
  f(x)
}

[vkuncak]

Here opaque is a function with identity run-time semantics that gets transformed away; a bit like we use specialize.

[vkuncak]

We have again ran into the need for this feature for internally generated calls in the full-imperative phase. Namely, we would like to state certain properties of the called function (that it depends only on its reads clause footprint). As a result, the call of a function f appears twice, but we are actually generating an assumption f(arg)==f(arg1). The intention is that we use the high-level fact about f, so even if we are unfolding f(arg), we do not want to unfold f(arg1), and thus would like to disable unfolding of this call.

[jad-hamza]

In the original post, if I think of f and f2 as properties, the problem is that since f2 is opaque, we can't prove that f2 implies f (outside those functions).

I'm thinking of having an inline keyword that would force inlining a function once, before the actual FunctionInliningPhase, and overriding @opaque. So for instance, if you have a complex function stating a property, you could keep it opaque most of the time, and have lemmas that talk about it. And when you need to use the property in a lemma, you would force inlining.

[jad-hamza]

The call-site inline idea doesn't work so well. If you have a predicate you'd like to keep opaque most of the time, such as: @opaque def p(x) = x > 0, then there's no way to relate the opaque p(x) call to the inlined predicate x > 0.

It'd be good to be able to prove lemmas such as:

def pWrap(x): Unit = {
  require(x > 0)
}.ensuring(_ => p(x))

def pUnwrap(x): Unit = {
  require(p(x)) 
}.ensuring(_ => x > 0)

We can add call-site inline to the p(x) in these lemmas, but the lemmas become useless from the outside, as they would state x > 0 <==> x > 0.

For this to work properly, p(x) would need to be inlined to prove the pWrap and pUnwrap lemmas, but shouldn't inlined when invoking the lemmas from the outside. We could do that, but that would an odd call-site inline behavior. Any thoughts?

[jad-hamza]

I've implemented @gsps's idea with unfold here: https://github.com/epfl-lara/stainless/pull/1174 It's not a call-site opaque, but should be good enough? Should we consider this fixed?