Thoughts on the Verifier

[DavePearce]

Despite a significant amount of effort, the verifier is still not working that well and I think a review of where I'm at might help. Here are the main points:

1. Collection Representation. Previously, I represented sets, maps and lists in a non-uniform manner. However, I have now merged them together into the same underlying set representation. This has many benefits, but it also results in more quantified formulas which need to be instantiated (see below).
2. Quantifier Instantiation. A lot of my recent efforts have focused on the issue of how to handle quantifier instantiation. My previous approach was based purely on a bounded quantifier approach. This works well, but leads to a discrepancy of representation where we can model the same facts with and without bounded quantifiers (and if not using the latter, then no instantiation occurs). Therefore, I moved towards using Prenex Normal Form and introducing a quantifier instantiation rule. Unfortunately, this rule is not sufficient (see e.g. #260).
3. Rewrite Rules. My rewrite rules are getting complex and it's often difficult to tell whether a given rule is right or not (in some sense). What we need are some overarching guidelines to help us see what kind of approach to apply in any given situation. For example, I have a developing theory of partial and total orders which is potentially fruitful.
4. Performance. Unfortunately, the quantifier instantiation rule above has really hit the performance of the system very hard. Typically things degrade fast when there are multiple quantifiers and disjunctions. An incremental solver would significant improve the situation.
5. Minor Niggles. There are quite a few minor niggles with the verifier at the moment. For example, its type system does handle a bunch of simple cases involving sets and any. I have a reasonable idea of how to fix this, but it will take some time.

Overall, the big question is: how to proceed? I could try to fix the instantiation issue, or rework the rewrite system, or just fix niggles. My feeling is that I need a handle on the instantiation issue, since this is the fundamentally hard one.

[DavePearce]

IDEA 1. The issue of quantifier instantiation raises the question of representation. In particular, I currently have that xs ⊆ ys is equivalent to:

forall ({int} xs, {int} ys):
    forall (int x in xs):
        x in ys

And, this makes me question whether having two representations is sensible. One possible solution is to change the ⊆ to only represent constraints of the form {...} ⊆ ys. Thus, it's really an enhanced "element of" operation, which can amalgamate elements together to connect with |ys|.

The one problem with this idea for the ⊆ is that I loose the ability to infer x ⊆ y && y ⊆ x ==> x == y.

[DavePearce]

IDEA 2. The other competing idea I have is to stick with bounded quantification and, instead, remove unbounded quantification. This would be closer to my original approach, and would eliminate the issue of instantiation altogether. Roughly speaking, the idea would be to replace quantifiers with single source set comprehensions. For example:

assert:
  forall(int y):
   if:
     y in { int x where x > 0 }
   then:
     y >= 0

Here we can always instantiate y as expected to get effectively y > 0 ==> y >= 0.

I'm not really sure what the downsides of this approach are. One interesting effect however is that, unlike before, quantifiers are no longer boolean expressions; rather, they are set expressions!

NOTE: an interesting question here is whether to support in or ⊆

NOTE: one thing nice about this approach is that it provides a clear syntactic distinction between (unbounded) quantification and (bounded) comprehension. This will at least help me picture in my mind what's going on, and will make clear where the "human" part of a proof comes in --- namely, instantiating quantifiers.

[DavePearce]

One issue with iDEA 2, is how to use these comprehensions in the verification condition generator. For example, consider this Whiley code:

define nat as int where $ >= 0
{nat} f({int} xs) requires all { x in xs | x > 0 }:
   return xs

This generates the following Wyil code:

void f({int} xs):
requires:
   forall x in xs:
       assert x > 0
ensures:
   forall x in $:
       assert x >= 0
body:
   return xs

And, the question now is, what verification condition should be generated? Previously, it would look something like this:

assert "":
   forall({int} xs):
     if:
       for (int x in xs):
         x > 0
     then:
       for (int x in xs):
         x >= 0

But, I don't know how to do this with comprehensions.

[DavePearce]

Ok, here's the verification condition (although how you get it I don't know):

assert "":
   forall({int} xs):
     if:
       xs ⊆ { int y | y > 0 }
     then:
       xs ⊆ { int y | y >= 0 }

Certainly, this raising some interesting questions for me about the uniform representation of formulas.

[DavePearce]

The current major causes of failure are:

1. Weak support for connecting subset relations and size of sets. e.g. |xs| > 0 ==> xs != 0.
2. Problem with numerical equality. Thus, x != y for numerical types should become x < y || x > y.
3. Problem with existentials and quantifier instantiation.

Possible improvements include:

1. representing all boolean predicates with a "positive" and "negative" form. This way we can instantiate quantifiers based on predicates more easily. This will particularly help inequalities -- see #247.
2. Represent disjuncts in a uniform fashion. For example don't allow Or{X,Y}, but require Or{And{X},And{Y}}. This might potentially help instantiation.