Kani harnesses for manifest-to-IR safety checks (4.2.1)

[lodyai]

Summary

• Draft an approval-gated execution plan for roadmap item 4.2.1 ("Add Kani harnesses for manifest-to-IR safety checks"). The plan lives at docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md.
• Place harnesses inline as #[cfg(kani)] mod verification blocks inside src/ir/from_manifest.rs and src/ir/cycle.rs, matching Kani's own layout guidance and avoiding any widening of the netsuke::ir public API.
• Cover the four roadmap sub-properties (duplicate-output rejection, rule-error selection, self-edge plus 2-3-node cycle rejection, missing-deps-do-not-create-false-cycles) with six harnesses, including a parameterised symbolic harness for the rule-error trio.
• Reconcile the roadmap's "up to 10 nodes, depth limit 20 edges" target with Kani's current cost on real HashMap types by bounding harnesses to 1-3 nodes and treating the Proptest layer scheduled under 4.3.1 as the closing commitment for the larger-N property. This is the chief approval-gated decision and will be captured in a new ADR-004 alongside two rejected alternatives (narrow leaf-function harnesses; a verification-only collection port).

Plan highlights

The plan was stress-tested with a Logisphere community-of-experts pre-mortem and revised in response:

• Stage B scaffold switched from kani::assert(false) to a trivially true assertion plus a cargo kani --list discovery check, avoiding training the wrong reflex for "intentional failure".
• ActionHasher::hash stubbing reframed as a contract decision (it changes the property being proven), not a budget tweak.
• Tiered make kani-ir / make kani-full targets introduced pre-emptively so 4.2.2 and 4.2.3 do not force a post-hoc split.
• Mutation evidence stored as literal patch files under docs/verification/mutations/<harness>.patch so it survives future production refactors.
• Cumulative solver-budget estimate (20 harnesses at 30-120s by end of 4.2) added to Tolerances.

The plan opens five Stage-A approval questions: bound reconciliation, the preferred ActionHasher escape hatch, the tiered Make-target split, the default unwind value, and the new docs/verification/mutations/ sub-directory.

Test plan

• Stage A: user reviews this draft, resolves the open questions, and explicitly approves the plan.
• Stage B: scaffold harness modules pass cargo kani --list discovery, then make kani-full, then the ordinary make check-fmt/make lint/make test/make markdownlint/make nixie gates.
• Stage C: each of the four sub-properties commits separately; cargo kani --harness ... runs for each new harness; mutation patch files validate falsification power.
• Stage D: developers' guide harness inventory, formal-verification design footnote, and ADR-004 land together.
• Stage E: coderabbit review --agent and the full local gate set pass cleanly.
• Stage F: roadmap 4.2.1 marked done, branch pushed, this draft PR updated with implementation summary.

References

• Roadmap: docs/roadmap.md §4.2.1.
• Design: docs/formal-verification-methods-in-netsuke.md §Kani for the IR core.
• Prior execplans in the same phase: docs/execplans/4-1-{1,2,3}-*.md.
• Lody session: https://lody.ai/leynos/sessions/8e1f0980-edb8-43a0-aacc-bad04b2e9b33

Summary by Sourcery

Add initial Kani verification harnesses and supporting infrastructure for manifest-to-IR safety checks, while tightening error construction helpers and documenting the small-N verification bound.

New Features:

• Introduce Kani-based verification harnesses for duplicate-output and rule-selection IR safety properties in the manifest-to-IR path.
• Add a Kani harness scaffold module for IR cycle detection to enable future proof development.

Enhancements:

• Refactor duplicate-output and rule-selection error construction into reusable helpers that support both production code and Kani harnesses without widening the IR public API.
• Adjust IR error message construction and duplicate-output handling to support Kani builds by avoiding localization argument formatting under cfg(kani).
• Document a Kani harness inventory in the developers' guide and record the small-N Kani bound with Proptest hand-off in a new ADR-004.
• Add a dedicated Kani IR make target and configure compiler lints to recognise cfg(kani) along with a default Kani unwind setting.
• Slightly relax a debug assertion in hex encoding to satisfy Kani and Clippy simultaneously.

Build:

