Repository navigation
Integrate #1694/#1695 into main with isolated math-foundry CI and semantic gates - #1698
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 |
|
Targeted CI result from the first integration head ( |
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. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: bbf10fe35c
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…isolated CI fmt step) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
…inside the checked range Two P0 gates from REVIEW_GATES.md (and codex P2 on #1698), both reproduced before the fix: - Premises. `oracle::solve` skipped any premise whose lhs was already known, so `[z=2c, z=3c]` certified 14 at c=7 and, with the premises swapped, 21; the oracle agreed both times because it had the same first-wins bias. `oracle::coefficients` now checks every premise (a second definition must agree; a cycle like c = 2c is inconsistent; a premise the target cannot reach is refused), and `ReplayCapsule::certify` refuses such systems with `InvalidPremises` before egglog runs. - Checked range. An exact-integer proof does not preserve the checked baseline's intermediate overflows: `a = -1*c; z = -1*a` compiles to `1*c` and answered i64::MIN on a cache hit where the eager checked baseline overflows (and `a = MAX*c; z = 0*a` answered 0 at c=2). Every premise is linear in the target, so `Catalogue::promote` now records the interval of inputs where every intermediate fits i64, and `execute_or` falls back to the baseline outside it (`FallbackReason::OutsideCheckedRange`). Two existing tests re-pinned with the reason: a dropped premise is now `InvalidPremises` (was `OpenTerm` after compiling), and E1 at i64::MAX is now `OutsideCheckedRange` (was `CompiledRefused`); both still refuse. 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
bbf10fe to
e5b06c0
Compare
…xecuted P0 falsifiers #1696 merged (df214bb), so #1694/#1695 are no longer stranded; the contradictory-premise counterexample has been executed (14 vs 21 by premise order) and is fixed for linear E1 in #1698 (11ca3fe), together with the checked-overflow range guard. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
2 participants
Why
#1694 merged into #1693's feature branch, and #1695 into #1694's feature branch, not
main. Their source modules remain absent from the default branch. This draft integrates the lab stages explicitly while withholding production admission.Changes
.github/workflows/egglog-r2il-probe.ymlfor the excluded Cargo workspace (fmt/clippy/release tests).crates/egglog-r2il-probe/REVIEW_GATES.mdwith explicit cross-PR falsifiers.Blocking gates (review findings, not fixes)
i64overflow of an eager checked baseline (e.g.a=i64::MAX*c, z=0*a, c=2). Require an error-preserving extractor or an input-range witness.BTreeMap<SemanticKey,Entry>stores only one ABI/binding per expression; promoting another replaces it rather than demonstrating multi-frame simultaneous reuse.ReplayCapsule::recheckregenerates egglog proofs and compares rendered bytes; an independent durable proof checker and pinned provenance remain open.CostEvidenceis a policy input, not a measured 256×4096 total-cost certificate.Non-goals
No production JIT admission, no hot egglog or MORK, no new R2IL opcodes, no cross-table gathers, no Thought-Git write-path change and no certification of historical attributions.
DRAFT / DO NOT MERGE until the isolated Cargo job passes and P0 semantics have been resolved. I have not run Cargo locally; GitHub CI is the execution gate.