viperproject/silicon

Quantifier with predicates/predicates with quantifiers interfere with each other

sakehl opened this issue · 4 comments

sakehl commented

Hi, maybe I am understanding something incorrectly, but otherwise this might be a bug?

The following program does not verify. And it uses a predicate, and quantifies over this predicate.

However, in another program, which tries to do the same, but the quantifier is moved inside the predicate, it does verify. (Which I included below)

Using the Stable silicon version from the Viper IDE.

Code which does not verify 
predicate arrR(x: Int, a: Option[Array], n: Int) {
  a != (none1(): Option[Array]) && alen(optGet1(a)) == n && 0 <= x && x < n &&
  acc(aloc(optGet1(a), x).int, write)
}

predicate arr(a: Option[Array], n: Int) {
  a != (none1(): Option[Array]) && alen(optGet1(a)) == n &&
  (forall i: Int ::
    { aloc(optGet1(a), i) }
    0 <= i && i < alen(optGet1(a)) ==> acc(aloc(optGet1(a), i).int, write))
}

method main(tid: Int, n: Int, x0: Option[Array], x1: Option[Array], x2: Option[Array])
  requires 0 < n
  requires acc(arr(x1, n), write/2)
  requires acc(arr(x2, n), write/2)
  requires (forall j: Int ::
      { aloc(optGet1(x1), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x1, n), write/2) in
        aloc(optGet1(x1), j).int) ==
      j)
  requires (forall j: Int ::
      { aloc(optGet1(x2), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x2, n), write/2) in
        aloc(optGet1(x2), j).int) ==
      2 * j)
  requires (forall i: Int ::
      { arrR(i, x0, n) }
      0 <= i && i < n ==> acc(arrR(i, x0, n), write))
  ensures 0 < n
  ensures acc(arr(x1, n), write/2)
  ensures acc(arr(x2, n), write/2)
  ensures (forall j: Int ::
      { aloc(optGet1(x1), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x1, n), write/2) in
        aloc(optGet1(x1), j).int) ==
      j)
  ensures (forall j: Int ::
      { aloc(optGet1(x2), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x2, n), write/2) in
        aloc(optGet1(x2), j).int) ==
      2 * j)
  ensures (forall i: Int ::
      { arrR(i, x0, n) }
      0 <= i && i < n ==> acc(arrR(i, x0, n), write))
  ensures (forall j: Int ::
      { aloc(optGet1(x0), j) }
      0 <= j && j < n ==>
      (unfolding acc(arrR(j, x0, n), write) in aloc(optGet1(x0), j).int) ==
      3 * j)
{
  {
    var i: Int
    var a1: Int
    var a2: Int
    i := 0
    while (i < n)
      invariant 0 < n
      invariant acc(arr(x1, n), write/2)
      invariant acc(arr(x2, n), write/2)
      invariant (forall j: Int ::
          { aloc(optGet1(x1), j) }
          0 <= j && j < n ==>
          (unfolding acc(arr(x1, n), write/2) in
            aloc(optGet1(x1), j).int) ==
          j)
      invariant (forall j: Int ::
          { aloc(optGet1(x2), j) }
          0 <= j && j < n ==>
          (unfolding acc(arr(x2, n), write/2) in
            aloc(optGet1(x2), j).int) ==
          2 * j)
      invariant 0 <= i && i < n + 1
      invariant (forall i1: Int ::
          { arrR(i1, x0, n) }
          0 <= i1 && i1 < n ==> acc(arrR(i1, x0, n), write))
      invariant (forall j: Int ::
          { aloc(optGet1(x0), j) } {arrR(j, x0, n)}
          0 <= j && j < i ==>
          (unfolding acc(arrR(j, x0, n), write) in
            aloc(optGet1(x0), j).int) ==
          3 * j) 
    {
      unfold acc(arr(x1, n), write/2)
      a1 :=  aloc(optGet1(x1), i).int
      fold acc(arr(x1, n), write/2)
      unfold acc(arr(x2, n), write/2)
      a2 := aloc(optGet1(x2), i).int
      fold acc(arr(x2, n), write/2)
      unfold acc(arrR(i, x0, n), write)
      aloc(optGet1(x0), i).int := a1 + a2
      fold acc(arrR(i, x0, n), write)
      i := i + 1
    }
  }
}

