Incompleteness for heap-dependent functions with quantified permissions

[jwkai]

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?

[marcoeilers]

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.

[marcoeilers]

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.

[jwkai]

Thanks! Sorry, I had done a search through old issues, but I guess I had missed that one.

[marcoeilers]

Sorry, I started working on this and then somehow forgot about it. It's finally fixed now in https://github.com/viperproject/silicon/pull/935.