Repository navigation
feat(math-foundry): E1 cold proof capsule and replayable R2IL recipe - #1693
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 |
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. |
This was referenced Oct 22, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
Source-grounded matrix of the math-compiler lab work (#1690/#1693/#1696/#1698/#1707): nothing SHIPPED; independent proof check, counterexample-driven refutation, full-domain lowering validation, second-fresh-binding reuse and Thought-Git linkage ABSENT. 34 tactics audited as a proposal vocabulary (no kernel emits a derivation; 15 unique signatures). Minimal typed ABI reusing existing names; stages S1-S6 with positive/negative/silent/disable tests. Plan only; no implementation. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
This was referenced Oct 23, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 26, 2026
…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
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 26, 2026
…, 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
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.
Stack 1/3 — E1 proof replay capsule
Base: merged #1690 (main). Stage: C1 / D-RFT-2 / E1, lab-only.
Adds
egglog-r2il-probe::artifact::ReplayCapsuleover #1690's existing compiled E1 mathematics. Retains exact premises, checked egglog extraction/proof rendering, and executable R2IL scalar steps.certifyrequires complete saturation, a closed term, a checked equality (via the existing egglog publicprovecommand), and a successful R2IL lowering.recheckregenerates the proof and compares the complete extracted term, rendered proof and program to the retained capsule. Conservative E1 replay check; not a standalone proof verifier or cryptographic artifact.executereuses the saved R2IL steps without calling egglog.replayrechecks before execution and compares to the independent i128 oracle.Not included: durable serialized proof format, 27-atom language, new law admissions, physical-register binding/ABI, production JIT, source writes or changes to contract/R2IL/mask-risc/Thought-Git. No duplicate executor.
Verification: tests authored, not locally executed (this assistant runtime has no Rust toolchain/checkout). CI and code review required. Do not merge autonomously.
Review commands:
cd crates/egglog-r2il-probe && cargo test;cargo fmt --check;cargo clippy --all-targets -- -D warnings.Next stacked PR: certified in-memory catalogue and guarded trusted-baseline fallback (base this branch). EXO-50 ownership claim posted.