Hacker News Reader

Comment by millstone | Hacker News Reader

Here's the Rust binary search source: https://github.com/rust-lang/rust/blob/27e766d7bc84be992c8dd...

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...

View on HN

If you read the Rust code you linked, you'll notice that it's written very differently than the classic binary search. Specifically, it doesn't keep track of low/high indices, which means it doesn't have the `(low + high) / 2` step that your googleblog.com article says is the source of integer overflow.

> 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().

Hey, there's more than one way to overflow an integer!

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..];

and now base will overflow.

Anyways the point of formal methods is to give yourself something better than "read carefully" to convince yourself of correctness.

Well, that change would also break the proof in general :) . But I see your point.

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.

I believe ( (low>>1) + (high>>1) + ((low&1) & (high&1)) ) renders the desired result sans overflow.

I imagine a basic proof amounts to: the result (base) is monotonically increasing (even in intermediate calculations) and the length of the slice fits in a usize, so if the correct result is always produced with infinite precision there's no concern for overflow (correct results are bounded by the len).

Similarly `s.len() >> 1` is a strictly decreasing value by division, so no concern for underflow.

I like that. That's a powerful argument!

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.

> I don't mean to attack this work, but what good are formal methods if they still allow failures like this? Honest question.

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.

Not "trivially", sure :) but it's not hard to prove either.

Reply on news.ycombinator.com