Share private IR comparison helper (#576) - #587
Conversation
|
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:
No actionable comments were generated in the recent review. 🎉 ℹ️ Recent review info⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Pro Plus Run ID: 📒 Files selected for processing (2)
🔗 Linked repositories identifiedCodeRabbit considers these linked repositories for cross-repo context during reviews:
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
Refs WalkthroughExtract the Kani first-byte string comparison into ChangesKani comparison deduplication
Suggested labels: Poem
🚥 Pre-merge checks | ✅ 19 | ❌ 1❌ Failed checks (1 warning)
✅ Passed checks (19 passed)
Full details: Linked Issues checkExplanation The changes satisfy issue 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 Full details: User-Facing DocumentationExplanation Pass this check. The committed diff changes only Full details: Developer DocumentationExplanation The pull request introduces an internal API and changes an internal support-module boundary without updating Resolution Update Full details: Module-Level DocumentationExplanation Pass the module-level documentation check. The PR changes no module declarations and adds no module. Both modified modules already carry 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 Full details: Testing (Property / Proof)Explanation Treat the check as passed. The diff changes only Full details: Testing (Compile-Time / Ui)Explanation Pass the compile-time/UI check. The change only refactors existing Full details: Unit ArchitectureExplanation Keep this change as a PASS. The diff extracts the existing Kani first-byte comparison into Full details: Domain ArchitectureExplanation Pass the Domain Architecture check. The PR changes only pure IR comparison helpers. It moves the existing Kani first-byte ordering logic into Full details: ObservabilityExplanation Classify the observability check as PASS. Restrict the change to a Kani-gated refactor: Full details: Security And PrivacyExplanation Pass the Security and Privacy check. The pull request changes only Kani-gated string comparison and delegates Full details: Performance And Resource UseExplanation Accept the change for this check. The diff only extracts the existing Kani first-byte comparison into Full details: Concurrency And StateExplanation Pass this check. The commit changes only comparison helper wiring in Full details: Architectural Complexity And MaintainabilityExplanation Pass this check. The change adds one small Full details: Rust Compiler Lint IntegrityExplanation Pass. The pull request adds no
✨ Finishing Touches📝 Generate docstrings
🧪 Generate unit tests (beta)
Comment |
Reviewer's guide (collapsed on small PRs)Reviewer's GuideThe 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 Flow diagram for shared Kani IR comparison helperflowchart 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)"]
File-Level Changes
Assessment against linked issues
Possibly linked issues
Tips and commandsInteracting with Sourcery
Customizing Your ExperienceAccess your dashboard to:
Getting Help
|
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.
044acad to
7c2c8bd
Compare
There was a problem hiding this comment.
💡 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".
| 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 { |
There was a problem hiding this comment.
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 👍 / 👎.
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