diff --git a/crates/egglog-r2il-probe/HERITAGE_STUDY.md b/crates/egglog-r2il-probe/HERITAGE_STUDY.md new file mode 100644 index 000000000..f6e58651d --- /dev/null +++ b/crates/egglog-r2il-probe/HERITAGE_STUDY.md @@ -0,0 +1,50 @@ +# 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. + +## 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. + +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. + +## 27-atom hypothesis, not a discovery + +Candidate vocabulary: six term constructors, eight algebra operators, seven relational operators, six derivation constructs. These are *research-level semantic categories*, not R2IL opcodes or claims that 27 operations suffice for all mathematical domains. No atom is considered "covered" unless an independently certified compiled procedure exercises it. Today the synthetic E1 program witnesses just `Const, Var, Multiply`. + +Measure on a future licensed corpus: +- Historical coverage: reviewed editions and unambiguous citations +- Formalization coverage: statements expressed with domain/assumption witnesses +- Proof coverage: mechanically checked lemmas, including independent proof-checker identity +- Lowering coverage: lawful mappings to extant R2IL opcodes/folds +- Minimum description length: vocabulary bytes + compiled corpus bytes; nonsharing control +- Replay cost, proof bytes, binding costs, cache hit rates and provenance retention + +**A shorter encoding is not evidence of semantic preservation.** The optimizer must refuse a proposed common template that changes SQL NULL/UNKNOWN, Set/Bag, numeric overflow, effects, source identity or historical attribution. + +## Thought-Git learning × audit integration (future gate) + +Do not duplicate Thought-Git's store or insert proof events into the nanosecond hot loop. Its existing D-TGB-4 receipts and landed commit witnesses are distinct from egglog proof DAGs. The future link is a reference-only citation from a versioned derivation or historical study row to: +- certified law identity and assumptions +- compiled procedure identity and checker version +- source edition/provenance and any uncertainty +- runtime binding witness (separately invalidatable) +- promotion/demotion decision, counterexamples and cost samples + +A replay recipe should be sufficient to recompute the outcome if the source snapshot/operands, codebook and checker are available. A hash alone is not a replay. An unsigned witness fold is not a cryptographic proof. Rubicon authorization and real LanceCycleWriter integration are out of scope. + +## Next falsifiable stages (not shipped here) + +1. Formalize the Leibniz product rule against an independent differentiation theorem checker. Preserve exact domain conditions, such as differentiability of both functions. +2. Add an explicit mapping from the formal derivative term graph into the low-code hypothesis, measuring needed *new* atoms instead of forcing a 27-atom success. +3. Compare Leibniz- and Newton-era equivalent formulas only after historical source reviews; equivalence does **not** establish intellectual influence. +4. E2: 256 templates × 4,096 focus contexts = 1,048,576 applications. Compare cold certified catalogue vs existing relalg/CSE baseline, share/no-share controls and **total** execution cost. No demonstrated throughput claim yet. +5. Add read-only Thought-Git proof/reference records and replay tests after EXO-98 owner coordination. + +## Verification + +`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. 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..bef7fc910 --- /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 change in this PR:** copy the five missing files byte-identically from the #1695 head and expose both modules in `lib.rs`. This branch deliberately leaves their logic unchanged. It does **not** claim to have executed the recovered tests or promoted them to production. Before merging, compare file blob SHAs against original #1695 and run **the excluded probe's own tests**, not just root CI. + +**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:** verify this recovery PR contains all six recovery changes and the original #1695 test suites; 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 review/recovery 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. diff --git a/crates/egglog-r2il-probe/src/catalogue.rs b/crates/egglog-r2il-probe/src/catalogue.rs new file mode 100644 index 000000000..4e644f319 --- /dev/null +++ b/crates/egglog-r2il-probe/src/catalogue.rs @@ -0,0 +1,201 @@ +//! Stage D (lab): pre-certified mathematical patterns with fallback. +//! +//! Egglog is invoked ONLY when a candidate is cold-certified/promoted. +//! The lookup path is a BTreeMap + exact semantic/target/binding guard + an +//! already-lowered R2IL scalar program. Every miss/refusal calls the existing +//! caller-supplied trusted baseline. This is NOT a production cache, data +//! attestation, benchmark framework, or background task scheduler. + +use std::collections::BTreeMap; + +use crate::artifact::{ReplayCapsule, ReplayRefusal}; +use crate::{LowerRefusal, Problem}; + +/// Full source expression signature. Deliberately preserve premise order, +/// coefficient, and variable names; no hashes or accidentally merged laws. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub struct SemanticKey { + goal: String, + target: String, + premises: Vec<(String, i64, String)>, +} + +impl From<&Problem> for SemanticKey { + fn from(p: &Problem) -> Self { + Self { + goal: p.goal.to_owned(), + target: p.target_var.to_owned(), + premises: p.premises.iter() + .map(|e| (e.lhs.to_owned(), e.coeff, e.rhs.to_owned())) + .collect(), + } + } +} + +/// Caller-supplied lab witness. A production owner must independently attest +/// these values from the sealed source and coordinates before any cache use. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct BindingWitness { + pub source_generation: u64, + pub scope: u64, + pub coordinate_generation: u64, +} + +/// Plan compatibility, independent of mathematical identity and bindings. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct TargetAbi { + pub revision: u32, + pub target: String, +} + +/// All times are supplied from external measurements; none are inferred from +/// AST size or fabricated by the catalogue. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct CostEvidence { + pub baseline_ns: u64, + pub candidate_ns: u64, + pub compile_and_certify_ns: u64, + pub expected_reuse: u64, +} + +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.compile_and_certify_ns) + } +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum PromotionRefusal { + Uncertified(ReplayRefusal), + NotAmortized, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum FallbackReason { + CacheMiss, + BindingChanged, + TargetChanged, + CompiledRefused, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Route { + Certified, + Baseline(FallbackReason), +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Execution { + pub route: Route, + pub result: Result, +} + +struct Entry { + capsule: ReplayCapsule, + binding: BindingWitness, + abi: TargetAbi, + _cost: CostEvidence, +} + +/// In-memory lab catalogue; never loads an unverified disk blob. +#[derive(Default)] +pub struct Catalogue { + entries: BTreeMap, +} + +impl Catalogue { + pub fn new() -> Self { + Self::default() + } + + pub fn len(&self) -> usize { + self.entries.len() + } + + pub fn is_empty(&self) -> bool { + self.entries.is_empty() + } + + /// Cold gate. A proof, replay, independent i128 oracle and supplied + /// break-even evidence are required before inserting executable steps. + /// This retains the existing Stage B exact-integer / E1-only restriction. + pub fn promote( + &mut self, + capsule: ReplayCapsule, + binding: BindingWitness, + abi: TargetAbi, + cost: CostEvidence, + ) -> Result<(), PromotionRefusal> { + capsule.recheck().map_err(PromotionRefusal::Uncertified)?; + for x in [0_i64, 1, -1, 7] { + capsule.replay(x).map_err(PromotionRefusal::Uncertified)?; + } + if !cost.pays_for_itself() { + return Err(PromotionRefusal::NotAmortized); + } + self.entries.insert( + SemanticKey::from(capsule.problem()), + Entry { + capsule, + binding, + abi, + _cost: cost, + }, + ); + Ok(()) + } + + /// Hot-compatible lookup and execution: neither egglog nor the i128 + /// oracle runs here. Source/coordinate/target validation is fail-closed, + /// but caller-supplied witnesses are not source attestation. + /// + /// Any miss or compiled execution refusal invokes baseline unconditionally. + pub fn execute_or( + &self, + problem: &Problem, + binding: BindingWitness, + abi: &TargetAbi, + x: i64, + baseline: F, + ) -> Execution + where + F: FnOnce(i64) -> Result, + { + let entry = match self.entries.get(&SemanticKey::from(problem)) { + Some(e) => e, + None => { + return Execution { + route: Route::Baseline(FallbackReason::CacheMiss), + result: baseline(x), + }; + } + }; + let refusal = if entry.binding != binding { + Some(FallbackReason::BindingChanged) + } else if &entry.abi != abi { + Some(FallbackReason::TargetChanged) + } else { + None + }; + if let Some(reason) = refusal { + return Execution { + route: Route::Baseline(reason), + result: baseline(x), + }; + } + match entry.capsule.execute(x) { + Ok(value) => Execution { + route: Route::Certified, + result: Ok(value), + }, + Err(_) => Execution { + route: Route::Baseline(FallbackReason::CompiledRefused), + result: baseline(x), + }, + } + } +} diff --git a/crates/egglog-r2il-probe/src/heritage.rs b/crates/egglog-r2il-probe/src/heritage.rs new file mode 100644 index 000000000..81bed9308 --- /dev/null +++ b/crates/egglog-r2il-probe/src/heritage.rs @@ -0,0 +1,214 @@ +//! Stage E (lab): mathematics heritage as explicitly labelled source claims, +//! not as automatically certified executable proofs. +//! +//! The first runnable entry is the SYNTHETIC #1690 E1 substitution theorem. +//! Historical examples are catalogue leads only. Leibniz's product rule and +//! Euler's identity require new higher-level term grammars, domain guards and +//! independent theorem checkers before they may become proof capsules. +//! +//! The 27 atoms are a falsifiable vocabulary hypothesis, NOT an admitted +//! universal mathematical basis and NOT 27 R2IL opcodes. + +use std::collections::BTreeSet; + +use crate::Step; +use crate::artifact::{ReplayCapsule, ReplayRefusal}; +use crate::e1_problem; + +/// Proposal for a cross-domain low-code vocabulary, NOT the R2IL ISA. +/// Grouped 6 terms + 8 algebra + 7 relation + 6 derivation = 27 candidates. +#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)] +pub enum Atom27 { + Const, + Var, + Lambda, + Apply, + Let, + Tuple, + Add, + Neg, + Multiply, + Divide, + Power, + Equal, + Order, + If, + Select, + Project, + Join, + Union, + Distinct, + Group, + Aggregate, + Substitute, + Rewrite, + Differentiate, + Integrate, + Iterate, + Prove, +} + +pub const PROPOSED_ATOMS: [Atom27; 27] = [ + Atom27::Const, + Atom27::Var, + Atom27::Lambda, + Atom27::Apply, + Atom27::Let, + Atom27::Tuple, + Atom27::Add, + Atom27::Neg, + Atom27::Multiply, + Atom27::Divide, + Atom27::Power, + Atom27::Equal, + Atom27::Order, + Atom27::If, + Atom27::Select, + Atom27::Project, + Atom27::Join, + Atom27::Union, + Atom27::Distinct, + Atom27::Group, + Atom27::Aggregate, + Atom27::Substitute, + Atom27::Rewrite, + Atom27::Differentiate, + Atom27::Integrate, + Atom27::Iterate, + Atom27::Prove, +]; + +/// Unverified historical bibliographic lead, not a proof and not the +/// attribution of the modern formal reconstruction to its historical author. +#[derive(Debug, Clone)] +pub struct SourceLead { + pub author: &'static str, + pub work: &'static str, + pub date_note: &'static str, + pub candidate_catalogue_uri: &'static str, +} + +/// Historical source and mathematical implementation certification are +/// orthogonal: proof replay can certify the math without establishing +/// historical authorship, and vice versa. +#[derive(Debug, Clone)] +pub struct HeritageEntry { + pub id: &'static str, + pub normalized_statement: &'static str, + pub source: Option, + capsule: Option, +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum HeritageRefusal { + NoCheckedMathematicalProof, + Replay(ReplayRefusal), +} + +impl HeritageEntry { + pub fn synthetic_e1() -> Result { + let capsule = ReplayCapsule::certify(&e1_problem(), 8)?; + Ok(Self { + id: "synthetic-e1-1690", + normalized_statement: "a=2b, b=2c, z=2a |- z=8c (exact integer premises)", + source: None, + capsule: Some(capsule), + }) + } + + /// Historical lead only; the existing E1 grammar has no differentiation, + /// function application or quantification over differentiable functions. + pub fn leibniz_product_rule() -> Self { + Self { + id: "leibniz-product-rule-candidate", + normalized_statement: "D(f*g)=D(f)*g+f*D(g), for differentiable f,g", + source: Some(SourceLead { + author: "Gottfried Wilhelm Leibniz", + work: "Nova Methodus pro Maximis et Minimis", + date_note: "1684; attribution and textual correspondence require primary-source review", + candidate_catalogue_uri: "https://digitalcollections.hkust.edu.hk/Detail/objects/b540295", + }), + capsule: None, + } + } + + /// An additional corpus lead. No proof or original-edition claim. + pub fn euler_identity() -> Self { + Self { + id: "euler-identity-candidate", + normalized_statement: "exp(i*pi)+1=0 (complex exponential)", + source: Some(SourceLead { + author: "Leonhard Euler", + work: "Historical attribution and notation to be verified", + date_note: "18th-century work; no primary-source edition checked by this probe", + candidate_catalogue_uri: "", + }), + capsule: None, + } + } + + pub fn is_mathematically_certified(&self) -> bool { + self.capsule.is_some() + } + + /// Replay is permitted only with an actual checked E1 capsule. A text + /// claim and bibliographic lead can never implicitly become executable. + pub fn replay(&self, value: i64) -> Result { + self.capsule + .as_ref() + .ok_or(HeritageRefusal::NoCheckedMathematicalProof)? + .replay(value) + .map_err(HeritageRefusal::Replay) + } + + fn program(&self) -> Option<&[Step]> { + self.capsule.as_ref().map(|c| c.program()) + } +} + +/// Research fixture, intentionally mixing an executable *synthetic* theorem +/// with historically attributed *uncompiled* mathematical statements. +pub fn sample_corpus() -> Result, ReplayRefusal> { + Ok(vec![ + HeritageEntry::synthetic_e1()?, + HeritageEntry::leibniz_product_rule(), + HeritageEntry::euler_identity(), + ]) +} + +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct MetaStudy { + pub total_entries: usize, + pub historical_leads: usize, + pub mathematically_certified: usize, + pub distinct_compiled_programs: usize, + /// Only atoms witnessed by an actually compiled R2IL program. + pub observed_atoms: Vec, +} + +/// Deterministic descriptive analysis. No equivalence between historical +/// methods, no complexity claim, and no unlicensed mathematical law inference. +pub fn analyse(corpus: &[HeritageEntry]) -> MetaStudy { + let mut programs = BTreeSet::new(); + let mut atoms = BTreeSet::new(); + for entry in corpus { + if let Some(steps) = entry.program() { + 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); } + } + } + } + } + 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(), + 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 a9d022cb8..62c30aa9b 100644 --- a/crates/egglog-r2il-probe/src/lib.rs +++ b/crates/egglog-r2il-probe/src/lib.rs @@ -22,6 +22,8 @@ //! sharing no code with steps 2-4. pub mod artifact; +pub mod catalogue; +pub mod heritage; pub mod encode; pub mod laws; pub mod lower; diff --git a/crates/egglog-r2il-probe/tests/catalogue.rs b/crates/egglog-r2il-probe/tests/catalogue.rs new file mode 100644 index 000000000..839076d1b --- /dev/null +++ b/crates/egglog-r2il-probe/tests/catalogue.rs @@ -0,0 +1,93 @@ +//! Stage D: certified cache hit, explicit witness fallbacks, no hot egglog. +use egglog_r2il_probe::artifact::ReplayCapsule; +use egglog_r2il_probe::catalogue::{ + BindingWitness, Catalogue, CostEvidence, FallbackReason, PromotionRefusal, Route, TargetAbi, +}; +use egglog_r2il_probe::{LowerRefusal, e1_problem}; + +fn bind() -> BindingWitness { + BindingWitness { source_generation: 1, scope: 42, coordinate_generation: 9 } +} + +fn abi() -> TargetAbi { + TargetAbi { revision: 1, target: "r2il-checked-i64".into() } +} + +fn measured() -> CostEvidence { + // Synthetic evidence for testing the policy, NOT measured performance. + CostEvidence { + baseline_ns: 300, + candidate_ns: 100, + compile_and_certify_ns: 1_000, + expected_reuse: 10, + } +} + +fn trusted(x: i64) -> Result { + x.checked_mul(2) + .and_then(|v| v.checked_mul(2)) + .and_then(|v| v.checked_mul(2)) + .ok_or(LowerRefusal::Overflow) +} + +#[test] +fn certified_hit_uses_saved_r2il_and_zero_baseline_calls() { + let mut cache = Catalogue::new(); + let p = e1_problem(); + let compiled = ReplayCapsule::certify(&p, 8).expect("cold E1"); + cache.promote(compiled, bind(), abi(), measured()).unwrap(); + assert_eq!(cache.len(), 1); + let hit = cache.execute_or(&p, bind(), &abi(), 7, |_| panic!("baseline on hit")); + assert_eq!(hit.route, Route::Certified); + assert_eq!(hit.result, Ok(56)); +} + +#[test] +fn no_certificate_is_installed_without_economic_gate() { + let mut cache = Catalogue::new(); + let mut losing = measured(); + losing.candidate_ns = 500; + let c = ReplayCapsule::certify(&e1_problem(), 8).expect("cold E1"); + assert_eq!( + cache.promote(c, bind(), abi(), losing), + Err(PromotionRefusal::NotAmortized) + ); + assert!(cache.is_empty()); +} + +#[test] +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(); + + let mut stale = bind(); + stale.source_generation += 1; + let out = cache.execute_or(&p, stale, &abi(), 7, trusted); + 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 out = cache.execute_or(&p, bind(), &other, 7, trusted); + assert_eq!(out.route, Route::Baseline(FallbackReason::TargetChanged)); + + let mut altered = p.clone(); + altered.premises[0].coeff = 3; + let out = cache.execute_or(&altered, bind(), &abi(), 7, |_| Ok(-123)); + assert_eq!(out.route, Route::Baseline(FallbackReason::CacheMiss)); + assert_eq!(out.result, Ok(-123)); +} + +#[test] +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(); + 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 new file mode 100644 index 000000000..93e67b217 --- /dev/null +++ b/crates/egglog-r2il-probe/tests/heritage.rs @@ -0,0 +1,44 @@ +//! 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, +}; + +#[test] +fn exactly_27_candidate_atoms_without_a_universality_claim() { + let unique: BTreeSet = PROPOSED_ATOMS.into_iter().collect(); + assert_eq!(PROPOSED_ATOMS.len(), 27); + assert_eq!(unique.len(), 27); +} + +#[test] +fn historical_catalogue_leads_do_not_execute_as_proofs() { + for entry in [ + HeritageEntry::leibniz_product_rule(), + HeritageEntry::euler_identity(), + ] { + assert!(entry.source.is_some()); + assert!(!entry.is_mathematically_certified()); + assert_eq!( + entry.replay(7), + Err(HeritageRefusal::NoCheckedMathematicalProof) + ); + } +} + +#[test] +fn synthetic_e1_is_replayable_but_not_misattributed_to_leibniz() { + let corpus = sample_corpus().expect("E1 proof certified"); + assert_eq!(corpus[0].id, "synthetic-e1-1690"); + assert!(corpus[0].source.is_none()); + assert_eq!(corpus[0].replay(7), Ok(56)); + let report = analyse(&corpus); + assert_eq!(report.total_entries, 3); + assert_eq!(report.historical_leads, 2); + assert_eq!(report.mathematically_certified, 1); + assert_eq!(report.distinct_compiled_programs, 1); + assert_eq!( + report.observed_atoms, + vec![Atom27::Const, Atom27::Var, Atom27::Multiply] + ); +}