From d3248e964272c9b924ba81618039013e4b338307 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 05:18:51 +0000 Subject: [PATCH 1/6] D-MPS-9 draft: MORK oracle for general admitted rules + differential tests Not yet compiled or tested; the central gate runs next. - boundary.rs: OracleRule/OracleFacts/TupleSet/OracleCost and mork_rules: any admitted conjunctive rule set run through MORK exec, answers as a set, plus MORK's unification alone (Space::query_multi callback count, no decode). - mork_api::to_oracle maps an admitted Rule to the oracle's input. - tests/mork_differential.rs: six fixtures vs the reference as sets, match count vs reference derivations over distinct facts, refusals unchanged. - examples/mork_split.rs: native prepare/fold/terminal vs MORK cost split. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../crepe-plan-probe/examples/mork_split.rs | 200 +++++++++ crates/crepe-plan-probe/src/mork_api.rs | 34 ++ .../tests/mork_differential.rs | 408 ++++++++++++++++++ crates/mork-pathmap-probe/src/boundary.rs | 253 ++++++++++- .../mork-pathmap-probe/tests/differential.rs | 57 +++ 5 files changed, 951 insertions(+), 1 deletion(-) create mode 100644 crates/crepe-plan-probe/examples/mork_split.rs create mode 100644 crates/crepe-plan-probe/tests/mork_differential.rs diff --git a/crates/crepe-plan-probe/examples/mork_split.rs b/crates/crepe-plan-probe/examples/mork_split.rs new file mode 100644 index 000000000..0ba0bb435 --- /dev/null +++ b/crates/crepe-plan-probe/examples/mork_split.rs @@ -0,0 +1,200 @@ +//! Cost split of the `two_way` join, native against the MORK oracle, so the +//! oracle's reference costs are not one lump. Run in release from this crate's +//! directory: +//! +//! ```text +//! cargo run --release --example mork_split [n] +//! ``` +//! +//! `T(x, y, z) <- R(x, y), S(y, z)` with `R(i, i % (n/4))` for `i` in `0..n` +//! and `S(y, 500_000 + y)` for `y` in `0..n/4` (default `n = 10_000`). Every +//! `R` row meets exactly one `S` row, so there are `n` answers. +//! +//! Native: `pipeline::evaluate` with `Count(BAG)` (the terminal) and with +//! `Bindings(BAG)` (answer production); `Report::costs` separates the +//! preparation (laying the relations out at one coordinate) from the +//! execution. MORK: `OracleCost` (fact encoding and build, unification only, +//! `exec` plus decode). MORK stores sets and its numbers are reference costs +//! for an oracle, not gates. Before any timing the native answer set is +//! asserted equal to the MORK set. + +use std::collections::BTreeSet; +use std::hint::black_box; +use std::time::{Duration, Instant}; + +use crepe_plan_probe::logic::{Labels, RelId, Rule, resolve}; +use crepe_plan_probe::mork_api::to_oracle; +use crepe_plan_probe::native::Store; +use crepe_plan_probe::optimize::{Demand, Options, ResultKind}; +use crepe_plan_probe::pipeline::{Outcome, evaluate}; +use crepe_plan_probe::programs::two_way; +use mork_pathmap_probe::Semantics; +use mork_pathmap_probe::boundary::{OracleCost, OracleFacts, mork_rules}; + +const RUNS: usize = 5; +const BAG: Semantics = Semantics::Bag; + +fn median(mut v: Vec) -> Duration { + v.sort(); + v[v.len() / 2] +} + +fn us(d: Duration) -> f64 { + d.as_secs_f64() * 1e6 +} + +/// Microseconds, and nanoseconds per input row. +fn show(label: &str, d: Duration, rows: usize) -> String { + format!( + " {label:<28} {:>12.1} us {:>10.1} ns/row", + us(d), + d.as_secs_f64() * 1e9 / rows as f64 + ) +} + +struct Native { + wall: Duration, + optimize: Duration, + map_and_admit: Duration, + prepare: Duration, + execute: Duration, +} + +fn run_native( + rules: &[Rule], + demand: &Demand, + kind: ResultKind, + store: &Store, +) -> Native { + let mut runs = Vec::with_capacity(RUNS); + for _ in 0..RUNS { + let t = Instant::now(); + let (out, rep) = evaluate(rules, demand, kind, Options::ALL, store).expect("native answers"); + let wall = t.elapsed(); + black_box((&out, &rep.costs)); + runs.push((wall, rep.costs)); + } + let col = |f: &dyn Fn(&(Duration, crepe_plan_probe::pipeline::Costs)) -> Duration| { + median(runs.iter().map(f).collect()) + }; + Native { + wall: col(&|r| r.0), + optimize: col(&|r| r.1.optimize), + map_and_admit: col(&|r| r.1.map_and_admit), + prepare: col(&|r| r.1.prepare), + execute: col(&|r| r.1.execute), + } +} + +fn print_native(name: &str, n: &Native, rows: usize) { + println!("{name}"); + println!("{}", show("wall (evaluate)", n.wall, rows)); + println!("{}", show(" optimize", n.optimize, rows)); + println!("{}", show(" map and admit", n.map_and_admit, rows)); + println!("{}", show(" prepare (layout)", n.prepare, rows)); + println!("{}", show(" execute", n.execute, rows)); +} + +fn main() { + let n: u32 = std::env::args() + .nth(1) + .map(|a| a.parse().expect("n is an integer")) + .unwrap_or(10_000); + let key_domain = n / 4; + assert!(key_domain > 0, "n must be at least 4"); + + let plan = two_way::crepe_plan(); + let labels = Labels::of(&plan); + let rules: Vec = resolve(&plan, &labels) + .into_iter() + .map(|r| r.expect("admitted rule")) + .collect(); + let (rel_r, rel_s): (RelId, RelId) = (labels.id("R").unwrap(), labels.id("S").unwrap()); + let r: Vec<[u32; 2]> = (0..n).map(|i| [i, i % key_domain]).collect(); + let s: Vec<[u32; 2]> = (0..key_domain).map(|y| [y, 500_000 + y]).collect(); + let store = Store::from_rows(vec![(rel_r, &r, 1), (rel_s, &s, 1)]); + let input_rows = r.len() + s.len(); + let demand = Demand { + goal: labels.id("T").unwrap(), + bound: vec![None, None, None], + }; + + // The MORK oracle. + let oracle_rules: Vec<_> = rules + .iter() + .filter(|rule| rule.head.rel == demand.goal) + .map(|rule| to_oracle(rule).expect("admitted")) + .collect(); + let facts = [ + OracleFacts { + rel: rel_r.0, + arity: 2, + view: store.view(rel_r), + }, + OracleFacts { + rel: rel_s.0, + arity: 2, + view: store.view(rel_s), + }, + ]; + let mut costs: Vec = Vec::with_capacity(RUNS); + let mut mork_set = BTreeSet::new(); + for _ in 0..RUNS { + let (set, cost) = mork_rules(&facts, &oracle_rules).expect("MORK answers"); + mork_set = set.rows; + costs.push(cost); + } + let matches = costs[0].matches; + assert!( + costs.iter().all(|c| c.matches == matches), + "the match count is deterministic" + ); + + // Parity before any timing: the native answer set equals MORK's. + let (out, rep) = evaluate( + &rules, + &demand, + ResultKind::Bindings(BAG), + Options::ALL, + &store, + ) + .expect("native answers"); + let Outcome::Bindings(answers) = out else { + panic!("a bindings answer"); + }; + let mut native_set: BTreeSet> = BTreeSet::new(); + // Comparison only (not timed): rows are built here to compare sets with MORK. + answers.for_each(&rep.tables, |get, _weight| { + native_set.insert( + (0..3) + .map(|c| u32::try_from(get(c)).expect("value fits u32")) + .collect(), + ); + }); + assert!(!native_set.is_empty(), "vacuous fixture"); + assert_eq!(native_set, mork_set, "native answers equal MORK's set"); + + println!( + "mork_split: release build, n = {n}, runs = {RUNS} (median), input rows = {input_rows}, answers = {}", + native_set.len() + ); + println!("MORK numbers are oracle reference costs, not gates."); + println!("units: microseconds, and nanoseconds per input row\n"); + + let count = run_native(&rules, &demand, ResultKind::Count(BAG), &store); + print_native("native, Count(BAG) (terminal)", &count, input_rows); + let bindings = run_native(&rules, &demand, ResultKind::Bindings(BAG), &store); + print_native("native, Bindings(BAG) (answer production)", &bindings, input_rows); + + let med = |f: &dyn Fn(&OracleCost) -> Duration| median(costs.iter().map(f).collect()); + println!("MORK oracle (set semantics, matches = {matches})"); + println!("{}", show("encode + build", med(&|c| c.encode_build), input_rows)); + println!( + "{}", + show("match only (query_multi)", med(&|c| c.match_only), input_rows) + ); + println!( + "{}", + show("exec + decode", med(&|c| c.exec_decode), input_rows) + ); +} diff --git a/crates/crepe-plan-probe/src/mork_api.rs b/crates/crepe-plan-probe/src/mork_api.rs index 5a85f1bb5..bab3c3ffa 100644 --- a/crates/crepe-plan-probe/src/mork_api.rs +++ b/crates/crepe-plan-probe/src/mork_api.rs @@ -9,6 +9,7 @@ //! variable repeated inside one atom and cyclic bodies are refused by name. use lance_graph_relalg::join_body::is_alpha_acyclic; +use mork_pathmap_probe::boundary::{OracleAtom, OracleRule, OracleTerm}; use crate::logic::{RelId, Rule, Term, VarId}; @@ -48,6 +49,8 @@ pub enum MorkRefusal { Cyclic, /// A pattern does not start with a relation symbol. NoRelation { pattern: usize }, + /// An integer constant does not fit the oracle's `u32` symbol space. + ConstOutOfRange { value: u64 }, } /// The pattern of one rule. @@ -100,6 +103,37 @@ pub fn admit(q: &QueryMulti) -> Result<(), MorkRefusal> { Ok(()) } +/// The rule as the MORK oracle's input (`mork_pathmap_probe::boundary`), after +/// the same admission as [`admit`]: a refused pattern returns its refusal +/// unchanged. Relation and variable ids carry over as numbers; a constant must +/// fit a `u32`, the oracle's symbol space. Nothing here names MORK. +pub fn to_oracle(rule: &Rule) -> Result { + admit(&query_multi(rule))?; + let term = |t: &Term| -> Result { + Ok(match *t { + Term::Var(VarId(v)) => OracleTerm::Var(v), + Term::Const(c) => OracleTerm::Const( + u32::try_from(c).map_err(|_| MorkRefusal::ConstOutOfRange { value: c })?, + ), + }) + }; + let terms = |ts: &[Term]| -> Result, MorkRefusal> { ts.iter().map(term).collect() }; + let body = rule + .body + .iter() + .map(|a| { + Ok(OracleAtom { + rel: a.rel.0, + terms: terms(&a.terms)?, + }) + }) + .collect::, MorkRefusal>>()?; + Ok(OracleRule { + head: terms(&rule.head.terms)?, + body, + }) +} + /// The pattern as MORK text, `(Parent 17 $1)`, for reports and test output /// only. Nothing reads it back. pub fn render(q: &QueryMulti, name: impl Fn(RelId) -> &'static str) -> String { diff --git a/crates/crepe-plan-probe/tests/mork_differential.rs b/crates/crepe-plan-probe/tests/mork_differential.rs new file mode 100644 index 000000000..f01589711 --- /dev/null +++ b/crates/crepe-plan-probe/tests/mork_differential.rs @@ -0,0 +1,408 @@ +//! MORK as the differential oracle for every admitted `query_multi` pattern +//! (D-MPS-9). Each fixture's rules are mapped by `mork_api::to_oracle`, run in +//! one MORK `Space` through `mork_pathmap_probe::boundary::mork_rules`, and the +//! distinct head tuples are compared as SETS with the independent nested-loop +//! reference. MORK stores sets: bag semantics stay with the reference, and no +//! count is ever invented for MORK. +//! +//! Run from the crate directory (own workspace root): +//! cd crates/crepe-plan-probe && cargo test --test mork_differential + +use std::collections::BTreeSet; + +use crepe_plan_probe::logic::{Atom, Labels, RelId, Rule, Term, VarId, resolve}; +use crepe_plan_probe::mork_api::{MorkRefusal, admit, query_multi, to_oracle}; +use crepe_plan_probe::native::Store; +use crepe_plan_probe::plan::Plan; +use crepe_plan_probe::programs::{family, family_noisy, refused, star3, two_way}; +use crepe_plan_probe::reference; +use mork_pathmap_probe::boundary::{OracleCost, OracleFacts, mork_rules}; + +// --------------------------------------------------------------------------- +// Fixtures (small helpers copied from tests/pipeline.rs; they are test code) +// --------------------------------------------------------------------------- + +/// The family fixture. `Allowed(2)` is stored twice: a bag of facts, which +/// MORK collapses (its set semantics) and the reference counts twice. +struct Family { + parent: Vec<[u32; 2]>, + allowed: Vec<[u32; 2]>, + sponsor: Vec<[u32; 2]>, +} + +fn family_data() -> Family { + let mut parent = vec![ + [17, 1], + [17, 2], + [17, 3], + [1, 10], + [1, 11], + [2, 10], + [2, 12], + [3, 13], + [5, 1], + [4, 2], + ]; + // Unrelated families: they enlarge the shared domain, never the answer. + for i in 0..200u32 { + parent.push([1000 + i, 2000 + i]); + parent.push([2000 + i, 3000 + i]); + } + Family { + parent, + allowed: vec![[1, 1], [2, 2], [2, 2], [2000, 2000]], + sponsor: vec![[20, 20], [21, 21]], + } +} + +fn resolved(plan: &Plan) -> (Labels, Vec) { + let labels = Labels::of(plan); + let rules = resolve(plan, &labels) + .into_iter() + .map(|r| r.expect("admitted rule")) + .collect(); + (labels, rules) +} + +/// Raw rows of a relation at its declared arity, for the reference. +fn raw<'a>(labels: &'a Labels, store: &'a Store) -> impl Fn(RelId) -> Vec> + 'a { + move |rel| { + let v = store.view(rel); + (0..v.len()) + .map(|i| { + v.cols[..labels.arity(rel)] + .iter() + .map(|c| u64::from(c[i])) + .collect() + }) + .collect() + } +} + +/// The same rows with each relation deduplicated: what a MORK `Space` holds. +fn distinct<'a>(labels: &'a Labels, store: &'a Store) -> impl Fn(RelId) -> Vec> + 'a { + let rows = raw(labels, store); + move |rel| { + rows(rel) + .into_iter() + .collect::>() + .into_iter() + .collect() + } +} + +struct Fixture { + name: &'static str, + labels: Labels, + rules: Vec, + store: Store, + goal: RelId, +} + +impl Fixture { + fn goal_rules(&self) -> Vec<&Rule> { + self.rules + .iter() + .filter(|r| r.head.rel == self.goal) + .collect() + } + + fn demand(&self) -> Vec> { + vec![None; self.goal_rules()[0].head.terms.len()] + } +} + +fn family_store(labels: &Labels, f: &Family) -> Store { + Store::from_rows(vec![ + (labels.id("Parent").unwrap(), &f.parent, 1), + (labels.id("Allowed").unwrap(), &f.allowed, 1), + (labels.id("Sponsor").unwrap(), &f.sponsor, 1), + ]) +} + +fn two_way_rows() -> (Vec<[u32; 2]>, Vec<[u32; 2]>) { + let r = (0..120u32).map(|i| [i, i % 17]).collect(); + let s = (0..90u32).map(|i| [i % 23, 500 + i]).collect(); + (r, s) +} + +fn fixtures() -> Vec { + let mut out = Vec::new(); + + let f = family_data(); + let (labels, rules) = resolved(&family::crepe_plan()); + let store = family_store(&labels, &f); + out.push(Fixture { + name: "family", + goal: labels.id("Answer").unwrap(), + labels, + rules, + store, + }); + + let (labels, rules) = resolved(&family_noisy::crepe_plan()); + let store = family_store(&labels, &f); + out.push(Fixture { + name: "family_noisy", + goal: labels.id("Answer").unwrap(), + labels, + rules, + store, + }); + + let (r, s) = two_way_rows(); + let (labels, rules) = resolved(&two_way::crepe_plan()); + let store = Store::from_rows(vec![ + (labels.id("R").unwrap(), &r, 1), + (labels.id("S").unwrap(), &s, 1), + ]); + out.push(Fixture { + name: "two_way", + goal: labels.id("T").unwrap(), + labels, + rules, + store, + }); + + // Unary relations are stored as `[v, v]` rows. + let (labels, rules) = resolved(&star3::crepe_plan()); + let r: Vec<[u32; 2]> = (0..50u32).map(|v| [v, v]).collect(); + let s: Vec<[u32; 2]> = (25..80u32).map(|v| [v, v]).collect(); + let q: Vec<[u32; 2]> = (0..100u32).filter(|v| v % 3 == 0).map(|v| [v, v]).collect(); + let store = Store::from_rows(vec![ + (labels.id("R").unwrap(), &r, 1), + (labels.id("S").unwrap(), &s, 1), + (labels.id("Q").unwrap(), &q, 1), + ]); + out.push(Fixture { + name: "star3", + goal: labels.id("Hit").unwrap(), + labels, + rules, + store, + }); + + // A constant in the BODY: `C(z) <- R(7, y), S(y, z)` over the two_way data, + // built by hand with `Atom`/`Term` (no `crepe_plan!` module). The head + // relation id is not in the label table; nothing here resolves it by name. + let (r, s) = two_way_rows(); + let (labels, _) = resolved(&two_way::crepe_plan()); + let (rel_r, rel_s) = (labels.id("R").unwrap(), labels.id("S").unwrap()); + let goal = RelId(99); + let (y, z) = (Term::Var(VarId(0)), Term::Var(VarId(1))); + let rule = Rule { + head: Atom { + rel: goal, + terms: vec![z], + }, + body: vec![ + Atom { + rel: rel_r, + terms: vec![Term::Const(7), y], + }, + Atom { + rel: rel_s, + terms: vec![y, z], + }, + ], + }; + let store = Store::from_rows(vec![(rel_r, &r, 1), (rel_s, &s, 1)]); + out.push(Fixture { + name: "body_constant", + labels, + rules: vec![rule], + store, + goal, + }); + + // A three-atom chain: acyclic, so the MORK shape admits it, but the native + // star refuses it. MORK answers it; the reference checks MORK. + let plan = refused::crepe_plan(); + let labels = Labels::of(&plan); + let rules: Vec = resolve(&plan, &labels) + .into_iter() + .filter_map(Result::ok) + .collect(); + let e: Vec<[u32; 2]> = (0..30u32).map(|i| [i, (i * 7 + 3) % 30]).collect(); + let store = Store::from_rows(vec![(labels.id("E").unwrap(), &e, 1)]); + out.push(Fixture { + name: "chain", + goal: labels.id("Chain").unwrap(), + labels, + rules, + store, + }); + + out +} + +/// The oracle's input relations: every relation the store holds, at its +/// declared arity. +fn oracle_facts(fx: &Fixture) -> Vec> { + fx.store + .relations + .iter() + .map(|(rel, view)| OracleFacts { + rel: rel.0, + arity: fx.labels.arity(*rel), + view, + }) + .collect() +} + +/// The reference's distinct head tuples, narrowed to `u32` (MORK's symbols). +fn reference_set(fx: &Fixture) -> BTreeSet> { + reference::eval(&fx.rules, fx.goal, &fx.demand(), &raw(&fx.labels, &fx.store)) + .keys() + .map(|row| { + row.iter() + .map(|&v| u32::try_from(v).expect("fixture values fit u32")) + .collect() + }) + .collect() +} + +fn mork_set(fx: &Fixture) -> (BTreeSet>, OracleCost) { + let oracle_rules: Vec<_> = fx + .goal_rules() + .into_iter() + .map(|r| to_oracle(r).expect("admitted by the logical interface")) + .collect(); + let (set, cost) = mork_rules(&oracle_facts(fx), &oracle_rules) + .unwrap_or_else(|e| panic!("{}: MORK refused: {e:?}", fx.name)); + (set.rows, cost) +} + +// --------------------------------------------------------------------------- +// Tests +// --------------------------------------------------------------------------- + +/// FAILS IF: any admitted pattern, run by MORK, derives a head tuple the +/// independent reference does not (or misses one it does). The set must also +/// be non-empty, so the equality cannot hold of two empty answers. +#[test] +fn mork_sets_equal_the_reference_sets() { + for fx in fixtures() { + let want = reference_set(&fx); + let (got, _) = mork_set(&fx); + assert!(!want.is_empty(), "{}: vacuous fixture", fx.name); + assert_eq!(got, want, "{}", fx.name); + } +} + +/// `family_noisy` renames variables and duplicates an atom and a rule; its +/// answer set is `family`'s. +#[test] +fn family_noisy_gives_the_same_mork_set_as_family() { + let all = fixtures(); + let by = |name: &str| all.iter().find(|f| f.name == name).expect("fixture"); + let (family_set, _) = mork_set(by("family")); + let (noisy_set, _) = mork_set(by("family_noisy")); + assert!(!family_set.is_empty()); + assert_eq!(noisy_set, family_set); +} + +/// The body constant selects: only `R(7, y)` rows feed the answer, so the +/// answer is a strict subset of the unrestricted join's `z` column. +#[test] +fn a_body_constant_restricts_the_mork_answer() { + let all = fixtures(); + let fx = all.iter().find(|f| f.name == "body_constant").unwrap(); + let (got, _) = mork_set(fx); + // y = 7 (R(7, 7)); S rows with i % 23 == 7 are i = 7, 30, 53, 76. + let want: BTreeSet> = [507u32, 530, 553, 576].iter().map(|&z| vec![z]).collect(); + assert_eq!(got, want); +} + +/// The number of `query_multi` effect callbacks equals the number of body +/// matches over the DISTINCT facts: the reference's derivation count with each +/// relation deduplicated first. MORK holds a set, so a duplicated fact row +/// (`Allowed(2)` twice in `family`) matches once. +/// +/// FAILS IF: the unification-only enumeration is not one callback per match, +/// or a duplicate fact reaches MORK as a second match. +#[test] +fn mork_match_count_equals_reference_derivations_over_distinct_facts() { + for fx in fixtures() { + let (_, cost) = mork_set(&fx); + let want: u64 = reference::eval( + &fx.rules, + fx.goal, + &fx.demand(), + &distinct(&fx.labels, &fx.store), + ) + .values() + .sum(); + assert!(want > 0, "{}: vacuous fixture", fx.name); + assert_eq!(cost.matches, want, "{}", fx.name); + } +} + +/// Over the BAG rows (duplicates kept) the reference counts more derivations +/// than MORK matched in `family`: the duplicate `Allowed(2)` is the difference. +/// Without this the distinct-facts test could pass with the dedup being a no-op. +#[test] +fn the_duplicate_allowed_row_is_what_separates_bag_from_set_matches() { + let all = fixtures(); + let fx = all.iter().find(|f| f.name == "family").unwrap(); + let (_, cost) = mork_set(fx); + let bag: u64 = reference::eval(&fx.rules, fx.goal, &fx.demand(), &raw(&fx.labels, &fx.store)) + .values() + .sum(); + assert!(bag > cost.matches, "bag {bag} must exceed set {}", cost.matches); +} + +/// `to_oracle` refuses exactly what `admit` refuses, and returns that refusal +/// unchanged. The chain is acyclic, so `admit` (and so `to_oracle`) admits it. +#[test] +fn to_oracle_returns_admits_refusals_unchanged() { + let plan = refused::crepe_plan(); + let labels = Labels::of(&plan); + let resolved = resolve(&plan, &labels); + let rule_of = |name: &str| -> Rule { + plan.rules + .iter() + .zip(&resolved) + .find(|(r, _)| r.goal.relation == name) + .and_then(|(_, res)| res.clone().ok()) + .unwrap_or_else(|| panic!("{name} resolves")) + }; + for name in ["Chain", "Tri", "Loop"] { + let rule = rule_of(name); + assert_eq!( + to_oracle(&rule).map(|_| ()), + admit(&query_multi(&rule)), + "{name}" + ); + } + assert!(to_oracle(&rule_of("Chain")).is_ok(), "chain is acyclic"); + assert_eq!( + to_oracle(&rule_of("Tri")).map(|_| ()), + Err(MorkRefusal::Cyclic) + ); + assert!(matches!( + to_oracle(&rule_of("Loop")), + Err(MorkRefusal::RepeatedVarInAtom { pattern: 0, .. }) + )); +} + +/// A constant that does not fit the oracle's `u32` symbols is refused by name, +/// never truncated. +#[test] +fn a_constant_beyond_u32_is_refused() { + let (labels, _) = resolved(&two_way::crepe_plan()); + let rule = Rule { + head: Atom { + rel: RelId(99), + terms: vec![Term::Var(VarId(0))], + }, + body: vec![Atom { + rel: labels.id("R").unwrap(), + terms: vec![Term::Const(1 << 40), Term::Var(VarId(0))], + }], + }; + assert_eq!( + to_oracle(&rule).map(|_| ()), + Err(MorkRefusal::ConstOutOfRange { value: 1 << 40 }) + ); +} diff --git a/crates/mork-pathmap-probe/src/boundary.rs b/crates/mork-pathmap-probe/src/boundary.rs index 8d577b806..c443c886a 100644 --- a/crates/mork-pathmap-probe/src/boundary.rs +++ b/crates/mork-pathmap-probe/src/boundary.rs @@ -11,6 +11,8 @@ //! is not zero-copy, and nothing here claims it is. A stale copy is caught by //! the generation witness ([`Refusal::Stale`]), not by a lifetime. +use std::collections::BTreeSet; +use std::fmt::Write as _; use std::time::{Duration, Instant}; use mork::space::Space; @@ -18,7 +20,7 @@ use pathmap::PathMap; use pathmap::zipper::{ZipperIteration, ZipperPath, ZipperValues}; use crate::join::{JoinExec, JoinTable}; -use crate::{Answers, JoinInput, Semantics}; +use crate::{Answers, JoinInput, RelationView, Semantics}; /// A physical implementation of the fixed query. #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -396,6 +398,255 @@ impl PostingTrie { } } +// ---- MORK, general rules --------------------------------------------------- +// +// The fixed query above answers one shape. This section answers any admitted +// conjunctive rule set, so MORK can be the differential oracle for every +// `query_multi` pattern the logical interface admits (D-MPS-9). The input types +// are plain Lance-owned data; no crepe type enters this crate (the dependency +// runs crepe-plan-probe -> mork-pathmap-probe only). +// +// MORK stores SETS. Its answers are compared as sets ([`TupleSet`]); bag +// semantics stay with the reference and datafrog, and no count is invented +// for MORK here. + +/// One term of an oracle atom. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum OracleTerm { + /// A rule variable, by number. The MORK text is `$v`. + Var(u16), + /// An integer constant. The MORK text is the symbol `n`. + Const(u32), +} + +/// `rel(terms…)`. The MORK text is `(r …)`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct OracleAtom { + pub rel: u16, + pub terms: Vec, +} + +/// One rule `Head(terms) <- body`. All rules handed to one call share one head +/// relation, so only the head's terms are carried. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct OracleRule { + pub head: Vec, + pub body: Vec, +} + +/// One input relation: its id and its first `arity` lanes of `view` +/// (arity 1 or 2). +#[derive(Clone, Copy, Debug)] +pub struct OracleFacts<'a> { + pub rel: u16, + pub arity: usize, + pub view: &'a RelationView, +} + +/// Distinct head tuples: MORK's representation (a set). Oracle-only. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct TupleSet { + pub rows: BTreeSet>, +} + +/// What the oracle cost, split so the reference costs are not one lump. +#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)] +pub struct OracleCost { + /// Fact text and `add_all_sexpr`. + pub encode_build: Duration, + /// `exec` + `metta_calculus` + dump + parse + remove, summed over rules. + pub exec_decode: Duration, + /// `Space::query_multi` callbacks only, no decode, summed over rules. + /// [`Duration::ZERO`] together with `matches == u64::MAX` means the + /// unification-only timing could not be driven (it can here; see + /// [`mork_rules`]). + pub match_only: Duration, + /// Number of `query_multi` effect callbacks, summed over rules. + pub matches: u64, +} + +fn push_term(out: &mut String, t: &OracleTerm) { + let written = match t { + OracleTerm::Var(v) => write!(out, "$v{v}"), + OracleTerm::Const(c) => write!(out, "n{c}"), + }; + written.expect("writing to a String cannot fail"); +} + +fn push_atom(out: &mut String, a: &OracleAtom) { + write!(out, "(r{}", a.rel).expect("writing to a String cannot fail"); + for t in &a.terms { + out.push(' '); + push_term(out, t); + } + out.push(')'); +} + +/// `(, (r3 $v0 $v1) (r4 $v1 n7))`. +fn pattern_text(rule: &OracleRule) -> String { + let mut s = String::from("(,"); + for a in &rule.body { + s.push(' '); + push_atom(&mut s, a); + } + s.push(')'); + s +} + +/// `(exec 0 (, body) (, (Q head)))`. +fn exec_text(rule: &OracleRule) -> String { + let mut s = format!("(exec 0 {} (, (Q", pattern_text(rule)); + for t in &rule.head { + s.push(' '); + push_term(&mut s, t); + } + s.push_str(")))\n"); + s +} + +/// The tokens of a `(Q n1 n2 …)` line's tail, or `None` if any is not `n`. +fn parse_tuple(rest: &[u8]) -> Option> { + let body = rest.strip_suffix(b")")?; + body.split(|&b| b == b' ') + .map(|tok| { + std::str::from_utf8(tok.strip_prefix(b"n")?) + .ok()? + .parse::() + .ok() + }) + .collect() +} + +/// Checks one rule before anything is built. +fn check_rule(rule: &OracleRule) -> Result<(), Refusal> { + if rule.body.is_empty() { + return Err(Refusal::Upstream("empty body".into())); + } + if rule.head.is_empty() { + return Err(Refusal::Upstream("empty head".into())); + } + for t in &rule.head { + if let OracleTerm::Var(v) = t { + let bound = rule + .body + .iter() + .any(|a| a.terms.iter().any(|b| *b == OracleTerm::Var(*v))); + if !bound { + return Err(Refusal::Upstream("unbound head var".into())); + } + } + } + Ok(()) +} + +/// Runs `rules` (one shared head relation) over `facts` in one MORK `Space` +/// and returns the distinct head tuples with a split cost. +/// +/// Each rule runs as its own MM2 `exec`, so one rule's `Q` facts never feed +/// another rule. Duplicated fact rows are fed as they are: MORK collapses +/// them, which is its set semantics, and nothing here dedupes for it. +/// +/// Per rule, BEFORE its `exec`, the body pattern is parsed with +/// `Space::parse_sexpr` and enumerated once with `Space::query_multi` over the +/// space's own trie. That is MORK's unification alone, with no decoding of the +/// answer; the callbacks are counted in [`OracleCost::matches`]. Running it +/// before the `exec` keeps this rule's `Q` facts out of the trie. +/// +/// The effect closure's `bool` is a CONTINUE flag, not an accepted/rejected +/// flag: `query_multi_raw` calls `effect` once per successful unification and +/// breaks out of the enumeration when it returns `false` +/// (`kernel/src/space.rs`, `if !effect(Err(&bs), e) { break }` / `longjmp`). +/// Returning `true` therefore visits every match, and the callback is never +/// invoked for a candidate that failed to unify, so the count is exactly the +/// number of body matches over the DISTINCT facts. +pub fn mork_rules( + facts: &[OracleFacts<'_>], + rules: &[OracleRule], +) -> Result<(TupleSet, OracleCost), Refusal> { + for rule in rules { + check_rule(rule)?; + } + let mut cost = OracleCost::default(); + + let start = Instant::now(); + let mut text = String::new(); + for f in facts { + if !(1..=2).contains(&f.arity) { + return Err(Refusal::Upstream(format!("fact arity {}", f.arity))); + } + let lanes = &f.view.cols[..f.arity]; + for i in 0..f.view.len() { + write!(text, "(r{}", f.rel).expect("writing to a String cannot fail"); + for lane in lanes { + write!(text, " n{}", lane[i]).expect("writing to a String cannot fail"); + } + text.push_str(")\n"); + } + } + let mut space = Space::new(); + space + .add_all_sexpr(text.as_bytes()) + .map_err(Refusal::Upstream)?; + cost.encode_build = start.elapsed(); + + // One caller-owned expression buffer for every pattern parse, alive across + // the whole function so no `Expr` outlives its bytes. + let longest = rules.iter().map(|r| pattern_text(r).len()).max().unwrap_or(0); + let mut buf: Vec = vec![0; 64 * longest + 4096]; + + let mut out = TupleSet::default(); + for rule in rules { + // Unification only. `parse_sexpr` writes the encoded pattern at `buf`; + // the `Expr` it returns is a raw pointer into `buf`, valid until `buf` + // is written again, so it is used only inside this block. + let mut pat = pattern_text(rule); + pat.push('\n'); + let parsed = space + .parse_sexpr(pat.as_bytes(), buf.as_mut_ptr()) + .map_err(|e| Refusal::Upstream(format!("parse_sexpr: {e:?}")))?; + let t = Instant::now(); + let mut n = 0u64; + // No `unsafe` is needed: `parse_sexpr` and `query_multi` are both safe + // `pub` fns. The soundness argument is only that `parsed.0` points into + // `buf`, which is neither moved, resized nor written between + // `parse_sexpr` and the end of this call, and that `buf` is sized well + // past the encoding (64 bytes per pattern byte plus slack; MORK writes + // one tag byte per element plus the symbol bytes). `query_multi` takes + // the trie by shared reference and only reads the expression. + Space::query_multi(&space.btm, parsed.0, |_res, _e| { + n += 1; + true + }); + cost.match_only += t.elapsed(); + cost.matches += n; + + let t = Instant::now(); + space + .add_all_sexpr(exec_text(rule).as_bytes()) + .map_err(Refusal::Upstream)?; + space.metta_calculus(1); + let mut dump = Vec::new(); + space.dump_all_sexpr(&mut dump).map_err(Refusal::Upstream)?; + let mut produced = Vec::new(); + for line in dump.split(|&b| b == b'\n') { + if let Some(rest) = line.strip_prefix(b"(Q ") { + let row = parse_tuple(rest) + .ok_or_else(|| Refusal::Upstream(String::from_utf8_lossy(line).into_owned()))?; + out.rows.insert(row); + produced.extend_from_slice(line); + produced.push(b'\n'); + } + } + if !produced.is_empty() { + space + .remove_all_sexpr(&produced) + .map_err(Refusal::Upstream)?; + } + cost.exec_decode += t.elapsed(); + } + Ok((out, cost)) +} + #[cfg(test)] mod tests { use super::*; diff --git a/crates/mork-pathmap-probe/tests/differential.rs b/crates/mork-pathmap-probe/tests/differential.rs index 1909367fb..73ea63418 100644 --- a/crates/mork-pathmap-probe/tests/differential.rs +++ b/crates/mork-pathmap-probe/tests/differential.rs @@ -207,3 +207,60 @@ fn native_join_answers_bags_from_the_coaddressed_table() { ); } } + +/// The general-rules oracle, given the fixed join as an `OracleRule`, answers +/// the same set as the fixed-query MORK arm on the same input. +#[test] +fn general_rules_agree_with_the_fixed_query() { + use mork_pathmap_probe::boundary::{ + OracleAtom, OracleFacts, OracleRule, OracleTerm, mork_rules, + }; + const R: u16 = 0; + const S: u16 = 1; + let r = [[1, 10], [1, 11], [2, 10], [3, 12], [1, 10]]; + let s = [[10, 100], [11, 101], [10, 102], [99, 103], [10, 100]]; + let inp = input(&r, &s, 1, 1); + + let mut fixed = bind(Backend::Mork, &inp, Semantics::Set).expect("set semantics is admitted"); + let want: std::collections::BTreeSet> = fixed + .answers(&inp) + .expect("fresh generations") + .rows + .keys() + .map(|row| row.to_vec()) + .collect(); + assert!(!want.is_empty(), "fixture must produce answers"); + + // Q(x, y, z) :- R(x, y), S(y, z). x = 0, y = 1, z = 2. + let (x, y, z) = (OracleTerm::Var(0), OracleTerm::Var(1), OracleTerm::Var(2)); + let rule = OracleRule { + head: vec![x.clone(), y.clone(), z.clone()], + body: vec![ + OracleAtom { + rel: R, + terms: vec![x, y.clone()], + }, + OracleAtom { + rel: S, + terms: vec![y, z], + }, + ], + }; + let facts = [ + OracleFacts { + rel: R, + arity: 2, + view: &inp.r, + }, + OracleFacts { + rel: S, + arity: 2, + view: &inp.s, + }, + ]; + let (got, cost) = mork_rules(&facts, &[rule]).expect("general rules answer"); + assert_eq!(got.rows, want); + // Over the distinct facts the body matches 5 times: + // (1,10,100) (1,10,102) (1,11,101) (2,10,100) (2,10,102). + assert_eq!(cost.matches, 5); +} From f61262fd45f37974b51895f45b4b808ac61a7354 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 05:33:53 +0000 Subject: [PATCH 2/6] D-MPS-9: MORK oracle measured for query_multi; timed answer enumeration; board MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Gate: mork-pathmap-probe 46 tests, crepe-plan-probe 59 tests (7 new differential), release; clippy -D warnings and fmt clean on both. - Disable runs, each red then restored: constants as variables (5 red), count only Ok callbacks (1 red), to_oracle without admit (1 red). - mork_split: the Bindings outcome is a deferred handle, so its execute time never read the answers; one full enumeration is now timed (188 us vs 17.6 us for the count terminal at n = 10 000). - clippy: contains() instead of iter().any() in check_rule. - Board: entry 2026-10-22-d-mps-9-mork-oracle (results, cost split, open verbs, slim_ptrs correction), STATUS_BOARD D-MPS-9 row, plan §7d, AGENT_LOG, regenerated entries index. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .claude/board/AGENT_LOG.md | 6 ++ .claude/board/STATUS_BOARD.md | 2 +- .../entries/2026-10-22-d-mps-9-mork-oracle.md | 41 ++++++++++++++ .claude/board/entries/README.md | 3 +- .../mork-pathmap-schnellverschluss-v1.md | 4 ++ .../crepe-plan-probe/examples/mork_split.rs | 55 +++++++++++++++---- crates/crepe-plan-probe/src/mork_api.rs | 3 +- .../tests/mork_differential.rs | 38 +++++++++---- crates/mork-pathmap-probe/src/boundary.rs | 8 ++- 9 files changed, 133 insertions(+), 27 deletions(-) create mode 100644 .claude/board/entries/2026-10-22-d-mps-9-mork-oracle.md diff --git a/.claude/board/AGENT_LOG.md b/.claude/board/AGENT_LOG.md index 2acd93876..b6476b361 100644 --- a/.claude/board/AGENT_LOG.md +++ b/.claude/board/AGENT_LOG.md @@ -1,3 +1,9 @@ +## 2026-10-22 — D-MPS-9 `query_multi` oracle (Haiku map, Opus spec, Sonnet draft) + +- Two Haiku `substrate-mapper` runs: MORK `space.rs`/`expr` (PARTIAL: the read stopped at line 1076/1094; `query_multi`, `Bindings`, `ExprEnv` read on the main thread) and the probe boundary plus fixtures (complete). +- One Sonnet drafter from a written spec (no cargo). The main thread compiled, ran the disable runs (3, all red), fixed one clippy lint and one measurement gap (the deferred `Bindings` handle had no timed enumeration). +- Result: `entries/2026-10-22-d-mps-9-mork-oracle.md`. Written by the orchestrating main thread only. + ## 2026-10-21 — 5+3 council: the tuple is a zero-copy violation (blast radius) - Five savants: prior-art-savant, iron-rule-savant, runtime-archaeologist (code truth), cascade-impact-savant (blast radius, Opus), creative-explorer-savant. Three reviewers on draft v2 only: overclaim-auditor (2 BLOCK, wording/grading, fixed), dilution-collapse-sentinel (0 BLOCK, 2 collapses restored), firewall-warden (0 BLOCK). diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 3618adb6f..0e903ca1c 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -41,7 +41,7 @@ Plan `mork-pathmap-schnellverschluss-v1.md`; entry `entries/2026-10-19-mork-path | D-MPS-5 | upstream MORK: leapfrog join generic over a cursor provider + reindex hook | PROPOSAL | MORK corpus unchanged on `PathMap<()>` | | D-MPS-6 | Lance-owned PathMap-trait cursor over a sealed `RelationOrder` | BLOCKED (`RelationOrder` not built) | no copy, or the copy stated | | D-MPS-7 | licence: no MORK source vendored until a licence is declared (#148 unmerged) | OPEN (intent stated, clearance incomplete): MIT intent stated by the maintainer (Adam-Vandervorst, trueagi-io/MORK issue #2, 2025-05-21: "Yes! It's now under MIT."); formal repository-level clearance incomplete: PR #148 "Add MIT License and Cargo manifest metadata" proposed 2026-08-20, still open when observed 2026-10-19. PathMap already advertises MIT Scope (operator, 2026-10-20): the gate covers using MORK code — vendoring, redistributing or translating its source. An independent implementation, written from documented behaviour and checked against our own tests and oracles, is not blocked by it; "openmork" was named as a further option (not located by this session, URL needed). The Schnellverschluss is the design answer to this gate (operator, 2026-10-20: "That's why we implemented it with Schnellverschluss"): MORK is fetched, never vendored; nothing outside `boundary.rs` names it; deleting it is one `Index` variant, two helpers and one `Cargo.toml` line (§3 removal test); and the native arm (D-MPS-8) answers the same join without MORK code. | probe vendors nothing; vendoring waits for #148 or an equivalent LICENSE file in MORK | -| D-MPS-9 | MORK `Space` verbs (`add_sexpr`/`remove_sexpr`/`query_multi`/`transform_multi_multi`/`dump_sexpr`) as the standard API, answered by our folding; MORK as the differential oracle behind the Schnellverschluss; first scope fixed-arity shared-variable patterns, other shapes refused by name (`mork-pathmap-schnellverschluss-v1.md` §7c) | Queued (lab; DECISION 2026-10-20) | answers == MORK (sets) and datafrog (bags) per verb and fixture; disable: silently flatten a nested pattern | +| D-MPS-9 | MORK `Space` verbs (`add_sexpr`/`remove_sexpr`/`query_multi`/`transform_multi_multi`/`dump_sexpr`) as the standard API, answered by our folding; MORK as the differential oracle behind the Schnellverschluss; first scope fixed-arity shared-variable patterns, other shapes refused by name (`mork-pathmap-schnellverschluss-v1.md` §7c) | MEASURED (lab) for `query_multi` only, 2026-10-22; other verbs Queued | `entries/2026-10-22-d-mps-9-mork-oracle.md`: 6 fixtures MORK set == reference, match count == reference over distinct facts, 3 disable runs red; flatten-nested disable not expressible (native has no nested facts) | ## Plan links for #1601–#1617 (2026-10-20) diff --git a/.claude/board/entries/2026-10-22-d-mps-9-mork-oracle.md b/.claude/board/entries/2026-10-22-d-mps-9-mork-oracle.md new file mode 100644 index 000000000..bde094a8b --- /dev/null +++ b/.claude/board/entries/2026-10-22-d-mps-9-mork-oracle.md @@ -0,0 +1,41 @@ +# 2026-10-22 — D-MPS-9: MORK as the differential oracle for every admitted `query_multi` + +**Status:** MEASURED (lab; mork-pathmap-probe, crepe-plan-probe). Not admitted, not wired into Quack or R2IL. + +## What changed + +- `boundary.rs` gains a general MORK arm, `mork_rules(facts, rules)`. It takes Lance-owned plain data (`OracleRule`, `OracleAtom`, `OracleTerm`, `OracleFacts`) and returns the distinct head tuples (`TupleSet`, a set, oracle only) plus `OracleCost`. No crepe type enters the crate; nothing upstream-typed leaves it. +- Each rule runs as its own MM2 `exec`, so one rule's output never feeds another. Before the `exec`, the body is parsed with `Space::parse_sexpr` and enumerated with `Space::query_multi`, counting the effect callbacks. That times MORK's unification alone, with no answer decode. The callback's `bool` is a continue flag (`space.rs:1253`, `:1343`, `:1364`); it is called only after a successful unify. +- `mork_api::to_oracle(rule)` runs `admit` first and returns its refusal unchanged; constants above `u32` are refused (`ConstOutOfRange`). + +## Tests (`crepe-plan-probe/tests/mork_differential.rs`, 7; `mork-pathmap-probe/tests/differential.rs` +1) + +- Six fixtures, MORK set == reference set, each non-empty: `family` (two rules, head constant, repeated relation, a duplicated fact), `family_noisy` (== `family`'s set), `two_way`, `star3`, a body constant, a three-atom chain (acyclic; the native star refuses it, MORK answers it). +- MORK's callback count == the reference's derivation count over DEDUPLICATED facts, and the bag count over raw facts exceeds it on `family` (the duplicate `Allowed(2)`), so the dedup is not a no-op. +- `to_oracle` refuses exactly what `admit` refuses (Tri `Cyclic`, Loop `RepeatedVarInAtom`; Chain admitted). +- The general arm agrees with the fixed `Q(x,y,z)` query. +- Disable runs, each red then restored: constants encoded as variables (5 tests red); counting only `Ok` callbacks (match-count test red); `to_oracle` skipping `admit` (refusal test red). + +## Cost split (`examples/mork_split.rs`, release, median of 5, n = 10 000, 12 500 input rows, 10 000 answers; Xeon @ 2.10 GHz, 4 vCPU, shared host) + +| arm | µs | ns / input row | +|---|---|---| +| native prepare (layout) | 162 | 13.0 | +| native execute, `Count(BAG)` terminal | 17.6 | 1.4 | +| native execute, `Bindings(BAG)` (deferred handle) | 2.8 | 0.2 | +| native: enumerate all 10 000 answers (no allocation per answer) | 188 | 15.0 | +| MORK encode + build | 3 564 | 285 | +| MORK unification only (`query_multi`) | 12 289 | 983 | +| MORK exec + text decode | 23 548 | 1 884 | + +- The `Bindings` outcome's `execute` does not read answers; enumeration is timed separately. Reading the answers costs 10× the count terminal here. +- MORK numbers are oracle reference costs, not gates. MORK's unification alone is about half its exec + decode time; the earlier §6 MORK query column (exec + dump + parse) is therefore roughly 2× MORK's join. + +## Not covered (OPEN) + +- `add_sexpr` / `remove_sexpr` / `dump_sexpr` / `transform_multi_multi` façade verbs: not built. Removal is a full re-prepare on the native side. +- Binding and witness validation are still inside `prepare`; not split out. +- The §7c disable "silently flatten a nested pattern" is not run: the native side has no representation for nested facts, so the flattened arm cannot be expressed. The nested refusal test stands. +- Structural sharing and memory across versions: not measured. Allocations: still blocked (MORK installs PathMap's jemalloc, D-MPS-4). + +**Correction (chat, 2026-10-22):** PathMap's default build uses `slim_ptrs` (`TrieNodeODRc` = `SlimNodePtr` + allocator, `trie_node.rs:3020`); `Arc` is only the non-`slim_ptrs` build (`:2721`/`:2726`). diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index a00b8d1ec..071f99977 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -425 entries, 2026-08-06 .. 2026-10-21. +426 entries, 2026-08-06 .. 2026-10-22. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-22 | `D-MPS-9` | | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) | | 2026-10-21 | `zero-copy-join-index-map` | | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) | | 2026-10-21 | `D-RU-4` | | [2026-10-21-u4-coaddressed-join.md](2026-10-21-u4-coaddressed-join.md) | | 2026-10-21 | `D-RU-3` | | [2026-10-21-u3-cross-rule-cse.md](2026-10-21-u3-cross-rule-cse.md) | diff --git a/.claude/plans/mork-pathmap-schnellverschluss-v1.md b/.claude/plans/mork-pathmap-schnellverschluss-v1.md index a18cbd88a..981e05cb8 100644 --- a/.claude/plans/mork-pathmap-schnellverschluss-v1.md +++ b/.claude/plans/mork-pathmap-schnellverschluss-v1.md @@ -192,6 +192,10 @@ Neo4j loaders, symbol and tree backup/restore and the parsers are out of scope. **Falsifier:** for every verb and fixture, the façade's answer equals MORK's through `boundary.rs` (as sets, since MORK stores sets) and datafrog's (as bags where multiplicity matters); a refused shape is refused by name on both arms. Disable: let the façade answer a nested pattern by flattening it silently; the oracle must then disagree. +## 7d. D-MPS-9 `query_multi`: measured (2026-10-22) + +`boundary::mork_rules` runs any admitted rule set through MORK (set answers, plus `Space::query_multi` unification timed alone); `crepe-plan-probe/tests/mork_differential.rs` compares six fixtures with the reference. Results, costs and the open verbs: `entries/2026-10-22-d-mps-9-mork-oracle.md`. The other §7c verbs stay Queued. + ## 8. Deliverables | D-id | Item | Status | Gate / evidence | diff --git a/crates/crepe-plan-probe/examples/mork_split.rs b/crates/crepe-plan-probe/examples/mork_split.rs index 0ba0bb435..0ed810554 100644 --- a/crates/crepe-plan-probe/examples/mork_split.rs +++ b/crates/crepe-plan-probe/examples/mork_split.rs @@ -60,16 +60,12 @@ struct Native { execute: Duration, } -fn run_native( - rules: &[Rule], - demand: &Demand, - kind: ResultKind, - store: &Store, -) -> Native { +fn run_native(rules: &[Rule], demand: &Demand, kind: ResultKind, store: &Store) -> Native { let mut runs = Vec::with_capacity(RUNS); for _ in 0..RUNS { let t = Instant::now(); - let (out, rep) = evaluate(rules, demand, kind, Options::ALL, store).expect("native answers"); + let (out, rep) = + evaluate(rules, demand, kind, Options::ALL, store).expect("native answers"); let wall = t.elapsed(); black_box((&out, &rep.costs)); runs.push((wall, rep.costs)); @@ -184,14 +180,53 @@ fn main() { let count = run_native(&rules, &demand, ResultKind::Count(BAG), &store); print_native("native, Count(BAG) (terminal)", &count, input_rows); let bindings = run_native(&rules, &demand, ResultKind::Bindings(BAG), &store); - print_native("native, Bindings(BAG) (answer production)", &bindings, input_rows); + print_native( + "native, Bindings(BAG) (deferred handle; enumeration below)", + &bindings, + input_rows, + ); + // The bindings outcome is a deferred handle over the prepared tables; its + // `execute` cost does not include reading the answers. This times one + // full enumeration: every answer's three columns and weight are read and + // folded into a checksum, nothing is allocated per answer. + let mut enum_runs = Vec::with_capacity(RUNS); + let mut visited = 0u64; + for _ in 0..RUNS { + let t = Instant::now(); + let mut sum = 0u64; + let mut seen = 0u64; + answers.for_each(&rep.tables, |get, weight| { + sum = sum.wrapping_add(get(0) ^ get(1).rotate_left(21) ^ get(2).rotate_left(42)); + sum = sum.wrapping_add(weight); + seen += 1; + }); + enum_runs.push(t.elapsed()); + black_box(sum); + visited = seen; + } + assert_eq!( + visited as usize, + native_set.len(), + "one visit per answer under this fixture" + ); + println!( + "{}", + show(" enumerate all answers", median(enum_runs), input_rows) + ); let med = |f: &dyn Fn(&OracleCost) -> Duration| median(costs.iter().map(f).collect()); println!("MORK oracle (set semantics, matches = {matches})"); - println!("{}", show("encode + build", med(&|c| c.encode_build), input_rows)); println!( "{}", - show("match only (query_multi)", med(&|c| c.match_only), input_rows) + show("encode + build", med(&|c| c.encode_build), input_rows) + ); + println!( + "{}", + show( + "match only (query_multi)", + med(&|c| c.match_only), + input_rows + ) ); println!( "{}", diff --git a/crates/crepe-plan-probe/src/mork_api.rs b/crates/crepe-plan-probe/src/mork_api.rs index bab3c3ffa..66658d69e 100644 --- a/crates/crepe-plan-probe/src/mork_api.rs +++ b/crates/crepe-plan-probe/src/mork_api.rs @@ -117,7 +117,8 @@ pub fn to_oracle(rule: &Rule) -> Result { ), }) }; - let terms = |ts: &[Term]| -> Result, MorkRefusal> { ts.iter().map(term).collect() }; + let terms = + |ts: &[Term]| -> Result, MorkRefusal> { ts.iter().map(term).collect() }; let body = rule .body .iter() diff --git a/crates/crepe-plan-probe/tests/mork_differential.rs b/crates/crepe-plan-probe/tests/mork_differential.rs index f01589711..6f705c0f7 100644 --- a/crates/crepe-plan-probe/tests/mork_differential.rs +++ b/crates/crepe-plan-probe/tests/mork_differential.rs @@ -252,14 +252,19 @@ fn oracle_facts(fx: &Fixture) -> Vec> { /// The reference's distinct head tuples, narrowed to `u32` (MORK's symbols). fn reference_set(fx: &Fixture) -> BTreeSet> { - reference::eval(&fx.rules, fx.goal, &fx.demand(), &raw(&fx.labels, &fx.store)) - .keys() - .map(|row| { - row.iter() - .map(|&v| u32::try_from(v).expect("fixture values fit u32")) - .collect() - }) - .collect() + reference::eval( + &fx.rules, + fx.goal, + &fx.demand(), + &raw(&fx.labels, &fx.store), + ) + .keys() + .map(|row| { + row.iter() + .map(|&v| u32::try_from(v).expect("fixture values fit u32")) + .collect() + }) + .collect() } fn mork_set(fx: &Fixture) -> (BTreeSet>, OracleCost) { @@ -346,10 +351,19 @@ fn the_duplicate_allowed_row_is_what_separates_bag_from_set_matches() { let all = fixtures(); let fx = all.iter().find(|f| f.name == "family").unwrap(); let (_, cost) = mork_set(fx); - let bag: u64 = reference::eval(&fx.rules, fx.goal, &fx.demand(), &raw(&fx.labels, &fx.store)) - .values() - .sum(); - assert!(bag > cost.matches, "bag {bag} must exceed set {}", cost.matches); + let bag: u64 = reference::eval( + &fx.rules, + fx.goal, + &fx.demand(), + &raw(&fx.labels, &fx.store), + ) + .values() + .sum(); + assert!( + bag > cost.matches, + "bag {bag} must exceed set {}", + cost.matches + ); } /// `to_oracle` refuses exactly what `admit` refuses, and returns that refusal diff --git a/crates/mork-pathmap-probe/src/boundary.rs b/crates/mork-pathmap-probe/src/boundary.rs index c443c886a..7712717ac 100644 --- a/crates/mork-pathmap-probe/src/boundary.rs +++ b/crates/mork-pathmap-probe/src/boundary.rs @@ -530,7 +530,7 @@ fn check_rule(rule: &OracleRule) -> Result<(), Refusal> { let bound = rule .body .iter() - .any(|a| a.terms.iter().any(|b| *b == OracleTerm::Var(*v))); + .any(|a| a.terms.contains(&OracleTerm::Var(*v))); if !bound { return Err(Refusal::Upstream("unbound head var".into())); } @@ -591,7 +591,11 @@ pub fn mork_rules( // One caller-owned expression buffer for every pattern parse, alive across // the whole function so no `Expr` outlives its bytes. - let longest = rules.iter().map(|r| pattern_text(r).len()).max().unwrap_or(0); + let longest = rules + .iter() + .map(|r| pattern_text(r).len()) + .max() + .unwrap_or(0); let mut buf: Vec = vec![0; 64 * longest + 4096]; let mut out = TupleSet::default(); From bd62d55f37f35af96ce5c28c7ec4a1515c5c8785 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 05:36:15 +0000 Subject: [PATCH 3/6] board: math-compiler Stage A gap matrix (egglog -> R2IL) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .../2026-10-22-math-compiler-gap-matrix.md | 27 +++++++++++++++++++ .claude/board/entries/README.md | 3 ++- 2 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-22-math-compiler-gap-matrix.md diff --git a/.claude/board/entries/2026-10-22-math-compiler-gap-matrix.md b/.claude/board/entries/2026-10-22-math-compiler-gap-matrix.md new file mode 100644 index 000000000..ab1a5cc0e --- /dev/null +++ b/.claude/board/entries/2026-10-22-math-compiler-gap-matrix.md @@ -0,0 +1,27 @@ +# 2026-10-22 — Proof-carrying math compiler: Stage A gap matrix (egglog → R2IL) + +**Status:** OPEN. Inventory only; no code. Read at `origin/main` `3b723df1`, egglog fork `main` `9c8396d`. Falsifiers E1–E5 are the ones registered in `.arxiv/2304.04332_egglog_equality_saturation_datalog_excerpt.md:23-28` (P6/P12 in `.arxiv/2026-10_qr256_gaussian_egglog_rotation_falsifier_paths.md`). D-RFT-2 (`d-rft-relalg-thought-git-frontier-v1.md`) is the owning plan; no new plan. + +| Piece | State | Where | Note | +|---|---|---|---| +| egglog equality saturation + proofs | EXISTS (fork) | AdaWorldAPI/egglog `prove`, `prove-variants` (#1, #2), `ProofStore`/`ProofId` | no lance-graph crate depends on egglog today (no Cargo.toml names it) | +| independent proof check callable from outside egglog | MISSING | `ProofStore::check_proof` is `pub(crate)` | demonstrated gap for E4; the only fork change this slice needs | +| bounded saturation | EXISTS | egglog `run` with iteration limit; no node/time limit exposed as a typed outcome | E5 needs a typed "incomplete" result, not an error | +| typed single-table measure IR + guarded rules | EXISTS | contract `set_rules`: `Measure {Const, Count, Sum, CountRows, Opaque, Add, Sub}`, `Semantics {universe, arith, truth, sums, population}`, 8 rules with per-rule `Refusal` | the guard vocabulary (Exact/Wrapping/Checked/Ieee, TwoValued/ThreeValued, Distinct/Bag, Plain/Sym) already covers E3's OR/XOR-free half | +| multiplication / scale-by-constant in the measure IR | MISSING | `Measure` has no `Mul`/`Scale` | E1 (`z = 8c`) cannot be written in the contract IR today | +| Boolean OR vs GF(2) XOR as separate laws | PARTIAL | R2IL has `INT_OR` and `INT_XOR` as distinct ops; `set_algebra` is Boolean; no XOR set law | E3's OR/XOR arm needs an egglog sort split, not a contract change | +| relalg lowering to R2IL / mask-risc | EXISTS | `relalg::lower::run`, `run_with_program`, `run_as_written`; `program::run_program` (`let` planes, U2) | lowers `Rel` + `Measure {Count, Sum, Min, Max, Keep}` | +| scalar arithmetic in R2IL | EXISTS | `INT_ADD`, `INT_SUB`, `INT_MULT`, `INT_S_DIV`: scalar × scalar, checked `i64` | | +| lane arithmetic in R2IL | MISSING (by design) | `FoldError::LaneVersusLane` | a lane-scale `8 * c[i]` is not expressible; `SUM(8·c) = 8·SUM(c)` is (scalar after the fold) | +| reusable parameterized procedures | EXISTS | `r2il::procs` (`filter_lt`, `count`, `sum`, `group_sum`, `avg_parts`, …) | the compile target for B | +| group counts keyed by a slot | EXISTS | mask-risc `Terminal::GroupReduce { key: GroupKey, fold }` (COUNT/MIN/…), `GroupSumI32`, `GroupPowerSumsI32` | Example B's `GROUP_COUNT(R, y)` | +| dot product over a shared domain (`Σ_y r[y]·s[y]`) | MISSING | no Terminal with a dot/product doc line | Example B's last step is a scalar loop today (`join.rs` `bag_count`) | +| co-addressed domain for B | EXISTS (lab) | `mork-pathmap-probe::join::JoinDomain`, `JoinTable` (D-MPS-8, not admitted) | ADMISSION B review still owed | +| shared `let` planes (Example C) | EXISTS | contract `set_program` + `relalg::program` (U2 measured), `crepe-plan-probe::cse` (U3) | no egglog needed for C's baseline | +| Boolean composition (Example D) | EXISTS (lab) | `rmap::Tile`, `tile_gemm`, DR256 (#1666), `dir-rmap-probe` (#1685) | | +| Thought-Git replay receipt | EXISTS (lab) | `thought-git-probe::receipt` (generations, ABA guard) | no substitution/proof link; grep `substitut`/`egglog` in the crate: 0 hits | +| ClassView method DAG | EXISTS | contract `ClassView::compute_dag` (`class_view.rs:1403`), `ComputeEdge` | consumer for compiled-pattern identity, later | +| logical traceroute | PARTIAL | `set_rules::Trace { steps, refusals, budget_exhausted }` | rule-level only; no proof link, no binding requirements | +| three cache identities (law / pattern / register) | MISSING as types | witnesses exist separately (`RelationView.generation`, receipts) | | + +**Smallest seam for Stage B (E1):** one lab crate that (1) encodes an exact-integer term language in egglog, (2) proves `z = 8c` from the premises with `prove`/`prove-variants`, (3) checks the proof with a newly public egglog checker, (4) extracts by a declared cost, (5) lowers to existing R2IL scalar ops over a `SUM` fold, (6) runs it on mask-risc, (7) compares with an exact oracle, (8) prints the traceroute. Open choice: whether the term language lives in the probe or `Measure` gains a guarded `Scale` in the contract (contract owner). diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 071f99977..0de90d968 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -426 entries, 2026-08-06 .. 2026-10-22. +427 entries, 2026-08-06 .. 2026-10-22. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-22 | `math-compiler-gap-matrix` | | [2026-10-22-math-compiler-gap-matrix.md](2026-10-22-math-compiler-gap-matrix.md) | | 2026-10-22 | `D-MPS-9` | | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) | | 2026-10-21 | `zero-copy-join-index-map` | | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) | | 2026-10-21 | `D-RU-4` | | [2026-10-21-u4-coaddressed-join.md](2026-10-21-u4-coaddressed-join.md) | From 5ac40740b4c62d4123d5a723116ce43366aeeaeb Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 06:04:23 +0000 Subject: [PATCH 4/6] mork-pathmap-probe: refuse rules past MORK's 63-child arity before parsing Codex P2 on #1690: a 63-atom body or 63-term head passed admit and reached MORK's encoder, whose six-bit arity tag asserts a < 64. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/mork-pathmap-probe/src/boundary.rs | 18 ++++++++ .../mork-pathmap-probe/tests/differential.rs | 46 +++++++++++++++++++ 2 files changed, 64 insertions(+) diff --git a/crates/mork-pathmap-probe/src/boundary.rs b/crates/mork-pathmap-probe/src/boundary.rs index 7712717ac..f968bb0fd 100644 --- a/crates/mork-pathmap-probe/src/boundary.rs +++ b/crates/mork-pathmap-probe/src/boundary.rs @@ -518,7 +518,25 @@ fn parse_tuple(rest: &[u8]) -> Option> { } /// Checks one rule before anything is built. +/// The most children one MORK expression can have: its arity tag is six bits +/// (`mork_expr::item_byte`, `Tag::Arity(a)` asserts `a < 64`). +pub const MORK_MAX_CHILDREN: usize = 63; + fn check_rule(rule: &OracleRule) -> Result<(), Refusal> { + // Every expression the oracle writes, counted with its head symbol: the + // conjunction `(, atoms…)`, the head `(Q terms…)` and each atom + // `(r terms…)`. Past the limit MORK's encoder would panic (debug) or + // write a reserved tag (release), so the rule is refused before parsing. + let widest = std::iter::once(rule.body.len() + 1) + .chain(std::iter::once(rule.head.len() + 1)) + .chain(rule.body.iter().map(|a| a.terms.len() + 1)) + .max() + .unwrap_or(0); + if widest > MORK_MAX_CHILDREN { + return Err(Refusal::Upstream(format!( + "expression with {widest} children; MORK encodes at most {MORK_MAX_CHILDREN}" + ))); + } if rule.body.is_empty() { return Err(Refusal::Upstream("empty body".into())); } diff --git a/crates/mork-pathmap-probe/tests/differential.rs b/crates/mork-pathmap-probe/tests/differential.rs index 73ea63418..6728f7f78 100644 --- a/crates/mork-pathmap-probe/tests/differential.rs +++ b/crates/mork-pathmap-probe/tests/differential.rs @@ -264,3 +264,49 @@ fn general_rules_agree_with_the_fixed_query() { // (1,10,100) (1,10,102) (1,11,101) (2,10,100) (2,10,102). assert_eq!(cost.matches, 5); } + +/// FAILS IF: a rule wider than MORK's six-bit arity reaches MORK's parser. A +/// conjunction of 62 atoms (63 children with `,`) is answered; 63 atoms, a +/// 63-term head and a 63-term atom are refused by name, never parsed. +#[test] +fn rules_past_morks_arity_limit_are_refused_before_parsing() { + use mork_pathmap_probe::boundary::{ + MORK_MAX_CHILDREN, OracleAtom, OracleFacts, OracleRule, OracleTerm, mork_rules, + }; + let r = RelationView::from_rows(&[[1, 2]], 1); + let facts = [OracleFacts { + rel: 0, + arity: 2, + view: &r, + }]; + let atom = || OracleAtom { + rel: 0, + terms: vec![OracleTerm::Var(0), OracleTerm::Var(1)], + }; + let rule = |atoms: usize, head: usize| OracleRule { + head: (0..head).map(|_| OracleTerm::Var(0)).collect(), + body: (0..atoms).map(|_| atom()).collect(), + }; + let at_limit = rule(MORK_MAX_CHILDREN - 1, 1); + let (set, _) = mork_rules(&facts, &[at_limit]).expect("62 atoms fit"); + assert_eq!(set.rows.len(), 1); + for (name, wide) in [ + ("63 atoms", rule(MORK_MAX_CHILDREN, 1)), + ("63-term head", rule(1, MORK_MAX_CHILDREN)), + ( + "63-term atom", + OracleRule { + head: vec![OracleTerm::Var(0)], + body: vec![OracleAtom { + rel: 0, + terms: (0..MORK_MAX_CHILDREN as u16).map(OracleTerm::Var).collect(), + }], + }, + ), + ] { + assert!( + matches!(mork_rules(&facts, &[wide]), Err(Refusal::Upstream(_))), + "{name}" + ); + } +} From 4be4c0416271d9c3789e77d822276792f41e1337 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 06:23:41 +0000 Subject: [PATCH 5/6] egglog-r2il-probe: E1 end to end, probe-local (Stage B) Exact-integer symbolic substitution (a = 2b, b = 2c, z = 2a gives z = 8c) compiled cold by egglog through its public API (proofs mode, prove-variants, every proof checked by egglog), lowered onto the existing R2IL scalar INT_MULT through FoldDialect, and compared with an independent i128 oracle. - Law domains are the contract's set_rules::Arith; the probe owns two laws (MulAssoc, ConstFold) whose rule id carries the domain. Checked and Ieee refuse reassociation; ConstFold is Exact only. - Extraction is egglog's own: non-target variables are (Def String :cost 1000), so the cheapest variant other than the goal's own name is the answer. - Falsifiers: missing premise refuses (UnboundVar, oracle None, egglog cannot prove 8c); overflow counterexamples refuse in Exact and Checked with the i64::MAX/8 boundary passing; a Wrapping term is not lowered onto checked arithmetic; extraction is deterministic; bounded fuel reports Incomplete. - No contract::Measure change, no new opcode, no egglog change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- crates/egglog-r2il-probe/Cargo.toml | 43 +++ .../examples/e1_cold_cost.rs | 68 ++++ crates/egglog-r2il-probe/src/encode.rs | 110 +++++++ crates/egglog-r2il-probe/src/laws.rs | 131 ++++++++ crates/egglog-r2il-probe/src/lib.rs | 307 ++++++++++++++++++ crates/egglog-r2il-probe/src/lower.rs | 130 ++++++++ crates/egglog-r2il-probe/src/oracle.rs | 70 ++++ crates/egglog-r2il-probe/src/session.rs | 131 ++++++++ crates/egglog-r2il-probe/src/term.rs | 202 ++++++++++++ crates/egglog-r2il-probe/src/trace.rs | 168 ++++++++++ crates/egglog-r2il-probe/tests/e1.rs | 250 ++++++++++++++ 11 files changed, 1610 insertions(+) create mode 100644 crates/egglog-r2il-probe/Cargo.toml create mode 100644 crates/egglog-r2il-probe/examples/e1_cold_cost.rs create mode 100644 crates/egglog-r2il-probe/src/encode.rs create mode 100644 crates/egglog-r2il-probe/src/laws.rs create mode 100644 crates/egglog-r2il-probe/src/lib.rs create mode 100644 crates/egglog-r2il-probe/src/lower.rs create mode 100644 crates/egglog-r2il-probe/src/oracle.rs create mode 100644 crates/egglog-r2il-probe/src/session.rs create mode 100644 crates/egglog-r2il-probe/src/term.rs create mode 100644 crates/egglog-r2il-probe/src/trace.rs create mode 100644 crates/egglog-r2il-probe/tests/e1.rs diff --git a/crates/egglog-r2il-probe/Cargo.toml b/crates/egglog-r2il-probe/Cargo.toml new file mode 100644 index 000000000..93e03211c --- /dev/null +++ b/crates/egglog-r2il-probe/Cargo.toml @@ -0,0 +1,43 @@ +# egglog-r2il-probe: Stage B, E1 end to end. Lab only. +# +# Exact-integer symbolic substitution (`a = 2*b`, `b = 2*c`, `z = 2*a` gives +# `z = 8*c`) compiled COLD by egglog (public API only, proofs mode, every proof +# already checked by egglog's own `check_proof`), then lowered onto the EXISTING +# R2IL scalar arithmetic (`INT_MULT` through `FoldDialect`), and compared with +# an independent i128 oracle. Nothing here is a production path; no opcode is +# added; no population measure is involved. +# +# Own [workspace] root, excluded from the lance-graph workspace like +# mork-pathmap-probe. Run from THIS directory: +# cargo test +# cargo run --release --example e1_cold_cost +[package] +name = "egglog-r2il-probe" +version = "0.0.0" +edition = "2024" +publish = false +description = "Stage B probe: egglog as a cold, bounded, proof-producing compiler for exact-integer substitution, lowered onto existing R2IL scalar arithmetic and checked against an i128 oracle. Results only; no production path." + +[workspace] + +[dependencies] +# Public API only (EGraph::new_with_proofs, parse_and_run_program, prove-variants). +egglog = { git = "https://github.com/AdaWorldAPI/egglog", branch = "main" } +# `set_rules::Arith`, the law-domain vocabulary. The catalogue is NOT copied. +lance-graph-contract = { path = "../lance-graph-contract" } +# FoldDialect, Val, INT_MULT, FoldError. +lance-graph-r2il = { path = "../lance-graph-r2il" } +# Planes / Foreign, the (empty) planes a scalar-only FoldDialect is built over. +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } +# The `Dialect` trait whose `call` is the interpreter seam. Same coordinate as +# lance-graph-r2il, so the graph holds one ogar-loco. +ogar-loco = { git = "https://github.com/AdaWorldAPI/OGAR", branch = "main" } + +# One contract and one ndarray identity (OGAR's crates name the contract by its +# git coordinate; mask-risc names ndarray by its git coordinate). Same patches +# as dir-rmap-probe / the lance-graph root. +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "../lance-graph-contract" } + +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "../../../ndarray" } diff --git a/crates/egglog-r2il-probe/examples/e1_cold_cost.rs b/crates/egglog-r2il-probe/examples/e1_cold_cost.rs new file mode 100644 index 000000000..ad6dba4f4 --- /dev/null +++ b/crates/egglog-r2il-probe/examples/e1_cold_cost.rs @@ -0,0 +1,68 @@ +//! In-fold cost of E1 (encode, and lowering + execution on R2IL), release +//! build, median of 5. +//! +//! The egglog phase is timed in `Compiled::timings.egglog` but NOT printed: +//! it is a cold, out-of-fold compile whose cost is above the workspace's +//! microsecond budget, and whether cold-compile costs may be reported at all +//! is an open operator decision (lance-graph `CLAUDE.md`, "no millisecond +//! results"). Until it is ruled, this example does not publish that number. +//! +//! cargo run --release --example e1_cold_cost +//! +//! Agreement with the oracle is asserted FIRST; a number for a wrong answer is +//! not worth printing. + +use std::time::{Duration, Instant}; + +use egglog_r2il_probe::{Arith, compile, e1_problem, lower_and_run, oracle}; + +const RUNS: usize = 5; +const C: i64 = 123_456; + +fn median(mut v: Vec) -> Duration { + v.sort(); + v[v.len() / 2] +} + +fn micros(d: Duration) -> u128 { + d.as_micros() +} + +fn main() { + let p = e1_problem(); + + // Agreement first. + let probe = compile(&p, Arith::Exact, 8); + assert!(probe.error.is_none(), "egglog error: {:?}", probe.error); + let got = lower_and_run(&probe, &[("c", C)]).expect("lowers and runs"); + let want = oracle::solve(&p, C).expect("oracle answers"); + assert_eq!( + i128::from(got), + want, + "lowered value disagrees with the oracle" + ); + + let mut encode = Vec::with_capacity(RUNS); + let mut lower = Vec::with_capacity(RUNS); + for _ in 0..RUNS { + let c = compile(&p, Arith::Exact, 8); + assert!(c.error.is_none(), "egglog error: {:?}", c.error); + encode.push(c.timings.encode); + let t = Instant::now(); + let v = lower_and_run(&c, &[("c", C)]).expect("lowers and runs"); + lower.push(t.elapsed()); + assert_eq!(i128::from(v), want); + } + + println!("in-fold costs; reported, not gates (egglog phase withheld, see module doc)"); + println!("E1 under Exact, fuel 8, c = {C}, median of {RUNS}, microseconds:"); + println!( + " encode {:>10}", + micros(median(encode)) + ); + println!( + " lower + execute {:>10}", + micros(median(lower)) + ); + println!(" extracted: {}", probe.extracted); +} diff --git a/crates/egglog-r2il-probe/src/encode.rs b/crates/egglog-r2il-probe/src/encode.rs new file mode 100644 index 000000000..a71e27726 --- /dev/null +++ b/crates/egglog-r2il-probe/src/encode.rs @@ -0,0 +1,110 @@ +//! Problem -> egglog program text. +//! +//! One datatype, one `union` per premise, the admitted rewrites in a single +//! `arith` ruleset. Saturation is driven from Rust one `(run arith 1)` step at +//! a time (see `crate::session`), because a combined `(run arith FUEL)` report +//! cannot tell saturation from fuel exhaustion in proofs mode (the report +//! ANDs `can_stop` across the rebuild iterations; see the finding in +//! `session.rs`). +//! +//! Constants: premise coefficients are used as given. Nothing here can +//! overflow egglog: its `i64` `*` is `checked_mul` and a failing primitive +//! just stops the rule from firing. + +use crate::laws::RuleId; +use crate::{Problem, laws}; + +/// The datatype and the (empty) ruleset. +/// +/// `Def` carries `:cost 1000` (datatype variant syntax, egglog +/// `src/ast/parse.rs:1051`). With egglog's default AST-size cost every other +/// node costs 1, so the cheapest member of a defined variable's e-class is any +/// expansion of fewer than 1000 nodes, never the name. The extraction that +/// picks the answer is therefore egglog's own; the probe adds no search. +pub const HEADER: &str = "(datatype Term (Num i64) (Var String) (Def String :cost 1000) (Mul Term Term))\n(ruleset arith)\n"; + +/// The one-step schedule. `(run )` parses as `Repeat(n, Run)` +/// (egglog `src/ast/parse.rs:670-698`). +pub const STEP: &str = "(run arith 1)"; + +/// A variable as a term: `(Var "c")` for the target, `(Def "a")` otherwise. +pub fn sym(name: &str, target: &str) -> String { + if name == target { + format!("(Var {name:?})") + } else { + format!("(Def {name:?})") + } +} + +/// The setup program: header, premises, admitted rewrites. +pub fn setup(problem: &Problem, admitted: &[RuleId]) -> String { + let t = problem.target_var; + let mut s = String::from(HEADER); + for eq in &problem.premises { + s.push_str(&format!( + "(union {} (Mul (Num {}) {}))\n", + sym(eq.lhs, t), + eq.coeff, + sym(eq.rhs, t) + )); + } + for id in admitted { + s.push_str(laws::rewrite_text(*id)); + s.push('\n'); + } + s +} + +/// `(prove-variants n)`. +pub fn prove_variants(problem: &Problem, n: usize) -> String { + format!( + "(prove-variants {} {n})", + sym(problem.goal, problem.target_var) + ) +} + +/// `(prove (= ))`. +pub fn prove_eq(problem: &Problem, rhs_term: &str) -> String { + format!( + "(prove (= {} {rhs_term}))", + sym(problem.goal, problem.target_var) + ) +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::Eq; + use lance_graph_contract::set_rules::Arith; + + /// FAILS IF: the encoding stops emitting one union per premise, or emits a + /// rewrite for a refused law (Checked admits none). + #[test] + fn setup_has_one_union_per_premise_and_only_admitted_rules() { + let p = Problem { + premises: vec![ + Eq { + lhs: "a", + coeff: 2, + rhs: "b", + }, + Eq { + lhs: "z", + coeff: 2, + rhs: "a", + }, + ], + goal: "z", + target_var: "b", + }; + let (exact, _) = laws::admit_all(Arith::Exact); + let (checked, _) = laws::admit_all(Arith::Checked); + let e = setup(&p, &exact); + let c = setup(&p, &checked); + assert_eq!(e.matches("(union ").count(), 2); + assert_eq!(e.matches("(rewrite ").count(), 2); + assert_eq!(c.matches("(union ").count(), 2); + assert_eq!(c.matches("(rewrite ").count(), 0); + assert!(e.contains(r#"(union (Def "a") (Mul (Num 2) (Var "b")))"#)); + } +} diff --git a/crates/egglog-r2il-probe/src/laws.rs b/crates/egglog-r2il-probe/src/laws.rs new file mode 100644 index 000000000..b76d669b8 --- /dev/null +++ b/crates/egglog-r2il-probe/src/laws.rs @@ -0,0 +1,131 @@ +//! The probe's two arithmetic laws and their domain guards. The whole table; +//! nothing else is admitted. +//! +//! | law | rewrite | Exact | Wrapping | Checked | Ieee | +//! |------------|----------------------------------------------------------------|-------|----------|---------|------| +//! | MulAssoc | `(Mul (Num x) (Mul (Num y) t)) => (Mul (Mul (Num x) (Num y)) t)` | admit | admit | refuse | refuse | +//! | ConstFold | `(Mul (Num x) (Num y)) => (Num (* x y))` | admit | refuse | refuse | refuse | +//! +//! The domains are the contract's own +//! ([`lance_graph_contract::set_rules::Arith`], set_rules.rs:34); the +//! contract's catalogue is neither copied nor extended here. + +use lance_graph_contract::set_rules::Arith; + +/// The two laws. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, PartialOrd, Ord)] +pub enum LawId { + /// `x * (y * t) = (x * y) * t`. + MulAssoc, + /// `Num x * Num y = Num (x * y)`. + ConstFold, +} + +/// A law admitted in a domain: the legal domain is part of the id, so a rule +/// cannot be named without the arithmetic it is valid in. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +pub struct RuleId { + /// Which law. + pub law: LawId, + /// The arithmetic domain it was admitted under. + pub domain: Arith, +} + +/// Why a law is not admitted in a domain. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum LawRefusal { + /// Re-association is not a theorem of this arithmetic. + /// + /// * `Checked`: an overflow is an error the caller sees, and + /// `set_rules.rs:40-42` says it in one line: "A rewrite that removes an + /// overflow the original would report changes the answer." Reassociating + /// `2 * (2 * (2 * c))` into `(2 * 2 * 2) * c` can move or remove the + /// point at which the checked product leaves `i64`. + /// * `Ieee`: floating-point multiplication is not associative. + NotAssociative(Arith), + /// Constant folding through egglog's `*` is not this domain's multiply. + /// + /// egglog's `i64` `*` is `a.checked_mul(b)` (egglog `src/sort/i64.rs:31`): + /// on overflow the primitive FAILS (no panic, no wrap) and the rule simply + /// does not fire. That matches no domain except an exact one that never + /// overflows: + /// + /// * `Wrapping`: the fold would need two's-complement `wrapping_mul`, which + /// egglog does not offer, so the folded constant could be absent where + /// the wrapping program has a value. + /// * `Checked`: the fold would hide an overflow the original reports. + /// * `Ieee`: not an integer domain. + NotExactFold(Arith), +} + +/// Admits `law` in `domain`, or says why not. +pub fn admit(law: LawId, domain: Arith) -> Result { + match (law, domain) { + (LawId::MulAssoc, Arith::Exact | Arith::Wrapping) => Ok(RuleId { law, domain }), + (LawId::MulAssoc, d @ (Arith::Checked | Arith::Ieee)) => Err(LawRefusal::NotAssociative(d)), + (LawId::ConstFold, Arith::Exact) => Ok(RuleId { law, domain }), + (LawId::ConstFold, d @ (Arith::Wrapping | Arith::Checked | Arith::Ieee)) => { + Err(LawRefusal::NotExactFold(d)) + } + } +} + +/// Both laws against one domain, in table order. +pub fn admit_all(domain: Arith) -> (Vec, Vec<(LawId, LawRefusal)>) { + let mut admitted = Vec::new(); + let mut refused = Vec::new(); + for law in [LawId::MulAssoc, LawId::ConstFold] { + match admit(law, domain) { + Ok(id) => admitted.push(id), + Err(why) => refused.push((law, why)), + } + } + (admitted, refused) +} + +/// The egglog `rewrite` for an admitted law, in the `arith` ruleset. +/// +/// ConstFold's RHS `(Num (* x y))` uses the `i64` `*` primitive, which is +/// `checked_mul`: an overflowing fold does not fire, it does not panic. +pub fn rewrite_text(id: RuleId) -> &'static str { + match id.law { + LawId::MulAssoc => { + "(rewrite (Mul (Num x) (Mul (Num y) t)) (Mul (Mul (Num x) (Num y)) t) :ruleset arith)" + } + LawId::ConstFold => "(rewrite (Mul (Num x) (Num y)) (Num (* x y)) :ruleset arith)", + } +} + +#[cfg(test)] +mod tests { + use super::*; + + /// FAILS IF: the table drifts from the spec: every cell is checked, so a + /// guard that admits too much or too little in any domain fails. + #[test] + fn the_whole_table() { + use Arith::*; + use LawId::*; + let want = [ + (MulAssoc, Exact, true), + (MulAssoc, Wrapping, true), + (MulAssoc, Checked, false), + (MulAssoc, Ieee, false), + (ConstFold, Exact, true), + (ConstFold, Wrapping, false), + (ConstFold, Checked, false), + (ConstFold, Ieee, false), + ]; + for (law, dom, ok) in want { + assert_eq!(admit(law, dom).is_ok(), ok, "{law:?} in {dom:?}"); + } + assert_eq!( + admit(MulAssoc, Checked), + Err(LawRefusal::NotAssociative(Checked)) + ); + assert_eq!( + admit(ConstFold, Wrapping), + Err(LawRefusal::NotExactFold(Wrapping)) + ); + } +} diff --git a/crates/egglog-r2il-probe/src/lib.rs b/crates/egglog-r2il-probe/src/lib.rs new file mode 100644 index 000000000..0c0db1f8a --- /dev/null +++ b/crates/egglog-r2il-probe/src/lib.rs @@ -0,0 +1,307 @@ +//! Stage B, E1 end to end, probe-local. +//! +//! E1 is exact-integer SYMBOLIC SUBSTITUTION: the premises `a = 2*b`, +//! `b = 2*c`, `z = 2*a` imply `z = 8*c`. It is not a population measure: no +//! SUM fold, no lanes, no masks. +//! +//! The pipeline, each hop named by the traceroute ([`trace`]): +//! +//! 1. [`laws`] admits or refuses each of the probe's two laws for the chosen +//! [`Arith`] domain (the contract's own vocabulary). +//! 2. [`encode`] + `session` hand egglog (cold, bounded, public API only, +//! proofs mode) the premises and the admitted rewrites, step it up to +//! `fuel` times and report whether it saturated. +//! 3. The extraction is egglog's own: `prove-variants` on the goal, cheapest +//! first under its default AST-size cost, with every non-target variable a +//! `Def` priced at 1000 ([`encode::HEADER`]). The answer is the cheapest +//! variant that is not the goal's own name. egglog checks every proof it +//! returns. +//! 4. [`lower`] turns the term into calls on the EXISTING R2IL scalar +//! arithmetic (`INT_MULT` through `FoldDialect`); no new opcode. +//! 5. [`oracle`] recomputes the answer in `i128` from the original premises, +//! sharing no code with steps 2-4. + +pub mod encode; +pub mod laws; +pub mod lower; +pub mod oracle; +mod session; +pub mod term; +pub mod trace; + +use std::time::{Duration, Instant}; + +pub use lance_graph_contract::set_rules::Arith; +pub use laws::{LawId, LawRefusal, RuleId}; +pub use lower::{Step, lower_and_run, lower_steps}; +pub use term::Tm; + +use session::{Session, VARIANTS}; + +/// One premise: `lhs = coeff * rhs`. +#[derive(Debug, Clone, Copy, PartialEq)] +pub struct Eq { + /// The defined variable. + pub lhs: &'static str, + /// The integer coefficient. + pub coeff: i64, + /// The variable it is a multiple of. + pub rhs: &'static str, +} + +/// A substitution problem: from the premises, express `goal` in `target_var`. +#[derive(Debug, Clone, PartialEq)] +pub struct Problem { + /// The premises. + pub premises: Vec, + /// The variable to express. + pub goal: &'static str, + /// The variable the answer should be in. + pub target_var: &'static str, +} + +/// E1: `a = 2b`, `b = 2c`, `z = 2a`; goal `z` in terms of `c`. +pub fn e1_problem() -> Problem { + Problem { + premises: vec![ + Eq { + lhs: "a", + coeff: 2, + rhs: "b", + }, + Eq { + lhs: "b", + coeff: 2, + rhs: "c", + }, + Eq { + lhs: "z", + coeff: 2, + rhs: "a", + }, + ], + goal: "z", + target_var: "c", + } +} + +/// A longer chain `p0 = 2 p1, ..., p5 = 2 p6` (goal `p0` in `p6`), which +/// needs more saturation steps than E1. +pub fn chain_problem() -> Problem { + Problem { + premises: vec![ + Eq { + lhs: "p0", + coeff: 2, + rhs: "p1", + }, + Eq { + lhs: "p1", + coeff: 2, + rhs: "p2", + }, + Eq { + lhs: "p2", + coeff: 2, + rhs: "p3", + }, + Eq { + lhs: "p3", + coeff: 2, + rhs: "p4", + }, + Eq { + lhs: "p4", + coeff: 2, + rhs: "p5", + }, + Eq { + lhs: "p5", + coeff: 2, + rhs: "p6", + }, + ], + goal: "p0", + target_var: "p6", + } +} + +/// Whether egglog reached a fixpoint within the fuel. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Saturation { + /// A step changed nothing. `iterations` counts the steps run, INCLUDING + /// that last, quiet one. Zero means no rule was admitted, so no step ran. + Saturated { + /// Steps run, the final quiet step included. + iterations: usize, + }, + /// Every one of `fuel` steps still changed the e-graph: nothing is + /// certified about completeness. + Incomplete { + /// The step budget that was exhausted. + fuel: usize, + }, +} + +/// Wall-clock cost of the cold compile, split. Reported, never gated. +#[derive(Debug, Clone, Copy, Default)] +pub struct ColdCost { + /// Building the egglog program text and the law table. + pub encode: Duration, + /// egglog: setup, saturation, `prove-variants`. + pub egglog: Duration, +} + +/// The result of the cold compile. +#[derive(Debug, Clone)] +pub struct Compiled { + /// The arithmetic domain the laws were admitted under. + pub arith: Arith, + /// The variable the answer is expressed in. + pub target_var: &'static str, + /// Laws admitted, with their domain. + pub admitted: Vec, + /// Laws refused, with the reason. + pub refused: Vec<(LawId, LawRefusal)>, + /// Fixpoint or fuel exhaustion. + pub saturation: Saturation, + /// The chosen term, rendered `(Mul (Num 8) (Var "c"))`: egglog's cheapest + /// variant of the goal other than the goal's own `(Def "z")`, which is a + /// self-identity, not an answer. A defined variable left in it is + /// rendered `(Def "b")`. + pub extracted: String, + /// Every variant `prove-variants` returned for the goal, in egglog's + /// order (cheapest first). + pub variants: Vec, + /// egglog's checked proof text that `goal = extracted`; `None` when no + /// non-trivial variant exists. + pub proof: Option, + /// The extracted term mentions no variable other than `target_var`. + pub closed: bool, + /// Cold-compile cost. + pub timings: ColdCost, + /// Non-fatal observations. + pub notes: Vec, + /// A fatal egglog error; everything else is then at its default. + pub error: Option, +} + +/// Why a term could not be run on R2IL scalar arithmetic. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum LowerRefusal { + /// A variable with no supplied value. + UnboundVar(String), + /// A checked multiply left `i64`. + Overflow, + /// The term cannot be lowered at all. + NotLowerable(&'static str), +} + +/// Everything `prepare` leaves behind. +struct Prepared { + session: Session, + admitted: Vec, + refused: Vec<(LawId, LawRefusal)>, + saturation: Saturation, +} + +fn prepare(problem: &Problem, arith: Arith, fuel: usize) -> Result { + let (admitted, refused) = laws::admit_all(arith); + let program = encode::setup(problem, &admitted); + let mut session = Session::new(); + session.run(&program)?; + let saturation = session.saturate(fuel, !admitted.is_empty())?; + Ok(Prepared { + session, + admitted, + refused, + saturation, + }) +} + +/// Cold-compiles `problem` under `arith`, with at most `fuel` saturation +/// steps. Never panics on an egglog failure: it is returned in +/// [`Compiled::error`]. +pub fn compile(problem: &Problem, arith: Arith, fuel: usize) -> Compiled { + let t_encode = Instant::now(); + let (admitted, refused) = laws::admit_all(arith); + let _ = encode::setup(problem, &admitted); // priced here; rebuilt inside `prepare` + let encode_cost = t_encode.elapsed(); + + let mut out = Compiled { + arith, + target_var: problem.target_var, + admitted: admitted.clone(), + refused: refused.clone(), + saturation: Saturation::Incomplete { fuel }, + extracted: String::new(), + variants: Vec::new(), + proof: None, + closed: false, + timings: ColdCost { + encode: encode_cost, + egglog: Duration::ZERO, + }, + notes: Vec::new(), + error: None, + }; + + let t_egg = Instant::now(); + if let Err(e) = compile_inner(problem, arith, fuel, &mut out) { + out.error = Some(e); + } + out.timings.egglog = t_egg.elapsed(); + out +} + +fn compile_inner( + problem: &Problem, + arith: Arith, + fuel: usize, + out: &mut Compiled, +) -> Result<(), String> { + let Prepared { + mut session, + admitted, + refused, + saturation, + } = prepare(problem, arith, fuel)?; + out.admitted = admitted; + out.refused = refused; + out.saturation = saturation; + + // egglog's own extraction: variants cheapest first, each with its proof. + let proved = session.prove_variants(problem, VARIANTS)?; + out.variants = proved.iter().map(|(t, _)| t.clone()).collect(); + let goal_name = encode::sym(problem.goal, problem.target_var); + let pick = proved.iter().find_map(|(t, proof)| { + let tm = Tm::parse(t)?; + (tm.to_string() != goal_name).then(|| (tm, proof.clone())) + }); + match pick { + Some((tm, proof)) => { + out.closed = tm.foreign_vars(problem.target_var).is_empty(); + out.extracted = tm.to_string(); + out.proof = Some(proof); + } + None => { + out.extracted = goal_name; + out.notes + .push("no variant other than the goal itself".to_string()); + } + } + Ok(()) +} + +/// Runs the same setup and saturation as [`compile`], then asks egglog to +/// `(prove (= (Var goal) ))`. `Ok` is the checked proof text; `Err` +/// is egglog's refusal (or a setup failure). +pub fn try_prove( + problem: &Problem, + arith: Arith, + fuel: usize, + rhs_term: &str, +) -> Result { + let mut p = prepare(problem, arith, fuel)?; + p.session.prove_eq(problem, rhs_term) +} diff --git a/crates/egglog-r2il-probe/src/lower.rs b/crates/egglog-r2il-probe/src/lower.rs new file mode 100644 index 000000000..645649422 --- /dev/null +++ b/crates/egglog-r2il-probe/src/lower.rs @@ -0,0 +1,130 @@ +//! Extracted term -> existing R2IL scalar arithmetic. +//! +//! The lowering target is the opcode that already exists: push +//! [`Val::Scalar`] literals and call +//! `ogar_loco::Dialect::call(&mut FoldDialect, INT_MULT, [0; 3], &mut stack)`, +//! the exact pattern of `lance-graph-r2il/tests/procs.rs:953-962`. No new +//! opcode, no mask, no lane: `FoldDialect` is built over empty planes. +//! +//! `INT_MULT` is CHECKED (`checked_mul`, `lance-graph-r2il/src/lib.rs:1064`): +//! overflow is `FoldError::Overflow`, never a wrap. A term compiled under +//! `Arith::Wrapping` is therefore refused up front rather than run on +//! checked arithmetic and silently answered. + +use lance_graph_contract::set_rules::Arith; +use lance_graph_mask_risc::{Foreign, Planes}; +use lance_graph_r2il::{FoldDialect, FoldError, INT_MULT, Val}; +use ogar_loco::Dialect; + +use crate::term::Tm; +use crate::{Compiled, LowerRefusal}; + +/// One step of the lowered program, symbolic (no input value yet), so the +/// sequence is comparable across runs and independent of the inputs. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Step { + /// `push k`: a literal scalar. + PushConst(i64), + /// Push the supplied value of the named variable. + PushVar(String), + /// `call INT_MULT` on the top two scalars. + IntMult, +} + +impl Step { + /// Mnemonic for the traceroute. + pub fn mnemonic(&self) -> String { + match self { + Step::PushConst(k) => format!("push {k}"), + Step::PushVar(v) => format!("push ${v}"), + Step::IntMult => "INT_MULT".to_string(), + } + } +} + +/// Post-order walk: `Num k` pushes, `Var v` pushes, `Mul l r` is `l; r; INT_MULT`. +pub fn steps_of(tm: &Tm) -> Vec { + let mut out = Vec::new(); + walk(tm, &mut out); + out +} + +fn walk(tm: &Tm, out: &mut Vec) { + match tm { + Tm::Num(k) => out.push(Step::PushConst(*k)), + Tm::Var(v) | Tm::Def(v) => out.push(Step::PushVar(v.clone())), + Tm::Mul(l, r) => { + walk(l, out); + walk(r, out); + out.push(Step::IntMult); + } + } +} + +/// The call sequence for the compiled problem's extracted term. Refuses a +/// `Wrapping` term and an unparseable one. +pub fn lower_steps(c: &Compiled) -> Result, LowerRefusal> { + if c.arith == Arith::Wrapping { + return Err(LowerRefusal::NotLowerable( + "R2IL scalar arithmetic is checked, not wrapping", + )); + } + let tm = Tm::parse(&c.extracted).ok_or(LowerRefusal::NotLowerable( + "extracted term is not parseable", + ))?; + Ok(steps_of(&tm)) +} + +/// Lowers and executes. `inputs` supplies values by variable name; only +/// `c.target_var` may be read, any other variable is `UnboundVar`. +pub fn lower_and_run(c: &Compiled, inputs: &[(&str, i64)]) -> Result { + let steps = lower_steps(c)?; + run_steps(&steps, c.target_var, inputs) +} + +/// Executes a step list on a scalar-only `FoldDialect`. +pub fn run_steps( + steps: &[Step], + target_var: &str, + inputs: &[(&str, i64)], +) -> Result { + let planes = Planes { + n_rows: 0, + masks: &[], + lanes: &[], + }; + let mut d = FoldDialect::new(&planes, &Foreign::NONE); + let mut stack: Vec = Vec::new(); + for step in steps { + match step { + Step::PushConst(k) => stack.push(Val::Scalar(*k)), + Step::PushVar(v) => { + let value = (v == target_var) + .then(|| { + inputs + .iter() + .find(|(n, _)| *n == v.as_str()) + .map(|(_, x)| *x) + }) + .flatten(); + match value { + Some(x) => stack.push(Val::Scalar(x)), + None => return Err(LowerRefusal::UnboundVar(v.clone())), + } + } + Step::IntMult => { + // Same call shape as lance-graph-r2il/tests/procs.rs:958-960. + d.call(INT_MULT, [0; 3], &mut stack).map_err(|e| match e { + FoldError::Overflow(_) => LowerRefusal::Overflow, + _ => LowerRefusal::NotLowerable("fold dialect refused INT_MULT"), + })?; + } + } + } + match stack.as_slice() { + [Val::Scalar(r)] => Ok(*r), + _ => Err(LowerRefusal::NotLowerable( + "lowering did not leave exactly one scalar", + )), + } +} diff --git a/crates/egglog-r2il-probe/src/oracle.rs b/crates/egglog-r2il-probe/src/oracle.rs new file mode 100644 index 000000000..cdf0137d4 --- /dev/null +++ b/crates/egglog-r2il-probe/src/oracle.rs @@ -0,0 +1,70 @@ +//! The independent oracle: plain `i128` substitution over the ORIGINAL +//! premises. It shares no code with the egglog encoding, the extraction, or +//! the lowering; it never sees the extracted term. + +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. + for _ in 0..=problem.premises.len() { + let mut progressed = false; + for eq in &problem.premises { + if known.contains_key(eq.lhs) { + 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; + } + } + if !progressed { + break; + } + } + known.get(problem.goal).copied() +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::{Eq, e1_problem}; + + /// FAILS IF: the oracle stops computing 8*c for E1, stops refusing a + /// disconnected goal, or truncates to i64 (the overflow counterexample + /// must come back as an i128 outside the i64 range). + #[test] + fn e1_is_8c_and_a_missing_premise_is_none() { + let p = e1_problem(); + assert_eq!(solve(&p, 7), Some(56)); + assert_eq!(solve(&p, -123_456), Some(-987_648)); + let big = solve(&p, i64::MAX).expect("i128 holds it"); + assert!(big > i128::from(i64::MAX)); + + let broken = Problem { + premises: vec![ + Eq { + lhs: "a", + coeff: 2, + rhs: "b", + }, + Eq { + lhs: "z", + coeff: 2, + rhs: "a", + }, + ], + goal: "z", + target_var: "c", + }; + assert_eq!(solve(&broken, 7), None); + } +} diff --git a/crates/egglog-r2il-probe/src/session.rs b/crates/egglog-r2il-probe/src/session.rs new file mode 100644 index 000000000..be91ceb85 --- /dev/null +++ b/crates/egglog-r2il-probe/src/session.rs @@ -0,0 +1,131 @@ +//! The only module that touches egglog, and only through its public API: +//! `EGraph::new_with_proofs`, `parse_and_run_program`, the +//! `prove` and `prove-variants` commands, `CommandOutput`, `ProvedVariants`. +//! egglog is not modified; every proof it returns has already been checked by +//! its own `check_proof` (egglog `src/proofs/proof_extraction.rs:126-139`). +//! +//! # Saturation versus fuel exhaustion +//! +//! The probe runs `(run arith 1)` itself, up to `fuel` times, and reads the +//! `changed()` flag of the FIRST iteration report of each step (the `arith` +//! ruleset's own iteration). A step that changed nothing is a fixpoint: +//! `Saturated`. If every one of the `fuel` steps changed something the probe +//! reports `Incomplete` and certifies nothing. +//! +//! Why not one `(run-schedule (repeat FUEL (run arith)))` and its `RunReport`? +//! In proofs mode egglog wraps every schedule with rebuild iterations +//! (`src/proofs/proof_encoding.rs:1498`, `instrument_schedule`), and +//! `RunReport::union` ANDs `can_stop` and ORs `updated` across all of them +//! (egglog-reports `src/lib.rs:260-264`), so the combined flags describe the +//! rebuilds as much as the rules and cannot be read as "the rules reached a +//! fixpoint". + +use egglog::{CommandOutput, EGraph, ProvedVariants}; + +use crate::Saturation; +use crate::{Problem, encode}; + +/// Variants requested per class (egglog returns at most one per e-node). +pub const VARIANTS: usize = 16; + +/// One proofs-mode e-graph. +pub struct Session { + egraph: EGraph, +} + +impl Session { + /// A fresh proofs-mode e-graph. + pub fn new() -> Self { + Session { + egraph: EGraph::new_with_proofs(), + } + } + + /// Runs program text; egglog errors become strings. + pub fn run(&mut self, text: &str) -> Result, String> { + self.egraph + .parse_and_run_program(None, text) + .map_err(|e| e.to_string()) + } + + /// Steps `arith` up to `fuel` times. `has_rules == false` (an empty + /// ruleset, nothing admitted) is saturated at zero iterations without + /// asking egglog to run an empty ruleset. + pub fn saturate(&mut self, fuel: usize, has_rules: bool) -> Result { + if !has_rules { + return Ok(Saturation::Saturated { iterations: 0 }); + } + for i in 1..=fuel { + let outs = self.run(encode::STEP)?; + if !step_changed(&outs) { + return Ok(Saturation::Saturated { iterations: i }); + } + } + Ok(Saturation::Incomplete { fuel }) + } + + /// `(prove-variants n)`: `(term, proof text)` per variant, in + /// the order egglog returns them (cheapest first). + /// + /// The result is recovered from `CommandOutput::UserDefined(arc)` with + /// `arc.as_ref().as_any().downcast_ref::()`: `as_ref()` + /// first, because the `Arc` itself also satisfies the blanket + /// `UserDefinedCommandOutput` impl and its `as_any` would describe the + /// `Arc`, not the payload (egglog `src/lib.rs:135-157`). + pub fn prove_variants( + &mut self, + problem: &Problem, + n: usize, + ) -> Result, String> { + let outs = self.run(&encode::prove_variants(problem, n))?; + for out in &outs { + if let CommandOutput::UserDefined(arc) = out + && let Some(pv) = arc.as_ref().as_any().downcast_ref::() + { + return Ok(pv + .variants + .iter() + .map(|v| (v.term.clone(), v.proof_store.proof_to_string(v.proof_id))) + .collect()); + } + } + Err("prove-variants returned no ProvedVariants".to_string()) + } + + /// `(prove (= rhs))`: the checked proof text, or egglog's error. + pub fn prove_eq(&mut self, problem: &Problem, rhs_term: &str) -> Result { + let outs = self.run(&encode::prove_eq(problem, rhs_term))?; + for out in &outs { + if let CommandOutput::ProveExists { + proof_store, + proof_id, + } = out + { + return Ok(proof_store.proof_to_string(*proof_id)); + } + } + Err("prove returned no proof".to_string()) + } +} + +impl Default for Session { + fn default() -> Self { + Self::new() + } +} + +/// Whether the `arith` ruleset changed the e-graph in one `(run arith 1)`: +/// the first `RunSchedule` output's first iteration. Falls back to the +/// report's `updated` flag if egglog returned no iteration list. +fn step_changed(outs: &[CommandOutput]) -> bool { + for out in outs { + if let CommandOutput::RunSchedule(report) = out { + return report + .iterations + .first() + .map_or(report.updated, |it| it.changed()); + } + } + // No report at all: do not claim a fixpoint. + true +} diff --git a/crates/egglog-r2il-probe/src/term.rs b/crates/egglog-r2il-probe/src/term.rs new file mode 100644 index 000000000..6b0c93b30 --- /dev/null +++ b/crates/egglog-r2il-probe/src/term.rs @@ -0,0 +1,202 @@ +//! The probe's term language, parsed back from egglog's rendered terms. +//! +//! egglog hands terms out as text (`TermDag::to_string`, e.g. +//! `(Mul (Num 8) (Var "c"))`). The probe reads them back into [`Tm`] so that +//! "closed" and the lowering walk operate on a structure, not on substrings. +//! A term egglog renders in a shape this parser does not know (for example a +//! `let` for a shared subterm) parses to `None` and is skipped, never guessed. + +use std::fmt; + +/// `(datatype Term (Num i64) (Var String) (Def String :cost 1000) (Mul Term Term))`. +/// +/// `Var` is the target variable, the only one an answer may mention. `Def` +/// is every other variable: a name the premises define, priced so that +/// egglog's own AST-size extraction prefers any expansion of it over the +/// name itself (see `crate::encode::HEADER`). +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] +pub enum Tm { + /// `(Num k)`. + Num(i64), + /// `(Var "v")`: the target variable. + Var(String), + /// `(Def "v")`: a non-target variable, defined by a premise. + Def(String), + /// `(Mul l r)`. + Mul(Box, Box), +} + +impl Tm { + /// Parses one rendered term. `None` when the text is not exactly one term + /// of the four constructors above. + pub fn parse(text: &str) -> Option { + let toks = tokenize(text)?; + let mut pos = 0; + let tm = parse_tm(&toks, &mut pos)?; + (pos == toks.len()).then_some(tm) + } + + /// Number of constructor nodes (the default AST-size cost, up to the + /// constant per-leaf weight). + pub fn size(&self) -> usize { + match self { + Tm::Num(_) | Tm::Var(_) | Tm::Def(_) => 1, + Tm::Mul(l, r) => 1 + l.size() + r.size(), + } + } + + /// Variable occurrences other than `target`, in left-to-right order. + pub fn foreign_vars(&self, target: &str) -> Vec { + let mut out = Vec::new(); + self.collect_foreign(target, &mut out); + out + } + + fn collect_foreign(&self, target: &str, out: &mut Vec) { + match self { + Tm::Num(_) => {} + Tm::Var(v) | Tm::Def(v) => { + if v != target { + out.push(v.clone()); + } + } + Tm::Mul(l, r) => { + l.collect_foreign(target, out); + r.collect_foreign(target, out); + } + } + } +} + +/// Canonical rendering, byte-identical to egglog's for these four +/// constructors: `(Mul (Num 8) (Var "c"))`. +impl fmt::Display for Tm { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + Tm::Num(k) => write!(f, "(Num {k})"), + Tm::Var(v) => write!(f, "(Var {v:?})"), + Tm::Def(v) => write!(f, "(Def {v:?})"), + Tm::Mul(l, r) => write!(f, "(Mul {l} {r})"), + } + } +} + +#[derive(Debug, PartialEq, Eq)] +enum Tok { + Open, + Close, + Atom(String), + Str(String), +} + +fn tokenize(text: &str) -> Option> { + let mut out = Vec::new(); + let mut chars = text.chars().peekable(); + while let Some(&c) = chars.peek() { + match c { + '(' => { + chars.next(); + out.push(Tok::Open); + } + ')' => { + chars.next(); + out.push(Tok::Close); + } + c if c.is_whitespace() => { + chars.next(); + } + '"' => { + chars.next(); + let mut s = String::new(); + loop { + match chars.next()? { + '"' => break, + '\\' => s.push(chars.next()?), + ch => s.push(ch), + } + } + out.push(Tok::Str(s)); + } + _ => { + let mut s = String::new(); + while let Some(&ch) = chars.peek() { + if ch == '(' || ch == ')' || ch == '"' || ch.is_whitespace() { + break; + } + s.push(ch); + chars.next(); + } + out.push(Tok::Atom(s)); + } + } + } + Some(out) +} + +fn parse_tm(toks: &[Tok], pos: &mut usize) -> Option { + if toks.get(*pos)? != &Tok::Open { + return None; + } + *pos += 1; + let Tok::Atom(head) = toks.get(*pos)? else { + return None; + }; + *pos += 1; + let tm = match head.as_str() { + "Num" => { + let Tok::Atom(n) = toks.get(*pos)? else { + return None; + }; + *pos += 1; + Tm::Num(n.parse().ok()?) + } + "Var" | "Def" => { + let Tok::Str(s) = toks.get(*pos)? else { + return None; + }; + *pos += 1; + if head == "Var" { + Tm::Var(s.clone()) + } else { + Tm::Def(s.clone()) + } + } + "Mul" => { + let l = parse_tm(toks, pos)?; + let r = parse_tm(toks, pos)?; + Tm::Mul(Box::new(l), Box::new(r)) + } + _ => return None, + }; + if toks.get(*pos)? != &Tok::Close { + return None; + } + *pos += 1; + Some(tm) +} + +#[cfg(test)] +mod tests { + use super::*; + + /// FAILS IF: a rendered term stops round-tripping, or a malformed one is + /// accepted (trailing text, unknown head, unbalanced parens). + #[test] + fn parse_round_trips_and_rejects_malformed() { + let t = Tm::parse(r#"(Mul (Num -8) (Var "c"))"#).expect("parses"); + assert_eq!(t.to_string(), r#"(Mul (Num -8) (Var "c"))"#); + assert_eq!(t.size(), 3); + assert_eq!(t.foreign_vars("c"), Vec::::new()); + assert_eq!(t.foreign_vars("x"), vec!["c".to_string()]); + for bad in [ + "", + "(Num 8) (Num 9)", + "(Frob 1)", + "(Mul (Num 8))", + r#"(Var c)"#, + "(Num 8", + ] { + assert_eq!(Tm::parse(bad), None, "{bad:?}"); + } + } +} diff --git a/crates/egglog-r2il-probe/src/trace.rs b/crates/egglog-r2il-probe/src/trace.rs new file mode 100644 index 000000000..e5c87850e --- /dev/null +++ b/crates/egglog-r2il-probe/src/trace.rs @@ -0,0 +1,168 @@ +//! The logical traceroute: every hop from premises to verdict, one line each. +//! +//! Hops, in order: Premises, Laws, Saturation, Extracted, Proof, R2IL, Value, +//! Oracle, Verdict. Each line renders as `N. Label: detail`. + +use std::fmt; + +use crate::lower::{Step, lower_steps, run_steps}; +use crate::{Arith, LowerRefusal, Problem, Saturation, compile, oracle}; + +/// The hop labels, in order. +pub const HOPS: [&str; 9] = [ + "Premises", + "Laws", + "Saturation", + "Extracted", + "Proof", + "R2IL", + "Value", + "Oracle", + "Verdict", +]; + +/// How the lowered value and the oracle relate. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Verdict { + /// Both answered and the values are equal. + Agree, + /// Both answered and the values differ, or the lowering answered where + /// the oracle has no answer. + Disagree, + /// Neither produced an `i64` answer, for a reason the other side shares: + /// no connecting premise (both refuse), or an overflow while the oracle's + /// exact value lies outside `i64`. + BothRefuse, + /// The oracle answers (in range) and the lowering refuses. + OracleOnly, +} + +/// One hop. +#[derive(Debug, Clone)] +pub struct Hop { + /// Label from [`HOPS`]. + pub label: &'static str, + /// What was observed there. + pub detail: String, +} + +/// The whole route. +#[derive(Debug, Clone)] +pub struct Trace { + /// Hops in order. + pub hops: Vec, + /// The final comparison. + pub verdict: Verdict, +} + +impl fmt::Display for Trace { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + for (i, h) in self.hops.iter().enumerate() { + writeln!(f, "{}. {}: {}", i + 1, h.label, h.detail)?; + } + Ok(()) + } +} + +/// Compiles, lowers, runs with `target_var = c`, consults the oracle. +pub fn traceroute(p: &Problem, arith: Arith, fuel: usize, c: i64) -> Trace { + let compiled = compile(p, arith, fuel); + let mut hops = Vec::with_capacity(HOPS.len()); + let mut push = |label: &'static str, detail: String| hops.push(Hop { label, detail }); + + push( + "Premises", + p.premises + .iter() + .map(|e| format!("{} = {}*{}", e.lhs, e.coeff, e.rhs)) + .collect::>() + .join("; ") + + &format!(" | goal {} in {}", p.goal, p.target_var), + ); + let admitted: Vec = compiled + .admitted + .iter() + .map(|r| format!("{:?}@{:?}", r.law, r.domain)) + .collect(); + let refused: Vec = compiled + .refused + .iter() + .map(|(l, why)| format!("{l:?}: {why:?}")) + .collect(); + push( + "Laws", + format!( + "admitted [{}] refused [{}]", + admitted.join(", "), + refused.join(", ") + ), + ); + push( + "Saturation", + match (&compiled.error, compiled.saturation) { + (Some(e), _) => format!("egglog error: {e}"), + (None, Saturation::Saturated { iterations }) => { + format!("saturated after {iterations} step(s)") + } + (None, Saturation::Incomplete { fuel }) => { + format!("INCOMPLETE: fuel {fuel} exhausted") + } + }, + ); + push( + "Extracted", + format!("{} (closed: {})", compiled.extracted, compiled.closed), + ); + push( + "Proof", + match &compiled.proof { + Some(p) => format!("present, {} bytes", p.len()), + None => "absent".to_string(), + }, + ); + + let steps = lower_steps(&compiled); + push( + "R2IL", + match &steps { + Ok(s) => s.iter().map(Step::mnemonic).collect::>().join(", "), + Err(e) => format!("refused: {e:?}"), + }, + ); + let value: Result = match &steps { + Ok(s) => run_steps(s, compiled.target_var, &[(p.target_var, c)]), + Err(e) => Err(e.clone()), + }; + push( + "Value", + match &value { + Ok(v) => format!("{v} (at {} = {c})", p.target_var), + Err(e) => format!("refused: {e:?}"), + }, + ); + let truth = oracle::solve(p, c); + push( + "Oracle", + match truth { + Some(v) => format!("{v} (i128)"), + None => "none".to_string(), + }, + ); + + let verdict = match (&value, truth) { + (Ok(v), Some(o)) => { + if i128::from(*v) == o { + Verdict::Agree + } else { + Verdict::Disagree + } + } + (Ok(_), None) => Verdict::Disagree, + (Err(_), None) => Verdict::BothRefuse, + (Err(LowerRefusal::Overflow), Some(o)) if i64::try_from(o).is_err() => Verdict::BothRefuse, + (Err(_), Some(_)) => Verdict::OracleOnly, + }; + push("Verdict", format!("{verdict:?}")); + + Trace { hops, verdict } +} diff --git a/crates/egglog-r2il-probe/tests/e1.rs b/crates/egglog-r2il-probe/tests/e1.rs new file mode 100644 index 000000000..876d30a2e --- /dev/null +++ b/crates/egglog-r2il-probe/tests/e1.rs @@ -0,0 +1,250 @@ +//! Stage B, E1 end to end: premises -> egglog (cold, proofs mode) -> R2IL +//! `INT_MULT` -> value, against an independent i128 oracle. + +use egglog_r2il_probe::trace::{HOPS, Verdict, traceroute}; +use egglog_r2il_probe::{ + Arith, Compiled, Eq, LawId, LawRefusal, LowerRefusal, Problem, Saturation, Step, chain_problem, + compile, e1_problem, lower_and_run, lower_steps, oracle, try_prove, +}; + +/// The c values every agreement test sweeps: zero, units, ordinary, and both +/// edges where 8*c still fits `i64`. +fn c_values() -> Vec { + vec![0, 1, -1, 7, -123_456, i64::MAX / 8, i64::MIN / 8] +} + +fn ok(c: &Compiled) { + assert!(c.error.is_none(), "egglog error: {:?}", c.error); +} + +fn mults(steps: &[Step]) -> usize { + steps.iter().filter(|s| matches!(s, Step::IntMult)).count() +} + +/// FAILS IF: Exact stops saturating within fuel 8, stops extracting +/// `(Mul (Num 8) (Var "c"))`, loses the proof, or the extraction is not closed. +#[test] +fn exact_e1_extracts_8c_with_a_checked_proof() { + let c = compile(&e1_problem(), Arith::Exact, 8); + ok(&c); + assert!( + matches!(c.saturation, Saturation::Saturated { .. }), + "{:?}", + c.saturation + ); + assert_eq!(c.extracted, r#"(Mul (Num 8) (Var "c"))"#); + let proof = c.proof.as_ref().expect("a proof for the extracted term"); + assert!(!proof.is_empty()); + assert!(c.closed); + assert!(c.refused.is_empty(), "{:?}", c.refused); + assert_eq!(c.admitted.len(), 2); +} + +/// FAILS IF: Exact lowers to anything other than ONE `INT_MULT`, or any value +/// disagrees with the i128 oracle over the original premises. +#[test] +fn exact_e1_lowers_to_one_int_mult_and_agrees_with_oracle() { + let p = e1_problem(); + let c = compile(&p, Arith::Exact, 8); + ok(&c); + let steps = lower_steps(&c).expect("lowerable"); + assert_eq!(mults(&steps), 1, "{steps:?}"); + for v in c_values() { + let got = lower_and_run(&c, &[("c", v)]).expect("in range"); + let want = oracle::solve(&p, v).expect("oracle answers"); + assert_eq!(i128::from(got), want, "c = {v}"); + } +} + +/// FAILS IF: the Checked domain admits re-association or folding (the two +/// must be refused with the Checked reasons), or still reaches `(Num 8)`, or +/// lowers to other than THREE `INT_MULT`s, or disagrees with the oracle. +/// Two-sided with the Exact test above: the domain changes the program. +#[test] +fn checked_domain_refuses_reassociation_and_lowers_three_mults() { + let p = e1_problem(); + let c = compile(&p, Arith::Checked, 8); + ok(&c); + assert!(c.admitted.is_empty(), "{:?}", c.admitted); + assert!( + c.refused + .contains(&(LawId::MulAssoc, LawRefusal::NotAssociative(Arith::Checked))) + ); + assert!( + c.refused + .contains(&(LawId::ConstFold, LawRefusal::NotExactFold(Arith::Checked))) + ); + assert!(!c.extracted.contains("(Num 8)"), "{}", c.extracted); + assert!(c.closed, "{}", c.extracted); + let steps = lower_steps(&c).expect("lowerable"); + assert_eq!(mults(&steps), 3, "{steps:?}"); + for v in c_values() { + let got = lower_and_run(&c, &[("c", v)]).expect("in range"); + let want = oracle::solve(&p, v).expect("oracle answers"); + assert_eq!(i128::from(got), want, "c = {v}"); + } +} + +/// FAILS IF: dropping `b = 2*c` still yields a closed answer, a variant +/// mentions `(Num 8)`, lowering with only `c` stops refusing with an unbound defined variable, +/// the oracle invents an answer, the verdict is not BothRefuse, or egglog +/// proves a claim the premises do not support. +#[test] +fn missing_premise_refuses() { + let p = Problem { + premises: vec![ + Eq { + lhs: "a", + coeff: 2, + rhs: "b", + }, + Eq { + lhs: "z", + coeff: 2, + rhs: "a", + }, + ], + goal: "z", + target_var: "c", + }; + let c = compile(&p, Arith::Exact, 8); + ok(&c); + assert!( + c.variants.iter().all(|v| !v.contains("(Num 8)")), + "{:?}", + c.variants + ); + assert!(!c.closed, "{}", c.extracted); + // Which defined name the answer keeps is egglog's tie-break: with + // `b = 2*c` gone, `(Mul (Num 2) (Def "a"))` and `(Mul (Num 4) (Def "b"))` + // both cost 1002. Either way the refusal must name a defined variable + // the target cannot reach, never the target and never a value. + match lower_and_run(&c, &[("c", 7)]) { + Err(LowerRefusal::UnboundVar(v)) => { + assert!(v == "a" || v == "b", "unexpected unbound {v}"); + } + other => panic!("expected UnboundVar, got {other:?} for {}", c.extracted), + } + assert_eq!(oracle::solve(&p, 7), None); + assert_eq!( + traceroute(&p, Arith::Exact, 8, 7).verdict, + Verdict::BothRefuse + ); + + let claim = try_prove(&p, Arith::Exact, 8, r#"(Mul (Num 8) (Var "c"))"#); + assert!( + claim.is_err(), + "egglog proved an unsupported claim: {claim:?}" + ); + // Paired half: the same call DOES prove a supported claim, so the Err + // above is the premises' doing and not a broken `try_prove`. + let supported = try_prove(&p, Arith::Exact, 8, r#"(Mul (Num 4) (Def "b"))"#); + assert!(supported.is_ok(), "{supported:?}"); +} + +/// FAILS IF: an overflowing c is answered in either domain instead of +/// `Overflow`, the oracle value stops lying outside `i64` for them, or the +/// boundary c = i64::MAX/8 stops succeeding (two-sided). +#[test] +fn overflow_counterexamples_refuse_in_both_domains() { + let p = e1_problem(); + let exact = compile(&p, Arith::Exact, 8); + let checked = compile(&p, Arith::Checked, 8); + ok(&exact); + ok(&checked); + for v in [i64::MAX / 8 + 1, i64::MIN / 8 - 1, i64::MAX] { + let want = oracle::solve(&p, v).expect("oracle answers in i128"); + assert!(i64::try_from(want).is_err(), "c = {v}: {want} fits i64"); + for c in [&exact, &checked] { + assert_eq!( + lower_and_run(c, &[("c", v)]), + Err(LowerRefusal::Overflow), + "c = {v} under {:?}", + c.arith + ); + } + } + let edge = i64::MAX / 8; + for c in [&exact, &checked] { + assert_eq!( + lower_and_run(c, &[("c", edge)]), + Ok(edge * 8), + "{:?}", + c.arith + ); + } +} + +/// FAILS IF: Wrapping stops refusing ConstFold, stops admitting MulAssoc, or +/// a wrapping term is run on R2IL's checked arithmetic instead of refused. +#[test] +fn wrapping_term_is_not_lowered() { + let c = compile(&e1_problem(), Arith::Wrapping, 8); + ok(&c); + assert!( + c.refused + .contains(&(LawId::ConstFold, LawRefusal::NotExactFold(Arith::Wrapping))) + ); + assert!(c.admitted.iter().any(|r| r.law == LawId::MulAssoc)); + assert!(!c.admitted.iter().any(|r| r.law == LawId::ConstFold)); + assert!(matches!( + lower_and_run(&c, &[("c", 7)]), + Err(LowerRefusal::NotLowerable(_)) + )); +} + +/// FAILS IF: two fresh e-graphs disagree on the extraction, the variant list, +/// or the lowered call list. +#[test] +fn extraction_is_deterministic() { + let p = e1_problem(); + let runs: Vec = (0..3).map(|_| compile(&p, Arith::Exact, 8)).collect(); + for r in &runs { + ok(r); + } + let steps: Vec> = runs + .iter() + .map(|r| lower_steps(r).expect("lowerable")) + .collect(); + for i in 1..3 { + assert_eq!(runs[0].extracted, runs[i].extracted); + assert_eq!(runs[0].variants, runs[i].variants); + assert_eq!(steps[0], steps[i]); + } +} + +/// FAILS IF: running out of fuel is reported as saturation, or a long chain +/// stops saturating given room (two-sided: Incomplete at fuel 1, Saturated at +/// fuel 16). Uses the six-link chain so one step cannot finish. +#[test] +fn bounded_fuel_reports_incomplete() { + let p = chain_problem(); + let tight = compile(&p, Arith::Exact, 1); + ok(&tight); + assert_eq!(tight.saturation, Saturation::Incomplete { fuel: 1 }); + let roomy = compile(&p, Arith::Exact, 16); + ok(&roomy); + assert!( + matches!(roomy.saturation, Saturation::Saturated { .. }), + "{:?}", + roomy.saturation + ); + assert_eq!(roomy.extracted, r#"(Mul (Num 64) (Var "p6"))"#); +} + +/// FAILS IF: the traceroute drops, renames or reorders a hop. +#[test] +fn traceroute_names_every_hop() { + let t = traceroute(&e1_problem(), Arith::Exact, 8, 7); + let text = t.to_string(); + let lines: Vec<&str> = text.lines().collect(); + assert_eq!(lines.len(), HOPS.len(), "{text}"); + for (i, label) in HOPS.iter().enumerate() { + assert!( + lines[i].starts_with(&format!("{}. {}:", i + 1, label)), + "line {i}: {}", + lines[i] + ); + } + assert_eq!(t.verdict, Verdict::Agree); +} From 99db186c0485789911c3a00a0ed2736beb11e99e Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 22 Oct 2026 06:25:27 +0000 Subject: [PATCH 6/6] board: Stage B E1 probe entry, AGENT_LOG, entries index Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg --- .claude/board/AGENT_LOG.md | 5 ++ .../2026-10-22-math-compiler-stage-b-e1.md | 48 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 3 files changed, 55 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md diff --git a/.claude/board/AGENT_LOG.md b/.claude/board/AGENT_LOG.md index b6476b361..3e3ca3091 100644 --- a/.claude/board/AGENT_LOG.md +++ b/.claude/board/AGENT_LOG.md @@ -1,3 +1,8 @@ +## 2026-10-22 — Stage B E1 probe (Opus spec, Sonnet draft) + +- One Sonnet drafter from a written spec (no cargo). The main thread replaced its hand-written variable expansion (a second rewriter outside egglog) with an egglog constructor cost, fixed a test that pinned egglog's cost tie-break, withheld the out-of-fold egglog timing pending an operator ruling, compiled, and ran 6 disable runs (all red). +- Result: `entries/2026-10-22-math-compiler-stage-b-e1.md`. Written by the orchestrating main thread only. + ## 2026-10-22 — D-MPS-9 `query_multi` oracle (Haiku map, Opus spec, Sonnet draft) - Two Haiku `substrate-mapper` runs: MORK `space.rs`/`expr` (PARTIAL: the read stopped at line 1076/1094; `query_multi`, `Bindings`, `ExprEnv` read on the main thread) and the probe boundary plus fixtures (complete). diff --git a/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md b/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md new file mode 100644 index 000000000..935e7e483 --- /dev/null +++ b/.claude/board/entries/2026-10-22-math-compiler-stage-b-e1.md @@ -0,0 +1,48 @@ +# 2026-10-22 — Proof-carrying math compiler: Stage B, E1 end to end (probe-local) + +**Status:** MEASURED (lab). Crate `crates/egglog-r2il-probe/`, own workspace root. egglog = AdaWorldAPI/egglog `main` (public API only, unmodified). Coordination: EXO-50 /043. Continues `entries/2026-10-22-math-compiler-gap-matrix.md`; falsifier E1 from `.arxiv/2304.04332_egglog_equality_saturation_datalog_excerpt.md`; D-RFT-2 owns the plan. + +**Shape (operator decision):** E1 is exact-integer symbolic substitution, `a = 2b, b = 2c, z = 2a ⇒ z = 8c`. It is not a population measure, so there is no SUM fold, no lane and no mask, and `contract::Measure` is unchanged. This supersedes the Stage A seam's "over a SUM fold" step. + +| Hop | What runs | Owner | +|---|---|---| +| law admission | two probe laws, `MulAssoc` and `ConstFold`; the rule id carries the contract's `set_rules::Arith` domain. Exact admits both; Wrapping admits only `MulAssoc`; Checked and Ieee admit neither | probe (`laws.rs`) | +| saturation | egglog proofs mode, `(run arith 1)` stepped up to `fuel`, `Saturated` / `Incomplete` read from the step's own iteration report | egglog, cold | +| extraction | egglog's own: `prove-variants` on the goal, cheapest first under the default AST-size cost, non-target variables as `(Def String :cost 1000)`; the answer is the cheapest variant other than the goal's own name | egglog | +| proof | the variant's proof from `prove-variants`, checked by egglog's `check_proof` before and after simplification (`src/proofs/proof_extraction.rs:126-139`) | egglog | +| lowering | straight-line R2IL scalar calls (`push`, `INT_MULT`) through `FoldDialect` over empty planes, the `procs.rs` pattern; no new opcode | existing R2IL | +| oracle | i128 substitution over the original premises, no shared code | probe (`oracle.rs`) | + +**Results (13 tests, release):** +- Exact: `(Mul (Num 8) (Var "c"))`, one `INT_MULT`, agreeing with the oracle for c ∈ {0, ±1, 7, -123456, i64::MAX/8, i64::MIN/8}. +- Checked: both laws are refused and the program is three `INT_MULT`s. The domain changes the program. +- Missing premise (`b = 2c` dropped): + - no variant contains `(Num 8)` and the result is not closed; + - lowering refuses `UnboundVar` (`a` or `b`; which one is egglog's cost tie-break, both cost 1002); + - the oracle returns None; + - egglog's `prove` of `z = 8c` fails, while the paired claim `z = 4·b` proves. +- Overflow counterexamples (c = i64::MAX/8 + 1, i64::MIN/8 − 1, i64::MAX): `Overflow` in both Exact and Checked, and the oracle's value lies outside i64. The boundary i64::MAX/8 passes. +- Wrapping: lowering refuses, because R2IL scalar arithmetic is checked, not wrapping. +- Determinism: three fresh e-graphs give an identical extraction, variant list and call list. +- Bounded fuel: the six-link chain is `Incomplete` at fuel 1 and `Saturated` at fuel 16. +- Traceroute: the hops are Premises, Laws, Saturation, Extracted, Proof, R2IL, Value, Oracle, Verdict. + +**Disable runs (6, all red):** +- Checked admits `MulAssoc`; +- `Def` without its cost; +- Wrapping is lowered; +- `Overflow` is mapped away; +- the goal's own name is accepted as the answer; +- every step is read as saturated. + +**Cost:** encode 2 µs; lower + execute 5 µs (median of 5, release). The egglog phase (saturation + `prove-variants`) is timed in `Compiled::timings.egglog` but not printed or reported here. It is above the workspace's microsecond budget, and whether cold, out-of-fold compile costs may be reported is an open operator decision (CLAUDE.md "no millisecond results"). + +**Corrections to Stage A:** +- "Independent proof check MISSING" overstated the gap. egglog already checks every proof it returns. What is missing is a check callable from outside egglog on a proof object. The i128 oracle covers answer correctness independently. +- No egglog change was needed. + +OPEN: +- the ruling on reporting cold-compile cost; +- E2–E5 beyond what E1 exercises; +- a lowering target for wrapping arithmetic (none exists; by design?); +- `Measure::Scale` stays gated on a real population-measure consumer in a separate PR. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 0de90d968..1f634299c 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -427 entries, 2026-08-06 .. 2026-10-22. +428 entries, 2026-08-06 .. 2026-10-22. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-22 | `math-compiler-stage-b-e1` | | [2026-10-22-math-compiler-stage-b-e1.md](2026-10-22-math-compiler-stage-b-e1.md) | | 2026-10-22 | `math-compiler-gap-matrix` | | [2026-10-22-math-compiler-gap-matrix.md](2026-10-22-math-compiler-gap-matrix.md) | | 2026-10-22 | `D-MPS-9` | | [2026-10-22-d-mps-9-mork-oracle.md](2026-10-22-d-mps-9-mork-oracle.md) | | 2026-10-21 | `zero-copy-join-index-map` | | [2026-10-21-zero-copy-join-index-map.md](2026-10-21-zero-copy-join-index-map.md) |