• Configure Kani verifier metadata in Cargo.toml with a default unwind bound and enable check-cfg for the kani configuration flag.

Documentation:

• Add a detailed execution plan for roadmap item 4.2.1 describing Kani harness introduction, bounds, and workflows.
• Record Architectural Decision Record 004 defining the small-N Kani harness strategy and Proptest hand-off.
• Extend the developers' guide with a Kani harness inventory table and guidance on harness layout and cfg(kani) usage.
• Update the documentation contents index to include ADR-004.

Tests:

• Add new Kani proof harnesses for duplicate output rejection and rule-selection error shapes in the manifest-to-IR code path, plus a scaffold harness for cycle detection.

[coderabbitai]

Note

Reviews paused

It looks like this branch is under active development. To avoid overwhelming you with review comments due to an influx of new commits, CodeRabbit has automatically paused this review. You can configure this behavior by changing the reviews.auto_review.auto_pause_after_reviewed_commits setting.

Use the following commands to manage reviews:

• @coderabbitai resume to resume automatic reviews.
• @coderabbitai review to trigger a single review.

Use the checkboxes below for quick actions:

• ▶️ Resume reviews
• 🔍 Trigger review

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Pro Plus

Run ID: 9163fc55-747d-4446-a15e-5c097b94a5e1

📥 Commits

Reviewing files that changed from the base of the PR and between 579ba4d and 50e6b40.

📒 Files selected for processing (1)

• src/ir/cycle.rs

---

Overview

This pull request introduces Kani-based formal verification harnesses for manifest-to-IR safety checks, fulfilling roadmap item 4.2.1. The implementation includes an approval-gated execution plan, architectural decision record, six Kani harnesses, supporting infrastructure, and code health refactorings.

Key Documents

Execution Plan (docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md): A 1,266-line living document detailing the staged approval gates (A–F), scope boundaries, operational tolerances, mutation-discipline requirements, and acceptance criteria for Kani harness integration. It records five Stage-A open questions, the planned harness properties (duplicate-output rejection, rule-selection error variants, cycle detection for bounded self/short cycles, and missing-dependency non-cycling behaviour), and the approved decision to bound Kani coverage to small N with a future Proptest hand-off.

ADR-004 (docs/adr-004-bound-kani-ir-harnesses-to-small-n.md): Decision record reconciling the roadmap's "up to 10 nodes, depth 20 edges" with Kani's budget constraints by bounding harnesses to 1–3 nodes. The ADR establishes constraints on harness design (keep make kani-full runnable locally, avoid verification-only public API changes, keep verification code private to IR modules, keep proofs close to the IR being tested), specifies harness scope and placement (fixed minimal manifests, cycle harnesses for self/two-node cycles), and documents what is explicitly not proven under this scheme (full manifest lowering, rendered output formatting, full report-building, larger-N coverage).

Verification Harnesses

Manifest-to-IR harnesses (src/ir/from_manifest_verification.rs, 119 lines): Four #[kani::proof] proofs validating error behaviours with symbolic reasoning: duplicate_output_always_rejected verifies duplicate-output detection, whilst empty_rule_shape_is_rejected, multiple_rule_shape_is_rejected, and missing_rule_shape_is_rejected validate rule-selector error shapes returned by resolve_rule.

Cycle-detection harnesses (src/ir/cycle_verification.rs, 95 lines): Five proofs covering self-dependency cycles, two-node cycles (insertion-order invariant), and missing-dependency non-cycling behaviour. All harnesses are bounded with #[kani::unwind(...)] (5–6 iterations).

Core Implementation

Support infrastructure: New src/ir/from_manifest_support.rs (353 lines) centralises manifest-lowering helpers: register_action, duplicate_output_error, insert_edge_for_outputs, rule resolution, and deterministic path/string sorting. Helper refactorings in src/ir/cycle.rs (find_rotation_start, rotate_cycle) and cycle traversal extraction (back_edge_result, visit_known_edge) reduce complexity and address code-health Bumpy Road issues.

