Unfolding predicate with rd() permission might fail

[fpoli]

The following verifies in Carbon but generates an error in Silicon:

field f: Ref

function rd(): Perm
    ensures result > 0/1
    ensures result < 1/1

predicate G(self: Ref)

predicate F(self: Ref) {
    acc(self.f, rd()) && G(self.f)
}

method test(x: Ref)
    requires acc(F(x), rd())
{
    // Carbon: ok
    // Silicon: Unfolding F(x) might fail. There might be insufficient permission to access self.f.
    unfold acc(F(x), rd())
}

[mschwerhoff]

Potentially related: #367, #480, #481

[fpoli]

Why is self.f checked to have enough permission?

[mschwerhoff]

In Silicon, well-definedness checks are often intertwined with producing/consuming assertions. Upon unfolding, there might thus be errors from a potentially not well-defined predicate body. I guess that here, the permission-wise scaled body can't be shown to be well-defined, due to the Z3 incompleteness.

[fpoli]

I see, so when unfolding acc(F(x), rd()) Silicon checks that the scaled acc(self.f, rd() * rd()) is enough to access the self.f in G(self.f).

But then, why does the well-definedness check run on the scaled predicate body at the unfolding site? Isn't it possible to check once for all that the original (non-scaled) predicate body is well-defined?

[mschwerhoff]

Yes, but that would actually make Silicon's implementation quite a bit more complex. Unlike Carbon, which implements total heap semantics, Silicon can't (easily) handle a heap access if permissions are missing, and it Silicon therefore always checks for permissions.

Another question, but that just occurred to me now, is how to handle degenerate cases such as the following:

field f: Int

predicate P(x: Ref, y: Ref) {
    acc(x.f) && x.f > 0 && (x.f > 0 ==> y != null) // Is well-defined
}

method test(x: Ref, y: Ref) {
    inhale acc(P(x, y), none)
    unfold acc(P(x, y), none) // Fails in Silicon
    assert y != null // Succeeds in Carbon, but shouldn't
}

Well, I guess we should simply forbid unfoldings with no permissions.

[fpoli]

For a similar case, I found that it's enough to assume none < rd() * rd() before the unfold, like in the following program. For some reason, adding that property to the postcondition of rd() is not enough.

field value: Int
field inner: Ref

function read(): Perm
    ensures none < result && result < write

method ReadPermLemma()
    ensures none < read() * read()

predicate Inner3(self: Ref) {
    acc(self.value)
}

predicate Inner2(self: Ref) {
    acc(self.inner) && acc(Inner3(self.inner), read())
}

predicate Inner1(self: Ref) {
    acc(self.inner) && acc(Inner2(self.inner), read())
}

predicate T(self: Ref) {
    acc(self.inner) && acc(Inner1(self.inner), read())
}

function lookup(x: Ref): Int
    requires T(x)
    requires none < read() * read()
{
    unfolding T(x) in
    unfolding acc(Inner1(x.inner), read()) in
    unfolding acc(Inner2(x.inner.inner), read() * read()) in
    unfolding acc(Inner3(x.inner.inner.inner), read() * read() * read()) in
    x.inner.inner.inner.value
}

method test(x: Ref)
    requires T(x)
{
    ReadPermLemma()
    unfold T(x)
    unfold acc(Inner1(x.inner), read())
    unfold acc(Inner2(x.inner.inner), read() * read())
    unfold acc(Inner3(x.inner.inner.inner), read() * read() * read())
}

[mschwerhoff]

Verification fails with Z3 4.8.7, but succeeds with Z3 4.8.9 and 4.8.14. I'll therefore close this issue.