Keep completed results when --fail-fast aborts a run

[ivmat]

check_all_harnesses collected results with collect::<Result<Vec<_>>>(), which short-circuits on the first error. A --fail-fast abort was such an error, so every result that had already completed was dropped. The summary then contradicted the per-harness output above it, and --export-json under-reported the run the same way.

Completed results now accumulate in a shared vector as harnesses finish. The abort signal carries no payload; the failing harness records its result like any other. Results are re-sorted into harness order after the parallel loop, since completion order is nondeterministic.

The parallel fail-fast UI test pinned the old behavior: "1 failures, 1 total" for ten failing harnesses under --jobs 4. With completed results retained, those counts depend on thread scheduling, so the test becomes a script-based test asserting the stable properties: the run aborts early (fewer than ten run) and every counted harness is a failure. The sequential UI test is unchanged: it aborts on its first harness, so its pinned summary stays correct. A new sequential script-based test proves retention deterministically ("1 successfully verified, 1 failures, 2 total"); it fails on main.

Testing: cargo test -p kani-driver, rustfmt, and clippy are clean; the two new script-based tests and the existing stop_at_single_fail UI test pass.

Resolves #4729

[Copilot]

Pull request overview

Retains completed harness results when --fail-fast aborts verification, keeping summaries and JSON exports accurate.

Changes:

• Accumulates parallel results safely and restores harness ordering.
• Replaces schedule-dependent UI expectations with script-based checks.
• Adds a deterministic sequential regression test.

Reviewed changes

Copilot reviewed 10 out of 10 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
kani-driver/src/harness_runner.rs	Retains and sorts completed results.
tests/ui/multiple-harnesses/stop_at_single_fail/fail_fast_test_parallel.expected	Removes obsolete fixed summary.
tests/script-based-pre/fail_fast_parallel/fixture.rs	Updates parallel fixture documentation.
tests/script-based-pre/fail_fast_parallel/early_abort.sh	Checks parallel fail-fast behavior.
tests/script-based-pre/fail_fast_parallel/early_abort.expected	Adds expected script result.
tests/script-based-pre/fail_fast_parallel/config.yml	Configures parallel regression test.
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.sh	Checks deterministic result retention.
tests/script-based-pre/fail_fast_keeps_completed/keeps_completed.expected	Adds expected script result.
tests/script-based-pre/fail_fast_keeps_completed/fixture.rs	Adds passing and failing harnesses.
tests/script-based-pre/fail_fast_keeps_completed/config.yml	Configures sequential regression test.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

[feliperodri]

Diagnosis and fix are right, and this is the direction I suggested in #4729 — the accumulator + re-sort is exactly it. Nice catch on the sort in particular: the old collect::<Result<Vec>> on an indexed rayon iterator was order-preserving, so without it you'd have silently changed export ordering for every parallel run, not just fail-fast ones. I also checked the determinism argument for the new sequential test and it holds (sort_harnesses_by_loc reverses on start line, jobs() defaults to 1 thread), and the existing sequential UI test really is unaffected.

Blocking on the first inline comment; the rest are cheap.

One more that I can't anchor inline because the file isn't in the diff: schema_utils.rs:362-365 says verification_results.results "is in completion order", which is why entries need harness_id. After this PR the order is deterministic. The conclusion still stands (sorted-by-loc != harness-metadata order) but the stated reason is now wrong — please reword.

Regression suites are still running, so I haven't seen an end-to-end green.

[feliperodri]

This is the one I'd like changed. FailFastAbort shares rayon's Err channel with real errors (instrument_model, check_harness, playback). If one harness trips fail-fast while another returns a real error, try_for_each surfaces one of them arbitrarily — and if the abort wins, the real error is swallowed and we print a normal-looking summary with exit 1.

Pre-existing in shape, but your restructure makes the clean fix nearly free: use an AtomicBool latch for fail-fast, check it at the top of the closure and return Ok(()), and keep Err for genuine errors only. You lose rayon's producer-level short-circuit, but a skipped harness then costs one atomic load instead of a CBMC run, and error precedence stops being luck.

[feliperodri]

The order is fixed here, but the set is still schedule-dependent, and that's a user-visible contract change: --export-json is no longer reproducible for --fail-fast --jobs N, so CI consumers diffing exports will see churn run to run.

I think that's the right behavior (it's the honest one), but it needs to be written down somewhere. --fail-fast has zero mentions in docs/ and a one-line help string (args/mod.rs:261). Please add a sentence there: in-flight harnesses finish and get counted, so counts vary under --jobs.

[feliperodri]

Wrong suite for this half. Every other --export-json test lives in tests/json-handler/, so nobody auditing export coverage will find this. Also, unlike its siblings there, it never runs scripts/validate_json_export.py — so nothing checks that the completed_with_fail_fast document still validates structurally.

Suggest splitting: keep the summary assertions here, move the export assertions to tests/json-handler/fail-fast/ and run the validator.

[feliperodri]

Flagging, not blocking: this turns a pinned test into a timing test. Realistically safe — 4 threads means ~4 chunks and full() is checked before each item, so TOTAL lands near 4 — but the bound is doing no work if scheduling ever changes.

The VERDICTS == TOTAL check below is the load-bearing assertion and holds under any schedule. Fine to keep the < 10 guard, just don't count it as the regression check.