Kani-specific abstractions: New src/ir/graph_kani_map.rs (174 lines) provides IrHashMap<K, V>, a bounded deterministic map for Kani (capacity 4) with IrMapKeyEq trait supporting byte-level path equality. src/ir/graph.rs abstracts the IR graph map behind a conditional IrHashMap type (standard HashMap for production, bounded map for Kani). src/ir/cycle.rs refactored to support dual traversal modes: a normal "Path" mode returning extracted cycles and a Kani-only "Presence" mode returning a boolean.

Cycle-detection refactoring: Public analyse now accepts &IrHashMap<Utf8PathBuf, BuildEdge>. Two-mode cycle detection (CycleSearch enum) allows Kani harnesses to reuse traversal logic without the full report-building path. Missing-dependency recording is mode-aware, returning early in "Presence" mode.

Configuration and Build

Cargo.toml: Added package.metadata.kani.flags.default-unwind = "6", [lints.rust].unexpected_cfgs allowing cfg(kani), and dev-dependency trybuild = "1.0.116".

Makefile: New kani-ir target aliases kani-full, enabling make kani-ir / make kani-full tiered targets.

Tests: New UI/compile-time tests (tests/kani_cfg_ui_tests.rs, tests/ui/cfg_kani_policy_pass.rs, tests/ui/cfg_kani_compile_pass.rs, tests/ui/unknown_cfg_compile_fail.rs, 80+ lines total) enforce cfg(kani) contract via trybuild and rustc --check-cfg.

Code Health Refactorings

Bumpy Road reduction in CycleDetector::visit and canonicalize_cycle through EXTRACT FUNCTION refactorings (back_edge_result, visit_known_edge, find_rotation_start, rotate_cycle).

Deduplication: Replaced duplicated sort_strings / sort_paths with a generic insertion_sort_by<T, F> helper; extracted shared assert_no_cycle assertion helper; refactored IrHashMap::key_at to delegate to entry_at; reduced visit_known_edge parameter count via BuildEdge parameter object.

String-argument biomarker mitigation from CodeScene review: deferred type conversions to error construction boundaries (replacing target_name: &str with target_paths: &[Utf8PathBuf] in error helpers; deferring get_target_display_name calls), centralised Kani-safe message logic via add_arg helper, changed register_action to accept description: Option<&str>.

Documentation

Developers' guide (docs/developers-guide.md): New "Kani harness inventory" subsection documents harness module locations, CFG contract requirements, and a table of six harnesses with owning modules, asserted properties, and unwind bounds. New "Kani cfg compile-time checks" subsection details UI/trybuild and rustc validation for the cfg(kani) policy. Updated "Formal-verification tooling" section with refined make target documentation.

Design diagram updates (docs/netsuke-design.md, docs/rstest-bdd-v0-5-0-migration-guide.md): Mermaid flowchart formatting and structure updates using explicit <br/> line breaks and extended configuration-discovery checks.

Mutation Evidence

Six patch files under docs/verification/mutations/ document boundary-condition mutations: ir__cycle__verification__*.patch (5 patches) and ir__from_manifest__verification__*.patch (4 patches) record targeted mutation kills verifying harness effectiveness.

Minor Changes

• Updated src/ast.rs to use deterministic BuildHasherDefault<DefaultHasher> for Vars under cfg(kani).
• Updated src/stdlib/path/hash_utils.rs to discard formatting errors in debug_assert! to satisfy Kani's determinism constraints.
• Updated docs/contents.md to reference ADR-004.

Walkthrough

This pull request establishes Kani bounded verification for IR safety properties. It introduces cfg(kani) build policy with compile-time contract tests, defines IrHashMap as abstraction over HashMap and a bounded array-backed map, refactors manifest-to-IR and cycle-detection logic into support modules, implements nine verification harnesses across both domains with mutation evidence, and documents verification strategy via ADR-004 and ExecPlan 4-2-1.

Changes

Kani IR Safety Harnesses and Refactored Verification Infrastructure