domain Array  {
  
  function array_loc(a: Array, i: Int): Ref 
  
  function alen(a: Array): Int 
  
  function loc_inv_1(loc: Ref): Array 
  
  function loc_inv_2(loc: Ref): Int 
  
  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }
  
  axiom {
    (forall a: Array :: { alen(a) } alen(a) >= 0)
  }
}

domain Option[T1]  {
  
  function none1(): Option[T1] 
  
  function some(x: T1): Option[T1] 
  
  function option_get(opt: Option[T1]): T1 
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (none1(): Option[T1]) != (some(x): Option[T1]))
  }
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (option_get((some(x): Option[T1])): T1) == x)
  }
  
  axiom {
    (forall opt: Option[T1] ::
      { (some((option_get(opt): T1)): Option[T1]) }
      (some((option_get(opt): T1)): Option[T1]) == opt)
  }
}

field int: Int

function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  decreases 
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}

function optGet1(opt: Option[Array]): Array
  requires opt != (none1(): Option[Array])
  decreases 
  ensures (some(result): Option[Array]) == opt
{
  (option_get(opt): Array)
}
Code which does verify 
predicate arrR(x: Int, a: Option[Array], n: Int) {
  a != (none1(): Option[Array]) && alen(optGet1(a)) == n && 0 <= x && x < n &&
  acc(aloc(optGet1(a), x).int, write)
}

predicate arr(a: Option[Array], n: Int) {
  a != (none1(): Option[Array]) && alen(optGet1(a)) == n &&
  (forall i: Int ::
    { aloc(optGet1(a), i) }
    0 <= i && i < alen(optGet1(a)) ==> acc(aloc(optGet1(a), i).int, write))
}

method main(tid: Int, n: Int, x0: Option[Array], x1: Option[Array], x2: Option[Array])
  requires 0 < n
  requires acc(arr(x1, n), write/2)
  requires acc(arr(x2, n), write/2)
  requires (forall j: Int ::
      { aloc(optGet1(x1), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x1, n), write/2) in
        aloc(optGet1(x1), j).int) ==
      j)
  requires (forall j: Int ::
      { aloc(optGet1(x2), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x2, n), write/2) in
        aloc(optGet1(x2), j).int) ==
      2 * j)
  requires acc(arr(x0, n), write)
  ensures 0 < n
  ensures acc(arr(x1, n), write/2)
  ensures acc(arr(x2, n), write/2)
  ensures (forall j: Int ::
      { aloc(optGet1(x1), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x1, n), write/2) in
        aloc(optGet1(x1), j).int) ==
      j)
  ensures (forall j: Int ::
      { aloc(optGet1(x2), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x2, n), write/2) in
        aloc(optGet1(x2), j).int) ==
      2 * j)
  ensures acc(arr(x0, n), write)
  ensures (forall j: Int ::
      { aloc(optGet1(x0), j) }
      0 <= j && j < n ==>
      (unfolding acc(arr(x0, n), write) in aloc(optGet1(x0), j).int) ==
      3 * j)
{
  {
    var i: Int
    var a1: Int
    var a2: Int
    i := 0
    while (i < n)
      invariant 0 < n
      invariant acc(arr(x1, n), write/2)
      invariant acc(arr(x2, n), write/2)
      invariant (forall j: Int ::
          { aloc(optGet1(x1), j) }
          0 <= j && j < n ==>
          (unfolding acc(arr(x1, n), write/2) in
            aloc(optGet1(x1), j).int) ==
          j)
      invariant (forall j: Int ::
          { aloc(optGet1(x2), j) }
          0 <= j && j < n ==>
          (unfolding acc(arr(x2, n), write/2) in
            aloc(optGet1(x2), j).int) ==
          2 * j)
      invariant 0 <= i && i < n + 1
      invariant acc(arr(x0, n), write)
      invariant (forall j: Int ::
          { aloc(optGet1(x0), j) }
          0 <= j && j < i ==>
          (unfolding acc(arr(x0, n), write) in
            aloc(optGet1(x0), j).int) ==
          3 * j) 
    {
      unfold acc(arr(x1, n), write/2)
      a1 :=  aloc(optGet1(x1), i).int
      fold acc(arr(x1, n), write/2)
      unfold acc(arr(x2, n), write/2)
      a2 := aloc(optGet1(x2), i).int
      fold acc(arr(x2, n), write/2)
      unfold acc(arr(x0, n), write)
      aloc(optGet1(x0), i).int := a1 + a2
      fold acc(arr(x0, n), write)
      i := i + 1
    }
  }
}

