Proofs and Refutations Using Z3 | Hacker News Reader

Proofs and Refutations Using Z3

blog.janestreet.com

77 pointsyminsky21 comments

Model checkers are amazing tools. I've been using one for C development for the past two years, and with the model checker, I feel more confident about code I write in C than I do about code in many other languages.

That being said, model checkers find counter-examples. This is not the same as a formal proof. Just because a counter-example cannot be found does not mean that a given property has been proven. It is _extremely_ important to understand that point. Model checking, combined with unit testing, is a formidable tool that should be used whenever possible. But, don't assume that model checking is the same as a proof. The subtle difference does matter, and it can bite you.

It is possible to write formal proofs about software, using Calculus of Constructions, Separation Logic, Hoare Logic, etc. However, this is much harder than using a model checker. For 95% of applications, a model checker is good enough.

This is not true in theory. A model checker (NOT a bounded model checker) either produces a counter-example, a proof of correctness or times-out/gives up if the theory is not decidable.

A bounded model checker on the other hand, checks the property for a given depth 'k', and hence the result is not applicable to a complete run.

In practice, it is all engineering, so anything can happen unless the model checker has been model checked.

To the extent the model corresponds with reality, a given property is proven due to lack of counterexample.

To the extent that the model checker is complete and error free, and to the extent that that the model corresponds with that under instrumentation.

I've been far down that rabbit hole, and I've found cases where certain model checkers fail to find counterexamples that other model checkers find. Sometimes, this is due to errors in one or more of the checkers. Sometimes this is due to differences in representation. But, ultimately, the argument is epistemological. There is a corollary to the phrase: "Absence of proof isn't proof of absence": absence of a counterexample isn't an absence of a contradiction.

As I've said, I love model checkers. But, they are not perfect, nor are they a panacea.

I said that about TLA+'s model checking. With things like Verasco, I figured a verified model checker could be done. As usual, I also searched for examples with SPIN since (a) they're used for similar things and (b) more people used SPIN in the past. Found this:

https://www21.in.tum.de/~lammich/pub/nfm2016_por.pdf

Lammich was a name I recognized immediately for his work converting functional data structures to imperative ones in Isabelle/HOL. He and his collaborators have done quite a few interesting things so I'll just leave you the whole list:

https://www21.in.tum.de/~lammich/

Far as lightweight methods, I recently summarized some recommendations with supporting case studies on Schneier's blog based on a message I sent someone trying to sell management on verification. It's a draft that I'm getting feedback on from various people rather than something I'm 100% solid on. The SPARK work combined with their book is still one of easiest methods in terms of automation achieved for covering specific properties that are often significant.

https://www.schneier.com/blog/archives/2018/02/friday_squid_...

Proof assistants are not magically bug-free.

As others have said, an exhaustive model checker failing to find a counterexample is a proof. That you trust proofs more because you haven't yet seen a bug in a proof assistant speaks only to your personal experience, not to any logical truism.

(That said, most models are not finite, and thus cannot be exhaustively checked. This is where proof systems do have a leg up. But that has nothing to do with bugs or representation of the system under test.)

That's very interesting, do you happen to have any toy examples where two model checkers differ?

In early days of CBMC, it was possible to confuse it and get it to generate incorrect code for MiniSat. This is a representation issue. Those issues have long since been solved. Now CBMC's biggest problem is that of performance, and the developers are diligently working to improve this problem.

When Z3 first came out, I built a machine model for a subset of ARMv7 and ran into a few cases that confused Z3, but worked fine in an equivalent MiniSat. However, this was years ago, and it appears -- although I have not verified this -- that the code in Z3 that I narrowed down in preparation to filing a bug report has already been fixed. The machine model has succumbed to bit rot; I abandoned the effort for a model I built on top of Coq. But, it would be interesting to attempt to fire it up again to see if it works now, and if so, use that to perform a binary search to find out when the fix was applied.

It shouldn't be hard to create an example where two model checkers differ. Check current bug reports for two model checkers, and build a model that exploits the bug in one model checker but in which the other model checker works. These code bases are complex. They are increasingly infrequent, as the developers working on these model checkers are quite diligent, but subtle errors do exist.

