[AdaWorldAPI]

Why this PR exists

PRs #1694 and #1695 are reported merged, but they merged into preceding feature branches, not the default branch. main contains #1693 (artifact.rs) and does not contain catalogue.rs, heritage.rs, HERITAGE_STUDY.md, or their tests. This is a base-branch integration correction, not a new implementation.

Diff verified against current main

Exactly six paths: crates/egglog-r2il-probe/{HERITAGE_STUDY.md,src/catalogue.rs,src/heritage.rs,src/lib.rs,tests/catalogue.rs,tests/heritage.rs}. The only existing-file modification is two module exports in src/lib.rs. No core contract/R2IL/Quack/mask-risc/Thought-Git modifications.

Review and release gates

1. Keep this draft pending targeted cd crates/egglog-r2il-probe && cargo test && cargo fmt --check && cargo clippy --all-targets -- -D warnings with pinned sibling OGAR/ndarray, or a dedicated CI job for this excluded crate. Root Build/Rust Tests do not exercise the entire Math Foundry probe.
2. ReplayCapsule::recheck regenerates proof with egglog and compares text; this is not an independent portable proof checker or durable certificate. Preserve the distinction.
3. Catalogue::promote accepts caller-supplied BindingWitness/CostEvidence, including synthetic cost fixtures. Those are lab policy inputs, not trusted source attestation or measured performance. Do not admit production JIT.
4. Semantic keys currently use exact names and premise order, not alpha-equivalent templates. Do not claim cross-context abstraction reuse, 256×4096 speedups, or a universal 27-atom basis.
5. feat(perturbation): distinguish grid and telecom outage causes #1691's domain-specific strong-Kleene outage oracle and MORK D-MPS-9 MORK query_multi oracle + math-compiler Stage A matrix and Stage B (E1) probe #1690 are independent reference semantics, not integrated with E1 arithmetic. JC/R (docs(plan): design R statistical API and formula lowering over JC #1613), egglog/eggcc (docs: harvest egglog, eggcc and 3LA compiler ideas #1689), Tatlock survey (docs: map Tatlock publications to mathematical compiler research #1692), and Thought-Git D-TGB/EXO-98 remain follow-up integrations.
6. Observe existing D-RA-2=A and ADMISSION=B boundaries, including set/bag, NULL/valid FALSE/UNKNOWN, source generation, cross-table gather restrictions, and write acknowledgement separation.

Follow-ups separate from this integration PR

• True independent, versioned proof-certificate checker + reproducible egglog/law ABI pins.
• Typed law/plan/binding cache split and verified source-generation identity/authorization.
• Bounded 256-rule × 4096-context differential with share/no-share, bind/compile/proof/execute/read/scratch telemetry.
• Historical bibliography/formalization and an audit-only Thought-Git link; no claim of independently proven Leibniz/Euler math in this fixture.

Do not merge on green root CI alone.

[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: e65295c9-d99c-496b-a0d1-d648626ad024

• 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.}

[AdaWorldAPI]

Additional P1 correctness gate from post-merge code review: inconsistent premises

crates/egglog-r2il-probe/src/oracle.rs::solve currently skips a premise whenever known.contains_key(eq.lhs), without verifying its equality. Minimal counterexample: a = 2*c; a = 3*c; z = 1*a, with target_var=c and c=7. The oracle takes the first assignment (a=14), silently skips the contradiction (a=21), and can return z=14 instead of refusing inconsistent input. egglog receives both equations as e-class unions; one equality derivation alone does not establish that the full premise set is satisfiable for arbitrary inputs. This breaks the intended independence of ReplayCapsule::replay and Catalogue::promote as guards against contradictory specifications.

Required invariant before promoting arbitrary E1 fixtures: every resolved premise is checked, including duplicate LHS, cycles, and goal==target constraints; contradictory values under an admitted assignment refuse. For a universally reusable symbolic capsule, prove premise consistency/parameterization in the declared integer theory rather than checking only four sample values. Add paired a=2c,a=3c (c=7), a=2a (a=1), consistent duplicate a=2c,a=2c, and a premise-order permutation. Ensure egglog extraction/codec and oracle do not silently certify conflicts.

This is an independent correctness finding, separate from #1696's six-file integration scope. Fix in a follow-up owned by the E1 probe, not by introducing Measure::Scale or changing the hot runtime. Keep #1696 as draft until targeted excluded-crate CI has run.

