Nothing validates the Kani mutation-evidence patches, and one harness has none

[leynos]

Observation

The repository's non-vacuity discipline for Kani harnesses rests entirely on the mutation patches under docs/verification/mutations/. Each patch seeds one realistic fault into production code that its harness must reject, which is what stops a harness from passing for the wrong reason — or for no reason at all.

Nothing in the repository checks that these patches still work, and one harness has no patch at all.

Evidence

No build target, workflow, or test references the directory:

$ grep -rn "verification/mutations" Makefile .github/ tests/ scripts/
(no matches)

There are twelve patches for thirteen harnesses:

$ ls docs/verification/mutations | wc -l
12
$ grep -rc "kani::proof" src/ir/cycle_verification.rs src/ir/from_manifest_verification.rs
src/ir/cycle_verification.rs:9
src/ir/from_manifest_verification.rs:4

The harness without a patch is canonicalize_path_wrapper_matches_u8_kernel_for_two_nodes (src/ir/cycle_verification.rs), added by roadmap item 4.2.2.

Why it matters

Two independent failure modes, neither of which produces a signal today.

Patch rot. The patches are handwritten unified diffs. Any edit near a patched hunk breaks git apply silently. When that happens the evidence is worthless, but make kani-ir still reports VERIFICATION:- SUCCESSFUL and nothing indicates that the harness is no longer known to be load-bearing.

Missing evidence. A harness added without a patch is a harness with no demonstration that it can fail. docs/developers-guide.md states that "Mutation evidence for these harnesses lives under docs/verification/mutations/" without recording an exception, so the discrepancy currently reads as an oversight rather than a decision.

This is not hypothetical damage yet — the existing harnesses are believed sound — but the guarantee is convention-only, and conventions do not survive refactors.

Suggested resolution

1. Add a contract test, in the style of the existing tests/kani_cfg_ui_tests.rs, that:

   • runs git apply --check over every file in docs/verification/mutations/, and
   • asserts that every #[kani::proof] harness in src/ has a correspondingly named patch or appears in an explicit exemption list with a stated reason.

   It runs in make test, costs about a second, and catches both failure modes.

2. Decide the adapter harness question. Either write a patch for canonicalize_path_wrapper_matches_u8_kernel_for_two_nodes, or record it as a deliberate exemption on the grounds that the u8 kernel harnesses carry the mutation evidence for the algorithm it adapts — and say so in docs/developers-guide.md so the count stops looking like drift.

Relationship to roadmap 4.2.3

The execution plan for roadmap item 4.2.3 (PR #564, obligation OBL-PATCHES) proposes adding exactly the contract test in (1), because five new harnesses would otherwise inherit the same gap. That plan deliberately does not resolve (2), since the missing patch belongs to 4.2.2's work and silently fixing another roadmap item's evidence inside an unrelated change would obscure the decision.

This issue exists so (2) is not lost, and so (1) is still tracked if 4.2.3 is descoped or deferred.

References

• docs/execplans/4-2-3-kani-harnesses-for-command-interpolation.md — OBL-PATCHES and the Surprises & discoveries entry
• docs/developers-guide.md — "Kani harness inventory"
• docs/adr-004-bound-kani-ir-harnesses-to-small-n.md