Unable to prove correctness of binary_search example

[polwel]

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]

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

To verify the program, Flux needs to infer 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.

[ranjitjhala]

@nilehmann the link above is broken? any idea -- usual issues on goto?