"wildcard could be negative"

[ArmborstL]

In the following code, I get the error that "Assert might fail. Fraction wildcard might be negative.".
Changing the program (e.g. removing the trigger on the assert, and using the function call right before it, which is currently commented out) causes viper to verify it successfully.
While playing around with triggers can circumvent the problem, I do not see how wildcard permissions could ever be negative. So I think there might be a deeper issue than just triggers...

Since this is an excerpt from a bigger example, where I stumbled upon negative wildcards quite a few times, I would be interested to hear if this is some underlying bug, or if it can actually be possible that wildcards are negative in certain cases.

domain VCTArray[CT] {
  
  function loc(a: VCTArray[CT], i: Int): CT
  
}

field bool_prop: Bool

field item: Ref

function alwaysTrue(v: Ref): Bool
  ensures result == true

method some_method(trees: VCTArray[Ref], g: Int) 
  requires 0 < g
  requires (forall i: Int :: {loc(trees, i).item} 0 <= i && i < g ==> acc(loc(trees, i).item, wildcard))
  requires (forall i: Int :: {loc(trees, i).item.bool_prop} 0 <= i && i < g ==> acc(loc(trees, i).item.bool_prop, wildcard))
{
  // assert alwaysTrue(loc(trees, 0).item)
  assert forall j: Int :: {loc(trees, j).item.bool_prop} 0 <= j && j < g ==> acc(loc(trees, j).item.bool_prop, wildcard)
}

[mschwerhoff]

Thanks for reporting this. The example is somewhat complex — loc-function, heap-dep. triggers, nested field accesses — are all these ingredients necessary for the problem to be reproducible?

[ArmborstL]

I mostly added the triggers because in the past, the solution often was "please define triggers". They are not actually needed for reproducing the issue.
In contrast to what I initially believed, the loc function is not needed. So a slightly simplified example is this:

field bool_prop: Bool

field item: Ref

function alwaysTrue(v: Ref): Bool
  ensures result == true

method some_method(trees: Seq[Ref], g: Int) 
  requires 0 < g && |trees|==g
  requires (forall i: Int :: 0 <= i && i < g ==> acc(trees[i].item, wildcard))
  requires (forall i: Int :: 0 <= i && i < g ==> acc(trees[i].item.bool_prop, wildcard))
{
  // assert alwaysTrue(trees[0])
  assert forall j: Int :: 0 <= j && j < g ==> acc(trees[j].item.bool_prop, wildcard)
}

The call to alwaysTrue, which makes the example verify, can be anything that accesses a concrete value of the sequence (e.g. also assert acc(trees[0].item, wildcard)).
However, the nested field access and the quantifiers are needed.

[mschwerhoff]

Providing triggers explicitly is always a good idea. What I meant was that a heap-dependent trigger is (for technical reasons) for complex than a pure trigger such as trees[i]. Either way, thanks for simplifying the example.

[mschwerhoff]

The difference between test03 and test04 in the program below suggests that the availability of the trigger is the problem. My theory so far: if the trigger term is part of the receiver expression (test03), then it is not yet available when checking that wildcard is non-negative (which it would have to be if no permission to the field were available at this point).

field bool_prop: Bool
field item: Ref

domain identity_function[T] {
  function id(v: T): T
  axiom { forall v: T :: {id(v)} id(v) == v }
}

method test03(trees: Set[Ref])
  requires (forall r: Ref :: {id(r)} r in trees ==> acc(id(r).item, 1/2))
  requires (forall r: Ref :: {id(r)} r in trees ==> acc(id(r).item.bool_prop, 1/2))
{
  assert forall s: Ref :: {id(s)} s in trees ==> acc(id(s).item.bool_prop, wildcard) // fails
}

method test04(trees: Set[Ref])
  requires (forall r: Ref :: {r in trees} r in trees ==> acc(id(r).item, 1/2))
  requires (forall r: Ref :: {r in trees} r in trees ==> acc(id(r).item.bool_prop, 1/2))
{
  assert forall s: Ref :: {s in trees} s in trees ==> acc(id(s).item.bool_prop, wildcard) // holds
}

Maybe this allows you to implement a work-around for the time being, until the problem has been resolved.

[mschwerhoff]

Resolved with commit 433d8ef