Proposal: two acceptance criteria for verification harnesses

[KyleClouthier]

Hi, outside reviewer here. I spent some time measuring the harness inventory in library/ and
would like to propose two acceptance criteria. Offering this as a suggestion, not as authority.

Leading with the conclusion, because it is the part most likely to get skipped: I read all 43
kani::assume sites in code and found no vacuous harness. The one that looks alarming,
kani::assume(min > max) in nonzero.rs, is correct: both bounds are symbolic and it is
deliberately paired with #[kani::should_panic] to exercise the invalid-range path. I also
mutated a merged function and the harnesses caught it. The repository is in good shape. What
follows is insurance against a regression, not a fix for present damage.

The failure mode, runnable in thirty seconds

https://github.com/KyleClouthier/kani-vacuity-demo

One deliberately broken function, (v * 2) / 2, and five harness styles against it. Only the
plain symbolic harness finds the overflow. The style whose precondition is satisfied by no i32
reports success over the empty set, with a verdict line character for character identical to a
real proof. Adding kani::cover! surfaces it in the detail and leaves the answer unchanged:

 ** 0 of 6 failed (4 unreachable)
 ** 0 of 1 cover properties satisfied (1 unreachable)
VERIFICATION:- SUCCESSFUL

None of this is new and the practice is already yours. Vacuity in model checking goes back
to Beer, Ben-David, Eisner and Rodeh (1997), formalized as mutation coverage by Chockler,
Kupferman and Vardi, and the Kani blog documented exactly this in Checking Code Reachability
and Sanity Checking Proof Harnesses with kani::cover
in January 2023. The proposal is only to make that advice mechanical, because a practice that is
recommended and not enforced is one nobody can rely on when reading a verdict.

Current state

$ grep -rn 'kani::proof'  library/ | wc -l     # 252
$ grep -rn 'kani::cover'  library/ | wc -l     #   0
$ grep -rn 'kani::assume' library/ | wc -l     #  45
$ grep -rniE 'unreachable|vacuity|cover' scripts/run-kani.sh .github/workflows/*.yml
(no matches)

Counting structurally instead of by line, so that comments and proof_for_contract forms are
handled correctly: 235 harnesses, 43 assume sites in code, and 26 harnesses that constrain
inputs with an assumption and carry no reachability check. The zero is robust under either
method.

Contracts are where this gets bigger

The autoharness job generates symbolic harnesses, so the concrete-input concern does not apply
to them. They take their assumptions from contracts instead, and library/ carries 163
#[requires] preconditions across 43 files, with 161 proof_for_contract harnesses.

A #[requires] clause is an assumption. A precondition no input satisfies, or one tightened
past the interesting case, gives a proof over an empty set and prints the same success line.
There are zero cover statements to catch that on any of the 163.

The two criteria

1. Reachability. Every assumption, whether written as kani::assume or as a #[requires]
contract, carries a reachability witness, and CI fails on UNREACHABLE. For a hand-written
harness that is a kani::cover!. For a contract the natural form is a cover check inside the
proof_for_contract harness, or a Kani-side report when a precondition is unsatisfiable. If
that second thing already exists I have missed it, and then only the CI enforcement is needed.

2. Mutation adequacy. Every submitted harness demonstrably fails against at least one
mutated implementation of the function it covers. This turns a coverage number, which answers
"was this reached," into a claim about teeth, which answers "would this have noticed if the
function were wrong."

The merged harnesses already meet the second one where I sampled. Mutating NonZero::clamp to
ignore both bounds:

Checking harness num::nonzero::verify::nonzero_check_clamp_for_u8...
Failed Checks: assertion failed: result == min
Failed Checks: assertion failed: result == max
VERIFICATION:- FAILED
Complete - 0 successfully verified harnesses, 2 failures, 2 total.

Both caught it and named the exact broken postconditions. Scope, so this is not oversold: two
harnesses on one function out of 235. A sample, not a survey. The mutation was reverted and
nothing upstream was touched.

Mutation testing is mature (Stryker, PIT, cargo-mutants, and equivalent-mutant work from
Offutt and Pan in the 1990s). Pointing mutation adequacy at verification harnesses instead of
test suites is the only part I have not been able to find prior work on, so I may be missing it
and would welcome the pointer.

Happy to open a PR against the challenge template wording if either criterion is worth pursuing.

Kyle Clouthier, Clouthier Simulation Labs