Plan: Add Proptest coverage for deterministic Ninja emission (4.3.1)

[leynos]

Summary

Draft execution plan for roadmap item 4.3.1, adding Proptest coverage for deterministic Ninja emission. The plan is for review and approval only — no implementation has been done.

Plan: docs/execplans/4-3-1-proptests-for-deterministic-ninja-emission.md

Scope

The three roadmap sub-items (insertion-order stability, default target ordering, path_key invariance), plus the larger-N duplicate-output and cycle-rejection obligations that roadmap 4.2.1 and ADR-004 both explicitly deferred to this item. The plan also settles the determinism contract that formal-verification-methods-in-netsuke.md asks for but no roadmap item owns.

Ten verification obligations, nine mutation patches, and eight milestones.

Design review

The first draft was reviewed through six expert lenses and then rewritten. Four findings reshaped it, each verified directly rather than taken on trust:

• The shared strategy cannot live in test_support. Proven by compile probe: passing a netsuke-typed value into a src/-side #[cfg(test)] module fails with "multiple different versions of crate netsuke in the dependency graph", because test_support depends on the crate that dev-depends on it. All strategies moved to src/.
• The insertion-order property was not seed-reproducible. RandomState is outside Proptest's seed, so shrinking silently discards valid candidates and committed regression seeds are decorative. Restructured around extracted pure ordering helpers over explicitly shuffled vectors.
• docs/verification/mutations/ is already governed by a contract test. tests/kani_mutation_evidence_tests.rs rejects any patch stem not rooted at ir, so the proposed ninja_gen patches were unrepresentable and would have failed make test.
• src/ninja_gen/mod.rs is exactly 400 lines — the AGENTS.md ceiling — so the first draft breached a constraint on its first commit.

Three obligation statements were also simply false and are corrected: path_key injectivity omitted the empty-path collision (path_key([]) == path_key([""])); OBL-ACTION claimed a converse amounting to SHA-256 collision resistance; and OBL-E2E's rule-permutation claim is false because process_rules is last-writer-wins on duplicate rule names.

Two obligations were added because nothing in the first draft reached them: a source-shape contract test forbidding unordered-collection iteration in src/ninja_gen/ (the only thing that catches a future map), and a two-run assert_cmd byte comparison (the guarantee the plan publishes, which nothing in the repository currently tests).

Decisions taken with the user

• Include the inherited larger-N IR obligations.
• Settle the determinism contract here, in an ADR plus user-facing documentation.
• Add a proptest Make target, measure it, and split only if justified. Measured: the whole suite is ~6 s of CPU and 2–3 s wall against a 45-second budget, so no light/heavy split is planned. A standalone CI job would have been ~98% compile.

Notes for reviewers

• The ADR number is a deliberate ADR-NNN placeholder: adr-021 is already claimed on four open branches and adr-020 on two.
• The plan is approval-gated. EP-M0 question 2 (does declaration-order invariance hold today?) gates the ADR's content and should be answered before approval if reviewers prefer.

References

• Lody session: https://lody.ai/leynos/sessions/3156b0c1-b311-4fd2-b735-649299305edb

🤖 Generated with Claude Code

Summary by Sourcery

Approve a detailed execution plan for adding deterministic Ninja emission coverage and completing deferred larger-N IR verification obligations.

Enhancements:

• Add an approval-gated execution plan for comprehensive property-based verification of deterministic Ninja emission and related larger-N IR invariants.
• Define the determinism contract, verification obligations, mutation evidence, milestones, constraints, and validation strategy for the planned work.

Documentation:

• Document the proposed determinism contract, testing scope, design decisions, and implementation roadmap for future user-facing and developer documentation updates.

Tests:

• Plan Proptest coverage for insertion-order stability, default-target ordering, path-key invariance, action hashing, duplicate-output rejection, cycle rejection, end-to-end declaration-order behaviour, and Ninja compatibility.
• Plan source-shape and process-level tests to guard against unordered collection iteration and verify byte-identical output across separate runs.

[coderabbitai]

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

---

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

[sourcery-ai]

Reviewer's Guide

This draft-only PR adds a detailed, approval-gated execution plan—not implementation—for Proptest coverage of deterministic Ninja emission, including the roadmap's ordering properties, inherited larger-N IR checks, mutation-backed evidence, an explicit determinism contract, and staged validation/documentation work.

Sequence diagram for planned end-to-end determinism verification

sequenceDiagram
    participant Test as Process test
    participant Binary as Netsuke binary
    participant Lowering as IR lowering
    participant Emitter as Ninja emitter
    participant FS as Temporary filesystem

    Test->>Binary: generate
    Binary->>Lowering: from_manifest
    Lowering-->>Binary: BuildGraph
    Binary->>Emitter: generate_bundle
    Emitter-->>Binary: GeneratedNinja
    Binary->>FS: write build.ninja and sidecars
    Binary-->>Test: generated bytes
    Test->>Binary: generate
    Binary->>Lowering: from_manifest
    Lowering-->>Binary: BuildGraph
    Binary->>Emitter: generate_bundle
    Emitter-->>Binary: GeneratedNinja
    Binary->>FS: write build.ninja and sidecars
    Binary-->>Test: generated bytes
    Test->>Test: compare generated bytes

Loading

Flow diagram for planned Proptest verification milestones

flowchart TD
    Approval[Approval gate] --> M0[EP-M0 feasibility spike]
    M0 --> M1[EP-M1 determinism contract ADR]
    M1 --> M2[EP-M2 refactors and make proptest]
    M2 --> M3[EP-M3 shared graph strategy]
    M3 --> M4[EP-M4 path_key and no-loss properties]
    M4 --> M5[EP-M5 ordering and default properties]
    M5 --> M6[EP-M6 hashing declaration order process output]
    M6 --> M7[EP-M7 larger-N duplicate and cycle checks]
    M7 --> M8[EP-M8 Ninja oracle documentation validation]
    M8 --> Gates[All gates and mutation evidence pass]

Loading

File-Level Changes

Change	Details	Files
Adds a comprehensive, approval-gated execution plan for property-based verification of deterministic Ninja emission.	Defines ten verification obligations covering path-key canonicality, edge preservation, insertion-order stability, unordered-collection boundaries, default-target ordering, action hashing, declaration-order behaviour, process-level byte stability, larger-N duplicate-output and cycle rejection, and real-Ninja compatibility. Specifies Proptest strategies, domains, independent oracles, non-vacuity requirements, regression-seed handling, mutation patches, and acceptance criteria. Organises implementation into eight milestones covering feasibility, contract documentation, refactoring and test infrastructure, shared strategies, properties, Ninja integration, documentation, and final validation.	docs/execplans/4-3-1-proptests-for-deterministic-ninja-emission.md
Records design-review findings and constraints that shape the proposed implementation.	Moves Netsuke-typed strategies into src-side tests after documenting the test_support crate-version incompatibility. Restructures insertion-order testing around seed-deterministic pure ordering helpers because HashMap RandomState is outside Proptest's seed. Adds a source-shape contract test and a two-run assert_cmd test to cover future unordered iteration and the published process-level guarantee. Corrects path_key injectivity, action-hash, and declaration-order claims, and accounts for existing mutation-evidence contracts, file-size ceilings, runtime measurements, and ADR-number allocation.	docs/execplans/4-3-1-proptests-for-deterministic-ninja-emission.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.

[codescene-access]

No quality gates enabled for this code.