4 ms·

Awesome! Interesting that it can prove that given only the loop invariant. The inner loop could be factored to a subroutine with the following contract: let P

by jules 8y ago

Awesome! Interesting that it can prove that given only the loop invariant. The inner loop could be factored to a subroutine with the following contract: let P be a predicate on the integers such that (i <= j) => (P(i) => P(j)), and let low be such that P(low) = false and high such that P(high) = true. The subroutine returns i such that P(i) = false and P(i+1) = true. The subroutine further promises to only call P(k) on low < k < high. This may be applied to the predicate P(k) = (x <= arr[k]) on the range (low,high) = (-1,arr.length) to find the point at which the predicate flips from false to true (we're essentially pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length], and the subroutine promises to only call P(k) on values strictly between -1 and arr.length). Is it possible to do this with WhyML?

wizeman 8y ago
Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.
wizeman 8y ago
Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the following bug in Why3 (it's already fixed in the master branch, but not in the most recent release): https://gitlab.inria.fr/why3/why3/issues/214 https://gitlab.inria.fr/why3/why3/issues/214 2. It turns out that the value of "high" is not statically known at compile time, because it depends on the size of the array. So I changed "high" to be a function of the array rather than a constant (I did the same to "low" for consistency). 3. Similarly and consequently, the predicate P(i) is not only a function of "i". It's also a function of the value being searched for ("x"), i.e. if P(i) is true or not depends on which value you're searching for. This also means that P() is also a function of the specific array being searched for (because some arrays may have "x" but others not). 4. You said that "we're pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length]", but unless I misunderstood something, we can't actually pretend that, this must be written in the code somewhere, otherwise it won't work. For simplicity, I have chosen to implement those rules in the predicate itself. However, this is also enforced by the function with the while loop, i.e., it always makes sure that whatever predicate you have chosen, it has to implement those rules. I am sure that this could be changed, but I think it would complicate the proofs. The result is that in module "GenericBinarySearch", like the name says, we have a neat generic binary search function which works with any predicate P (called "pred" in the code), any function "low", any function "high" and for any type. And in module "ArrayBinarySearch" we have an instantiation of "GenericBinarySearch" which works for sorted arrays! Also note that the axiom in the code is only an axiom in the generic module (it specifies what must be true of P()), but when the generic module is instantiated, Why3 verifies that the axiom is actually true for the specific instance of the predicate (so there is no cheating). You can find the code in the link below. Enjoy! https://clbin.com/Ov3NX https://clbin.com/Ov3NX
- 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.

by jules 8y ago

wizeman 8y ago

Actually, my loop invariant was unnecessarily confusing (I was sleep deprived), here's a better version: https://clbin.com/OhyJ3 https://clbin.com/OhyJ3 Your question is very interesting and I think the answer is 'yes'. I will try to implement it and report back.

wizeman 8y ago

Ok, so this proved to be more difficult than I anticipated and it took me a while, but fortunately I really enjoyed the challenge! It seems that the answer is definitely "yes", it can be done with WhyML. There are a few minor caveats: 1. I had to change the function with the while loop to return an option instead of raising the Not_found exception, which makes the code a bit uglier. This is because I ran into the following bug in Why3 (it's already fixed in the master branch, but not in the most recent release): https://gitlab.inria.fr/why3/why3/issues/214 https://gitlab.inria.fr/why3/why3/issues/214 2. It turns out that the value of "high" is not statically known at compile time, because it depends on the size of the array. So I changed "high" to be a function of the array rather than a constant (I did the same to "low" for consistency). 3. Similarly and consequently, the predicate P(i) is not only a function of "i". It's also a function of the value being searched for ("x"), i.e. if P(i) is true or not depends on which value you're searching for. This also means that P() is also a function of the specific array being searched for (because some arrays may have "x" but others not). 4. You said that "we're pretending to know that there is a small value at arr[-1] and a large value at arr[arr.length]", but unless I misunderstood something, we can't actually pretend that, this must be written in the code somewhere, otherwise it won't work. For simplicity, I have chosen to implement those rules in the predicate itself. However, this is also enforced by the function with the while loop, i.e., it always makes sure that whatever predicate you have chosen, it has to implement those rules. I am sure that this could be changed, but I think it would complicate the proofs. The result is that in module "GenericBinarySearch", like the name says, we have a neat generic binary search function which works with any predicate P (called "pred" in the code), any function "low", any function "high" and for any type. And in module "ArrayBinarySearch" we have an instantiation of "GenericBinarySearch" which works for sorted arrays! Also note that the axiom in the code is only an axiom in the generic module (it specifies what must be true of P()), but when the generic module is instantiated, Why3 verifies that the axiom is actually true for the specific instance of the predicate (so there is no cheating). You can find the code in the link below. Enjoy! https://clbin.com/Ov3NX https://clbin.com/Ov3NX

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.