`unfolding` body does not admit resources

[pieter-bos]

Viper disallows putting resource assertions in the body of an unfolding:

field f: Int

predicate p(x: Ref) { acc(x.f, 1/4) }

method test(x: Ref)
requires p(x)
requires unfolding p(x) in p(x)
{
}

reports in the Viper IDE:

• Consistency error: acc(p(x), write) is non pure and appears where only pure expressions are allowed. ([email protected])

I noticed that this is not mentioned in the tutorial, so I was wondering whether there is a technical reason that this is not allowed?

Also, I suspect it may be possible to desugar impure unfolding expressions into pure ones, by pushing in the unfolding into the pure bits of the expression (unfolding pr() in acc(x.f, p) -> acc((unfolding pr() in x).f, unfolding pr() in p), unfolding pr() in x && y -> (unfolding pr() in x) && (unfolding pr() in y), etc.). We're considering implementing that, so I'm also interested in whether you would implement something like this, or see a glaring flaw with this plan.

[mschwerhoff]

Hi Pieter, interesting observation! The tutorial even hints at the opposite:

Viper supports assertions of the form unfolding P(...) in A, which temporarily unfolds the predicate instance P(...) for (only) the evaluation of the assertion A.

My guess is that we accidentally forbid in-assertions when adding a consistency checker that prevents impure unfoldings in expression position, in particular function bodies.

We'll discuss, and I'll get back to you.

[marcoeilers]

For what it's worth, Silicon crashes if it gets an impure assertion in this position. So if we get rid of the consistency check, we'll also need to extend the backend(s).