From 8e447bec494d8458e69d3407e51c4abbc7c70a76 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:07:11 +0000 Subject: [PATCH 01/11] xlog-relcomp-probe: XLOG's compiled transitive closure, evaluated semi-naively on DR64 admit_closure accepts exactly one linear recursive SCC (base Scan edge, step ChainJoin path.1 = edge.0 projecting 0 and 3, fallback agreeing) and refuses non-linear and mutual recursion. closure binds edge under the sealed frame and runs semi-naive rounds over the existing relcomp::compose. support and affected read derivations back from the closure as masks on demand. Tests: BFS and a fixpoint walk of XLOG's own plan as references, a 200-case differential, cycle termination, both diamond alternatives in support, the affected set of one fact, refusals, and a stale frame. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/src/lib.rs | 1 + crates/xlog-relcomp-probe/src/recursive.rs | 239 ++++++++++++ crates/xlog-relcomp-probe/tests/recursive.rs | 369 +++++++++++++++++++ 3 files changed, 609 insertions(+) create mode 100644 crates/xlog-relcomp-probe/src/recursive.rs create mode 100644 crates/xlog-relcomp-probe/tests/recursive.rs diff --git a/crates/xlog-relcomp-probe/src/lib.rs b/crates/xlog-relcomp-probe/src/lib.rs index 681329955..f82e2964d 100644 --- a/crates/xlog-relcomp-probe/src/lib.rs +++ b/crates/xlog-relcomp-probe/src/lib.rs @@ -39,6 +39,7 @@ use std::collections::BTreeMap; pub mod native; +pub mod recursive; use dr_math_binding_probe::relcomp::{ComposeRefusal, Rows, Work, compose}; use dr_math_binding_probe::{ diff --git a/crates/xlog-relcomp-probe/src/recursive.rs b/crates/xlog-relcomp-probe/src/recursive.rs new file mode 100644 index 000000000..c5e82c6d9 --- /dev/null +++ b/crates/xlog-relcomp-probe/src/recursive.rs @@ -0,0 +1,239 @@ +//! Recursive reachability: XLOG's compiled recursive SCC, evaluated on the +//! DR64 register with the existing compose kernel. +//! +//! XLOG compiles +//! +//! ```text +//! path(X, Y) :- edge(X, Y). +//! path(X, Y) :- path(X, Z), edge(Z, Y). +//! ``` +//! +//! into one recursive SCC with two rule bodies: `Scan edge`, and a +//! `ChainJoin` of `Scan path` with `Scan edge` on `path.1 = edge.0`, +//! projecting columns 0 and 3, whose `fallback` is the same join written +//! out. [`admit_closure`] accepts exactly that shape and refuses everything +//! else. [`closure`] evaluates it semi-naively (each round composes only the +//! newly derived pairs with `edge`), which is the evaluation order XLOG's own +//! runtime uses for a recursive SCC. +//! +//! Derivations are never stored. [`support`] and [`affected`] read them back +//! from the closure as masks when asked: the base facts an answer depends on, +//! and the answers a base fact feeds. + +use std::collections::HashMap; + +use dr_math_binding_probe::relcomp::{Chain, Rows, Work, compose}; +use dr_math_binding_probe::{FrameStore, Guards, MethodSignature}; +use xlog_core::RelId; +use xlog_ir::{ExecutionPlan, JoinType, ProjectExpr, RirNode}; + +use crate::{EvalRefusal, LowerRefusal, SLOTS, bind}; + +/// The admitted recursive SCC: `head` is the closure of `edge`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct ClosureQuery { + pub head: String, + pub edge: RelId, +} + +/// Admit XLOG's compiled plan when it is exactly one linear transitive +/// closure over one base relation, or say why not. +pub fn admit_closure( + plan: &ExecutionPlan, + rel_ids: &HashMap, +) -> Result { + let recursive: Vec<_> = plan.sccs.iter().filter(|s| s.is_recursive).collect(); + let [scc] = recursive.as_slice() else { + return Err(LowerRefusal::UnsupportedNode("recursive SCC count")); + }; + let [head] = scc.predicates.as_slice() else { + return Err(LowerRefusal::UnsupportedNode("mutual recursion")); + }; + let head_id = *rel_ids + .get(head) + .ok_or(LowerRefusal::UnsupportedNode("head id"))?; + let rules: Vec<&RirNode> = plan + .rules_by_scc + .iter() + .flatten() + .filter(|r| &r.head == head) + .map(|r| &r.body) + .collect(); + let mut base = None; + let mut step = None; + for body in rules { + match body { + RirNode::Scan { rel } if *rel != head_id && base.is_none() => base = Some(*rel), + _ if step.is_none() => step = Some(step_edge(body, head_id)?), + _ => return Err(LowerRefusal::UnsupportedNode("extra rule in the SCC")), + } + } + match (base, step) { + (Some(b), Some(s)) if b == s => Ok(ClosureQuery { + head: head.clone(), + edge: b, + }), + (Some(_), Some(_)) => Err(LowerRefusal::UnsupportedNode("step over another relation")), + _ => Err(LowerRefusal::UnsupportedNode("missing base or step rule")), + } +} + +/// The relation a step `head(X, Y) :- head(X, Z), edge(Z, Y)` extends by. +fn step_edge(body: &RirNode, head: RelId) -> Result { + let joined = + |left: &RirNode, right: &RirNode, lk: usize, rk: usize, cols: &[ProjectExpr]| match ( + left, right, + ) { + (RirNode::Scan { rel: l }, RirNode::Scan { rel: r }) if *l == head && *r != head => { + if (lk, rk) != (1, 0) { + return Err(LowerRefusal::NeedsInverse { + left_keys: vec![lk], + right_keys: vec![rk], + }); + } + if !matches!(cols, [ProjectExpr::Column(0), ProjectExpr::Column(3)]) { + return Err(LowerRefusal::UnsupportedProjection); + } + Ok(*r) + } + _ => Err(LowerRefusal::UnsupportedNode( + "non-linear or reordered step", + )), + }; + let plain = |node: &RirNode| match node { + RirNode::Project { input, columns } => match input.as_ref() { + RirNode::Join { + left, + right, + left_keys, + right_keys, + join_type, + } => { + if *join_type != JoinType::Inner { + return Err(LowerRefusal::UnsupportedJoin(join_type.clone())); + } + let ([lk], [rk]) = (left_keys.as_slice(), right_keys.as_slice()) else { + return Err(LowerRefusal::NeedsInverse { + left_keys: left_keys.clone(), + right_keys: right_keys.clone(), + }); + }; + joined(left, right, *lk, *rk, columns) + } + _ => Err(LowerRefusal::UnsupportedNode("projected non-join")), + }, + _ => Err(LowerRefusal::UnsupportedNode("step shape")), + }; + match body { + RirNode::ChainJoin { + left, + right, + left_key, + right_key, + output_columns, + fallback, + } => { + let fast = joined(left, right, *left_key, *right_key, output_columns)?; + if plain(fallback)? != fast { + return Err(LowerRefusal::ChainJoinDisagrees); + } + Ok(fast) + } + other => plain(other), + } +} + +/// The closure and the work done to reach it. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Closure { + pub rows: Rows, + /// Rounds until no new pair appeared (the last round derives nothing). + pub rounds: usize, + /// Row ORs done by `compose`. + pub work: Work, +} + +/// Bind `edge` under the sealed frame, type `edge ∘ edge`, then evaluate the +/// closure semi-naively. `valid` masks the assigned slots of the one axis. +pub fn closure( + store: &FrameStore, + guards: &Guards, + now: (dr_math_binding_probe::Focus, dr_math_binding_probe::Scope), + sig: MethodSignature, + edge: &Rows, + valid: u64, +) -> Result { + let e = bind(store, guards, now, sig, edge)?; + // The existing typing: the row axis of `edge` is its column axis. + Chain::new(store, vec![e.clone(), e.clone()]).map_err(EvalRefusal::Chain)?; + let mut path = [0u64; SLOTS]; + for (p, w) in path.iter_mut().zip(e.rows) { + *p = w & valid; + } + let mut delta = path; + let mut work = Work::default(); + let mut rounds = 0; + loop { + rounds += 1; + let next = compose(&delta, e.rows, &mut work); + let mut any = false; + for i in 0..SLOTS { + delta[i] = next[i] & valid & !path[i]; + path[i] |= delta[i]; + any |= delta[i] != 0; + } + if !any { + return Ok(Closure { + rows: path, + rounds, + work, + }); + } + } +} + +/// `R* = I ∪ R` over the assigned slots. +fn reflexive(path: &Rows, valid: u64) -> Rows { + let mut out = *path; + for (i, w) in out.iter_mut().enumerate() { + if valid >> i & 1 == 1 { + *w |= 1 << i; + } + } + out +} + +/// The `edge` facts a derivation of `path(x, y)` can use: `(u, v)` with +/// `u` reachable from `x` (or `u = x`) and `y` reachable from `v` (or +/// `v = y`). Empty when `path(x, y)` does not hold. Computed from the closure +/// on demand; no derivation is stored. +pub fn support(edge: &Rows, path: &Rows, valid: u64, x: usize, y: usize) -> Rows { + let mut out = [0u64; SLOTS]; + if path[x] >> y & 1 == 0 { + return out; + } + let star = reflexive(path, valid); + // Columns v whose closure reaches y: column y of R*, read row by row. + let to_y: u64 = (0..SLOTS) + .filter(|&v| star[v] >> y & 1 == 1) + .fold(0, |m, v| m | 1 << v); + for u in 0..SLOTS { + if star[x] >> u & 1 == 1 { + out[u] = edge[u] & to_y; + } + } + out +} + +/// The `path` answers a base fact `edge(u, v)` feeds: `(a, b)` with `u` +/// reachable from `a` (or `a = u`) and `b` reachable from `v` (or `b = v`). +pub fn affected(path: &Rows, valid: u64, u: usize, v: usize) -> Rows { + let star = reflexive(path, valid); + let mut out = [0u64; SLOTS]; + for a in 0..SLOTS { + if star[a] >> u & 1 == 1 { + out[a] = star[v]; + } + } + out +} diff --git a/crates/xlog-relcomp-probe/tests/recursive.rs b/crates/xlog-relcomp-probe/tests/recursive.rs new file mode 100644 index 000000000..808a16265 --- /dev/null +++ b/crates/xlog-relcomp-probe/tests/recursive.rs @@ -0,0 +1,369 @@ +//! Recursive reachability compiled by XLOG, evaluated on the DR64 register. +//! +//! Two references share no code with the evaluation: +//! 1. breadth-first search over the source tuples; +//! 2. a naive fixpoint walk of XLOG's own compiled rule bodies over tuples. + +use std::collections::{BTreeSet, HashMap}; + +use dr_math_binding_probe::{ + Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Refusal, Scope, +}; +use xlog_core::RelId; +use xlog_ir::{ExecutionPlan, JoinType, ProjectExpr, RirNode}; +use xlog_logic::{Compiler, parse_program}; +use xlog_relcomp_probe::recursive::{admit_closure, affected, closure, support}; +use xlog_relcomp_probe::{AddressMap, EvalRefusal, LowerRefusal, SLOTS, facts, register}; + +const N: Axis = Axis { + class: 30, + kind: AxisKind::Identity, +}; +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; + +fn sig() -> MethodSignature { + MethodSignature::presence(40, 0, N, N) +} +fn store() -> FrameStore { + FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: 1, + }) +} +fn guards(st: &FrameStore) -> Guards { + Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + } +} + +const RULES: &str = "pred edge(u32, u32). +pred path(u32, u32). +path(X, Y) :- edge(X, Y). +path(X, Y) :- path(X, Z), edge(Z, Y). +?- path(X, Y). +"; + +fn program(edges: &[(u32, u32)], rules: &str) -> String { + let mut s = String::new(); + for (a, b) in edges { + s.push_str(&format!("edge({a}, {b}). ")); + } + format!("{rules}\n{s}\n") +} + +fn compile(src: &str) -> (ExecutionPlan, HashMap) { + let mut c = Compiler::new(); + let plan = c.compile(src).expect("compile"); + (plan, c.rel_ids().clone()) +} + +/// Reference 1: BFS from every node over the tuples. +fn bfs(edges: &[(u32, u32)]) -> BTreeSet<(u32, u32)> { + let mut out = BTreeSet::new(); + let nodes: BTreeSet = edges.iter().flat_map(|&(a, b)| [a, b]).collect(); + for &s in &nodes { + let mut seen = BTreeSet::new(); + let mut frontier = vec![s]; + while let Some(u) = frontier.pop() { + for &(a, b) in edges { + if a == u && seen.insert(b) { + frontier.push(b); + } + } + } + out.extend(seen.into_iter().map(|t| (s, t))); + } + out +} + +/// Reference 2: XLOG's compiled bodies applied naively until nothing changes. +fn walk_plan( + plan: &ExecutionPlan, + rel: &HashMap, + edges: &[(u32, u32)], +) -> BTreeSet<(u32, u32)> { + let mut db: HashMap>> = HashMap::new(); + db.insert( + rel["edge"], + edges.iter().map(|&(a, b)| vec![a, b]).collect(), + ); + db.insert(rel["path"], BTreeSet::new()); + loop { + let mut grew = false; + for r in plan + .rules_by_scc + .iter() + .flatten() + .filter(|r| r.head == "path") + { + let derived = eval(&r.body, &db); + let tgt = db.get_mut(&rel["path"]).unwrap(); + for t in derived { + grew |= tgt.insert(t); + } + } + if !grew { + break; + } + } + db[&rel["path"]].iter().map(|t| (t[0], t[1])).collect() +} + +fn eval(node: &RirNode, db: &HashMap>>) -> BTreeSet> { + match node { + RirNode::Scan { rel } => db[rel].clone(), + RirNode::ChainJoin { + left, + right, + left_key, + right_key, + output_columns, + .. + } => project( + &join( + &eval(left, db), + &eval(right, db), + &[*left_key], + &[*right_key], + ), + output_columns, + ), + RirNode::Project { input, columns } => match input.as_ref() { + RirNode::Join { + left, + right, + left_keys, + right_keys, + join_type: JoinType::Inner, + } => project( + &join(&eval(left, db), &eval(right, db), left_keys, right_keys), + columns, + ), + _ => panic!("oracle covers joins only"), + }, + other => panic!("oracle does not cover {other:?}"), + } +} + +fn join( + l: &BTreeSet>, + r: &BTreeSet>, + lk: &[usize], + rk: &[usize], +) -> BTreeSet> { + let mut out = BTreeSet::new(); + for a in l { + for b in r { + if lk.iter().zip(rk).all(|(i, j)| a[*i] == b[*j]) { + out.insert(a.iter().chain(b).copied().collect()); + } + } + } + out +} + +fn project(rows: &BTreeSet>, cols: &[ProjectExpr]) -> BTreeSet> { + rows.iter() + .map(|t| { + cols.iter() + .map(|c| match c { + ProjectExpr::Column(i) => t[*i], + ProjectExpr::Computed(..) => panic!("columns only"), + }) + .collect() + }) + .collect() +} + +struct Run { + map: AddressMap, + edge: [u64; SLOTS], + path: [u64; SLOTS], + rounds: usize, +} + +fn run(edges: &[(u32, u32)]) -> Run { + let src = program(edges, RULES); + let (plan, rel) = compile(&src); + let q = admit_closure(&plan, &rel).expect("admitted"); + assert_eq!(q.head, "path"); + let tuples = facts(&parse_program(&src).unwrap(), "edge").unwrap(); + let map = AddressMap::new(N, tuples.iter().flat_map(|&(a, b)| [a, b])).unwrap(); + let edge = register(&tuples, &map, &map).unwrap(); + let st = store(); + let c = closure(&st, &guards(&st), (FOCUS, SCOPE), sig(), &edge, map.valid()).unwrap(); + Run { + map, + edge, + path: c.rows, + rounds: c.rounds, + } +} + +fn pairs(r: &Run) -> BTreeSet<(u32, u32)> { + let mut out = BTreeSet::new(); + for (i, &w) in r.path.iter().enumerate().take(r.map.len()) { + let from = r.map.ids(1 << i)[0]; + for to in r.map.ids(w) { + out.insert((from, to)); + } + } + out +} + +const DIAMOND: &[(u32, u32)] = &[(1, 2), (1, 3), (2, 4), (3, 4), (4, 5)]; +const CYCLE: &[(u32, u32)] = &[(1, 2), (2, 3), (3, 1), (3, 4)]; + +#[test] +fn xlog_compiles_reachability_to_one_admitted_recursive_scc() { + let (plan, rel) = compile(&program(DIAMOND, RULES)); + assert_eq!(plan.sccs.iter().filter(|s| s.is_recursive).count(), 1); + let q = admit_closure(&plan, &rel).unwrap(); + assert_eq!(q.edge, rel["edge"]); +} + +#[test] +fn closure_matches_bfs_and_a_walk_of_xlogs_own_plan() { + for edges in [DIAMOND, CYCLE] { + let r = run(edges); + let src = program(edges, RULES); + let (plan, rel) = compile(&src); + assert_eq!(pairs(&r), bfs(edges), "{edges:?}"); + assert_eq!(pairs(&r), walk_plan(&plan, &rel, edges), "{edges:?}"); + } +} + +#[test] +fn deterministic_differential_against_bfs() { + let mut s = 0x9E37_79B9_7F4A_7C15u64; + let mut next = || { + s = s + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + (s >> 33) as u32 + }; + for case in 0..200 { + let n = 2 + next() % 40; + let m = next() % (3 * n); + let edges: Vec<(u32, u32)> = (0..m).map(|_| (next() % n, next() % n)).collect(); + let mut dedup = Vec::new(); + for e in edges { + if !dedup.contains(&e) { + dedup.push(e); + } + } + if dedup.is_empty() { + continue; + } + assert_eq!(pairs(&run(&dedup)), bfs(&dedup), "case {case}"); + } +} + +#[test] +fn a_cycle_terminates_and_reaches_itself() { + let r = run(CYCLE); + let p = pairs(&r); + assert!(p.contains(&(1, 1)) && p.contains(&(3, 3))); + assert!(!p.contains(&(4, 1))); + // Semi-naive: rounds are bounded by the longest shortest path plus one. + assert!(r.rounds <= 4, "rounds {}", r.rounds); +} + +#[test] +fn support_names_both_alternative_derivations_and_nothing_else() { + let r = run(DIAMOND); + let s = |id| r.map.slot(id).unwrap(); + let sup = support(&r.edge, &r.path, r.map.valid(), s(1), s(5)); + let got: BTreeSet<(u32, u32)> = (0..r.map.len()) + .flat_map(|u| r.map.ids(sup[u]).into_iter().map(move |v| (u, v))) + .map(|(u, v)| (r.map.ids(1 << u)[0], v)) + .collect(); + // Both branches of the diamond, and the shared tail. + let want: BTreeSet<(u32, u32)> = DIAMOND.iter().copied().collect(); + assert_eq!(got, want); + // A pair with one route uses only that route. + let one = support(&r.edge, &r.path, r.map.valid(), s(2), s(5)); + assert_eq!(one[s(1)], 0, "1->2 is not on any route from 2"); + assert_eq!(one[s(3)], 0, "3->4 is not on any route from 2"); + // An answer that does not hold has no support. + let none = support(&r.edge, &r.path, r.map.valid(), s(5), s(1)); + assert!(none.iter().all(|&w| w == 0)); +} + +#[test] +fn affected_is_every_answer_the_fact_feeds() { + let r = run(DIAMOND); + let s = |id| r.map.slot(id).unwrap(); + // Removing 3->4 and recomputing changes no answer (2->4 still routes). + let without: Vec<_> = DIAMOND.iter().copied().filter(|&e| e != (3, 4)).collect(); + let before = bfs(DIAMOND); + let after = bfs(&without); + let lost: BTreeSet<_> = before.difference(&after).copied().collect(); + assert_eq!(lost, [(3, 4), (3, 5)].into_iter().collect()); + // `affected` over-approximates what a removal can change: every answer + // with some derivation through 3->4. + let aff = affected(&r.path, r.map.valid(), s(3), s(4)); + let fed: BTreeSet<(u32, u32)> = (0..r.map.len()) + .flat_map(|a| r.map.ids(aff[a]).into_iter().map(move |b| (a, b))) + .map(|(a, b)| (r.map.ids(1 << a)[0], b)) + .collect(); + assert!(lost.is_subset(&fed)); + assert_eq!( + fed, + [(1, 4), (1, 5), (3, 4), (3, 5)] + .into_iter() + .collect::>() + ); +} + +#[test] +fn refuses_non_linear_and_reordered_recursion() { + let nonlinear = "pred edge(u32, u32). +pred path(u32, u32). +path(X, Y) :- edge(X, Y). +path(X, Y) :- path(X, Z), path(Z, Y). +?- path(X, Y). +"; + let (plan, rel) = compile(&program(DIAMOND, nonlinear)); + assert!(matches!( + admit_closure(&plan, &rel), + Err(LowerRefusal::UnsupportedNode(_)) + )); + + let mutual = "pred edge(u32, u32). +pred a(u32, u32). +pred b(u32, u32). +a(X, Y) :- edge(X, Y). +a(X, Y) :- b(X, Z), edge(Z, Y). +b(X, Y) :- a(X, Y). +?- a(X, Y). +"; + let (plan, rel) = compile(&program(DIAMOND, mutual)); + assert_eq!( + admit_closure(&plan, &rel), + Err(LowerRefusal::UnsupportedNode("mutual recursion")) + ); +} + +#[test] +fn refuses_a_stale_frame() { + let src = program(DIAMOND, RULES); + let tuples = facts(&parse_program(&src).unwrap(), "edge").unwrap(); + let map = AddressMap::new(N, tuples.iter().flat_map(|&(a, b)| [a, b])).unwrap(); + let edge = register(&tuples, &map, &map).unwrap(); + let mut st = store(); + let old = guards(&st); + st.advance(FrameRevisions { + source: 2, + relation_map: 1, + coordinates: 1, + }); + assert!(matches!( + closure(&st, &old, (FOCUS, SCOPE), sig(), &edge, map.valid()), + Err(EvalRefusal::Bind(Refusal::SourceChanged)) + )); +} From 9a7b418139b52e41295cae4a00840b163d95175e Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:08:14 +0000 Subject: [PATCH 02/11] xlog-relcomp-probe: tighten the support and non-linear refusal tests Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/tests/recursive.rs | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/crates/xlog-relcomp-probe/tests/recursive.rs b/crates/xlog-relcomp-probe/tests/recursive.rs index 808a16265..07db3a3cb 100644 --- a/crates/xlog-relcomp-probe/tests/recursive.rs +++ b/crates/xlog-relcomp-probe/tests/recursive.rs @@ -289,6 +289,11 @@ fn support_names_both_alternative_derivations_and_nothing_else() { let one = support(&r.edge, &r.path, r.map.valid(), s(2), s(5)); assert_eq!(one[s(1)], 0, "1->2 is not on any route from 2"); assert_eq!(one[s(3)], 0, "3->4 is not on any route from 2"); + // An edge reachable from x that cannot reach y is not support: 4->5 + // for path(1, 4). + let to4 = support(&r.edge, &r.path, r.map.valid(), s(1), s(4)); + assert_eq!(to4[s(4)], 0, "4->5 does not lead to 4"); + assert_eq!(to4[s(2)], 1 << s(4)); // An answer that does not hold has no support. let none = support(&r.edge, &r.path, r.map.valid(), s(5), s(1)); assert!(none.iter().all(|&w| w == 0)); @@ -329,10 +334,12 @@ path(X, Y) :- path(X, Z), path(Z, Y). ?- path(X, Y). "; let (plan, rel) = compile(&program(DIAMOND, nonlinear)); - assert!(matches!( + assert_eq!( admit_closure(&plan, &rel), - Err(LowerRefusal::UnsupportedNode(_)) - )); + Err(LowerRefusal::UnsupportedNode( + "non-linear or reordered step" + )) + ); let mutual = "pred edge(u32, u32). pred a(u32, u32). From 38d21a50f0b46c66b3f136cee493dbd5b06b77cd Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:08:44 +0000 Subject: [PATCH 03/11] xlog-relcomp-probe: pin semi-naive work to one row OR per derived pair Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/tests/recursive.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/crates/xlog-relcomp-probe/tests/recursive.rs b/crates/xlog-relcomp-probe/tests/recursive.rs index 07db3a3cb..d8da91881 100644 --- a/crates/xlog-relcomp-probe/tests/recursive.rs +++ b/crates/xlog-relcomp-probe/tests/recursive.rs @@ -184,6 +184,7 @@ struct Run { edge: [u64; SLOTS], path: [u64; SLOTS], rounds: usize, + row_ors: u64, } fn run(edges: &[(u32, u32)]) -> Run { @@ -201,6 +202,7 @@ fn run(edges: &[(u32, u32)]) -> Run { edge, path: c.rows, rounds: c.rounds, + row_ors: c.work.row_ors, } } @@ -374,3 +376,16 @@ fn refuses_a_stale_frame() { Err(EvalRefusal::Bind(Refusal::SourceChanged)) )); } + +#[test] +fn semi_naive_composes_each_derived_pair_exactly_once() { + // Each derived pair enters the delta in exactly one round, and composing + // a delta does one row OR per set bit, so the total work is |path|. + // Naive evaluation recomposes the whole closure every round. + let chain: Vec<(u32, u32)> = (0..20).map(|i| (i, i + 1)).collect(); + for edges in [DIAMOND, CYCLE, chain.as_slice()] { + let r = run(edges); + let derived: u64 = r.path.iter().map(|w| u64::from(w.count_ones())).sum(); + assert_eq!(r.row_ors, derived, "{edges:?}"); + } +} From aed7f4b586acc12a3c9b00361538cde688d16a23 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:11:16 +0000 Subject: [PATCH 04/11] xlog-relcomp-probe: XLOG and egglog reasoning over one DR64 relation One edge register under a sealed frame is read by XLOG's compiled closure (directed reachability) and by egglog (equality with proofs, via (rule ((edge a b)) ((union a b)))). Tests: egglog equality equals the closure of E u E^T on all pairs; every directed path is an equality; an egglog proof rests only on bits of the shared register, and on a directed answer every proof fact lies in XLOG's support mask; a removed fact invalidates the XLOG bind and is found in the old proof by address. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/Cargo.toml | 4 + crates/xlog-relcomp-probe/src/recursive.rs | 2 +- .../tests/shared_relation.rs | 341 ++++++++++++++++++ 3 files changed, 346 insertions(+), 1 deletion(-) create mode 100644 crates/xlog-relcomp-probe/tests/shared_relation.rs diff --git a/crates/xlog-relcomp-probe/Cargo.toml b/crates/xlog-relcomp-probe/Cargo.toml index e4c3c6bb2..283d2b1a2 100644 --- a/crates/xlog-relcomp-probe/Cargo.toml +++ b/crates/xlog-relcomp-probe/Cargo.toml @@ -34,6 +34,10 @@ xlog-logic = { git = "https://github.com/BrainyBlaze/xlog", rev = "bff6da6633081 lance-graph-contract = { path = "../lance-graph-contract" } # CausalEdge64, for the Epi5 reading of XLOG results (tests/epi5_reading.rs). causal-edge = { path = "../causal-edge" } +# egglog, on the coordinate dr-math-binding-probe already uses, for the +# shared-relation experiment (tests/shared_relation.rs): equality with proofs +# over the same DR64 register the closure reads. +egglog = { git = "https://github.com/AdaWorldAPI/egglog", branch = "main" } [patch."https://github.com/AdaWorldAPI/lance-graph"] lance-graph-contract = { path = "../lance-graph-contract" } diff --git a/crates/xlog-relcomp-probe/src/recursive.rs b/crates/xlog-relcomp-probe/src/recursive.rs index c5e82c6d9..acf187127 100644 --- a/crates/xlog-relcomp-probe/src/recursive.rs +++ b/crates/xlog-relcomp-probe/src/recursive.rs @@ -110,7 +110,7 @@ fn step_edge(body: &RirNode, head: RelId) -> Result { join_type, } => { if *join_type != JoinType::Inner { - return Err(LowerRefusal::UnsupportedJoin(join_type.clone())); + return Err(LowerRefusal::UnsupportedJoin(*join_type)); } let ([lk], [rk]) = (left_keys.as_slice(), right_keys.as_slice()) else { return Err(LowerRefusal::NeedsInverse { diff --git a/crates/xlog-relcomp-probe/tests/shared_relation.rs b/crates/xlog-relcomp-probe/tests/shared_relation.rs new file mode 100644 index 000000000..3c6a58380 --- /dev/null +++ b/crates/xlog-relcomp-probe/tests/shared_relation.rs @@ -0,0 +1,341 @@ +//! XLOG and egglog reasoning over one relation. +//! +//! One `edge` relation is stored once, as a DR64 register under a sealed +//! frame. XLOG's compiled closure (`recursive::closure`) reads it for +//! directed reachability. egglog reads the same register for equality: +//! `(rule ((edge a b)) ((union a b)))`, so `a = b` exactly when `a` and `b` +//! are connected ignoring direction, and egglog returns a proof. +//! +//! What is shared: +//! - **Addresses.** Both engines name a node by its source id through one +//! `AddressMap`; the register stores slots. The one conversion is +//! register bits -> egglog fact text, counted below. +//! - **Witnesses.** The `edge` facts an egglog proof rests on are read back +//! from the proof and checked against the same register bits, and against +//! the closure's `support` masks. Neither engine's derivation is +//! re-encoded as the other's. +//! +//! What is not shared: egglog keeps its own tables and union-find, and XLOG's +//! closure is not an equality. egglog's union-find is not replaced by masks. + +#![allow(clippy::needless_range_loop)] // slot arithmetic reads clearer indexed + +use std::collections::BTreeSet; + +use dr_math_binding_probe::{ + Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Scope, +}; +use egglog::proof::{Justification, ProofId, ProofStore}; +use egglog::{CommandOutput, EGraph}; +use xlog_relcomp_probe::recursive::{closure, support}; +use xlog_relcomp_probe::{AddressMap, SLOTS, register}; + +const N: Axis = Axis { + class: 30, + kind: AxisKind::Identity, +}; +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; + +fn sig() -> MethodSignature { + MethodSignature::presence(40, 0, N, N) +} +fn revs(source: u64) -> FrameRevisions { + FrameRevisions { + source, + relation_map: 1, + coordinates: 1, + } +} +fn guards(st: &FrameStore) -> Guards { + Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + } +} + +type Rows = [u64; SLOTS]; + +/// The one stored relation, and the map that names its slots. +struct Shared { + map: AddressMap, + edge: Rows, + store: FrameStore, +} + +fn shared(edges: &[(u32, u32)]) -> Shared { + let map = AddressMap::new(N, edges.iter().flat_map(|&(a, b)| [a, b])).unwrap(); + let edge = register(edges, &map, &map).unwrap(); + Shared { + map, + edge, + store: FrameStore::new(revs(1)), + } +} + +fn id(map: &AddressMap, slot: usize) -> u32 { + map.ids(1 << slot)[0] +} + +/// The conversion into egglog: one fact per set bit of the register, named +/// by source id. Read from the register, not from the source tuples. +fn egglog_facts(s: &Shared) -> String { + let mut out = String::new(); + for u in 0..s.map.len() { + for v in s.map.ids(s.edge[u]) { + out.push_str(&format!("(edge (N {}) (N {v}))\n", id(&s.map, u))); + } + } + out +} + +const HEADER: &str = "(datatype Node (N i64)) +(relation edge (Node Node)) +(ruleset same) +(rule ((edge a b)) ((union a b)) :ruleset same) +"; + +/// egglog's proof of `(N x) = (N y)`, or `None` when it cannot prove it. +fn prove(s: &Shared, x: u32, y: u32) -> Option<(ProofStore, ProofId)> { + let program = format!( + "{HEADER}{}(run same 100)\n(prove (= (N {x}) (N {y})))\n", + egglog_facts(s) + ); + EGraph::new_with_proofs() + .parse_and_run_program(None, &program) + .ok()? + .into_iter() + .find_map(|o| match o { + CommandOutput::ProveExists { + proof_store, + proof_id, + } => Some((proof_store, proof_id)), + _ => None, + }) +} + +/// Whether egglog holds `(N x) = (N y)`, without proofs. +fn equal(s: &Shared, x: u32, y: u32) -> bool { + let program = format!( + "{HEADER}{}(run same 100)\n(check (= (N {x}) (N {y})))\n", + egglog_facts(s) + ); + EGraph::default() + .parse_and_run_program(None, &program) + .is_ok() +} + +/// The `edge` facts a proof rests on: every proposition in the proof DAG +/// whose term is an `edge` atom, read as `(u, v)` source ids. +fn proof_edges(store: &ProofStore, root: ProofId) -> BTreeSet<(u32, u32)> { + let mut out = BTreeSet::new(); + let mut seen = BTreeSet::new(); + let mut todo = vec![root]; + while let Some(p) = todo.pop() { + if !seen.insert(p) { + continue; + } + let proof = store.get(p); + for t in [proof.lhs(), proof.rhs()] { + if let Some(e) = parse_edge(&store.term_dag().to_string(t)) { + out.insert(e); + } + } + match proof.justification() { + Justification::Rule { premise_proofs, .. } => todo.extend(premise_proofs), + Justification::MergeFn { + old_proof, + new_proof, + .. + } => todo.extend([*old_proof, *new_proof]), + Justification::Trans(a, b) => todo.extend([*a, *b]), + Justification::Sym(a) => todo.push(*a), + Justification::Congr { + proof, child_proof, .. + } => todo.extend([*proof, *child_proof]), + Justification::ContainerNormalize { proof } => todo.push(*proof), + Justification::Fiat | Justification::Eval => {} + } + } + out +} + +fn parse_edge(t: &str) -> Option<(u32, u32)> { + let rest = t.strip_prefix("(edge (N ")?; + let (a, rest) = rest.split_once(") (N ")?; + let b = rest.strip_suffix("))")?; + Some((a.parse().ok()?, b.parse().ok()?)) +} + +/// `E ∪ Eᵀ` over the same slots, computed from the register. +fn symmetric(edge: &Rows) -> Rows { + let mut out = *edge; + for (u, &w) in edge.iter().enumerate() { + for v in 0..SLOTS { + if w >> v & 1 == 1 { + out[v] |= 1 << u; + } + } + } + out +} + +fn closure_of(s: &Shared, rows: &Rows) -> Rows { + closure( + &s.store, + &guards(&s.store), + (FOCUS, SCOPE), + sig(), + rows, + s.map.valid(), + ) + .unwrap() + .rows +} + +const DIAMOND: &[(u32, u32)] = &[(1, 2), (1, 3), (2, 4), (3, 4), (4, 5)]; +/// Two components: {1,2,3,4,5} and {7,8}. +const TWO: &[(u32, u32)] = &[(1, 2), (1, 3), (2, 4), (3, 4), (4, 5), (8, 7)]; + +#[test] +fn egglog_equality_is_the_closure_of_the_symmetric_relation() { + let s = shared(TWO); + let sym = closure_of(&s, &symmetric(&s.edge)); + for x in 0..s.map.len() { + for y in 0..s.map.len() { + let want = sym[x] >> y & 1 == 1; + assert_eq!( + equal(&s, id(&s.map, x), id(&s.map, y)), + want, + "{} = {}", + id(&s.map, x), + id(&s.map, y) + ); + } + } +} + +#[test] +fn every_directed_path_is_an_egglog_equality() { + let s = shared(TWO); + let path = closure_of(&s, &s.edge); + for x in 0..s.map.len() { + for y in s.map.ids(path[x]) { + assert!(equal(&s, id(&s.map, x), y)); + } + } + // The converse fails: 5 = 1 holds, path(5, 1) does not. + assert!(equal(&s, 5, 1)); + assert_eq!( + path[s.map.slot(5).unwrap()] >> s.map.slot(1).unwrap() & 1, + 0 + ); +} + +#[test] +fn an_egglog_proof_rests_only_on_facts_in_the_shared_register() { + let s = shared(DIAMOND); + let (store, root) = prove(&s, 1, 5).expect("1 = 5 is provable"); + let used = proof_edges(&store, root); + assert!(!used.is_empty(), "the proof names at least one edge fact"); + for &(u, v) in &used { + let (su, sv) = (s.map.slot(u).unwrap(), s.map.slot(v).unwrap()); + assert_eq!( + s.edge[su] >> sv & 1, + 1, + "edge({u}, {v}) is a bit of the register" + ); + } + // The facts connect 1 and 5 ignoring direction. + let mut reach = BTreeSet::from([1u32]); + loop { + let before = reach.len(); + for &(u, v) in &used { + if reach.contains(&u) || reach.contains(&v) { + reach.extend([u, v]); + } + } + if reach.len() == before { + break; + } + } + assert!(reach.contains(&5)); +} + +#[test] +fn egglog_and_xlog_witnesses_meet_on_the_same_coordinates() { + // For a directed answer, egglog's proof of the equality and XLOG's + // support mask name facts in one coordinate space. Here every proof fact + // is in the support, because the diamond has no edge off the 1 -> 5 + // routes. + let s = shared(DIAMOND); + let path = closure_of(&s, &s.edge); + let (x, y) = (s.map.slot(1).unwrap(), s.map.slot(5).unwrap()); + let sup = support(&s.edge, &path, s.map.valid(), x, y); + let (store, root) = prove(&s, 1, 5).unwrap(); + for (u, v) in proof_edges(&store, root) { + let (su, sv) = (s.map.slot(u).unwrap(), s.map.slot(v).unwrap()); + assert_eq!(sup[su] >> sv & 1, 1, "edge({u}, {v}) supports path(1, 5)"); + } +} + +#[test] +fn a_changed_fact_invalidates_both_readers_by_address() { + let mut s = shared(DIAMOND); + let old = guards(&s.store); + let (store, root) = prove(&s, 1, 5).unwrap(); + let used = proof_edges(&store, root); + // The source changes: 4 -> 5 is removed, the frame advances. + let (s4, s5) = (s.map.slot(4).unwrap(), s.map.slot(5).unwrap()); + s.edge[s4] &= !(1 << s5); + s.store.advance(revs(2)); + // XLOG: the old frame no longer binds. + assert!( + closure( + &s.store, + &old, + (FOCUS, SCOPE), + sig(), + &s.edge, + s.map.valid() + ) + .is_err() + ); + // egglog: the old proof names a fact that is no longer a bit, found by + // address without re-running egglog. + let stale: Vec<_> = used + .iter() + .filter(|&&(u, v)| s.edge[s.map.slot(u).unwrap()] >> s.map.slot(v).unwrap() & 1 == 0) + .collect(); + assert_eq!(stale, [&(4, 5)]); + // Re-running on the new frame agrees: 1 = 5 is gone, while 1 = 4 still + // proves on the same program (so the program itself still runs). + assert!(prove(&s, 1, 5).is_none()); + assert!(!equal(&s, 1, 5)); + assert!(prove(&s, 1, 4).is_some()); +} + +#[test] +fn report_conversion_and_work() { + let s = shared(TWO); + let facts = egglog_facts(&s); + let path = closure( + &s.store, + &guards(&s.store), + (FOCUS, SCOPE), + sig(), + &s.edge, + s.map.valid(), + ) + .unwrap(); + println!( + "register: {} B, {} edges; egglog fact text: {} B; closure: {} rounds, {} row ORs", + SLOTS * 8, + TWO.len(), + facts.len(), + path.rounds, + path.work.row_ors + ); + assert_eq!(facts.lines().count(), TWO.len()); +} From b75a26c9f6a86ef530946622c6b15aec9e789036 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:11:37 +0000 Subject: [PATCH 05/11] xlog-relcomp-probe: README section and board entry for the shared-relation stage Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- ...codegraph-0-xlog-egglog-shared-relation.md | 19 +++++++++ .claude/board/entries/README.md | 3 +- crates/xlog-relcomp-probe/README.md | 41 +++++++++++++++++++ 3 files changed, 62 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md diff --git a/.claude/board/entries/2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md b/.claude/board/entries/2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md new file mode 100644 index 000000000..b935beaf6 --- /dev/null +++ b/.claude/board/entries/2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md @@ -0,0 +1,19 @@ +# D-REASONING-CODEGRAPH-0 stage 1: XLOG × egglog over one DR64 relation + +**Date 2026-10-31 · Status MEASURED (lab probe) · Crate `crates/xlog-relcomp-probe` (`src/recursive.rs`, `tests/recursive.rs`, `tests/shared_relation.rs`)** + +**XLOG recursion on the CPU kernel.** XLOG's compiled transitive-closure SCC is admitted (`admit_closure`) and evaluated semi-naively on the DR64 register with the existing `relcomp::compose`. #1888 noted this was not covered by #1884. It matches BFS and a fixpoint walk of XLOG's own plan, and a 200-case differential. Work is exactly one row OR per derived pair. Non-linear and mutual recursion are refused. + +**Shared relation.** One `edge` register under one sealed frame is read by XLOG's closure (directed reachability) and by egglog (equality with `ProofStore` proofs). +- egglog's equality equals the closure of `E ∪ Eᵀ`. +- egglog proof facts are bits of the same register, and lie inside XLOG's `support` mask for a directed answer. +- A removed fact invalidates the XLOG bind (stale frame) and is located in the old egglog proof by address, without re-running egglog. + +**Traceroute.** Backward is `support(x, y)` and forward is `affected(u, v)`, both computed from the closure on demand; derivations are not stored. The one conversion is register bits to egglog fact text (114 B for 6 edges). + +OPEN: +- timing; +- MLIR/DialEgg leg; +- SQL and Java legs; +- egglog proofs of a directed relation; +- XLOG recursion shapes beyond one linear closure. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c49146404..4c6d40e7b 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ 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. -526 entries, 2026-08-06 .. 2026-10-31. +527 entries, 2026-08-06 .. 2026-10-31. | date | entry id | finding | file | |---|---|---|---| @@ -35,6 +35,7 @@ exactly one of them, never both. | 2026-10-31 | `D-SAG-6-2-JOIN-IDENT` | | [2026-10-31-d-sag-6-2-span-join-identity.md](2026-10-31-d-sag-6-2-span-join-identity.md) | | 2026-10-31 | `D-SAG-6-2-LAB` | | [2026-10-31-d-sag-6-2-lab-projection.md](2026-10-31-d-sag-6-2-lab-projection.md) | | 2026-10-31 | `D-SAG-6-1-CHECKLIST` | | [2026-10-31-d-sag-6-1-checklist.md](2026-10-31-d-sag-6-1-checklist.md) | +| 2026-10-31 | `D-REASONING-CODEGRAPH-0` | | [2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md](2026-10-31-d-reasoning-codegraph-0-xlog-egglog-shared-relation.md) | | 2026-10-31 | `D-MIST-NATIVE-1b` | | [2026-10-31-d-mist-native-1b-makor-hydrate.md](2026-10-31-d-mist-native-1b-makor-hydrate.md) | | 2026-10-31 | `D-DT64-6-DR` | | [2026-10-31-d-dt64-6-dr-addressing-module.md](2026-10-31-d-dt64-6-dr-addressing-module.md) | | 2026-10-31 | `D-DYNBAG-X` | | [2026-10-31-cross-frontend-projection-crosswalk.md](2026-10-31-cross-frontend-projection-crosswalk.md) | diff --git a/crates/xlog-relcomp-probe/README.md b/crates/xlog-relcomp-probe/README.md index 97bb01e4d..20a227d18 100644 --- a/crates/xlog-relcomp-probe/README.md +++ b/crates/xlog-relcomp-probe/README.md @@ -342,3 +342,44 @@ The Y axis is DR's `lance_graph_dt64::dr::LocalMap` (64 or 256 wide). `admit_cou - adding instead of multiplying: 2 failed; - ignoring a bound: 5 + 1 failed; - admitting any aggregate: 1 failed. + +## Recursion and a second engine on the same relation (`src/recursive.rs`) + +**Recursion.** XLOG compiles `path(X, Y) :- edge(X, Y). path(X, Y) :- path(X, Z), edge(Z, Y).` +into one recursive SCC: a base `Scan edge`, and a `ChainJoin` of `Scan path` with `Scan edge` on +`path.1 = edge.0`, projecting columns 0 and 3, with an agreeing `fallback`. `admit_closure` +accepts exactly that shape. It refuses non-linear recursion (`path ∘ path`) and mutual recursion, +each with its own reason. `closure` binds `edge` under the sealed frame, types `edge ∘ edge` with +the existing chain typing, and runs semi-naive rounds over the existing `relcomp::compose`. No new +kernel is added. + +`tests/recursive.rs` (9 tests): +- the result equals BFS over the tuples and a naive fixpoint walk of XLOG's own compiled bodies; +- a 200-case deterministic differential against BFS passes; +- cycles terminate; +- semi-naive work is exactly one row OR per derived pair; +- a stale frame is refused. + +**Derivations on demand.** `support(x, y)` returns the `edge` facts some derivation of +`path(x, y)` can use: both branches of a diamond, nothing off-route. `affected(u, v)` returns the +answers a fact can feed. Both are masks read from the closure; nothing about a derivation is stored. + +**A second engine.** `tests/shared_relation.rs` puts egglog on the same register. Equality comes +from `(rule ((edge a b)) ((union a b)))`, and proofs from `prove`. +- egglog's `a = b` equals the closure of `E ∪ Eᵀ` on every pair of a two-component graph. +- Every directed `path` is an egglog equality; the converse fails. +- Every `edge` fact an egglog proof rests on is a bit of the shared register. On the diamond, every + such fact also lies in XLOG's `support` mask for the same answer. +- When a fact is removed and the frame advances, the XLOG bind refuses, and the removed fact is + found in the old egglog proof by its address, without re-running egglog. + +The one conversion is register bits to egglog fact text. For 6 edges that is 114 bytes, against a +512-byte register. egglog keeps its own tables and union-find; they are not replaced by masks. + +Disable runs: dropping the support filter, the reflexive star in `affected`, the non-linear guard, +the mutual-recursion guard, or semi-naive deltas each turns its test red. + +Not done: +- timing, for either engine; +- XLOG recursion beyond one linear closure; +- egglog proofs of a directed relation (egglog's equality is symmetric by construction). From 29aca90ff56a7c89f6892f6f6432cd86f63ead94 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:27:50 +0000 Subject: [PATCH 06/11] xlog-relcomp-probe: authentic backward trace and X6 provenance trace(edge, valid, x, y) replays closure's semi-naive rounds and returns the derivation evaluation performed: from the round path(x, y) first appeared, back through the previous round's delta and edge, smallest intermediate first. tests/trace.rs checks it against BFS shortest paths, the register, and support. tests/provenance.rs: provenance is source root + frame version + program hash + CE64 declared reading (XLOG only). The root is an observer and its sorted, deduplicated facts, so re-serializing a report is never new evidence; the program hash covers the program, never the facts. Derivation multiplicity is counted separately from independent roots, and two consumers of one root are one observation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/README.md | 29 ++ crates/xlog-relcomp-probe/src/recursive.rs | 50 ++ crates/xlog-relcomp-probe/tests/provenance.rs | 449 ++++++++++++++++++ crates/xlog-relcomp-probe/tests/trace.rs | 173 +++++++ 4 files changed, 701 insertions(+) create mode 100644 crates/xlog-relcomp-probe/tests/provenance.rs create mode 100644 crates/xlog-relcomp-probe/tests/trace.rs diff --git a/crates/xlog-relcomp-probe/README.md b/crates/xlog-relcomp-probe/README.md index 20a227d18..659531a1d 100644 --- a/crates/xlog-relcomp-probe/README.md +++ b/crates/xlog-relcomp-probe/README.md @@ -383,3 +383,32 @@ Not done: - timing, for either engine; - XLOG recursion beyond one linear closure; - egglog proofs of a directed relation (egglog's equality is symmetric by construction). + +## Traceroute and provenance (`src/recursive.rs`, `tests/trace.rs`, `tests/provenance.rs`) + +**Traceroute.** `trace(edge, valid, x, y)` replays the semi-naive rounds `closure` runs, keeps each +round's delta, and walks back from the round in which `path(x, y)` first appeared, choosing the +smallest `z` with `(x, z)` in the previous delta and `edge(z, y)`. It returns the chain of `edge` +facts, or `None` when the pair does not hold. `closure` is unchanged. `tests/trace.rs` (6 tests) +checks on the diamond, the cycle and a 200-case random differential that every chain starts at `x`, +ends at `y`, links up, uses only bits of `edge` inside `support(x, y)`, and has the BFS +shortest-path length. + +**Provenance.** `tests/provenance.rs` (6 tests) carries X6 provenance at test level: +`Provenance { root, version, program_hash, reading }`. +- `root` identifies the original source: an observer and the set of facts it reported, sorted and + deduplicated, so a reordered or repeated copy of one report is the same root. +- `version` is the frame's `FrameRevisions`. +- `program_hash` is FNV-1a over the consumer's program text (XLOG rules, or egglog rules), never over + the facts. +- `reading` is the CE64 declared reading, read through `Epi5Declarations`: `Direct × Open` for a + trace of length 1, `IndirectKnown × Open` otherwise. An egglog equality has no declared reading + (`None`). + +Evidence and derivations are counted separately: +- On the diamond, `path(1, 5)` has 2 derivations. With one observer they rest on 1 root; with a + second observer reporting one branch, the same 2 derivations rest on 2 roots. +- XLOG's trace and an egglog proof over one register are two consumers with two program hashes and + one root: 1 independent observation. + +Not shown: that a root hash is a durable source identity outside these tests. diff --git a/crates/xlog-relcomp-probe/src/recursive.rs b/crates/xlog-relcomp-probe/src/recursive.rs index acf187127..93abcf77b 100644 --- a/crates/xlog-relcomp-probe/src/recursive.rs +++ b/crates/xlog-relcomp-probe/src/recursive.rs @@ -237,3 +237,53 @@ pub fn affected(path: &Rows, valid: u64, u: usize, v: usize) -> Rows { } out } + +/// The derivation semi-naive evaluation performed for `path(x, y)`, as the +/// `edge` facts `[(x, z1), (z1, z2), ..., (zk, y)]` in slot coordinates. +/// +/// Replays the rounds [`closure`] runs (round 1 is `edge & valid`; round +/// r+1 is `compose(delta, edge) & valid & !path`) and keeps each round's +/// delta. `path(x, y)` enters the delta in exactly one round r; for r = 1 the +/// derivation is the base fact, otherwise it extends a pair `(x, z)` from +/// round r-1 by `edge(z, y)`, taking the smallest such `z`. The chain length +/// is therefore the shortest-path length. `None` when `path(x, y)` does not +/// hold. Allocates; it is a cold replay and does not touch [`closure`]. +pub fn trace(edge: &Rows, valid: u64, x: usize, y: usize) -> Option> { + if x >= SLOTS || y >= SLOTS { + return None; + } + let mut path = [0u64; SLOTS]; + for (p, w) in path.iter_mut().zip(edge) { + *p = w & valid; + } + let mut deltas: Vec = vec![path]; + let mut work = Work::default(); + loop { + let last = deltas[deltas.len() - 1]; + let next = compose(&last, edge, &mut work); + let mut delta = [0u64; SLOTS]; + let mut any = false; + for i in 0..SLOTS { + delta[i] = next[i] & valid & !path[i]; + path[i] |= delta[i]; + any |= delta[i] != 0; + } + if !any { + break; + } + deltas.push(delta); + } + let mut round = deltas.iter().position(|d| d[x] >> y & 1 == 1)?; + let mut chain = Vec::with_capacity(round + 1); + let mut end = y; + while round > 0 { + let prev = &deltas[round - 1]; + let z = (0..SLOTS).find(|&z| prev[x] >> z & 1 == 1 && edge[z] >> end & 1 == 1)?; + chain.push((z, end)); + end = z; + round -= 1; + } + chain.push((x, end)); + chain.reverse(); + Some(chain) +} diff --git a/crates/xlog-relcomp-probe/tests/provenance.rs b/crates/xlog-relcomp-probe/tests/provenance.rs new file mode 100644 index 000000000..bf019eea1 --- /dev/null +++ b/crates/xlog-relcomp-probe/tests/provenance.rs @@ -0,0 +1,449 @@ +//! X6 provenance and evidence roots. +//! +//! Provenance is the original source root, the frame version, the XLOG +//! program hash, and the CE64 declared reading. Evidence-root uniqueness is +//! counted separately from derivation multiplicity: two consumers of one +//! root are one independent observation, however many distinct derivations +//! the bag algebra holds. + +use std::collections::BTreeSet; + +use causal_edge::edge::CausalEdge64; +use dr_math_binding_probe::{ + Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Scope, +}; +use egglog::proof::{Justification, ProofId, ProofStore}; +use egglog::{CommandOutput, EGraph}; +use lance_graph_contract::band_reading::EdgeProvenance; +use lance_graph_contract::class_view::ClassId; +use lance_graph_contract::epistemic_state5::{ + Certification3, Epi5Declarations, Epi5Gen, Epi5Reading, EpistemicState5, Topology2, +}; +use lance_graph_contract::rail_geometry::RailAxis; +use xlog_relcomp_probe::recursive::{closure, trace}; +use xlog_relcomp_probe::{AddressMap, SLOTS, register}; + +const N: Axis = Axis { + class: 30, + kind: AxisKind::Identity, +}; +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; +const XLOG_VIEW: ClassId = 0x7F01; +const RAIL: RailAxis = RailAxis::Taxonomy; + +const RULES: &str = "pred edge(u32, u32). +pred path(u32, u32). +path(X, Y) :- edge(X, Y). +path(X, Y) :- path(X, Z), edge(Z, Y). +?- path(X, Y). +"; + +const DIAMOND: &[(u32, u32)] = &[(1, 2), (1, 3), (2, 4), (3, 4), (4, 5)]; + +const BASE: EpistemicState5 = + EpistemicState5::new(Epi5Gen::V1, Topology2::Direct, Certification3::Open); +const COMPOSED: EpistemicState5 = + EpistemicState5::new(Epi5Gen::V1, Topology2::IndirectKnown, Certification3::Open); + +fn fnv1a64(bytes: &[u8]) -> u64 { + let mut h = 0xcbf2_9ce4_8422_2325u64; + for &b in bytes { + h ^= u64::from(b); + h = h.wrapping_mul(0x0000_0100_0000_01b3); + } + h +} + +/// One observer's facts: who reported them, and what was reported. +struct Source<'a> { + observer: &'a str, + facts: &'a [(u32, u32)], +} + +/// The original source root: the observer and the set of facts it reported. +/// The facts are sorted and deduplicated first, so re-serializing the same +/// report in another order is the same root, never a new observation. +fn root(s: &Source<'_>) -> u64 { + let mut facts = s.facts.to_vec(); + facts.sort_unstable(); + facts.dedup(); + let mut bytes = s.observer.as_bytes().to_vec(); + bytes.push(0); + for (a, b) in facts { + bytes.extend_from_slice(&a.to_le_bytes()); + bytes.extend_from_slice(&b.to_le_bytes()); + } + fnv1a64(&bytes) +} + +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +struct Provenance { + root: u64, + version: FrameRevisions, + /// FNV-1a over the consumer's program text (XLOG rules, or egglog rules); + /// never over the facts, which the root already identifies. + program_hash: u64, + /// The CE64 declared reading. Declared for XLOG results only; an egglog + /// equality has no declared CE64 reading, so it is `None`. + reading: Option, +} + +fn declared() -> Epi5Declarations { + let mut d = Epi5Declarations::new(); + d.declare(XLOG_VIEW, RAIL, Epi5Reading::default()); + d +} + +/// The declared reading of an XLOG result whose trace has `trace_len` facts, +/// stamped into a CE64 edge and read back through the declaration. +fn reading(trace_len: usize) -> EpistemicState5 { + let state = if trace_len > 1 { COMPOSED } else { BASE }; + let e = CausalEdge64(0x0000_00AB_CD12_3456).with_epistemic_raw5(state.raw()); + declared() + .project_state5( + XLOG_VIEW, + RAIL, + Epi5Gen::V1, + e.epistemic_raw5(), + EdgeProvenance::V2Stamped, + ) + .unwrap() +} + +fn xlog_provenance( + s: &Source<'_>, + rules: &str, + version: FrameRevisions, + trace_len: usize, +) -> Provenance { + Provenance { + root: root(s), + version, + program_hash: fnv1a64(rules.as_bytes()), + reading: Some(reading(trace_len)), + } +} + +fn egglog_provenance(s: &Source<'_>, version: FrameRevisions) -> Provenance { + Provenance { + root: root(s), + version, + program_hash: fnv1a64(HEADER.as_bytes()), + reading: None, + } +} + +fn revs(source: u64) -> FrameRevisions { + FrameRevisions { + source, + relation_map: 1, + coordinates: 1, + } +} + +/// Every simple path from `x` to `y` over the edge tuples, as its facts. +fn derivations(edges: &[(u32, u32)], x: u32, y: u32) -> Vec> { + fn go( + edges: &[(u32, u32)], + at: u32, + y: u32, + seen: &mut Vec, + path: &mut Vec<(u32, u32)>, + out: &mut Vec>, + ) { + for &(a, b) in edges { + if a != at || seen.contains(&b) { + continue; + } + path.push((a, b)); + if b == y { + out.push(path.clone()); + } + seen.push(b); + go(edges, b, y, seen, path, out); + seen.pop(); + path.pop(); + } + } + let mut out = Vec::new(); + go(edges, x, y, &mut vec![x], &mut Vec::new(), &mut out); + out +} + +struct Reg { + map: AddressMap, + edge: [u64; SLOTS], +} + +fn reg(edges: &[(u32, u32)]) -> Reg { + let map = AddressMap::new(N, edges.iter().flat_map(|&(a, b)| [a, b])).unwrap(); + let edge = register(edges, &map, &map).unwrap(); + Reg { map, edge } +} + +/// The XLOG consumer: closure over the register, trace of `path(x, y)`. +fn xlog_trace_len(r: &Reg, x: u32, y: u32) -> usize { + let st = FrameStore::new(revs(1)); + let g = Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + }; + let sig = MethodSignature::presence(40, 0, N, N); + let c = closure(&st, &g, (FOCUS, SCOPE), sig, &r.edge, r.map.valid()).unwrap(); + let (sx, sy) = (r.map.slot(x).unwrap(), r.map.slot(y).unwrap()); + assert_eq!(c.rows[sx] >> sy & 1, 1, "path({x}, {y}) holds"); + trace(&r.edge, r.map.valid(), sx, sy).unwrap().len() +} + +const HEADER: &str = "(datatype Node (N i64)) +(relation edge (Node Node)) +(ruleset same) +(rule ((edge a b)) ((union a b)) :ruleset same) +"; + +/// egglog's proof of `(N x) = (N y)` over the register's facts. +fn prove(r: &Reg, x: u32, y: u32) -> Option<(ProofStore, ProofId)> { + let mut facts = String::new(); + for u in 0..r.map.len() { + for v in r.map.ids(r.edge[u]) { + facts.push_str(&format!("(edge (N {}) (N {v}))\n", r.map.ids(1 << u)[0])); + } + } + let program = format!("{HEADER}{facts}(run same 100)\n(prove (= (N {x}) (N {y})))\n"); + EGraph::new_with_proofs() + .parse_and_run_program(None, &program) + .ok()? + .into_iter() + .find_map(|o| match o { + CommandOutput::ProveExists { + proof_store, + proof_id, + } => Some((proof_store, proof_id)), + _ => None, + }) +} + +fn proof_edges(store: &ProofStore, root: ProofId) -> BTreeSet<(u32, u32)> { + let mut out = BTreeSet::new(); + let mut seen = BTreeSet::new(); + let mut todo = vec![root]; + while let Some(p) = todo.pop() { + if !seen.insert(p) { + continue; + } + let proof = store.get(p); + for t in [proof.lhs(), proof.rhs()] { + if let Some(e) = parse_edge(&store.term_dag().to_string(t)) { + out.insert(e); + } + } + match proof.justification() { + Justification::Rule { premise_proofs, .. } => todo.extend(premise_proofs), + Justification::MergeFn { + old_proof, + new_proof, + .. + } => todo.extend([*old_proof, *new_proof]), + Justification::Trans(a, b) => todo.extend([*a, *b]), + Justification::Sym(a) => todo.push(*a), + Justification::Congr { + proof, child_proof, .. + } => todo.extend([*proof, *child_proof]), + Justification::ContainerNormalize { proof } => todo.push(*proof), + Justification::Fiat | Justification::Eval => {} + } + } + out +} + +fn parse_edge(t: &str) -> Option<(u32, u32)> { + let rest = t.strip_prefix("(edge (N ")?; + let (a, rest) = rest.split_once(") (N ")?; + let b = rest.strip_suffix("))")?; + Some((a.parse().ok()?, b.parse().ok()?)) +} + +const A: &str = "observer-a"; +const B: &str = "observer-b"; + +#[test] +fn provenance_changes_when_and_only_when_its_inputs_change() { + let src = Source { + observer: A, + facts: DIAMOND, + }; + let base = xlog_provenance(&src, RULES, revs(1), 3); + + // A one-character rule change moves only the program hash. + let rules2 = RULES.replace("?- path(X, Y).", "?- path(X, Z)."); + let p = xlog_provenance(&src, &rules2, revs(1), 3); + assert_ne!(p.program_hash, base.program_hash); + assert_eq!( + (p.root, p.version, p.reading), + (base.root, base.version, base.reading) + ); + + // The frame advances: only the version moves. + let p = xlog_provenance(&src, RULES, revs(2), 3); + assert_ne!(p.version, base.version); + assert_eq!( + (p.root, p.program_hash, p.reading), + (base.root, base.program_hash, base.reading) + ); + + // One fact changes: only the root moves. The program hash covers the + // rules, never the facts. + let mut changed = DIAMOND.to_vec(); + changed[4] = (4, 6); + let p = xlog_provenance( + &Source { + observer: A, + facts: &changed, + }, + RULES, + revs(1), + 3, + ); + assert_ne!(p.root, base.root); + assert_eq!( + (p.program_hash, p.version, p.reading), + (base.program_hash, base.version, base.reading) + ); + + // Trace length 1 is Direct, longer is IndirectKnown; only the reading moves. + let direct = xlog_provenance(&src, RULES, revs(1), 1); + assert_eq!(direct.reading, Some(BASE)); + assert_eq!(base.reading, Some(COMPOSED)); + assert_eq!( + (direct.root, direct.version, direct.program_hash), + (base.root, base.version, base.program_hash) + ); +} + +#[test] +fn readings_follow_the_trace_of_the_real_closure() { + let r = reg(DIAMOND); + // Fails if a base fact reads as composed or a composed edge as direct. + assert_eq!(reading(xlog_trace_len(&r, 4, 5)), BASE); + assert_eq!(reading(xlog_trace_len(&r, 1, 5)), COMPOSED); +} + +#[test] +fn reordering_a_report_is_not_a_new_observation() { + // Fails if the root depends on how the facts were serialized: a reordered + // copy of one report would then count as independent evidence. + let reordered: Vec<(u32, u32)> = DIAMOND.iter().rev().copied().collect(); + let duplicated: Vec<(u32, u32)> = DIAMOND.iter().chain(DIAMOND).copied().collect(); + let a = root(&Source { + observer: A, + facts: DIAMOND, + }); + assert_eq!( + a, + root(&Source { + observer: A, + facts: &reordered + }) + ); + assert_eq!( + a, + root(&Source { + observer: A, + facts: &duplicated + }) + ); + // The same facts from another observer are a different root. + assert_ne!( + a, + root(&Source { + observer: B, + facts: DIAMOND + }) + ); +} + +#[test] +fn derivation_multiplicity_is_not_independent_evidence() { + // path(1, 5) has two derivations, 1->2->4->5 and 1->3->4->5. + let derivs = derivations(DIAMOND, 1, 5); + assert_eq!(derivs.len(), 2); + + // Case 1: one observer reported every fact. Two derivations, one root. + let roots_of = |sources: &[Source<'_>]| -> BTreeSet { + derivs + .iter() + .flatten() + .map(|f| { + let s = sources + .iter() + .find(|s| s.facts.contains(f)) + .expect("every fact has an observer"); + root(s) + }) + .collect() + }; + let one = [Source { + observer: A, + facts: DIAMOND, + }]; + assert_eq!(roots_of(&one).len(), 1); + assert_ne!(derivs.len(), roots_of(&one).len()); + + // Case 2: a second observer reported the 1->3->4 branch. The derivations + // are unchanged; the independent evidence is now two roots. + let a_facts: &[(u32, u32)] = &[(1, 2), (2, 4), (4, 5)]; + let b_facts: &[(u32, u32)] = &[(1, 3), (3, 4)]; + let two = [ + Source { + observer: A, + facts: a_facts, + }, + Source { + observer: B, + facts: b_facts, + }, + ]; + assert_eq!(derivations(DIAMOND, 1, 5).len(), 2); + assert_eq!(roots_of(&two).len(), 2); +} + +#[test] +fn two_consumers_of_one_root_are_one_observation() { + let src = Source { + observer: A, + facts: DIAMOND, + }; + let r = reg(DIAMOND); + + // Consumer 1: XLOG's closure and trace, with its declared CE64 reading. + let xlog = xlog_provenance(&src, RULES, revs(1), xlog_trace_len(&r, 1, 5)); + // Consumer 2: an egglog proof over the same register. Its facts are bits + // of that register, and it has no declared CE64 reading. + let (store, proof) = prove(&r, 1, 5).expect("1 = 5 is provable"); + let used = proof_edges(&store, proof); + assert!(!used.is_empty()); + assert!(used.iter().all(|f| DIAMOND.contains(f))); + let egg = egglog_provenance(&src, revs(1)); + assert_eq!(egg.reading, None); + assert_ne!(egg.program_hash, xlog.program_hash, "two programs"); + + // Two consumers, two programs, one root: one independent observation. + let roots: BTreeSet = [xlog.root, egg.root].into(); + assert_eq!(roots.len(), 1); +} + +#[test] +fn unrelated_sources_never_collapse_to_one_root() { + let b: &[(u32, u32)] = &[(7, 8), (8, 9)]; + let pa = root(&Source { + observer: A, + facts: DIAMOND, + }); + let pb = root(&Source { + observer: A, + facts: b, + }); + assert_ne!(pa, pb); +} diff --git a/crates/xlog-relcomp-probe/tests/trace.rs b/crates/xlog-relcomp-probe/tests/trace.rs new file mode 100644 index 000000000..c1e6b0532 --- /dev/null +++ b/crates/xlog-relcomp-probe/tests/trace.rs @@ -0,0 +1,173 @@ +//! `trace` returns the derivation semi-naive evaluation performed. + +use std::collections::{BTreeSet, VecDeque}; + +use dr_math_binding_probe::{ + Axis, AxisKind, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Scope, +}; +use xlog_relcomp_probe::recursive::{closure, support, trace}; +use xlog_relcomp_probe::{AddressMap, SLOTS, register}; + +const N: Axis = Axis { + class: 30, + kind: AxisKind::Identity, +}; +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 2 }; + +const DIAMOND: &[(u32, u32)] = &[(1, 2), (1, 3), (2, 4), (3, 4), (4, 5)]; +const CYCLE: &[(u32, u32)] = &[(1, 2), (2, 3), (3, 1), (3, 4)]; + +struct Run { + map: AddressMap, + edge: [u64; SLOTS], + path: [u64; SLOTS], +} + +fn run(edges: &[(u32, u32)]) -> Run { + let map = AddressMap::new(N, edges.iter().flat_map(|&(a, b)| [a, b])).unwrap(); + let edge = register(edges, &map, &map).unwrap(); + let st = FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: 1, + }); + let g = Guards { + frame: st.seal(), + focus: FOCUS, + scope: SCOPE, + }; + let sig = MethodSignature::presence(40, 0, N, N); + let path = closure(&st, &g, (FOCUS, SCOPE), sig, &edge, map.valid()) + .unwrap() + .rows; + Run { map, edge, path } +} + +/// BFS shortest path length in edges from `x` to `y` (at least 1). +fn bfs_len(edges: &[(u32, u32)], x: u32, y: u32) -> Option { + let mut dist = std::collections::BTreeMap::new(); + let mut q = VecDeque::new(); + for &(a, b) in edges { + if a == x && !dist.contains_key(&b) { + dist.insert(b, 1usize); + q.push_back(b); + } + } + while let Some(u) = q.pop_front() { + let d = dist[&u]; + for &(a, b) in edges { + if a == u && !dist.contains_key(&b) { + dist.insert(b, d + 1); + q.push_back(b); + } + } + } + dist.get(&y).copied() +} + +fn check_all(edges: &[(u32, u32)], label: &str) { + let r = run(edges); + let valid = r.map.valid(); + for x in 0..r.map.len() { + for y in 0..r.map.len() { + let holds = r.path[x] >> y & 1 == 1; + let t = trace(&r.edge, valid, x, y); + if !holds { + assert!(t.is_none(), "{label}: ({x},{y}) does not hold"); + continue; + } + let chain = t.unwrap_or_else(|| panic!("{label}: ({x},{y}) holds, trace is None")); + // Fails if the chain does not start at x or end at y. + assert_eq!(chain.first().unwrap().0, x, "{label}: start"); + assert_eq!(chain.last().unwrap().1, y, "{label}: end"); + // Fails if consecutive facts do not share endpoints. + for w in chain.windows(2) { + assert_eq!(w[0].1, w[1].0, "{label}: link"); + } + // Fails if a fact is not a bit of the register. + let sup = support(&r.edge, &r.path, valid, x, y); + for &(u, v) in &chain { + assert_eq!(r.edge[u] >> v & 1, 1, "{label}: ({u},{v}) not in edge"); + // Fails if the chain uses a fact outside support. + assert_eq!(sup[u] >> v & 1, 1, "{label}: ({u},{v}) not in support"); + } + // Fails if the first-derivation round is not the shortest distance. + let (ix, iy) = (r.map.ids(1 << x)[0], r.map.ids(1 << y)[0]); + assert_eq!( + Some(chain.len()), + bfs_len(edges, ix, iy), + "{label}: length of ({ix},{iy})" + ); + } + } +} + +#[test] +fn diamond_trace_takes_the_smallest_intermediate() { + let r = run(DIAMOND); + let s = |id| r.map.slot(id).unwrap(); + // Fails if the tie between 1->2->4 and 1->3->4 is not broken by smallest z. + let got = trace(&r.edge, r.map.valid(), s(1), s(5)).unwrap(); + assert_eq!(got, vec![(s(1), s(2)), (s(2), s(4)), (s(4), s(5))]); +} + +#[test] +fn a_base_fact_traces_to_itself() { + let r = run(DIAMOND); + let s = |id| r.map.slot(id).unwrap(); + // Fails if a round-1 pair recurses instead of returning the fact. + assert_eq!( + trace(&r.edge, r.map.valid(), s(4), s(5)).unwrap(), + vec![(s(4), s(5))] + ); +} + +#[test] +fn diamond_traces_are_valid_derivations() { + check_all(DIAMOND, "diamond"); +} + +#[test] +fn cycle_traces_are_valid_derivations() { + check_all(CYCLE, "cycle"); +} + +#[test] +fn a_pair_that_does_not_hold_has_no_trace() { + let r = run(DIAMOND); + let s = |id| r.map.slot(id).unwrap(); + // Fails if trace invents a chain against edge direction. + assert_eq!(trace(&r.edge, r.map.valid(), s(5), s(1)), None); + // Fails if an out-of-range slot is not refused. + assert_eq!(trace(&r.edge, r.map.valid(), SLOTS, 0), None); +} + +#[test] +fn deterministic_differential() { + let mut s = 0x9E37_79B9_7F4A_7C15u64; + let mut next = || { + s = s + .wrapping_mul(6364136223846793005) + .wrapping_add(1442695040888963407); + (s >> 33) as u32 + }; + let mut checked = BTreeSet::new(); + for case in 0..200 { + let n = 2 + next() % 40; + let m = next() % (3 * n); + let mut dedup: Vec<(u32, u32)> = Vec::new(); + for _ in 0..m { + let e = (next() % n, next() % n); + if !dedup.contains(&e) { + dedup.push(e); + } + } + if dedup.is_empty() { + continue; + } + check_all(&dedup, &format!("case {case}")); + checked.insert(case); + } + assert!(checked.len() > 150); +} From 8ecc963468a6028d67f5cf7713c75cf8060a8922 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:29:45 +0000 Subject: [PATCH 07/11] xlog-relcomp-probe: record the traceroute and provenance disable runs Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/README.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/crates/xlog-relcomp-probe/README.md b/crates/xlog-relcomp-probe/README.md index 659531a1d..37413c883 100644 --- a/crates/xlog-relcomp-probe/README.md +++ b/crates/xlog-relcomp-probe/README.md @@ -412,3 +412,16 @@ Evidence and derivations are counted separately: one root: 1 independent observation. Not shown: that a root hash is a durable source identity outside these tests. + +Disable runs for the traceroute and provenance (committed first, one patch at a time, each anchor asserted, file restored with `git checkout`): + +| Disabled | Red | +|---|---| +| `trace` picks the largest intermediate | `diamond_trace_takes_the_smallest_intermediate` | +| `trace` drops the `edge(z, y)` check | `deterministic_differential` | +| root depends on serialization order (no sort/dedup) | `reordering_a_report_is_not_a_new_observation` | +| program hash covers the facts | `provenance_changes_when_and_only_when_its_inputs_change` | +| root ignores the observer | `reordering_a_report_is_not_a_new_observation` | +| a base fact reads as composed | `readings_follow_the_trace_of_the_real_closure`, `provenance_changes_…` | + +One mutant stays green and is equivalent, not a missing test: searching for the last round that holds `(x, y)` instead of the first. Each round's delta excludes everything already derived, so a pair appears in exactly one round. From 900772424f66a7c1811d334672f12db681f40938 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:54:51 +0000 Subject: [PATCH 08/11] xlog-relcomp-probe: count independent support as minimal environments, not lineage derivation_multiplicity_is_not_independent_evidence counted the union of roots over all derivations (lineage) and called it independent evidence. With A reporting 1->2->4->5 and B only 1->3->4, the derivations rest on {A} and {A, B}; absorption leaves {A}, so there is one independent support, not two. The test now computes the ATMS label (PosBool provenance over source roots) and pins three cases: one observer, B dependent on A, and B independent of A. Lineage stays as a separate count and cannot tell the last two apart. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/tests/provenance.rs | 130 +++++++++++++----- 1 file changed, 93 insertions(+), 37 deletions(-) diff --git a/crates/xlog-relcomp-probe/tests/provenance.rs b/crates/xlog-relcomp-probe/tests/provenance.rs index bf019eea1..9be1bf541 100644 --- a/crates/xlog-relcomp-probe/tests/provenance.rs +++ b/crates/xlog-relcomp-probe/tests/provenance.rs @@ -364,49 +364,105 @@ fn reordering_a_report_is_not_a_new_observation() { ); } +type Env = BTreeSet; + +/// The minimal sets of roots that entail `path(x, y)`: the ATMS label, or +/// PosBool provenance, over source roots. A fact's label is one singleton +/// environment per source that reports it. A derivation's label is the +/// pairwise union of its facts' labels, and the answer's label is the union +/// over derivations. Every environment that contains another is dropped +/// (absorption: `A + A·B = A`). +fn label(derivs: &[Vec<(u32, u32)>], sources: &[Source<'_>]) -> BTreeSet { + let mut answer: BTreeSet = BTreeSet::new(); + for d in derivs { + let mut envs: BTreeSet = [Env::new()].into(); + for f in d { + let reporters: Vec = sources + .iter() + .filter(|s| s.facts.contains(f)) + .map(root) + .collect(); + assert!(!reporters.is_empty(), "every fact has an observer"); + envs = envs + .iter() + .flat_map(|e| { + reporters.iter().map(move |&r| { + let mut e = e.clone(); + e.insert(r); + e + }) + }) + .collect(); + } + answer.extend(envs); + } + let all = answer.clone(); + answer.retain(|e| !all.iter().any(|o| o != e && o.is_subset(e))); + answer +} + +/// The roots any derivation touches: lineage. It is not independent support. +fn lineage(derivs: &[Vec<(u32, u32)>], sources: &[Source<'_>]) -> BTreeSet { + derivs + .iter() + .flatten() + .flat_map(|f| { + sources + .iter() + .filter(move |s| s.facts.contains(f)) + .map(root) + }) + .collect() +} + +/// Independent supports: minimal environments that share no root. +fn disjoint(label: &BTreeSet) -> bool { + let envs: Vec<&Env> = label.iter().collect(); + envs.iter() + .enumerate() + .all(|(i, a)| envs[i + 1..].iter().all(|b| a.is_disjoint(b))) +} + #[test] fn derivation_multiplicity_is_not_independent_evidence() { // path(1, 5) has two derivations, 1->2->4->5 and 1->3->4->5. let derivs = derivations(DIAMOND, 1, 5); assert_eq!(derivs.len(), 2); - - // Case 1: one observer reported every fact. Two derivations, one root. - let roots_of = |sources: &[Source<'_>]| -> BTreeSet { - derivs - .iter() - .flatten() - .map(|f| { - let s = sources - .iter() - .find(|s| s.facts.contains(f)) - .expect("every fact has an observer"); - root(s) - }) - .collect() + let a_branch: &[(u32, u32)] = &[(1, 2), (2, 4), (4, 5)]; + let b_branch: &[(u32, u32)] = &[(1, 3), (3, 4)]; + let b_full: &[(u32, u32)] = &[(1, 3), (3, 4), (4, 5)]; + let src = |o, f| Source { + observer: o, + facts: f, }; - let one = [Source { - observer: A, - facts: DIAMOND, - }]; - assert_eq!(roots_of(&one).len(), 1); - assert_ne!(derivs.len(), roots_of(&one).len()); - - // Case 2: a second observer reported the 1->3->4 branch. The derivations - // are unchanged; the independent evidence is now two roots. - let a_facts: &[(u32, u32)] = &[(1, 2), (2, 4), (4, 5)]; - let b_facts: &[(u32, u32)] = &[(1, 3), (3, 4)]; - let two = [ - Source { - observer: A, - facts: a_facts, - }, - Source { - observer: B, - facts: b_facts, - }, - ]; - assert_eq!(derivations(DIAMOND, 1, 5).len(), 2); - assert_eq!(roots_of(&two).len(), 2); + + // Case 1: one observer reported every fact. Two derivations, one + // environment {A}. + let one = [src(A, DIAMOND)]; + assert_eq!(label(&derivs, &one).len(), 1); + assert_eq!(lineage(&derivs, &one).len(), 1); + + // Case 2: B reported 1->3->4, but 4->5 only A reported. The derivations + // rest on {A} and {A, B}; absorption leaves {A}. Lineage touches two + // roots, yet B never supports path(1, 5) without A: one independent + // support, not two. + let two = [src(A, a_branch), src(B, b_branch)]; + assert_eq!(lineage(&derivs, &two).len(), 2); + let l = label(&derivs, &two); + assert_eq!(l.len(), 1); + assert_eq!(l.iter().next().unwrap().len(), 1); + + // Case 3: B also reported 4->5. Now {A} and {B} each entail path(1, 5) + // on their own and share no root: two independent supports. + let three = [src(A, a_branch), src(B, b_full)]; + let l = label(&derivs, &three); + assert_eq!(l.len(), 2); + assert!(disjoint(&l)); + // Lineage counts two roots in both cases, so it cannot tell them apart. + assert_eq!(lineage(&derivs, &three).len(), 2); + // Two environments that share a root are not independent. + let shared: BTreeSet = [[1u64, 2].into(), [2u64, 3].into()].into(); + assert!(!disjoint(&shared)); } #[test] From da0feb5f8886a375625186d13e90822666b40c4c Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:56:14 +0000 Subject: [PATCH 09/11] xlog-relcomp-probe README: independent support is the minimal-environment label Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/README.md | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/crates/xlog-relcomp-probe/README.md b/crates/xlog-relcomp-probe/README.md index 37413c883..92a94682a 100644 --- a/crates/xlog-relcomp-probe/README.md +++ b/crates/xlog-relcomp-probe/README.md @@ -406,8 +406,14 @@ shortest-path length. (`None`). Evidence and derivations are counted separately: -- On the diamond, `path(1, 5)` has 2 derivations. With one observer they rest on 1 root; with a - second observer reporting one branch, the same 2 derivations rest on 2 roots. +- Independent support is the set of minimal environments of source roots that entail the answer: + the ATMS label, PosBool provenance. Lineage (every root any derivation touches) is a separate, + weaker count. +- On the diamond, `path(1, 5)` has 2 derivations. With one observer they rest on one environment + `{A}`. If B reports `1->3->4` but only A reports `4->5`, the derivations rest on `{A}` and + `{A, B}`; absorption leaves `{A}`, so B adds no independent support, although lineage touches 2 + roots. If B also reports `4->5`, `{A}` and `{B}` are disjoint: 2 independent supports. Lineage is + 2 in both cases. - XLOG's trace and an egglog proof over one register are two consumers with two program hashes and one root: 1 independent observation. @@ -424,4 +430,10 @@ Disable runs for the traceroute and provenance (committed first, one patch at a | root ignores the observer | `reordering_a_report_is_not_a_new_observation` | | a base fact reads as composed | `readings_follow_the_trace_of_the_real_closure`, `provenance_changes_…` | +Disable runs for the minimal-environment label (2026-10-31, after the co-research on the D-STAUNEN +arc found that the first version counted lineage and called it independent support): dropping +absorption, keeping only the first reporter of a fact, `disjoint` always true and `disjoint` always +false each turn `derivation_multiplicity_is_not_independent_evidence` red, at four different +assertions. + One mutant stays green and is equivalent, not a missing test: searching for the last round that holds `(x, y)` instead of the first. Each round's delta excludes everything already derived, so a pair appears in exactly one round. From c295d259cf3b06d368aac09798ba088970b2be72 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:58:42 +0000 Subject: [PATCH 10/11] xlog-relcomp-probe: scope the test-local label as a cold oracle Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- crates/xlog-relcomp-probe/tests/provenance.rs | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/crates/xlog-relcomp-probe/tests/provenance.rs b/crates/xlog-relcomp-probe/tests/provenance.rs index 9be1bf541..f4cf9502a 100644 --- a/crates/xlog-relcomp-probe/tests/provenance.rs +++ b/crates/xlog-relcomp-probe/tests/provenance.rs @@ -5,6 +5,14 @@ //! counted separately from derivation multiplicity: two consumers of one //! root are one independent observation, however many distinct derivations //! the bag algebra holds. +//! +//! Independent support is the set of minimal root environments that entail +//! an answer (an ATMS label, PosBool provenance), not the lineage of roots +//! the derivations touch. `label` and `derivations` here are a cold, test-only +//! oracle over tiny fixtures: they enumerate paths and build owned sets of +//! environments, which the fold never does. They are not a precedent for a +//! label type in a query path; production root-disjoint support belongs to +//! `lance_graph_planner::nars::support::DerivationLedger`. use std::collections::BTreeSet; From 2678550a734fda9c758424a022513cb9276a9599 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 18:59:20 +0000 Subject: [PATCH 11/11] board: co-research map for the D-STAUNEN arc (#1885..#1889) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .../2026-10-31-coresearch-d-staunen-arc.md | 65 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 67 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-31-coresearch-d-staunen-arc.md diff --git a/.claude/board/entries/2026-10-31-coresearch-d-staunen-arc.md b/.claude/board/entries/2026-10-31-coresearch-d-staunen-arc.md new file mode 100644 index 000000000..f0f8e6f11 --- /dev/null +++ b/.claude/board/entries/2026-10-31-coresearch-d-staunen-arc.md @@ -0,0 +1,65 @@ +# Co-research: the D-STAUNEN arc (#1885–#1889) against code and outside sources — 2026-10-31 + +**Status: exploration map. Ratifies nothing.** The operator chooses which probes run. + +## Question +The arc is five docs-only maps (D-STAUNEN-0..4): plasticity as a DT64 capability over Atlas SNN events, HDC signatures, novelty-gated eligibility, XLOG/NSL hypotheses in sparse THOUGHT deltas, and 64-thought metaplasticity with root-disjoint evidence. Which of its gates have their own falsifier run, and what outside knowledge changes which gate to run first? + +Premise gate (premise-auditor): PREMISE-SPLIT. A PR that overlaps a gate is candidate evidence, not admission. X6 splits into X6a (lineage and independent support) and X6b (attribution). HDC and SNN map only onto candidate discovery and novelty modulation, never onto evidence. + +## Gate ledger (code cartographer; file:line in the scratch crosswalk) +- **Falsified by its own gate:** X3 only (lance-graph-nsl oracles, #1846). +- **Partial:** X0, X1, X2 (#1884 bag counts; no forced-overflow test on the checked multiply), X4 (no gradient check), X6 (test-level, #1896), X7, X8. +- **Candidate evidence:** C1, M2. +- **Absent:** C0, C2, C6, X5, M0, M1, M3–M8, A0–A7. For A0–A7 the closed search space was `crates/**/*.rs,*.toml` for brian2, stdp, atlasir, three-factor and eligibility traces. + +## Fixed during the run +#1896's `derivation_multiplicity_is_not_independent_evidence` counted **lineage** (every root any derivation touches) and called it independent evidence. With A reporting 1→2→4→5 and B only 1→3→4, the derivations rest on {A} and {A,B}. Absorption leaves {A}: one independent support, where the test asserted two. + +The test now computes the minimal-environment label (ATMS / PosBool, arXiv 2202.10766 §2–3) for three cases, and keeps lineage as a separate count. Four disables are red, each at a distinct assertion. Commits `9007724`, `da0feb5`, `c295d25`; the last scopes the label as a cold test-only oracle. + +## Verdicts +| # | idea | verdict | why / probe | +|---|---|---|---| +| 1 | Independent support = root-disjoint minimal environments (X6a) | **PROBE** P-X6A-LEDGER | Already in production as `DerivationLedger` (`lance-graph-planner/src/nars/support.rs:308-323`, D-EPI-COT C1/C2). Probe: a plain-text fixture exported by xlog-relcomp-probe, replayed by a planner dev test into the ledger. `pooled` must agree with the probe's label on {A}/{A,B} and on disjoint {A},{B}. On the triangle {A,B},{B,C},{A,C} they **diverge by design**: the label has 3 environments, `pooled` selects 1. The test pins that divergence. The probe crate does not depend on the planner: the probe is a separate workspace because of arrow 60 vs 58, and the planner takes a path ndarray. | +| 1b | Label stable under cycle unrolling | **PROBE** P-X6A-CYCLE (run first) | `derivations()` lists simple paths only, so recursion is unexercised. Fixture: 1→2, 2→3, 3→2, 3→4; A = {1→2, 2→3, 3→4}, B = {3→2}. The label must equal {{A}} for k = 0..3 unrollings. Twin: a bypass 1→5→4 reported by C must give {{A},{C}}, disjoint. Disable: drop minimality. | +| 2 | N[X] is infinite under recursion | **PROBE** P-REC-NO-COUNT | Pin that no API returns a multiplicity for a recursive fact. Twin: the acyclic count is admitted. | +| 3 | One witness is not lineage | **PROBE** P-TRACE-NOT-DISJOINT | On the diamond, `trace` roots == 1 and the `support` label == 2. Twin: a chain. | +| 4 | Truncated proof sets prove overlap only | **PARK** | One-way rule; matters only once a k-truncated proof set exists. The ledger horizon is k = 1. | +| 5 | Retraction under recursion (DRed^c) | **PARK** | Stale frame refused plus recompute is enough until incremental retraction is asked for; a counter store would be a new store. | +| 6 | PROV attribution (X6b) | **ADOPT-NOW (vocabulary)** | Root, version and program hash stay on the test record and fixture header, not a new type. `reading` is an attribute of the result, not provenance. CE64 W never carries it (#1847 :405). | +| 7 | Root = agent or report? | **OPEN, operator** | `root()` hashes observer and facts, so one observer filing two reports counts twice. P-AGENT-VS-REPORT pins both readings once ruled. | +| 8 | Three senses of "provenance" | ADOPT-NOW (vocabulary only) | Attribution (PROV) / lineage-support (semiring) / encoding generation (`EdgeProvenance`). Rename nothing. | +| 9 | Cross-THOUGHT root-disjointness | SKIP (duplicate) | Already D-HL-3 (Queued, falsifier pre-registered; capstone :150). | +| 10 | Replay must not reinforce | SKIP (duplicate) | 2026-10-22 E2/E3/P-M1 and #1847 E1–E7 already cover it. | +| 11 | Novelty gating | PARK | Must inherit D-CE64-STAUNEN-0's kill condition: raw surprise lost to round-robin. | +| 12 | Eligibility traces / delayed credit | PARK | H3 inconclusive under Holm. Traces would make W carry evidence. | +| 13 | HDC/SNN for discovery only | ADOPT-NOW (ruling) | I-VSA-IDENTITIES; ScentLearner #1844 is the surface. Nengo is non-commercial: never a dependency. | +| 14 | Mask-union why-provenance holds only for monotone queries | **PROBE** (cheap) | X-gates over NOT/minus refuse; a test pins the refusal. | +| 15 | Stored N[X]/Why(X) carrier | SKIP (anchor) | 2026-10-21 PARK/SKIP; #1888 forbids a provenance store. | +| 16 | Signed diffs as multiplicity | PARK (lens) | A DD/DDlog engine would be a new engine. The concrete X2 gap is a forced-overflow test on `native.rs:45`: PROBE, cheap. | +| 17 | Kythe ref/call | PROBE (P-KYTHE-CALL) | #1894 emits `ref` only. The probe must start red; call facts need a source (Charon not installed). | +| 18 | egglog proofs | SKIP (resolved) | The PLDI'23 paper calls proofs future work; the fork has `new_with_proofs` and #1896 uses it. | +| 19 | Atlas Definition/Instance/Run identity | PROBE (document check, needs network) | The fetched Atlas README does not mention it. A0–A2 stay parked until it is found at file:line. Brian2 CeCILL-2.1: external oracle only. | +| 20 | NSL neighbour packing | SKIP (anchor) | Copies neighbour features per example (zero copy). Oracle use (#1846) stays. | + +## Recommended order +1. P-X6A-CYCLE +2. P-REC-NO-COUNT and P-TRACE-NOT-DISJOINT (all offline, test-only) +3. P-X6A-LEDGER, which decides whether X6a is already met by the ledger +4. The X2 overflow test + +A-gates wait for P-ATLAS-IDENTITY. M-gates cite D-HL-3 and the 2026-10-22 probes rather than re-plan them. + +## Not searched +- Atlas source tree: only the README was fetched. +- Green et al. 2007, de Kleer 1986, Nieuwenhuis–Oliveras and the Soufflé TOPLAS paper are cited secondhand. +- Miconi 2018's arXiv id is unverified. +- Scallop's licence file was not read. +- The arc's ACT-R, PointCare, qualia and Brain-SoC context was not researched, by design. +- `holograph`, `cognitive-shader-driver/src/serve.rs` and `learning/src/cam_ops.rs` matched eligibility/STDP terms and were not read. + +PR #1896 | STATUS: open | OUTCOME: co-research map for the D-STAUNEN arc; lineage-as-evidence defect fixed | OPEN: root = agent or report; which probes to run + +MIRROR +- BLIND SPOT: #1896's provenance test was reviewed for multiplicity versus roots, but never against a case where a second observer depends on the first. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 4c6d40e7b..a5c1d57b1 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ 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. -527 entries, 2026-08-06 .. 2026-10-31. +528 entries, 2026-08-06 .. 2026-10-31. | date | entry id | finding | file | |---|---|---|---| @@ -40,6 +40,7 @@ exactly one of them, never both. | 2026-10-31 | `D-DT64-6-DR` | | [2026-10-31-d-dt64-6-dr-addressing-module.md](2026-10-31-d-dt64-6-dr-addressing-module.md) | | 2026-10-31 | `D-DYNBAG-X` | | [2026-10-31-cross-frontend-projection-crosswalk.md](2026-10-31-cross-frontend-projection-crosswalk.md) | | 2026-10-31 | `coresearch-mandatory-codegraph` | | [2026-10-31-coresearch-mandatory-codegraph.md](2026-10-31-coresearch-mandatory-codegraph.md) | +| 2026-10-31 | `D-STAUNEN` | | [2026-10-31-coresearch-d-staunen-arc.md](2026-10-31-coresearch-d-staunen-arc.md) | | 2026-10-30 | `D-XLOG-NATIVE-0` | | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) | | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) | | 2026-10-30 | `D-TRACT-SHAPE-1` | | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) |