Plan: Add Kani harnesses for command interpolation (4.2.3) by leynos · Pull Request #564 · leynos/netsuke

leynos · 2026-08-16T23:41:56Z

Summary

Adds the execution plan for roadmap item 4.2.3, which brings bounded formal verification to src/ir/cmd_interpolate.rs — the command-interpolation stage that substitutes $in and $out into recipe templates and rejects commands whose shell syntax the substitution has damaged.

This pull request contains the plan only. No implementation, and the plan must be approved before implementation starts.

Execution plan: docs/execplans/4-2-3-kani-harnesses-for-command-interpolation.md

What the plan delivers

Five Kani harnesses covering all four roadmap sub-items, plus a contract test:

Obligation	Roadmap item	Harness
Sigil placeholders match exactly at token boundaries	4.2.3.a	`sigil_placeholder_match_is_exact`
Marker placeholders match on exact text, no boundary rule	4.2.3.a	`marker_token_match_is_exact`
Scanner agrees with a declarative specification	4.2.3.b	`substitute_agrees_with_spec`
Odd backtick count after substitution is rejected	4.2.3.c	`odd_backticks_are_rejected`
The guard is applied to the substituted command	4.2.3.d	`guard_applies_to_substituted_command`

The production change is deliberately tiny: a three-line substitute_chars(&[char], ..) seam plus a #[cfg(kani)] CommandBindings constructor. Nothing else.

Design points worth a reviewer's attention

The roadmap's literal 4.2.3.d wording is vacuous, and the plan says so. interpolate_command_with_bindings returns Ok only after testing shlex::split(..).is_some(), so asserting that on the Ok branch restates the branch condition and cannot fail for any implementation. The plan reformulates it as a guard-placement biconditional with a mutation patch that moves the guard onto the template. This deviates from the roadmap wording and needs acceptance.

The 256-character bound largely dissolves for 4.2.3.a. find_substitution reads at most chars[pos - 1 ..= pos + 4], so an eight-character window with a symbolic offset is complete for the sigil contract at any string length, not merely bounded. Where a genuine bound remains (the string-level and guard harnesses) the plan measures it in a spike and hands the residual range to Proptest, following the precedent ADR-004 set for 4.2.1.

Nothing currently validates the mutation-evidence patches, and there are twelve patches for thirteen harnesses. The plan adds tests/mutation_evidence_tests.rs to make test. The missing patch belongs to 4.2.2's adapter harness and is raised rather than absorbed here.

Two latent behaviours are pinned, not changed. $$in substitutes (yielding $<ins>) even though $$ is Ninja's escape for a literal dollar, and x__NETSUKE_INS_PLACEHOLDER__ is rewritten because marker forms carry no boundary rule. Both may be defects; both are out of scope under the no-behaviour-change constraint. The plan asks for a classification.

Decisions requiring maintainer acceptance

The 4.2.3.d reformulation above.
Permitting harness-local oracles for side conditions and a declarative specification for the scanner. Without them, odd_backticks_are_rejected would compare has_unmatched_backticks against itself and its mutation would flip both sides.
Accepting a string-level bound below the roadmap's 256/8, if the feasibility spike shows one.

Review process

Revision 1 was rewritten after a six-lens design review. The review withdrew a proposed fixed-capacity scanning kernel (it would have introduced a capacity bound into unbounded security-sensitive code), corrected a mutation patch whose sign was backwards, found that the original alphabet made try_match_token structurally unreachable, and replaced guessed budgets with measured ones. The Revision note at the foot of the plan records the full list.

Validation

make markdownlint passes. No code changes, so the Rust gates are unaffected.

References

Roadmap item: docs/roadmap.md §4.2.3
Design basis: docs/formal-verification-methods-in-netsuke.md §Kani for command interpolation
Governing decision: docs/adr-004-bound-kani-ir-harnesses-to-small-n.md
Lody session: https://lody.ai/leynos/sessions/ac36bbe2-72c0-44e8-8d59-aaf79d5e8205

🤖 Generated with Claude Code

