Multi-property solving

[agacek]

Sally seems to process process queries sequentially. For k-induction, it's often beneficial to attack problems simultaneously so that they can be used to strengthen each other. We can simulate this by just conjoining all of our properties, but if any one of them is false then the whole property becomes false.

Something like the "Multi-property incremental verification" from "Incremental verification with mode variable invariants in state machines" by Kahsai, et al. would be very useful.

[dddejan]

This can be done with not too much work, depending on the engine used.

There is a question of how to interact with the user in this case, with the user potentially being another program, e.g. how to report that a specific property is valid or a counter-example is found.

Do you have any problems you can share for the multi-property checking?

[agacek]

Here's an example of a multi-property file where lemmas are needed to prove a property:

https://gist.github.com/agacek/ad0b3513b0e78b47995b

Here lemmaA is hard to prove on its own, but easy if you conjoin it with lemmaB (or lemmaC even). Moreover, the ok1 property is much easier if conjoined with lemmaA, lemmaB, and lemmaC.

Playing with this file also exposed another strange result in sally. Consider these two queries for the transition system given in the file.

(query T (and (or |lemmaA| |%init|)
          (or |lemmaB| |%init|)))
(query T (or |lemmaA| |%init|))

Using k-induction, the first query is proved instantly. Sally then gets stuck on the second property. But the second property is an immediate consequence of the first. Sally should be using previously proven results as invariants for proving future properties.

I have no strong feelings about the UI / API.