Verifcation of "passing on" permissions fails

[bobismijnnaam]

In the example below permissions are shifted to the right. That is, first permissions are stated in terms of acc(nodes[j].out, write), and then they are stated in terms of acc(nodes[j + 1 % n], write) (more or less). After that shift and doing some work, we'd like to transition back to acc(nodes[j].out, write) from the translated state. This last step, transitioning back, carbon cannot verify. Silicon verifies the snippet below as-is. Is this to be expected, or can carbon be improved to also verify this? We'd like to be able to use carbon for the code the below snippet is derived from, because carbon is a lot faster than silicon in this case.

field out: Int

function next(i: Int, size: Int): Int
  requires 0 < size
  requires 0 <= i && i < size
  ensures 0 <= result && result < size
{
  (i <= 0 ? i - 1 + size : i - 1)
}

method parThreads(diz: Ref, nodes: Seq[Ref], globals: Ref)
  requires diz != null
  requires 0 < |nodes| ==> |nodes| == 3
  requires (forall tid: Int :: { nodes[next(tid, |nodes|)].out } 0 <= tid && tid < |nodes| ==> acc(nodes[next(tid, |nodes|)].out, 1 / 2))
  ensures (forall tid: Int :: { nodes[next(tid, |nodes|)].out } 0 <= tid && tid < |nodes| ==> acc(nodes[next(tid, |nodes|)].out, 1 / 2))
{
  inhale false
}

method main(diz: Ref, globals: Ref, nodes: Seq[Ref])
  requires diz != null
  requires |nodes| == 3
  requires (forall j: Int :: { nodes[j] } 0 <= j && j < |nodes| ==> acc(nodes[j].out, write))
{
    parThreads(diz, nodes, globals)
    // assert
    assert (forall k: Int :: { nodes[k] } 0 <= k && k < |nodes| ==> acc(nodes[k].out, write))
}

[gauravpartha]

Carbon also can't prove assert acc(nodes[0].out) at the end. Carbon has issues with heap-dependent triggers in general. Changing the trigger nodes[next(tid, |nodes|)].out to next(tid, |nodes|) does not help Carbon either (actually even with nodes[next(tid, |nodes|)].out, Carbon adds the location as a separate trigger). I don't have a good intuition on what would be required in the encoding to fix this. I remember that @alexanderjsummers thought about Carbon triggering issues more deeply. Alex, do you have any intuition on this particular example?

[bobismijnnaam]

For now I've solved it with the following (unproven, abstract) lemma:

  requires (\forall* int i = 0 .. |nodes|; Perm(nodes[next(i, |nodes|)].outMessage, 1\2));
  ensures (\forall* int i = 0 .. |nodes|; Perm(nodes[i].outMessage, 1\2));
  void transmuteOutMessages(seq<Node> nodes);

After calling this twice it seems the permissions are transformed back again. This allows me to continue verification work, and it doesn't seem to cause unsoundness, but I am a bit scary that it might break or cause unsoundness in the future. Alternatively, I've been thinking seeing if I can maybe prove this manually, but it'd be even better if carbon could prove this natively...

[alexanderjsummers]

Hi there,

Sorry to join the thread so late. I had a quite look at the example. The trigger nodes[next(tid, |nodes|)].out would generally only be matched by a correspondingly used term of this shape (or one which, modulo equalities known at the appropriate program point could be rewritten into that shape). So it seems I would not expect the example to go through: for example, looking at what is known in the state after parThreads is called, I don't see any calls to the next function (e.g. it's not mentioned in the failing assert), so it seems that trigger should never be matched and the quantifier not instantiated).

In other words, what's surprising to me based on my understanding so far is that Silicon does verify the example. I suspect this has something to do with how Silicon translates the trigger terms themselves. I'll see what I can find out. @mschwerhoff might have something to say here. Note that commenting-out the body of next causes the example to fail in Silicon too, although that might be for other reasons; I didn't look into that so closely. @gauravpartha is certainly right that there are some issues in the design of heap-dependent triggers, and we certainly see discrepancies between the two verifiers right now with respect to those triggers.

Since in this case, the underlying issue seems to be that you'd like to prove that your last assert follows from the postcondition with a trigger that doesn't get matched, I think this should really fail. However, here is one potential workaround (I think the one you found is also reasonable): you can make clear that each k is the "next of something" by adding a symmetrical prev function, and making the symmetry explicit as follows:

field out: Int

function next(i: Int, size: Int): Int
  requires 0 < size
  requires 0 <= i && i < size
  ensures 0 <= result && result < size
{
  (i <= 0 ? i - 1 + size : i - 1)
}

function prev(i: Int, size:Int): Int 
  requires 0 < size
  requires 0 <= i && i < size
  ensures 0 <= result && result < size
  {
      (i == size - 1 ? 0 : i + 1)
  }

method parThreads(diz: Ref, nodes: Seq[Ref], globals: Ref)
  requires diz != null
  requires 0 < |nodes| ==> |nodes| == 3
  requires (forall i:Int, j:Int :: 0 <= i && i < j && j < |nodes| ==> nodes[next(i, |nodes|)] != nodes[next(j, |nodes|)])
  requires (forall tid: Int :: { nodes[next(tid, |nodes|)] } 0 <= tid && tid < |nodes| ==> acc(nodes[next(tid, |nodes|)].out, 1 / 2))
  ensures (forall tid: Int :: { nodes[next(tid, |nodes|)] } 0 <= tid && tid < |nodes| ==> acc(nodes[next(tid, |nodes|)].out, 1 / 2))

method main(diz: Ref, globals: Ref, nodes: Seq[Ref])
  requires diz != null
  requires |nodes| == 3
  requires (forall j: Int :: { nodes[j] } 0 <= j && j < |nodes| ==> acc(nodes[j].out, write))
{
    parThreads(diz, nodes, globals)
    assert (forall k: Int :: { nodes[k] } 0 <= k && k < |nodes| ==> next(prev(k, |nodes|), |nodes|) == k && acc(nodes[k].out, write))
}

Let me know if that makes sense and/or you have some more questions (I'll try to notice the message this time :))

Cheers, Alex

[bobismijnnaam]

Thank you for looking at my problem! That looks like a very nice workaround, especially since no assumptions are needed. Strangely enough I couldn't carbon copy your workaround to my input program, even though the minimal example I gave you is derived from that. I had to add a small part to get it working (note the implies in the second-to-last assert):

assert (\forall* int j=0..|nodes|; Perm(nodes[next(j, |nodes|)].outMessage,1));
assert (\forall* int j=0..|nodes|; Perm({: nodes[next(prev(j, |nodes|), |nodes|)].outMessage :},1));
assert (\forall* int j=0..|nodes|; next(prev(j, |nodes|), |nodes|)) == j  ==> Perm(nodes[j].outMessage,1));
assert (\forall* int j=0..|nodes|; Perm(nodes[j].outMessage,1));

So if I change the ==> to **, it breaks...

In any case, I am happy for now, and if you are interested in why the ** breaks it I can minimise the example again to see if there is something interesting happening.

EDIT: My colleague @ArmborstL thought of a nice explanation of why ** doesn't work in VerCors, but ==> does:

I think your issue with the ==> vs ** is because VerCors splits the two forall* in the case of **. After that, it's again a trigger issue, I think: the next(prev(i))==i quantifier probably doesn't get triggered in your last assert. Using a ==> keeps the quantifier as one, and triggering works better.

EDIT 2: As far as I am concerned, this issue may be closed, but maybe you want to keep it open to track the difference in behaviour between silicon & carbon.