Summary by Sourcery

Approve a staged plan for adding bounded formal verification to command interpolation without changing production behaviour.

Enhancements:

Define an execution plan for bounded Kani verification of command interpolation, including placeholder matching, scanner behaviour, substituted-command validation, and guard placement.
Add a planned mutation-evidence contract test to ensure verification harnesses remain backed by effective mutation patches.
Specify measured-bound and Proptest hand-off criteria for cases that exceed practical Kani limits while preserving existing command-interpolation behaviour.

Documentation:

Add the roadmap 4.2.3 execution plan covering implementation stages, verification obligations, acceptance criteria, risks, and maintainer decisions.

coderabbitai · 2026-08-16T23:42:08Z

Important

Draft PR not reviewed

Draft PRs are not automatically reviewed by default.

Trigger a manual review

To automatically review draft PRs, update your CodeRabbit configuration:

reviews:
  auto_review:
    drafts: true

Warning

Your free Security trial is over. An organization admin can activate billing to continue.

_{Comment @coderabbitai help to get the list of available commands.}

sourcery-ai · 2026-08-16T23:42:18Z

Reviewer's Guide

Execution-plan-only PR adding a detailed ExecPlan document for Kani harnesses around command interpolation, plus specifying a minimal future production seam and a cfg(kani) helper; no Rust code changes yet but the plan itself is dense with design decisions, verification obligations, and process steps that need conceptual review.

File-Level Changes

Change	Details	Files
Add a comprehensive execution plan document for roadmap item 4.2.3 covering Kani harnesses, bounds, obligations, risks, and stepwise milestones for command interpolation verification.	Introduce ExecPlan structure with sections for context, constraints, tolerances, risks, verification plan, milestones, interfaces, and validation. Describe existing command interpolation behaviour in detail, including placeholder rules, backtick handling, and current tests. Define five Kani harness obligations (sigil matching, marker matching, scanner spec agreement, odd backtick rejection, guard placement) plus a mutation-patch contract test. Lay out concrete implementation stages (EP-M0–EP-M6) with red-green-refactor guidance and CI/resource considerations. Document surprises, decisions, and required maintainer-acceptance deviations from roadmap wording.	`docs/execplans/4-2-3-kani-harnesses-for-command-interpolation.md`
Specify the intended minimal future production code changes needed to support Kani harnesses without altering behaviour.	Plan to split substitute(&str, ..) into a substitute_chars(&[char], ..) seam to avoid symbolic UTF-8 overhead. Plan to add a #[cfg(kani)] CommandBindings::from_parts constructor for proof-only arbitrary bindings. Plan to move existing cmd_interpolate tests into a sibling *_tests.rs module to keep file size under the 400-line cap.	`docs/execplans/4-2-3-kani-harnesses-for-command-interpolation.md`

Tips and commands

Interacting with Sourcery

Trigger a new review: Comment @sourcery-ai review on the pull request.
Continue discussions: Reply directly to Sourcery's review comments.
Generate a GitHub issue from a review comment: Ask Sourcery to create an
issue from a review comment by replying to it. You can also reply to a
review comment with @sourcery-ai issue to create an issue from it.
Generate a pull request title: Write @sourcery-ai anywhere in the pull
request title to generate a title at any time. You can also comment
@sourcery-ai title on the pull request to (re-)generate the title at any time.
Generate a pull request summary: Write @sourcery-ai summary anywhere in
the pull request body to generate a PR summary at any time exactly where you
want it. You can also comment @sourcery-ai summary on the pull request to
(re-)generate the summary at any time.
Generate reviewer's guide: Comment @sourcery-ai guide on the pull
request to (re-)generate the reviewer's guide at any time.
Resolve all Sourcery comments: Comment @sourcery-ai resolve on the
pull request to resolve all Sourcery comments. Useful if you've already
addressed all the comments and don't want to see them anymore.
Dismiss all Sourcery reviews: Comment @sourcery-ai dismiss on the pull
request to dismiss all existing Sourcery reviews. Especially useful if you
want to start fresh with a new review - don't forget to comment
@sourcery-ai review to trigger a new review!

