Mutation patches can apply cleanly and still not compile under -D warnings

[leynos]

Summary

Three tracked mutation patches in docs/verification/mutations/ still apply
cleanly and still pass the repository's contract test, but the tree they produce
cannot compile. They therefore contribute zero mutation evidence while
appearing healthy.

Mechanism

make kani-full gained RUSTFLAGS="… -D warnings" on 2026-09-18 (commit
2c030fd1, PR #714). Each of these patches seeds its fault by leaving a binding
or helper unused — a warning when written, and a hard compile error under
-D warnings. The mutation no longer runs at all.

This is the same mechanism that silently disabled two of roadmap 4.2.3's five
patches, repaired in PR #755 (commit 3a282018). Those two were in scope for
that plan; the three below are not, and were deliberately left alone.

Evidence (reproduced at adce1949, 2026-09-20)

Each patch was applied to a clean tree, then RUSTFLAGS="-D warnings" cargo check --lib --all-features was run:

Patch	Error
ir__from_manifest__verification__empty_rule_shape_is_rejected	error: function empty_rule_error is never used; error: function empty_rule_message is never used
ir__from_manifest__verification__multiple_rule_shape_is_rejected	error: function sort_strings is never used; error: function string_cmp is never used; error: variable does not need to be mutable
ir__cycle__verification__canonicalize_two_node_cycle_is_canonical	error: variable does not need to be mutable → src/ir/cycle_support.rs:28:9

All three: cargo check exits non-zero with could not compile netsuke-build (lib), while git apply --check exits zero.

Why the contract test misses it

tests/kani_mutation_evidence_tests.rs::every_patch_applies_cleanly only runs
git apply --check over each patch. That proves a patch applies; it does not
prove the patched tree compiles. A patch can be textually valid, apply
cleanly, and still be dead evidence.

Suggested fix

Widen every_patch_applies_cleanly to also compile each patched tree under
-D warnings. Note the cost: this runs a cargo check per patch (~18 patches
today), which is a meaningful increase in test time and interacts with build
caching, so it may deserve its own #[ignore]-gated or CI-only target rather
than the default nextest profile.

The patches themselves also need regeneration so they seed the same production
fault without introducing dead code — e.g. rebinding to _name, or moving the
"unused" helper to a #[cfg(test)]-visible position.

Impact

Three harnesses in roadmap items 4.2.1 and 4.2.2 currently have mutation
evidence that cannot be trusted. The OBL-PATCHES obligation in the
command-interpolation ExecPlan exists to stop mutation evidence rotting
silently; this is that failure mode one level deeper.

References

• Discovered while reconciling roadmap 4.2.3 for Reconcile roadmap 4.2.3 with ExecPlan completion evidence #738 (PR Reconcile roadmap 4.2.3 with ExecPlan completion evidence (#738) #755).
• Two in-scope patches repaired in commit 3a282018.
• Introduced by PR Store multi-output build edges once (#652) #714 (2c030fd1).

[leynos]

@CodeRabbit plan

[coderabbitai]

Coding Plan

Summary

• Regenerate the three rotted patches with in-place mutations that keep every helper and mut binding live, so each patched tree compiles under -D warnings while still killing its harness.
• Add a new #[ignore]-gated contract test that applies each patch, compiles the tree under -D warnings through a shared CARGO_TARGET_DIR, and reverts through a Drop guard.
• Gate the expensive test with the nested-cargo-builds nextest group, a dedicated make target, and a CI job, and document the widened gate.

Design Choices

Design Choice 1: How to gate the new per-patch compile-check test

Options Considered:

1. Run the check in the default nextest profile as a normal test, registered in the nested-cargo-builds group.
2. Add a separate #[ignore]-gated test, register it in the nested-cargo-builds group, and invoke it from a dedicated make target and a CI job.
3. Gate the check behind a custom environment variable that only CI sets.

Chosen Option: 2

Rationale: Each patch needs a real cargo check under -D warnings. There are roughly 18 patches. A sequential loop risks the 300 s per-test budget and slows local runs. The ticket flags this cost. Option 2 matches the ticket's stated preference, keeps the default profile fast, reuses the established nested-cargo-builds convention, and gives a clear invocation path for CI.

Design Choice 2: Whether to extend `every_patch_applies_cleanly` or add a new test

Options Considered:

1. Add the compile loop inside every_patch_applies_cleanly.
2. Add a new #[ignore]-gated test that reuses the existing helpers.

Chosen Option: 2

Rationale: The existing test is cheap and runs by default. The compile check is expensive and must be gated. Option 2 keeps the cheap textual check in the default profile and isolates the expensive compile check behind the #[ignore] gate.

💡 User Tips

Regenerate the plan with different choices with @coderabbitai <feedback>.

Implementation Steps

Phase 1: Regenerate the three rotted mutation patches

This phase repairs the mutation evidence. Each regenerated patch must seed the same behavioural fault as before, keep every helper referenced, keep every mut binding reassigned, and compile cleanly under -D warnings. Follow the in-place mutation idiom that the fixed cmd_interpolate patches use: swap an operator, comparator, index, or literal in place rather than deleting a statement or redirecting a call to a different helper.

Task 1: Regenerate the two `from_manifest` patches

Repair the two patches that orphan helpers in src/ir/from_manifest_support.rs.

• Regenerate docs/verification/mutations/ir__from_manifest__verification__empty_rule_shape_is_rejected.patch so it keeps empty_rule_error and empty_rule_message called. Seed the fault inside the body of empty_rule_error or empty_rule_message (for example, change the localization key or the message argument) instead of replacing the empty_rule_error(target_name) call with rule_not_found_error(target_name, "").
• Regenerate docs/verification/mutations/ir__from_manifest__verification__multiple_rule_shape_is_rejected.patch so it keeps the sort_utils::sort_strings(&mut rules) call, which keeps sort_strings, string_cmp, and the mut rules binding live. Seed the sort fault inside string_cmp or sort_strings in src/ir/sort_utils.rs (for example, reverse or flatten the comparator) rather than deleting the sort call.
• Confirm each regenerated patch targets the current production location of the moved helpers.

Task 2: Regenerate the cycle canonicalization patch

Repair the patch that orphans the mut start binding in src/ir/cycle_support.rs.

• Regenerate docs/verification/mutations/ir__cycle__verification__canonicalize_two_node_cycle_is_canonical.patch so it keeps start = index; intact, which keeps the mut start binding justified. Seed the fault by swapping the comparator in place (for example, Ordering::Less to Ordering::Greater) in find_rotation_start_by, rather than replacing the reassignment with let _ = index;.

Task 3: Validate each regenerated patch behaviourally

Confirm each regenerated patch still seeds a detectable fault and compiles.

• For each patch: run git apply --check, then apply it for real.
• Run RUSTFLAGS="-D warnings" cargo check --lib --all-features and confirm it exits zero.
• Run the focused Kani harness that owns the patch (cargo kani --harness <name>) and confirm the harness now fails on the expected assertion.
• Revert with git apply -R in the same session and confirm the harness passes.

🤖 Prompt for AI agents

Regenerate the three rotted mutation patches in `docs/verification/mutations/`
so they seed the same faults without dead code and compile under `-D warnings`.
Follow the in-place mutation idiom: swap an operator, comparator, index, or
literal in place rather than deleting a statement or redirecting a call to a
different helper.

- For `ir__from_manifest__verification__empty_rule_shape_is_rejected.patch`:
keep `empty_rule_error` and `empty_rule_message` called. Seed the fault inside
the body of `empty_rule_error` or `empty_rule_message` (for example, change the
localization key or the message argument). Do not replace the
`empty_rule_error(target_name)` call with `rule_not_found_error(target_name,
"")`.
- For `ir__from_manifest__verification__multiple_rule_shape_is_rejected.patch`:
keep the `sort_utils::sort_strings(&mut rules)` call, which keeps
`sort_strings`, `string_cmp`, and the `mut rules` binding live. Seed the sort
fault inside `string_cmp` or `sort_strings` in `src/ir/sort_utils.rs` (for
example, reverse or flatten the comparator) rather than deleting the sort call.
- Confirm each regenerated patch targets the current production location of the
moved helpers.
- For `ir__cycle__verification__canonicalize_two_node_cycle_is_canonical.patch`:
keep `start = index;` intact in `find_rotation_start_by`, which keeps the `mut
start` binding justified. Seed the fault by swapping the comparator in place
(for example, `Ordering::Less` to `Ordering::Greater`) rather than replacing the
reassignment with `let _ = index;`.

Validate each regenerated patch:

- Run `git apply --check`, then apply it for real.
- Run `RUSTFLAGS="-D warnings" cargo check --lib --all-features` and confirm
exit zero.
- Run `cargo kani --harness <name>` for the owning harness and confirm it fails
on the expected assertion.
- Revert with `git apply -R` in the same session and confirm the harness passes.

Phase 2: Add and gate a compile-check contract test

This phase closes the gap that let the rotted patches pass. Add a new contract test that applies each patch, compiles the patched tree under -D warnings, and reverts. Gate the test so it does not inflate the default test budget, and document the new gate.

Task 1: Add an apply-and-revert guard and the compile-check test

Add a new contract test to tests/kani_mutation_evidence_tests.rs that proves each patched tree compiles.

• Reuse the existing helpers MUTATIONS_DIR, manifest_dir, is_git_work_tree, and patch_stems.
• Skip the test when is_git_work_tree is false, matching every_patch_applies_cleanly, so cargo-mutants sandbox copies without .git do not false-fail.
• Add a Drop-based guard local to the test file, modelled on the existing ModeGuard/LocalizerGuard pattern. On construction it runs git apply <patch>. On drop it unconditionally reverts with git apply -R <patch> (or git checkout -- <affected paths>), so a panic mid-loop cannot leave the tree mutated.
• For each patch: construct the guard, then run cargo check --lib --all-features with RUSTFLAGS extended to include -D warnings, against a shared isolated CARGO_TARGET_DIR reused across all patches to keep builds incremental.
• Assert the check exits zero. Aggregate any non-compiling patch into a failure list with its stderr, and fail with the combined list, mirroring the rotted aggregation style of every_patch_applies_cleanly.
• Annotate the test #[ignore = "…"] with a reason that names the expensive per-patch cargo check.

Task 2: Register the test in nextest and add invocation paths

Wire the gated test into the build and CI conventions.

• Add a [[profile.default.overrides]] entry in .config/nextest.toml that filters the new test by exact name, assigns test-group = "nested-cargo-builds", and sets success-output = "immediate", matching the existing isolated-Cargo-build overrides.
• Add a Makefile target that invokes the new test through nextest with the ignored test included (for example, alongside the existing verification targets), so the compile check has a single named entry point.
• Wire the new make target into the appropriate CI lane so the gate runs on CI, following the placement of the existing verification jobs.

Task 3: Document the widened gate

Record the new behaviour and the regeneration process.

• Update the mutation-evidence section of docs/developers-guide.md to state that mutation patches must both apply cleanly and compile under -D warnings, and to name the new gated test and its make target.
• State the regeneration rule: seed faults by in-place expression edits that keep every helper referenced and every mut binding reassigned, so the patched tree compiles under -D warnings.

🤖 Prompt for AI agents

Add a new `#[ignore]`-gated contract test that closes the gap that let the
rotted patches pass, then wire it into the build, CI, and documentation.

In `tests/kani_mutation_evidence_tests.rs`:

- Reuse the existing helpers `MUTATIONS_DIR`, `manifest_dir`,
`is_git_work_tree`, and `patch_stems`.
- Skip the test when `is_git_work_tree` is false, matching
`every_patch_applies_cleanly`, so `cargo-mutants` sandbox copies without `.git`
do not false-fail.
- Add a `Drop`-based guard local to the test file, modelled on the existing
`ModeGuard`/`LocalizerGuard` pattern. On construction it runs `git apply
<patch>`. On drop it unconditionally reverts with `git apply -R <patch>` (or
`git checkout -- <affected paths>`), so a panic mid-loop cannot leave the tree
mutated.
- For each patch: construct the guard, then run `cargo check --lib
--all-features` with `RUSTFLAGS` extended to include `-D warnings`, against a
shared isolated `CARGO_TARGET_DIR` reused across all patches to keep builds
incremental.
- Assert the check exits zero. Aggregate any non-compiling patch into a failure
list with its stderr, and fail with the combined list, mirroring the `rotted`
aggregation style of `every_patch_applies_cleanly`.
- Annotate the test `#[ignore = "…"]` with a reason that names the expensive
per-patch `cargo check`.

Register and wire the test:

- Add a `[[profile.default.overrides]]` entry in `.config/nextest.toml` that
filters the new test by exact name, assigns `test-group =
"nested-cargo-builds"`, and sets `success-output = "immediate"`, matching the
existing isolated-Cargo-build overrides.
- Add a `Makefile` target that invokes the new test through nextest with the
ignored test included, alongside the existing verification targets.
- Wire the new `make` target into the appropriate CI lane, following the
placement of the existing verification jobs.

Update documentation:

- Update the mutation-evidence section of `docs/developers-guide.md` to state
that mutation patches must both apply cleanly and compile under `-D warnings`,
and to name the new gated test and its `make` target.
- State the regeneration rule: seed faults by in-place expression edits that
keep every helper referenced and every `mut` binding reassigned, so the patched
tree compiles under `-D warnings`.

Research

The src/ir/ module holds paired verification units. Each pair has a support module with shared production and Kani logic, and a sibling verification module gated behind #[cfg(kani)] that proves properties with #[kani::proof] harnesses. The three broken patches seed faults into src/ir/cycle_support.rs and src/ir/from_manifest_support.rs. The workspace [lints] in Cargo.toml denies blanket #[allow(...)], so the code keeps helpers live through dual #[cfg(kani)]/#[cfg(not(kani))] implementations instead of dead-code allowances. tests/kani_mutation_evidence_tests.rs holds three contract tests. every_patch_applies_cleanly runs git apply --check for each patch and skips when the tree is not a git work tree. make kani-full sets RUSTFLAGS="… -D warnings", which turns the dead-code warnings from the broken patches into hard compile errors. Expensive compile-style tests in this repository run under the [test-groups.nested-cargo-builds] group in .config/nextest.toml with a shared isolated CARGO_TARGET_DIR, and the per-test budget is 300 s.

---

🚀 Next Steps

🤖 All AI agent prompts combined

Task: 1

Regenerate the three rotted mutation patches in `docs/verification/mutations/`
so they seed the same faults without dead code and compile under `-D warnings`.
Follow the in-place mutation idiom: swap an operator, comparator, index, or
literal in place rather than deleting a statement or redirecting a call to a
different helper.

- For `ir__from_manifest__verification__empty_rule_shape_is_rejected.patch`:
keep `empty_rule_error` and `empty_rule_message` called. Seed the fault inside
the body of `empty_rule_error` or `empty_rule_message` (for example, change the
localization key or the message argument). Do not replace the
`empty_rule_error(target_name)` call with `rule_not_found_error(target_name,
"")`.
- For `ir__from_manifest__verification__multiple_rule_shape_is_rejected.patch`:
keep the `sort_utils::sort_strings(&mut rules)` call, which keeps
`sort_strings`, `string_cmp`, and the `mut rules` binding live. Seed the sort
fault inside `string_cmp` or `sort_strings` in `src/ir/sort_utils.rs` (for
example, reverse or flatten the comparator) rather than deleting the sort call.
- Confirm each regenerated patch targets the current production location of the
moved helpers.
- For `ir__cycle__verification__canonicalize_two_node_cycle_is_canonical.patch`:
keep `start = index;` intact in `find_rotation_start_by`, which keeps the `mut
start` binding justified. Seed the fault by swapping the comparator in place
(for example, `Ordering::Less` to `Ordering::Greater`) rather than replacing the
reassignment with `let _ = index;`.

Validate each regenerated patch:

- Run `git apply --check`, then apply it for real.
- Run `RUSTFLAGS="-D warnings" cargo check --lib --all-features` and confirm
exit zero.
- Run `cargo kani --harness <name>` for the owning harness and confirm it fails
on the expected assertion.
- Revert with `git apply -R` in the same session and confirm the harness passes.
===============================================================================

Task: 2

Add a new `#[ignore]`-gated contract test that closes the gap that let the
rotted patches pass, then wire it into the build, CI, and documentation.

In `tests/kani_mutation_evidence_tests.rs`:

- Reuse the existing helpers `MUTATIONS_DIR`, `manifest_dir`,
`is_git_work_tree`, and `patch_stems`.
- Skip the test when `is_git_work_tree` is false, matching
`every_patch_applies_cleanly`, so `cargo-mutants` sandbox copies without `.git`
do not false-fail.
- Add a `Drop`-based guard local to the test file, modelled on the existing
`ModeGuard`/`LocalizerGuard` pattern. On construction it runs `git apply
<patch>`. On drop it unconditionally reverts with `git apply -R <patch>` (or
`git checkout -- <affected paths>`), so a panic mid-loop cannot leave the tree
mutated.
- For each patch: construct the guard, then run `cargo check --lib
--all-features` with `RUSTFLAGS` extended to include `-D warnings`, against a
shared isolated `CARGO_TARGET_DIR` reused across all patches to keep builds
incremental.
- Assert the check exits zero. Aggregate any non-compiling patch into a failure
list with its stderr, and fail with the combined list, mirroring the `rotted`
aggregation style of `every_patch_applies_cleanly`.
- Annotate the test `#[ignore = "…"]` with a reason that names the expensive
per-patch `cargo check`.

Register and wire the test:

- Add a `[[profile.default.overrides]]` entry in `.config/nextest.toml` that
filters the new test by exact name, assigns `test-group =
"nested-cargo-builds"`, and sets `success-output = "immediate"`, matching the
existing isolated-Cargo-build overrides.
- Add a `Makefile` target that invokes the new test through nextest with the
ignored test included, alongside the existing verification targets.
- Wire the new `make` target into the appropriate CI lane, following the
placement of the existing verification jobs.

Update documentation:

- Update the mutation-evidence section of `docs/developers-guide.md` to state
that mutation patches must both apply cleanly and compile under `-D warnings`,
and to name the new gated test and its `make` target.
- State the regeneration rule: seed faults by in-place expression edits that
keep every helper referenced and every `mut` binding reassigned, so the patched
tree compiles under `-D warnings`.

💡 Iterate on the plan with: `@coderabbitai` <feedback>

Example Feedback
- `@coderabbitai` You can skip phase 3. Add a simple unit test case for phase 2.
- `@coderabbitai` For design choice 1 go ahead with option 3 and replan.

---