Kani cycle-canonicalization harnesses (4.2.2)#392
Conversation
Draft the approval-gated execution plan for roadmap item 4.2.2, which adds Kani harnesses proving the canonicalize_cycle normalisation contract: preserved length and closed-cycle output, interior-node multiset preservation, and a stable smallest-first start node. The plan harnesses the pure canonicalize_cycle end-to-end over fixed-length closed cycles built from single-byte symbolic node names, reusing the existing cfg(kani) path_cmp helper, and splits by node count (N in 2..=4). It adds a rotation strengthening assertion so the suite is non-vacuous against order-scrambling bugs the three roadmap properties alone would miss, and records mutation-discipline patches per harness. Planning used a Plan agent for the harness design, a Firecrawl-backed research agent for Kani prior art, and a Logisphere community-of-experts review that drove the rotation strengthening, the unwrap-free symbolic_node, the unwind-bound reconciliation, and the honest multiset co-proof note. Status: DRAFT; awaits approval before implementation. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Note Reviews pausedIt 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 Use the following commands to manage reviews:
Use the checkboxes below for quick actions:
Added approval-gated ExecPlan coverage for cycle canonicalisation and updated the related ADR, roadmap, and developer docs to match the approved proof boundary. The main implementation change extracts a private generic Also recorded the verification and mutation results in the roadmap/ADR docs, and added the new ExecPlan document WalkthroughCycle canonicalisation now uses generic comparator-driven helpers in ChangesCycle canonicalisation Kani coverage
Possibly related PRs
Suggested labels
Suggested reviewers
Poem
🚥 Pre-merge checks | ✅ 20✅ Passed checks (20 passed)
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Reviewer's GuideAdds an approval-gated ExecPlan document describing how to introduce Kani harnesses for the private canonicalize_cycle function, without changing any production code, and specifying constraints, risks, stages of work, and harness design details. Sequence diagram for planned Kani harness execution for canonicalize_cyclesequenceDiagram
participant Kani as Kani_driver
participant Harness as canonicalize_two_node_cycle_is_canonical
participant Cycle as canonicalize_cycle
Kani->>Harness: execute_proof_harness()
Harness->>Harness: closed_cycle_n(2)
Harness->>Cycle: canonicalize_cycle(input_cycle)
Cycle-->>Harness: output_cycle
Harness->>Harness: count_byte(in_interior, sym)
Harness->>Harness: count_byte(out_interior, sym)
Harness->>Harness: is_rotation_of(out_interior, in_interior)
Harness->>Harness: path_cmp(first_node, node)
Harness->>Kani: assertion_results
File-Level Changes
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
![codescene-delta-analysis[bot]](https://avatars.githubusercontent.com/in/53921?s=60&v=4){kind=small}
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Add the red-stage harness names for cycle canonicalization so `cargo kani list` discovers the planned two-, three-, and four-node proofs before their real assertions are implemented. Record the Stage A approval, Kani library-path finding, red Kani evidence, deterministic gate results, and CodeRabbit review outcome in the ExecPlan.
Replace the red canonicalization harness assertions with the first real length-and-closure proof shape and keep the execplan current with the resource-capped Kani findings. Document that N=2 verifies under the user-scope cap, while the direct N=3 `Vec<Utf8PathBuf>` proof reaches the 8G memory cap. Also record the rejected concrete-enumeration fallback so the next implementation pass starts from the measured blocker rather than repeating it.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
|
@coderabbitai are you satisfied that the introduced proof is substantive, rigorous, and well-founded? |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "=== ExecPlan 4.2.2 ==="
cat docs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md
echo ""
echo "=== src/ir/cycle.rs ==="
cat src/ir/cycle.rs
echo ""
echo "=== Predecessor ExecPlan 4.2.1 (for comparison) ==="
cat docs/execplans/4-2-1-kani-harnesses-for-manifest-to-ir-safety-checks.md 2>/dev/null || echo "(not found)"
echo ""
echo "=== cycle_property_tests.rs (if present) ==="
fd -e rs -g '*cycle_property*' . | head -5 | xargs cat 2>/dev/null || echo "(not found)"Length of output: 173273
Assessment: substantive, rigorous, and well-founded?Short verdictThe plan is substantive and architecturally well-founded. The rigour is mostly sound but has one unresolved blocking issue and one internal inconsistency that should be corrected before Stage C can close. StrengthsTarget selection. Property completeness. The three roadmap properties (length+closure, interior multiset, stable smallest-first) directly match the documented contract. The Logisphere-driven addition of the rotation-strengthening assertion ( Honest co-proof documentation. The plan records openly that the interior-multiset property is co-proven rather than independently falsifiable by a small mutation, and assigns a clean falsification path to the rotation assertion instead. This is more intellectually honest than inventing a contrived isolation patch. Input construction discipline. Building closed cycles by construction ( Input-consumption handling. Tie-handling. Admitting repeated node bytes and using Mutation discipline. The three patches target three distinct code paths ( Proptest cross-reference. Explicitly delegating N≥5 to Concerns1. Stage C is blocked — no resolution committed (blocking)The Progress section records this explicitly: the direct end-to-end The 177-second N=2 runtime is itself a signal worth flagging: for two symbolic bytes and a deterministic three-node closed vector, that is slow. It suggests the solver is exploring the full 2.
|
| Criterion | Assessment |
|---|---|
| Target function is the right candidate | ✓ |
| Properties match the contract | ✓ |
| Rotation strengthening is non-vacuous | ✓ |
| Input construction is correct | ✓ |
| Mutation isolation is sound | ✓ |
| Proptest hand-off is appropriate | ✓ |
| N=2 verified, N≥3 tractable | ✗ — blocked; decision required |
| Interfaces section reflects current implementation | ✗ — stale symbolic_node snippet |
Unwind bounds safe for is_rotation_of |
⚠ — recheck for N=4 |
The plan is worth approving as a design document. Commit a resolution decision for the N≥3 tractability issue and update the Interfaces section before Stage C proceeds.
Align the ExecPlan and pull request description with the committed harness work and measured tractability blocker. Add the Stage C approval gate for selecting the proof boundary, update stale helper and alphabet examples, correct the unwind discussion to use per-loop bounds, and rewrite acceptance criteria so they describe the approved boundary rather than assuming every direct `Utf8PathBuf` proof will pass.
Document the capped N=2 salvage experiment result for cycle canonicalization. The ID-retaining direct proof shape still exceeds the 8 GiB Kani memory envelope before N=3 can be attempted, so record the run as a tractability finding rather than a completed proof boundary.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Update the 4.2.2 ExecPlan to reflect the approved production-owned kernel boundary. Keep the public API closed while allowing private production refactoring of cycle canonicalization for legibility, testability, and Kani tractability.
Move cycle rotation and closure into a private generic production helper and keep `canonicalize_cycle` as the path-bearing wrapper. This gives Kani a production-owned integer instantiation without adding a public verification port or a separate model. Update the canonicalization harnesses to prove length, closure, interior multiset preservation, smallest-start selection, and rotation for distinct `u8` cycles at N=2, N=3, and N=4. Add a small direct path wrapper harness so the `Utf8PathBuf` adapter and comparator remain covered by Kani.
Document the approved private production-kernel proof boundary for cycle canonicalization and add mutation patches for the three property harnesses. Tighten the Kani closure helper so empty output is not treated as closed, and record the ADR/developer-guide evidence tying the `u8` kernel proof back to the path-bearing wrapper.
Mark roadmap item `4.2.2` complete against the approved private production-kernel boundary. Record the final deterministic gate evidence and the capped `make kani-ir` run, which verified 13 IR harnesses with zero failures.
lodyai
Bot
changed the title
Mark the cycle-canonicalization ExecPlan complete after the final CodeRabbit review returned zero findings and the draft pull request was updated to describe the implemented proof boundary.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
leynos
changed the title
|
@coderabbitai following the latest commit, are you satisfied that the introduced proof is substantive, rigorous, and well-founded? |
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
|
@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. Ensure that this is validated against the current version of the codegraph. If further refinement to address this finding would be deleterious, please supply a clear explanatory one to two paragraph markdown message I can paste into the CodeScene web ui's diagnostic suppression function so this diagnostic can be silenced. Comment on file //! Kani harnesses for bounded IR cycle-detection properties.
//! Kani harnesses for bounded IR cycle-handling properties.
❌ New issue: Primitive Obsession |
|
Tip For best results, initiate chat on the files or code changes. 🧩 Analysis chain🏁 Script executed: #!/bin/bash
set -euo pipefail
echo "=== src/ir/cycle.rs ==="
cat src/ir/cycle.rs
echo ""
echo "=== src/ir/cycle_verification.rs ==="
cat src/ir/cycle_verification.rs
echo ""
echo "=== src/ir/cycle_property_tests.rs ==="
cat src/ir/cycle_property_tests.rs
echo ""
echo "=== ExecPlan 4.2.2 ==="
cat docs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md
echo ""
echo "=== ADR-004 ==="
cat docs/adr-004-bound-kani-ir-harnesses-to-small-n.md 2>/dev/null || echo "(not found)"
echo ""
echo "=== Mutation patches ==="
find docs/verification/mutations -type f | sort | while read -r f; do
echo "--- $f ---"
cat "$f"
echo ""
doneLength of output: 134001
Revised assessmentResolved concerns from the previous reviewN≥3 tractability (was blocking). The private Stale Unwind bounds for the nested rotation check. The deepest single loop at N=4 is 4 iterations; every loop in the proof path (the outer Positive observations on the final stateFive load-bearing assertions per kernel harness. Length, closure, interior-multiset (per-symbol count), smallest-start, and rotation-existential are all present. The rotation assertion closes the order-scrambling gap flagged in the previous review; the multiset assertion is honestly documented as co-proven.
Pairwise distinctness is complete. N=2 constrains 1 pair, N=3 constrains 3, N=4 constrains all 6. The Adapter harness is sound. Mutation discipline is clean. The two-node patch breaks Thirteen harnesses, zero failures, zero unresolved review findings. The final Summary
The proof is substantive, rigorous, and well-founded. No outstanding concerns. |
This comment was marked as resolved.
This comment was marked as resolved.
This comment was marked as outdated.
This comment was marked as outdated.
Sorry, something went wrong.
Expand the roadmap entry for 4.2.2 with the settled private-kernel proof boundary, final validation count, mutation evidence, and CodeRabbit review state. Record the documentary audit in the ExecPlan so the roadmap and plan agree on the current implementation status.
There was a problem hiding this comment.
Actionable comments posted: 5
Caution
Some comments are outside the diff and can’t be posted inline due to platform limitations.
⚠️ Outside diff range comments (1)
docs/adr-004-bound-kani-ir-harnesses-to-small-n.md (1)
14-16: 📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick winUpdate the
## Datefield to match the latest status entry.The style guide defines the Date field as "the date the ADR was created or last updated." The Status section records an extension on 2026-06-23, so the Date field must be updated accordingly.
📝 Proposed fix
## Date -2026-06-12. +2026-06-23.Triage:
[type:docstyle]🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the rest with a brief reason, keep changes minimal, and validate. In `@docs/adr-004-bound-kani-ir-harnesses-to-small-n.md` around lines 14 - 16, The ADR’s Date field is out of sync with its latest status update. Update the `## Date` entry in this document to the most recent ADR update date recorded in the Status section, using the existing ADR heading and `Date` field as the only place to change.
🤖 Prompt for all review comments with AI agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
Inline comments:
In `@docs/adr-004-bound-kani-ir-harnesses-to-small-n.md`:
- Line 124: Fix the spelling in the affected documentation sentence by changing
“randomised” to “randomized” to match the required -ize form. Update the text in
the ADR markdown where the phrase about “exercise path-bearing canonicalization
up to the larger randomised bounds” appears, keeping the rest of the sentence
unchanged.
In `@docs/developers-guide.md`:
- Line 200: Add the missing comma before “so” in the sentence in the
documentation table entry, since it joins two independent clauses. Update the
wording in the affected docs row so the phrase around “This complements the
a-first harness” reads with a comma before “so,” keeping the rest of the
`two_node_cycle_reports_cycle_b_first` description unchanged.
- Line 202: The documentation entry uses the British spelling “synthesise” where
the project requires “synthesize”; update the wording in the affected table row
in docs/developers-guide.md and keep the rest of the description unchanged.
In `@docs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md`:
- Line 1124: The section heading currently uses the US spelling “Artifacts”
while the surrounding text uses the required en-GB form “artefacts”; update the
heading in the affected markdown section to “Artefacts and notes” so it matches
the body text and project spelling conventions.
- Around line 14-15: The documentation text uses inconsistent en-GB-oxendict
spelling for the cycle canonicalization description. Update the prose around
canonicalize_cycle to use -ize forms such as “normalization” and “normalize”
instead of “normalisation” and “normalise”, and make the same spelling
correction anywhere else in this section where the same words appear.
---
Outside diff comments:
In `@docs/adr-004-bound-kani-ir-harnesses-to-small-n.md`:
- Around line 14-16: The ADR’s Date field is out of sync with its latest status
update. Update the `## Date` entry in this document to the most recent ADR
update date recorded in the Status section, using the existing ADR heading and
`Date` field as the only place to change.
🪄 Autofix (Beta)
Fix all unresolved CodeRabbit comments on this PR:
- Push a commit to this branch (recommended)
- Create a new PR with the fixes
ℹ️ Review info
⚙️ Run configuration
Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Pro Plus
Run ID: 8efe8414-479a-476d-a0cf-671935a75ba8
📒 Files selected for processing (10)
docs/adr-004-bound-kani-ir-harnesses-to-small-n.mddocs/developers-guide.mddocs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.mddocs/roadmap.mddocs/verification/mutations/ir__cycle__verification__canonicalize_four_node_cycle_is_canonical.patchdocs/verification/mutations/ir__cycle__verification__canonicalize_three_node_cycle_is_canonical.patchdocs/verification/mutations/ir__cycle__verification__canonicalize_two_node_cycle_is_canonical.patchsrc/ir/cycle.rssrc/ir/cycle_property_tests.rssrc/ir/cycle_verification.rs
| while `canonicalize_cycle(Vec<Utf8PathBuf>)` remains the production wrapper | ||
| using the path comparator. A small direct adapter harness checks the | ||
| wrapper/kernel connection for two-node path cycles, and Proptest continues to | ||
| exercise path-bearing canonicalization up to the larger randomised bounds. |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Replace "randomised" with "randomized".
en-GB-oxendict mandates the -ize suffix for this verb.
📝 Proposed fix
-earing canonicalization up to the larger randomised bounds.
+earing canonicalization up to the larger randomized bounds.Triage: [type:spelling]
🧰 Tools
🪛 LanguageTool
[style] ~124-~124: Would you like to use the Oxford spelling “randomized”? The spelling ‘randomised’ is also correct.
Context: ...aring canonicalization up to the larger randomised bounds. ## Known risks and limitations...
(OXFORD_SPELLING_Z_NOT_S)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/adr-004-bound-kani-ir-harnesses-to-small-n.md` at line 124, Fix the
spelling in the affected documentation sentence by changing “randomised” to
“randomized” to match the required -ize form. Update the text in the ADR
markdown where the phrase about “exercise path-bearing canonicalization up to
the larger randomised bounds” appears, keeping the rest of the sentence
unchanged.
Source: Path instructions
| | `missing_rule_shape_is_rejected` | `src/ir/from_manifest_verification.rs` | A missing single rule reaches `IrGenError::RuleNotFound` and preserves target and rule names. | `#[kani::unwind(6)]` | Drives production `resolve_rule` with symbolic target and rule names and an empty rule map. | | ||
| | `self_dependency_reports_cycle` | `src/ir/cycle_verification.rs` | A self-dependency is reported as a cycle by production traversal. | `#[kani::unwind(5)]` | Drives production `contains_cycle`, which reuses `CycleDetector::visit` in boolean mode. | | ||
| | `two_node_cycle_reports_cycle_a_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `a` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; the separate insertion-order harnesses cover deterministic map-entry traversal under the Kani map. | | ||
| | `two_node_cycle_reports_cycle_b_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `b` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; this complements the `a`-first harness so the proof is not tied to one insertion order. | |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Add a comma before "so" — it links two independent clauses.
📝 Proposed fix
-| `two_node_cycle_reports_cycle_b_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `b` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; this complements the `a`-first harness so the proof is not tied to one insertion order. |
+| `two_node_cycle_reports_cycle_b_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `b` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; this complements the `a`-first harness, so the proof is not tied to one insertion order. |Triage: [type:grammar]
🧰 Tools
🪛 LanguageTool
[uncategorized] ~200-~200: Use a comma before ‘so’ if it connects two independent clauses (unless they are closely connected and short).
Context: ...; this complements the a-first harness so the proof is not tied to one insertion ...
(COMMA_COMPOUND_SENTENCE_2)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/developers-guide.md` at line 200, Add the missing comma before “so” in
the sentence in the documentation table entry, since it joins two independent
clauses. Update the wording in the affected docs row so the phrase around “This
complements the a-first harness” reads with a comma before “so,” keeping the
rest of the `two_node_cycle_reports_cycle_b_first` description unchanged.
| | `two_node_cycle_reports_cycle_a_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `a` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; the separate insertion-order harnesses cover deterministic map-entry traversal under the Kani map. | | ||
| | `two_node_cycle_reports_cycle_b_first` | `src/ir/cycle_verification.rs` | A two-node cycle is reported when the `b` node is inserted first. | `#[kani::unwind(5)]` | Drives production `contains_cycle`; this complements the `a`-first harness so the proof is not tied to one insertion order. | | ||
| | `direct_missing_dependency_does_not_report_cycle` | `src/ir/cycle_verification.rs` | A single target with an absent dependency is not reported as a cycle. | `#[kani::unwind(6)]` | Drives production `contains_cycle` and proves that a missing direct dependency does not enter the cycle branch. | | ||
| | `transitive_missing_dependency_does_not_report_cycle` | `src/ir/cycle_verification.rs` | A two-target chain whose deeper dependency is absent is not reported as a cycle. | `#[kani::unwind(6)]` | Drives production `contains_cycle` and proves that an absent dependency below another target does not synthesise a false cycle. | |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Replace "synthesise" with "synthesize".
en-GB-oxendict requires the -ize suffix.
📝 Proposed fix
-| `transitive_missing_dependency_does_not_report_cycle` | `src/ir/cycle_verification.rs` | A two-target chain whose deeper dependency is absent is not reported as a cycle. | `#[kani::unwind(6)]` | Drives production `contains_cycle` and proves that an absent dependency below another target does not synthesise a false cycle. |
+| `transitive_missing_dependency_does_not_report_cycle` | `src/ir/cycle_verification.rs` | A two-target chain whose deeper dependency is absent is not reported as a cycle. | `#[kani::unwind(6)]` | Drives production `contains_cycle` and proves that an absent dependency below another target does not synthesize a false cycle. |Triage: [type:spelling]
🧰 Tools
🪛 LanguageTool
[style] ~202-~202: Would you like to use the Oxford spelling “synthesize”? The spelling ‘synthesise’ is also correct.
Context: ...ependency below another target does not synthesise a false cycle. ...
(OXFORD_SPELLING_Z_NOT_S)
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/developers-guide.md` at line 202, The documentation entry uses the
British spelling “synthesise” where the project requires “synthesize”; update
the wording in the affected table row in docs/developers-guide.md and keep the
rest of the description unchanged.
Source: Path instructions
| of the pure normalisation function `canonicalize_cycle` in | ||
| [`src/ir/cycle.rs`](../../src/ir/cycle.rs). Canonicalization is what turns a |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Replace "-ise" spellings with "-ize" throughout.
Per en-GB-oxendict, words derived from the Greek -izo suffix take the "-ize" ending — "normalisation" and "normalise" must be "normalization" and "normalize". The same applies at lines 779 and 781.
✏️ Suggested corrections
-of the pure normalisation function `canonicalize_cycle` in
+of the pure normalization function `canonicalize_cycle` inLine 779:
-`canonicalize_cycle` (lines ~440-447) normalises that raw witness so the
+`canonicalize_cycle` (lines ~440-447) normalizes that raw witness so theLine 781:
-diagnostic is stable by delegating to the private generic
-`canonicalize_cycle_by` kernel with the production path comparator.
+diagnostic is stable by delegating to the private generic normalization
+`canonicalize_cycle_by` kernel with the production path comparator.Triage: [type:spelling]
As per path instructions: "Use en-GB-oxendict (-ize / -yse / -our) spelling and grammar."
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md` around
lines 14 - 15, The documentation text uses inconsistent en-GB-oxendict spelling
for the cycle canonicalization description. Update the prose around
canonicalize_cycle to use -ize forms such as “normalization” and “normalize”
instead of “normalisation” and “normalise”, and make the same spelling
correction anywhere else in this section where the same words appear.
Source: Path instructions
| small and per-property, so any stage can be rolled back with `git revert` | ||
| without disturbing the others. | ||
|
|
||
| ## Artifacts and notes |
There was a problem hiding this comment.
📐 Maintainability & Code Quality | 🟡 Minor | ⚡ Quick win
Correct "Artifacts" to "Artefacts" in the section heading.
The heading uses US spelling whilst the body text at line 1126 correctly uses the British form "artefacts". Align the heading with the body.
✏️ Suggested correction
-## Artifacts and notes
+## Artefacts and notesTriage: [type:spelling]
As per path instructions: "Use en-GB-oxendict (-ize / -yse / -our) spelling and grammar."
🤖 Prompt for AI Agents
Verify each finding against current code. Fix only still-valid issues, skip the
rest with a brief reason, keep changes minimal, and validate.
In `@docs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md` at line
1124, The section heading currently uses the US spelling “Artifacts” while the
surrounding text uses the required en-GB form “artefacts”; update the heading in
the affected markdown section to “Artefacts and notes” so it matches the body
text and project spelling conventions.
Source: Path instructions
1 participant
Summary
This branch completes roadmap task 4.2.2 — Add Kani harnesses for cycle canonicalization.
It extracts a private production-owned canonicalization kernel in
src/ir/cycle.rs, proves that kernel exhaustively with Kani over distinct smallu8cycles, and keeps the existingUtf8PathBufwrapper as the production adapter. The completed execution plan isdocs/execplans/4-2-2-kani-harnesses-for-cycle-canonicalization.md.The original direct
Utf8PathBufproof route was measured and rejected under the required 8 GiB, five-minute cap. The approved proof claim is now narrower and cleaner: Kani proves the production canonicalization algorithm for N=2, N=3, and N=4 integer cycles; a direct adapter harness and the existing Proptest suite exercise the path-bearing instantiation.Roadmap task: 4.2.2
Review walkthrough
src/ir/cycle.rsfor the privatecanonicalize_cycle_byextraction and theUtf8PathBufwrapper.src/ir/cycle_verification.rsfor the threeu8kernel harnesses and the two-node wrapper adapter harness.src/ir/cycle_property_tests.rsfor the ordinary tests tying the extracted kernel to the existing property coverage.docs/developers-guide.md,docs/adr-004-bound-kani-ir-harnesses-to-small-n.md, anddocs/roadmap.mdfor the documented proof boundary.docs/verification/mutations/, which deliberately break the rotation-start, closure, and wrap-around paths.Validation
make check-fmt: passedmake lint: passedmake test: passedmake markdownlint: passedmake nixie: passedmake kani-ir: passed withComplete - 13 successfully verified harnesses, 0 failures, 13 total.coderabbit review --agent: zero findings for the scaffold, kernel, proof-boundary, and final branch reviewsNotes
Direct
Utf8PathBufproperty proofs for N=2 through N=4 remain a measured non-goal for this branch. They exceeded the agreed resource envelope even after the ID-retaining salvage encoding. The branch avoids a Kani-only duplicate by moving the algorithm into private production code and proving that implementation directly over a tractableu8instantiation.