Skip to content

Share private IR comparison helper (#576) - #587

Open
leynos wants to merge 1 commit into
mainfrom
issue-576-deduplicate-private-ir-sorting-and-cycle-support-helpers
Open

Share private IR comparison helper (#576)#587
leynos wants to merge 1 commit into
mainfrom
issue-576-deduplicate-private-ir-sorting-and-cycle-support-helpers

Conversation

@leynos

@leynos leynos commented Aug 24, 2026

Copy link
Copy Markdown
Owner

Summary

This branch shares the Kani-specific first-byte comparison used by IR cycle
paths and manifest rule names. It removes the duplicate bounded comparison
without changing standard-build ordering, public API visibility, or the
existing cap-split structure.

Closes #576

Review walkthrough

Validation

  • make check-fmt: passed.
  • make test: passed (2,398 tests; 3 skipped; doctests passed).
  • make typecheck: passed.
  • make lint: passed.
  • make kani-full: passed (13 verified; 0 failures).
  • coderabbit review --light --committed --base origin/main --agent: passed
    (0 findings).

References

@coderabbitai

coderabbitai Bot commented Aug 24, 2026

Copy link
Copy Markdown
Contributor

Review Change Stack

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: cffa64b9-210b-4df1-9196-30d47e179369

📥 Commits

Reviewing files that changed from the base of the PR and between 1d0cb16 and 7c2c8bd.

📒 Files selected for processing (2)
  • src/ir/cycle_support.rs
  • src/ir/sort_utils.rs
🔗 Linked repositories identified

CodeRabbit considers these linked repositories for cross-repo context during reviews:

  • leynos/monotony (auto-detected)
  • leynos/rstest-bdd (auto-detected)
  • leynos/whitaker (auto-detected)
  • leynos/ortho-config (auto-detected)
  • leynos/shared-actions (auto-detected)

Limit details: You’ve used all 3 included reviews currently available. Your 75 included PR review attempts over the past 7 days set your current allowance at 3 reviews per hour.


Summary

  • Share the Kani-specific first_byte_cmp helper between cycle-path ordering and manifest rule-name sorting.
  • Keep the helper restricted to crate::ir and preserve the public API.
  • Preserve standard-build ordering, Kani comparison semantics, and the existing cap-split structure.
  • Validate formatting, tests, type checking, linting, and Kani verification.

Refs #576

Walkthrough

Extract the Kani first-byte string comparison into first_byte_cmp. Make path_cmp and the Kani comparator in sort_utils.rs use the shared helper while preserving existing ordering behaviour.

Changes

Kani comparison deduplication

Layer / File(s) Summary
Shared first-byte comparison
src/ir/cycle_support.rs, src/ir/sort_utils.rs
Add the Kani-only first_byte_cmp helper. Route both path and string comparisons through it. Preserve empty-string and first-byte ordering semantics.

Suggested labels: Issue

Poem

Share the bytes, keep order bright
Let Kani trace the same clear flight
Paths and strings now speak as one
Empty checks remain well done
One small helper, work is spun

🚥 Pre-merge checks | ✅ 19 | ❌ 1

❌ Failed checks (1 warning)

Check name Status Explanation Resolution
Developer Documentation ⚠️ Warning The pull request introduces an internal API and changes an internal support-module boundary without updating docs/developers-guide.md. src/ir/cycle_support.rs adds `#[cfg(kani)] pub(in crate::ir) … Update docs/developers-guide.md to document first_byte_cmp, its cfg(kani) first-byte and empty-string semantics, its pub(in crate::ir) visibility, and its use by cycle-path and manifest rule-name sorting. Correct the existing `sort_…
✅ Passed checks (19 passed)
Check name Status Explanation
Linked Issues check ✅ Passed The changes satisfy issue #576 by sharing the Kani-specific comparison helper, using crate-internal visibility, preserving standard-build and Kani semantics, avoiding public API changes, and retaining…
Out of Scope Changes check ✅ Passed The changes remain within issue #576. They modify only the comparison-helper sharing and related Kani usage, with no unrelated scope or cap-split work.
Docstring Coverage ✅ Passed Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 4 functions across 2 files.
Testing (Overall) ✅ Passed Pass the testing check. Treat this PR as a behaviour-preserving extraction, not new functionality: the non-Kani path remains left.cmp(right), and the Kani helper copies the previous first-byte logic…
User-Facing Documentation ✅ Passed Pass this check. The committed diff changes only src/ir/cycle_support.rs and src/ir/sort_utils.rs. It moves Kani-only first-byte comparison logic into pub(in crate::ir) first_byte_cmp; standard-…
Module-Level Documentation ✅ Passed Pass the module-level documentation check. The PR changes no module declarations and adds no module. Both modified modules already carry //! documentation in the base and PR revisions. `cycle_suppor…
Testing (Unit And Behavioural) ✅ Passed Pass the testing check. The pull request performs a Kani-only helper extraction and preserves the comparison body and call semantics. Existing cycle property tests verify canonicalisation invariants a…
Testing (Property / Proof) ✅ Passed Treat the check as passed. The diff changes only src/ir/cycle_support.rs and src/ir/sort_utils.rs. It moves the existing Kani first-byte comparison into first_byte_cmp; it does not introduce a n…
Testing (Compile-Time / Ui) ✅ Passed Pass the compile-time/UI check. The change only refactors existing #[cfg(kani)] comparison logic and keeps standard-build behaviour unchanged. Existing direct-rustc UI tests in `tests/kani_cfg_ui_…
Unit Architecture ✅ Passed Keep this change as a PASS. The diff extracts the existing Kani first-byte comparison into first_byte_cmp and delegates path_cmp and string_cmp to it. The helper reads explicit &str inputs and…
Domain Architecture ✅ Passed Pass the Domain Architecture check. The PR changes only pure IR comparison helpers. It moves the existing Kani first-byte ordering logic into cycle::support::first_byte_cmp and calls it from `sort_u…
Observability ✅ Passed Classify the observability check as PASS. Restrict the change to a Kani-gated refactor: first_byte_cmp contains the same first-byte and empty-string ordering logic, and path_cmp delegates to it. K…
Security And Privacy ✅ Passed Pass the Security and Privacy check. The pull request changes only Kani-gated string comparison and delegates path_cmp and string_cmp to the private first_byte_cmp helper. The diff adds no secre…
Performance And Resource Use ✅ Passed Accept the change for this check. The diff only extracts the existing Kani first-byte comparison into first_byte_cmp. The helper uses borrowed &str values and as_bytes().first(), so it adds no a…
Concurrency And State ✅ Passed Pass this check. The commit changes only comparison helper wiring in src/ir/cycle_support.rs and src/ir/sort_utils.rs. It adds no shared mutable state, locks, tasks, channels, globals, or asynchro…
Architectural Complexity And Maintainability ✅ Passed Pass this check. The change adds one small first_byte_cmp helper in the existing cycle::support boundary and gives it an immediate second consumer in sort_utils. It removes the exact duplicated …
Rust Compiler Lint Integrity ✅ Passed Pass. The pull request adds no #[allow(dead_code)], #[allow(unused_imports)], #[allow(unused)], broad #[expect], artificial anchors, or new clone calls. Under cfg(kani), first_byte_cmp has…
Title check ✅ Passed The title accurately describes sharing the private IR comparison helper and references issue #576 as required.
Description check ✅ Passed The description clearly explains the shared Kani comparison helper, preserved behaviour, validation results, and linked issue.
Full details: Linked Issues check

Explanation

The changes satisfy issue #576 by sharing the Kani-specific comparison helper, using crate-internal visibility, preserving standard-build and Kani semantics, avoiding public API changes, and retaining the cap-split structure.

Full details: Testing (Overall)

Explanation

Pass the testing check. Treat this PR as a behaviour-preserving extraction, not new functionality: the non-Kani path remains left.cmp(right), and the Kani helper copies the previous first-byte logic exactly. Existing Kani proofs substantively exercise both consumers. multiple_rule_shape_is_rejected tests both rule-name input orders and asserts the sorted result. canonicalize_path_wrapper_matches_u8_kernel_for_two_nodes tests both path orders against an independent ordering oracle. A no-op or inverted comparator would fail these assertions. The committed diff adds no untested behavioural path.

Full details: User-Facing Documentation

Explanation

Pass this check. The committed diff changes only src/ir/cycle_support.rs and src/ir/sort_utils.rs. It moves Kani-only first-byte comparison logic into pub(in crate::ir) first_byte_cmp; standard-build ordering remains left.cmp(right). The helper is crate-internal, and no user-facing functionality or behaviour is introduced. docs/users-guide.md and README.md are unchanged, which is appropriate because this refactor does not require user documentation.

Full details: Developer Documentation

Explanation

The pull request introduces an internal API and changes an internal support-module boundary without updating docs/developers-guide.md. src/ir/cycle_support.rs adds #[cfg(kani)] pub(in crate::ir) fn first_byte_cmp, and src/ir/sort_utils.rs now imports it across the cycle::support and manifest-support areas. The existing guide instead states that sort_utils.rs owns the comparison helpers and that cycle_support.rs owns path comparison, with no record of the shared first_byte_cmp contract. The commit changes only the two Rust files, so the developer documentation is stale and incomplete.

Resolution

Update docs/developers-guide.md to document first_byte_cmp, its cfg(kani) first-byte and empty-string semantics, its pub(in crate::ir) visibility, and its use by cycle-path and manifest rule-name sorting. Correct the existing sort_utils.rs and cycle_support.rs ownership and boundary descriptions. Record the boundary decision in the relevant ADR or design document when treating this refactor as an architectural decision.

Full details: Module-Level Documentation

Explanation

Pass the module-level documentation check. The PR changes no module declarations and adds no module. Both modified modules already carry //! documentation in the base and PR revisions. cycle_support explains cycle-support utilities, path comparison, canonical rotation, and Kani variants. sort_utils explains deterministic sorting, its manifest-lowering relationship, and its Kani purpose. The source-module audit found documentation on all module-bearing Rust files inspected.

Full details: Testing (Unit And Behavioural)

Explanation

Pass the testing check. The pull request performs a Kani-only helper extraction and preserves the comparison body and call semantics. Existing cycle property tests verify canonicalisation invariants and deterministic ordering. Existing manifest behavioural tests verify multiple-rule error ordering. Kani harnesses exercise both changed caller paths: cycle canonicalisation reaches path_cmp and first_byte_cmp, while multiple_rule_shape_is_rejected reaches resolve_rule and sort_strings and checks sorted output. Standard-build ordering is unchanged, so no new end-to-end workflow test is required.

Full details: Testing (Property / Proof)

Explanation

Treat the check as passed. The diff changes only src/ir/cycle_support.rs and src/ir/sort_utils.rs. It moves the existing Kani first-byte comparison into first_byte_cmp; it does not introduce a new ordering invariant or proof assumption. The standard path_cmp implementation remains unchanged. Existing substantive Kani proofs cover cycle canonicalisation and manifest rule sorting, and existing proptest tests cover cycle ordering properties. The custom check therefore requires no additional property-test recommendation for this refactor.

Full details: Testing (Compile-Time / Ui)

Explanation

Pass the compile-time/UI check. The change only refactors existing #[cfg(kani)] comparison logic and keeps standard-build behaviour unchanged. Existing direct-rustc UI tests in tests/kani_cfg_ui_tests.rs cover the cfg(kani) compile contract, while the Kani harnesses exercise both cycle-path and manifest-rule sorting consumers. No text or UI output changes, so snapshot coverage is not applicable.

Full details: Unit Architecture

Explanation

Keep this change as a PASS. The diff extracts the existing Kani first-byte comparison into first_byte_cmp and delegates path_cmp and string_cmp to it. The helper reads explicit &str inputs and performs no I/O, mutation, clock access, network call, fallible work, or hidden dependency. The helper remains private to crate::ir through pub(in crate::ir). sort_strings retains its existing in-place mutation, and the pull request adds no new command, persistence, or external side-effect responsibility. No Unit Architecture failure condition is introduced.

Full details: Domain Architecture

Explanation

Pass the Domain Architecture check. The PR changes only pure IR comparison helpers. It moves the existing Kani first-byte ordering logic into cycle::support::first_byte_cmp and calls it from sort_utils; both remain private within crate::ir. The changed files add no HTTP, SQL, ORM, filesystem, transport, persistence, or adapter dependency, and the diff introduces no domain-policy leakage.

Full details: Observability

Explanation

Classify the observability check as PASS. Restrict the change to a Kani-gated refactor: first_byte_cmp contains the same first-byte and empty-string ordering logic, and path_cmp delegates to it. Keep the non-Kani path_cmp unchanged as left.cmp(right). The diff adds no production operational behaviour, process or service boundary, logging, metrics, tracing, alerts, retries, or resource-management changes. No additional observability is required.

Full details: Security And Privacy

Explanation

Pass the Security and Privacy check. The pull request changes only Kani-gated string comparison and delegates path_cmp and string_cmp to the private first_byte_cmp helper. The diff adds no secrets, credentials, authentication or authorization logic, permissions, external I/O, command construction, deserialization, logging, telemetry, or data exposure. The helper retains pub(in crate::ir) visibility, and the standard-build comparison remains unchanged.

Full details: Performance And Resource Use

Explanation

Accept the change for this check. The diff only extracts the existing Kani first-byte comparison into first_byte_cmp. The helper uses borrowed &str values and as_bytes().first(), so it adds no allocation, clone, I/O, loop, or unbounded storage. Kani path_cmp and string_cmp retain the same constant-work comparison and empty-string handling. The insertion sort, call counts, and standard-build path_cmp behaviour are unchanged.

Full details: Concurrency And State

Explanation

Pass this check. The commit changes only comparison helper wiring in src/ir/cycle_support.rs and src/ir/sort_utils.rs. It adds no shared mutable state, locks, tasks, channels, globals, or asynchronous execution. The ordering change is a pure, stateless comparator for bounded Kani inputs, not a concurrent processing guarantee. No explicit concurrency or state failure condition applies.

Full details: Architectural Complexity And Maintainability

Explanation

Pass this check. The change adds one small first_byte_cmp helper in the existing cycle::support boundary and gives it an immediate second consumer in sort_utils. It removes the exact duplicated Kani comparison, preserves the existing path_cmp and standard-build branches, adds no dependency or architectural layer, and keeps visibility at pub(in crate::ir). The import path remains acyclic: manifest sorting depends on cycle support, while cycle support does not depend on manifest code. The parent-to-HEAD diff confirms that only these two helper implementations changed.

Full details: Rust Compiler Lint Integrity

Explanation

Pass. The pull request adds no #[allow(dead_code)], #[allow(unused_imports)], #[allow(unused)], broad #[expect], artificial anchors, or new clone calls. Under cfg(kani), first_byte_cmp has two real callers: path_cmp and string_cmp. The import is also Kani-gated and is used by string_cmp. The helper keeps the existing pub(in crate::ir) internal boundary, and the diff only removes duplicated comparison code. No unnecessary ownership work or stale helper surface is introduced.

  • Fix all pre-merge checks with AI
✨ 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 issue-576-deduplicate-private-ir-sorting-and-cycle-support-helpers

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

@sourcery-ai

sourcery-ai Bot commented Aug 24, 2026

Copy link
Copy Markdown
Contributor
Reviewer's guide (collapsed on small PRs)

Reviewer's Guide

The PR centralizes the Kani-only first-byte comparison used for IR paths and manifest rule names in the cycle support module, exposing it only within crate::ir and preserving standard-build behavior, ordering, and existing verification structure.

Flow diagram for shared Kani IR comparison helper

flowchart LR
    CycleSupport["cycle::support"] --> FirstByteCmp["first_byte_cmp(left, right)"]
    PathCmp["path_cmp(left, right)"] --> FirstByteCmp
    StringCmp["from_manifest_support::string_cmp(left, right)"] --> FirstByteCmp
    StandardPathCmp["standard path_cmp uses left.cmp(right)"]
Loading

File-Level Changes

Change Details Files
Expose the cycle support module within crate::ir so its Kani-specific comparison helper can be reused without making it public outside the crate.
  • Change the support module visibility to pub(super).
  • Broaden comparison helper visibility to pub(in crate::ir) while preserving existing standard and Kani configurations.
src/ir/cycle.rs
src/ir/cycle_support.rs
Extract the bounded first-byte ordering logic into a shared Kani-only helper and retain path comparison as a thin adapter.
  • Add first_byte_cmp(&str, &str) with the existing empty/non-empty and byte-order behavior.
  • Delegate Kani path comparison to the shared helper without changing the cap-split structure or standard-build ordering.
src/ir/cycle_support.rs
Replace the manifest rule-name comparison duplicate with the shared IR helper.
  • Import the helper only under Kani.
  • Delegate Kani string sorting to first_byte_cmp while leaving the standard comparator unchanged.
src/ir/from_manifest_support.rs

Assessment against linked issues

Issue Objective Addressed Explanation
#576 Deduplicate the private comparison and sorting helpers shared between the IR sorting and cycle-support code, including the Kani-specific bounded comparison logic. The PR successfully shares the Kani first-byte comparison between cycle paths and manifest rule names, but it does not modify or demonstrate deduplication of the helpers in src/ir/sort_utils.rs. Therefore, it does not fully address the issue's broader sorting-helper deduplication objective.
#576 Create a narrowly scoped internal module boundary for sharing the helpers without widening public API visibility.
#576 Preserve standard-build and Kani comparison semantics while validating the refactor with formatting, lint, tests, type checking, and Kani checks.

Possibly linked issues


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

codescene-access[bot]

This comment was marked as outdated.

codescene-access[bot]

This comment was marked as outdated.

Move the bounded first-byte comparison into cycle support so manifest
rule sorting and cycle path ordering use one Kani-specific implementation.

Keep the helper visible only within `crate::ir`; standard-build ordering
and the public API remain unchanged.
@leynos
leynos force-pushed the issue-576-deduplicate-private-ir-sorting-and-cycle-support-helpers branch from 044acad to 7c2c8bd Compare August 27, 2026 00:16
@leynos
leynos marked this pull request as ready for review August 27, 2026 00:17

@sourcery-ai sourcery-ai Bot left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry @leynos, you've used your own review budget of 250,000 diff characters for the last 7 days.

You can request another review in 8 hours and 48 minutes by commenting @sourcery-ai review. Upgrade to get a review now.

codescene-access[bot]

This comment was marked as outdated.

@coderabbitai coderabbitai Bot added the Issue label Aug 27, 2026

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: 7c2c8bdb0c

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment thread src/ir/cycle_support.rs
let left = left.as_str().as_bytes();
let right = right.as_str().as_bytes();
match (left.first(), right.first()) {
pub(in crate::ir) fn first_byte_cmp(left: &str, right: &str) -> Ordering {

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P1 Badge Document the shared comparison abstraction

This extraction turns cycle-local comparison logic into a shared crate-IR helper consumed by both cycle paths and manifest rule sorting, but the commit does not record its ownership boundary, permitted call-sites, or composition rules in the appropriate architecture, design, or developer documentation. Add that repository-level documentation so future IR code can determine whether and how this Kani-only abstraction should be reused.

AGENTS.md reference: AGENTS.md:L111-L119

Useful? React with 👍 / 👎.

@codescene-access codescene-access Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No quality gates enabled for this code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Deduplicate private IR sorting and cycle-support helpers

1 participant