Incompleteness for heap-dependent functions with quantified permissions
Opened this issue · 3 comments
Hello,
I've found an unknown source of incompleteness in Silicon while working with heap-dependent functions that are set-valued (and hence require quantified permissions).
The following Viper code will verify in Carbon, but not Silicon:
field f: Bool
function hfun(rs: Set[Ref]): Bool
requires (forall r: Ref :: { (r in rs) } (r in rs) ==> acc(r.f))
method test1(rs: Set[Ref])
requires (forall r: Ref :: { (r in rs) } (r in rs) ==> acc(r.f))
{
assume (forall rs2: Set[Ref] :: { (rs2 subset rs) }
(rs2 subset rs) ==> hfun(rs2))
// fails in Silicon -- assertion may not hold
assert (forall rs2: Set[Ref] :: { (rs2 subset rs) }
(rs2 subset rs) ==> hfun(rs2))
}
(This is a minimized example; my original issue used a heap-dependent trigger on a limited version of hfun
, i.e. { hfun_prime(rs2) }
, and also had the assume (forall rs2 ...)
statement written as a postcondition for hfun
, but neither of these seem to be the source of incompleteness, so I have simplified things here.)
On the other hand, Silicon (and Carbon) will verify a variant of this code where hfun
is not set-valued and therefore lacks the precondition for quantified permissions:
field f: Bool
function hfun_single(r: Ref): Bool
requires acc(r.f)
method test2(rs: Set[Ref])
requires (forall r: Ref :: { (r in rs) } (r in rs) ==> acc(r.f))
{
assume (forall r: Ref :: { (r in rs) }
(r in rs) ==> hfun_single(r))
// verifies in Silicon
assert (forall r: Ref :: { (r in rs) }
(r in rs) ==> hfun_single(r))
}
Is there any reason why this might be expected behaviour in Silicon, perhaps based on Silicon's heap model?
Is there any reason why this might be expected behaviour in Silicon, perhaps based on Silicon's heap model?
No, this is not expected, it's an incompleteness. I'll look into it.
Turns out there is an old issue that seems to describe the exact same problem (that I just didn't know about): #327
I'm working on a fix.
Thanks! Sorry, I had done a search through old issues, but I guess I had missed that one.