"Fraction might be negative" when unfolding predicate

[bobismijnnaam]

The following input:

class C {
  int f;

  inline resource inner() = Perm(f, 1);

  resource outer(frac x) = x > 0 ** [x]inner();

  requires x > 0 ** outer(x);
  requires 0 < x && x > 0;
  pure boolean readPair(frac x, int j) =
    \Unfolding outer(x) \in true;
}

Yields:

[ERROR] Viper returned an error reason that VerCors does not recognize: Fraction scale(frac_val(x)) * (1 * write) might be negative.

Removing the int j paramter makes the error go away, or removing one of the last two requires clauses makes it go away...?

[bobismijnnaam]

vscode and the local silicon script only give check-sat related errors.

[pieter-bos]

I was under the impression that permission being negative was not a well-formedness property, but part of the truth value of the contract it is stated in, e.g.:

class C {
  int f;

  given rational r;
  requires Perm(f, r);
  void test()
  {
  }
}

used to verify. This is apparently a change I missed. I guess we nearly never run into this, since we always use frac anyway, which is axiomatically positive (zfrac, non-negative respectively).

NegativePermissionValue should thus not be a ContractFailure, but a VerificationFailure. I have to investigate the implications of this for a bit, but I suspect it won't be a big problem (e.g. scales are already a well-formedness property)

[pieter-bos]

To get to your specific case, funnily enough it appears that it does not verify in VerCors, but does so when passing the output directly to silicon. It appears the order in which functions are verified matters in this case, and it so happens that from vercors readPair is verified before scale, and vice-versa in silicon. We could set --alternativeFunctionVerificationOrder, which would deterministically order readPair/scale, but the documentation says that this may have adverse effects in other cases.