Unknown QP unsoundness

[JonasAlaif]

The following program verifies in Silicon (latest Nightly, more complete exhale disabled), but fails in Carbon as expected

field ref: Ref
field f: Ref
field n: Ref

predicate T(x: Ref)
predicate List(x: Ref) {
  x != null ==> acc(x.ref) && Node(x.ref)
}
predicate Node(x: Ref) {
  acc(x.f) && acc(x.f.ref) && T(x.f.ref) &&
  acc(x.n) && acc(x.n.ref) && List(x.n.ref)
}
define ref_T(x, lft, mut) (valid_lft(lft) && x in lft[tpT] && (mut ==> lft[tpT][x] == 1/1))
define ref_List(x, lft, mut) (valid_lft(lft) && x in lft[tpListT] && (mut ==> lft[tpListT][x] == 1/1))
predicate ListRef(x: Ref, lft: Map[Int, Map[Ref, Perm]], mut: Bool) {
  x != null ==> acc(x.ref) && NodeRef(x.ref, lft, mut)
}
predicate NodeRef(x: Ref, lft: Map[Int, Map[Ref, Perm]], mut: Bool) {
  acc(x.f) && acc(x.f.ref) && ref_T(x.f.ref, lft, mut) &&
  acc(x.n) && acc(x.n.ref) && ListRef(x.n.ref, lft, mut)
}

define tpT 0
define tpListT 1

predicate lft_T(x: Ref) {
  acc(x.ref) && T(x.ref)
}
predicate lft_List(x: Ref) {
  acc(x.ref) && List(x.ref)
}
define Lifetime(lft) (valid_lft(lft) && LifetimeP(lft))
predicate LifetimeP(lft: Map[Int, Map[Ref, Perm]]) {
  valid_lft(lft) &&
  (forall x: Ref :: x in lft[tpT] ==> lft[tpT][x] > 0/1 && lft[tpT][x] <= 1/1 && acc(lft_T(x), lft[tpT][x])) &&
  (forall x: Ref :: x in lft[tpListT] ==> lft[tpListT][x] > 0/1 && lft[tpListT][x] <= 1/1 && acc(lft_List(x), lft[tpListT][x]))
}
function valid_lft(lft: Map[Int, Map[Ref, Perm]]): Bool {
  tpT in lft && tpListT in lft
}

function get_disc(x: Ref, lft: Map[Int, Map[Ref, Perm]]): Ref
  requires Lifetime(lft)
  requires ref_List(x, lft, false)
{
  unfolding LifetimeP(lft) in unfolding acc(lft_List(x), wildcard) in x.ref
}

method foo(x: Ref, lft: Map[Int, Map[Ref, Perm]]) returns (res: Ref, new_lft: Map[Int, Map[Ref, Perm]])
  requires Lifetime(lft)
  requires acc(x.ref) && ref_List(x.ref, lft, false)
  ensures Lifetime(new_lft)
  ensures acc(res.ref) && ListRef(res.ref, new_lft, false)
  ensures Lifetime(new_lft) --* Lifetime(lft)
{
  new_lft := lft
  package Lifetime(new_lft) --* Lifetime(lft)

  inhale acc(res.ref)
  res.ref := null
  fold ListRef(res.ref, new_lft, false)

  while (get_disc(x.ref, new_lft) != null)
    invariant Lifetime(new_lft)
    invariant acc(x.ref) && ref_List(x.ref, new_lft, false)
    invariant acc(res.ref) && ListRef(res.ref, new_lft, false)
    invariant Lifetime(new_lft) --* Lifetime(lft)
  {
    unfold LifetimeP(new_lft)
    assert x.ref in new_lft[tpListT]
    unfold acc(lft_List(x.ref), new_lft[tpListT][x.ref])
    var x_nxt: Ref
    x_nxt := sh_borrow(x.ref, new_lft[tpListT][x.ref])
    assert x_nxt.ref == x.ref.ref

    fold acc(lft_List(x.ref), new_lft[tpListT][x.ref]/2)
    fold LifetimeP(new_lft)

    fold acc(lft_List(x_nxt), new_lft[tpListT][x.ref])

    new_lft := new_lft
  }
}

method sh_borrow(a: Ref, p: Perm) returns (bw: Ref)
  requires p > 0/1 && acc(a.ref, p)
  ensures acc(a.ref, p/2) && a.ref == old(a.ref)
  ensures acc(bw.ref, p/2) && bw.ref == a.ref
  ensures acc(bw.ref, p/2) --* acc(a.ref, p/2) && old[lhs](bw.ref) == a.ref
{
  bw := a
  package acc(bw.ref, p/2) --* acc(a.ref, p/2) && old[lhs](bw.ref) == a.ref
}

It should fail at the fold LifetimeP(new_lft) line since we only have acc(lft_List(x.ref), new_lft[tpListT][x.ref]/2) and not acc(lft_List(x.ref), new_lft[tpListT][x.ref]). Another strange thing is that the fold acc(lft_List(x_nxt), new_lft[tpListT][x.ref]) also passes; here we should only have enough perms left to fold new_lft[tpListT][x.ref]/2.

[marcoeilers]

I just merged PR #694 (which just drops some old Z3 options) and now this example no longer verifies.
So there is a chance this was an issue with a weird Z3 option, or there is an unsoundness somewhere in some axiom that is now no longer triggered.

[JonasAlaif]

I tried with that PR and it fixes something:

• fold acc(lft_List(x_nxt), new_lft[tpListT][x.ref]) now fails as expected
• fold LifetimeP(new_lft) still doesn't fail (try removing the failing line above)

[marcoeilers]

Really?? For me, it fails on theLifetimeP fold every time. Interesting.

[JonasAlaif]

Hmm I'm running it from the IDE so maybe I'm still using a different version. I'll double check

[marcoeilers]

Either way it's not a Z3 bug then (that seemed kind of unlikely in the first place). Looking into it.

[JonasAlaif]

Could you just doublecheck what behavior you get right before the Z3 PR, just to see if it matches what I saw

[marcoeilers]

I did check that, the file verified.

[JonasAlaif]

Hmm so you can't reproduce the issue? Strange

[marcoeilers]

? I can reproduce the issue. It's not supposed to verify, right, but it did.

[JonasAlaif]

Ah oops, sorry I misunderstood your comment - I automatically took "the file verified" to mean "all good", but here that's not the case 😄

[JonasAlaif]

I tried with that PR

Btw this is not true; I thought the PR was from 4 days ago, but it was only just merged - I think that the fold acc(lft_List(x_nxt), new_lft[tpListT][x.ref]) failing/passing is unstable; imo the whole thing is probably some triggering limit - I've been running into issues with this file where I e.g. can't verify:

fold acc(T(x), p)
assert acc(T(x), p) // Error

But if that's the case then the soundness of Silicon QPs relying on triggering is pretty sketchy

[marcoeilers]

No, of course it shouldn't rely on triggering for soundness (and it doesn't in any way I know of).
But I found the issue, it was a general problem when folding a predicate with a multiplier that's not write if the predicate is used in a QP somewhere. Surprising that that wasn't found earlier.

[marcoeilers]

Fixed in PR #696