[AdaWorldAPI]

Additional P1 semantic gap: Exact proof ≠ checked-i64 execution equivalence

laws.rs admits MulAssoc under Arith::Exact, while lower.rs::run_steps always executes through R2IL checked i64 INT_MULT (wrapping alone is refused). artifact::ReplayCapsule::certify checks a proof over exact mathematical expressions and catalogue::promote checks oracle::solve in i128 on four sample inputs. Neither proves preservation of intermediate overflow/refusal behavior of the original checked computation.

Concrete future-E1 negative fixture: b = i64::MAX * c; a = 0 * b, goal a in target c, input c=2. Exact arithmetic says a=0; an egglog re-association/constant fold can emit checked 0*c -> 0. But a faithful checked execution of the original premise order must refuse overflow on i64::MAX * 2. The independent i128 value oracle also returns 0 and cannot catch the removed overflow. More generally, 0*(MAX*2) vs (0*MAX)*2 is equal in ℤ but not observationally equal with checked intermediate operations.

Gate: either (A) explicitly define this compiler's source semantics as unbounded exact integer mathematics with checked i64 only at the final boundary (so there is no claim of checked-source observational equivalence), or (B) require effect/refusal-preserving extraction (eggcc-style) or guards proving intermediate checked operations equivalent to the original order. Add the zero-times-overflow adversary and compare success/error outcomes, not only result integers. No generalized Exact -> checked R2IL promotion without this declaration.

[AdaWorldAPI]

Additional #1690–#1695 source review (coordination, not a request to expand this integration diff)

I verified that #1696's six-file restoration corresponds to the original #1695 head. Please keep the recovery PR minimal and do not merge on root CI alone: the new tests live in crates/egglog-r2il-probe, its own excluded [workspace]. Targeted Cargo test/fmt/clippy remains the admission gate.

New P0 candidate for a separate, owned code correction: Problem { premises: Vec<Eq> } is public; encode::setup asserts every premise with egglog union, but oracle::solve silently skips subsequent equations sharing the same lhs (its known.contains_key(eq.lhs) branch). Neither ReplayCapsule::certify nor Catalogue::promote validates unique definitions, target freedom, or cycles.

Counterexample to pre-register (not executed): goal=z; target=c; premises=[z=2*c, z=3*c], with runtime c=7. The axioms cannot both hold. The oracle's first-definition-wins behavior is not a model of all premises. Before E1 is generalized, reject conflicting/duplicate definitions and cycles (or define and check the intended equational semantics for all input assignments) before calling egglog, and add an independent conflicting-path oracle test. This is a caller/premise semantics problem, not an egglog proof-checker defect.

Additional explicit identity separation: math_id (typed statement/laws) ≠ compiled_pattern_id (R2IL steps, lowering/ABI/checker version) ≠ binding_id (dataset, source snapshot, typed coordinates/codebook/generations) ≠ replay_receipt_id (inputs, outputs/refusal, independent oracle) ≠ commit_witness_id (real sealed write). Existing Thought-Git D-TGB-4 Receipt, BaseRef, ProgramId, metadata seal and CommitWitness are distinct and should be linked by immutable references only, outside the hot loop. Historical edition/authorship is a sixth, orthogonal provenance track.

What is not established by #1690–#1695: independent durable proof certificates, authenticated binding witnesses, accurate measured CostEvidence, 256×4096 amortization, general mathematical equivalence or 27-atom universality. E1 remains scalar checked i64 R2IL with exact-integer egglog proof, not a benchmark of mask fusion or a SUM/lane population operator. #1691 K3 outage and #1692 Tatlock research are independent prerequisites, not E1 extensions already integrated.

I placed a full review matrix, counterexample, proposed reference schema and falsifier plan in a read-only review file on the superseded branch: REVIEW_1690_1695.md. No owner-controlled board files or executors changed there.

[AdaWorldAPI]

Coordination update: the full cross-PR review is now proposed separately as docs-only #1699, adding only crates/egglog-r2il-probe/REVIEW_1690_1695.md against main. No overlap with #1696's six restored source/test paths. The temporary duplicate recovery #1697 has been closed unmerged. Please retain #1696 as the only integration PR, and treat the conflicting-premise falsifier documented in #1699 as a distinct future guarded-input correction, not as a hidden amendment to this recovery.

[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-22T10:19:17.881018Z	68043f2	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.