Verifying Quicksort

[amacfie]

CrossHair verifies a contract if, with the --report_all flag, it tells us the contract was "Confirmed over all paths". It would be cool if we could exhibit an implementation of Quicksort together with a contract asserting its correctness which CrossHair verifies.

For reference, implementations of Quicksort have been verified by the F* type checker and Isabelle.

[pschanely]

Sadly, CrossHair alone won't meet the bar for most verification tasks. It's hopefully a good bug finder, but cases that it can fully verify are pretty trivial. Quicksort is beyond what CrossHair can manage: at a minimum, it requires iterating over the input list, which results in an infinite number of unique execution paths.

There's a product-design tradeoff here: real verification systems require the engineer to guide the proof; you might need to specify lemmas or provide loop invariants and likely prove termination properties before you even start. CrossHair doesn't expect or even allow you to say such things. And (in my experience) learning how to guide verification systems effectively is really hard!

Perhaps a small footnote: You can do something like bounded model checking with CrossHair; e.g. you can prove that quicksort works for lists that are smaller than a certain size. (by adding a restriction on the length as a precondition)

It would still be informative to have standard examples like quicksort and compare it to verification tool solutions - it might be a good way to talk about CrossHair's design tradeoffs.

[amacfie]

To some extent lemmas and loop invariants can be expressed as contracts on recursive functions (maybe not the most pythonic functions). A proof of termination could also be supplied in a contract I guess, it's just that CrossHair won't realize that it's a proof of termination or that a proof of termination is required. But as the above example shows, CrossHair doesn't use shortcircuiting in its reasoning in a powerful enough way.

[pschanely]

Ah, well now you've got something I can dig into.

I'll be excited to investigate your implementation of partition() above, as I too think it should (at least in theory) be possible. More later this week.

And, yeah, I didn't even get into the soundness stuff. CrossHair assumes the validity of all other contracts including those on recursive calls. I think this only results in potential over-pruning of paths. (but a second opinion would be valued!) It certainly means that one can't interpret "Confirmed over all paths" as verified.

[pschanely]

Got it. The unnecessary branching was happening in a CrossHair-internal part of the code where we confirm that the input list has not been mutated by the function. (due to post[]:)
Essentially, the symbolic lists didn't have enough special casing to understand that such a comparison can happen without iterating over the lists. This is fixed in c759d3b!

[amacfie]

Cool, what about this conjunctive contract:

from typing import List, Tuple

def partition(pivot: int, nums: List[int]) -> Tuple[List[int], List[int]]:
    '''
    post[]: len(nums) == len(__return__[0]) + len(__return__[1]) and all(x <= pivot for x in __return__[0])
    '''
    if len(nums) == 0:
        return [], []
    else:
        lo, hi = partition(pivot, nums[1:])
        if nums[0] <= pivot:
            return [nums[0]] + lo, hi
        else:
            return lo, [nums[0]] + hi

or maybe

from typing import List, Tuple

def all_lte(pivot: int, xs: List[int]) -> bool:
    if len(xs) == 0:
        return True
    else:
        return xs[0] <= pivot and all_lte(pivot, xs[1:])

def partition(pivot: int, nums: List[int]) -> Tuple[List[int], List[int]]:
    '''
    post[]: len(nums) == len(__return__[0]) + len(__return__[1]) and all_lte(pivot, __return__[0])
    '''
    if len(nums) == 0:
        return [], []
    else:
        lo, hi = partition(pivot, nums[1:])
        if nums[0] <= pivot:
            return [nums[0]] + lo, hi
        else:
            return lo, [nums[0]] + hi

[pschanely]

Ah, sadly I don't think either of these will work, at least at the moment.

In the first, the generator expression in the all() will try to unroll the list. And yup, the second avoids this with the recursive all_lte function. However, short-circuiting essentially works by creating a fresh return value and then executing the postconditions on it; such an execution will also effectively realize the list length.

We aren't fully at the limit of what we can do within CrossHair's framework, however. Special handling for min()/max() is possible (and I think(?) might be sufficient for this example). And I can imagine preserving symbolic sequences through generator expressions in some cases, and we could then apply appropriate handling in any()/all(). Problems in here: sequence solving gets slow quickly, and adding quantifiers to the mix makes everything much harder. (SMT solvers pair really nicely with concolic execution for this reason). It's also easy to screw up exception cases and evaluation time stuff if you aren't paying a lot of attention to it.