Information lost in implication after exists clause

[JLedelay]

The following input:

public class C {
  final D[] arr;

  /*@
    yields int y;
    context arr != null && 0 <= x && x < arr.length;
    context Value(arr[x]) ** arr[x] != null;
    ensures (\exists boolean b; b) ==>
      (0 <= y && y < arr[x].f && arr[x].m(y));
  @*/
  private boolean test(int x);
}

public class D {
  final int f;

  //@ requires 0 <= i && i < f;
  /*@ pure @*/ boolean m(int i) {
    return true;
  }
}

Leads to the following output:

======================================
 At Test.java:9:34:
--------------------------------------
    7      context Value(arr[x]) ** arr[x] != null;
    8      ensures (\exists boolean b; b) ==>
                                       [-----------
    9        (0 <= y && y < arr[x].f && arr[x].m(y));
                                        -----------]
   10    @*/
   11    private boolean test(int x);
--------------------------------------
[1/2] Precondition may not hold, since ...
--------------------------------------
 At Test.java:17:16:
--------------------------------------
   15    final int f;
   16
                     [---------------
   17    //@ requires 0 <= i && i < f;
                      ---------------]
   18    /*@ pure @*/ boolean m(int i) {
   19      return true;
--------------------------------------
[2/2] ... this expression may be false (https://utwente.nl/vercors#preFailed:false)
======================================

The following also result in this error:

• (\exists boolean b; b) (evaluates to true) is replaced with (\exists int j = 0 .. 10; true) (which evaluates to true) or (\forall boolean b; b) (which evaluates to false)
• Separating 0 <= y && y < arr[x].f from arr[x].m(y) by putting it in a separate implication, as such:

  ensures (\exists boolean b; b) ==> 0 <= y && y < arr[x].f; 
  ensures (\exists boolean b; b) ==> arr[x].m(y);

  Doing any of the following results in successful verification:

• Removing the exists clause
• Replacing (\exists boolean b; b) with (\exists boolean b; true) or (\forall boolean b; true)
• Splitting 0 <= y && y < arr[x].f out of the implication, as such:

  ensures 0 <= y && y < arr[x].f; // alternatively: true ==> 0 <= y && y < arr[x].f;
  ensures (\exists boolean b; b) ==> arr[x].m(y);

  It looks like the information that 0 <= y && y < arr[x].f is somehow lost.

[pieter-bos]

Reduced:

public class C {
    /*@
    requires (\exists boolean b; b) ==> guardedCondition;
    ensures (\exists boolean b; b) ==> guardedCondition;
    @*/
    void test(boolean guardedCondition){}
}

[JLedelay]

Ah, I was under the impression that the array indexing also had an effect, but clearly didn't thoroughly test this. Thanks!

[pieter-bos]

In the first instance, the problem is being caused by the implication being split over its consequent: a ==> b && c is split as (a ==> b) && (a ==> c).

The root cause is in the underlying smt solver (z3). The solver is very good at boolean satisfiability, so a ==> b && c is normally absolutely equivalent to (a ==> b) && (a == c). I suspect however that terms that are not quantifier-free are not treated normally in the sat solver - even when the terms are syntactically identical.

We might want to do an encoding where every quantifier gains an otherwise inaccessible trigger, so that situations like this cause matching quantifiers to trigger each other, e.g.:

/*@
adt triggers {
    pure boolean trigger1(boolean b);
}
@*/

public class C {
    /*@
    requires (\exists boolean b; {:triggers.trigger1(b):} && b) ==> guardedCondition;
    ensures (\exists boolean b; {:triggers.trigger1(b):} && b) ==> guardedCondition;
    @*/
    void test(boolean guardedCondition){}
}

In the meantime, you can also prevent unwanted simplifications by writing a trigger around expressions that you do not want to be split, e.g. (\exists boolean b; b) ==> {: 0 <= y && y < arr[x].f && arr[x].m(y) :}.