The other day I found an error in the Glucose SAT solver, but only when running with one of the options (-rcheck) changed away from its default setting. Glucose produced an alleged satisfying assignment that didn't actually work.

So it's possible for mainstream SAT solvers to have errors, but I imagine their default configurations are very thoroughly tested.

It's interesting that the SAT solvers haven't put in a check at the very end to confirm that satisfying instances really satisfy the constraints, since that step is of course supposed to be the radically easy one! I guess their authors have had a lot of (usually well-placed) confidence in the solvers' logic and correctness.

When I told them about it they said that the -rcheck code was inherited from MiniSAT. Since it's also not enabled by default it's understandable that it hadn't been as thoroughly checked as usual. I wouldn't blame them if they just dump it instead of fixing it.

But yes it is strange that it doesn't verify its outputs. On the other hand SAT solvers want to be as fast as possible and there shouldn't be a need to do it if the solver is operating correctly.

What do you use?

For C model checking, I use CBMC. It is a great tool, but it does take some finesse to use well.

http://www.cprover.org/cbmc/

Interesting coincidence! I just wrote a post on checking Azure firewall equivalence with Z3 two days ago: https://medium.com/@ahelwer/checking-firewall-equivalence-wi...

This post deals with a significantly harder problem, though.

Have you seen http://www.margrave-tool.org/v3/ which builds on Kodkod (which came after Alloy...)?

If you're not a fan of lispy languages, Z3 has bindings for .NET, C, C++, Java, OCaml and Python.

For example, Python version of the “x + +0 = x” check looks like this:

  from z3 import *
  s = SolverFor('QF_FP')
  x = FP('x', FPSort(11, 53))
  z = fpPlusZero(FPSort(11, 53))
  r = RNE()
  s.add(Not(fpAdd(r, x, z) == x))
  print(s.check())
  print(s.model())

(Except that I hardcoded rounding-mode, because I couldn't figure out how to make an unknown one. :-/)

Does anyone know of any good resources for high-level guidelines on how to incorporate model checking into a typical software development flow? I've only used TLA+ in my own time for some fairly basic modeling of simplified service interactions at work. The team I'm on is soon inheriting a fairly complex codebase that is one of the core backend services at my company. At a high level, it is responsible for kicking off a "state machine" (which spans a few backend services) that ultimately updates a single "item", which is the smallest unit of data we care about. I'd be interested in spending a weekend or two with getting a rudimentary model of it up and running to aid in tech spec writing of new features and perhaps documenting possible bugs in the entire state machine flow. As it stands today, the state machine spans multiple services and is ill defined so I'll be diving into that for documentation purposes regardless, and it seems like creating a codified model simultaneously won't be too much overhead (at the very least, it could be fun).

You can combine the model with property-based testing of that code to essentially try your model on the code and vice versa. You might also encode some of your expectations in there as preconditions, invariants, or postconditions that are checked at runtime during the tests. Throw a fuzzer like AFL at them.

Hwayne has write-ups on both of those concepts:

learntla.com

https://hillelwayne.com/post/pbt-contracts/

Here's one on contracts that even your management might like:

https://www.win.tue.nl/~wstomv/edu/2ip30/references/design-b...

Property-based testing seems to be an interesting idea and fairly easy to trial and then recommend to my teammates. The js library I stumbled upon even has TypeScript support and plays nicely with mocha, both of which are directly relevant to my work (https://github.com/jsverify/jsverify)!

I wrote a finite model checker in C#, which I used to exhaustively check reads/writes against some complicated serialization code (serializing a bunch of different types into the blob, updating existing objects, ensuring values of all objects were as expected). Used during some tricky memory footprint reduction stuff inside Microsoft, I'll see whether I can open source it.

Other than that, integrating TLA+ with your dev workflow is very straightforward if you're dealing with concurrency or distributed systems. In other domains its value is less obvious.

You might also take a look at the P language, which will model-check your code if you add the right hooks.

Yes, I suppose I'll try my naive TLA+ approach of modeling what I can as I document various parts of the system and see where it gets me. P looks like an interesting experiment to dabble in.

Reply on news.ycombinator.com