From 1da25267d9808b7589ff4477cadf10acac5e84fd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:23:37 +0000 Subject: [PATCH 01/11] pearl::retract: lower a certification whose support was withdrawn revise only raises. retract is its counterpart: it re-runs the edge's own operator and lowers the certification to what is still earned, or to Open when the remaining evidence no longer grounds the fold or refutes it. It never raises; SPO/SP and projections with no operator leave the edge as is. The A10 admission probe's F4 now holds: a withdrawn source lowers the code it had supported. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/lance-graph-planner/src/pearl.rs | 121 ++++++++++++++++++ .../tests/a10_admission_probe.rs | 33 ++--- 2 files changed, 138 insertions(+), 16 deletions(-) diff --git a/crates/lance-graph-planner/src/pearl.rs b/crates/lance-graph-planner/src/pearl.rs index b96fe02e3..8c7da0107 100644 --- a/crates/lance-graph-planner/src/pearl.rs +++ b/crates/lance-graph-planner/src/pearl.rs @@ -425,6 +425,40 @@ pub fn revise(m: &Measured, reading: Reading<'_>) -> Result) -> Result { + let edge = m.edge; + let state = reading.project(edge)?; + let current = state.certification(); + let still = match m.operation { + Operation::Association | Operation::Intervention => { + m.earned.unwrap_or(Certification3::Open) + } + Operation::Counterfactual | Operation::ConfounderCheck | Operation::NoOperator(_) => { + return Ok(edge); + } + }; + let next = if still != current && current.entails(still) { + still + } else { + current + }; + Ok(stamp(edge, state.with_certification(next))) +} + /// What a candidate intermediate B turned out to be. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Hydration { @@ -688,6 +722,93 @@ mod tests { ) } + /// Fails if a withdrawn source leaves its certification standing: after + /// one of the two observational sources is withdrawn the fold no longer + /// grounds, and `retract` lowers the edge to `Open`. + #[test] + fn retract_lowers_a_certification_whose_support_was_withdrawn() { + let d = declarations(); + let mut model = related_population().build(); + let e = query( + CausalMask::SO, + Certification3::Open, + Topology2::IndirectKnown, + ); + let ev = Evidence { + model: &model, + chain: None, + }; + let written = revise(&reason(e, &ev, Edit::None), reading(&d)).unwrap(); + assert_eq!(state(written).1, Certification3::Related); + + model + .ledger + .withdraw_source(lance_graph_contract::causal_audit::EvidenceSourceId(1)); + let ev = Evidence { + model: &model, + chain: None, + }; + let m = reason(written, &ev, Edit::None); + assert!(m.ungrounded().is_some()); + let after = retract(&m, reading(&d)).unwrap(); + assert_eq!( + state(after), + (Topology2::IndirectKnown, Certification3::Open) + ); + assert_eq!(after.0 & !EPISTEMIC_MASK, written.0 & !EPISTEMIC_MASK); + } + + /// The silence twin: with the evidence intact, or with only an unrelated + /// source withdrawn, `retract` changes nothing; and it never raises. + #[test] + fn retract_never_raises_and_ignores_unrelated_withdrawals() { + let d = declarations(); + let mut model = related_population().build(); + let e = query( + CausalMask::SO, + Certification3::Related, + Topology2::IndirectKnown, + ); + model + .ledger + .withdraw_source(lance_graph_contract::causal_audit::EvidenceSourceId(99)); + let ev = Evidence { + model: &model, + chain: None, + }; + assert_eq!( + retract(&reason(e, &ev, Edit::None), reading(&d)).unwrap(), + e + ); + + // Earned is stronger than the written code: no raise. + let low = query( + CausalMask::SO, + Certification3::Associated, + Topology2::IndirectKnown, + ); + assert_eq!( + retract(&reason(low, &ev, Edit::None), reading(&d)).unwrap(), + low + ); + + // An operator that earns nothing leaves the edge alone. + let spo = query( + CausalMask::SPO, + Certification3::Causes, + Topology2::IndirectKnown, + ); + let empty = ModelBuilder::new().build(); + let ev = Evidence { + model: &empty, + chain: None, + }; + assert_eq!( + retract(&reason(spo, &ev, Edit::CutStep(0)), reading(&d)).unwrap(), + spo + ); + } + /// The CUI BONO script: the edge leaves with a different state only where /// an operator earned it. #[test] diff --git a/crates/lance-graph-planner/tests/a10_admission_probe.rs b/crates/lance-graph-planner/tests/a10_admission_probe.rs index 0bed80032..d509aceb5 100644 --- a/crates/lance-graph-planner/tests/a10_admission_probe.rs +++ b/crates/lance-graph-planner/tests/a10_admission_probe.rs @@ -22,6 +22,9 @@ //! them goes through an admission check like this one; this probe does not //! change that. //! +//! Retraction (F4) is closed by `pearl::retract`, the lowering counterpart of +//! `pearl::revise`. +//! //! The "Derived never above Related" line is the pre-registered F5 bar //! (`a10-finding.md`): Supports is earned by an observational fold, and a //! formally valid derivation is neither observation nor causal evidence. @@ -457,7 +460,7 @@ fn f2_two_givens_from_different_sources_stay_independent() { // ── F4: retraction ─────────────────────────────────────────────────── #[test] -fn f4_withdrawn_sources_block_new_certification_but_nothing_lowers_the_old() { +fn f4_withdrawn_sources_block_new_certification_and_retract_lowers_the_old() { let d = declarations(); let mut model = observational().build(); let so = edge( @@ -494,21 +497,19 @@ fn f4_withdrawn_sources_block_new_certification_but_nothing_lowers_the_old() { ), Err(Refusal::Ungrounded) ); - // The gap: the code written before the withdrawal stands. No production - // writer lowers a certification when its support is withdrawn. - assert_eq!( - admit( - before, - &Admission::Measured { - edge: before, - evidence: &evidence(&model) - }, - 0, - &d - ), - Err(Refusal::Ungrounded) - ); - assert_ne!(state(before).certification(), Certification3::Open); + // The code written before the withdrawal no longer stands: re-measuring + // with the edge's own operator and `pearl::retract` lowers it to Open. + let ev = evidence(&model); + let m = pearl::reason(before, &ev, Edit::None); + let reading = Reading { + declarations: &d, + class: CLASS, + rail: RAIL, + provenance: EdgeProvenance::V2Stamped, + }; + let after = pearl::retract(&m, reading).expect("declared"); + assert_eq!(state(after).certification(), Certification3::Open); + assert_eq!(state(after).topology(), state(before).topology()); } /// F4 silent twin: withdrawing a source the ledger never held changes From 57512e80a89d079a29a75ca07f48ca570fe2b5b0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:25:35 +0000 Subject: [PATCH 02/11] deepnsm-v2 wire: stop writing CausalCandidate from text wire promoted a Related cause row to CausalCandidate on two independent implication sources, outside pearl and against the contract's own code-4 obligation (Supports plus temporal ordering over a population, which text cannot witness). That made it a second evidence authority. The two-source count stays as a reading (WireReport::two_source_causes, renamed from causal_candidates); the row's certification is no longer raised. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/deepnsm-v2/src/wire.rs | 42 +++++++++++++++++------------------ 1 file changed, 21 insertions(+), 21 deletions(-) diff --git a/crates/deepnsm-v2/src/wire.rs b/crates/deepnsm-v2/src/wire.rs index 242247db3..73afeec77 100644 --- a/crates/deepnsm-v2/src/wire.rs +++ b/crates/deepnsm-v2/src/wire.rs @@ -33,9 +33,12 @@ //! whose clause the Kausal marker (`weil`) opens; every matrix event of the //! same verse is an effect. `Impl` does not auto-transit. //! -//! A cause event is certified `CausalCandidate` only when its `cause ⇒ -//! effect` belief rests on two or more disjoint verse stamps (and the triple -//! itself is Related). Text never certifies `Causes`. The arena's stamps are +//! A cause event whose `cause ⇒ effect` belief rests on two or more disjoint +//! verse stamps is COUNTED (`WireReport::two_source_causes`), never certified +//! above what the text evidence earns: `CausalCandidate` is owned by +//! `lance_graph_contract::certification` and requires `Supports` plus +//! temporal ordering over a population, which text cannot witness. Text never +//! certifies `CausalCandidate` or `Causes`. The arena's stamps are //! a 64-source bitset that folds by modulo: past 64 verses two sources can //! collide, which turns a revision into a CHOICE (an undercount, never a //! double count). @@ -305,8 +308,10 @@ pub struct WireReport { /// Observations not admitted because a group had more than 256 distinct /// verses or objects. pub gate_overflow: usize, - /// Rows certified `CausalCandidate`. - pub causal_candidates: usize, + /// Cause rows whose `cause ⇒ effect` belief rests on two or more disjoint + /// verse stamps (and whose triple is Related). A reading, not a + /// certification: the row's code is not raised. + pub two_source_causes: usize, /// `cause ⇒ effect` observations offered to the causes arena. pub implications: usize, /// Of those, observations the arena pooled (disjoint stamps). @@ -955,7 +960,6 @@ pub fn wire( }; st.last = Some((cohort, slot)); row.cohort = cohort; - // CausalCandidate is decided after the Kausal claims are counted. let certification = if pos >= 2 && balance_pos { Certification3::Related } else { @@ -1022,18 +1026,13 @@ pub fn wire( cause_sources = cause_sources.max(causes.get(stmt).map_or(0, |b| b.stamp.0.count_ones())); } - // Two independent implication sources promote a Related cause. - let row = &mut rows[first + j]; + // Two independent implication sources are counted, never written: + // the certification stays what the text earned. + let row = &rows[first + j]; let state = EpistemicState5::decode(Epi5Gen::V1, row.edge.epistemic_raw5()) .expect("written above as V1"); if cause_sources >= 2 && state.certification() == Certification3::Related { - rep.causal_candidates += 1; - let up = EpistemicState5::new( - Epi5Gen::V1, - state.topology(), - Certification3::CausalCandidate, - ); - row.edge = row.edge.with_epistemic_raw5(up.raw()); + rep.two_source_causes += 1; } } @@ -1639,7 +1638,8 @@ mod tests { /// Can fire: two independent `weil` verses pool `cause ⇒ effect` in the /// causes arena (two disjoint stamps), the cause event sits at the - /// intervention rung and is certified CausalCandidate; the effect is not. + /// intervention rung and is counted as a two-source cause, but its + /// certification stays Related: text never earns CausalCandidate. #[test] fn weil_feeds_the_causes_arena() { let w = run_in(&[weil_verse(), weil_verse()]); @@ -1653,14 +1653,14 @@ mod tests { assert_eq!(row(1, cause).edge.causal_mask(), CausalMask::PO); assert_eq!( epi(row(1, cause).edge).certification(), - Certification3::CausalCandidate + Certification3::Related ); assert_eq!(row(1, effect).edge.causal_mask(), CausalMask::SO); assert_eq!( epi(row(1, effect).edge).certification(), Certification3::Related ); - assert_eq!(w.report.causal_candidates, 1); + assert_eq!(w.report.two_source_causes, 1); } /// Stay silent: the cause clause seen twice, but the causal claim only @@ -1672,7 +1672,7 @@ mod tests { plain.extend(svo(DOG, BIT, MAN)); // The plain verse first, so the weil verse's cause row already has two // supports and a positive balance: only the single implication - // source keeps it from CausalCandidate. + // source keeps it from being counted. let w = run_in(&[ VerseIn { readings: plain, @@ -1682,7 +1682,7 @@ mod tests { ]); assert_eq!(w.report.implications, 1); assert_eq!(w.report.implications_revised, 0); - assert_eq!(w.report.causal_candidates, 0); + assert_eq!(w.report.two_source_causes, 0); let cause = w .rows .iter() @@ -1853,7 +1853,7 @@ mod tests { assert_eq!(cause.revision, Some(RevisionKind::ContradictionPreserved)); assert_eq!(w.report.implications, 0); assert!(w.causes.entries().is_empty()); - assert_eq!(w.report.causal_candidates, 0); + assert_eq!(w.report.two_source_causes, 0); } /// An adjective on the object lands on the object pair; an adverb before From 8b2d8bdd06fcaa2c975456d4c2a7d70a59fd8238 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:26:39 +0000 Subject: [PATCH 03/11] causal-edge: census ratchet for writers of bits 59..63 Every with_epistemic_raw5 call in a crates/*/src file must be classified by file and enclosing function as an AUTHORIZED production writer (pearl's stamp behind revise/retract/hydrate, edge_v3::rehydrate, deepnsm-v2 wire's text reading) or a TEST_FIXTURE. An unclassified call and a stale entry both fail. This is the production admission boundary made enforceable; the test-local A10 admission probe is not promoted. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .../tests/epistemic_writer_census.rs | 198 ++++++++++++++++++ 1 file changed, 198 insertions(+) create mode 100644 crates/causal-edge/tests/epistemic_writer_census.rs diff --git a/crates/causal-edge/tests/epistemic_writer_census.rs b/crates/causal-edge/tests/epistemic_writer_census.rs new file mode 100644 index 000000000..e24c1e130 --- /dev/null +++ b/crates/causal-edge/tests/epistemic_writer_census.rs @@ -0,0 +1,198 @@ +//! The production admission boundary for bits 59..63, as a two-way ratchet. +//! +//! `CausalEdge64::with_epistemic_raw5` is the one physical writer of the +//! `EpistemicState5` field. Every call in a `crates/*/src` file must be +//! classified below, by file and enclosing function: +//! +//! - [`AUTHORIZED`]: a production writer, with what licenses it. +//! - [`TEST_FIXTURES`]: a call inside test code that builds an input. +//! +//! The test fails when a call appears that neither table names, and when a +//! table entry no longer matches any call. Adding a writer is therefore a +//! visible change to this file, never a silent second evidence authority. +//! +//! Scope: calls to `with_epistemic_raw5` in `src/`. Examples and `tests/` +//! directories are lab code and are not scanned. A write that bypasses the +//! method (raw `u64` arithmetic on the edge) is not caught here. + +use std::collections::BTreeSet; +use std::path::{Path, PathBuf}; + +/// `(file relative to crates/, enclosing fn, why it may write)`. +const AUTHORIZED: &[(&str, &str, &str)] = &[ + ( + "lance-graph-planner/src/pearl.rs", + "stamp", + "behind pearl::revise (raise to what an operator earned), pearl::retract (lower to what is still earned) and pearl::hydrate (topology only)", + ), + ( + "causal-edge/src/edge_v3.rs", + "rehydrate", + "restores the existing code on the V3 -> CE64 lift; mints nothing", + ), + ( + "deepnsm-v2/src/wire.rs", + "wire", + "text reading: Associated or Related from independent verse support; never CausalCandidate or Causes", + ), +]; + +/// `(file relative to crates/, enclosing fn)` of test-only calls. +const TEST_FIXTURES: &[(&str, &str)] = &[ + ( + "causal-edge/src/v2_layout_tests.rs", + "every_code_round_trips_and_touches_only_59_63", + ), + ( + "causal-edge/src/v2_layout_tests.rs", + "joint_write_replaces_both_halves", + ), + ( + "causal-edge/src/v2_layout_tests.rs", + "the_field_survives_the_le_image", + ), + ( + "causal-edge/src/v2_layout_tests.rs", + "the_topology_writer_is_a_factor_update_and_the_band_writer_is_not_canonical", + ), + ( + "causal-edge/src/edge_v3.rs", + "the_lift_preserves_the_joint_epistemic_code", + ), + ( + "lance-graph-planner/src/chain_counterfactual.rs", + "the_role_reports_the_cut_edges_own_coordinate_not_a_bare_boolean", + ), + ("lance-graph-planner/src/nars/scent_learn.rs", "edge"), + ("lance-graph-planner/src/nars/scent.rs", "edge"), + ("lance-graph-planner/src/nars/mediator.rs", "edge"), + ( + "lance-graph-planner/src/nars/warrant.rs", + "a_judgment_is_never_promoted_by_its_premises", + ), +]; + +fn crates_dir() -> PathBuf { + Path::new(env!("CARGO_MANIFEST_DIR")) + .parent() + .expect("crates/") + .to_path_buf() +} + +fn rust_files(dir: &Path, out: &mut Vec) { + let Ok(entries) = std::fs::read_dir(dir) else { + return; + }; + for e in entries.flatten() { + let p = e.path(); + if p.is_dir() { + if p.file_name().is_some_and(|n| n == "target") { + continue; + } + rust_files(&p, out); + } else if p.extension().is_some_and(|x| x == "rs") { + out.push(p); + } + } +} + +/// The name in the nearest `fn name` line at or above `line`. +fn enclosing_fn(lines: &[&str], line: usize) -> String { + for l in lines[..=line].iter().rev() { + let t = l.trim_start(); + if let Some(i) = t.find("fn ") { + let before = &t[..i]; + if before.is_empty() || before.ends_with(' ') { + let rest = &t[i + 3..]; + let name: String = rest + .chars() + .take_while(|c| c.is_alphanumeric() || *c == '_') + .collect(); + if !name.is_empty() { + return name; + } + } + } + } + String::new() +} + +/// Every `(file, enclosing fn)` that calls `with_epistemic_raw5` in a +/// `crates/*/src` file, excluding comments and the method's definitions. +fn call_sites() -> BTreeSet<(String, String)> { + let root = crates_dir(); + let mut files = Vec::new(); + for krate in std::fs::read_dir(&root).expect("crates/").flatten() { + rust_files(&krate.path().join("src"), &mut files); + } + let mut out = BTreeSet::new(); + for f in files { + let text = std::fs::read_to_string(&f).expect("read source"); + let lines: Vec<&str> = text.lines().collect(); + for (i, l) in lines.iter().enumerate() { + let t = l.trim_start(); + if t.starts_with("//") || !t.contains("with_epistemic_raw5(") { + continue; + } + if t.contains("fn with_epistemic_raw5") { + continue; + } + let rel = f + .strip_prefix(&root) + .expect("under crates/") + .to_string_lossy() + .replace('\\', "/"); + out.insert((rel, enclosing_fn(&lines, i))); + } + } + out +} + +fn classified() -> BTreeSet<(String, String)> { + AUTHORIZED + .iter() + .map(|(f, n, _)| ((*f).to_string(), (*n).to_string())) + .chain( + TEST_FIXTURES + .iter() + .map(|(f, n)| ((*f).to_string(), (*n).to_string())), + ) + .collect() +} + +#[test] +fn every_epistemic_writer_is_classified() { + let found = call_sites(); + let known = classified(); + let unknown: Vec<_> = found.difference(&known).collect(); + assert!( + unknown.is_empty(), + "with_epistemic_raw5 called outside the census; add it to AUTHORIZED \ + (with what licenses it) or TEST_FIXTURES: {unknown:?}" + ); +} + +#[test] +fn every_census_entry_still_exists() { + let found = call_sites(); + let known = classified(); + let stale: Vec<_> = known.difference(&found).collect(); + assert!( + stale.is_empty(), + "census entries with no matching call; remove them: {stale:?}" + ); +} + +/// Anti-vacuity: the scan finds the authorized writers, so an empty scan +/// (wrong root, renamed method) cannot pass both directions at once. +#[test] +fn the_scan_finds_the_authorized_writers() { + let found = call_sites(); + for (f, n, _) in AUTHORIZED { + assert!( + found.contains(&((*f).to_string(), (*n).to_string())), + "{f}::{n} not found by the scan" + ); + } + assert!(found.len() >= AUTHORIZED.len() + TEST_FIXTURES.len()); +} From 8893506819a5ba660b604a1c5cf5b2b564cdea92 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:27:34 +0000 Subject: [PATCH 04/11] A10 probe: NAL derivations name their rule with contract::nars::InferenceType The rule-identity stand-in is replaced by the existing owner for NAL figures. Only derivations with no owner (elimination, constraint propagation) keep a test-local stand-in, DerivationRule::Unowned, which is the remaining gap. The probe's docs now point at the production writer census instead of describing the boundary as unenforced. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .../tests/a10_admission_probe.rs | 62 ++++++++++++------- 1 file changed, 39 insertions(+), 23 deletions(-) diff --git a/crates/lance-graph-planner/tests/a10_admission_probe.rs b/crates/lance-graph-planner/tests/a10_admission_probe.rs index d509aceb5..6a465fd2f 100644 --- a/crates/lance-graph-planner/tests/a10_admission_probe.rs +++ b/crates/lance-graph-planner/tests/a10_admission_probe.rs @@ -11,15 +11,22 @@ //! | Derived | a rule identity, premises, inherited roots only | `GadamerRevision` (inherited roots never count as new) | min of the premises, never above Related | //! | Measured | an executed operator result | `pearl::reason` + `pearl::revise` | what the operator earned (SO ≤ CausalCandidate; only PO reaches Causes) | //! -//! Two gaps are explicit, not papered over: +//! Rule identity reuses its existing owner where one exists: //! -//! - **Rule identity.** No contract type carries the identity of a -//! derivation rule. [`RuleIdentityGap`] stands in for it here, and a -//! derivation without one is refused. -//! - **The production admission boundary.** Production code writes bits -//! 59..63 through `pearl::revise` / `pearl::hydrate`, `edge_v3::rehydrate` -//! (a restore) and `deepnsm_v2::wire` (its own observational rule). None of -//! them goes through an admission check like this one; this probe does not +//! - **NAL derivations** name their rule with +//! `lance_graph_contract::nars::InferenceType` (Deduction, Induction, +//! Abduction, Revision, Synthesis). +//! - **Derivations outside NAL** (elimination, constraint propagation) have +//! no owner. [`DerivationRule::Unowned`] stands in for them here; that +//! variant is the remaining gap. +//! +//! A derivation with no rule at all is refused. +//! +//! The production boundary is enforced separately: every production call of +//! `with_epistemic_raw5` must be listed in `causal-edge`'s +//! `tests/epistemic_writer_census.rs` (pearl's `stamp`, `edge_v3::rehydrate`, +//! `deepnsm_v2::wire`). None of them goes through an admission check like +//! this one; this probe does not //! change that. //! //! Retraction (F4) is closed by `pearl::retract`, the lowering counterpart of @@ -38,6 +45,7 @@ use lance_graph_contract::class_view::ClassId; use lance_graph_contract::epistemic_state5::{ Certification3, Epi5Declarations, Epi5Gen, Epi5Reading, EpistemicState5, Topology2, }; +use lance_graph_contract::nars::InferenceType as NalRule; use lance_graph_contract::rail_geometry::RailAxis; use lance_graph_contract::revision::{ BasisView, CodebookId, EncounterEvidence, EvidentialEffect, GadamerRevision, GrammarId, @@ -48,10 +56,15 @@ use lance_graph_planner::pearl::{self, Edit, Evidence, Reading}; const CLASS: ClassId = 0x0902; const RAIL: RailAxis = RailAxis::Taxonomy; -/// Stand-in for the missing rule-identity carrier. Its existence here is the -/// gap: no contract type names which rule produced a derivation. +/// Which rule produced a derivation. #[derive(Clone, Copy)] -struct RuleIdentityGap(#[allow(dead_code)] u32); +enum DerivationRule { + /// A NAL figure, named by its existing owner. + Nal(#[allow(dead_code)] NalRule), + /// A rule with no owner (elimination, constraint propagation). Test-local + /// stand-in: no contract type names these yet. + Unowned(#[allow(dead_code)] u32), +} #[derive(Clone, Copy)] enum GivenProof { @@ -70,7 +83,7 @@ enum Admission<'a> { roots: u64, }, Derived { - rule: Option, + rule: Option, premises: &'a [EpistemicState5], inherited: u64, independent: u64, @@ -86,7 +99,7 @@ enum Refusal { Unidentified, NoNewRoot, MintsRoot, - RuleIdentityGap, + NoRule, NoPremises, Ungrounded, } @@ -187,7 +200,7 @@ fn admit( independent, } => { if rule.is_none() { - return Err(Refusal::RuleIdentityGap); + return Err(Refusal::NoRule); } if *independent != 0 { return Err(Refusal::MintsRoot); @@ -317,11 +330,14 @@ fn a_derivation_without_rule_identity_is_refused() { inherited: 0b110, independent: 0, }; - assert_eq!( - admit(e, &derived(None), 0, &d), - Err(Refusal::RuleIdentityGap) - ); - assert!(admit(e, &derived(Some(RuleIdentityGap(7))), 0, &d).is_ok()); + assert_eq!(admit(e, &derived(None), 0, &d), Err(Refusal::NoRule)); + assert!(admit( + e, + &derived(Some(DerivationRule::Nal(NalRule::Deduction))), + 0, + &d + ) + .is_ok()); } #[test] @@ -330,7 +346,7 @@ fn a_derivation_cannot_mint_an_independent_root() { let e = edge(CausalMask::SO, at(Topology2::Direct, Certification3::Open)); let premises = [at(Topology2::Direct, Certification3::Related)]; let a = Admission::Derived { - rule: Some(RuleIdentityGap(7)), + rule: Some(DerivationRule::Nal(NalRule::Deduction)), premises: &premises, inherited: 0b110, independent: 0b1000, @@ -354,7 +370,7 @@ fn f5_a_derivation_from_causal_premises_stays_below_causal() { let out = admit( e, &Admission::Derived { - rule: Some(RuleIdentityGap(1)), + rule: Some(DerivationRule::Nal(NalRule::Deduction)), premises: &causes, inherited: 0b11, independent: 0, @@ -427,7 +443,7 @@ fn f2_ruling_out_rivals_does_not_raise_the_survivors_certification() { at(Topology2::Direct, Certification3::Associated), ); let elim = Admission::Derived { - rule: Some(RuleIdentityGap(9)), + rule: Some(DerivationRule::Unowned(9)), premises: &constraints, inherited: 0xFF, independent: 0, @@ -436,7 +452,7 @@ fn f2_ruling_out_rivals_does_not_raise_the_survivors_certification() { assert_eq!(state(once).certification(), Certification3::Related); // The derived cell may not carry a root of its own. let minted = Admission::Derived { - rule: Some(RuleIdentityGap(9)), + rule: Some(DerivationRule::Unowned(9)), premises: &constraints, inherited: 0xFF, independent: 0x100, From 3253d1f2b69cb3fcba7252ae67aa5444a49e7b1f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:33:03 +0000 Subject: [PATCH 05/11] board: retraction, wire, writer census, rule identity, reach/far, B3 deferral Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .claude/board/STATUS_BOARD.md | 2 +- .../2026-11-03-a10-writers-retract-xlog-pr.md | 28 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 3 files changed, 31 insertions(+), 2 deletions(-) create mode 100644 .claude/board/entries/2026-11-03-a10-writers-retract-xlog-pr.md diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index b14ca8536..5f94baf3f 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -241,7 +241,7 @@ Plan: [d-codegraph-0-resident-codegraph-v1.md](../plans/d-codegraph-0-resident-c | **D-CODEGRAPH-0-B** | resident rows via the ruff sink; per-file digests; incremental invalidation | LANDED (offline form): ruff #130 (merged `95be2e480b`; offline store in `ruff_charon`; `RefinedTruthSink` not reused, typed to R2IL). Incremental == clean on the fixture, byte-identical; skipped dependent leaves exactly one dangling edge. Follow-up fixes in ruff #131 (open). Lance-graph SoA residency still open | clean import == incremental import | | **D-CODEGRAPH-0-C** | callers / callees / impact / diagnostics; tiled closure; body → R2IL design check | SHIPPED (fixture scale): ruff #132 (merged `ed8fd4194f`, rows v2) + lance-graph #1921 (merged `4ab93bf3e`), `crates/lance-graph-codegraph` (queries as confirmed / possible / unknown masks over the xlog cube; dead function, unresolved call, dangling call; unused import NOT_RUN). 27 tests, 12 disable runs red. Tiled closure deferred: refusals `ClosureWidth` (> 64) and `TooMany` (> 256) are surfaced as typed UNKNOWN | each guard disable-verified; unused import proven only without macros, traits, globs, re-exports | | **D-CODEGRAPH-0-C2** | wide closure (multi-word rows, block presence), multi-tile cube, merge-on-read refresh, interned lanes | SHIPPED: #1923 (merged `2e19a5adc`). Impact over any size; mask-risc store (695 symbols, 3 tiles): impact 286 ns, callers 29 µs, references 45 µs; refresh of an unchanged crate 1.5–1.7 ms = FAILED gate (reading the 2.5 MB text file), fixed by D-CODEGRAPH-0-BIN. `refresh_crate` atomic (prepare → validate → commit: staged interner, positions, tile map, `Cube::stage`, closure; commit has no error path); codegraph suites now in `rust-test.yml` | narrow vs wide bit-identical ≤ 64; BFS reference on 694 positions; refresh == clean open; a refused refresh changes nothing (NeedsReopen, injected stage and closure refusals; no version issued); retry == the refresh that never failed, call-site multiplicity included; 7 disable runs red | -| **D-CODEGRAPH-0-BIN** | ruff_charon binary row lanes + header digest; codec9 small codebooks; Quack counting; no strings in the hot path; provenance header + per-row `(artifact, FunDeclId)`; `INVOKES_WORD` to a registered DT64 word | PLATEAU (operator 2026-11-02): reader merged as lance-graph #1929 `4fadef69d` — rows.bin intake + header-only unchanged refresh 2.58 µs (met); changed-crate 2.5 ms vs ≤1 ms gate NOT met (`Symbols::intern` 2.04 ms) → B3 interner open, then re-run gate; F7 Quack counting open. WRITER SHIPPED: ruff #133 merged `6c3d1bf8da` (follow-up ruff #134: stale `rows.tsv` removed when export is off; section offsets past 4 GiB refused, both from Codex review); reader PR B unblocked. ruff #133 `ruff_charon` `store_bin.rs` + `Store` wiring — format §2 + PROV/FUNDECL/OBJ_KIND (ARTREF elided, one artifact), verifying reader with one refusal per shape, golden `cg_lib.rows.bin`; 32 new tests, 6 disables red; TSV export stays ON by default until PR B (lance-graph reader) lands, then flips; `INVOKES_WORD` still OPEN (association source). Plan `d-codegraph-0-binary-lanes-v1.md` (operator: graph-wide u32 ids, TSV kept as debug `open_tsv`; Amendment A §8: PROV section, FUNDECL/ARTREF lanes, `INVOKES_WORD`, F9–F12). Ruff writer PR first, then the codegraph reader. OPEN: source of the "function realises word" association | unchanged refresh ≤ 20 µs; changed-crate open ≤ 1 ms; binary == TSV row for row | +| **D-CODEGRAPH-0-BIN** | ruff_charon binary row lanes + header digest; codec9 small codebooks; Quack counting; no strings in the hot path; provenance header + per-row `(artifact, FunDeclId)`; `INVOKES_WORD` to a registered DT64 word | DEFERRED (operator 2026-11-03): B3 waits until strings are outside the hot path and the XLOG wiring-gap list (6+ gaps, the polyfill among them) has reached the hot path; any remaining string is taken off at the codebook label ("wardrobe"). PLATEAU (operator 2026-11-02): reader merged as lance-graph #1929 `4fadef69d` — rows.bin intake + header-only unchanged refresh 2.58 µs (met); changed-crate 2.5 ms vs ≤1 ms gate NOT met (`Symbols::intern` 2.04 ms) → B3 interner open, then re-run gate; F7 Quack counting open. WRITER SHIPPED: ruff #133 merged `6c3d1bf8da` (follow-up ruff #134: stale `rows.tsv` removed when export is off; section offsets past 4 GiB refused, both from Codex review); reader PR B unblocked. ruff #133 `ruff_charon` `store_bin.rs` + `Store` wiring — format §2 + PROV/FUNDECL/OBJ_KIND (ARTREF elided, one artifact), verifying reader with one refusal per shape, golden `cg_lib.rows.bin`; 32 new tests, 6 disables red; TSV export stays ON by default until PR B (lance-graph reader) lands, then flips; `INVOKES_WORD` still OPEN (association source). Plan `d-codegraph-0-binary-lanes-v1.md` (operator: graph-wide u32 ids, TSV kept as debug `open_tsv`; Amendment A §8: PROV section, FUNDECL/ARTREF lanes, `INVOKES_WORD`, F9–F12). Ruff writer PR first, then the codegraph reader. OPEN: source of the "function realises word" association | unchanged refresh ≤ 20 µs; changed-crate open ≤ 1 ms; binary == TSV row for row | | **D-TGL-0** | GitHub-analogue Thought-Git lifecycle as a shared contract (branch → change → diff → PR → checks → review → rebase/squash → land → receipt/replay; rework / discard) for Codegraph, DT64, XLOG | CONTRACT (docs): plan `thought-git-lifecycle-contract-v1.md`; PR states are readings of existing records, no workflow engine | each step expressible with listed primitives | | **D-TGL-LAB** | Codegraph lab: F-LAND / F-DISCARD | SHIPPED (lab, crate-private): `prepare_refresh` / `commit_refresh` with a generation fence (`RefreshRefusal::Stale`); second branch recomputed against current W0 == clean open incl. call-site counts; discard leaves W0 unchanged; 2 disables red (without the fence only a `debug_assert` catches the collision) | not a production land | | **D-TGL-G8** | bag semantics: merge source revisions, never raw edge ADDs | DECIDED (contract §4) | 5 call sites from two sources after both land (F-LAND) | diff --git a/.claude/board/entries/2026-11-03-a10-writers-retract-xlog-pr.md b/.claude/board/entries/2026-11-03-a10-writers-retract-xlog-pr.md new file mode 100644 index 000000000..233cadaaf --- /dev/null +++ b/.claude/board/entries/2026-11-03-a10-writers-retract-xlog-pr.md @@ -0,0 +1,28 @@ +# Epistemic writers, retraction, rule identity, and the reach/far run (2026-11-03) + +**Status:** implemented in lance-graph (this PR). The XLOG fork change is in fork PR #7; runtime acceptance is still missing. The NNUE optimizer switch is blocked. + +## What changed + +- **Retraction (F4 closed).** `pearl::retract` is the counterpart of `pearl::revise`: it re-runs the edge's own operator and lowers the certification to what is still earned, or to Open when the remaining evidence no longer grounds the fold. It never raises; SPO/SP and projections without an operator leave the edge unchanged. The A10 probe's F4 now holds. Two disables turn it red: a no-op retract, and a retract without the never-raise check. +- **No second evidence authority.** `deepnsm_v2::wire` no longer writes CausalCandidate. The contract's obligation for code 4 is Supports plus temporal ordering over a population, and text cannot witness that. The two-source count stays a reading, `WireReport::two_source_causes`. Two disables turn the test red: restoring the promotion, and dropping the count. +- **Production writer boundary.** `causal-edge/tests/epistemic_writer_census.rs` classifies every `with_epistemic_raw5` call in `crates/*/src` by file and enclosing function. The three AUTHORIZED writers are pearl's `stamp` (behind revise / retract / hydrate), `edge_v3::rehydrate` and `deepnsm_v2::wire`; everything else is a TEST_FIXTURE. An unclassified call and a stale entry both fail; the first run, with guessed names, failed in both directions. The test-local admission probe stays test-local: per the A10 ruling it is not promoted before validity survives the publication and read boundary. +- **Rule identity.** NAL derivations name their rule with the existing owner `lance_graph_contract::nars::InferenceType`. Derivations outside NAL (elimination, constraint propagation) have no owner; the probe keeps `DerivationRule::Unowned` for them, and that is the remaining gap. + +## XLOG fork: reach/far + +- Fork PR AdaWorldAPI/xlog#7 is commit `ea924b3`. The integration request goes to the lead; the PR is not the integration. +- A local run outside the fork tree went through `parse_program`, `rewrite_magic_sets` and `compile`: + - on fork `main`, reach/far is `Applied` (the hazard); + - at `ea924b3`, `on` refuses ("rule for far reads magic_sets target reach outside the demanded queries") and `auto` declines with no magic relations in the plan; + - without `far`, both modes still apply. +- The fork's AGENTS.md excludes local component experiments, so this run is an observation, not runtime evidence. The authorized run on the production path (RunPod GPU) has not been done. The runner was deleted. + +## NNUE + +- **Exact-degree pairing in the fork optimizer: BLOCKED.** xlog-stats keeps only per-column summaries (`PrefixDegreeStats`: average and maximum degree), and no production code feeds even those; the only caller of `add_prefix_degree` is `wcoj_phase_report`, with hardcoded values. The exact fold needs a per-key degree statistic and a producer on the runtime insert path. That is an XLOG wiring gap and belongs on the XLOG wiring-gap list, not in a blind optimizer change. +- **Second application:** the outcome table now exists on the consumer side, outside this repository. The measured baseline still needs per-round method counts re-derived from harvests. + +## Deferral recorded + +D-CODEGRAPH-0-BIN B3 (the interner) is DEFERRED until strings are outside the hot path and the XLOG wiring-gap list (6+ gaps, the polyfill among them) has reached the hot path. Any remaining string is taken off at the codebook label ("wardrobe"). The STATUS_BOARD row carries this. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index e10dbcc19..caa886ffc 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. -557 entries, 2026-08-06 .. 2026-11-02. +558 entries, 2026-08-06 .. 2026-11-03. | date | entry id | finding | file | |---|---|---|---| +| 2026-11-03 | `a10-writers-retract-xlog-pr` | | [2026-11-03-a10-writers-retract-xlog-pr.md](2026-11-03-a10-writers-retract-xlog-pr.md) | | 2026-11-02 | `sgr-recovery-gates` | | [2026-11-02-sgr-recovery-gates.md](2026-11-02-sgr-recovery-gates.md) | | 2026-11-02 | `p4-thought-git-codegraph-dt64-review` | | [2026-11-02-p4-thought-git-codegraph-dt64-review.md](2026-11-02-p4-thought-git-codegraph-dt64-review.md) | | 2026-11-02 | `p4-operator-decisions-lifecycle-lab` | | [2026-11-02-p4-operator-decisions-lifecycle-lab.md](2026-11-02-p4-operator-decisions-lifecycle-lab.md) | From 342ca0357960e26b9716df3c63b8d2a1eefea02b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:36:31 +0000 Subject: [PATCH 06/11] egglog-r2il: no name reaches execution Step::PushVar(String) made run_steps resolve a variable by string comparison on every execution. Only the target may be read, so lowering now resolves each variable once: the target becomes Step::PushInput (no name) and any other variable is refused at lowering as UnboundVar. run_steps takes the input value and reads no string; Step is Copy. The variable's name lives only in the cold traceroute (Step::mnemonic_with). Closes the PARK I3 item of the XLOG archaeology map (PushVar(String) -> resolved at lowering). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- crates/egglog-r2il-probe/src/artifact.rs | 7 +- crates/egglog-r2il-probe/src/heritage.rs | 2 +- crates/egglog-r2il-probe/src/lower.rs | 81 +++++++++++++----------- crates/egglog-r2il-probe/src/trace.rs | 13 +++- crates/egglog-r2il-probe/tests/e1.rs | 17 +++++ 5 files changed, 74 insertions(+), 46 deletions(-) diff --git a/crates/egglog-r2il-probe/src/artifact.rs b/crates/egglog-r2il-probe/src/artifact.rs index 955ee6f73..c59818672 100644 --- a/crates/egglog-r2il-probe/src/artifact.rs +++ b/crates/egglog-r2il-probe/src/artifact.rs @@ -130,12 +130,7 @@ impl ReplayCapsule { /// Hot-compatible execution: no egglog and no oracle. This requires /// *prior* certification and must not be confused with proof checking. pub fn execute(&self, target_value: i64) -> Result { - run_steps( - &self.program, - self.problem.target_var, - &[(self.problem.target_var, target_value)], - ) - .map_err(ReplayRefusal::Execution) + run_steps(&self.program, target_value).map_err(ReplayRefusal::Execution) } /// Cold replay with re-certification and independent i128 value oracle. diff --git a/crates/egglog-r2il-probe/src/heritage.rs b/crates/egglog-r2il-probe/src/heritage.rs index c02b885b6..56c41656c 100644 --- a/crates/egglog-r2il-probe/src/heritage.rs +++ b/crates/egglog-r2il-probe/src/heritage.rs @@ -199,7 +199,7 @@ pub fn analyse(corpus: &[HeritageEntry]) -> MetaStudy { Step::PushConst(_) => { atoms.insert(Atom27::Const); } - Step::PushVar(_) => { + Step::PushInput => { atoms.insert(Atom27::Var); } Step::IntMult => { diff --git a/crates/egglog-r2il-probe/src/lower.rs b/crates/egglog-r2il-probe/src/lower.rs index cc3bf444b..0521242b0 100644 --- a/crates/egglog-r2il-probe/src/lower.rs +++ b/crates/egglog-r2il-probe/src/lower.rs @@ -10,6 +10,13 @@ //! 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. +//! +//! No name reaches execution. Only the target variable may be read, so +//! lowering resolves every variable once: the target becomes +//! [`Step::PushInput`], and any other variable is refused there, at lowering, +//! as [`LowerRefusal::UnboundVar`]. [`run_steps`] takes the input value and +//! reads no string. The variable's name lives only in the cold traceroute +//! ([`Step::mnemonic_with`]). use lance_graph_contract::set_rules::Arith; use lance_graph_mask_risc::{Foreign, Planes}; @@ -20,44 +27,54 @@ 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)] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum Step { /// `push k`: a literal scalar. PushConst(i64), - /// Push the supplied value of the named variable. - PushVar(String), + /// Push the input: the target variable's value. Resolved at lowering; + /// carries no name. + PushInput, /// `call INT_MULT` on the top two scalars. IntMult, } impl Step { - /// Mnemonic for the traceroute. + /// Mnemonic for the traceroute, with the input shown as `$input`. pub fn mnemonic(&self) -> String { + self.mnemonic_with("input") + } + + /// Mnemonic with the input shown under `label` (the target's name). Cold: + /// only the traceroute reads it. + pub fn mnemonic_with(&self, label: &str) -> String { match self { Step::PushConst(k) => format!("push {k}"), - Step::PushVar(v) => format!("push ${v}"), + Step::PushInput => format!("push ${label}"), 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 { +/// Post-order walk: `Num k` pushes, the target pushes the input, `Mul l r` +/// is `l; r; INT_MULT`. Any other variable is refused. +pub fn steps_of(tm: &Tm, target_var: &str) -> Result, LowerRefusal> { let mut out = Vec::new(); - walk(tm, &mut out); - out + walk(tm, target_var, &mut out)?; + Ok(out) } -fn walk(tm: &Tm, out: &mut Vec) { +fn walk(tm: &Tm, target_var: &str, out: &mut Vec) -> Result<(), LowerRefusal> { match tm { Tm::Num(k) => out.push(Step::PushConst(*k)), - Tm::Var(v) | Tm::Def(v) => out.push(Step::PushVar(v.clone())), + Tm::Var(v) | Tm::Def(v) if v == target_var => out.push(Step::PushInput), + Tm::Var(v) | Tm::Def(v) => return Err(LowerRefusal::UnboundVar(v.clone())), Tm::Mul(l, r) => { - walk(l, out); - walk(r, out); + walk(l, target_var, out)?; + walk(r, target_var, out)?; out.push(Step::IntMult); } } + Ok(()) } /// The call sequence for the compiled problem's extracted term. Refuses a @@ -71,22 +88,27 @@ pub fn lower_steps(c: &Compiled) -> Result, LowerRefusal> { let tm = Tm::parse(&c.extracted).ok_or(LowerRefusal::NotLowerable( "extracted term is not parseable", ))?; - Ok(steps_of(&tm)) + steps_of(&tm, c.target_var) } /// Lowers and executes. `inputs` supplies values by variable name; only -/// `c.target_var` may be read, any other variable is `UnboundVar`. +/// `c.target_var` may be read, any other variable is `UnboundVar` (refused at +/// lowering). The name lookup happens here, once, before execution. pub fn lower_and_run(c: &Compiled, inputs: &[(&str, i64)]) -> Result { let steps = lower_steps(c)?; - run_steps(&steps, c.target_var, inputs) + let input = inputs + .iter() + .find(|(n, _)| *n == c.target_var) + .map(|(_, x)| *x); + match (steps.contains(&Step::PushInput), input) { + (true, None) => Err(LowerRefusal::UnboundVar(c.target_var.to_string())), + (_, x) => run_steps(&steps, x.unwrap_or(0)), + } } -/// Executes a step list on a scalar-only `FoldDialect`. -pub fn run_steps( - steps: &[Step], - target_var: &str, - inputs: &[(&str, i64)], -) -> Result { +/// Executes a step list on a scalar-only `FoldDialect`. `input` is the value +/// [`Step::PushInput`] pushes. No name is read. +pub fn run_steps(steps: &[Step], input: i64) -> Result { let planes = Planes { n_rows: 0, masks: &[], @@ -97,20 +119,7 @@ pub fn run_steps( 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::PushInput => stack.push(Val::Scalar(input)), 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 { diff --git a/crates/egglog-r2il-probe/src/trace.rs b/crates/egglog-r2il-probe/src/trace.rs index e5c87850e..2ec67943c 100644 --- a/crates/egglog-r2il-probe/src/trace.rs +++ b/crates/egglog-r2il-probe/src/trace.rs @@ -5,7 +5,7 @@ use std::fmt; -use crate::lower::{Step, lower_steps, run_steps}; +use crate::lower::{lower_steps, run_steps}; use crate::{Arith, LowerRefusal, Problem, Saturation, compile, oracle}; /// The hop labels, in order. @@ -125,12 +125,19 @@ pub fn traceroute(p: &Problem, arith: Arith, fuel: usize, c: i64) -> Trace { push( "R2IL", match &steps { - Ok(s) => s.iter().map(Step::mnemonic).collect::>().join(", "), + Ok(s) => s + .iter() + .map(|step| step.mnemonic_with(compiled.target_var)) + .collect::>() + .join(", "), Err(e) => format!("refused: {e:?}"), }, ); let value: Result = match &steps { - Ok(s) => run_steps(s, compiled.target_var, &[(p.target_var, c)]), + // The traceroute's input is supplied under the problem's target name; + // it is the compiled program's input only when the two names agree. + Ok(s) if p.target_var == compiled.target_var => run_steps(s, c), + Ok(_) => Err(LowerRefusal::UnboundVar(compiled.target_var.to_string())), Err(e) => Err(e.clone()), }; push( diff --git a/crates/egglog-r2il-probe/tests/e1.rs b/crates/egglog-r2il-probe/tests/e1.rs index 876d30a2e..bcb06daf0 100644 --- a/crates/egglog-r2il-probe/tests/e1.rs +++ b/crates/egglog-r2il-probe/tests/e1.rs @@ -125,6 +125,12 @@ fn missing_premise_refuses() { } other => panic!("expected UnboundVar, got {other:?} for {}", c.extracted), } + // The refusal happens at lowering, before any execution: no step list + // that reads a name is ever produced. + assert!( + matches!(lower_steps(&c), Err(LowerRefusal::UnboundVar(_))), + "a non-target variable must be refused at lowering" + ); assert_eq!(oracle::solve(&p, 7), None); assert_eq!( traceroute(&p, Arith::Exact, 8, 7).verdict, @@ -248,3 +254,14 @@ fn traceroute_names_every_hop() { } assert_eq!(t.verdict, Verdict::Agree); } + +/// FAILS IF: a lowered step can carry text. `Step` being `Copy` rules out a +/// `String` (or any heap name) inside it, so execution reads no name. +#[test] +fn lowered_steps_carry_no_text() { + fn copy() {} + copy::(); + let c = compile(&e1_problem(), Arith::Exact, 8); + let steps = lower_steps(&c).expect("lowerable"); + assert!(steps.contains(&Step::PushInput), "{steps:?}"); +} From 3c8c9860882e970334f8efbc7bcceaa7135c2157 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 00:39:11 +0000 Subject: [PATCH 07/11] plan: XLOG wiring gaps to the hot path (D-XLOG-WIRE), the B3 gating list Eight gaps W1-W8, each re-verified at the AdaWorldAPI/xlog main 84da1a8 or found in code: magic report dropped, polarity dropped, estimates discarded, no degree-statistic producer, dormant RirNode::Fixpoint, semi-naive without one owner, XLOG_LENS F100 never executed, competing plan identities. Includes the text-on-hot-path table (egglog-r2il fixed; the codegraph interner is B3). W5 and W7 need operator decisions. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .claude/board/INTEGRATION_PLANS.md | 5 ++ .claude/board/STATUS_BOARD.md | 1 + .claude/plans/xlog-wiring-to-hot-path-v1.md | 80 +++++++++++++++++++++ 3 files changed, 86 insertions(+) create mode 100644 .claude/plans/xlog-wiring-to-hot-path-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 994846357..6a337cee3 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,8 @@ +## 2026-11-03 — D-XLOG-WIRE: XLOG wiring gaps to the hot path → `.claude/plans/xlog-wiring-to-hot-path-v1.md` + +**Status:** PLAN. Gating input for D-CODEGRAPH-0-BIN B3 (operator 2026-11-03). **Board:** [STATUS_BOARD](STATUS_BOARD.md) D-XLOG-WIRE; [entry](entries/2026-11-03-a10-writers-retract-xlog-pr.md). +**Confidence:** eight gaps W1–W8, each re-verified at the fork `main` `84da1a8` or found in code on 2026-11-03; no wiring done yet. The egglog-r2il text-on-hot-path site is fixed. + ## 2026-11-02 — D-TGL-PUB: G10 × G11 atomic publication lab spec → `.claude/plans/g10-g11-atomic-publication-lab-v1.md` **Status:** SPEC, lab only; nothing implemented. **Board:** [STATUS_BOARD](STATUS_BOARD.md) D-TGL-PUB; [entry](entries/2026-11-02-d-tgl-release-fence-and-g10-g11-boundaries.md). diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 5f94baf3f..942f098d9 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -241,6 +241,7 @@ Plan: [d-codegraph-0-resident-codegraph-v1.md](../plans/d-codegraph-0-resident-c | **D-CODEGRAPH-0-B** | resident rows via the ruff sink; per-file digests; incremental invalidation | LANDED (offline form): ruff #130 (merged `95be2e480b`; offline store in `ruff_charon`; `RefinedTruthSink` not reused, typed to R2IL). Incremental == clean on the fixture, byte-identical; skipped dependent leaves exactly one dangling edge. Follow-up fixes in ruff #131 (open). Lance-graph SoA residency still open | clean import == incremental import | | **D-CODEGRAPH-0-C** | callers / callees / impact / diagnostics; tiled closure; body → R2IL design check | SHIPPED (fixture scale): ruff #132 (merged `ed8fd4194f`, rows v2) + lance-graph #1921 (merged `4ab93bf3e`), `crates/lance-graph-codegraph` (queries as confirmed / possible / unknown masks over the xlog cube; dead function, unresolved call, dangling call; unused import NOT_RUN). 27 tests, 12 disable runs red. Tiled closure deferred: refusals `ClosureWidth` (> 64) and `TooMany` (> 256) are surfaced as typed UNKNOWN | each guard disable-verified; unused import proven only without macros, traits, globs, re-exports | | **D-CODEGRAPH-0-C2** | wide closure (multi-word rows, block presence), multi-tile cube, merge-on-read refresh, interned lanes | SHIPPED: #1923 (merged `2e19a5adc`). Impact over any size; mask-risc store (695 symbols, 3 tiles): impact 286 ns, callers 29 µs, references 45 µs; refresh of an unchanged crate 1.5–1.7 ms = FAILED gate (reading the 2.5 MB text file), fixed by D-CODEGRAPH-0-BIN. `refresh_crate` atomic (prepare → validate → commit: staged interner, positions, tile map, `Cube::stage`, closure; commit has no error path); codegraph suites now in `rust-test.yml` | narrow vs wide bit-identical ≤ 64; BFS reference on 694 positions; refresh == clean open; a refused refresh changes nothing (NeedsReopen, injected stage and closure refusals; no version issued); retry == the refresh that never failed, call-site multiplicity included; 7 disable runs red | +| **D-XLOG-WIRE** | XLOG wiring gaps W1–W8 to the hot path (magic report, polarity, estimates, degree producer, dormant Fixpoint, semi-naive owner, F100 execution, plan identity) | Queued: plan `xlog-wiring-to-hot-path-v1.md`; gates D-CODEGRAPH-0-BIN B3; W7 and W5 need operator decisions | each gap's named falsifier (reach/far, P-A3, triangle probe, degree regret, P-A4a/b, P-I1) | | **D-CODEGRAPH-0-BIN** | ruff_charon binary row lanes + header digest; codec9 small codebooks; Quack counting; no strings in the hot path; provenance header + per-row `(artifact, FunDeclId)`; `INVOKES_WORD` to a registered DT64 word | DEFERRED (operator 2026-11-03): B3 waits until strings are outside the hot path and the XLOG wiring-gap list (6+ gaps, the polyfill among them) has reached the hot path; any remaining string is taken off at the codebook label ("wardrobe"). PLATEAU (operator 2026-11-02): reader merged as lance-graph #1929 `4fadef69d` — rows.bin intake + header-only unchanged refresh 2.58 µs (met); changed-crate 2.5 ms vs ≤1 ms gate NOT met (`Symbols::intern` 2.04 ms) → B3 interner open, then re-run gate; F7 Quack counting open. WRITER SHIPPED: ruff #133 merged `6c3d1bf8da` (follow-up ruff #134: stale `rows.tsv` removed when export is off; section offsets past 4 GiB refused, both from Codex review); reader PR B unblocked. ruff #133 `ruff_charon` `store_bin.rs` + `Store` wiring — format §2 + PROV/FUNDECL/OBJ_KIND (ARTREF elided, one artifact), verifying reader with one refusal per shape, golden `cg_lib.rows.bin`; 32 new tests, 6 disables red; TSV export stays ON by default until PR B (lance-graph reader) lands, then flips; `INVOKES_WORD` still OPEN (association source). Plan `d-codegraph-0-binary-lanes-v1.md` (operator: graph-wide u32 ids, TSV kept as debug `open_tsv`; Amendment A §8: PROV section, FUNDECL/ARTREF lanes, `INVOKES_WORD`, F9–F12). Ruff writer PR first, then the codegraph reader. OPEN: source of the "function realises word" association | unchanged refresh ≤ 20 µs; changed-crate open ≤ 1 ms; binary == TSV row for row | | **D-TGL-0** | GitHub-analogue Thought-Git lifecycle as a shared contract (branch → change → diff → PR → checks → review → rebase/squash → land → receipt/replay; rework / discard) for Codegraph, DT64, XLOG | CONTRACT (docs): plan `thought-git-lifecycle-contract-v1.md`; PR states are readings of existing records, no workflow engine | each step expressible with listed primitives | | **D-TGL-LAB** | Codegraph lab: F-LAND / F-DISCARD | SHIPPED (lab, crate-private): `prepare_refresh` / `commit_refresh` with a generation fence (`RefreshRefusal::Stale`); second branch recomputed against current W0 == clean open incl. call-site counts; discard leaves W0 unchanged; 2 disables red (without the fence only a `debug_assert` catches the collision) | not a production land | diff --git a/.claude/plans/xlog-wiring-to-hot-path-v1.md b/.claude/plans/xlog-wiring-to-hot-path-v1.md new file mode 100644 index 000000000..89bbcfbb5 --- /dev/null +++ b/.claude/plans/xlog-wiring-to-hot-path-v1.md @@ -0,0 +1,80 @@ +# XLOG wiring gaps to the hot path — v1 (D-XLOG-WIRE) + +**Status:** PLAN. Gating input for D-CODEGRAPH-0-BIN B3 (operator, 2026-11-03: B3 waits until strings are outside the hot path and this list has reached the hot path; any remaining string comes off at the codebook label, the "wardrobe"). +**Sources:** `.claude/board/entries/2026-11-02-coresearch-xlog-souffle-crepe-dr3-archaeology.md` §1–§3, re-verified at AdaWorldAPI/xlog `main` `84da1a8` on 2026-11-03 (citations below); today's findings. +**Rule for every row:** a compile result reaches lance-graph as DATA through the existing admission gates. No import of XLOG's runtime, CUDA executor, or a second planner (archaeology §2.7, SKIP list). + +## The list + +Each row gives the gap, where it is lost, the smallest wiring step, its falsifier, and whether it can run in a CPU-only container. + +**W1. Magic-set report discarded.** +- Lost at: `xlog-logic/src/compile.rs:1496` and `:1511`, both `drop(rewritten.report)`. +- Wiring step: carry `MagicSetReport` on the compiled plan; admission refuses a plan whose report is `Declined` when the caller required `on`. +- Falsifier: reach/far (fork PR #7) yields a plan with a `Declined` report, and the no-`far` twin yields `Applied`. +- CPU-only: compile only. + +**W2. Edge polarity dropped.** +- Lost at: stratify → lower (archaeology P-A3). +- Wiring step: a polarity record per rule body literal on the plan. +- Falsifier: P-A3, a negated literal whose polarity a consumer must see. +- CPU-only: compile only. + +**W3. Join estimates discarded.** +- Lost at: estimates are baked into the tree shape; `RirMeta` is schema-only. +- Wiring step: the optimizer's chosen estimates travel on the plan as data. +- Falsifier: the triangle pairing probe (`xlog-relcomp-probe/examples/triangle_pairing_baselines.rs`) reads the plan's estimates and matches `optimizer.rs:3395-3404`. +- CPU-only: yes, the lab probe. + +**W4. Degree statistics have no producer** (found 2026-11-03). +- Lost at: no production caller of `add_prefix_degree`; the only caller is `xlog-integration/src/bin/wcoj_phase_report.rs:347`, with hardcoded values. `PrefixDegreeStats` holds only an average and a maximum. +- Wiring step: a per-key degree statistic maintained on insert, and a producer on the runtime insert path. Measured cost in the lab: 1.3–2.7 ns per insert, 96 KiB. +- Falsifier: exact-degree pairing regret 1.000 against the estimate argmin, on the probe corpus. +- CPU-only: no. The runtime insert path is CUDA; acceptance needs an authorized GPU run. + +**W5. `RirNode::Fixpoint` dormant.** +- Where: production compile never constructs one. The only construction is `optimizer.rs:4672`, inside `#[cfg(test)]`. The runtime handler exists (`xlog-runtime/src/executor/node_dispatch.rs:280` → `execute_fixpoint`). +- Wiring step: decide whether recursive SCCs lower to `Fixpoint` (one owner for semi-naive) or the node is removed (the fork's no-dead-code rule). +- Falsifier: P-A4a. +- CPU-only: compile only. + +**W6. Semi-naive deltas are runtime-only and CUDA-only.** lance-graph separately re-implements semi-naive recursion 4+ times. +- Where: XLOG runtime; lance-graph `lance-graph-xlog`, relcomp gate, and others (archaeology §1). +- Wiring step: one delta owner on the resident path; the copies compared by folds and then removed. +- Falsifier: P-A4b, all copies agree by folds before any is removed. +- CPU-only: lance-graph half yes. + +**W7. `XLOG_LENS` (`0xFFFF::0xF100`) declared, never executed.** This is the polyfill-adjacent gap. +- Where: `lance-graph-xlog/src/lens.rs:33`. `lance-graph-r2il/src/binding.rs:296` refuses every lens except `POLYFILL_LENS` (`F000`) and R2IL-fold concepts. +- What it needs: the words (`functor/3`, `arg/3`, `=../2`) read helper relations the XLOG compiler emits as facts. They are column-reading words, not scalar folds, so r2il needs a relational word execution (a mask fold over the helper relation's lanes). +- Wiring step: an executor decision (operator), then one word end to end. +- Falsifier: P-I1, F100 executes through `BindStore` and `prepare` and agrees with XLOG's helper rows. +- CPU-only: yes once decided. + +**W8. Competing plan identities.** +- Where: `MethodSignature`, the SHA-256 lowering digest, and the FNV `plan_id` (`binding.rs`, `plan_id`). +- Wiring step: DT64 is the one identity authority (D-DT64-AUTH); the other two become derived or removed. +- Falsifier: P-I1 / the census ratchet. +- CPU-only: yes. + +## Text on the hot path (the precondition named with this list) + +| site | state | +|---|---| +| egglog-r2il `Step::PushVar(String)`: a name lookup on every run | FIXED 2026-11-03: names resolve at lowering; `Step` is `Copy` | +| codegraph `Symbols::intern` on open and refresh (2.04 ms of the 2.5 ms changed-crate refresh) | B3; design already in `d-codegraph-0-binary-lanes-v1.md` §2 (`SYM_HASH` u64 + `SYM_OWNER`; labels stay in the KV section, the wardrobe). Deferred behind this list | +| r2il `opcode()` matches a label against `R2ILVocabulary` names | cold (`prepare`, once per method); not hot | + +## Order + +1. W1 and W5. Both are fork-side and compile-only, and each closes a loss with a known falsifier. +2. W7 once the executor shape is decided. +3. W3, then W4 (W4 needs the GPU acceptance run). +4. W2, W6 and W8. + +Then B3. Fork changes follow the fork's own rules: no local tests or runs, an atomic commit, a push, and an integration request to the lead. Runtime acceptance is an authorized GPU run, never a local experiment. + +## Decisions only the operator makes + +- **W7:** how a column-reading word executes on DR³. Either a mask fold over the helper relation in r2il, or F100 stays declared-only and the helper relations are plain data reads. +- **W5:** lower recursion to `Fixpoint`, or remove the dormant node. From 6ef9fd7ae347b869567e29e36f7a733abbcf2b51 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 01:21:52 +0000 Subject: [PATCH 08/11] plan: D-XLOG-WIRE runs on the cube, not CUDA W4 and W6 said the insert path and the semi-naive delta were CUDA-only. lance-graph-xlog already has a CPU mask-native delta (Cube::closure, wide::closure_wide, wide::refresh) and an insert path (Cube::add_edge, DeltaLog). Corrects both, names xlog-cube's host BTreeSet loop as the copy to retire, and records the measured cube refusal census (140/230 rules admitted, 90 refused by first reason) as the gap list. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .claude/plans/xlog-wiring-to-hot-path-v1.md | 42 ++++++++++++++++----- 1 file changed, 33 insertions(+), 9 deletions(-) diff --git a/.claude/plans/xlog-wiring-to-hot-path-v1.md b/.claude/plans/xlog-wiring-to-hot-path-v1.md index 89bbcfbb5..75110c4a9 100644 --- a/.claude/plans/xlog-wiring-to-hot-path-v1.md +++ b/.claude/plans/xlog-wiring-to-hot-path-v1.md @@ -28,9 +28,9 @@ Each row gives the gap, where it is lost, the smallest wiring step, its falsifie **W4. Degree statistics have no producer** (found 2026-11-03). - Lost at: no production caller of `add_prefix_degree`; the only caller is `xlog-integration/src/bin/wcoj_phase_report.rs:347`, with hardcoded values. `PrefixDegreeStats` holds only an average and a maximum. -- Wiring step: a per-key degree statistic maintained on insert, and a producer on the runtime insert path. Measured cost in the lab: 1.3–2.7 ns per insert, 96 KiB. +- Wiring step: a per-key degree statistic maintained on insert, and a producer on the insert path. On the cube that path is `Cube::new` intake and `Cube::add_edge` / `DeltaLog` (`lance-graph-xlog/src/cube.rs:250`, `:742`). Measured cost in the lab: 1.3–2.7 ns per insert, 96 KiB. - Falsifier: exact-degree pairing regret 1.000 against the estimate argmin, on the probe corpus. -- CPU-only: no. The runtime insert path is CUDA; acceptance needs an authorized GPU run. +- CPU-only: yes, on the cube. (The first version said the insert path was CUDA-only; that holds for `xlog-runtime`, not for the cube executor.) **W5. `RirNode::Fixpoint` dormant.** - Where: production compile never constructs one. The only construction is `optimizer.rs:4672`, inside `#[cfg(test)]`. The runtime handler exists (`xlog-runtime/src/executor/node_dispatch.rs:280` → `execute_fixpoint`). @@ -38,11 +38,15 @@ Each row gives the gap, where it is lost, the smallest wiring step, its falsifie - Falsifier: P-A4a. - CPU-only: compile only. -**W6. Semi-naive deltas are runtime-only and CUDA-only.** lance-graph separately re-implements semi-naive recursion 4+ times. -- Where: XLOG runtime; lance-graph `lance-graph-xlog`, relcomp gate, and others (archaeology §1). -- Wiring step: one delta owner on the resident path; the copies compared by folds and then removed. -- Falsifier: P-A4b, all copies agree by folds before any is removed. -- CPU-only: lance-graph half yes. +**W6. Semi-naive recursion has several owners.** +- Where: + - XLOG runtime: `Executor::execute_recursive_scc` (`xlog-runtime/src/executor/recursive.rs:445`), CUDA (`diff_gpu`, `union_gpu`, `union_many_gpu`). + - `lance-graph-xlog`, mask-native and CPU: `Cube::closure` (`cube.rs:669`, ≤ 64 positions, `FixpointBound` cap) and `wide::closure_wide` / `wide::refresh` (`wide.rs:395`, `:560`, block presence, retire-aware). Both cover `edge⁺` of one binary relation only. + - `xlog-cube` (fork): general recursive SCCs with its own host loop over owned rows, `BTreeSet>` with a `contains` filter and no cap (`xlog-cube/src/lib.rs:474–500`). D-STAUNEN-5 already names this shortcut. + - The relcomp gate and others (archaeology §1). +- Wiring step: `lance-graph-xlog` owns the delta. The general SCC round becomes `delta' = new andnot full` on cube masks, generalizing `closure` beyond `edge⁺`. The other copies are compared by folds, then removed. +- Falsifier: P-A4b, all copies agree before any is removed; the existing three-way C0 parity (`xlog-cube/tests/closure_parity.rs`) is the starting point. +- CPU-only: yes. **W7. `XLOG_LENS` (`0xFFFF::0xF100`) declared, never executed.** This is the polyfill-adjacent gap. - Where: `lance-graph-xlog/src/lens.rs:33`. `lance-graph-r2il/src/binding.rs:296` refuses every lens except `POLYFILL_LENS` (`F000`) and R2IL-fold concepts. @@ -69,10 +73,30 @@ Each row gives the gap, where it is lost, the smallest wiring step, its falsifie 1. W1 and W5. Both are fork-side and compile-only, and each closes a loss with a known falsifier. 2. W7 once the executor shape is decided. -3. W3, then W4 (W4 needs the GPU acceptance run). +3. W3, then W4. 4. W2, W6 and W8. -Then B3. Fork changes follow the fork's own rules: no local tests or runs, an atomic commit, a push, and an integration request to the lead. Runtime acceptance is an authorized GPU run, never a local experiment. +Then B3. Fork changes follow the fork's own rules: an atomic commit, a push, and an integration request to the lead. Local runs are allowed (operator, 2026-11-03). + +## Executor: the cube, not CUDA + +CUDA is replaced by the cube executor that already exists, not by a new backing under `CudaKernelProvider`. `xlog-cube::CubeExecutor` takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. + +Measured 2026-11-03 (`cargo run --example coverage` over `xlog-integration/tests/*.rs`, fork `main` `84da1a8`): 188 programs, 230 rules, 140 admitted, 90 refused. First refusal reason per rule: + +- 33 reads a relation that is not binary +- 17 filter other than `col == const` +- 12 computed or out-of-range output column +- 7 Join body +- 6 join key outside its input +- 5 Project over Project +- 5 XLOG word `0xFFFF :: 0xF100` +- 3 Project over GroupBy +- 2 Project over Join + +Admitted is not correct: `coverage` gives every base relation as empty, and a rule counts under its first refusal only (D-STAUNEN-5 plan, "Relation to the xlog-cube coverage work"). That plan also carries the agreed order: projection composition, filter algebra, resident execution, computed columns, F100, N-ary relations. + +Limits of the cube that bound this work: `xlog-cube` builds a single-tile cube (`Width::W256`, at most 256 ids; `xlog-cube/src/lib.rs:272`), while `Cube::new_tiled` and `closure_wide` (used by `lance-graph-codegraph`) span many tiles; relations are binary; the cube has no union or difference view. ## Decisions only the operator makes From cfb356a8acc458875ca63b743dba4f37b8062700 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 01:23:44 +0000 Subject: [PATCH 09/11] plan: D-XLOG-WIRE follows Amendment E; Amendment F was never written Cites d-xlog-native Amendment E (#1910) as the decided route: assimilate into lance-graph-xlog, polyfill the callers, CubeCL over ndarray only for the residue; CudaBuffer plumbing is not ported. Records that the device-less provider / CudaBuffer::View idea (#1911) is OPEN and that the "Amendment F" cited by cube.rs:2 and the D-XLOG-NATIVE-7 entry is absent from the plan. Adds the per-crate caller-surface count toward E's open census. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .claude/plans/xlog-wiring-to-hot-path-v1.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.claude/plans/xlog-wiring-to-hot-path-v1.md b/.claude/plans/xlog-wiring-to-hot-path-v1.md index 75110c4a9..441cca72f 100644 --- a/.claude/plans/xlog-wiring-to-hot-path-v1.md +++ b/.claude/plans/xlog-wiring-to-hot-path-v1.md @@ -80,7 +80,11 @@ Then B3. Fork changes follow the fork's own rules: an atomic commit, a push, and ## Executor: the cube, not CUDA -CUDA is replaced by the cube executor that already exists, not by a new backing under `CudaKernelProvider`. `xlog-cube::CubeExecutor` takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. +The route is already decided: `d-xlog-native-v1.md` Amendment E (#1910, operator 2026-11-01). XLOG's RIR kinds are assimilated into our algebra in `lance-graph-xlog`; XLOG's caller API (`pyxlog`, `xlog-cli`, `xlog-integration`) is polyfilled back onto it; the fork depends on `lance-graph-xlog`, never the reverse; XLOG's runtime and its `CudaBuffer` plumbing are not ported. Tiers, in order: (1) assimilate into `lance-graph-xlog`; (2) polyfill or migrate the callers; (3) only for a kernel with no algebra counterpart, port it from CUDA to CubeCL over ndarray. "Replace CUDA" (operator, 2026-11-03) is executed through these tiers, not by a DR³ backing under `CudaKernelProvider`. + +Not decided: a device-less `CudaKernelProvider` with a `CudaBuffer::View` variant. The D-XLOG-NATIVE-7 entry (#1911) lists it as OPEN and says "neither is promoted". It cites an "Amendment F" (also cited at `lance-graph-xlog/src/cube.rs:2`) that was never written into `d-xlog-native-v1.md`; the plan ends at E. + +`xlog-cube::CubeExecutor` is the tier-1/2 executor today: it takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. Measured 2026-11-03 (`cargo run --example coverage` over `xlog-integration/tests/*.rs`, fork `main` `84da1a8`): 188 programs, 230 rules, 140 admitted, 90 refused. First refusal reason per rule: @@ -96,6 +100,8 @@ Measured 2026-11-03 (`cargo run --example coverage` over `xlog-integration/tests Admitted is not correct: `coverage` gives every base relation as empty, and a rule counts under its first refusal only (D-STAUNEN-5 plan, "Relation to the xlog-cube coverage work"). That plan also carries the agreed order: projection composition, filter algebra, resident execution, computed columns, F100, N-ary relations. +Amendment E's open item, the caller-API census, is partly answered by a count of `provider.(` calls per crate, multi-line chains included (2026-11-03): pyxlog 50 methods / 234 calls, xlog-integration 24 / 105, xlog-cli 8 / 14. pyxlog calls the provider directly for ILP, DLPack and the semantic engine, so its caller surface is wider than the executor. xlog-prob (426 kernel launch sites) and xlog-solve (27) launch SAT, CNF, circuit, PIR, cache, weights and Monte-Carlo kernels through `provider.device()`; these have no algebra counterpart and are tier-3 candidates. + Limits of the cube that bound this work: `xlog-cube` builds a single-tile cube (`Width::W256`, at most 256 ids; `xlog-cube/src/lib.rs:272`), while `Cube::new_tiled` and `closure_wide` (used by `lance-graph-codegraph`) span many tiles; relations are binary; the cube has no union or difference view. ## Decisions only the operator makes From f94c20a9ed2469f32515723e594e6aaae775e731 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 01:43:21 +0000 Subject: [PATCH 10/11] plan: write d-xlog-native Amendment F, the reactor swap cube.rs:2 and the D-XLOG-NATIVE-7 entry cited an Amendment F that was never written. Records it: XLOG's caller-visible interface (Executor, CudaKernelProvider, CudaBuffer) stays, the resident cube is the machine underneath. Lists what is done (coordinates, evaluation, cube, mask recursion, tiles, F100 lens, CubeExecutor with no xlog-cuda dependency) and what is not (no caller reaches the cube; 90 refused shapes; general SCCs on host rows; tier-3 residue). D-XLOG-WIRE now points to F instead of calling the swap undecided. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- .claude/plans/d-xlog-native-v1.md | 23 +++++++++++++++++++++ .claude/plans/xlog-wiring-to-hot-path-v1.md | 2 +- 2 files changed, 24 insertions(+), 1 deletion(-) diff --git a/.claude/plans/d-xlog-native-v1.md b/.claude/plans/d-xlog-native-v1.md index 3d7ce5f0d..023bb0072 100644 --- a/.claude/plans/d-xlog-native-v1.md +++ b/.claude/plans/d-xlog-native-v1.md @@ -216,3 +216,26 @@ Effect on §2: - **OPEN:** - The exact caller API. Next step is a census of what `pyxlog` / `xlog-cli` / `xlog-integration` call on the executor, and how each call maps onto a `lance-graph-xlog` call. - Which translation the XLOG fork carries: a translator per RIR kind, or a thin adapter crate inside the fork. + +## Amendment F (2026-11-01, written 2026-11-03): the reactor swap — same interface, the resident cube underneath + +Cited since #1911 by `crates/lance-graph-xlog/src/cube.rs:2` and the D-XLOG-NATIVE-7 entry, but never written here until now. + +**DECISION (operator; #1911 "replace the machine under XLOG's CUDA-facing API"; restated 2026-11-03 as the Semantic Reactor Swap: "same interface above, different physics below").** What XLOG's callers see stays: `Executor`, `CudaKernelProvider`, `CudaBuffer` as `pyxlog`, `xlog-cli` and `xlog-integration` use them. The machine underneath is the resident hypercube: DR/DT64 coordinates, mask-risc / Quack evaluation, materialization only at the boundary. Observable answers must match; the internal model is free. + +Relation to Amendment E: E's "the `CudaBuffer` plumbing is not ported" holds. XLOG's internals are not translated operator by operator; the caller-visible handles keep their names and get the cube as their backing. E's three tiers decide what backs each operation. + +**Done (the reactor runs):** +- Coordinates: DR `LocalMap` / `MapTable` frames, DT64 `MethodBinding` admission (#1884, #1907). +- Evaluation: `support` / `bag_count` as Quack → mask-risc programs (#1907). +- The resident hypercube: `Cube`, `Copy` views, terminals that run programs, `materialize_rows` as the one row builder (#1911). +- Recursion on masks: `Cube::closure` (#1914) and `wide::closure_wide` / `refresh` / `DeltaLog`, many tiles via `Cube::new_tiled`, `stage` / `commit` (#1923; running in `lance-graph-codegraph`). +- Behaviour lens `0xFFFF :: 0xF100` (#1913). +- XLOG plans on the cube: `xlog-cube::CubeExecutor` (fork, xlog#2–#6) runs XLOG's compiled `ExecutionPlan` with no `xlog-cuda` or `xlog-runtime` dependency; three-way closure parity (`tests/closure_parity.rs`); 140 of 230 integration rules admitted (measured 2026-11-03; admitted is not checked). +- A device-less build of the fork's runtime is reachable (`XLOG_RUSTDOC_NO_CUDA=1`, measured 2026-11-01). + +**Not done (the translation channels):** +- No caller reaches the cube: `pyxlog`, `xlog-cli` and `xlog-integration` still construct `Executor::new(Arc)` (138 sites). The device-less provider and the `CudaBuffer::View` variant that would let them are not built. +- 90 refused rule shapes (D-XLOG-WIRE plan, "Executor: the cube, not CUDA"). +- General recursive SCCs: `xlog-cube` keeps a host `BTreeSet` loop; only `edge⁺` runs on masks. +- The residue with no algebra counterpart (SAT, knowledge compilation, the semantic engine): E tier 3. diff --git a/.claude/plans/xlog-wiring-to-hot-path-v1.md b/.claude/plans/xlog-wiring-to-hot-path-v1.md index 441cca72f..f99a19d34 100644 --- a/.claude/plans/xlog-wiring-to-hot-path-v1.md +++ b/.claude/plans/xlog-wiring-to-hot-path-v1.md @@ -82,7 +82,7 @@ Then B3. Fork changes follow the fork's own rules: an atomic commit, a push, and The route is already decided: `d-xlog-native-v1.md` Amendment E (#1910, operator 2026-11-01). XLOG's RIR kinds are assimilated into our algebra in `lance-graph-xlog`; XLOG's caller API (`pyxlog`, `xlog-cli`, `xlog-integration`) is polyfilled back onto it; the fork depends on `lance-graph-xlog`, never the reverse; XLOG's runtime and its `CudaBuffer` plumbing are not ported. Tiers, in order: (1) assimilate into `lance-graph-xlog`; (2) polyfill or migrate the callers; (3) only for a kernel with no algebra counterpart, port it from CUDA to CubeCL over ndarray. "Replace CUDA" (operator, 2026-11-03) is executed through these tiers, not by a DR³ backing under `CudaKernelProvider`. -Not decided: a device-less `CudaKernelProvider` with a `CudaBuffer::View` variant. The D-XLOG-NATIVE-7 entry (#1911) lists it as OPEN and says "neither is promoted". It cites an "Amendment F" (also cited at `lance-graph-xlog/src/cube.rs:2`) that was never written into `d-xlog-native-v1.md`; the plan ends at E. +The reactor swap is `d-xlog-native-v1.md` Amendment F: the interface callers see (`Executor`, `CudaKernelProvider`, `CudaBuffer`) stays, and the resident cube is the machine underneath. The reactor is built; the device-less provider / `CudaBuffer::View` that connects the callers to it is the open channel. `xlog-cube::CubeExecutor` is the tier-1/2 executor today: it takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. From 3dcfac9d1508b7218ab4bea1bcd7d698235eab6a Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 01:46:53 +0000 Subject: [PATCH 11/11] docs: no Amendment F; cite D-XLOG-NATIVE-7 instead Removes the Amendment F written in f94c20a9e: it backfilled an experiment's scope as an architectural decision. d-xlog-native-v1.md is back to its pre-F text. The three citations of a never-written Amendment F (cube.rs:2, tests/cube.rs:1, the D-XLOG-NATIVE-7 entry header) now point to the D-XLOG-NATIVE-7 entry and PR #1911. Doc comments only; no code changes. D-XLOG-WIRE: Amendment E stays the decision of record. The device-less provider and CudaBuffer::View are a non-authoritative research possibility. The provider-call count is an inventory, not a migration mandate. Cube::closure / closure_wide are not equivalent to xlog-cube's host-row recursive SCC evaluation. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX --- ...6-11-01-xlog-resident-hypercube-context.md | 2 +- .claude/plans/d-xlog-native-v1.md | 23 ------------------- .claude/plans/xlog-wiring-to-hot-path-v1.md | 8 +++---- crates/lance-graph-xlog/src/cube.rs | 2 +- crates/lance-graph-xlog/tests/cube.rs | 2 +- 5 files changed, 7 insertions(+), 30 deletions(-) diff --git a/.claude/board/entries/2026-11-01-xlog-resident-hypercube-context.md b/.claude/board/entries/2026-11-01-xlog-resident-hypercube-context.md index 3e9cf6fb2..c2487f0e2 100644 --- a/.claude/board/entries/2026-11-01-xlog-resident-hypercube-context.md +++ b/.claude/board/entries/2026-11-01-xlog-resident-hypercube-context.md @@ -1,6 +1,6 @@ # D-XLOG-NATIVE-7: one resident hypercube as XLOG's execution context (probe) -**Date 2026-11-01 · ID D-XLOG-NATIVE-7 · Status PROBE · Plan `.claude/plans/d-xlog-native-v1.md` (Amendment F, pending beside E in #1910) · Crate `crates/lance-graph-xlog` (`cube`)** +**Date 2026-11-01 · ID D-XLOG-NATIVE-7 · Status PROBE · Plan `.claude/plans/d-xlog-native-v1.md` (Amendment E is the decision of record; no Amendment F exists — corrected 2026-11-03) · Crate `crates/lance-graph-xlog` (`cube`)** DECISION (direction, from the session): the experiment replaces the machine under XLOG's CUDA-facing API with one resident context, rather than speeding up diff --git a/.claude/plans/d-xlog-native-v1.md b/.claude/plans/d-xlog-native-v1.md index 023bb0072..3d7ce5f0d 100644 --- a/.claude/plans/d-xlog-native-v1.md +++ b/.claude/plans/d-xlog-native-v1.md @@ -216,26 +216,3 @@ Effect on §2: - **OPEN:** - The exact caller API. Next step is a census of what `pyxlog` / `xlog-cli` / `xlog-integration` call on the executor, and how each call maps onto a `lance-graph-xlog` call. - Which translation the XLOG fork carries: a translator per RIR kind, or a thin adapter crate inside the fork. - -## Amendment F (2026-11-01, written 2026-11-03): the reactor swap — same interface, the resident cube underneath - -Cited since #1911 by `crates/lance-graph-xlog/src/cube.rs:2` and the D-XLOG-NATIVE-7 entry, but never written here until now. - -**DECISION (operator; #1911 "replace the machine under XLOG's CUDA-facing API"; restated 2026-11-03 as the Semantic Reactor Swap: "same interface above, different physics below").** What XLOG's callers see stays: `Executor`, `CudaKernelProvider`, `CudaBuffer` as `pyxlog`, `xlog-cli` and `xlog-integration` use them. The machine underneath is the resident hypercube: DR/DT64 coordinates, mask-risc / Quack evaluation, materialization only at the boundary. Observable answers must match; the internal model is free. - -Relation to Amendment E: E's "the `CudaBuffer` plumbing is not ported" holds. XLOG's internals are not translated operator by operator; the caller-visible handles keep their names and get the cube as their backing. E's three tiers decide what backs each operation. - -**Done (the reactor runs):** -- Coordinates: DR `LocalMap` / `MapTable` frames, DT64 `MethodBinding` admission (#1884, #1907). -- Evaluation: `support` / `bag_count` as Quack → mask-risc programs (#1907). -- The resident hypercube: `Cube`, `Copy` views, terminals that run programs, `materialize_rows` as the one row builder (#1911). -- Recursion on masks: `Cube::closure` (#1914) and `wide::closure_wide` / `refresh` / `DeltaLog`, many tiles via `Cube::new_tiled`, `stage` / `commit` (#1923; running in `lance-graph-codegraph`). -- Behaviour lens `0xFFFF :: 0xF100` (#1913). -- XLOG plans on the cube: `xlog-cube::CubeExecutor` (fork, xlog#2–#6) runs XLOG's compiled `ExecutionPlan` with no `xlog-cuda` or `xlog-runtime` dependency; three-way closure parity (`tests/closure_parity.rs`); 140 of 230 integration rules admitted (measured 2026-11-03; admitted is not checked). -- A device-less build of the fork's runtime is reachable (`XLOG_RUSTDOC_NO_CUDA=1`, measured 2026-11-01). - -**Not done (the translation channels):** -- No caller reaches the cube: `pyxlog`, `xlog-cli` and `xlog-integration` still construct `Executor::new(Arc)` (138 sites). The device-less provider and the `CudaBuffer::View` variant that would let them are not built. -- 90 refused rule shapes (D-XLOG-WIRE plan, "Executor: the cube, not CUDA"). -- General recursive SCCs: `xlog-cube` keeps a host `BTreeSet` loop; only `edge⁺` runs on masks. -- The residue with no algebra counterpart (SAT, knowledge compilation, the semantic engine): E tier 3. diff --git a/.claude/plans/xlog-wiring-to-hot-path-v1.md b/.claude/plans/xlog-wiring-to-hot-path-v1.md index f99a19d34..8899cd550 100644 --- a/.claude/plans/xlog-wiring-to-hot-path-v1.md +++ b/.claude/plans/xlog-wiring-to-hot-path-v1.md @@ -41,7 +41,7 @@ Each row gives the gap, where it is lost, the smallest wiring step, its falsifie **W6. Semi-naive recursion has several owners.** - Where: - XLOG runtime: `Executor::execute_recursive_scc` (`xlog-runtime/src/executor/recursive.rs:445`), CUDA (`diff_gpu`, `union_gpu`, `union_many_gpu`). - - `lance-graph-xlog`, mask-native and CPU: `Cube::closure` (`cube.rs:669`, ≤ 64 positions, `FixpointBound` cap) and `wide::closure_wide` / `wide::refresh` (`wide.rs:395`, `:560`, block presence, retire-aware). Both cover `edge⁺` of one binary relation only. + - `lance-graph-xlog`, mask-native and CPU: `Cube::closure` (`cube.rs:669`, ≤ 64 positions, `FixpointBound` cap) and `wide::closure_wide` / `wide::refresh` (`wide.rs:395`, `:560`, block presence, retire-aware). Both cover `edge⁺` of one binary relation only. They are not equivalent to `xlog-cube`'s recursive SCC evaluation, which runs on host-owned rows (next item). - `xlog-cube` (fork): general recursive SCCs with its own host loop over owned rows, `BTreeSet>` with a `contains` filter and no cap (`xlog-cube/src/lib.rs:474–500`). D-STAUNEN-5 already names this shortcut. - The relcomp gate and others (archaeology §1). - Wiring step: `lance-graph-xlog` owns the delta. The general SCC round becomes `delta' = new andnot full` on cube masks, generalizing `closure` beyond `edge⁺`. The other copies are compared by folds, then removed. @@ -82,9 +82,9 @@ Then B3. Fork changes follow the fork's own rules: an atomic commit, a push, and The route is already decided: `d-xlog-native-v1.md` Amendment E (#1910, operator 2026-11-01). XLOG's RIR kinds are assimilated into our algebra in `lance-graph-xlog`; XLOG's caller API (`pyxlog`, `xlog-cli`, `xlog-integration`) is polyfilled back onto it; the fork depends on `lance-graph-xlog`, never the reverse; XLOG's runtime and its `CudaBuffer` plumbing are not ported. Tiers, in order: (1) assimilate into `lance-graph-xlog`; (2) polyfill or migrate the callers; (3) only for a kernel with no algebra counterpart, port it from CUDA to CubeCL over ndarray. "Replace CUDA" (operator, 2026-11-03) is executed through these tiers, not by a DR³ backing under `CudaKernelProvider`. -The reactor swap is `d-xlog-native-v1.md` Amendment F: the interface callers see (`Executor`, `CudaKernelProvider`, `CudaBuffer`) stays, and the resident cube is the machine underneath. The reactor is built; the device-less provider / `CudaBuffer::View` that connects the callers to it is the open channel. +Implementation evidence for the resident cube is D-XLOG-NATIVE-7 (PR #1911, board entry `2026-11-01-xlog-resident-hypercube-context.md`). A device-less `CudaKernelProvider` and a `CudaBuffer::View` variant are listed there as OPEN and not promoted: a research possibility, not an authorized route. There is no Amendment F. -`xlog-cube::CubeExecutor` is the tier-1/2 executor today: it takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. +`xlog-cube::CubeExecutor` is the cube executor today: it takes the same `ExecutionPlan` as `xlog_runtime::Executor` and runs it on `lance_graph_xlog::cube::Cube`. Its refusal census is the gap list. Measured 2026-11-03 (`cargo run --example coverage` over `xlog-integration/tests/*.rs`, fork `main` `84da1a8`): 188 programs, 230 rules, 140 admitted, 90 refused. First refusal reason per rule: @@ -100,7 +100,7 @@ Measured 2026-11-03 (`cargo run --example coverage` over `xlog-integration/tests Admitted is not correct: `coverage` gives every base relation as empty, and a rule counts under its first refusal only (D-STAUNEN-5 plan, "Relation to the xlog-cube coverage work"). That plan also carries the agreed order: projection composition, filter algebra, resident execution, computed columns, F100, N-ary relations. -Amendment E's open item, the caller-API census, is partly answered by a count of `provider.(` calls per crate, multi-line chains included (2026-11-03): pyxlog 50 methods / 234 calls, xlog-integration 24 / 105, xlog-cli 8 / 14. pyxlog calls the provider directly for ILP, DLPack and the semantic engine, so its caller surface is wider than the executor. xlog-prob (426 kernel launch sites) and xlog-solve (27) launch SAT, CNF, circuit, PIR, cache, weights and Monte-Carlo kernels through `provider.device()`; these have no algebra counterpart and are tier-3 candidates. +Toward Amendment E's open caller-API census, a count of `provider.(` calls per crate, multi-line chains included (2026-11-03): pyxlog 50 methods / 234 calls, xlog-integration 24 / 105, xlog-cli 8 / 14. pyxlog calls the provider directly for ILP, DLPack and the semantic engine, so its caller surface is wider than the executor. xlog-prob (426 kernel launch sites) and xlog-solve (27) launch SAT, CNF, circuit, PIR, cache, weights and Monte-Carlo kernels through `provider.device()`; these have no algebra counterpart and are tier-3 candidates. The count is an inventory, not a migration mandate: it does not make any provider method a seam. Limits of the cube that bound this work: `xlog-cube` builds a single-tile cube (`Width::W256`, at most 256 ids; `xlog-cube/src/lib.rs:272`), while `Cube::new_tiled` and `closure_wide` (used by `lance-graph-codegraph`) span many tiles; relations are binary; the cube has no union or difference view. diff --git a/crates/lance-graph-xlog/src/cube.rs b/crates/lance-graph-xlog/src/cube.rs index 5c9fb82c9..b8eecd074 100644 --- a/crates/lance-graph-xlog/src/cube.rs +++ b/crates/lance-graph-xlog/src/cube.rs @@ -1,5 +1,5 @@ //! The resident hypercube: one execution context for every relation, and -//! views into it (plan `d-xlog-native-v1.md` Amendment F). +//! views into it (D-XLOG-NATIVE-7, PR #1911; board entry `2026-11-01-xlog-resident-hypercube-context.md`). //! //! [`support`](crate::support) and [`bag_count`](crate::bag_count) build their //! lanes per call, oriented for one join. A [`Cube`] builds them once, for diff --git a/crates/lance-graph-xlog/tests/cube.rs b/crates/lance-graph-xlog/tests/cube.rs index 54e26532b..bb5d4095f 100644 --- a/crates/lance-graph-xlog/tests/cube.rs +++ b/crates/lance-graph-xlog/tests/cube.rs @@ -1,4 +1,4 @@ -//! The resident hypercube (plan `d-xlog-native-v1.md` Amendment F) against a +//! The resident hypercube (D-XLOG-NATIVE-7, PR #1911; board entry `2026-11-01-xlog-resident-hypercube-context.md`) against a //! scalar oracle and against the per-call free functions, plus the gates that //! make it a context rather than a faster operator: composing views runs //! nothing, any pair of relations joins on any columns without a new lookup,