search

flux-rs / flux

Refinement Types for Rust
MIT License
637 stars 17 forks source link

Unable to prove correctness of binary_search example #753

Closed polwel closed 2 weeks ago

polwel commented 3 weeks ago

The documentation presents a flawed implementation of binary search. That is an awesome example!

The text mentions that an off-by-one error has been introduced. Indeed, I can tell the while left <= right condition should read while left < right. AFAICT, the implementation otherwise is identical to the one from std.

However, flux still rejects it.

What am I missing?

nilehmann commented 3 weeks ago

Hi @polwel, thanks for posting. Flux can't prove the program correct because it's missing qualifiers.

To verify the program, Flux needs to inver that size == left + right is a loop invariant. Flux infer loops invariants by instantiating formulas from a set of "templates" called qualifiers. You can use the scrape_quals flag to tell Flux to try to infer those templates from the constraint. You can enable it with #![flux::cfg(scrape_quals = true)] (for example). The flag is not enabled by default because it has performance impacts.