Customizing Your Experience

Access your dashboard to:

Enable or disable review features such as the Sourcery-generated pull request
summary, the reviewer's guide, and others.
Change the review language.
Add, remove or edit custom review instructions.
Adjust other review settings.

Getting Help

Contact our support team for questions or feedback.
Visit our documentation for detailed guides and information.
Keep in touch with the Sourcery team by following us on X/Twitter, LinkedIn or GitHub.

Add the execution plan for roadmap item 4.2.3, which adds bounded model-checking coverage to `src/ir/cmd_interpolate.rs`. The plan covers all four roadmap sub-items: - `$in` and `$out` rewrite only at valid token boundaries - backtick-delimited regions are preserved - unmatched backticks are rejected - successful results satisfy the current `shlex` guard Key design points: - The production change is a three-line `substitute_chars(&[char], ..)` seam plus a `cfg(kani)` `CommandBindings` constructor. Symbolic UTF-8 across the `&str` boundary is the dominant solver cost. - `RM-4.2.3.a` is discharged by a window-completeness argument rather than a large bound: the sigil decision reads at most six characters of context, so an eight-character window with a symbolic offset covers strings of any length. - `RM-4.2.3.d` is reformulated as a guard-placement biconditional. The literal wording restates the branch condition and cannot fail. - A new contract test validates the mutation-evidence patches, which no gate currently checks. Three decisions require maintainer acceptance before their milestones start; they are marked in the Decision log.

Rebase onto `origin/main` at 7e5c267 ("Add target descriptions and netsuke help targets") shifted line numbers in several documents the plan cites. Refresh references into `docs/roadmap.md`, `docs/developers-guide.md`, `Cargo.toml`, and `src/ir/from_manifest.rs`, and add a note that such numbers drift, so an anchor should be verified by heading or symbol name before the number is trusted. That commit introduces nothing this branch must adopt. Its only change under `src/ir/` is a comment recording that target descriptions are discovery metadata and never take part in recipe resolution, which reinforces the boundary this plan verifies. The assessment is recorded in the Decision log.

Both observations recorded in `Surprises & discoveries` now have tracking issues, so the trail survives beyond this branch. - #585: nothing validates the Kani mutation-evidence patches, and the 4.2.2 adapter harness has none. - #586: ExecPlan status fields are stale and use an inconsistent vocabulary.

All three decisions marked "requires maintainer acceptance" are ratified: the 4.2.3.d reformulation as a guard-placement biconditional, harness-local oracles, and a string-level bound below the roadmap's stated 256/8. The bound decision was accepted in advance, so EP-M0 no longer sets the plan to BLOCKED on a string-level shortfall. It records the achieved bound, the residual gap, and the Proptest hand-off, then continues. The mechanical stop for a sigil-shape shortfall below an 8-character window is unchanged, since that would undermine the plan's premise rather than narrow its reach. Also correct the planning dates from 2026-08-17 to 2026-08-24. The plan stays DRAFT pending approval to begin implementation.

Rebase onto `origin/main` at aa93ef8 brought nine commits, including serial dependency ordering, config-load caching, a Windows CI job, and a large restructuring of the developers' guide. Nothing this plan depends on changed. A semantic diff over `src/ir` reports a new `DependencyOrder` enum and one added `BuildEdge` field; `cmd_interpolate` does not appear. The harness count is still thirteen, the patch count still twelve, and `kani-smoke` keeps its shape, cache key, and 20-minute cap. Convert Markdown citations from line numbers to section headings. Two consecutive rebases have now moved them, and the numbers cannot be kept true. Line numbers are retained only for code, where `src/ir/cmd_interpolate.rs` has been stable throughout. Record two operational notes in Risks: `main` has edited the Makefile, so the Kani cache is cold and the next timing will be pessimistic; and a merge-gating Windows job now runs alongside `kani-smoke`.

codescene-access

No quality gates enabled for this code.