Layer / File(s)	Summary
Kani build policy and Cargo/Make configuration Cargo.toml, Makefile	Adds package.metadata.kani.flags with default-unwind = "6", introduces [lints.rust].unexpected_cfgs allowing cfg(kani), and includes trybuild dev-dependency. Makefile adds kani-ir target as alias to kani-full.
cfg(kani) compile-time contract validation tests/kani_cfg_ui_tests.rs, tests/ui/cfg_kani_*.rs	Trybuild test validates cfg(kani) policy markers in Cargo.toml and Makefile. Two rustc-based tests enforce cfg(kani) acceptance and reject unknown cfg names. UI snippets demonstrate compile-pass and compile-fail behaviour for the cfg contract.
IrHashMap type abstraction and bounded implementation src/ir/graph.rs, src/ir/graph_kani_map.rs, src/ast.rs, src/stdlib/path/hash_utils.rs	graph.rs introduces public IrHashMap as HashMap alias for non-Kani, custom bounded 4-entry map for Kani cfg; BuildGraph fields switch to IrHashMap<K, V>. graph_kani_map.rs implements deterministic insertion-order map with IrMapKeyEq trait for String and Utf8PathBuf. ast.Vars uses conditional hasher under cfg(kani).
Manifest-to-IR support extraction and lowering refactoring src/ir/from_manifest.rs, src/ir/from_manifest_support.rs	New from_manifest_support.rs extracts action registration, duplicate/rule-resolution helpers, and deterministic sorting; from_manifest.rs switches internal maps to IrHashMap, uses support module functions, passes template description by reference, and wires cfg(kani) verification module.
Manifest error-shape proofs and mutation evidence src/ir/from_manifest_verification.rs, docs/verification/mutations/ir__from_manifest__*, docs/developers-guide.md	Four Kani harnesses prove duplicate-output rejection and rule-selector error shapes (empty, multiple, missing rules). Symbolic helpers generate test inputs. Mutation patches under docs/verification/mutations/ document proof boundaries for logic gates and error constructors. Developers-guide documents harness properties and unwind bounds.
Cycle detection mode refactoring and IrHashMap integration src/ir/cycle.rs	Introduces CycleSearch (Path vs Presence modes) and CycleVisitResult enums; analyse accepts IrHashMap<Utf8PathBuf, BuildEdge>; adds Kani-only contains_cycle boolean entrypoint; records missing dependencies only in Path mode; refactors traversal, canonicalisation helpers, and test assertions.
Cycle detection bounded proofs and mutation evidence src/ir/cycle_verification.rs, docs/verification/mutations/ir__cycle__*	Five Kani harnesses cover self-dependencies, two-node cycles (both insertion orders), and missing dependencies (direct/transitive). Shared assert_no_cycle helper and graph constructors build test graphs. Mutation patches document proof boundaries for search-mode returns and visit recursion logic.
ADR-004: bounded harness strategy decision docs/adr-004-bound-kani-ir-harnesses-to-small-n.md, docs/contents.md	Records decision to use small bounded Kani harnesses with Proptest hand-off for larger graphs; rejects encoding roadmap bounds in Kani and verification-only public APIs; establishes proof-boundary constraints, private cfg(kani) IrHashMap compatibility layer, and known coverage limitations.
ExecPlan 4-2-1: staged implementation roadmap docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md	Specifies approval-gated workflow, strict scope boundaries (no public IR API changes, cfg(kani) code private to modules), operational tolerances (solver runtime, unwind budget), mutation discipline with replayable patch files, and detailed plan-of-work across stages A–F from scaffold through validation.
Developer guide updates and diagram formatting docs/developers-guide.md, docs/netsuke-design.md, docs/rstest-bdd-v0-5-0-migration-guide.md	developers-guide documents make targets, cfg(kani) harness contract, harness inventory table (module paths, asserted properties, unwind bounds, verification focus), and IrHashMap compatibility layer. Mermaid diagrams in netsuke-design and migration guide reformatted to use inline <br/> for readability.

Possibly related PRs

• leynos/netsuke#305: Both PRs extend Kani workflow integration in the Makefile—this PR adds kani-ir alias to existing kani-full target.
• leynos/netsuke#163: Both PRs refactor cycle detection in src/ir/cycle.rs, with this PR introducing mode-based Path/Presence traversal.
• leynos/netsuke#315: Both PRs modify cycle-detection implementation, with this PR adding IrHashMap integration and mode-based behaviour.

Suggested reviewers

• codescene-delta-analysis

---

🧪 Proof harnesses mark the ground,
Error shapes are now unwound,
From manifest through IR we trace,
Small bounds keep the solver's pace,
Proptest waits for larger space. 🚀

