From dd03f3bb73ac093baf61cbda8930de7136aebe16 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 09:06:56 +0200 Subject: [PATCH 1/6] ci(math-foundry): run excluded egglog-r2il probe tests --- .github/workflows/egglog-r2il-probe.yml | 70 +++++++++++++++++++++++++ 1 file changed, 70 insertions(+) create mode 100644 .github/workflows/egglog-r2il-probe.yml diff --git a/.github/workflows/egglog-r2il-probe.yml b/.github/workflows/egglog-r2il-probe.yml new file mode 100644 index 000000000..be96d5d7b --- /dev/null +++ b/.github/workflows/egglog-r2il-probe.yml @@ -0,0 +1,70 @@ +name: egglog R2IL mathematical compiler probe +# Own [workspace] excluded from root tests; this is a lab gate, not production admission. +on: + pull_request: + paths: + - 'crates/egglog-r2il-probe/**' + - 'crates/lance-graph-contract/**' + - 'crates/lance-graph-r2il/**' + - 'crates/lance-graph-mask-risc/**' + - '.github/workflows/egglog-r2il-probe.yml' + - 'rust-toolchain.toml' + push: + branches: [main] + paths: + - 'crates/egglog-r2il-probe/**' + - 'crates/lance-graph-contract/**' + - 'crates/lance-graph-r2il/**' + - 'crates/lance-graph-mask-risc/**' + - '.github/workflows/egglog-r2il-probe.yml' + - 'rust-toolchain.toml' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} + cancel-in-progress: true +env: + CARGO_TERM_COLOR: always + CARGO_INCREMENTAL: "0" + CARGO_PROFILE_DEV_DEBUG: "0" + CARGO_PROFILE_TEST_DEBUG: "0" + RUST_BACKTRACE: "1" +jobs: + math-foundry: + name: excluded-crate fmt, clippy and tests + runs-on: ubuntu-24.04 + timeout-minutes: 60 + defaults: + run: + working-directory: lance-graph + steps: + - uses: actions/checkout@v4 + with: + path: lance-graph + persist-credentials: false + - name: Checkout AdaWorldAPI/ndarray (sibling path patch) + uses: actions/checkout@v4 + with: + repository: AdaWorldAPI/ndarray + path: ndarray + persist-credentials: false + - name: Rust toolchain + run: rustup show + - name: Resolve target-cpu=native for this runner + id: cpu + run: | + flags=$(.github/scripts/resolve-native-rustflags.sh) + echo "RUSTFLAGS=$flags" >> "$GITHUB_ENV" + hash=$(printf %s "$flags" | sha256sum | cut -c1-16) + echo "flags=$hash" >> "$GITHUB_OUTPUT" + - uses: Swatinem/rust-cache@v2 + with: + key: cpu-${{ steps.cpu.outputs.flags }} + workspaces: lance-graph/crates/egglog-r2il-probe + - name: fmt + run: cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml --check + - name: clippy + run: cargo clippy --manifest-path crates/egglog-r2il-probe/Cargo.toml --all-targets -- -D warnings + - name: tests + run: cargo test --release --manifest-path crates/egglog-r2il-probe/Cargo.toml From 30f27f95747ea6eff32332cbdb164365fd88156a Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 09:08:23 +0200 Subject: [PATCH 2/6] docs(math-foundry): cross-PR integration and falsifier gates --- crates/egglog-r2il-probe/REVIEW_GATES.md | 63 ++++++++++++++++++++++++ 1 file changed, 63 insertions(+) create mode 100644 crates/egglog-r2il-probe/REVIEW_GATES.md diff --git a/crates/egglog-r2il-probe/REVIEW_GATES.md b/crates/egglog-r2il-probe/REVIEW_GATES.md new file mode 100644 index 000000000..75ae63ec7 --- /dev/null +++ b/crates/egglog-r2il-probe/REVIEW_GATES.md @@ -0,0 +1,63 @@ +# Mathematical foundry integration review, 2026-10-22 + +**Status: REVIEW GATES, not certification or production admission.** This document connects #1689–#1695 and records the falsifiers required to integrate the Stage D/E research branch into `main`. It is a review artifact, not an implementation claim. The branch also adds a dedicated Cargo CI workflow, because `crates/egglog-r2il-probe` is a workspace-excluded lab. + +## Merge topology + +- #1689 and #1692: source harvest, not executable admission. +- #1690: merged into main; MORK query_multi SET oracle and independent answer/cost split, plus egglog exact E1 Stage B. The MORK oracle is not a BAG execution engine; callback counts and deduplicated head tuples have different types. +- #1691: merged into main; separate three-valued Bangladesh site-service scalar oracle with independent grid, backup and telecom inputs. No grid risk becomes a measured tower-down observation. +- #1693: merged into main; E1 cold `ReplayCapsule`. +- #1694: merged into `lab/math-foundry-1-proof-replay-20261022`, not main. +- #1695: merged into `lab/math-foundry-2-certified-catalogue-20261022`, not main. +- This integration review is based on the latter branch after merge commit `67d060134e570c5cc99caa782af8fd6fcbeec5c3`; the catalogue and heritage remain lab-only. + +## Gate P0: mathematical proof is not checked runtime substitutability + +`artifact::ReplayCapsule::certify` proves `Arith::Exact` symbolic identities; `lower::run_steps` executes `INT_MULT` with *checked i64* semantics. For general inputs, a correct exact-integer final value is insufficient to establish that baseline and optimized programs have the same intermediate overflow/refusal behavior. + +**Falsifier E-OVERFLOW-CANCEL:** For an eager checked baseline `a = i64::MAX * c; z = 0 * a`, input `c=2` refuses with overflow; a direct exact reduction of `z` to zero must NOT be accepted as equivalent on this input without an explicit valid-range/effect certificate. Test both `Ok(value)` and `Err(Overflow)` arms against a separately implemented, specified baseline. Do not assume egglog currently selects this reduction: verify extraction and keep a failure witness regardless of its tie-break. + +**Admission:** either a cheaply checkable input-range witness covering every original intermediate step and the compiled steps, or an effect/error-preserving checked extraction. A certificate must include arithmetic domain and baseline evaluation semantics. A four-point i128 sample cannot discharge a quantified proof obligation. Remain in lab until falsified or resolved. + +## Gate P0: contradictory or ambiguous premises + +`Problem.premises` are fed to egglog as unrestricted `union` assertions while `oracle::solve` ignores a premise once its `lhs` is known. Duplicate contradictory equations, cycles and conflicting paths may therefore have no consistent assignment for arbitrary runtime inputs, yet a purely equational proof need not identify that domain restriction. + +**Falsifier E-PREMISE:** `a=2*c; a=3*c` with `c=1` must not become a universally applicable compiled function. Require a coherent constraint/domain witness, or conservatively refuse ambiguous/cyclic/nonfunctional systems. Test duplicate `lhs`, cycles, disconnected premises and order permutation independently of egglog's extraction. + +## Gate P1: cache is currently one entry per SemanticKey + +`catalogue::Catalogue.entries` is `BTreeMap`; ABI and binding witness are stored inside `Entry`, not the map key. A second promotion for the same expression but a different target/binding **replaces** the earlier entry. The guard causes a conservative fallback, but the implementation does not yet demonstrate simultaneous multi-binding reuse. + +**Falsifier E-MULTIBIND:** Promote the same expression for (target A, source generation 1) and (target B, generation 2), then request both. Either both remain separately retrievable, or the spec must label overwrite+fallback as a deliberate single-slot cache. For 256 × 4096 contexts, prefer an immutable `RecipeKey = (canonical term, typed laws, arithmetic domain, checker/toolchain version, target ABI)` and an independent **validated** `BindingKey = (dataset/version, scope, coordinate generation, source roots)`. A witness is supplied by the caller today; no source attestation is performed. + +## Gate P1: independent proof verification and durable identity + +`ReplayCapsule::recheck` regenerates egglog proof text with egglog and compares rendering bytes. That is conservative regeneration, **not** an independent proof checker, a portable proof format or an integrity-authenticated durable certificate. + +**Falsifier E-PROOF:** mutate one premise, law/domain, proof edge, cost/target, lowered step, source root, checker identity or ABI; every material mutation must be rejected by an independently implemented verifier (or exact signed/hash-bound certificate format). A changed pretty-printer must not silently redefine proof validity. Pin the egglog, OGAR, R2IL and law-catalogue identities; branch=`main` git dependencies are not version pins. + +Prefer a canonical typed proof DAG and explicit checker version; keep rendered text as a human-readable annex. Capsule digest, certification verdict and Thought-Git execution/commit receipts are three different objects. + +## Gate P1: economic and execution certification + +`CostEvidence` is provided by the caller and `pays_for_itself` checks a strict arithmetic inequality. This is an in-memory lab policy, not an independent performance measurement or statistical admission. + +**Falsifier E-COST:** measure cold harvest/rewrite/proof-check/lowering plus lookup, binding, execution and fallback at fixed inputs; include a no-sharing competitor, an existing R2IL/relalg baseline, miss/stale/overflow arms, confidence ranges and source/version scope. Benchmark 256 templates × 4096 frames with at least two bindings for one template; measure total time and memory, not only the hot hit. Never relabel a synthetic test `CostEvidence` as empirical data. + +## Gate P1: excluded-crate checks + +The root workspace's green Build/Rust tests do not exercise this excluded crate. `.github/workflows/egglog-r2il-probe.yml` is the new targeted workflow and must finish green on this integration PR (fmt, clippy, release tests). The local Cargo toolchain and sibling ndarray checkout were unavailable to this review; all checks remain unverified until CI reports. + +## Gate P2: historical mathematics, provenance and typed effects + +`heritage::HeritageEntry` keeps source leads and mathematical capsules separate. Keep Leibniz and Euler **uncertified**. A modern formal reconstruction is not a checked historical attribution. Treat the 27 atoms as candidate semantic categories, not 27 machine opcodes or a universal grammar. Its current observed coverage is only `Const/Var/Multiply`. + +The next study must version original source edition/folio, normalized statement, assumptions, theorem/checker, extraction/proof, target/ABI, actual input binding, output/overflow, and cold versus hot costs. D-TGB-4 should store **references** to these artifacts, not megabytes of proof text in each thought, and must keep proof checking, replay evidence and actual `LanceCycleWriter` commit acknowledgement distinct. + +For #1691, reuse the typed **three-state physical oracle** only after independently versioned site/telecom/backup observations. Preserve `Unknown` and contradiction, per-tower GUID/window, and pure-versus-effect ordering. Do not map the synthetic legacy `grid_status` to independent observed grid power. Do not admit external `Gather` or physical side effects via algebraic equivalence. + +## Admission decision + +**Do not auto-merge.** This review enables a real integration diff and a missing CI gate; it does **not** certify the semantic counterexamples above as fixed. Maintain `egglog -> proof/rewrite` strictly cold and `R2IL -> FoldDialect -> mask-risc execute_into` as the permitted execution chain. Promote only after P0 invariants are either proven by witnesses/tests or explicitly restricted to the synthetic E1 admitted input domain. From 766e31467621087515d2b476241a7b7e0e6e0b5a Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 09:12:43 +0200 Subject: [PATCH 3/6] docs(math-foundry): correct stacked-merge status and scalar E1 boundary --- crates/egglog-r2il-probe/HERITAGE_STUDY.md | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/crates/egglog-r2il-probe/HERITAGE_STUDY.md b/crates/egglog-r2il-probe/HERITAGE_STUDY.md index f6e58651d..746329ecb 100644 --- a/crates/egglog-r2il-probe/HERITAGE_STUDY.md +++ b/crates/egglog-r2il-probe/HERITAGE_STUDY.md @@ -1,13 +1,13 @@ # Stage E: mathematical heritage / 27-atom falsifier (lab only) -**Dependency chain:** merged [#1690](https://github.com/AdaWorldAPI/lance-graph/pull/1690) (E1 compiler) → draft Stage C proof capsule (#1693) → draft Stage D catalogue (#1694) → this draft. +**Dependency chain (2026-10-22):** [#1690](https://github.com/AdaWorldAPI/lance-graph/pull/1690) (E1 compiler) and [#1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693) (Stage C capsule) merged into `main`; [#1694](https://github.com/AdaWorldAPI/lance-graph/pull/1694) (Stage D catalogue) merged into the Stage C feature branch, and [#1695](https://github.com/AdaWorldAPI/lance-graph/pull/1695) (this Stage E) into the Stage D feature branch, not into `main`. Draft integration [#1698](https://github.com/AdaWorldAPI/lance-graph/pull/1698) carries the combined lab stack and dedicated excluded-workspace tests; it is not production-admitted. ## What this implements The Rust `heritage` module distinguishes: 1. **Source lead**: an author/work/edition candidate. NOT a reviewed facsimile, historical influence proof or mathematical certification. 2. **Normalized mathematical statement**: a modern reconstruction with its assumptions, not necessarily the author's original proof. -3. **Checked computational artifact**: currently only the synthetic E1 exact-integer substitution, compiled by egglog and replayed through R2IL with independent i128 oracle. +3. **Checked computational artifact**: currently only the synthetic E1 exact-integer substitution, compiled by egglog and replayed through R2IL scalar `FoldDialect` with independent i128 oracle. E1 uses empty planes and scalar `INT_MULT`; it does NOT yet exercise a mask-RISC `execute_into` population fold. An exact symbolic proof is not a proof of checked-i64 intermediate-overflow equivalence for arbitrary inputs (see `REVIEW_GATES.md`). The Leibniz 1684 product-rule and Euler-identity entries are **uncertified source candidates**. Neither is executable, because the current E1 language has only `Num/Var/Def/Mul` and does not express differentiation, complex exponentials or the necessary side conditions. A test refuses both, by design. @@ -48,3 +48,5 @@ A replay recipe should be sufficient to recompute the outcome if the source snap `cd crates/egglog-r2il-probe && cargo test` (requires sibling OGAR and ndarray checkout). No runnable historical theorem is claimed. The three source/sample fixtures remain entirely outside production. + +**Integration check (2026-10-22):** #1698's new isolated Cargo job was triggered and stopped at `cargo fmt --check`; Clippy and tests were consequently skipped on that first run. Formatting and a complete targeted green CI run are open, independent of the semantic gates. The main-workspace checks are not substitutes. From 3e4102330c60c9e6bdf763787bfb857379760179 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 11:17:29 +0000 Subject: [PATCH 4/6] egglog-r2il-probe: rustfmt artifact/catalogue/heritage (unblocks the isolated CI fmt step) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/egglog-r2il-probe/src/artifact.rs | 7 ++-- crates/egglog-r2il-probe/src/catalogue.rs | 7 ++-- crates/egglog-r2il-probe/src/heritage.rs | 18 +++++++--- crates/egglog-r2il-probe/src/lib.rs | 2 +- crates/egglog-r2il-probe/tests/catalogue.rs | 38 ++++++++++++++++----- crates/egglog-r2il-probe/tests/heritage.rs | 2 +- crates/egglog-r2il-probe/tests/replay.rs | 10 ++++-- 7 files changed, 59 insertions(+), 25 deletions(-) diff --git a/crates/egglog-r2il-probe/src/artifact.rs b/crates/egglog-r2il-probe/src/artifact.rs index 4e2bad91f..470679e53 100644 --- a/crates/egglog-r2il-probe/src/artifact.rs +++ b/crates/egglog-r2il-probe/src/artifact.rs @@ -66,8 +66,7 @@ impl ReplayCapsule { let proof = c.proof.ok_or(ReplayRefusal::NoProof)?; // This asks egglog to prove the specific selected equality again, // rather than treating nonempty rendered proof text as certification. - try_prove(problem, Arith::Exact, fuel, &c.extracted) - .map_err(ReplayRefusal::Compiler)?; + try_prove(problem, Arith::Exact, fuel, &c.extracted).map_err(ReplayRefusal::Compiler)?; Ok(Self { problem: problem.clone(), arith: Arith::Exact, @@ -139,8 +138,8 @@ impl ReplayCapsule { pub fn replay(&self, target_value: i64) -> Result { self.recheck()?; let v = self.execute(target_value)?; - let expected = oracle::solve(&self.problem, target_value) - .ok_or(ReplayRefusal::InvalidPremises)?; + let expected = + oracle::solve(&self.problem, target_value).ok_or(ReplayRefusal::InvalidPremises)?; if i128::from(v) != expected { return Err(ReplayRefusal::ResultMismatch { compiled: v, diff --git a/crates/egglog-r2il-probe/src/catalogue.rs b/crates/egglog-r2il-probe/src/catalogue.rs index 4e644f319..34b462163 100644 --- a/crates/egglog-r2il-probe/src/catalogue.rs +++ b/crates/egglog-r2il-probe/src/catalogue.rs @@ -25,7 +25,9 @@ impl From<&Problem> for SemanticKey { Self { goal: p.goal.to_owned(), target: p.target_var.to_owned(), - premises: p.premises.iter() + premises: p + .premises + .iter() .map(|e| (e.lhs.to_owned(), e.coeff, e.rhs.to_owned())) .collect(), } @@ -62,8 +64,7 @@ impl CostEvidence { pub fn pays_for_itself(&self) -> bool { self.candidate_ns < self.baseline_ns && self.expected_reuse > 0 - && u128::from(self.baseline_ns - self.candidate_ns) - * u128::from(self.expected_reuse) + && u128::from(self.baseline_ns - self.candidate_ns) * u128::from(self.expected_reuse) > u128::from(self.compile_and_certify_ns) } } diff --git a/crates/egglog-r2il-probe/src/heritage.rs b/crates/egglog-r2il-probe/src/heritage.rs index 81bed9308..c02b885b6 100644 --- a/crates/egglog-r2il-probe/src/heritage.rs +++ b/crates/egglog-r2il-probe/src/heritage.rs @@ -196,9 +196,15 @@ pub fn analyse(corpus: &[HeritageEntry]) -> MetaStudy { programs.insert(steps.iter().map(Step::mnemonic).collect::>()); for step in steps { match step { - Step::PushConst(_) => { atoms.insert(Atom27::Const); } - Step::PushVar(_) => { atoms.insert(Atom27::Var); } - Step::IntMult => { atoms.insert(Atom27::Multiply); } + Step::PushConst(_) => { + atoms.insert(Atom27::Const); + } + Step::PushVar(_) => { + atoms.insert(Atom27::Var); + } + Step::IntMult => { + atoms.insert(Atom27::Multiply); + } } } } @@ -206,8 +212,10 @@ pub fn analyse(corpus: &[HeritageEntry]) -> MetaStudy { MetaStudy { total_entries: corpus.len(), historical_leads: corpus.iter().filter(|x| x.source.is_some()).count(), - mathematically_certified: corpus.iter() - .filter(|x| x.is_mathematically_certified()).count(), + mathematically_certified: corpus + .iter() + .filter(|x| x.is_mathematically_certified()) + .count(), distinct_compiled_programs: programs.len(), observed_atoms: atoms.into_iter().collect(), } diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs index 62c30aa9b..5c1e6e699 100644 --- a/crates/egglog-r2il-probe/src/lib.rs +++ b/crates/egglog-r2il-probe/src/lib.rs @@ -23,8 +23,8 @@ pub mod artifact; pub mod catalogue; -pub mod heritage; pub mod encode; +pub mod heritage; pub mod laws; pub mod lower; pub mod oracle; diff --git a/crates/egglog-r2il-probe/tests/catalogue.rs b/crates/egglog-r2il-probe/tests/catalogue.rs index 839076d1b..202bec6e2 100644 --- a/crates/egglog-r2il-probe/tests/catalogue.rs +++ b/crates/egglog-r2il-probe/tests/catalogue.rs @@ -6,11 +6,18 @@ use egglog_r2il_probe::catalogue::{ use egglog_r2il_probe::{LowerRefusal, e1_problem}; fn bind() -> BindingWitness { - BindingWitness { source_generation: 1, scope: 42, coordinate_generation: 9 } + BindingWitness { + source_generation: 1, + scope: 42, + coordinate_generation: 9, + } } fn abi() -> TargetAbi { - TargetAbi { revision: 1, target: "r2il-checked-i64".into() } + TargetAbi { + revision: 1, + target: "r2il-checked-i64".into(), + } } fn measured() -> CostEvidence { @@ -59,9 +66,14 @@ fn no_certificate_is_installed_without_economic_gate() { fn changed_coordinates_target_and_semantics_call_baseline() { let mut cache = Catalogue::new(); let p = e1_problem(); - cache.promote( - ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured() - ).unwrap(); + cache + .promote( + ReplayCapsule::certify(&p, 8).unwrap(), + bind(), + abi(), + measured(), + ) + .unwrap(); let mut stale = bind(); stale.source_generation += 1; @@ -69,7 +81,10 @@ fn changed_coordinates_target_and_semantics_call_baseline() { assert_eq!(out.route, Route::Baseline(FallbackReason::BindingChanged)); assert_eq!(out.result, Ok(56)); - let other = TargetAbi { revision: 2, target: "r2il-checked-i64".into() }; + let other = TargetAbi { + revision: 2, + target: "r2il-checked-i64".into(), + }; let out = cache.execute_or(&p, bind(), &other, 7, trusted); assert_eq!(out.route, Route::Baseline(FallbackReason::TargetChanged)); @@ -84,9 +99,14 @@ fn changed_coordinates_target_and_semantics_call_baseline() { fn overflow_must_fallback_without_manufacturing_an_answer() { let mut cache = Catalogue::new(); let p = e1_problem(); - cache.promote( - ReplayCapsule::certify(&p, 8).unwrap(), bind(), abi(), measured() - ).unwrap(); + cache + .promote( + ReplayCapsule::certify(&p, 8).unwrap(), + bind(), + abi(), + measured(), + ) + .unwrap(); let out = cache.execute_or(&p, bind(), &abi(), i64::MAX, trusted); assert_eq!(out.route, Route::Baseline(FallbackReason::CompiledRefused)); assert_eq!(out.result, Err(LowerRefusal::Overflow)); diff --git a/crates/egglog-r2il-probe/tests/heritage.rs b/crates/egglog-r2il-probe/tests/heritage.rs index 93e67b217..192415d0f 100644 --- a/crates/egglog-r2il-probe/tests/heritage.rs +++ b/crates/egglog-r2il-probe/tests/heritage.rs @@ -1,8 +1,8 @@ //! Heritage study cannot confuse attribution with a checked proof. -use std::collections::BTreeSet; use egglog_r2il_probe::heritage::{ Atom27, HeritageEntry, HeritageRefusal, PROPOSED_ATOMS, analyse, sample_corpus, }; +use std::collections::BTreeSet; #[test] fn exactly_27_candidate_atoms_without_a_universality_claim() { diff --git a/crates/egglog-r2il-probe/tests/replay.rs b/crates/egglog-r2il-probe/tests/replay.rs index e7ac12042..8fe16d014 100644 --- a/crates/egglog-r2il-probe/tests/replay.rs +++ b/crates/egglog-r2il-probe/tests/replay.rs @@ -21,7 +21,11 @@ fn missing_premise_and_incomplete_fuel_never_certify() { ReplayRefusal::OpenTerm ); let p = Problem { - premises: vec![Eq { lhs: "z", coeff: 2, rhs: "c" }], + premises: vec![Eq { + lhs: "z", + coeff: 2, + rhs: "c", + }], goal: "z", target_var: "c", }; @@ -35,6 +39,8 @@ fn prior_certification_does_not_make_overflow_a_valid_result() { let capsule = ReplayCapsule::certify(&e1_problem(), 8).expect("E1"); assert_eq!( capsule.replay(i64::MAX), - Err(ReplayRefusal::Execution(egglog_r2il_probe::LowerRefusal::Overflow)) + Err(ReplayRefusal::Execution( + egglog_r2il_probe::LowerRefusal::Overflow + )) ); } From 11ca3fe8803c58d373ad41d422393c2247477a7e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 11:23:06 +0000 Subject: [PATCH 5/6] egglog-r2il-probe: refuse inconsistent premises; certified hits stay 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 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/egglog-r2il-probe/src/artifact.rs | 46 ++++++++ crates/egglog-r2il-probe/src/catalogue.rs | 83 ++++++++++++- crates/egglog-r2il-probe/src/oracle.rs | 124 +++++++++++++++++--- crates/egglog-r2il-probe/tests/catalogue.rs | 74 +++++++++++- crates/egglog-r2il-probe/tests/replay.rs | 5 +- 5 files changed, 313 insertions(+), 19 deletions(-) diff --git a/crates/egglog-r2il-probe/src/artifact.rs b/crates/egglog-r2il-probe/src/artifact.rs index 470679e53..955ee6f73 100644 --- a/crates/egglog-r2il-probe/src/artifact.rs +++ b/crates/egglog-r2il-probe/src/artifact.rs @@ -60,6 +60,10 @@ fn check_compilation(c: &Compiled) -> Result<(), ReplayRefusal> { impl ReplayCapsule { /// Run the cold compiler and require a checked, closed exact result. pub fn certify(problem: &Problem, fuel: usize) -> Result { + // The premises must define the goal as ONE function of the target. + // egglog unions contradictory premises without complaint, and its + // extraction then picks a definition by cost or order. + oracle::coefficients(problem).map_err(|_| ReplayRefusal::InvalidPremises)?; let c = compile(problem, Arith::Exact, fuel); check_compilation(&c)?; let program = lower_steps(&c).map_err(ReplayRefusal::Execution)?; @@ -155,6 +159,48 @@ mod tests { use super::*; use crate::e1_problem; + /// FAILS IF: contradictory premises are certified (in either order). + #[test] + fn contradictory_premises_are_not_certified() { + use crate::Eq; + for premises in [ + vec![ + Eq { + lhs: "z", + coeff: 2, + rhs: "c", + }, + Eq { + lhs: "z", + coeff: 3, + rhs: "c", + }, + ], + vec![ + Eq { + lhs: "z", + coeff: 3, + rhs: "c", + }, + Eq { + lhs: "z", + coeff: 2, + rhs: "c", + }, + ], + ] { + let p = Problem { + premises, + goal: "z", + target_var: "c", + }; + assert_eq!( + ReplayCapsule::certify(&p, 8).map(|_| ()), + Err(ReplayRefusal::InvalidPremises) + ); + } + } + #[test] fn corrupt_proof_and_program_refuse_on_replay() { let good = ReplayCapsule::certify(&e1_problem(), 8).expect("E1"); diff --git a/crates/egglog-r2il-probe/src/catalogue.rs b/crates/egglog-r2il-probe/src/catalogue.rs index 34b462163..a4709b91c 100644 --- a/crates/egglog-r2il-probe/src/catalogue.rs +++ b/crates/egglog-r2il-probe/src/catalogue.rs @@ -9,7 +9,7 @@ use std::collections::BTreeMap; use crate::artifact::{ReplayCapsule, ReplayRefusal}; -use crate::{LowerRefusal, Problem}; +use crate::{LowerRefusal, Problem, oracle}; /// Full source expression signature. Deliberately preserve premise order, /// coefficient, and variable names; no hashes or accidentally merged laws. @@ -81,6 +81,82 @@ pub enum FallbackReason { BindingChanged, TargetChanged, CompiledRefused, + /// The input lies outside [`CheckedRange`]: the eager checked baseline + /// may refuse there, and a certified hit would have answered instead. + OutsideCheckedRange, +} + +/// The inputs on which the eager checked baseline cannot overflow. +/// +/// An exact-integer proof says the compiled program and the premises AGREE +/// as mathematics. It says nothing about the baseline's checked `i64` +/// intermediates: `a = -1*c; z = -1*a` compiles to `1*c`, which answers +/// `i64::MIN` where the baseline overflows computing `a`. Every premise is +/// linear in the target, so each intermediate is `k * x` for a known `k`, +/// and the set of `x` where every intermediate fits `i64` is one interval. +/// Inside it the certified hit and the baseline have the same outcome; +/// outside it the catalogue runs the baseline. +/// +/// The interval covers the eager baseline that evaluates EVERY premise. A +/// caller whose baseline computes something else must not use the catalogue. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct CheckedRange { + pub lo: i64, + pub hi: i64, +} + +impl CheckedRange { + fn of(problem: &Problem) -> Result { + let coeff = oracle::coefficients(problem).map_err(|_| ReplayRefusal::InvalidPremises)?; + let (mut lo, mut hi) = (i128::from(i64::MIN), i128::from(i64::MAX)); + for &k in coeff.values() { + if k == 0 { + continue; + } + // MIN <= k * x <= MAX, solved for x. + let (a, b) = ( + div_ceil(i128::from(i64::MIN), k), + div_floor(i128::from(i64::MAX), k), + ); + let (a, b) = if k > 0 { + (a, b) + } else { + ( + div_ceil(i128::from(i64::MAX), k), + div_floor(i128::from(i64::MIN), k), + ) + }; + lo = lo.max(a); + hi = hi.min(b); + } + // 0 is always inside (k * 0 = 0), so the interval is never empty. + Ok(Self { + lo: i64::try_from(lo).map_err(|_| ReplayRefusal::InvalidPremises)?, + hi: i64::try_from(hi).map_err(|_| ReplayRefusal::InvalidPremises)?, + }) + } + + pub fn contains(&self, x: i64) -> bool { + self.lo <= x && x <= self.hi + } +} + +fn div_floor(a: i128, b: i128) -> i128 { + let q = a / b; + if (a % b != 0) && ((a < 0) != (b < 0)) { + q - 1 + } else { + q + } +} + +fn div_ceil(a: i128, b: i128) -> i128 { + let q = a / b; + if (a % b != 0) && ((a < 0) == (b < 0)) { + q + 1 + } else { + q + } } #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -97,6 +173,7 @@ pub struct Execution { struct Entry { capsule: ReplayCapsule, + range: CheckedRange, binding: BindingWitness, abi: TargetAbi, _cost: CostEvidence, @@ -138,10 +215,12 @@ impl Catalogue { if !cost.pays_for_itself() { return Err(PromotionRefusal::NotAmortized); } + let range = CheckedRange::of(capsule.problem()).map_err(PromotionRefusal::Uncertified)?; self.entries.insert( SemanticKey::from(capsule.problem()), Entry { capsule, + range, binding, abi, _cost: cost, @@ -179,6 +258,8 @@ impl Catalogue { Some(FallbackReason::BindingChanged) } else if &entry.abi != abi { Some(FallbackReason::TargetChanged) + } else if !entry.range.contains(x) { + Some(FallbackReason::OutsideCheckedRange) } else { None }; diff --git a/crates/egglog-r2il-probe/src/oracle.rs b/crates/egglog-r2il-probe/src/oracle.rs index cdf0137d4..3b65fea80 100644 --- a/crates/egglog-r2il-probe/src/oracle.rs +++ b/crates/egglog-r2il-probe/src/oracle.rs @@ -1,36 +1,86 @@ -//! The independent oracle: plain `i128` substitution over the ORIGINAL +//! The independent oracle: plain `i128` arithmetic over the ORIGINAL //! premises. It shares no code with the egglog encoding, the extraction, or //! the lowering; it never sees the extracted term. +//! +//! Every premise is linear in the target, so the oracle works on +//! coefficients: `coeff[v]` is the integer `k` with `v = k * target`. A +//! premise is never skipped. One that defines an already-known variable must +//! AGREE with it, so `[z = 2c, z = 3c]` is refused as inconsistent instead of +//! being answered by whichever premise comes first. use std::collections::BTreeMap; use crate::Problem; -/// Solves the premises forward from `target_var = c` and returns the value of -/// `goal`. `None` when the premises do not connect `goal` to `target_var` -/// (a missing premise), or when an `i128` product would itself overflow. -pub fn solve(problem: &Problem, c: i64) -> Option { - let mut known: BTreeMap<&str, i128> = BTreeMap::new(); - known.insert(problem.target_var, i128::from(c)); - // Each pass can resolve at least one more variable; premises.len() + 1 - // passes reach every variable that is reachable at all. +/// Why the premises do not define the goal as a function of the target. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum OracleRefusal { + /// Two premises give `lhs` different coefficients (this includes a cycle + /// such as `c = 2c`, which only holds at `c = 0`). + Inconsistent { lhs: &'static str }, + /// A premise whose right-hand side the target never reaches. Its meaning + /// would be a constraint on an unknown, not a definition. + Unreachable { lhs: &'static str }, + /// The goal is not reached from the target. + GoalUnreachable, + /// A coefficient left `i128`. + Overflow, +} + +/// `coeff[v]` for every variable the premises define from the target, +/// checking every premise. +pub fn coefficients(problem: &Problem) -> Result, OracleRefusal> { + let mut known: BTreeMap<&'static str, i128> = BTreeMap::new(); + known.insert(problem.target_var, 1); + let mut used = vec![false; problem.premises.len()]; + // Each pass resolves at least one more premise; premises.len() + 1 passes + // reach every premise that is reachable at all. for _ in 0..=problem.premises.len() { let mut progressed = false; - for eq in &problem.premises { - if known.contains_key(eq.lhs) { + for (i, eq) in problem.premises.iter().enumerate() { + if used[i] { continue; } - if let Some(&r) = known.get(eq.rhs) { - let v = r.checked_mul(i128::from(eq.coeff))?; - known.insert(eq.lhs, v); - progressed = true; + let Some(&r) = known.get(eq.rhs) else { + continue; + }; + let k = r + .checked_mul(i128::from(eq.coeff)) + .ok_or(OracleRefusal::Overflow)?; + match known.get(eq.lhs) { + Some(&have) if have != k => { + return Err(OracleRefusal::Inconsistent { lhs: eq.lhs }); + } + Some(_) => {} + None => { + known.insert(eq.lhs, k); + } } + used[i] = true; + progressed = true; } if !progressed { break; } } - known.get(problem.goal).copied() + if let Some(i) = used.iter().position(|u| !u) { + return Err(OracleRefusal::Unreachable { + lhs: problem.premises[i].lhs, + }); + } + if !known.contains_key(problem.goal) { + return Err(OracleRefusal::GoalUnreachable); + } + Ok(known) +} + +/// The value of `goal` at `target_var = c`. `None` when the premises are +/// refused by [`coefficients`] or the value leaves `i128`. +pub fn solve(problem: &Problem, c: i64) -> Option { + coefficients(problem) + .ok()? + .get(problem.goal)? + .checked_mul(i128::from(c)) } #[cfg(test)] @@ -67,4 +117,46 @@ mod tests { }; assert_eq!(solve(&broken, 7), None); } + + fn eq(lhs: &'static str, coeff: i64, rhs: &'static str) -> Eq { + Eq { lhs, coeff, rhs } + } + + fn problem(premises: Vec) -> Problem { + Problem { + premises, + goal: "z", + target_var: "c", + } + } + + /// FAILS IF: contradictory definitions are answered (in either premise + /// order) instead of refused, an agreeing duplicate stops being accepted + /// (two-sided), or a cycle through the target is accepted. + #[test] + fn every_premise_is_checked_not_just_the_first_definition() { + for premises in [ + vec![eq("z", 2, "c"), eq("z", 3, "c")], + vec![eq("z", 3, "c"), eq("z", 2, "c")], + ] { + let p = problem(premises); + assert_eq!( + coefficients(&p), + Err(OracleRefusal::Inconsistent { lhs: "z" }) + ); + assert_eq!(solve(&p, 7), None); + } + let agreeing = problem(vec![eq("a", 2, "c"), eq("z", 4, "c"), eq("z", 2, "a")]); + assert_eq!(solve(&agreeing, 7), Some(28)); + let cycle = problem(vec![eq("c", 2, "c"), eq("z", 1, "c")]); + assert_eq!( + coefficients(&cycle), + Err(OracleRefusal::Inconsistent { lhs: "c" }) + ); + let dangling = problem(vec![eq("z", 2, "c"), eq("z", 3, "q")]); + assert_eq!( + coefficients(&dangling), + Err(OracleRefusal::Unreachable { lhs: "z" }) + ); + } } diff --git a/crates/egglog-r2il-probe/tests/catalogue.rs b/crates/egglog-r2il-probe/tests/catalogue.rs index 202bec6e2..edfe79f70 100644 --- a/crates/egglog-r2il-probe/tests/catalogue.rs +++ b/crates/egglog-r2il-probe/tests/catalogue.rs @@ -108,6 +108,78 @@ fn overflow_must_fallback_without_manufacturing_an_answer() { ) .unwrap(); let out = cache.execute_or(&p, bind(), &abi(), i64::MAX, trusted); - assert_eq!(out.route, Route::Baseline(FallbackReason::CompiledRefused)); + // i64::MAX lies outside E1's checked range (8 * x must fit), so the range + // guard falls back before the compiled program runs; it used to be caught + // one step later as `CompiledRefused`. Either way no answer is made up. + assert_eq!( + out.route, + Route::Baseline(FallbackReason::OutsideCheckedRange) + ); assert_eq!(out.result, Err(LowerRefusal::Overflow)); } + +/// The eager checked baseline: every premise, in dependency order, in checked +/// `i64`. Written here, independently of the probe's oracle and lowering. +fn eager(p: &egglog_r2il_probe::Problem, x: i64) -> Result { + let mut known = vec![(p.target_var, x)]; + for _ in 0..=p.premises.len() { + for e in &p.premises { + if known.iter().any(|(n, _)| *n == e.lhs) { + continue; + } + if let Some(&(_, r)) = known.iter().find(|(n, _)| *n == e.rhs) { + let v = r.checked_mul(e.coeff).ok_or(LowerRefusal::Overflow)?; + known.push((e.lhs, v)); + } + } + } + known + .iter() + .find(|(n, _)| *n == p.goal) + .map(|(_, v)| *v) + .ok_or(LowerRefusal::UnboundVar(p.goal.to_string())) +} + +fn chain(a_coeff: i64, z_coeff: i64) -> egglog_r2il_probe::Problem { + egglog_r2il_probe::Problem { + premises: vec![ + egglog_r2il_probe::Eq { + lhs: "a", + coeff: a_coeff, + rhs: "c", + }, + egglog_r2il_probe::Eq { + lhs: "z", + coeff: z_coeff, + rhs: "a", + }, + ], + goal: "z", + target_var: "c", + } +} + +/// FAILS IF: a certified hit answers where the eager checked baseline refuses +/// (codex P2 on #1698: `a = -1*c; z = -1*a` at `c = i64::MIN`; and +/// `a = i64::MAX*c; z = 0*a` at `c = 2`), or the hit stops being taken on +/// inputs inside the checked range (two-sided). +#[test] +fn certified_hit_never_answers_where_the_checked_baseline_overflows() { + for (p, outside, inside) in [(chain(-1, -1), i64::MIN, 5), (chain(i64::MAX, 0), 2, 1)] { + let mut cache = Catalogue::new(); + let cap = ReplayCapsule::certify(&p, 16).expect("certifies"); + cache.promote(cap, bind(), abi(), measured()).unwrap(); + + assert_eq!(eager(&p, outside), Err(LowerRefusal::Overflow)); + let out = cache.execute_or(&p, bind(), &abi(), outside, |x| eager(&p, x)); + assert_eq!( + out.route, + Route::Baseline(FallbackReason::OutsideCheckedRange) + ); + assert_eq!(out.result, Err(LowerRefusal::Overflow)); + + let hit = cache.execute_or(&p, bind(), &abi(), inside, |_| panic!("baseline on hit")); + assert_eq!(hit.route, Route::Certified); + assert_eq!(hit.result, eager(&p, inside)); + } +} diff --git a/crates/egglog-r2il-probe/tests/replay.rs b/crates/egglog-r2il-probe/tests/replay.rs index 8fe16d014..5e0f50f9c 100644 --- a/crates/egglog-r2il-probe/tests/replay.rs +++ b/crates/egglog-r2il-probe/tests/replay.rs @@ -16,9 +16,12 @@ fn e1_replays_compiled_math_without_a_second_executor() { fn missing_premise_and_incomplete_fuel_never_certify() { let mut missing = e1_problem(); missing.premises.retain(|e| e.lhs != "b"); + // The premise graph is checked before egglog runs: without `b = 2c` the + // goal is unreachable from the target, so this is `InvalidPremises` + // (it used to surface after compiling, as `OpenTerm`). assert_eq!( ReplayCapsule::certify(&missing, 8).unwrap_err(), - ReplayRefusal::OpenTerm + ReplayRefusal::InvalidPremises ); let p = Problem { premises: vec![Eq { From e5b06c09eff8dc8aecf5673ffe53acfd1f7caa12 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 11:23:32 +0000 Subject: [PATCH 6/6] docs(math-foundry): record the two P0 gates as closed for linear E1 Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/egglog-r2il-probe/REVIEW_GATES.md | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/crates/egglog-r2il-probe/REVIEW_GATES.md b/crates/egglog-r2il-probe/REVIEW_GATES.md index 75ae63ec7..6b75f6a9d 100644 --- a/crates/egglog-r2il-probe/REVIEW_GATES.md +++ b/crates/egglog-r2il-probe/REVIEW_GATES.md @@ -61,3 +61,20 @@ For #1691, reuse the typed **three-state physical oracle** only after independen ## Admission decision **Do not auto-merge.** This review enables a real integration diff and a missing CI gate; it does **not** certify the semantic counterexamples above as fixed. Maintain `egglog -> proof/rewrite` strictly cold and `R2IL -> FoldDialect -> mask-risc execute_into` as the permitted execution chain. Promote only after P0 invariants are either proven by witnesses/tests or explicitly restricted to the synthetic E1 admitted input domain. + +## Status after rebase onto main (2026-10-22, #1696 merged) + +Both P0 gates are now closed **for the linear E1 language**, each with a test that fails when its guard is removed. The P1 gates are unchanged. + +- **E-PREMISE: closed.** + - Reproduced first: `[z=2c, z=3c]` at c=7 certified 14, and 21 with the premises swapped; the oracle agreed both times. + - `oracle::coefficients` now checks every premise: + - a second definition must agree; + - a cycle such as `c = 2c` is inconsistent; + - a premise the target cannot reach is refused. + - `ReplayCapsule::certify` refuses such systems with `InvalidPremises` before egglog runs. +- **E-OVERFLOW-CANCEL: closed by an input-range witness.** + - Reproduced first: `a = -1*c; z = -1*a` returned `Ok(i64::MIN)` on a hit where the eager checked baseline overflows (the codex P2), and `a = MAX*c; z = 0*a` returned 0 at c=2. + - `Catalogue::promote` records `CheckedRange`: the inputs on which every premise's intermediate `k * x` fits i64. + - `execute_or` falls back outside it (`OutsideCheckedRange`). + - The witness covers only the eager baseline that evaluates every premise, and only premises linear in the target. A non-linear language needs a new witness.