fail harness if cover is not satisfied

[camshaft]

Requested feature: fail harness
Use case:

I just realized that the current bolero integration allows a proof to go through, even if you've specified a generator that is impossible to satisfy:

#[test]
#[kani::proof]
fn my_test() {
    bolero::check!().with_type::<u8>().filter(|_| false).for_each(|_| {
        panic!();
    });
}

$ cargo kani --tests --harness my_test --output-format=terse
Checking harness my_test...

VERIFICATION RESULT:
 ** 0 of 255 failed

 ** 0 of 1 cover properties satisfied (1 unreachable) // <= this should ideally fail the proof

VERIFICATION:- SUCCESSFUL
Verification Time: 0.14628594s

Complete - 1 successfully verified harnesses, 0 failures, 1 total.

Ideally, we'd replace the call to kani::assume with a cover call that would force harness failure. This could be called something like kani::cover_or_fail! or kani::assert_cover!.

Doing a test with multiple harnesses, it seems to behave as one would expect and only applies to the individual harness:

#[test]
#[kani::proof]
fn my_test() {
    bolero::check!().with_type::<u8>().for_each(|_| {
        // noop
    });
}

#[test]
#[kani::proof]
fn my_test() {
    bolero::check!().with_type::<u8>().filter(|_| false).for_each(|_| {
        panic!();
    });
}

#[kani::proof]
fn my_kani_proof() {
    assert_eq!(1 + 2, 3);
}

$ cargo kani --tests --output-format=terse
VERIFICATION:- SUCCESSFUL
Verification Time: 0.89504564s

Checking harness add_test...

VERIFICATION RESULT:
 ** 0 of 1502 failed (69 unreachable)

 ** 1 of 1 cover properties satisfied // <= the generator produced at least 1 valid value


VERIFICATION:- SUCCESSFUL
Verification Time: 0.8548021s

Checking harness my_test...

VERIFICATION RESULT:
 ** 0 of 255 failed

 ** 0 of 1 cover properties satisfied (1 unreachable) // <= the generator was UNSAT; should fail the harness!


VERIFICATION:- SUCCESSFUL
Verification Time: 0.14286228s

Checking harness my_kani_proof...

VERIFICATION RESULT:
 ** 0 of 2 failed  // <= this harness doesn't use bolero at all; no references to the cover property

VERIFICATION:- SUCCESSFUL
Verification Time: 0.024725173s