domain Array  {
  
  function array_loc(a: Array, i: Int): Ref 
  
  function alen(a: Array): Int 
  
  function loc_inv_1(loc: Ref): Array 
  
  function loc_inv_2(loc: Ref): Int 
  
  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }
  
  axiom {
    (forall a: Array :: { alen(a) } alen(a) >= 0)
  }
}

domain Option[T1]  {
  
  function none1(): Option[T1] 
  
  function some(x: T1): Option[T1] 
  
  function option_get(opt: Option[T1]): T1 
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (none1(): Option[T1]) != (some(x): Option[T1]))
  }
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (option_get((some(x): Option[T1])): T1) == x)
  }
  
  axiom {
    (forall opt: Option[T1] ::
      { (some((option_get(opt): T1)): Option[T1]) }
      (some((option_get(opt): T1)): Option[T1]) == opt)
  }
}

field int: Int

function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  decreases 
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}

function optGet1(opt: Option[Array]): Array
  requires opt != (none1(): Option[Array])
  decreases 
  ensures (some(result): Option[Array]) == opt
{
  (option_get(opt): Array)
}
sakehl commented

So I still am running into this problem, but I've tried to minimize the example. The code below does not verify.

However if you remove the unrelated quantifier

requires (forall j: Int :: { aloc(x1, j) }
    0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)

from the requirements, it does verify. So the quantifiers seem to interfere with each other.

This code does not work

method test(x0: Array, x1:Array)
  requires (forall j: Int :: {arrR(j, x0, 10)} 0 <= j && j < 10 ==> arrR(j, x0, 10))
  requires arr(x1, 10)
  requires (forall j: Int :: { aloc(x1, j) }
    0 <= j && j < 10 ==> (unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) == j)
  requires (forall j: Int :: { aloc(x0, j) }
    0 <= j && j < 10 ==> (unfolding arrR(j, x0, 10) in aloc(x0, j).int == 3 * j))
{
  assert (unfolding arrR(0, x0, 10) in
            aloc(x0, 0).int == 3 * 0)
}

predicate arrR(x: Int, a: Array, n: Int) {
  alen(a) == n && 0 <= x && x < n && acc(aloc(a, x).int, write)
}

predicate arr(a: Array, n: Int) {
  alen(a) == n && (forall i: Int :: { aloc(a, i) } 0 <= i && i < alen(a) ==> acc(aloc(a, i).int, write))
}

field int: Int
domain Array  {
  
  function array_loc(a: Array, i: Int): Ref 
  function alen(a: Array): Int 
  function loc_inv_1(loc: Ref): Array 
  function loc_inv_2(loc: Ref): Int 
  
  axiom {
    (forall a: Array, i: Int ::
      { array_loc(a, i) }
      loc_inv_1(array_loc(a, i)) == a && loc_inv_2(array_loc(a, i)) == i)
  }
  
  axiom {
    (forall a: Array :: { alen(a) } alen(a) >= 0)
  }
}

function aloc(a: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a)
  decreases 
  ensures loc_inv_1(result) == a
  ensures loc_inv_2(result) == i
{
  array_loc(a, i)
}
marcoeilers commented

Part of the reason this happens is that arr contains a quantified permission for field int, and as a result, unfolding arr in test forces the use of Silicon's quantified permission algorithm for all usages of the int field inside test (when without that unfolding, there is no quantified permission for int anywhere in test, and it can use the simpler algorithm for non-quantified resources).

Then, for some reason, the QP algorithm seems to be incomplete in this setting, which it obviously shouldn't be. I'll try to figure out why.

Edit: A simple workaround would be to move the unfolding of arr to a function (i.e., write a getter function that returns unfolding acc(arr(x1, 10), write/2) in aloc(x1, j).int) and call that function from test, which would allow Silicon to keep using the simpler non-QP algorithm in test and avoid the incompleteness.
Also, thanks a lot for the minimized example!

marcoeilers commented

PR #840 fixes the underlying issue.

  • 🎉1
sakehl commented

Awesome, thanks a lot!