✨ Finishing Touches

📝 Generate docstrings

• Create stacked PR
• Commit on current branch

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch 4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks

[sourcery-ai]

Reviewer's Guide

Adds Kani verification scaffolding and initial IR harnesses for manifest-to-IR safety checks, refactors IR error construction to be more testable under Kani, documents the harness strategy and bounds (including ADR-004), and wires project metadata and Make targets to support Kani while keeping the public IR API unchanged.

File-Level Changes

Change	Details	Files
Refactor IR error and duplicate-output handling to support narrow Kani harnesses without widening the public IR API.	Change resolve_rule to take target paths instead of a precomputed display name and introduce helper constructors for EmptyRule, MultipleRules, and RuleNotFound errors. Introduce duplicate_output_error and duplicate_output_error_from_paths helpers and change duplicate detection to return IrGenError directly rather than building the error at call site. Adjust find_duplicates to return Utf8PathBufs instead of Strings and split message construction into duplicate_outputs_message with different cfg(kani) and non-kani behaviours.	src/ir/from_manifest.rs
Introduce Kani harness modules and verification-specific helper files for manifest-to-IR and cycle detection, focused on duplicate outputs and rule-selection errors.	Add #[cfg(kani)] verification modules in from_manifest and cycle, delegating harness bodies to sibling *_verification.rs files to keep production files under line limits. Implement Kani proofs duplicate_output_always_rejected and rule_selection_errors_match_rule_shape that exercise private IR error constructors with symbolic inputs. Add placeholder Kani scaffold harness for cycle verification to establish layout and wiring without yet proving cycle properties.	src/ir/from_manifest.rs src/ir/cycle.rs src/ir/from_manifest_verification.rs src/ir/cycle_verification.rs
Configure project-level Kani metadata, cfg(kani) linting, and Make targets to integrate Kani into the workflow without affecting standard builds.	Add [package.metadata.kani.flags] with default-unwind = "6" so Kani runs with a bounded unwind by default. Enable unexpected_cfgs lint with check-cfg = ["cfg(kani)"] so cfg(kani) uses are recognised and warned on if mis-specified. Add kani-ir Make target as an alias for kani-full and extend PHONY targets list accordingly.	Cargo.toml Makefile
Document the Kani IR harness strategy, bounds, and decisions, including an execution plan and a new ADR.	Add an extensive execplan describing roadmap item 4.2.1, Kani harness design, bounds reconciliation, risks, and staged implementation. Document Kani harness inventory in the developers guide, including harness names, modules, properties, bounds, and notes about message-key-only checks under cfg(kani). Introduce ADR-004 capturing the decision to bound Kani IR harnesses to small N with Proptest hand-off and index it from docs/contents.md.	docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md docs/developers-guide.md docs/adr-004-bound-kani-ir-harnesses-to-small-n.md docs/contents.md
Tidy a hash formatting debug path to satisfy Kani and Clippy simultaneously.	Change encode_hex debug_assert to drop the error value explicitly and use a static message, avoiding unused variable and formatting-related lint noise under Kani builds.	src/stdlib/path/hash_utils.rs

---

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.

[leynos]

@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response.

src/ir/from_manifest.rs

