Use of wildcard in function precondition causes incompleteness (but not in an equivalent method)

[bobismijnnaam]

As far as I can tell, the following function & method are identical. But, for the master branch of silicon, only the method verifies. The function does not. Specifically, the last ensures clause of the function cannot be proven. Strangely enough the current version of viper used in vscode verifies both the function and method (as well as very old version of viper currently used by VerCors). My vscode plugin version is 2.2.2, though I suspect the version of viper it is using is different, but I'm not sure how to dig that up.

EDIT: The "v" field in my default vscode settings seems to be set to: "674a514867b1"

//  a field
field item: Int

function seqToSeqHelper(xs: Seq[Ref], i: Int): Seq[Int]
  requires 0 <= i && i <= |xs|
  requires (forall j: Int :: 0 <= j && j < |xs| ==> acc(xs[j].item, wildcard))

  ensures |result| == |xs| - i
  ensures (forall j: Int :: i <= j && j < |xs| ==> result[j - i] == xs[j].item)
{
  (i < |xs| ? Seq(xs[i].item) ++ seqToSeqHelper(xs, i + 1) : Seq[Int]())
}

method method_seqToSeqHelper(xs: Seq[Ref], i: Int) returns (res: Seq[Int])
  requires 0 <= i && i <= |xs|
  requires (forall j: Int :: 0 <= j && j < |xs| ==> acc(xs[j].item, wildcard))
  ensures 0 <= i && i <= |xs|
  ensures (forall j: Int :: 0 <= j && j < |xs| ==> acc(xs[j].item, wildcard))

  ensures |res| == |xs| - i
  ensures (forall j: Int :: i <= j && j < |xs| ==> res[j - i] == xs[j].item)
{
  if (i < |xs|) {
    var tail: Seq[Int]
    // tail := seqToSeqHelper(xs, i + 1) // with this instead of the line below, both methods fail
    tail := method_seqToSeqHelper(xs, i + 1)
    res := Seq(xs[i].item) ++ tail
  } else {
    res := Seq()
  }
}

[mschwerhoff]

Thanks for reporting the problem. I can reproduce it, whereas Carbon verifies the code just fine.

The problem appears to be wildcard-related: replacing acc(xs[j].item, wildcard) in the precondition of function seqToSeqHelper with acc(xs[j].item, 1/1000) (or any other constant value) makes the code verify with Silicon. I'll investigate.

[bobismijnnaam]

Ran into the problem again today, seems like a slight variation on the example above so thought I'd post it as well. Here inlining the function definition manually fails. In this example exchanging the wildcards for concrete permissions (or rationals passed in as an argument P) works as well.

domain VCTArray[CT] {
  function loc(a: VCTArray[CT], i: Int): CT
  
  function alen(a: VCTArray[CT]): Int
  
  axiom len_nonneg {
    (forall a: VCTArray[CT] :: { alen(a) } alen(a) >= 0)
  }
}

//  a field 
field item: Int

function sumContrib(A: VCTArray[Ref], i: Int, P: Rational): Int
  requires 0/1 < P && P < 1/1;
  requires 0 <= i && i <= alen(A)
  requires (forall j: Int :: 0 <= j && j < alen(A) ==> acc(loc(A, j).item, wildcard))
{
  (i == alen(A) ? 0 : loc(A, i).item + sumContrib(A, i + 1, P))
}

method lemmaSumInit(xs: VCTArray[Ref], i: Int, P: Rational)
  requires 0/1 < P && P < 1/1;
  requires (forall i_fresh_rw_0: Int :: 0 <= i_fresh_rw_0 && i_fresh_rw_0 < alen(xs) ==> acc(loc(xs, i_fresh_rw_0).item, wildcard))
  requires (forall j: Int :: 0 <= j && j < alen(xs) ==> loc(xs, j).item == 0)
  requires 0 <= i && i <= alen(xs)
{
    assert sumContrib(xs, i, P) == (i == alen(xs) ? 0 : loc(xs, i).item + sumContrib(xs, i + 1, P))
}

[mschwerhoff]

Resolved with commit e8354ad