Support harness partition

[celinval]

Requested feature: Users should be able to partition a harness which will be verified as if it was two or more harnesses.
Use case: One way to mitigate the cost of verifying a harness is to split it one harness into multiple harnesses that contains different assumptions. This is however error prone, potentially impacting the soundness of user proof.

Test case:

/// Dummy function to be verified
pub fn target_fn(input: i32) {
    let val = if input > 0 {
        do_something_expensive(val)
    } else {
        do_something_else_expensive()
    };
    unsafe { yet_another_fn(val) }
}

/// First proof
#[kani::proof]
pub fn positive_harness() {
    let input = kani::any_where(|i| i > 0i32);
    target_fn(input)
}

/// Second proof
#[kani::proof]
pub fn negative_harness() {
    let input = kani::any_where(|i| i < 0i32); // This should've been i <= 0
    target_fn(input)
}

Note that we are missing the case where input is 0. And this can only be caught today by inspecting the proofs. Instead, it would be nice if Kani could allow users to do this as part of one harness. Something like:

#[kani::proof]
pub fn target_fn_harness() {
    let input: i32 = kani::any();
    kani::partition([i > 0, i <= 0], || target_fn(input));
}

The syntax shall be improved... But the idea would be to create a chain of harnesses, where each harness assumes a given condition. And we create a check to make sure that all the assumptions together cover all reachable cases.

I.e.: The following harness would fail:

#[kani::proof]
pub fn target_fn_harness() {
    let input: i32 = kani::any();
    kani::partition([i > 0, i < 0], || target_fn(input));
}

Since the partition doesn't handle all reachable cases.

[zhassan-aws]

And we create a check to make sure that all the assumptions together cover all reachable cases.

This can be done by checking whether the negation of the disjunction of all the partitions is satisfiable (or alternatively, whether asserting the disjunction of all the partitions passes). For example, for your example, we can do:

assert!(i > 0 || i < 0);

which will fail, indicating that i = 0 is not covered by any of the partitions.

[celinval]

Yep! That's the plan.