Obviously true precondition "doesn't hold" when using predicate

[ArmborstL]

The file below is a reduced version to highlight the problem:

function nonNull(): Ref
  ensures result != null

function check(min_value1: Ref): Bool
  requires min_value1 != null


predicate pred(nl: Ref) {
 check(nonNull())
}

function funThatUnfolds( nl: Ref): Int
  requires acc(pred( nl), write)
{
  unfolding acc(pred(nl), write) in 1
}

function funThatUses(nl: Ref): Seq[Ref]
  requires acc(pred(nl), write)
  ensures |result| == funThatUnfolds(nl)

The function check requires its argument to be non-null, and nonNull never returns null. So everything should be fine. However, Silicon reports for the call check(nonNull()) inside the predicate that the precondition of check might not hold: "Precondition of function check might not hold. Assertion nonNull() != null might not hold. ([email protected])"

The error disappears if the predicate is not unfolded in funThatUnfolds. It also disappears if funThatUnfolds is not used in funThatUses.

The issue occurs in the Viper VSCode plugin (version reported as Viper v4.3.1, seems to be most recent), as well as Silicon as used by VerCors (which uses commit 529d2a49108b954d2b0749356faf985d622f54f0).

[marcoeilers]

The issue is that Silicon verifies funThatUnfolds before nonNull, and thus the postcondition of nonNull is not available yet. Silicon computes which functions rely on which other functions to determine in what order to verify the functions, but by default does not take dependencies through a predicate unfolding (like in this case) into account. This behavior can be changed by using the flag --alternativeFunctionVerificationOrder (which unfortunately can lead to incompleteness in other cases, which is why it's not the default), and then the file verifies.