`--export-json`: a failed, empty, or partial run can serialize as a clean pass

[ivmat]

--export-json is a -Z-gated, currently-undocumented output. Using it as a CI pass/fail
oracle in a standard-library verification effort, we hit several cases where the exported file
does not faithfully represent the run: a run that failed, was skipped, matched nothing, or
wasn't fully measured can be read as a clean, complete pass by a consumer that trusts the file.

These are reporting-fidelity issues in an unstable output — none changes a verification
verdict, a property status, or Kani's exit code. Grouped below by how each is best fixed.

Driver bugs — pre-existing (predate #4472), surfaced but not caused by --export-json; tracked as two small standalone PRs

A. A filter that matches zero harnesses runs to a completed / 0 failed export.
determine_targets only bails on a missing filter under --exact (metadata.rs:112); the
generic "no harnesses matched" bail lives in print_final_summary (harness_runner.rs:302),
which runs after the export is written — so a filter typo yields Ok([]), a clean-looking
export, and exit 0. Same area, independent of --export-json: print_final_summary
early-returns under --quiet (harness_runner.rs:255) before that bail, so
kani --quiet --harness <typo> skips the "no harnesses matched" error and exits 0.
Fix in determine_targets, before codegen and before any export.

B. --fail-fast drops the harnesses it skipped (#4729).
Root cause: collect::<Result<Vec<_>>>() (harness_runner.rs:105) short-circuits on the first
Err and discards already-completed Ok results. The lost harnesses are then absent from the
per-harness details, and the plain-text summary and SARIF under-report too — not only the JSON.
Fix the collect (#4729), not the reporter.

Deferred to RFC #4727

• Stale export is never invalidated. A run that reuses an existing --export-json path and
  dies before the write leaves the previous complete-looking file in place. The completeness
  mechanism (atomic temp-file + rename, "file exists ⇒ complete") is a schema/design decision
  specified in RFC RFC: Structured verification results (export-json) #4727, not a writer patch.
• No leaf-value / semantic validation of the exported file. Pending the RFC's open question
  on shipping a JSON Schema (schemars) vs. a homegrown validator.
• cbmc_stats parsing is brittle (exact strip_prefix/strip_suffix; a malformed duplicate
  can clobber a valid value; overflow/absence collapse to null). Pending the RFC decision on
  whether CBMC statistics remain in the schema at all.

Schema (with the RFC)

• harness_id == pretty_name can misattribute across a workspace. pretty_name can collide
  between two crates, so the metadata↔details join can attribute a result to the wrong harness
  (confirmed with a workspace carrying duplicate harness names). Fix: make harness_id
  crate-qualified (mangled_name / crate::pretty) — the consumer-facing id, not only the join.

---

The paired implementation PR #4732 is closed in favor of this decomposition: the two driver PRs,
the RFC, and crate-qualified harness_id.

[feliperodri]

@ivmat I verified five of the six claims directly:

• Stale export — verify_project (main.rs:143) has a single handler.export()? at the end. Nothing invalidates the target first. True.
• Zero-match exports as a clean pass — determine_targets only bails when --exact (metadata.rs:112). The generic "no harnesses matched" bail lives in print_final_summary (harness_runner.rs:302), which runs after the export. True.
• --fail-fast drops skipped harnesses — process_harness_results (schema_utils.rs:336) has if let Some(result) = ... with no else. True.
• Validator checks no leaf values — validate_json_export.py ends at # Leaf values - no validation needed. failed: -100 passes. True.
• record_seconds clobbers — *field = value.strip_suffix('s').and_then(...) assigns unconditionally (call_cbmc.rs:161). A later malformed duplicate erases a valid value. True. u32 overflow → null also true.
• pretty_name collisions — pretty_name is readable_name, which strips the local crate prefix, so two workspace crates can share one. Real, though it needs a workspace with duplicate harness names.

But labeling these [S] soundness is wrong, and that framing is doing a lot of work in the issue. None of them affect a verification verdict, a property status, or Kani's exit code. They are reporting-fidelity bugs in a -Z unstable-options-gated flag that has zero documentation (grep -rn export-json docs/src/ → nothing) and, as far as I can tell, one consumer: the reporter's own verified-std effort. "Soundness/misreport" reads like a CBMC-level unsoundness claim. It isn't.

[feliperodri]

Also, @ivmat. Two of the six items are work against code the RFC #4727 deletes...

• Item 5 (cbmc_stats) is 111 added lines in call_cbmc.rs hardening a text scraper that RFC 0016 explicitly proposes to remove. The RFC's own exclusions section says CBMC statistics are "available only inside CBMC's free-text messages. Extracting them means pattern-matching human-readable output, which is the fragility this RFC exists to remove; doing it inside the fix would be self-defeating." PR Fix --export-json reporting a failed, skipped, or zero-match run as clean #4732 then builds parse_leading_number_with_remainder to make that pattern-matching more robust.
• Item 4 (validator) is ~290 lines — 111 in the Python validator, a 113-line fixture generator, a 68-line test script, roughly half the PR... building a second homegrown validator, when you already declined that on Add --export-json for structured verification results #4472 on the grounds that "anything homegrown I write here gets thrown away when that's settled," pending the schemars/JSON Schema decision that is open question Consider having our own CBMC mode instead of just using "C" #1 in the RFC.

[feliperodri]

Let's be more concrete, @ivmat:

1. Extract the two items that are real driver bugs with no schema dependency, as separate small PRs benefiting all users: zero-match failing before verification (plus the --quiet exit-0 bug), and --fail-fast discards results for harnesses that already completed #4729. Both make issue items 2 and 3 disappear.
2. Defer items 4 and 5 to RFC decisions (JSON Schema/schemars; whether cbmc_stats survives at all).
3. Take item 6 only as part of making harness_id crate-qualified in the schema; the join-only change is cosmetic.

The core a general user needs is per-harness status, per-property status/location/class, the exhaustive counts, and enough provenance to reproduce. The rest of what #4472 shipped is niche: CBMC internal statistics (VCC counts, symex time, slicing), os_info, object_bits, and solver-binary version probing... create_tool_versions_json spawns a process per tool, and cbmc --version twice per run since get_cbmc_info probes it again. That's the surface generating the follow-up stream. Cutting v1 to the core, removes items 4, 5 and most of the schema-validator burden by construction.

[feliperodri]

Item 7 was filed unverified ("NEEDS CONFIRMATION"), which shouldn't be in an issue.

[ivmat]

@feliperodri you are correct — this issue report and related PR were reported hastily without much thinking or consideration from my side. i wanted to "get on with it so I can add PRs on enhancements" but wanted to clear issues beforehand - and did not actually do disciplined work myself. the s labels overclaimed — you are right these are reporting-fidelity bugs, not soundness — and item 7 should not have been filed unverified. i apologise for causing unnecessary work for you and for wasting CI. you are taking time to do proper review so i should do the proper work myself

what i did now: close #4732 and edited this issue per your plan (removed s labels, dropped item 7, restructured per your comments). to be done: the 2 small kani-driver PRs first (zeromatch/quiet in determine_targets, and #4729). will reproduce both on my machine before writing any fix. items 4-5 wait for the RFC decisions, item 6 goes with crate-qualified harness id. ive done too much bulk-things — rigor and focus is what is most important & whats missing in general when using ai (especially for formal verification tool contribution delivery) and this clashes with my "get things out asap" approach.