--fail-fast discards results for harnesses that already completed #4729

When --fail-fast stops a run, the results of harnesses that already finished are discarded. Kani reports only the failing harness, so its own summary contradicts the output printed just above it.

Reproduce

// ff.rs
#[kani::proof]
fn aaa_passes() {
    let x: u8 = kani::any();
    kani::assume(x < 10);
    assert!(x < 20);
}

#[kani::proof]
fn bbb_fails() {
    let x: u8 = kani::any();
    assert!(x < 20);
}

#[kani::proof]
fn ccc_passes() {
    let x: u8 = kani::any();
    kani::assume(x < 5);
    assert!(x < 20);
}

$ kani ff.rs --fail-fast
Checking harness ccc_passes...
VERIFICATION:- SUCCESSFUL
Checking harness bbb_fails...
VERIFICATION:- FAILED
Verification failed for - bbb_fails
Complete - 0 successfully verified harnesses, 1 failures, 1 total.

ccc_passes ran and was reported SUCCESSFUL two lines earlier, but the summary says 0 successfully verified harnesses and 1 total.

Expected

The summary should account for the harnesses that actually ran: 1 successful, 1 failed, 2 executed out of 3 selected. Whether the remaining unrun harnesses are reported as skipped is a separate question; the ones that completed should not vanish.

Root cause

In kani-driver/src/harness_runner.rs, check_all_harnesses collects with collect::<Result<Vec<_>>>(), which short-circuits on the first Err and drops the Ok results already produced. The fail-fast branch then rebuilds a vector containing only the failing harness:

if err.is::<FailFastHarnessInfo>() {
    let failed = err.downcast::<FailFastHarnessInfo>().unwrap();
    Ok(vec![HarnessResult {
        harness: sorted_harnesses[failed.index_to_failing_harness],
        result: failed.result,
    }])
}

That vector is what feeds print_final_summary, which is why the counts are wrong.

Impact

Two places, and the second is new:

1. The rendered summary is self-contradicting, as above. A user who runs with --fail-fast cannot tell from the summary how much of the suite got through before the failure.
2. Machine-readable output. Add --export-json for structured verification results #4472 adds --export-json, and because it derives from the same vector, the export reports "executed": 1 and "successful": 0 for the run above, with results containing only bbb_fails while harness_metadata lists all three. Any CI consumer counting executed harnesses gets a number that is simply untrue. Fixing it here fixes both.

Suggested direction

Carry the completed results through the fail-fast path rather than reconstructing a single-element vector — for example by accumulating into a Vec<HarnessResult> that the fail-fast error can hand back alongside the failing harness, or by partitioning the iterator's results instead of using collect::<Result<_>>'s short-circuit.

Found while reviewing #4472. Related: #3458, which requested the --fail-fast behaviour.