Expected error or incompleteness with quantified permissions and wildcards?

Question

Consider the following Viper program:

field f: Int

method g(r: Ref, N: Int)
  requires forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)
{
  // Got error: insufficient permission for r.f
  assert 0 < N ==> acc(r.f, wildcard)
}

method h(r: Ref, N: Int)
requires 0 < N ==> acc(r.f, wildcard);
{
  assert 0 < N ==> acc(r.f, wildcard)
  assert 0 < N ==> acc(r.f, wildcard) && acc(r.f, wildcard)
  // Got error: receiver of r.f might not be injective
  assert forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)
}

Intuitively, the failing asserts should hold. Is there a subtle aspect of wildcard permissions that causes the asserts to fail, or is this a completeness issue?

^{(Originally filed as an issue for one of Viper's backends, but copied here since the explanation might help others to avoid similar pitfalls)}

Answer 1

The failures have different root causes, but both are expected.

Error "receiver might not be injective"

For technical reasons (see this paper for details), a quantified permission assertion of the shape

forall x :: c(x) ==> acc(e(x).f)

must be injective in e(x). I.e. for two different instantiations of x, the expression e(x) evaluates to two different receivers. That is not the case for your assertion

forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)

and hence the error message.

If you're wondering why you don't get the same error for method g's precondition: since the precondition is inhaled, Viper assumes (this might change in the future) that it is well-defined, i.e. that the receiver is injective. If you call g, then you'll get the same error:

method caller(r: Ref, N: Int) {
  g(r, N) // receiver r.f might not be injective
}

So g's current precondition is basically false (since r is not injective in x). If you're wondering why Viper cannot (yet) prove false right after the precondition, please continue reading.

Error "insufficient permission"

Ignoring the unsound assumption about receiver injectivity, then this error is due to triggering: the quantifier

forall tid: Int :: 0 <= tid && tid < N ==> acc(r.f, wildcard)

admits no triggers that Viper could pick for you, since valid triggers (i) must not include interpreted functions (from the SMT solvers point of view), but (ii) they must include all quantified variables. Here, that rules out subexpressions such as 0 <= tid (interpreted function), but also r.f (doesn't mention quantified variable tid). It is basically undefined what SMT solvers do with quantifiers that don't have triggers; here, it isn't instantiated at all.

The only real option you have in this situation (other than faith) is to add an artificial trigger. Here are two examples:

/* ------------- Example 1 ------------- */

domain dummy {
  function T(n: Int): Bool
  axiom T_always_true { forall n: Int :: T(n) }
}

method g1(r: Ref, N: Int)
  requires (forall tid: Int :: {T(tid)} 0 <= tid && tid < N ==> acc(r.f, wildcard))
{
    assert T(0) // Must mention T(_) somewhere to trigger quantifier
    assert 0 < N /* && T(0) */ ==> acc(r.f, wildcard)
}

/* ------------- Example 2 ------------- */

function id(r: Ref, n: Int): Ref { r }

method g2(r: Ref, N: Int)
  requires (forall tid: Int :: {id(r, tid)} 0 <= tid && tid < N ==> acc(id(r, tid).f, wildcard))
{
    assert 0 < N ==> acc(id(r, 0).f, wildcard)
}

By the way, it is strongly advised to always add triggers explicitly. For one, because it forces one to think about triggers and triggering strategies (how do different axioms interact and when should which be instantiated). The other reason is that Viper does a best-effort approach to choose quantifiers, but for complex, interacting quantifiers, you should not rely on Vipers heuristics.

Let me know if you have further questions regarding triggers. The Viper tutorial also has a section on quantifiers, and references a great paper on triggers.

Error "receiver might not be injective" (continued)

With the triggering issue resolved, we can now get Viper to prove false in the body of g:

method g(r: Ref, N: Int)
  requires (forall tid: Int :: 0 <= tid && tid < N ==> acc(id(r, tid).f, wildcard))
{
  assume 2 < N
  assert id(r, 0) == id(r, 1)
  assert false // holds, because the malformed precondition is inhaled
}