From 7db63991c7c01c1e9bfca5672bb3ded513ee307e Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 09:11:37 +0200 Subject: [PATCH 1/2] docs(math-foundry): retain six-PR review and falsifier gaps --- crates/egglog-r2il-probe/REVIEW_1690_1695.md | 88 ++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 crates/egglog-r2il-probe/REVIEW_1690_1695.md diff --git a/crates/egglog-r2il-probe/REVIEW_1690_1695.md b/crates/egglog-r2il-probe/REVIEW_1690_1695.md new file mode 100644 index 000000000..1a6c8c1e0 --- /dev/null +++ b/crates/egglog-r2il-probe/REVIEW_1690_1695.md @@ -0,0 +1,88 @@ +# Review of #1690–#1695: preserve merged-stack provenance and complete the mathematical compiler seams + +**Review date:** 2026-10-22. **Scope:** current `main` compared to the exact GitHub PR metadata and the #1695 head branch; selected source-level inspection of `egglog-r2il-probe`, `perturbation-sim::outage_oracle`, Stage A/B board entries and `thought-git-probe::receipt`. This is **not** a successful local Cargo run (Rust toolchain unavailable in reviewer environment). Separate observed repository facts from research recommendations. + +## Critical integration finding and recovery + +GitHub marks [#1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693), [#1694](https://github.com/AdaWorldAPI/lance-graph/pull/1694) and [#1695](https://github.com/AdaWorldAPI/lance-graph/pull/1695) as merged. But their targets differ: + +- #1693: `lab/math-foundry-1-proof-replay-20261022` -> **main**. +- #1694: `lab/math-foundry-2-certified-catalogue-20261022` -> **#1693 feature branch**. +- #1695: `lab/math-foundry-3-heritage-study-20261022` -> **#1694 feature branch**. + +As inspected, **main had `artifact.rs` and `tests/replay.rs`, but lacked `catalogue.rs`, `heritage.rs`, both associated integration tests, `HERITAGE_STUDY.md` and corresponding `pub mod` declarations**. Merely reading merged PR status substantially overstates deployed integration. + +**Recovery owner:** [#1696](https://github.com/AdaWorldAPI/lance-graph/pull/1696) is the canonical *separate draft integration PR* for the six absent catalogue/heritage files. The present review document changes no executable code. The #1696 file SHA comparison and the excluded probe's targeted tests remain required gates. + +**Regression requirement for stacked PRs:** Require that *all expected file paths appear under the intended final integration branch* before marking a staged program delivered. Mark stacked child PR merge-to-feature as `integrated_into_parent`, not as `shipped_on_main`. Revalidate after parent merge. The ordinary repository build/test jobs do not establish coverage for the separate `[workspace]` `egglog-r2il-probe`. + +## Review by PR and missing connections + +| PR | Directly established | Open, not established | +|---|---|---| +| #1690 | MORK `query_multi` oracle behind plain Lance value boundary; egglog E1 exact substitution, bounded scheduling, checked egglog proof, R2IL scalar `INT_MULT`, independent i128 value comparison. | E2–E5, production source bindings, general optimizer, memory/sharing study and cold compile economics; MORK callback/derivation count is not SQL BAG semantics without explicit de-dup policy. | +| #1691 | Standalone K3 site-service scalar oracle with distinct grid, backup and telecom signals; source-generation and stable focus guard. | No measured site↔bus mapping, independent grid/telecom telemetry, graph-risk-to-site-power inference, egglog/R2IL extraction or observed-outage validation. `grid_status` in legacy A10H data is a synthetic label derivative, not a fresh observation. | +| #1692 | Three source-attributed Tatlock `.arxiv` research notes, **documentation only**. | Relational e-matching, Ruler/Enumo, babble anti-unification, Small Proofs, Chassis or Lakeroad are not integrated just because they are studied. | +| #1693 | In-memory replay capsule, deterministic re-egglog `recheck`, proof/extraction/step-list consistency, no egglog on saved `execute`. | No durable certificate, independent proof checker, trusted artifact import, pinned egglog/compiler version or cryptographic identity. Proof text stability across compiler revisions is not guaranteed. | +| #1694 | *Recovering via this PR*: in-memory semantic-keyed catalogue, caller-supplied binding/ABI witness, economic gate and baseline callback. | A four-input i128 sample check and caller-supplied nanosecond estimates are not universal theorem verification or measured break-even. No source-backed witness attestation; key omits explicitly named algorithm/law-set/version/source identity beyond the caller fields. | +| #1695 | *Recovering via this PR*: synthetic E1 execution, uncertified Leibniz/Euler leads, 27 **candidate** atoms, descriptive meta-study. | 24/27 atoms are not compiled; historical source/authorship and theorem proof are independent evidentiary questions. No real Thought-Git reference, source edition pin, durable provenance, derivative/complex term grammar or replay from disk. | + +## P0: mathematical premise soundness before expanding beyond E1 + +**Observed:** `Problem { premises: Vec }` is public. `encode::setup` indiscriminately `union`s every equation, while `oracle::solve` builds a forward `BTreeMap` and silently skips subsequent definitions of the same `lhs`. Neither `ReplayCapsule::certify` nor `Catalogue::promote` currently validates duplicate/conflicting definitions, attempts to define the freely supplied target, or cycles in a generalized input graph. + +**Concrete counterexample to test (NOT claimed executed):** +```text +goal=z; target=c; premises=[ z=2*c, z=3*c ]; supplied c=7 +``` +These premises conflict for nonzero c. egglog considers both asserted equalities true; the i128 oracle may retain the first equation and ignore the second. A matching sample therefore need not establish that the full equation set is jointly valid for every runtime input. This is **not a flaw in egglog**: it is a missing caller contract for treating equations as universally valid definitions. + +**Minimal next code change, separate owned PR:** validate that `target_var` is a free parameter, each `lhs` has a unique definition, reachable definitions are acyclic and every dependency needed by the goal resolves to the target or refuses. Reject conflicts **before `union` or promotion**. Add adversarial tests for conflicting duplicate heads, two contradictory paths, `c=2c`, cycles, disconnected premises and benign duplicate equations. Independently check every equation against generated input assignments, including negative and boundary values, rather than trusting the first path. Only then consider reusable arbitrary equation DAGs. Keep #1693's valid E1 behavior unchanged. + +## P1: distinguish mathematical, compiled, binding and execution identities + +The following are different and must not be collapsed into one `SemanticKey` or one vague `certified` flag: + +1. **Math identity**: normalized statement + assumptions + typed domain (Exact / Checked / Wrapping / IEEE, Boolean set / SQL K3+validity / Bag+Distinct) + admitted law IDs and rule versions. A historical attribution is *not* a mathematical assumption. +2. **Compiler identity**: extracted term, R2IL step list, lowering and target/ABI versions, cost objective, egglog engine/checker version, and optional proof DAG/checker receipt. A rendered proof string alone is not a durable independent proof. +3. **Binding identity**: dataset and source snapshot(s), focus, source↔local codebook mapping, typed coordinate domain and attested generations. `BindingWitness { source_generation, scope, coordinate_generation }` is currently caller-supplied lab metadata. Two unrelated sources with the same numeric generation values still must not alias. +4. **Execution identity**: actual inputs, BEFORE/AFTER or independent output oracle, error/refusal codes, physical reads and separate durable commit acknowledgment. `ReplayCapsule::execute` is **not** a write or a source-attested replay. +5. **Historical identity**: edition/source locator, transcription normalization and uncertainty; can be reviewed independently from mathematical formalization or proof. + +Proposed reference-only join shape for EXO-98 / D-TGB-4 (no writer integration here): +```text +TheoremRef(math_id, source_edition?, assumptions, domain) + -> LawProofRef(proof_id, checker_version, typed_law_ids) + -> CompiledPatternRef(r2il_steps_digest, target_abi, compiler_revision) + -> BindingRef(dataset, snapshot, focus, coordinate_codebook, generations) + -> ReplayRef(inputs, result, comparison, error, proof_receipt) + -> CommitRef(optional, real coalesced cycle + durable store witness) +``` +**Never** mistake an equality proof, a call-success result, an unsigned Fold receipt, or `CandidateDirty` for a durable acknowledged commit. Thought-Git's current `Receipt`, `BaseRef`, `ProgramId`, metadata seal and `CommitWitness` already express **different** lifecycle concepts. Link by immutable IDs/references and admission fences rather than putting egglog into Thought-Git's hot cycle. + +## P1: honest fallback and measured economics + +`Catalogue::promote` checks a caller-provided `CostEvidence` where `(baseline_ns-candidate_ns)*expected_reuse > compile_and_certify_ns`. This is a good *lab policy formula* but not self-attesting cost evidence. A false positive can be generated by invented inputs; even honest averages need variance and workload shape. + +**Measure independently**: cold egglog+proof, cold independent oracle/checker, catalogue lookup, binding/attestation, first execution, steady R2IL path, baseline path, runtime refusal/fallback, output materialization and retained proof bytes. Include instruction-cache and e-graph costs for high-width extraction. A cache hit with identical goal and coefficients but wrong source snapshot is a red failure, irrespective of the saved nanoseconds. + +**Required E2 sample**: 256 distinct rules × 4,096 pinned contexts (1,048,576 requested uses), plus deliberately *nonsharing* control. Compare direct relalg normalization/CSE and existing R2IL procedures first; optionally add relational e-matching, babble abstraction reuse and effect-safe extraction **only if those baselines show a real gap**. Quantify amortized net savings and refused/witness-invalidated work. Cold compile cannot be hidden by `CLAUDE.md`'s reporting-budget language. + +## P1/P2: complete the research connections without replacing the runtime + +- **#1690 ↔ #1692:** Ruler/Enumo propose typed rewrite candidates; relational e-matching searches for them; babble suggests template factoring; eggcc requires effect-aware extraction; Small Proofs motivates shared proof DAG; Chassis applies only in explicitly approximate real-number domains. All are **cold** / optional. None authorizes a foreign positional gather or new hot runner. +- **#1691 ↔ #1690:** a pure K3 site equation could become a *new* bounded compilation fixture **after** source version, tower focus and independent power/telecom evidence are resolved; it cannot be evaluated as checked integer E1 or infer causality from historical synthetic labels. +- **#1693 ↔ Thought-Git:** replayable proof equations are not replayable physical thought histories. Use distinct IDs for math proof, compiler recipe, source binding and actual sealed thought receipt; preserve D-TGB-4 ABA, provenance roots, multi-thought coalescing and two-write crash window. +- **#1695 ↔ mathematical heritage:** freeze a licensed primary-source edition and transcribed statement; separately formalize Leibniz with derivative assumptions/quantifiers and Euler with complex exponential definitions; mechanical proof and modern compiled recipe are distinct again. E1 currently witnesses `Const, Var, Multiply` only. +- **relalg/R2IL/Quack boundary:** `lance-graph-contract` is the admitted set-law owner (D-RA-2=A); relalg plans/lower; R2IL is the SIMD polyfill; Quack selects the physical procedure; `mask-risc::execute_into` is the hot executor. E1 is scalar-only, so it does not demonstrate 256-bit mask fusion or a population `SUM`. ADMISSION=B prohibits cross-table foreign-value-directed positional gathers during preparation. + +## Minimum practical gates before calling the full stage delivered + +1. **Restore to main via #1696:** verify that its six recovery changes and the original #1695 test suites are present; run `cargo test --manifest-path crates/egglog-r2il-probe/Cargo.toml`, `cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml -- --check`, and isolated clippy with sibling OGAR/ndarray available. Root CI success does **not** substitute. +2. **Premise validation:** contradictory duplicate/cycle cases fail; independent oracle checks *all* premises and full goal, not the first forward path. +3. **Artifact portability:** serialization → fresh-process import → pinned checker and R2IL replay; reject tampered proof, compiler revision, law ID, input and binding. +4. **Cache soundness:** stale dataset/scope/coordinate, same ordinal/different entity, Bag/Distinct and valid FALSE/NULL/K3 witnesses all fail closed or use trusted fallback. +5. **Cost validity:** E2 measured with sharing/nonsharing controls and accounted cold+warm costs. +6. **Historical honesty:** 27 atoms remain hypotheses and historical claims cannot be upgraded without reviewed source and independent formal theorem proof. + +**Owner boundaries:** this research-only review does not modify `.claude/board/STATUS_BOARD.md` or EXO-50/EXO-98 owner fields; coordinating sessions should update those after the restored files are demonstrably present and tested on `main`. The Stage A gap-matrix claim that no LG crate depends on egglog is stale after Stage B, although its subsequent Stage B entry already documents the correction. Stage A should be retained as a historical snapshot, with a cross-link rather than silently rewritten as current state. From a0b21a122a24c81119a7c8186cdb410736049ddc Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 11:43:44 +0000 Subject: [PATCH 2/2] docs(math-foundry): update #1690-#1695 review with merged #1696 and executed P0 falsifiers #1696 merged (df214bb7), 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 (11ca3fe8), together with the checked-overflow range guard. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/egglog-r2il-probe/REVIEW_1690_1695.md | 30 ++++++++++++++++---- 1 file changed, 24 insertions(+), 6 deletions(-) diff --git a/crates/egglog-r2il-probe/REVIEW_1690_1695.md b/crates/egglog-r2il-probe/REVIEW_1690_1695.md index 1a6c8c1e0..6f9478238 100644 --- a/crates/egglog-r2il-probe/REVIEW_1690_1695.md +++ b/crates/egglog-r2il-probe/REVIEW_1690_1695.md @@ -12,7 +12,14 @@ GitHub marks [#1693](https://github.com/AdaWorldAPI/lance-graph/pull/1693), [#16 As inspected, **main had `artifact.rs` and `tests/replay.rs`, but lacked `catalogue.rs`, `heritage.rs`, both associated integration tests, `HERITAGE_STUDY.md` and corresponding `pub mod` declarations**. Merely reading merged PR status substantially overstates deployed integration. -**Recovery owner:** [#1696](https://github.com/AdaWorldAPI/lance-graph/pull/1696) is the canonical *separate draft integration PR* for the six absent catalogue/heritage files. The present review document changes no executable code. The #1696 file SHA comparison and the excluded probe's targeted tests remain required gates. +**Recovery owner:** [#1696](https://github.com/AdaWorldAPI/lance-graph/pull/1696) was the canonical integration PR for the six absent catalogue/heritage files. + +**Update 2026-10-22: recovered.** #1696 merged into `main` as `df214bb7`. Re-checked on `origin/main`: +- `catalogue.rs`, `heritage.rs`, `HERITAGE_STUDY.md`, `tests/catalogue.rs` and `tests/heritage.rs` are present; +- `src/lib.rs` exports `pub mod catalogue` and `pub mod heritage`; +- the original #1694 and #1695 heads (`4cca545a`, `68043f20`) are ancestors of `main`. + +The excluded probe's targeted tests have since been run locally (release; fmt, clippy and tests). [#1698](https://github.com/AdaWorldAPI/lance-graph/pull/1698) adds the dedicated CI job for them. This review document still changes no executable code. **Regression requirement for stacked PRs:** Require that *all expected file paths appear under the intended final integration branch* before marking a staged program delivered. Mark stacked child PR merge-to-feature as `integrated_into_parent`, not as `shipped_on_main`. Revalidate after parent merge. The ordinary repository build/test jobs do not establish coverage for the separate `[workspace]` `egglog-r2il-probe`. @@ -24,19 +31,30 @@ As inspected, **main had `artifact.rs` and `tests/replay.rs`, but lacked `catalo | #1691 | Standalone K3 site-service scalar oracle with distinct grid, backup and telecom signals; source-generation and stable focus guard. | No measured site↔bus mapping, independent grid/telecom telemetry, graph-risk-to-site-power inference, egglog/R2IL extraction or observed-outage validation. `grid_status` in legacy A10H data is a synthetic label derivative, not a fresh observation. | | #1692 | Three source-attributed Tatlock `.arxiv` research notes, **documentation only**. | Relational e-matching, Ruler/Enumo, babble anti-unification, Small Proofs, Chassis or Lakeroad are not integrated just because they are studied. | | #1693 | In-memory replay capsule, deterministic re-egglog `recheck`, proof/extraction/step-list consistency, no egglog on saved `execute`. | No durable certificate, independent proof checker, trusted artifact import, pinned egglog/compiler version or cryptographic identity. Proof text stability across compiler revisions is not guaranteed. | -| #1694 | *Recovering via this PR*: in-memory semantic-keyed catalogue, caller-supplied binding/ABI witness, economic gate and baseline callback. | A four-input i128 sample check and caller-supplied nanosecond estimates are not universal theorem verification or measured break-even. No source-backed witness attestation; key omits explicitly named algorithm/law-set/version/source identity beyond the caller fields. | -| #1695 | *Recovering via this PR*: synthetic E1 execution, uncertified Leibniz/Euler leads, 27 **candidate** atoms, descriptive meta-study. | 24/27 atoms are not compiled; historical source/authorship and theorem proof are independent evidentiary questions. No real Thought-Git reference, source edition pin, durable provenance, derivative/complex term grammar or replay from disk. | +| #1694 | *Restored to main by #1696 (`df214bb7`)*: in-memory semantic-keyed catalogue, caller-supplied binding/ABI witness, economic gate and baseline callback. | A four-input i128 sample check and caller-supplied nanosecond estimates are not universal theorem verification or measured break-even. No source-backed witness attestation; key omits explicitly named algorithm/law-set/version/source identity beyond the caller fields. | +| #1695 | *Restored to main by #1696 (`df214bb7`)*: synthetic E1 execution, uncertified Leibniz/Euler leads, 27 **candidate** atoms, descriptive meta-study. | 24/27 atoms are not compiled; historical source/authorship and theorem proof are independent evidentiary questions. No real Thought-Git reference, source edition pin, durable provenance, derivative/complex term grammar or replay from disk. | ## P0: mathematical premise soundness before expanding beyond E1 **Observed:** `Problem { premises: Vec }` is public. `encode::setup` indiscriminately `union`s every equation, while `oracle::solve` builds a forward `BTreeMap` and silently skips subsequent definitions of the same `lhs`. Neither `ReplayCapsule::certify` nor `Catalogue::promote` currently validates duplicate/conflicting definitions, attempts to define the freely supplied target, or cycles in a generalized input graph. -**Concrete counterexample to test (NOT claimed executed):** +**Concrete counterexample** (at the time of this review, not executed; see the update below): ```text goal=z; target=c; premises=[ z=2*c, z=3*c ]; supplied c=7 ``` These premises conflict for nonzero c. egglog considers both asserted equalities true; the i128 oracle may retain the first equation and ignore the second. A matching sample therefore need not establish that the full equation set is jointly valid for every runtime input. This is **not a flaw in egglog**: it is a missing caller contract for treating equations as universally valid definitions. +**Update 2026-10-22: executed, reproduced and fixed in #1698** (`11ca3fe8`, pending merge). +- Before the fix, `[z=2*c, z=3*c]` at `c=7` certified **14**. With the two premises swapped it certified **21**. +- The oracle reported agreement both times, because it shared the same first-definition bias. It was not independent on this input. +- `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. +- The same commit closes the checked-overflow gap: `Catalogue` records the input range on which the eager checked baseline cannot overflow, and falls back outside it. Example: `a=-1*c; z=-1*a` at `c=i64::MIN`. +- Both fixes cover the linear E1 language only. + **Minimal next code change, separate owned PR:** validate that `target_var` is a free parameter, each `lhs` has a unique definition, reachable definitions are acyclic and every dependency needed by the goal resolves to the target or refuses. Reject conflicts **before `union` or promotion**. Add adversarial tests for conflicting duplicate heads, two contradictory paths, `c=2c`, cycles, disconnected premises and benign duplicate equations. Independently check every equation against generated input assignments, including negative and boundary values, rather than trusting the first path. Only then consider reusable arbitrary equation DAGs. Keep #1693's valid E1 behavior unchanged. ## P1: distinguish mathematical, compiled, binding and execution identities @@ -78,8 +96,8 @@ TheoremRef(math_id, source_edition?, assumptions, domain) ## Minimum practical gates before calling the full stage delivered -1. **Restore to main via #1696:** verify that its six recovery changes and the original #1695 test suites are present; run `cargo test --manifest-path crates/egglog-r2il-probe/Cargo.toml`, `cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml -- --check`, and isolated clippy with sibling OGAR/ndarray available. Root CI success does **not** substitute. -2. **Premise validation:** contradictory duplicate/cycle cases fail; independent oracle checks *all* premises and full goal, not the first forward path. +1. **Restore to main via #1696** (done: merged `df214bb7`; the targeted tests pass locally, and the dedicated CI job arrives with #1698): verify that its six recovery changes and the original #1695 test suites are present; run `cargo test --manifest-path crates/egglog-r2il-probe/Cargo.toml`, `cargo fmt --manifest-path crates/egglog-r2il-probe/Cargo.toml -- --check`, and isolated clippy with sibling OGAR/ndarray available. Root CI success does **not** substitute. +2. **Premise validation** (done for linear E1 in #1698, pending merge): contradictory duplicate/cycle cases fail; independent oracle checks *all* premises and full goal, not the first forward path. 3. **Artifact portability:** serialization → fresh-process import → pinned checker and R2IL replay; reject tampered proof, compiler revision, law ID, input and binding. 4. **Cache soundness:** stale dataset/scope/coordinate, same ordinal/different entity, Bag/Distinct and valid FALSE/NULL/K3 witnesses all fail closed or use trusted fallback. 5. **Cost validity:** E2 measured with sharing/nonsharing controls and accounted cold+warm costs.