dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8) by AdaWorldAPI · Pull Request #1740 · AdaWorldAPI/lance-graph

AdaWorldAPI · 2026-10-23T10:46:22Z

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

RecipeCertificate now records source_digest, which identifies the query it answers, and its compiled step list. These are separate from the law reference, compiled_digest and 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.

5 orders were certified on frame 1 and executed on new frames at 4 densities.
On every call: 0 egglog calls, and the result equals both an independent oracle and Chain::eval.
Commutation was refused at certification.
All three refusals are pinned.

Disable runs D1, D2 and D3 each turned their named test red.

Measured (reported, not gates):

measure	result
cold certify	15 696 µs
hot reuse	2 142 ns/call
plain eval of the requested order	7 216 ns/call
certificate size	1 284 B

Checks: the full crate test suite, clippy -D warnings and fmt are clean.

Not shown

There is no independent proof checker yet.
The passive proof reference (option B) is to be agreed with CC1 before any contract PR.
No second law yet.

Generated by Claude Code

coderabbitai · 2026-10-23T10:46:30Z

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: 04728e14-4408-475e-b302-daeeb6c11793

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

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

… 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

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

chatgpt-codex-connector · 2026-10-23T10:54:03Z

Codex Review Summary

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

Review	Status	Commit	Review trigger
📝 Code Review	🔄 Running since 2026-10-23T10:53:59.350975Z	`09d43eb`	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.

…frame-20261023 # Conflicts: # .claude/board/entries/README.md

…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

… 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

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

…, binding store, traceroute) Architecture compatibility note only; P2 scope unchanged, nothing new authorized. References D-DRMC-0, D-NFR/D-NFC, D-ONNX-RELALG-CAP, D-DR3 and D-RPR instead of restating them. Records the existing lab precedents on main: typed DR64 binding (#1701, integrated by #1708), law/recipe/binding separation (#1703), certified recipe reuse on a fresh frame without egglog (#1740), witness-refusing populations (#1666) and zero-copy relation lanes (#1659). Corrects P2: a witnessed kept population exists in the lab; a Quack Keep plane still has none. Answers the five P2 compatibility checks and names each missing hook with its existing owner. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX

…endent invalidation falsifier Corrects the binding-store wording: the generalized Quack Binding Store is planned/unbuilt, while numeric binding, RelAlg let reuse (#1649, #1653), witnessed DR populations (#1666), typed DR method binding (#1701/#1708) and compiled mathematical recipes (#1693/#1694/#1707/ #1740) exist in production or lab. Notes #1666 Pop's witness refusal in B.7(5). Replaces "a property change is harmless" with the three-way invalidation rule, and adds the falsifier it needs to the P2 lab: a property read by R's criteria is mutated; the reused R2 keeps 1,032 rows vs 31 fresh and a downstream read differs, silently (`--controls`, seed 0x0D0D_F00D). Disable run red (skipping the mutation fails the non-vacuity assertion). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX

…, P2) Links the existing implementation spine with source and status: #1649, #1653, #1659, #1666, #1681, #1685, #1693, #1694 (landed via #1696/#1698), #1701/#1703 (via #1708), #1707, #1740. Separates production (Quack numeric binding, CompiledProgram, mask-risc terminals, r2il procedures, the contract's SetProgram type) from lab. Names the smallest missing seams with their owners: D-NFR-1 frame on a bound Query (needs NFR-OP-1), an input-generation dependency witness for kept planes (binding store; witness type is NFR-OP-3, so no new Pop), and the D-NFR-2 codebook generation. Shows how one certified recipe applies to many witnessed bindings without copying populations, re-reads the DuckDB harvest against what exists, and states the authorization boundary. Documentation only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX

claude added 3 commits October 23, 2026 10:47

board: pre-register L1 (D-DRMC-5 certificate reused on a fresh frame,…

f1d5f1d

… 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

board: L1 result entry (X8 fresh-frame reuse measured)

221aeff

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 8f2ab13 to 221aeff Compare October 23, 2026 10:47

AdaWorldAPI marked this pull request as ready for review October 23, 2026 10:53

Merge remote-tracking branch 'origin/main' into lab/drmc-l1-x8-fresh-…

95b2cb1

…frame-20261023 # Conflicts: # .claude/board/entries/README.md

AdaWorldAPI merged commit c42140b into main Oct 23, 2026
5 checks passed

AdaWorldAPI mentioned this pull request Oct 23, 2026

lab(drmc): certificate keeps egglog's ProofStore + ProofId, not its rendering; L1 board records #1742

Merged

AdaWorldAPI mentioned this pull request Oct 24, 2026

docs(D-SAG-6): Rust Codegraph → Mathematics → Logic → Tracert, prompt and board #1760

Merged

AdaWorldAPI mentioned this pull request Oct 26, 2026

D-DR256-WHERE: capstone, DR64³ inventory, P2 Quack-path lab, evidence reconciliation, D-NFR-1 ownership correction #1792

Merged

Navigation Menu

Repository navigation

dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8) - #1740

dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8)#1740
AdaWorldAPI merged 5 commits into
mainfrom
lab/drmc-l1-x8-fresh-frame-20261023

AdaWorldAPI commented Oct 23, 2026

Uh oh!

coderabbitai Bot commented Oct 23, 2026 •

edited

Loading

Uh oh!

chatgpt-codex-connector Bot commented Oct 23, 2026

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

AdaWorldAPI commented Oct 23, 2026

What it adds

Evidence

Not shown

Uh oh!

coderabbitai Bot commented Oct 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

chatgpt-codex-connector Bot commented Oct 23, 2026

Codex Review Summary

Uh oh!

Uh oh!

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

coderabbitai Bot commented Oct 23, 2026 •

edited

Loading