Repository navigation
dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8) - #1740
Merged
Merged
Conversation
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configuration
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. Comment |
… X8) Committed before any code. Lab only (dr-math-binding-probe). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…ame (X8) The certificate now records the query it answers (source_digest) and its compiled step list. execute_certified refuses an ABI mismatch, an order the certificate does not cover, and a chain of another length; otherwise it runs the stored steps without calling egglog. A thread-local counter on prove_equation lets the hit path assert zero egglog calls. tests/x8_fresh_frame.rs: 5 proposed orders certified on frame 1, all executed on frames 2 at densities 0/4/32/63, equal to an independent pair-enumeration oracle and to Chain::eval; commutation refused at certification; WrongTarget, NotCertifiedQuery, NotThisChain refused. Lab only. Pre-registration: .claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
AdaWorldAPI
force-pushed
the
lab/drmc-l1-x8-fresh-frame-20261023
branch
from
October 23, 2026 10:47
8f2ab13 to
221aeff
Compare
entries_index.py takes the first id in an entry's heading. Both L1 headings named D-DRMC-5, which #1707's entry already holds, and the structural falsifier rejected the duplicate. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
AdaWorldAPI
marked this pull request as ready for review
October 23, 2026 10:53
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
…frame-20261023 # Conflicts: # .claude/board/entries/README.md
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
…certified-compiler row D-TGA-5D said In PR; #1739 merged as 9a458ca. X8: #1740 ran the fresh-frame half; the catalogue multi-binding half is untouched. Certified-compiler row: certify_reassociation (#1707) is an issuer; the single-operand admit_recipe path still refuses. Independent checker, second law and prover revision are still missing. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
… substrate Documentation only. ONNX GraphProto stays the graph at the membrane; no new AST, rewrite pass or interpreter. relalg takes only the Boolean/compare/reduce fragment; value maths has no existing home (OP-ONNX-1, operator). Value-indexed ops are refused under ADMISSION B; no float law is admitted; certified applies only to egglog-proved Boolean-Distinct composition associativity (#1707, #1740). The original DR64³ plan was not found (0 files; branch and PR search negative). The DR64³ section is a new, labelled proposal. Open points OP-ONNX-1..14. Board: STATUS_BOARD D-ONNX-0/1/3, INTEGRATION_PLANS, entry 2026-10-23-d-onnx-relalg-cap-s0, entries index regenerated. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
This was referenced Oct 23, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
Board conflicts resolved, keeping both sides: - STATUS_BOARD: the D-DRMC section from #1742 and the D-ONNX section. - PR_ARC_INVENTORY: #1742's entries for #1740 and #1741 replace this branch's catch-up versions; the #1726-#1739 catch-up stays. - LATEST_STATE: this branch's "main after #1741" text, which now has per-PR records for #1726-#1739. entries/README.md regenerated with entries_index.py. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Lab only (
crates/dr-math-binding-probe). It changes no production crate and no contract type. Authorized by the operator as CC2's L1. Coordinated on EXO-50.What it adds
RecipeCertificatenow recordssource_digest, which identifies the query it answers, and its compiled step list. These are separate from the law reference,compiled_digestand the proof text.execute_certified(cert, chain, requested, runtime_abi)refuses three cases:WrongTarget: an ABI mismatch;NotCertifiedQuery: an order the certificate does not cover;NotThisChain: a chain of another length.Otherwise it runs the stored steps and never calls egglog.
A thread-local egglog call counter, incremented on
prove_equation, so tests can assert zero egglog calls on the hit path.Evidence
Pre-registration was committed first, in e55991f. The result entry is
.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md.tests/x8_fresh_frame.rs: 7/7 pass.Chain::eval.Disable runs D1, D2 and D3 each turned their named test red.
Measured (reported, not gates):
Checks: the full crate test suite, clippy
-D warningsand fmt are clean.Not shown
Generated by Claude Code