[AdaWorldAPI]

Stage 3 of D-DRMC

New lab-only law/recipe metadata and six tests. It separates (a) a reusable mathematical shape+law revision independent of ClassId/source, (b) an externally claimed proof receipt, (c) the compiled target/ABI artifact, (d) the current witnessed DR64 operand, and (e) independent effect authorization.

Negative tests reject mismatched semantic axes, unverified conjectures, missing proof/code identities, changed law or target ABI, and any proposal/effect conflated with pure mathematics. One positive test admits the SAME law across two different class/method identities while preserving their own bound operands.

Not claimed: proof verification, scientific generalization, runtime compilation or execution. CheckedByExternalAuthority is caller asserted and needs real trusted checker attestation before production; merged #1690–#1696 E1 and #1698 owners remain untouched. Tests authored, not run (no Cargo here). Stacked on #1702; no new hot engine or opcodes.

[coderabbitai]

Important

Review skipped

Auto reviews are disabled on base/target branches other than the default branch.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ 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: d2a049d9-f8c3-4a2c-b5ed-5a951eb4beab

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

• 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 Summary

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

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-22T14:59:32.093716Z	f0b0f28	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.

[AdaWorldAPI]

Pushed 55f88ef4 and b14dc037 here. They apply coresearch item X15 (operator-chosen) and X17 for the recipe fixtures:

• Removed ProofDisposition::CheckedByExternalAuthority (a flag the caller set) and the caller-supplied proof digest.
• ProofReference now has private fields and a single constructor, rechecked(law, ReplayCapsule). It requires that the capsule proves law.statement (Stage B's SemanticKey) and re-runs ReplayCapsule::recheck. A forged nonzero digest used to pass; now it cannot be written at all (a compile_fail doctest covers this). A real proof of a different statement returns ProofOfOtherStatement.
• The CompiledReference target is Stage B's TargetAbi.
• The crate now depends on egglog-r2il-probe. That brings in egglog and ogar-loco from git and ndarray through the sibling patch.

Two limits, also stated in RECIPE_ADMISSION.md:

1. Stage B proves exact-integer substitution statements only, and no checker exists for Boolean-DR64 laws. The tests therefore pair a DR64 law shape with E1's statement to exercise the plumbing. That pairing does not claim E1 proves anything about DR64.
2. Disabling the recheck call leaves every test green, because a capsule can only come from certify in-process. A test for that path belongs with a future capsule loader.

---

Generated by Claude Code

[AdaWorldAPI]

Correction to my previous comment. 55f88ef4 was wrong in two ways:

• It made ReplayCapsule::recheck the proof authority.
• It paired a DR64 law shape with Stage B's scalar E1 statement.

ca88feaf replaces it.

How the responsibilities split:

• egglog derives equivalences from admitted laws and checks its own proofs.
• Law admission owns the assumptions a law holds under.
• A certified-compiler boundary issues a reusable certificate, after both of those and a lowering check.
• ReplayCapsule is replay and audit evidence for Stage B's E1 substitution language only.

What changed:

• RecipeCertificate is opaque: it has no public constructor and no status field. A compile_fail doctest covers this. The caller-set CheckedByExternalAuthority flag and the caller-supplied digest stay removed.
• No certified-compiler boundary exists for Boolean-DR64 laws. admit_recipe runs every metadata check (capability, shape, law identity, code identity, target) and then refuses with NoCertifiedCompiler. Making certify return a certificate turns the cross-class test red.
• The egglog-r2il-probe dependency and the ndarray patch are gone. E1 stays Stage B's own artifact.

The candidate next milestone is recorded as open on the board entry; it is a hypothesis, not built. It is associativity of Boolean relation composition over compatible ClassView domains, plus a specialization-selection gate to be measured against a general relational baseline.

---

Generated by Claude Code