Problems with scaling predicates

[JLedelay]

I encountered some issues scaling predicates:

class C {
  final D[] arr;

  /*@
    inline resource pred() =
      arr != null ** Perm(arr[*], write) **
      (\forall int i = 0 .. arr.length, int j = 0 .. i; {:arr[i]:} != {:arr[j]:})
    ;
  @*/

  //@ context [1\2]pred();
  void m() {}
}

class D {
  boolean x;

  //@ inline resource common() = Perm(x, write);
}

[INFO] Starting verification
======================================
 At Test.java:12:3:
--------------------------------------
   10
   11    //@ context [1\2]pred();
        [-----------
   12    void m() {}
         -----------]
   13  }
   14
--------------------------------------
[1/2] Postcondition may not hold, since ...
--------------------------------------

--------------------------------------
[2/2] ... this expression may be false (https://utwente.nl/vercors#postFailed:false)
======================================

Removing the scaling in the specification for the method m() removes the error, as does removing the \forall loop with the injectivity check.

Changing the predicate pred() to the following introduces a different error:

/*@
  inline resource pred() =
    arr != null ** Perm(arr[*], write) **
    (\forall int i = 0 .. arr.length, int j = 0 .. i; {:arr[i]:} != {:arr[j]:}) ** 
    (\forall* int i = 0 .. arr.length; arr[i] != null ** arr[i].common()); 
@*/

[INFO] Starting verification
A verification condition failed inside a file loaded as a library file, which is never supposed to happen. The internal error is:
======================================
 At Test.java:12:15:
--------------------------------------
   10    @*/
   11
                    [-----
   12    //@ context [1\2]pred();
                     -----]
   13    void m() {}
   14  }
--------------------------------------
[1/2] This quantifier causes the resources in its body to be quantified, ...
--------------------------------------
 Inlined from:
--------------------------------------
 At Test.java:12:20:
--------------------------------------
   10    @*/
   11
                         [------
   12    //@ context [1\2]pred();
                          ------]
   13    void m() {}
   14  }
--------------------------------------
 ...Then inlined from:
--------------------------------------
 At Test.java:8:60:
--------------------------------------
    6        arr != null ** Perm(arr[*], write) **
    7        (\forall int i = 0 .. arr.length, int j = 0 .. i; {:arr[i]:} != {:arr[j]:}) **
                                                                 [---------------
    8        (\forall* int i = 0 .. arr.length; arr[i] != null ** arr[i].common())
                                                                  ---------------]
    9      ;
   10    @*/
--------------------------------------
 In definition:
--------------------------------------
 At Test.java:19:34:
--------------------------------------
   17    boolean x;
   18
                                       [--------------
   19    //@ inline resource common() = Perm(x, write);
                                        --------------]
   20  }
   21
--------------------------------------
[2/2] ... but this resource may not be unique with regards to the quantified variables.
======================================

I'd expect this to work because of the injectivity check arr[i] != arr[j]. Again, removing the scaling on the predicate removes this error and gives a successful verification.

[bobismijnnaam]

Your first error is because your quantifier with multiple binders gets split up into a nested quantifier. I've minimized that case down to this:

class C {
  /*@
    inline resource pred(int[] arr) =
      (\forall int i, int j; true; arr[i] != arr[j])
    ;
  @*/

  void m() {
      //@ assert [1\2]pred(null);
  }
}

@niomaster Do you see how maybe the simplifier messes this up? As soon as you remove the inline or the scaling the problem indeed goes away.

A theory for why the second case is an error is that this splitting up of quantifiers causes the injectivity knowledge to be unusable, hence the injectivity check fails.

[pieter-bos]

Yes, this is the report for the bad simplification (when passing -v --dev-simplify-debug-match --dev-simplify-debug-match-long --dev-simplify-debug-filter-input-kind Forall):

[DEBUG] Expression:       (\forall int j; true; (i\memberof{0 .. this.arr.length}) && (j\memberof{0 .. i}) ==> {: this.arr[i] :} != {: this.arr[j] :})
[DEBUG] Matches:          (\forall T binding; true; cond1 && (cond2!binding) ==> (body!binding))
[DEBUG] With bindings:
[DEBUG]   boolean body = ({: this.arr[i] :} != {: this.arr[j] :}) parametric over int j
[DEBUG]   boolean cond1 = (i\memberof{0 .. this.arr.length})
[DEBUG]   boolean cond2 = ((j\memberof{0 .. i})) parametric over int j
[DEBUG] With type bindings:
[DEBUG]   any T = int
[DEBUG] Applied to:       cond1 ==> (\forall T binding; true; (cond2!binding) ==> (body!binding))
[DEBUG] Result:           (i\memberof{0 .. this.arr.length}) ==> (\forall int j; true; (j\memberof{0 .. i}) ==> {: this.arr[i] :} != {: this.arr[j] :})

Note that the expression is in fact not yet split up into multiple quantifiers before this point, but the simplifier treats foralls with multiple bindings as equivalent to multiple foralls with one binding, to keep the simplification rules manageable. That did improve the situation (because we no longer need to split up every quantifier), but clearly in this case is not enough.

[pieter-bos]

We could consider first translating all quantifiers with multiple bindings to their tupled form:

(\forall T1 a, T2 b; (body!a,b))
==
(\forall tuple<T1, T2> t; (body!t.0,t.1))

That way we no longer have to hack around quantifiers having multiple bindings, and we can just write simplifications as though quantifiers have only one binding. As a consequence we can never split out quantifiers over their bindings, but that is probably just what we want.

[bobismijnnaam]

As a consequence we can never split out quantifiers over their bindings, but that is probably just what we want.

Do you mean, define rewrite rules about quantifiers, that are parametric over the number of arguments the quantifier has?

Do we even have rules like that? We could consider moving those to a specialized pass anyway, as the exact way of whether or not to split a quantifier or not seems delicate.

[pieter-bos]

No, I mean to alter the nesting level of quantifiers.