[AdaWorldAPI]

Stage 5 of the D-DRMC stack. Base is #1708, which lands the stranded stages 1–4 and the charter amendment on main. This is the first law the certified-compiler boundary can certify, per the amended charter.

(R ∘ S) ∘ T = R ∘ (S ∘ T) over OR/AND is established algebra. The probe tests whether the pieces around it preserve it.

What relcomp adds

• Typing. A Chain composes bound DR64 operands only where:
  • each column domain is the next operand's row domain;
  • all operands share one current frame issue, one focus and one scope;
  • every operand is a two-valued Distinct relation (the Boolean semiring).
• Law admission. admit_composition_assoc admits associativity only for BooleanCompose over two-valued Distinct relations. Bag (counting) and three-valued composition are refused. AdmittedLaw has no other constructor; a compile_fail doctest checks this.
• Proof. egglog is given only the admitted rule. It proves every reassociation of a 5-chain and checks its own proofs. Commutation gets no proof, even with both terms in the e-graph.
• Lowering. An order lowers to push/compose steps that raise back to the same order. This is a structural check. The compose kernel is checked separately, against an independent pair enumeration.
• Certificate. certify_reassociation is the first issuer of a RecipeCertificate, which now carries egglog's proof text. It refuses a law reference for another shape, a non-reassociation, and a missing code identity. admit_recipe's single-operand path still has no certifier.

Measured

cargo run --release --example assoc_orders on one dense-to-sparse 5-chain (4-vCPU shared Xeon @ 2.10 GHz):

• All 14 orders compute the same relation.
• Work ranges from 6 414 to 15 310 row-ORs.
• Time per evaluation ranges from about 4.4 to 10.8 µs.
• The cold egglog proof takes about 12.5 ms. It runs outside the fold, so it is reported, not gated.

Checks

• 11 new tests. All existing suites still pass, and the two doctests pass.
• clippy -D warnings and fmt are clean.
• Disable runs: each guard was switched off in turn, and each run fails a test. The guards are:
  • the domain check and the Boolean-Distinct gate;
  • the stale-frame check;
  • the semiring check in law admission;
  • the compose kernel itself;
  • adding a commutation rule, which breaks the refusal test;
  • the certificate's law check and the lowering round-trip.

Not done

• Order selection. The costs above come from evaluating every order, which a selector must not do.
• Certificate rebinding to a second frame (X8).
• GF(2)/M4RI reduction. None is attempted.
• R2IL/Quack wiring.

The crate now depends on egglog from git (public API only); no ndarray patch is needed.

---

Generated by Claude Code

[coderabbitai]

Important

• 🔍 Trigger review

This repository does not receive automatic reviews because it has fewer than 10 stars.

⚙️ Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 284bc66c-ccea-4015-ae73-58afd6599eef

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Warning

Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption.

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

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

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: a554da1cc4

ℹ️ 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".

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-22T17:13:37.451845Z	a554da1	Draft marked ready

ℹ️ 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" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.