A Formal Verification of Rust's Binary Search Implementation
kha.github.io
kha.github.io
I don't know much about formal methods. I was surprised by this:
> Indeed, if you like at the prelude, you may notice that currently there’s no modelling of overflows – all integer types are unbounded on the Lean side
But integer overflow is one of the most common bugs in binary search [1]. I don't mean to attack this work, but what good are formal methods if they still allow failures like this? Honest question.
> In any case, overflow checking is not very interesting for the implementation at hand because every integer in there is trivially bounded by self.len()
Hmmm. See line 317 or 321: base + head.len() is not "trivially" bounded by self.len(), at least not to me.
[1]: https://research.googleblog.com/2006/06/extra-extra-read-all...
Similarly `s.len() >> 1` is a strictly decreasing value by division, so no concern for underflow.
For it to work, it requires that every number be returned as part of the result, and that all calculations are monotonically increasing, as you said. Most algorithms won't have those invariants, but perhaps you can tweak them until they do. Once you have, you can extend an infinite-width proof to a finite-width proof.
It's research and not a production product: they're likely concentrating on problems that are original and interesting to the research community instead of looking at problems that the community knows are already solvable.
> Hmmm. See line 317 or 321: base + head.len() is not "trivially" bounded by self.len(), at least not to me.
Sure it is. Just look at that next line, `s = &tail[1..];`. When head.len()+1 is added to base, we then discard head and the first element of tail, so we just discarded head.len()+1 elements. It should be fairly obvious that if we always add the number of discarded elements to base, then base can never exceed the number of discarded elements, and similarly that we can never discard more elements than self.len(). Therefore, base can never exceed self.len().
Trivially true things cannot depend on "fairly obvious" observations. In fact you cannot reason locally here: you must understand the whole code to convince yourself that it does not overflow. Consider an off-by-one error, like replacing line 318 with:
s=&tail[0..];
Anyways the point of formal methods is to give yourself something better than "read carefully" to convince yourself of correctness.
I've written about overflow checking some more below, but what you'd really want for that is some solid support of subtypes or refinement types - it's not just integers that have to become bounded, but also most data structures. Lean isn't quite there yet, unfortunately, but this should change in the near future with its new focus on powerful automation.
Unwinding assignments into a single-assignment notation is common in verification. (We did it automatically 30 years ago in the Pascal-F verifier.) Rust is expressive enough that you can do that in Rust itself, which is convenient. It's not "functional" that's important for this; it's single-assignment. Each variable in the proofs can have only one meaning, because the proofs have no notion of time. (Well, there's temporal logic, but you don't need to go that route.)
Whether you should trust the compiler is always an issue. When we did this, we verified at the stack-machine level. At that level, operations are like "pop two operands from stack, add in 16 bit integer mode, push result". At that level, semantics are relatively simple. If you have the compiler's dictionary available, you can give names to all those things being pushed and popped, much as a debugger does.
The answer is no.
In the early days of program verification it was popular to work at the source code level, because automatic efforts were trying to emulate what humans were doing by hand. Early programming verification was trying to emulate what mathematicians did. Efforts were made to describe languages axiomatically at the source level. Now that's recognized as both very hard and likely to lead to errors.
You're correct in that what I'm constructing is some form of Dynamic Single Assignment. But together with the eradication of mutable references (and perhaps other effects in the future), it felt better to me to describe the transformation from the purity aspect.
Oh.
When I used Uppaal in my grad school course, I kept messing up when I tried to hand translating my code from the model.
Haven't tried it but this claims to be able to extract Rust programs from Coq proofs:
As of right now, the project would probably be easier in Coq. But I'm confident that Lean 3 will eventually feature more powerful automation (and no Ltac). It is, after all, being developed by Leonardo de Moura, one of the creators of Z3.
If you haven't looked at it already, you may be interested in Arthur Charguéraud's work on program verification using characteristic formulas (http://www.chargueraud.org/softs/cfml). CFML is a similar tool for ocaml verification using Coq.
Aside, if we're reinventing the wheel anyways, why not in a proper style? There's no reason to not deploy purely functional code (+some effectful shims). Think https://mirage.io https://nqsb.io -- rust has way too much mutation and unsafe builtin already...
[1] http://dl.acm.org/citation.cfm?id=1573604 also available at [2]