Combining permission amounts from folded predicate and QP incompleteness
JonasAlaif opened this issue · 2 comments
JonasAlaif commented
And another one, sorry @marcoeilers
The following program with quantified permissions and folding fails to verify in Silicon but works in Carbon:
field ref: Ref
predicate T(x: Ref) {
acc(x.ref)
}
method foo(lft: Map[Ref, Perm], x: Ref, p: Perm)
requires forall r: Ref :: r in lft && lft[r] >= 0/1 && lft[r] <= 1/1 && acc(T(r), lft[r])
requires p > 0/1 && acc(x.ref, p)
{
fold acc(T(x), p)
assert acc(T(x), p + lft[x])
}
The strange thing is that it works without the fold
:
method bar(lft: Map[Ref, Perm], x: Ref, p: Perm)
requires forall r: Ref :: r in lft && lft[r] >= 0/1 && lft[r] <= 1/1 && acc(T(r), lft[r])
requires p > 0/1 && acc(T(x), p) // <- get the predicate directly
{
assert acc(T(x), p + lft[x])
}
marcoeilers commented
Everything verifies for me with master Silicon (and no options).
JonasAlaif commented
Seems that it was also fixed by #696, sorry I didn't think the two were related :P