Comment on file

                        .with_arg("outputs", format!("{dups:?}")),
                    outputs: dups,
                });
            if let Some(error) = duplicate_output_error(&outputs, targets) {

❌ New issue: String Heavy Function Arguments
In this module, 57.1% of all arguments to its 20 functions are strings. The threshold for string arguments is 39.0%

[leynos]

@coderabbitai Has this now been resolved in the latest commit?

Use codegraph analysis to determine your answer.

If this comment is now resolved, please mark it as such using the API. Otherwise, please provide an AI agent prompt for the remaining work to be done to address this comment.

## Overall Comments
- The `*_message` helpers now have separate `cfg(kani)` and non-`cfg(kani)` implementations; consider adding a brief comment or consolidating the key selection so it’s harder for the two branches to drift if the message keys or arguments change in future.
- The new error-construction helpers (`empty_rule_error`, `multiple_rules_error`, `rule_not_found_error`, and their `*_message` counterparts) repeat similar patterns for computing `target_name` and building `LocalizedMessage`; you could reduce duplication by factoring out small shared helpers for the common pieces.

## Individual Comments

### Comment 1
<location path="docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md" line_range="1247-1250" />
<code_context>
+## Revision note
+
+- 2026-06-07: Initial draft.
+- 2026-06-07: Logisphere community-of-experts review folded in.
+  Stage B scaffold switched from `kani::assert(false)` to a trivially true
+  assertion plus `cargo kani --list` discovery check. `ActionHasher::hash`
</code_context>
<issue_to_address>
**nitpick (typo):** Fix the stray space in 'Duplicate- output'.

In the revision note, remove the space after the hyphen in 'Duplicate- output'; use 'Duplicate-output' or 'duplicate output' to avoid the awkward break.

```suggestion
  `make kani-ir` alias added pre-emptively. Mutation evidence stored as literal
  patch files under `docs/verification/mutations/`. Rule-error harness trio
  collapsed into one parameterised symbolic harness. duplicate output
  assertion restated in input-shape terms. 3-node cycle fallback escalated as a
```
</issue_to_address>

### Comment 2
<location path="docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md" line_range="928-929" />
<code_context>
+   bound-reduction risk in ADR-004 and in the corresponding roadmap entry, not
+   as a sibling concern.
+
+4. **Missing dependencies do not create false cycles** (same
+   module). Two harnesses: one with a single target whose dependency is absent
+   from the target map, and one with a two- target chain where the deeper
+   dependency is absent. Each asserts `report.cycle.is_none()` and that
</code_context>
<issue_to_address>
**nitpick (typo):** Correct spacing in 'two- target chain'.

In the missing-dependency harness description, remove the extra space so it reads either 'two-target chain' or 'two target chain' for correct spacing.

```suggestion
   module). Two harnesses: one with a single target whose dependency is absent
   from the target map, and one with a two-target chain where the deeper
```
</issue_to_address>

### Comment 3
<location path="src/ir/from_manifest.rs" line_range="248" />
<code_context>
 fn resolve_rule(
     rule: &StringOrList,
     rule_map: &HashMap<String, Arc<Rule>>,
</code_context>
<issue_to_address>
**issue (complexity):** Consider simplifying the new Kani and error-handling changes by reusing target_name, centralizing cfg-specific message logic, and constructing errors in-place instead of via multiple helper layers.

You can keep the new functionality (Kani support, path-based duplicates, borrowed descriptions) while reducing the added complexity by centralizing the Kani-specific behavior and avoiding extra error helpers.

### 1. Keep `resolve_rule` simple: pass `target_name` again

Compute `target_name` once at the call site and pass it into `resolve_rule`, as before. Let the Kani/`with_arg` differences live in small shared helpers instead of new error-specific functions.

```rust
// caller
let target_name = get_target_display_name(&outputs);
let tmpl = resolve_rule(rule, rule_map, &target_name)?;

// callee
fn resolve_rule(
    rule: &StringOrList,
    rule_map: &HashMap<String, Arc<Rule>>,
    target_name: &str,
) -> Result<Arc<Rule>, IrGenError> {
    extract_single(rule).map_or_else(
        || {
            let mut rules = to_string_vec(rule);
            if rules.is_empty() {
                Err(IrGenError::EmptyRule {
                    target_name: target_name.to_owned(),
                    message: empty_rule_message(target_name),
                })
            } else {
                rules.sort();
                Err(IrGenError::MultipleRules {
                    target_name: target_name.to_owned(),
                    rules,
                    message: multiple_rules_message(target_name, &rules),
                })
            }
        },
        |name| {
            rule_map
                .get(name)
                .cloned()
                .ok_or_else(|| IrGenError::RuleNotFound {
                    target_name: target_name.to_owned(),
                    rule_name: name.to_owned(),
                    message: rule_not_found_message(target_name, name),
                })
        },
    )
}
```

### 2. Centralize `#[cfg(kani)]` behavior for messages

Instead of `empty_rule_message` vs `multiple_rules_message` vs `rule_not_found_message` each having their own cfg-split implementations, extract a couple of generic helpers that hide `with_arg` from Kani entirely:

```rust
#[cfg(not(kani))]
fn add_arg(
    msg: localization::LocalizedMessage,
    key: &'static str,
    val: impl ToString,
) -> localization::LocalizedMessage {
    msg.with_arg(key, val.to_string())
}

#[cfg(kani)]
fn add_arg(
    msg: localization::LocalizedMessage,
    _key: &'static str,
    _val: impl ToString,
) -> localization::LocalizedMessage {
    msg
}
```

Then message builders can be shared and small:

```rust
fn empty_rule_message(target_name: &str) -> localization::LocalizedMessage {
    add_arg(localization::message(keys::IR_EMPTY_RULE), "target", target_name)
}

fn multiple_rules_message(
    target_name: &str,
    rules: &[String],
) -> localization::LocalizedMessage {
    let msg = localization::message(keys::IR_MULTIPLE_RULES);
    let msg = add_arg(msg, "target", target_name);
    add_arg(msg, "rules", format!("{rules:?}"))
}

fn rule_not_found_message(
    target_name: &str,
    rule_name: &str,
) -> localization::LocalizedMessage {
    let msg = localization::message(keys::IR_RULE_NOT_FOUND);
    let msg = add_arg(msg, "target", target_name);
    add_arg(msg, "rule", rule_name)
}
```

This removes all per-error `#[cfg(kani)]` functions while still keeping Kani-safe messages.

### 3. Simplify duplicate-output error pipeline

You can keep `find_duplicates` working on `Utf8PathBuf` (to satisfy Kani / path requirements) but collapse the extra layers and keep error construction co-located at the call site.

```rust
fn find_duplicates(
    outputs: &[Utf8PathBuf],
    targets: &HashMap<Utf8PathBuf, BuildEdge>,
) -> Option<Vec<Utf8PathBuf>> {
    let mut dups: Vec<Utf8PathBuf> = outputs
        .iter()
        .filter(|o| targets.contains_key(*o))
        .cloned()
        .collect();
    if dups.is_empty() {
        None
    } else {
        dups.sort();
        Some(dups)
    }
}
```

At the call site, build the error directly with a shared message helper:

```rust
if let Some(dups) = find_duplicates(&outputs, targets) {
    return Err(IrGenError::DuplicateOutput {
        message: duplicate_outputs_message(&dups),
        outputs: dups.iter().map(|p| p.as_str().to_owned()).collect(),
    });
}
```

And again hide cfg differences in a single helper:

```rust
#[cfg(not(kani))]
fn duplicate_outputs_message(dups: &[Utf8PathBuf]) -> localization::LocalizedMessage {
    add_arg(
        localization::message(keys::IR_DUPLICATE_OUTPUTS),
        "outputs",
        format!("{dups:?}"),
    )
}

#[cfg(kani)]
fn duplicate_outputs_message(_dups: &[Utf8PathBuf]) -> localization::LocalizedMessage {
    localization::message(keys::IR_DUPLICATE_OUTPUTS)
}
```

This keeps:

- Kani-safe messages (no `.with_arg` in Kani),
- path-based duplicates and structured errors,
- and the new `register_action` borrowing behavior,

while removing the extra `*_error(...)` → `*_message(...)` → `get_target_display_name(...)` chains and per-error cfg duplication.
</issue_to_address>

### Comment 4
<location path="docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md" line_range="1170" />
<code_context>
+
+These questions must be resolved at Stage A before implementation begins:
+
+1. **Bound reconciliation.** Do you accept Kani harnesses bounded to
+   1-3 nodes, with the larger "up to 10 nodes, depth limit 20 edges" property
+   delivered by Proptest under roadmap item `4.3.1` (and `4.3.1` treated as the
</code_context>
<issue_to_address>
**issue (review_instructions):** This question sentence uses the second-person pronoun "you", which the documentation guidelines prohibit.

Please rephrase this and the other open-question bullets to avoid second-person pronouns. For example, instead of "Do you accept Kani harnesses bounded to", use a neutral construction such as "Confirm whether Kani harnesses bounded to" or "This plan assumes Kani harnesses bounded to". The same pattern appears in subsequent bullets ("which escape hatch do you prefer", "Confirm or specify", "Acceptable?", "Confirm that … are acceptable").

<details>
<summary>Review instructions:</summary>

**Path patterns:** `**/*.md`

**Instructions:**
Avoid 2nd person or 1st person pronouns ("I", "you", "we").

</details>
</issue_to_address>

### Comment 5
<location path="docs/developers-guide.md" line_range="128" />
<code_context>
+| `duplicate_output_always_rejected`       | `src/ir/from_manifest_verification.rs` | A known duplicate path set produces `IrGenError::DuplicateOutput` and preserves the reported path.        | Global `default-unwind = "6"` | Verifies the private duplicate-output error constructor rather than full manifest lowering. Kani uses the real message key without formatted arguments so the proof avoids localization formatting.         |
</code_context>
<issue_to_address>
**nitpick (review_instructions):** The word "localization" uses US spelling; the documentation standard requires en-GB-oxendict spelling ("localisation").

<details>
<summary>Review instructions:</summary>

**Path patterns:** `**/*.md`

**Instructions:**
Use en-GB-oxendic (-ize / -yse / -our) spelling and grammar.

</details>
</issue_to_address>

### Comment 6
<location path="docs/adr-004-bound-kani-ir-harnesses-to-small-n.md" line_range="83" />
<code_context>
+through manifest lowering and `HashMap<Utf8PathBuf, _>` lookup exceeded the
+solver budget in path and map hashing. Under `cfg(kani)`, this constructor also
+uses the real duplicate-output message key without formatted arguments so the
+proof does not execute localization formatting internals.
+
+The rule-selection harness follows the same boundary. It verifies private
</code_context>
<issue_to_address>
**nitpick (review_instructions):** "localization" is spelled with US "-zation" rather than the en-GB "localisation" required by the style guide.

Update this sentence to use "localisation" instead of "localization" to align with en-GB-oxendict spelling.

<details>
<summary>Review instructions:</summary>

**Path patterns:** `**/*.md`

**Instructions:**
Use en-GB-oxendic (-ize / -yse / -our) spelling and grammar.

</details>
</issue_to_address>

### Comment 7
<location path="docs/adr-004-bound-kani-ir-harnesses-to-small-n.md" line_range="17" />
<code_context>
+
+## Context and problem statement
+
+Roadmap item `4.2.1` asks for Kani harnesses over the manifest-to-IR lowering
+path and cycle detector. The roadmap also describes coverage "up to 10 nodes,
+depth limit 20 edges". That bound is too large for Kani against the current
</code_context>
<issue_to_address>
**issue (review_instructions):** The acronym "IR" is used here without first being expanded to "Intermediate Representation (IR)" in this ADR.

Please expand "IR" on its first occurrence in this ADR, for example: "manifest-to-Intermediate Representation (IR) lowering". Subsequent uses can remain as "IR".

<details>
<summary>Review instructions:</summary>

**Path patterns:** `**/*.md`

**Instructions:**
Define uncommon acronyms on first use.

</details>
</issue_to_address>

[leynos]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[pandalump]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[lodyai]

@coderabbitai resume

[pandalump]

@coderabbitai resume

[coderabbitai]

✅ Action performed

Reviews resumed.

[leynos]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

[leynos]

@coderabbitai Please suggest a fix for this issue and supply a prompt for an AI coding agent to enable it to apply the fix. Include the file and symbol names indicated in the issue at the head of your response.

Excess Number of Function Arguments

src/ir/cycle.rs: CycleDetector.visit_known_edge

What lead to degradation?

CycleDetector.visit_known_edge has 5 arguments, max arguments = 4

Why does this problem occur?

Functions with many arguments indicate either a) low cohesion where the function has too many responsibilities, or b) a missing abstraction that encapsulates those arguments.
The threshold for the Rust language is 4 function arguments.

How to fix it?

Start by investigating the responsibilities of the function. Make sure it doesn't do too many things, in which case it should be split into smaller and more cohesive functions. Consider the refactoring INTRODUCE PARAMETER OBJECT to encapsulate arguments that refer to the same logical concept.

[pandalump]

@coderabbitai review

[coderabbitai]

✅ Action performed

Review finished.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.