4 ms·

Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind:

by jules 8y ago

Very nice. I don't quite understand why you need the option in GenericBinarySearch. Doesn't the function always return Some? I had something like this in mind: let binary_search (pred: int -> bool) (low: int) (high: int): int requires { pred low = False } requires { pred high = True } requires { forall i j. (i <= j) -> (pred i -> pred j)} ensures { pred result = False /\ pred (result+1) = True } = let cur_low = ref low in let cur_high = ref high in while !cur_high - !cur_low > 1 do variant { !cur_high - !cur_low } invariant { pred !cur_low = False /\ pred !cur_high = True } let mid = div (!cur_high + !cur_low) 2 in if not (pred mid) then cur_low := mid else cur_high := mid done; !cur_low Can something like that work? let predicate pred (i: int) (x: t) (k: int) = if i <= low x then false else if i >= high x then true else k <= x.arr[i] Those tests are only necessary for the proofs, right? At run time the predicate will never be called with i <= low or i >= high, but only on low < i < high, because if high - low > 1 then low < (high + low)/2 < high. That's what I meant by pretending that the predicate returns false/true on -1 or arr.length: we don't actually need the predicate to work on those indices, because we never call the predicate at those indices.

wizeman 8y ago
> Can something like that work? Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works. Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML. Here's a working complete implementation of your version: https://clbin.com/cwvKY https://clbin.com/cwvKY There's only a minor caveat with your version: there's no formal guarantee that `binary_search` won't call `pred` below `low` or above `high`, because (as far as I know) we can't encode those requirements if we pass the function as an argument. Maybe there's a way to do that, but I don't know WhyML that deeply. > Those tests are only necessary for the proofs, right? I think so. We can probably separate `pred` into a logical version and a run-time version, making sure that the result of the logical `pred` matches the result of the run-time `pred` when `-1 < idx < length arr`. I think this should be very easy to do with WhyML, I will try and figure out if I can do it.
- jules 8y ago
  That would be nice, then the run time predicate can be fast while the logical version remains elegant. What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property. If you add the uniqueness to the ensures, does Z3 still automatically prove it correct? ensures { forall j. pred j = False /\ pred (j+1) = True -> j == result) }
  - wizeman 8y ago
    > What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed). Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verified correctly, and `pred (result+1) = True`, which cannot be verified automatically. I think this is because nothing stops `high` from actually being lower than `low`. If someone passes those 2 arguments reversed (high as low and low as high), then probably the algorithm wouldn't work, right? At least, Why3 is not convinced that it would work. However, if I add this loop invariant: `!cur_low < !cur_high` and this function precondition: `requires { low < high }`, then it all works fine! (both are required). Diff here: https://clbin.com/wVkhO https://clbin.com/wVkhO And full code here: https://clbin.com/2gBfJ https://clbin.com/2gBfJ I tried separating `pred` into logical and run-time versions (one with the ifs and the other only with the comparison), and it all seems to work fine, except for one problem: The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition. Therefore, Why3 complains that the precondition of `pred` may not be respected (all other verification conditions are proven to be valid). I could do what I did before (making `low` and `high` functions, etc) but that greatly complicates the code... Maybe there is some way to do that, but currently I don't know how.

by jules 8y ago

wizeman 8y ago

> Can something like that work? Yes, indeed! Your version is not only a lot more simple and elegant than mine, but your proof code was enough for Z3 to automatically figure out that everything works. Therefore, I hereby declare that you are ready to use and learn more about Why3/WhyML. Here's a working complete implementation of your version: https://clbin.com/cwvKY https://clbin.com/cwvKY There's only a minor caveat with your version: there's no formal guarantee that `binary_search` won't call `pred` below `low` or above `high`, because (as far as I know) we can't encode those requirements if we pass the function as an argument. Maybe there's a way to do that, but I don't know WhyML that deeply. > Those tests are only necessary for the proofs, right? I think so. We can probably separate `pred` into a logical version and a run-time version, making sure that the result of the logical `pred` matches the result of the run-time `pred` when `-1 < idx < length arr`. I think this should be very easy to do with WhyML, I will try and figure out if I can do it.

jules 8y ago
That would be nice, then the run time predicate can be fast while the logical version remains elegant. What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. That property ensures that the answer will be unique, but the algorithm will find a point pred i = False /\ pred (i+1) = True even if the predicate does not satisfy that property. If you add the uniqueness to the ensures, does Z3 still automatically prove it correct? ensures { forall j. pred j = False /\ pred (j+1) = True -> j == result) }
- wizeman 8y ago
  > What happens if you remove requires { forall i j. (i <= j) -> (pred i -> pred j)}? I think it should still check, actually. If I simply remove that 'requires', then Why3 cannot prove the postcondition of `binary_search` automatically anymore (using the Z3, CVC4 and Eprover automatic provers that I have installed). Specifically, Why3 tries to split the postcondition into the 2 parts: `pred result = False`, which gets verified correctly, and `pred (result+1) = True`, which cannot be verified automatically. I think this is because nothing stops `high` from actually being lower than `low`. If someone passes those 2 arguments reversed (high as low and low as high), then probably the algorithm wouldn't work, right? At least, Why3 is not convinced that it would work. However, if I add this loop invariant: `!cur_low < !cur_high` and this function precondition: `requires { low < high }`, then it all works fine! (both are required). Diff here: https://clbin.com/wVkhO https://clbin.com/wVkhO And full code here: https://clbin.com/2gBfJ https://clbin.com/2gBfJ I tried separating `pred` into logical and run-time versions (one with the ifs and the other only with the comparison), and it all seems to work fine, except for one problem: The run-time version of `pred` is a partial function (it only works for valid array indices), so it needs a precondition. However, when I pass `pred` as an argument to `binary_search`, I can't / don't know how to specify that the argument needs the precondition. Therefore, Why3 complains that the precondition of `pred` may not be respected (all other verification conditions are proven to be valid). I could do what I did before (making `low` and `high` functions, etc) but that greatly complicates the code... Maybe there is some way to do that, but currently I don't know how.