3 ms·
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 lo
by eridius 10y ago
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().
- millstone 10y agoHey, 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.
- derkha 10y agoWell, 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.
- ArkyBeagle 10y agoI believe ( (low>>1) + (high>>1) + ((low&1) & (high&1)) ) renders the desired result sans overflow.