Proving forall with only 1 wildcard

[bobismijnnaam]

In the following snippet, silicon can prove the second assert, but not the first:

field f: Int
method m(o: Ref)
  requires acc(o.f, wildcard)
{
  assert (forall r: Ref :: acc(r.f, r == o ? wildcard : (0/1)))
}

method n(o: Ref)
  requires acc(o.f, 1/2)
{
  assert (forall r: Ref :: acc(r.f, r == o ? 1/2 : (0/1)))
}

I would expect them both to pass. Is this a limitation or a bug?

EDIT: I guess there are two caveats I should have considered earlier:

1. Complex wildcard expressions are not fully supported.
2. Trigger issue. I'd say the quantifier could use r.f as trigger. Adding it doesn't change the situation.

If either of these bullets is the case that would be acceptable, and I'd be interested on any thoughts about how to work around them.

[mschwerhoff]

Your first caveat basically gives the answer: since defining the semantics of wildcard in (arbitrary) compound expressions is tricky, and probably wouldn't increase Viper's expressiveness significantly, such expressions are currently not supported. Silicon translates them ... somehow, Carbon simply crashes.

There's a Silver issue for properly rejecting such expressions, which you might remember :-)

[bobismijnnaam]

Thanks for looking at my repeat issue :) To give some more context: we were considering how to deal with quantifiers such as forall tid: Int :: 0 <= tid && tid < N ==> Perm(x.f, read), which VerCors often generates such expressions for parallel blocks. (In short, each thread requires wildcard permission in the precondition, these are all combined into one universal quantifier, resulting in the above expression).

One option is to rewrite such a forall to 0 < N ==> Perm(x.f, read), which we expect to be safe because of the duplicable nature of read permissions. The downside of that is that we're not sure if it's entirely theoretically sound, since it circumvents the injectivity check (we apply this rewrite before handing the program over to viper, and only to very restricted forms of read permissions).

Another option is to employ a more general strategy of transforming a non-injective forall into an injective forall, by making the permission amount argument of acc more complex (as suggested by @niomaster). This is more or less what I try to do in the example in the initial post. Since it's not fully supported, though, we should probably stick with collapsing foralls into read permissions.

Besides the above comments, as far as I'm concerned this issue can be closed.

[mschwerhoff]

I'm not entirely sure I understand the last comment: Is Perm(x.f, read) VerCors syntax, and equivalent to acc(x.f, wildcard)? And why is the RHS of the first quantifier's implication independent of the quantified variable?).

I'll close this issue, but feel free to continue the discussion via e-mail.