From 68f9a3802f15f785209cecb1cc7f302caeb31aac Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 21:36:24 +0000 Subject: [PATCH 1/4] wip D-GRAMMAR-WHEN-1 lab --- crates/grammar-constraints-probe/Cargo.toml | 2 + crates/grammar-constraints-probe/src/lib.rs | 1 + crates/grammar-constraints-probe/src/when.rs | 457 ++++++++++++++++++ .../grammar-constraints-probe/tests/when.rs | 422 ++++++++++++++++ 4 files changed, 882 insertions(+) create mode 100644 crates/grammar-constraints-probe/src/when.rs create mode 100644 crates/grammar-constraints-probe/tests/when.rs diff --git a/crates/grammar-constraints-probe/Cargo.toml b/crates/grammar-constraints-probe/Cargo.toml index 8e8f0fda7..572b4d2d4 100644 --- a/crates/grammar-constraints-probe/Cargo.toml +++ b/crates/grammar-constraints-probe/Cargo.toml @@ -16,6 +16,8 @@ lance-graph-dt64 = { path = "../lance-graph-dt64" } lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } # WHEN expressibility check (SetExpr / Guard normal form). lance-graph-contract = { path = "../lance-graph-contract" } +# D-GRAMMAR-WHEN-1: the relational description (Filter) and its lowering. +lance-graph-quack = { path = "../lance-graph-quack" } [patch."https://github.com/AdaWorldAPI/ndarray"] ndarray = { path = "../../../ndarray" } diff --git a/crates/grammar-constraints-probe/src/lib.rs b/crates/grammar-constraints-probe/src/lib.rs index 9d77f6dd6..e7d10c203 100644 --- a/crates/grammar-constraints-probe/src/lib.rs +++ b/crates/grammar-constraints-probe/src/lib.rs @@ -42,6 +42,7 @@ #![forbid(unsafe_code)] pub mod fixtures; +pub mod when; use std::collections::HashMap; diff --git a/crates/grammar-constraints-probe/src/when.rs b/crates/grammar-constraints-probe/src/when.rs new file mode 100644 index 000000000..53c421bc6 --- /dev/null +++ b/crates/grammar-constraints-probe/src/when.rs @@ -0,0 +1,457 @@ +//! D-GRAMMAR-WHEN-1 — binding a grammatical WHEN through DT64 (LAB ONLY). +//! +//! Two class-bound read-only methods, `CandidateRecipient` and +//! `CandidateExperiencer`, share `deprel = obl:arg ∧ Case = Dat` and differ in +//! the head verb's frame. This module tests how DT64 can carry that +//! difference, and what runs it, in two physical forms: +//! +//! - [`Physical::Via`]: the head's lemma is read through the token's HEAD +//! pointer (`Filter::EqU32Via` → `Pred::EqU32Via`), as in #1947. The guard +//! names the frame only as an opaque `SetExpr::Sym(digest)`. The read is +//! at a position taken from another lane's value: ADMISSION B +//! (`entries/2026-10-20-six-decisions.md` §1) says such a position "is not +//! admissible as a read address", and `EqU32Via` "need[s] call-site +//! classification" (EXO-140, OPEN). LAB. +//! - [`Physical::CoAddressed`]: "the join is the layout" (D-HOLO H14c/H14d). +//! The head's frame code is a lane at the DEPENDENT's own coordinate +//! (`head_frame[i]`), written once by the producer ([`FramedPopulation`]). +//! The guard is then row-local and fully stated in today's `SetExpr`; the +//! query reads every lane at address `i`. What stays OPEN is the producer +//! step itself: it derives `head_frame[i]` from `lemma[head[i]]`, which is +//! a cross-row read at ingestion (EXO-46 / D-RMAP-1 membrane), counted +//! here. +//! +//! Neither form is an admission. The composer ([`compose`]) is the +//! approach-C model: DT64 admits the reference, the composer checks the +//! description against the bound guard witness, and lowers the description +//! plus the global WHERE plane into ONE mask-risc program through +//! `lance_graph_quack::lower`. Nothing is written; the result is a candidate +//! mask. + +use std::cell::Cell; + +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_contract::set_algebra::{Logic, SetExpr}; +use lance_graph_contract::set_rules::{Population as Multiplicity, Truth}; +use lance_graph_dt64::dr::{Frame, MapTable}; +use lance_graph_dt64::{ + BindStore, ClassSchema, Extent, Guard, MethodBinding, MethodId, MethodRef, Refusal, SchemaRev, + SigRev, ValueDemand, +}; +use lance_graph_mask_risc::{ + execute_into, words_for, Foreign, LaneRef, Out, Planes, Program, Scratch, +}; +use lance_graph_quack::{lower, Agg, Cmp, Col, Filter, ForeignLane, LowerError, Mask, Query}; + +use crate::{Population, Refusal as PopRefusal, Tok, Vocab, CASE, DEPREL, HEAD, LEMMA, TILE, WIDTH}; + +/// Field position (and lane) of the head's frame code, co-addressed. +pub const HEAD_FRAME: u16 = 4; +/// Fields of the lab token class: lemma, deprel, case, head, head_frame. +pub const FIELDS: usize = 5; + +/// Lab stand-in classids. Unminted; they say nothing about OGAR allocation. +pub const CLASS_VIA: u32 = 0x7F21_0000; +pub const CLASS_COADDR: u32 = 0x7F21_0001; +pub const CLASS_FOREIGN: u32 = 0x7F22_0000; + +pub const RECIPIENT: MethodId = MethodId(1); +pub const EXPERIENCER: MethodId = MethodId(2); + +/// Frame codes of the lab lexicon. 0 = no entry (never a negative role). +pub const FRAME_NONE: u32 = 0; +pub const FRAME_GIVE: u32 = 1; +pub const FRAME_EXPERIENCE: u32 = 2; + +/// A versioned, language-scoped verb-frame lexicon (lab data, German). +#[derive(Clone, Debug)] +pub struct Lexicon { + pub rev: u64, + pub language: &'static str, + pub entries: Vec<(&'static str, u32)>, +} + +impl Lexicon { + /// `de-dative-frames-fixture-v0` from #1947. + pub fn v0() -> Self { + Lexicon { + rev: 1, + language: "de", + entries: vec![ + ("geben", FRAME_GIVE), + ("schenken", FRAME_GIVE), + ("gefallen", FRAME_EXPERIENCE), + ], + } + } + + /// The same lemmas with GIVE and EXPERIENCE exchanged (control 2). + pub fn swapped() -> Self { + let mut l = Self::v0(); + l.rev = 2; + for e in &mut l.entries { + e.1 = match e.1 { + FRAME_GIVE => FRAME_EXPERIENCE, + FRAME_EXPERIENCE => FRAME_GIVE, + x => x, + }; + } + l + } + + pub fn frame(&self, lemma: &str) -> u32 { + self.entries + .iter() + .find(|(l, _)| *l == lemma) + .map_or(FRAME_NONE, |e| e.1) + } + + /// Lemmas carrying `frame`, sorted. + pub fn lemmas(&self, frame: u32) -> Vec<&'static str> { + let mut v: Vec<_> = self + .entries + .iter() + .filter(|e| e.1 == frame) + .map(|e| e.0) + .collect(); + v.sort_unstable(); + v + } +} + +/// The base population plus the co-addressed `head_frame` lane, produced once +/// under one lexicon revision. +pub struct FramedPopulation { + pub base: Population, + pub head_frame: Vec, + pub lexicon_rev: u64, + /// Cross-row reads the producer performed (`lemma[head[i]]`): the + /// EXO-46 / D-RMAP-1 membrane cost, counted, never in the query. + pub producer_lookups: usize, +} + +impl FramedPopulation { + /// Produce `head_frame[i] = frame(lemma(head(i)))`. Cold. + pub fn produce( + toks: &[Tok], + vocab: &mut Vocab, + table: &MapTable, + frame: &Frame, + lex: &Lexicon, + ) -> Result { + let base = Population::bind(toks, vocab, table, frame)?; + let map = table.map(frame, TILE).map_err(PopRefusal::Read)?; + let lookups = Cell::new(0usize); + let mut head_frame = vec![FRAME_NONE; base.n]; + for t in toks { + if t.head == 0 { + continue; + } + let i = usize::from(map.local(t.gid).map_err(PopRefusal::Map)?); + lookups.set(lookups.get() + 1); + let head = toks.iter().find(|h| h.gid == t.head); + head_frame[i] = head.map_or(FRAME_NONE, |h| lex.frame(h.lemma)); + } + Ok(FramedPopulation { + base, + head_frame, + lexicon_rev: lex.rev, + producer_lookups: lookups.get(), + }) + } +} + +/// Which physical form the description lowers to. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Physical { + Via, + CoAddressed, +} + +/// A candidate-role rule as a relational description (data, not code). +#[derive(Clone, Debug)] +pub struct RuleDesc { + pub method: MethodId, + pub name: &'static str, + pub deprel: Option<&'static str>, + pub case: Option<&'static str>, + /// `None` = the head-frame condition removed (control 1). + pub frame: Option, +} + +/// Resolved ids a description needs (cold). +#[derive(Clone, Copy, Debug)] +struct Bound { + deprel: u32, + case: u32, +} + +impl RuleDesc { + pub fn recipient() -> Self { + RuleDesc { + method: RECIPIENT, + name: "CandidateRecipient", + deprel: Some("obl:arg"), + case: Some("Dat"), + frame: Some(FRAME_GIVE), + } + } + + pub fn experiencer() -> Self { + RuleDesc { + method: EXPERIENCER, + name: "CandidateExperiencer", + deprel: Some("obl:arg"), + case: Some("Dat"), + frame: Some(FRAME_EXPERIENCE), + } + } + + fn bound(&self, v: &Vocab) -> Bound { + Bound { + deprel: self.deprel.map_or(0, |d| v.get(d)), + case: self.case.map_or(0, |c| v.get(c)), + } + } + + /// FNV-1a over the frame's lemma set and the lexicon revision: the only + /// identity a `Sym` leaf can carry for the Via form. + pub fn frame_digest(&self, lex: &Lexicon) -> u32 { + let mut h: u32 = 0x811c_9dc5; + let mut eat = |b: &[u8]| { + for &x in b { + h ^= u32::from(x); + h = h.wrapping_mul(0x0100_0193); + } + }; + eat(&lex.rev.to_le_bytes()); + eat(lex.language.as_bytes()); + if let Some(f) = self.frame { + for l in lex.lemmas(f) { + eat(l.as_bytes()); + eat(&[0]); + } + } + h + } + + /// The WHEN this description binds as. + pub fn guard(&self, phys: Physical, v: &Vocab, lex: &Lexicon) -> Guard { + let b = self.bound(v); + let mut parts = Vec::new(); + if self.deprel.is_some() { + parts.push(SetExpr::eq_u32(DEPREL, b.deprel)); + } + if self.case.is_some() { + parts.push(SetExpr::eq_u32(CASE, b.case)); + } + if let Some(f) = self.frame { + parts.push(match phys { + // Only an opaque symbol can stand for a hop. + Physical::Via => SetExpr::Sym(self.frame_digest(lex)), + // Row-local: stated in full. + Physical::CoAddressed => SetExpr::eq_u32(HEAD_FRAME, f), + }); + } + Guard::new(SetExpr::And(parts), Logic::TwoValued) + } + + /// The relational description in Quack's vocabulary, scoped by the + /// global WHERE plane (`Mask(0)`). + pub fn filter(&self, phys: Physical, v: &Vocab, lex: &Lexicon) -> Filter { + let b = self.bound(v); + let mut parts = vec![Filter::plane(Mask(0))]; + if self.deprel.is_some() { + parts.push(Filter::cmp(Col(DEPREL), Cmp::EqU32(b.deprel))); + } + if self.case.is_some() { + parts.push(Filter::cmp(Col(CASE), Cmp::EqU32(b.case))); + } + if let Some(f) = self.frame { + parts.push(match phys { + Physical::Via => Filter::or( + lex.lemmas(f) + .into_iter() + .map(|l| Filter::eq_u32_via(Col(HEAD), ForeignLane(0), v.get(l))), + ), + Physical::CoAddressed => Filter::cmp(Col(HEAD_FRAME), Cmp::EqU32(f)), + }); + } + Filter::and(parts) + } + + /// The DT64 binding: read-only (no effects), reading every field. + pub fn binding(&self, phys: Physical, v: &Vocab, lex: &Lexicon) -> MethodBinding { + MethodBinding { + id: self.method, + sig_rev: SigRev(1), + name: self.name.to_string(), + on: WideFieldMask::from_positions(&[1, 2, 3]), + when: Some(self.guard(phys, v, lex)), + reads: WideFieldMask::from_positions(&[0, 1, 2, 3, 4]), + effects: Vec::new(), + population: Multiplicity::Distinct, + truth: Truth::TwoValued, + demand: ValueDemand::Values, + } + } +} + +pub fn schema() -> ClassSchema { + ClassSchema { + schema_rev: SchemaRev(1), + field_count: FIELDS, + extent: Extent::DR256_SQ_X64, + } +} + +/// Register both candidate methods for `class`. +pub fn register( + store: &mut BindStore, + class: u32, + phys: Physical, + rules: &[RuleDesc], + v: &Vocab, + lex: &Lexicon, +) -> Result<(), Refusal> { + store.register( + class, + schema(), + rules.iter().map(|r| r.binding(phys, v, lex)).collect(), + ) +} + +/// Why the composer refused. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ComposeRefusal { + Binding(Refusal), + /// The method writes: not a read-only candidate. + NotReadOnly, + NoGuard, + /// The description given does not produce the bound guard's witness. + DescriptionMismatch, + Lower(LowerError), +} + +/// Why a composed run refused. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum RunRefusal { + Frame(PopRefusal), + /// The population was produced under another lexicon revision. + LexiconRevision { bound: u64, population: u64 }, + /// The WHERE plane is not over this population. + WhereShape, +} + +/// One admitted method, its description inlined with the WHERE plane into +/// one program. Cold to build; hot to run. +pub struct Composed { + pub method: MethodRef, + pub phys: Physical, + pub lexicon_rev: u64, + program: Program, + scratch: Scratch<'static>, + out: Vec, +} + +/// Approach C (lab): admit, check the description against the bound witness, +/// lower once. +pub fn compose( + store: &BindStore, + mref: &MethodRef, + desc: &RuleDesc, + phys: Physical, + v: &Vocab, + lex: &Lexicon, +) -> Result { + let b = store.admit(mref).map_err(ComposeRefusal::Binding)?; + if !b.effects.is_empty() { + return Err(ComposeRefusal::NotReadOnly); + } + let bound = b.when.as_ref().ok_or(ComposeRefusal::NoGuard)?; + if desc.guard(phys, v, lex).witness() != bound.witness() { + return Err(ComposeRefusal::DescriptionMismatch); + } + let program = lower(&Query { + filter: desc.filter(phys, v, lex), + agg: Agg::Rows, + }) + .map_err(ComposeRefusal::Lower)?; + let words = words_for(WIDTH.positions()); + Ok(Composed { + method: mref.clone(), + phys, + lexicon_rev: lex.rev, + scratch: Scratch::new(words, program.scratch_slots as usize), + program, + out: vec![0; words], + }) +} + +impl Composed { + /// Program size (mask ops). + pub fn ops(&self) -> usize { + self.program.ops.len() + } + + /// Hot: one program over borrowed lanes and the shared WHERE plane. + pub fn run( + &mut self, + pop: &FramedPopulation, + table: &MapTable, + frame: &Frame, + where_plane: &[u64], + ) -> Result<[u64; 4], RunRefusal> { + let map = table + .map(frame, TILE) + .map_err(|e| RunRefusal::Frame(PopRefusal::Read(e)))?; + if map.len() != pop.base.n { + return Err(RunRefusal::Frame(PopRefusal::Map( + lance_graph_dt64::dr::MapRefusal::OutOfTile, + ))); + } + if pop.lexicon_rev != self.lexicon_rev { + return Err(RunRefusal::LexiconRevision { + bound: self.lexicon_rev, + population: pop.lexicon_rev, + }); + } + let words = words_for(pop.base.n); + if where_plane.len() != words { + return Err(RunRefusal::WhereShape); + } + let p = &pop.base; + let lanes = [ + LaneRef::U32(&p.lemma), + LaneRef::U32(&p.deprel), + LaneRef::U32(&p.case), + LaneRef::U32(&p.head), + LaneRef::U32(&pop.head_frame), + ]; + let flanes = [LaneRef::U32(&p.lemma)]; + let masks = [where_plane]; + let planes = Planes { + n_rows: p.n, + masks: &masks, + lanes: &lanes, + }; + let foreign = Foreign { + planes: &[], + lanes: &flanes, + }; + execute_into( + &self.program, + &planes, + &foreign, + &mut self.scratch, + Out::Mask(&mut self.out[..words]), + ) + .expect("composed program is valid"); + let mut r = [0u64; 4]; + r[..words].copy_from_slice(&self.out[..words]); + Ok(r) + } +} + +// Lane-index sanity: the lab class fields are the lanes, in order. +const _: () = assert!(LEMMA == 0 && DEPREL == 1 && CASE == 2 && HEAD == 3 && HEAD_FRAME == 4); diff --git a/crates/grammar-constraints-probe/tests/when.rs b/crates/grammar-constraints-probe/tests/when.rs new file mode 100644 index 000000000..1289acb24 --- /dev/null +++ b/crates/grammar-constraints-probe/tests/when.rs @@ -0,0 +1,422 @@ +//! D-GRAMMAR-WHEN-1 falsifier. Each control states its predicted outcome in +//! its doc comment, written before it was run. + +use std::alloc::{GlobalAlloc, Layout, System}; +use std::cell::Cell; + +use grammar_constraints_probe::fixtures::{self, Gold, A, B, C, GOLD}; +use grammar_constraints_probe::when::*; +use grammar_constraints_probe::{has, tile, Ids, Operands, Refusal as PopRefusal, Rules, Tok, Vocab, TILE}; +use lance_graph_contract::set_algebra::{Logic, SetExpr}; +use lance_graph_dt64::dr::{Frame, MapRead, MapRefusal, MapTable}; +use lance_graph_dt64::{ + AlgebraRef, Arg, BindStore, Effect, Extent, Guard, MethodRef, Refusal, SchemaRev, +}; + +thread_local! { static BYTES: Cell = const { Cell::new(0) }; } +struct Counting; +unsafe impl GlobalAlloc for Counting { + unsafe fn alloc(&self, l: Layout) -> *mut u8 { + let _ = BYTES.try_with(|b| b.set(b.get() + l.size())); + System.alloc(l) + } + unsafe fn dealloc(&self, p: *mut u8, l: Layout) { + System.dealloc(p, l) + } +} +#[global_allocator] +static ALLOC: Counting = Counting; + +// --- harness ------------------------------------------------------------------ + +struct W { + v: Vocab, + table: MapTable, + frame: Frame, + pop: FramedPopulation, + store: BindStore, + lex: Lexicon, +} + +fn world_with(toks: &[Tok], lex: Lexicon) -> W { + let mut v = Vocab::new(); + let _ = Ids::bind(&mut v); + let (table, frame) = tile(9, &fixtures::gids(toks)); + let pop = FramedPopulation::produce(toks, &mut v, &table, &frame, &lex).unwrap(); + let mut store = BindStore::new(); + let rules = [RuleDesc::recipient(), RuleDesc::experiencer()]; + register(&mut store, CLASS_VIA, Physical::Via, &rules, &v, &lex).unwrap(); + register(&mut store, CLASS_COADDR, Physical::CoAddressed, &rules, &v, &lex).unwrap(); + W { + v, + table, + frame, + pop, + store, + lex, + } +} + +fn world(toks: &[Tok]) -> W { + world_with(toks, Lexicon::v0()) +} + +fn class_of(p: Physical) -> u32 { + match p { + Physical::Via => CLASS_VIA, + Physical::CoAddressed => CLASS_COADDR, + } +} + +fn mref(w: &W, class: u32, desc: &RuleDesc, p: Physical) -> MethodRef { + MethodRef::of(class, &desc.binding(p, &w.v, &w.lex)) +} + +fn all_plane(w: &W) -> Vec { + let n = w.pop.base.n; + let mut m = vec![0u64; n.div_ceil(64)]; + for i in 0..n { + m[i / 64] |= 1 << (i % 64); + } + m +} + +fn plane_of(w: &W, gids: &[u64]) -> Vec { + let map = w.table.map(&w.frame, TILE).unwrap(); + let mut m = vec![0u64; w.pop.base.n.div_ceil(64)]; + for &g in gids { + let l = usize::from(map.local(g).unwrap()); + m[l / 64] |= 1 << (l % 64); + } + m +} + +fn gids_of(w: &W, mask: &[u64; 4]) -> Vec { + let map = w.table.map(&w.frame, TILE).unwrap(); + let mut v: Vec = (0..w.pop.base.n as u8) + .filter(|&l| has(mask, l)) + .map(|l| map.global(l).unwrap()) + .collect(); + v.sort_unstable(); + v +} + +/// Compose and run `desc` under its own registered binding. +fn answer(w: &W, desc: &RuleDesc, p: Physical, plane: &[u64]) -> Vec { + let r = mref(w, class_of(p), desc, p); + let mut c = compose(&w.store, &r, desc, p, &w.v, &w.lex).unwrap(); + let m = c.run(&w.pop, &w.table, &w.frame, plane).unwrap(); + gids_of(w, &m) +} + +/// Independent oracle: string-level, over the token structs, no ids, no +/// programs. +fn oracle(toks: &[Tok], lex: &Lexicon, frame: u32) -> Vec { + let lemmas = lex.lemmas(frame); + let mut v: Vec = toks + .iter() + .filter(|t| t.deprel == "obl:arg" && t.case == "Dat") + .filter(|t| { + toks.iter() + .find(|h| h.gid == t.head) + .is_some_and(|h| lemmas.contains(&h.lemma)) + }) + .map(|t| t.gid) + .collect(); + v.sort_unstable(); + v +} + +const BOTH: [Physical; 2] = [Physical::Via, Physical::CoAddressed]; + +// --- P0 ------------------------------------------------------------------------- + +#[test] +fn p0_both_forms_match_oracle_and_gold() { + let corpus = fixtures::corpus(); + let w = world(&corpus); + let all = all_plane(&w); + for p in BOTH { + let rec = answer(&w, &RuleDesc::recipient(), p, &all); + let exp = answer(&w, &RuleDesc::experiencer(), p, &all); + assert_eq!(rec, oracle(&corpus, &w.lex, FRAME_GIVE), "{p:?}"); + assert_eq!(exp, oracle(&corpus, &w.lex, FRAME_EXPERIENCE), "{p:?}"); + assert_eq!(rec, vec![105, 405], "{p:?}"); + assert_eq!(exp, vec![302], "{p:?}"); + } + // gold agreement (independent annotation) + for (gid, g) in GOLD { + let rec = answer(&w, &RuleDesc::recipient(), Physical::CoAddressed, &all); + let exp = answer(&w, &RuleDesc::experiencer(), Physical::CoAddressed, &all); + assert_eq!(rec.contains(&gid), g == Gold::Recipient, "{gid}"); + assert_eq!(exp.contains(&gid), g == Gold::Experiencer, "{gid}"); + } +} + +#[test] +fn guards_keep_distinct_witnesses_in_both_forms() { + let w = world(&fixtures::corpus()); + for p in BOTH { + let r = RuleDesc::recipient().guard(p, &w.v, &w.lex).witness(); + let e = RuleDesc::experiencer().guard(p, &w.v, &w.lex).witness(); + assert_ne!(r, e, "{p:?}"); + } + // ...but without the frame part, they coincide (the #1947 finding). + let strip = |mut d: RuleDesc| { + d.frame = None; + d.guard(Physical::CoAddressed, &w.v, &w.lex).witness() + }; + assert_eq!(strip(RuleDesc::recipient()), strip(RuleDesc::experiencer())); +} + +#[test] +fn unknown_stays_unknown_and_ambiguity_is_kept() { + // helfen (E): no frame entry → no candidate in either method, and the + // #1947 abstention rule still reports it UNKNOWN. + let corpus = fixtures::corpus(); + let w = world(&corpus); + let all = all_plane(&w); + for p in BOTH { + assert!(!answer(&w, &RuleDesc::recipient(), p, &all).contains(&505)); + assert!(!answer(&w, &RuleDesc::experiencer(), p, &all).contains(&505)); + } + assert_eq!(w.pop.head_frame[usize::from(local(&w, 505))], FRAME_NONE); + let mut v = Vocab::new(); + let ids = Ids::bind(&mut v); + let pop = grammar_constraints_probe::Population::bind(&corpus, &mut v, &w.table, &w.frame).unwrap(); + let mut rules = Rules::prepare(&ids, Operands::ALL); + let r = rules.run(&pop, &w.table, &w.frame).unwrap(); + assert!(has(&r.abstain_frame, local(&w, 505))); + // control 9: Direction AND Purpose both kept for Schule + assert!(has(&r.direction_or_purpose, local(&w, 208))); +} + +fn local(w: &W, gid: u64) -> u8 { + w.table.map(&w.frame, TILE).unwrap().local(gid).unwrap() +} + +#[test] +fn candidates_are_read_only() { + let w = world(&fixtures::corpus()); + for p in BOTH { + for d in [RuleDesc::recipient(), RuleDesc::experiencer()] { + let b = w.store.admit(&mref(&w, class_of(p), &d, p)).unwrap(); + assert!(b.effects.is_empty() && b.writes() == lance_graph_contract::class_view::WideFieldMask::EMPTY); + } + } + // A method with an effect is refused by the composer. + let mut store = BindStore::new(); + store + .declare_algebra(0x7F30_0000, SchemaRev(1), Extent::DR64_CUBE, vec![1]) + .unwrap(); + let mut b = RuleDesc::recipient().binding(Physical::CoAddressed, &w.v, &w.lex); + b.effects = vec![Effect { + target: 4, + algebra: AlgebraRef { lens: 0x7F30_0000, word: 0 }, + args: vec![Arg::Field(1)], + }]; + store.register(CLASS_COADDR, schema(), vec![b.clone()]).unwrap(); + let r = MethodRef::of(CLASS_COADDR, &b); + assert_eq!( + compose(&store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).err(), + Some(ComposeRefusal::NotReadOnly) + ); +} + +#[test] +fn dt64_does_not_validate_guard_lanes() { + // FINDING: `validate` checks ON / reads / effects positions against the + // basis, never the WHEN guard's lanes. A guard over lane 99 of a + // five-field class registers. + let w = world(&fixtures::corpus()); + let mut b = RuleDesc::recipient().binding(Physical::CoAddressed, &w.v, &w.lex); + b.when = Some(Guard::new(SetExpr::eq_u32(99, 1), Logic::TwoValued)); + let mut store = BindStore::new(); + assert!(store.register(CLASS_COADDR, schema(), vec![b]).is_ok()); +} + +// --- negative controls --------------------------------------------------------- + +/// 1. Head-frame condition removed. PREDICTED: recipient fires on 105, 302, +/// 405, 505 (both rules collapse onto obl:arg ∧ Dat). +#[test] +fn n01_remove_head_frame() { + let corpus = fixtures::corpus(); + let w = world(&corpus); + let mut d = RuleDesc::recipient(); + d.frame = None; + let mut store = BindStore::new(); + register(&mut store, CLASS_COADDR, Physical::CoAddressed, std::slice::from_ref(&d), &w.v, &w.lex).unwrap(); + let r = MethodRef::of(CLASS_COADDR, &d.binding(Physical::CoAddressed, &w.v, &w.lex)); + let mut c = compose(&store, &r, &d, Physical::CoAddressed, &w.v, &w.lex).unwrap(); + let m = c.run(&w.pop, &w.table, &w.frame, &all_plane(&w)).unwrap(); + assert_eq!(gids_of(&w, &m), vec![105, 302, 405, 505]); + // and the stripped description no longer matches the bound guard + let bound = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + assert_eq!( + compose(&w.store, &bound, &d, Physical::CoAddressed, &w.v, &w.lex).err(), + Some(ComposeRefusal::DescriptionMismatch) + ); +} + +/// 2. GIVE and EXPERIENCE frames swapped in the lexicon. PREDICTED: +/// Via — the bound Sym(digest) no longer matches → DescriptionMismatch; +/// CoAddressed — a population produced under the swapped lexicon (rev 2) +/// is refused by a method composed under rev 1; recomposed honestly under +/// rev 2, the answers swap (105 → experiencer). +#[test] +fn n02_swap_frames() { + let corpus = fixtures::corpus(); + let w = world(&corpus); + let swapped = Lexicon::swapped(); + let bound = mref(&w, CLASS_VIA, &RuleDesc::recipient(), Physical::Via); + assert_eq!( + compose(&w.store, &bound, &RuleDesc::recipient(), Physical::Via, &w.v, &swapped).err(), + Some(ComposeRefusal::DescriptionMismatch) + ); + let ws = world_with(&corpus, swapped); + let r = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + let mut c = compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).unwrap(); + assert_eq!( + c.run(&ws.pop, &ws.table, &ws.frame, &all_plane(&ws)).err(), + Some(RunRefusal::LexiconRevision { bound: 1, population: 2 }) + ); + assert_eq!(answer(&ws, &RuleDesc::experiencer(), Physical::CoAddressed, &all_plane(&ws)), vec![105, 405]); + assert_eq!(answer(&ws, &RuleDesc::recipient(), Physical::CoAddressed, &all_plane(&ws)), vec![302]); +} + +/// 3. Dative → accusative on Kind (A). PREDICTED: no candidate for 105. +#[test] +fn n03_dative_to_accusative() { + let mut a = A; + a[4].case = "Acc"; + let w = world(&a); + for p in BOTH { + assert!(answer(&w, &RuleDesc::recipient(), p, &all_plane(&w)).is_empty()); + } +} + +/// 4. Dependency reversed (Kind heads the verb). PREDICTED: no candidate. +#[test] +fn n04_reversed_dependency() { + let mut a = A; + a[2].head = 105; + a[2].deprel = "obl:arg"; + a[2].case = "Dat"; + a[4].head = 0; + a[4].deprel = "root"; + let w = world(&a); + for p in BOTH { + assert!(answer(&w, &RuleDesc::recipient(), p, &all_plane(&w)).is_empty(), "{p:?}"); + } +} + +/// 5. The referenced head removed from the population. PREDICTED: a typed +/// refusal at binding (Unmapped), never a FALSE role. +#[test] +fn n05_missing_head() { + let a: Vec = A.iter().copied().filter(|t| t.gid != 103).collect(); + let mut v = Vocab::new(); + let (table, frame) = tile(9, &fixtures::gids(&a)); + let r = FramedPopulation::produce(&a, &mut v, &table, &frame, &Lexicon::v0()); + assert!(matches!(r, Err(PopRefusal::Map(MapRefusal::Unmapped)))); +} + +/// 6. Stale (foreign) frame. PREDICTED: Stale refusal. +#[test] +fn n06_foreign_frame() { + let w = world(&A); + let (_t, foreign) = tile(9, &fixtures::gids(&A)); + let r = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + let mut c = compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).unwrap(); + assert!(matches!( + c.run(&w.pop, &w.table, &foreign, &all_plane(&w)), + Err(RunRefusal::Frame(PopRefusal::Read(MapRead::Stale(_)))) + )); +} + +/// 7. Foreign classid. PREDICTED: UnknownClass from admit. +#[test] +fn n07_foreign_class() { + let w = world(&A); + let r = mref(&w, CLASS_FOREIGN, &RuleDesc::recipient(), Physical::CoAddressed); + assert_eq!( + compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).err(), + Some(ComposeRefusal::Binding(Refusal::UnknownClass(CLASS_FOREIGN))) + ); +} + +/// 8. One supporting operand (deprel) removed. PREDICTED: against the bound +/// guard → DescriptionMismatch; under its own binding the instrument +/// Löffel (408, obl, Dat, under geben) becomes a recipient. +#[test] +fn n08_remove_operand() { + let corpus = fixtures::corpus(); + let w = world(&corpus); + let mut d = RuleDesc::recipient(); + d.deprel = None; + let bound = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + assert_eq!( + compose(&w.store, &bound, &d, Physical::CoAddressed, &w.v, &w.lex).err(), + Some(ComposeRefusal::DescriptionMismatch) + ); + let mut store = BindStore::new(); + register(&mut store, CLASS_COADDR, Physical::CoAddressed, std::slice::from_ref(&d), &w.v, &w.lex).unwrap(); + let r = MethodRef::of(CLASS_COADDR, &d.binding(Physical::CoAddressed, &w.v, &w.lex)); + let mut c = compose(&store, &r, &d, Physical::CoAddressed, &w.v, &w.lex).unwrap(); + let got = gids_of(&w, &c.run(&w.pop, &w.table, &w.frame, &all_plane(&w)).unwrap()); + assert!(got.contains(&408), "{got:?}"); +} + +/// 10. One global WHERE plane reused by both methods. PREDICTED: with W = +/// tokens of A and C only, recipient = {105}, experiencer = {302}; equal +/// to the unscoped answer ∩ W; W = all gives the unscoped answer. +#[test] +fn n10_shared_where_plane() { + let corpus = fixtures::corpus(); + let w = world(&corpus); + let ac: Vec = A.iter().chain(C.iter()).map(|t| t.gid).collect(); + let scoped = plane_of(&w, &ac); + for p in BOTH { + let rec = answer(&w, &RuleDesc::recipient(), p, &scoped); + let exp = answer(&w, &RuleDesc::experiencer(), p, &scoped); + assert_eq!(rec, vec![105]); + assert_eq!(exp, vec![302]); + let full = answer(&w, &RuleDesc::recipient(), p, &all_plane(&w)); + let inter: Vec = full.into_iter().filter(|g| ac.contains(g)).collect(); + assert_eq!(rec, inter); + } + // B's Schule is outside W: no rule here can name it + let _ = B; +} + +// --- physical form --------------------------------------------------------------- + +#[test] +fn coaddressed_query_has_no_via_and_via_query_does() { + let w = world(&fixtures::corpus()); + for (p, want_via) in [(Physical::Via, true), (Physical::CoAddressed, false)] { + let f = RuleDesc::recipient().filter(p, &w.v, &w.lex); + let dbg = format!("{f:?}"); + assert_eq!(dbg.contains("EqU32Via"), want_via, "{p:?}"); + } + // the producer did the cross-row reads once, counted: one per non-root token + let non_root = fixtures::corpus().iter().filter(|t| t.head != 0).count(); + assert_eq!(w.pop.producer_lookups, non_root); +} + +#[test] +fn hot_run_allocates_nothing() { + let w = world(&fixtures::corpus()); + let all = all_plane(&w); + for p in BOTH { + let r = mref(&w, class_of(p), &RuleDesc::recipient(), p); + let mut c = compose(&w.store, &r, &RuleDesc::recipient(), p, &w.v, &w.lex).unwrap(); + let _ = c.run(&w.pop, &w.table, &w.frame, &all).unwrap(); + let before = BYTES.with(|b| b.get()); + for _ in 0..1000 { + let _ = c.run(&w.pop, &w.table, &w.frame, &all).unwrap(); + } + assert_eq!(BYTES.with(|b| b.get()) - before, 0, "{p:?}"); + } +} From 956e4d503cb260a4e69ece11941adb3e4cf20d5b Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 21:39:21 +0000 Subject: [PATCH 2/4] D-GRAMMAR-WHEN-1: binding a grammatical WHEN through DT64 (lab) Source audit and lab falsifier for two read-only DT64 methods, CandidateRecipient and CandidateExperiencer, that share obl:arg + Case=Dat and differ in the head verb's frame. Extends crates/grammar-constraints-probe (src/when.rs, tests/when.rs, examples/when_cost.rs). - The #1947 head hop (Pred::EqU32Via, foreign[fk[i]]) is gather-shaped: ADMISSION B does not admit a position derived from another column as a read address, and EXO-140 is still unclassified. A correction note is added to the #1947 report. - DT64 states the dependent's own conditions but not the head frame (only an opaque Sym); admit checks witness equality only; validate does not check guard lanes; no read-only DO exists; R2IL still refuses WHEN. - Co-addressed form ("the join is the layout"): the head's frame as a lane at the dependent's coordinate makes the WHEN row-local in today's SetExpr with distinct witnesses and no EqU32Via in the query. The cross-row read moves into a counted producer (EXO-46 / D-RMAP-1). - Lab composer: admit, check description against witness, lower description and a shared global WHERE into one program. Both forms match an independent oracle and gold; 10 negative controls as predicted; 9 source disables red; 0 B per hot run. No production change, no ClassId, no F###. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMLBmi7EtDd15CGwGb8 --- .../entries/2026-11-03-d-grammar-when-1.md | 36 +++ .claude/board/entries/README.md | 3 +- .../REPORT.md | 10 + .../2026-11-03-d-grammar-when-1/REPORT.md | 264 ++++++++++++++++++ .../examples/when_cost.rs | 72 +++++ crates/grammar-constraints-probe/src/when.rs | 9 +- .../grammar-constraints-probe/tests/when.rs | 185 ++++++++++-- 7 files changed, 550 insertions(+), 29 deletions(-) create mode 100644 .claude/board/entries/2026-11-03-d-grammar-when-1.md create mode 100644 .claude/probes/2026-11-03-d-grammar-when-1/REPORT.md create mode 100644 crates/grammar-constraints-probe/examples/when_cost.rs diff --git a/.claude/board/entries/2026-11-03-d-grammar-when-1.md b/.claude/board/entries/2026-11-03-d-grammar-when-1.md new file mode 100644 index 000000000..5503a0a37 --- /dev/null +++ b/.claude/board/entries/2026-11-03-d-grammar-when-1.md @@ -0,0 +1,36 @@ +# D-GRAMMAR-WHEN-1: binding a grammatical WHEN through DT64 (2026-11-03) + +**Status:** measured, lab only. Probe `crates/grammar-constraints-probe` (`src/when.rs`, `tests/when.rs`, `examples/when_cost.rs`); report `.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md`. No production change, no ClassId, no `F###`. + +## Measured + +- **The #1947 head hop is gather-shaped.** + - #1947 used `Pred::EqU32Via`, which reads `foreign[fk[i]]`. + - ADMISSION B: "a position derived from another relational column or table is not admissible as a read address … Execution remains co-addressed." + - The 2026-10-16 banner bans reads at a position taken from another lane's value. + - Its sibling `EqU32ViaLane` is marked VIOLATION (D-ASM-11A). + - No ruling admits `EqU32Via`; EXO-140 is still OPEN. +- **DT64 can state the dependent's own conditions, but not the head frame.** + - The only hop-shaped leaf is an opaque `Sym`, and `admit` checks witness equality only. + - `validate` never checks WHEN lanes against the class basis (pinned by a test). + - No read-only "returns" DO exists. + - R2IL `prepare` still refuses any WHEN (`GuardNotExecutable`); its integration suite passes 52/52. +- **A co-addressed form ("the join is the layout") makes the WHEN row-local in today's SetExpr.** + - The head's frame is written as a lane at the dependent's own coordinate, so the WHEN needs no `Sym`, and the two guards keep distinct witnesses. + - The query needs no `EqU32Via`: 10 ops, about 0.41–0.47 µs for both methods over 40 tokens, against 0.56–0.57 µs via the hop. + - The cross-row read moves into the producer, which does it once and counted (35 lookups). +- **Lab composer (approach C): admit → check description vs witness → lower description ∧ shared WHERE into ONE program.** + - Both forms match an independent oracle and the gold. + - 10 negative controls behave as predicted; 9 source disables go red. + +## Open (owner) + +- **EXO-140:** classify `EqU32Via`. Proposed, nonbinding: gather-class, not admitted on the query path. +- **EXO-46 / D-RMAP-1:** admit, or refuse, a witnessed sequential producer for co-addressed relation lanes. +- **D-DT64-6:** three open questions. + - A verified description identity in place of an opaque `Sym`. + - Checking guard lanes in `validate`. + - A read-only DO. +- **Frame lexicon:** an owner, a revision and a language scope (`LanguageId` exists). +- **Role identity:** CE64 `Orientation` (one code: `Core`+7) vs `DativeFunction` (a set of 8 incl. Judicantis). The 7 shared functions are offset by one. +- **Candidate promotion:** a selection policy, plus the hydration / Rubicon gate. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 32bea6719..2a3ff806c 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,11 +25,12 @@ 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. -566 entries, 2026-08-06 .. 2026-11-03. +567 entries, 2026-08-06 .. 2026-11-03. | date | entry id | finding | file | |---|---|---|---| | 2026-11-03 | `D-XLOG-META-WIRE-P0` | | [2026-11-03-d-xlog-meta-wire-p0.md](2026-11-03-d-xlog-meta-wire-p0.md) | +| 2026-11-03 | `D-GRAMMAR-WHEN-1` | | [2026-11-03-d-grammar-when-1.md](2026-11-03-d-grammar-when-1.md) | | 2026-11-03 | `D-GRAMMAR-CONSTRAINTS-0` | | [2026-11-03-d-grammar-constraints-0.md](2026-11-03-d-grammar-constraints-0.md) | | 2026-11-03 | `D-GLOBAL-WHERE` | | [2026-11-03-d-global-where-p0.md](2026-11-03-d-global-where-p0.md) | | 2026-11-03 | `D-DR-FOLD-MAP` | | [2026-11-03-d-dr-fold-map.md](2026-11-03-d-dr-fold-map.md) | diff --git a/.claude/probes/2026-11-03-d-grammar-constraints/REPORT.md b/.claude/probes/2026-11-03-d-grammar-constraints/REPORT.md index 3b6d22028..489d8a4b9 100644 --- a/.claude/probes/2026-11-03-d-grammar-constraints/REPORT.md +++ b/.claude/probes/2026-11-03-d-grammar-constraints/REPORT.md @@ -1,5 +1,15 @@ # D-GRAMMAR-CONSTRAINTS-0 — grammatical constraints × RelAlg × CE64/DT64 +> **⊘ CORRECTION (D-GRAMMAR-WHEN-1, 2026-11-03).** This report says the head hop +> `Pred::EqU32Via` "executes; call sites EXO-140-unclassified". That is true but +> understated. ADMISSION B (`entries/2026-10-20-six-decisions.md:26-34`) says "a +> position derived from another relational column or table is not admissible as +> a read address", and the 2026-10-16 banner calls a read "at a position taken +> from another lane's values" a violation. `EqU32Via` reads `foreign[fk[i]]`, so +> it is gather-shaped, and no ruling admits it. The results below stand as LAB. +> The co-addressed alternative, and the owner decisions it raises, are in +> `.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md`. + **Date:** 2026-11-03. **Status:** RESEARCH + LAB PROBE. - Probe: `crates/grammar-constraints-probe`. It has its own workspace and is excluded from the root workspace. diff --git a/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md b/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md new file mode 100644 index 000000000..90c7659f2 --- /dev/null +++ b/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md @@ -0,0 +1,264 @@ +# D-GRAMMAR-WHEN-1 — relational guard binding × DT64 × global WHERE + +**Date:** 2026-11-03. **Status:** SOURCE AUDIT + LAB PROBE. + +- **Base:** `main` @ `0df42b9` (the #1947 merge). +- **Probe:** `crates/grammar-constraints-probe`. + - New module `src/when.rs`. + - New tests `tests/when.rs`. + - New example `examples/when_cost.rs`. +- **Not changed:** no production code, no ClassId mint, no `F###`, no executor. Nothing here is an admission. + +**Question:** can DT64 bind and invoke the meaning of a grammatical WHEN lawfully? The case is two read-only methods that share `obl:arg ∧ Case=Dat` and differ in the head verb's frame. + +--- + +## 0. Correction to #1947 (stated first, because it changes the answer) + +#1947 said the head hop `Pred::EqU32Via` "executes; its call sites are EXO-140-unclassified". That is true but understated. Source: + +- **ADMISSION B, the operator's words** (`.claude/board/entries/2026-10-20-six-decisions.md:26-34`): + > "A position derived from another relational column or table is not admissible as a read address merely because the lookup occurs during preparation. … Execution remains co-addressed." +- **The same entry, `:46-48`:** + > "`Filter::Semijoin`, `Pred::EqU32Via` and `MaskOp::Gather` need call-site classification before any removal." +- **The 2026-10-16 banner** (`entries/2026-10-16-wcoj-probes-1-3.md:3`) calls a read + > "AT A POSITION TAKEN FROM ANOTHER LANE'S VALUES" + + a violation. The correct shape is `Thought(t)[T_a[i] : T_b[i]]`: "THE JOIN IS THE LAYOUT". +- **Sibling atom.** `EqU32ViaLane`, a sibling closing atom, is marked "⛔ VIOLATION — GATHER. DO NOT BUILD" (`STATUS_BOARD.md:580`, D-ASM-11A). + +`EqU32Via` reads `foreign[fk[i]]`. That is exactly a position taken from another lane's value. **No text admits it. It is not forbidden by an explicit ruling either: it is unclassified, and gather-shaped by the rulings' own definition.** #1947's lab result stands as LAB. Its physical mechanism is in the disputed class. + +## 1. Source-backed wiring map + +| arrow | exists? | source | +|---|---|---| +| Global WHERE (Quack `Plane`/`Keep`) | yes, production | `lance-graph-quack/src/lib.rs` `Filter::Plane` | +| DR population + frame check | yes | `lance-graph-dt64/src/dr.rs` `LocalMap`, `MapTable::map` | +| DT64 `MethodBinding` ON × WHEN × DO | yes | `lance-graph-dt64/src/lib.rs:197` | +| WHEN = `Guard{SetExpr, Logic}` | yes, single population | `lib.rs:152`; `set_algebra.rs:135` (`Sym`, `Res::{I32,U32}`, `And/Or/Not`) | +| `admit` checks the guard | **witness equality only** | `lib.rs:832-858` | +| `validate` checks guard lanes | **no.** ON/reads/effects are checked; WHEN lanes are not | `lib.rs:900-955`; test `dt64_does_not_validate_guard_lanes` | +| A read-only ("returns") DO | **no.** Every `Effect` writes a `target` field | `lib.rs:128-137` | +| `SetExpr` ↔ relational description | relalg `Rel` ↔ `SetExpr` (single table) | `lance-graph-relalg/src/normalize.rs:82-105` | +| `SetExpr` → mask-risc | yes, `set_lower` (D-CMR-2, same-table runs) | `lance-graph/src/fold/set_lower.rs` | +| RelAlg hop / join atom | **no**: `Rel` = `All/Empty/Plane/Atom/And/Or/Not` | `lance-graph-relalg/src/ir.rs:47` | +| Quack head hop | `Filter::EqU32Via` → `Pred::EqU32Via` | `lance-graph-quack/src/lib.rs:358`; `mask-risc/src/ir.rs:158` | +| R2IL WHEN execution | **refused**: `GuardNotExecutable` (`binding.rs:291`), `ThreeValuedNotExecutable` (`:293`) | re-run: `what_the_reading_cannot_honour_is_refused_at_prepare` ok, r2il integration 52/52 | +| R2IL is mandatory? | **no**: "A consumer executes its own prepared native plan … without consulting any codegraph" | `binding.rs:6-10` | +| Read-only admission policy | LAB: `Admitted::Pure` | `crates/dt64-admission-probe/src/lib.rs` | +| Vector × tile fold (co-addressed hop) | **no** (LAB `relcomp` only) | `entries/2026-11-03-d-dr-fold-map.md` (C) | + +## 2. Actual DT64 / execution refusals + +The first typed refusal on each path: + +- **Production R2IL path.** `prepare` returns `ExecRefusal::GuardNotExecutable` for any WHEN, before any effect is read (`binding.rs:290-292`). +- **DT64 itself.** + - No refusal is reachable for the frame difference: `SetExpr` cannot state it. + - The only hop-shaped leaf is `Sym(u32)`, whose meaning "is the consumer's business" (`set_algebra.rs:140-142`). + - `admit` therefore accepts any `Sym` number the witness carries. Nothing checks what it means. +- **Lab composer (approach C).** The lab composer adds `DescriptionMismatch`, `NotReadOnly` and `LexiconRevision`. These are lab refusals, not production refusals. + +## 3. Approaches A / B / C + +| | A: hop leaf in `SetExpr` | B: WHEN references a prepared relational description | C: cold composition under a shared WHERE | +|---|---|---|---| +| What it is | e.g. `HeadLemmaEq(fk, foreign, v)` | WHEN carries an identity of a Quack/RelAlg description | admit → check description against the witness → lower description ∧ WHERE into ONE program | +| Expressible today | no | the description, **yes, in Quack** (`Filter::and[cmp, cmp, or[eq_u32_via…]]`). Not in RelAlg (`Rel` has no hop). DT64 can only point at it through an opaque `Sym` | **yes, lab** (`when::compose`); its physical op is whatever the description lowers to | +| Witness keeps the relation | yes, if the leaf names (fk lane, foreign lane, value) | **only by convention**: `Sym(digest)` (lab). The store does not verify the digest | via the description check (lab) | +| Duplicates RelAlg/Quack | yes: a second hop vocabulary | no | no | +| Leaks physical navigation into the guard | yes | no | no | +| Global→local authorization | none: the leaf would read `foreign[fk[i]]` in the hot path | same as the description | same | +| Admission | ADMISSION B text applies directly (gather-shaped) | the same, once lowered: `Pred::EqU32Via` | the same, **unless** the description is co-addressed (C′) | +| Hot cost (lab, 2 methods, 40 tokens) | n/a | n/a | Via form 0.56–0.57 µs/run, 12 ops | + +**C′, the co-addressed form ("the join is the layout").** The head's frame code is a lane at the DEPENDENT's own coordinate, `head_frame[i]`. + +- **WHEN.** It becomes row-local and fully stated in today's `SetExpr`: `And[eq_u32(DEPREL,·), eq_u32(CASE,·), eq_u32(HEAD_FRAME, GIVE)]`. +- **Witnesses.** They are distinct with no `Sym`. +- **Query.** It reads every lane at address `i`: no `EqU32Via`, 10 ops, 0.41–0.47 µs/run. +- **What remains.** The cross-row read moves into the producer, which writes `head_frame[i] = frame(lemma[head[i]])` once. The probe counts 35 lookups for 35 non-root tokens. +- **Open membrane.** That producer step is the EXO-46 / D-RMAP-1 membrane. ADMISSION B leaves one door open for it ("rewritten as a sequential, witnessed relationship projection it could come under B", `six-decisions.md:40-44`). The lab producer is a plain loop, not that witnessed projection. + +**Verdict.** +- C reuses existing algebra (Quack `Filter` + `lower` + mask-risc; no new executor). But C over the Via form inherits the admission problem. +- C′ is the only form whose query side matches the rulings as written. It moves the open question to the producer. +- C does not win on its own. **C′ = C with a co-addressed description** is the smallest lawful candidate. + +## 4. Falsifier (`tests/when.rs`, 16/16; `tests/p0.rs` from #1947 still 12/12) + +**Setup.** +- **Fixtures and gold:** #1947's. +- **Independent oracle:** a string-level evaluator over the token structs. It uses no ids and no programs. +- **Bindings:** `CandidateRecipient` (`MethodId 1`) and `CandidateExperiencer` (`MethodId 2`), registered in a real `BindStore`. + - Lab stand-in classids `0x7F21_0000` (Via) and `0x7F21_0001` (co-addressed); unminted. + - No effects. + - `Population::Distinct`, `Truth::TwoValued`. + +**Results.** +- Both forms equal the oracle and the gold: recipient = {105, 405}, experiencer = {302}. +- The recipient and experiencer witnesses are distinct in both forms. Stripped of the frame part, they coincide (the #1947 finding). +- **UNKNOWN stays UNKNOWN.** *helfen* gives no candidate, its `head_frame` is `FRAME_NONE` (no entry, not a negative role), and #1947's abstention rule still reports it. +- The Direction/Purpose ambiguity is kept. +- Candidates are read-only: `effects` is empty and `writes` is empty. A method with an effect is refused (`NotReadOnly`). + +**Negative controls.** Each prediction was written in the test's doc comment before it ran. + +| # | control | predicted = observed | +|---|---|---| +| 1 | head-frame condition removed | recipient = {105, 302, 405, 505}; against the bound guard: `DescriptionMismatch` | +| 2 | GIVE ↔ EXPERIENCE swapped in the lexicon | Via: `DescriptionMismatch` (digest moved). Co-addressed: `LexiconRevision{bound 1, population 2}`; recomposed honestly under rev 2, the answers swap | +| 3 | Dat → Acc | no candidate | +| 4 | dependency reversed | no candidate | +| 5 | referenced head removed | typed refusal `Map(Unmapped)` at production, never a FALSE role | +| 6 | foreign frame | `Stale` | +| 7 | foreign ClassId | `UnknownClass` from `admit` | +| 8 | deprel operand removed | `DescriptionMismatch`; under its own binding the instrument 408 becomes a recipient | +| 9 | Direction/Purpose | both kept (#1947 rule, same population) | +| 10 | one WHERE plane (tokens of A and C) shared by both methods | recipient {105}, experiencer {302}; equals unscoped ∩ W, in both forms | + +**Source disables.** Each anchor was asserted and read from the `test result` line; 9 guards, all red: + +| guard disabled | red | +|---|---| +| witness check | n01, n02, n08 | +| lexicon revision | n02 | +| co-addressed frame | 5 | +| Via frame | 5 | +| Sym digest | witnesses, n02 | +| producer reads head (not self) | 5 | +| read-only check | 1 | +| WHERE plane | n10 | +| frame check | n06 | + +## 5. EXO-140 classification proposal (NONBINDING) + +`Pred::EqU32Via` reads `foreign.lanes[key][fk[i]]` (`ir.rs:148-158`). Its properties: + +- It is an indexed per-row load at a position taken from a value. It is **not** a vertical lane read, and not a same-table attested seek. +- The mapping (`fk` = HEAD) is resident. In this probe it is versioned only through the population's frame check. +- It runs in the hot path, per row, every run. It is not bound once in preparation. +- It cannot cross a tile: `fk` indexes one foreign lane slice. + +**Proposed classification:** gather-class read (ADMISSION B "position derived from another relational column", option C), not admitted. **Smallest admissible scope for an operator to consider:** none for the query path. Instead, admit the *producer* of a co-addressed relation lane under B's "sequential, witnessed relationship projection". This is an operator decision. + +**What RelAlg lowers to.** RelAlg cannot lower to `EqU32Via`: it has no hop. Quack's `Filter::EqU32Via` lowers to exactly that primitive. The co-addressed description lowers to `Pred::EqU32` only. + +## 6. Frame lexicon: reuse candidates + +| existing | fits? | +|---|---| +| `lance-graph-contract/src/grammar/verb_lexicon.rs:47` `FAMILY_LEXICON` (lemma → `VerbFamily`, 12 families → TEKAMOLO `SlotPrior`) | no slot → role mapping; the file calls itself "starter knowledge" | +| `grammar/witness.rs:134-137` names `ArgumentStatus{CoreArgument, GovernedOblique, CircumstantialOblique, Unknown}` | named, not implemented | +| `revision.rs:104` `LanguageId(pub u16)` (in `InterpretiveHorizon`) | language scope exists, as an "opaque" id | +| deepnsm-v2 `haspelmath.rs` `FormAttestation` | form → function set, not lemma → frame | +| UD | HEAD/DEPREL/FEATS only; no frames | + +**Gap.** No contract holds `(language, lemma, slot, role, source revision)`. The lab `Lexicon{rev, language, entries}` is fixture data. + +**Requirements for an owner design.** +- A frame lexicon needs a revision that the produced lane carries. Control 2 shows why: a swapped lexicon is otherwise undetectable in the co-addressed form. +- Multiple frames per lemma need either a mask-test leaf in `SetExpr` or multiple candidate rows. `SetExpr::Res::U32` is eq/ne only; Quack already has `Cmp::MatchU32`. +- A missing entry = `FRAME_NONE` = abstain, never a negative role. + +## 7. Two role vocabularies + +| function | CE64 `Orientation` (`causal-edge/src/orientation.rs:17`, 3-bit code) | deepnsm-v2 `DativeFunction` (`haspelmath.rs:27`, bit in a `u8` set) | +|---|---|---| +| none / plain core argument | `Core` = 0 | — | +| Direction | 1 | 0 | +| Recipient | 2 | 1 | +| Experiencer | 3 | 2 | +| Purpose | 4 | 3 | +| Beneficiary | 5 | 4 | +| Predicative possessor | 6 | 5 | +| External possessor | 7 | 6 | +| Judicantis | — | 7 | + +- **Overlap.** The vocabularies share 7 functions, with ordinals offset by one. +- **Not subsets.** Neither is a subset of the other: CE64 has `Core`, deepnsm-v2 has Judicantis. +- **Not equivalent.** CE64 holds ONE code per edge. `DativeFunction` is a SET (`u8` bitmask). +- **Projection.** CE64 is a lossy projection for any ambiguous reading (Direction|Purpose) and has no Judicantis. +- **Recommendation for representation, not identity.** Keep candidate roles as separate masks/relations, one per function, as both probes do. Canonical identity is an owner decision. + +## 8. Candidate-to-fact boundary + +**Existing boundary.** +- Layer 0 GIVENS are "written only by hydration (pearl::hydrate), never overwritten" (`knowledge/epistemic-frontier-capstone.md:34`). Layers 1..63 are HYPOTHESES (`:38`). +- A write is "the Rubicon decision … landed into Lance only when it is satisfactory" (`plans/thought-git-basics-v1.md:45`), gated by `mul::GateDecision {Flow, Hold, Block}` (`:155`). +- D-STAUNEN-3: "candidate relations in THOUGHT, not WORLD … independent observation permits promotion" (`docs/research/learning/d-staunen-3-xlog-nsl-hydration.md:7`). + +A grammatical candidate is a layer ≥1 hypothesis. Minimum conditions before promotion: +1. The supporting observations are named: the token gids and the source annotation revision. +2. The frame lexicon revision is recorded with the candidate. The produced lane carries it (control 2). +3. An explicit selection policy decides ambiguous candidates. None exists; nothing is chosen today. +4. The write goes through hydration / the Rubicon gate, never through a method `Effect`. +5. UNKNOWN (no frame, no Case) stays UNKNOWN. + +**Out of scope.** No confidence score is invented here, and no causal certification. CG-3 SELECT/REMOVE is excluded. + +## 9. Measurements + +`cargo run --release --example when_cost`, Xeon @ 2.10 GHz, three runs: +- 40 tokens; 2 programs per form. +- One tile read per lane per run. + +**Cold (reported, not gates):** + +| phase | cost | +|---|---| +| vocab bind | 4.7–7.0 µs | +| DR map | 5.9–6.4 µs | +| producing `head_frame` (35 lookups) | 9.1–10.0 µs | +| registering 4 methods | 8.3–8.9 µs | +| compose ×2 (admit + witness check + lower), Via | 21.4–22.0 µs | +| compose ×2, co-addressed | 16.0–18.6 µs | + +- The lab producer uses a linear search per token. It is not a production algorithm. + +**Hot (both methods, including the frame and lexicon-revision checks):** + +| form | mask ops | cost | +|---|---|---| +| Via | 12 | 557–574 ns/run | +| Co-addressed | 10 | 413–465 ns/run | + +**Other properties.** +- **Allocation:** 0 B per hot run. +- **Working set:** 5 `u32` lanes × 40 = 800 B, plus scratch. +- **Not measured:** binding enumeration (masks only). #1947's 1.2–1.3 µs covers 5 rules and is not comparable one-to-one. +- **Scale:** no corpus-scale claim. + +## 10. Owner decisions (with evidence) + +1. **EXO-140.** Classify `Pred::EqU32Via` at the grammar call site. Proposed: gather-class, not admitted on the query path (§5). +2. **EXO-46 / D-RMAP-1.** Admit, or refuse, a producer that writes a co-addressed relation lane (`head_frame[i]`) as a "sequential, witnessed relationship projection" under ADMISSION B. +3. **D-DT64-6.** + - Should WHEN carry a description identity the store verifies, rather than an opaque `Sym`? + - Should `validate` check guard lanes against the basis? + - Should a read-only "returns" DO exist? +4. **Frame lexicon owner** (OGAR codebook, DT64 class data or neither), with revision and language scope (`LanguageId` exists). +5. **Role vocabulary identity:** CE64 `Orientation` vs `DativeFunction`. Representation stays per-function masks. +6. **Promotion policy** for candidates (selection policy; hydration / Rubicon gate). + +## Final verdict + +- **WIRE NOW:** none in production. In the lab, `compose` connects existing parts only (`admit`, `Guard::witness`, Quack `Filter` + `lower`, mask-risc `execute_into`, dt64 `MapTable` frames). +- **PROBE:** + - a witnessed sequential producer for `head_frame` at GSD scale; + - the multi-frame lexicon (a mask-test leaf); + - the R2IL path with WHEN once D-DT64-6 rules. +- **OWNER DECISION:** items 1–6 above. +- **PARK:** + - cross-language runtime; + - full CG-3 ordered SELECT/REMOVE; + - grammar learning; + - recursion (EXO-73). +- **SKIP:** + - a new grammar executor; + - a grammar AST; + - a second relation store; + - copied presence planes; + - scratch-mask handoff between programs; + - a new `F###` family. The F000 polyfill words `IntEqual` / `IntAnd` / `IntOr` already name every op the co-addressed WHEN needs. diff --git a/crates/grammar-constraints-probe/examples/when_cost.rs b/crates/grammar-constraints-probe/examples/when_cost.rs new file mode 100644 index 000000000..b9ca9973b --- /dev/null +++ b/crates/grammar-constraints-probe/examples/when_cost.rs @@ -0,0 +1,72 @@ +//! D-GRAMMAR-WHEN-1 costs, cold and hot kept apart, for both physical forms. +//! cargo run --release --manifest-path crates/grammar-constraints-probe/Cargo.toml --example when_cost +//! Cold phases are one-off (reported, not gates). + +use std::hint::black_box; +use std::time::Instant; + +use grammar_constraints_probe::fixtures; +use grammar_constraints_probe::when::*; +use grammar_constraints_probe::{tile, Ids, Vocab}; +use lance_graph_dt64::{BindStore, MethodRef}; + +fn ns(f: impl FnOnce() -> T) -> (T, u128) { + let t = Instant::now(); + let r = f(); + (r, t.elapsed().as_nanos()) +} + +fn main() { + let corpus = fixtures::corpus(); + let lex = Lexicon::v0(); + let mut v = Vocab::new(); + let (_, t_vocab) = ns(|| Ids::bind(&mut v)); + let ((table, frame), t_dr) = ns(|| tile(9, &fixtures::gids(&corpus))); + let (pop, t_prod) = + ns(|| FramedPopulation::produce(&corpus, &mut v, &table, &frame, &lex).unwrap()); + let rules = [RuleDesc::recipient(), RuleDesc::experiencer()]; + let mut store = BindStore::new(); + let (_, t_reg) = ns(|| { + register(&mut store, CLASS_VIA, Physical::Via, &rules, &v, &lex).unwrap(); + register(&mut store, CLASS_COADDR, Physical::CoAddressed, &rules, &v, &lex).unwrap(); + }); + let n = pop.base.n; + let mut all = vec![0u64; n.div_ceil(64)]; + for i in 0..n { + all[i / 64] |= 1 << (i % 64); + } + println!("tokens={n} producer_lookups={}", pop.producer_lookups); + println!( + "cold (reported, not gates): vocab_bind={t_vocab} ns dr_map={t_dr} ns produce_head_frame={t_prod} ns register_4_methods={t_reg} ns" + ); + for (phys, class) in [(Physical::Via, CLASS_VIA), (Physical::CoAddressed, CLASS_COADDR)] { + let mut composed = Vec::new(); + let mut t_comp = 0; + for d in &rules { + let r = MethodRef::of(class, &d.binding(phys, &v, &lex)); + let (c, t) = ns(|| compose(&store, &r, d, phys, &v, &lex).unwrap()); + t_comp += t; + composed.push(c); + } + let ops: usize = composed.iter().map(|c| c.ops()).sum(); + for c in composed.iter_mut() { + for _ in 0..10_000 { + black_box(c.run(&pop, &table, &frame, &all).unwrap()); + } + } + let reps = 100_000u32; + let mut best = u128::MAX; + for _ in 0..5 { + let t = Instant::now(); + for _ in 0..reps { + for c in composed.iter_mut() { + black_box(c.run(black_box(&pop), &table, &frame, &all).unwrap()); + } + } + best = best.min(t.elapsed().as_nanos() / u128::from(reps)); + } + println!( + "{phys:?}: compose(admit+witness+lower) x2 = {t_comp} ns cold; programs=2 mask_ops={ops}; hot both methods incl. frame + lexicon-rev check = {best} ns/run (best of 5 x {reps})" + ); + } +} diff --git a/crates/grammar-constraints-probe/src/when.rs b/crates/grammar-constraints-probe/src/when.rs index 53c421bc6..95817f85f 100644 --- a/crates/grammar-constraints-probe/src/when.rs +++ b/crates/grammar-constraints-probe/src/when.rs @@ -43,7 +43,9 @@ use lance_graph_mask_risc::{ }; use lance_graph_quack::{lower, Agg, Cmp, Col, Filter, ForeignLane, LowerError, Mask, Query}; -use crate::{Population, Refusal as PopRefusal, Tok, Vocab, CASE, DEPREL, HEAD, LEMMA, TILE, WIDTH}; +use crate::{ + Population, Refusal as PopRefusal, Tok, Vocab, CASE, DEPREL, HEAD, LEMMA, TILE, WIDTH, +}; /// Field position (and lane) of the head's frame code, co-addressed. pub const HEAD_FRAME: u16 = 4; @@ -338,7 +340,10 @@ pub enum ComposeRefusal { pub enum RunRefusal { Frame(PopRefusal), /// The population was produced under another lexicon revision. - LexiconRevision { bound: u64, population: u64 }, + LexiconRevision { + bound: u64, + population: u64, + }, /// The WHERE plane is not over this population. WhereShape, } diff --git a/crates/grammar-constraints-probe/tests/when.rs b/crates/grammar-constraints-probe/tests/when.rs index 1289acb24..04a58b472 100644 --- a/crates/grammar-constraints-probe/tests/when.rs +++ b/crates/grammar-constraints-probe/tests/when.rs @@ -6,7 +6,9 @@ use std::cell::Cell; use grammar_constraints_probe::fixtures::{self, Gold, A, B, C, GOLD}; use grammar_constraints_probe::when::*; -use grammar_constraints_probe::{has, tile, Ids, Operands, Refusal as PopRefusal, Rules, Tok, Vocab, TILE}; +use grammar_constraints_probe::{ + has, tile, Ids, Operands, Refusal as PopRefusal, Rules, Tok, Vocab, TILE, +}; use lance_graph_contract::set_algebra::{Logic, SetExpr}; use lance_graph_dt64::dr::{Frame, MapRead, MapRefusal, MapTable}; use lance_graph_dt64::{ @@ -46,7 +48,15 @@ fn world_with(toks: &[Tok], lex: Lexicon) -> W { let mut store = BindStore::new(); let rules = [RuleDesc::recipient(), RuleDesc::experiencer()]; register(&mut store, CLASS_VIA, Physical::Via, &rules, &v, &lex).unwrap(); - register(&mut store, CLASS_COADDR, Physical::CoAddressed, &rules, &v, &lex).unwrap(); + register( + &mut store, + CLASS_COADDR, + Physical::CoAddressed, + &rules, + &v, + &lex, + ) + .unwrap(); W { v, table, @@ -183,7 +193,8 @@ fn unknown_stays_unknown_and_ambiguity_is_kept() { assert_eq!(w.pop.head_frame[usize::from(local(&w, 505))], FRAME_NONE); let mut v = Vocab::new(); let ids = Ids::bind(&mut v); - let pop = grammar_constraints_probe::Population::bind(&corpus, &mut v, &w.table, &w.frame).unwrap(); + let pop = + grammar_constraints_probe::Population::bind(&corpus, &mut v, &w.table, &w.frame).unwrap(); let mut rules = Rules::prepare(&ids, Operands::ALL); let r = rules.run(&pop, &w.table, &w.frame).unwrap(); assert!(has(&r.abstain_frame, local(&w, 505))); @@ -201,7 +212,10 @@ fn candidates_are_read_only() { for p in BOTH { for d in [RuleDesc::recipient(), RuleDesc::experiencer()] { let b = w.store.admit(&mref(&w, class_of(p), &d, p)).unwrap(); - assert!(b.effects.is_empty() && b.writes() == lance_graph_contract::class_view::WideFieldMask::EMPTY); + assert!( + b.effects.is_empty() + && b.writes() == lance_graph_contract::class_view::WideFieldMask::EMPTY + ); } } // A method with an effect is refused by the composer. @@ -212,13 +226,26 @@ fn candidates_are_read_only() { let mut b = RuleDesc::recipient().binding(Physical::CoAddressed, &w.v, &w.lex); b.effects = vec![Effect { target: 4, - algebra: AlgebraRef { lens: 0x7F30_0000, word: 0 }, + algebra: AlgebraRef { + lens: 0x7F30_0000, + word: 0, + }, args: vec![Arg::Field(1)], }]; - store.register(CLASS_COADDR, schema(), vec![b.clone()]).unwrap(); + store + .register(CLASS_COADDR, schema(), vec![b.clone()]) + .unwrap(); let r = MethodRef::of(CLASS_COADDR, &b); assert_eq!( - compose(&store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).err(), + compose( + &store, + &r, + &RuleDesc::recipient(), + Physical::CoAddressed, + &w.v, + &w.lex + ) + .err(), Some(ComposeRefusal::NotReadOnly) ); } @@ -246,13 +273,29 @@ fn n01_remove_head_frame() { let mut d = RuleDesc::recipient(); d.frame = None; let mut store = BindStore::new(); - register(&mut store, CLASS_COADDR, Physical::CoAddressed, std::slice::from_ref(&d), &w.v, &w.lex).unwrap(); - let r = MethodRef::of(CLASS_COADDR, &d.binding(Physical::CoAddressed, &w.v, &w.lex)); + register( + &mut store, + CLASS_COADDR, + Physical::CoAddressed, + std::slice::from_ref(&d), + &w.v, + &w.lex, + ) + .unwrap(); + let r = MethodRef::of( + CLASS_COADDR, + &d.binding(Physical::CoAddressed, &w.v, &w.lex), + ); let mut c = compose(&store, &r, &d, Physical::CoAddressed, &w.v, &w.lex).unwrap(); let m = c.run(&w.pop, &w.table, &w.frame, &all_plane(&w)).unwrap(); assert_eq!(gids_of(&w, &m), vec![105, 302, 405, 505]); // and the stripped description no longer matches the bound guard - let bound = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + let bound = mref( + &w, + CLASS_COADDR, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); assert_eq!( compose(&w.store, &bound, &d, Physical::CoAddressed, &w.v, &w.lex).err(), Some(ComposeRefusal::DescriptionMismatch) @@ -271,18 +314,58 @@ fn n02_swap_frames() { let swapped = Lexicon::swapped(); let bound = mref(&w, CLASS_VIA, &RuleDesc::recipient(), Physical::Via); assert_eq!( - compose(&w.store, &bound, &RuleDesc::recipient(), Physical::Via, &w.v, &swapped).err(), + compose( + &w.store, + &bound, + &RuleDesc::recipient(), + Physical::Via, + &w.v, + &swapped + ) + .err(), Some(ComposeRefusal::DescriptionMismatch) ); let ws = world_with(&corpus, swapped); - let r = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); - let mut c = compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).unwrap(); + let r = mref( + &w, + CLASS_COADDR, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); + let mut c = compose( + &w.store, + &r, + &RuleDesc::recipient(), + Physical::CoAddressed, + &w.v, + &w.lex, + ) + .unwrap(); assert_eq!( c.run(&ws.pop, &ws.table, &ws.frame, &all_plane(&ws)).err(), - Some(RunRefusal::LexiconRevision { bound: 1, population: 2 }) + Some(RunRefusal::LexiconRevision { + bound: 1, + population: 2 + }) + ); + assert_eq!( + answer( + &ws, + &RuleDesc::experiencer(), + Physical::CoAddressed, + &all_plane(&ws) + ), + vec![105, 405] + ); + assert_eq!( + answer( + &ws, + &RuleDesc::recipient(), + Physical::CoAddressed, + &all_plane(&ws) + ), + vec![302] ); - assert_eq!(answer(&ws, &RuleDesc::experiencer(), Physical::CoAddressed, &all_plane(&ws)), vec![105, 405]); - assert_eq!(answer(&ws, &RuleDesc::recipient(), Physical::CoAddressed, &all_plane(&ws)), vec![302]); } /// 3. Dative → accusative on Kind (A). PREDICTED: no candidate for 105. @@ -307,7 +390,10 @@ fn n04_reversed_dependency() { a[4].deprel = "root"; let w = world(&a); for p in BOTH { - assert!(answer(&w, &RuleDesc::recipient(), p, &all_plane(&w)).is_empty(), "{p:?}"); + assert!( + answer(&w, &RuleDesc::recipient(), p, &all_plane(&w)).is_empty(), + "{p:?}" + ); } } @@ -327,8 +413,21 @@ fn n05_missing_head() { fn n06_foreign_frame() { let w = world(&A); let (_t, foreign) = tile(9, &fixtures::gids(&A)); - let r = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); - let mut c = compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).unwrap(); + let r = mref( + &w, + CLASS_COADDR, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); + let mut c = compose( + &w.store, + &r, + &RuleDesc::recipient(), + Physical::CoAddressed, + &w.v, + &w.lex, + ) + .unwrap(); assert!(matches!( c.run(&w.pop, &w.table, &foreign, &all_plane(&w)), Err(RunRefusal::Frame(PopRefusal::Read(MapRead::Stale(_)))) @@ -339,10 +438,25 @@ fn n06_foreign_frame() { #[test] fn n07_foreign_class() { let w = world(&A); - let r = mref(&w, CLASS_FOREIGN, &RuleDesc::recipient(), Physical::CoAddressed); + let r = mref( + &w, + CLASS_FOREIGN, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); assert_eq!( - compose(&w.store, &r, &RuleDesc::recipient(), Physical::CoAddressed, &w.v, &w.lex).err(), - Some(ComposeRefusal::Binding(Refusal::UnknownClass(CLASS_FOREIGN))) + compose( + &w.store, + &r, + &RuleDesc::recipient(), + Physical::CoAddressed, + &w.v, + &w.lex + ) + .err(), + Some(ComposeRefusal::Binding(Refusal::UnknownClass( + CLASS_FOREIGN + ))) ); } @@ -355,16 +469,35 @@ fn n08_remove_operand() { let w = world(&corpus); let mut d = RuleDesc::recipient(); d.deprel = None; - let bound = mref(&w, CLASS_COADDR, &RuleDesc::recipient(), Physical::CoAddressed); + let bound = mref( + &w, + CLASS_COADDR, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); assert_eq!( compose(&w.store, &bound, &d, Physical::CoAddressed, &w.v, &w.lex).err(), Some(ComposeRefusal::DescriptionMismatch) ); let mut store = BindStore::new(); - register(&mut store, CLASS_COADDR, Physical::CoAddressed, std::slice::from_ref(&d), &w.v, &w.lex).unwrap(); - let r = MethodRef::of(CLASS_COADDR, &d.binding(Physical::CoAddressed, &w.v, &w.lex)); + register( + &mut store, + CLASS_COADDR, + Physical::CoAddressed, + std::slice::from_ref(&d), + &w.v, + &w.lex, + ) + .unwrap(); + let r = MethodRef::of( + CLASS_COADDR, + &d.binding(Physical::CoAddressed, &w.v, &w.lex), + ); let mut c = compose(&store, &r, &d, Physical::CoAddressed, &w.v, &w.lex).unwrap(); - let got = gids_of(&w, &c.run(&w.pop, &w.table, &w.frame, &all_plane(&w)).unwrap()); + let got = gids_of( + &w, + &c.run(&w.pop, &w.table, &w.frame, &all_plane(&w)).unwrap(), + ); assert!(got.contains(&408), "{got:?}"); } From 7f63815ca448d141a882d44299246751ca2f57a0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 21:39:40 +0000 Subject: [PATCH 3/4] D-GRAMMAR-WHEN-1: rustfmt the cost example Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMLBmi7EtDd15CGwGb8 --- .../examples/when_cost.rs | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/crates/grammar-constraints-probe/examples/when_cost.rs b/crates/grammar-constraints-probe/examples/when_cost.rs index b9ca9973b..f06b3c687 100644 --- a/crates/grammar-constraints-probe/examples/when_cost.rs +++ b/crates/grammar-constraints-probe/examples/when_cost.rs @@ -28,7 +28,15 @@ fn main() { let mut store = BindStore::new(); let (_, t_reg) = ns(|| { register(&mut store, CLASS_VIA, Physical::Via, &rules, &v, &lex).unwrap(); - register(&mut store, CLASS_COADDR, Physical::CoAddressed, &rules, &v, &lex).unwrap(); + register( + &mut store, + CLASS_COADDR, + Physical::CoAddressed, + &rules, + &v, + &lex, + ) + .unwrap(); }); let n = pop.base.n; let mut all = vec![0u64; n.div_ceil(64)]; @@ -39,7 +47,10 @@ fn main() { println!( "cold (reported, not gates): vocab_bind={t_vocab} ns dr_map={t_dr} ns produce_head_frame={t_prod} ns register_4_methods={t_reg} ns" ); - for (phys, class) in [(Physical::Via, CLASS_VIA), (Physical::CoAddressed, CLASS_COADDR)] { + for (phys, class) in [ + (Physical::Via, CLASS_VIA), + (Physical::CoAddressed, CLASS_COADDR), + ] { let mut composed = Vec::new(); let mut t_comp = 0; for d in &rules { From bf94df1d53452bd81de4fe8fd70f83f0342ce6ed Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 22:22:23 +0000 Subject: [PATCH 4/4] D-GRAMMAR-WHEN-1: bind each population to the frame it was produced under Codex review on #1948: run() checked only that the frame belongs to the table and that the row count matches, so a table re-sealed under a permuted layout of the same size was answered with bits naming other gids. The population now keeps its binding frame and both Rules::run and Composed::run refuse any other (Refusal::PopulationFrame, checked with Frame::same_issue after the map read). Falsifiers c7b (p0) and n06b (when) were written first and failed before the fix; both pass after. p0 13/13, when 17/17. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMLBmi7EtDd15CGwGb8 --- .../entries/2026-11-03-d-grammar-when-1.md | 2 +- .../2026-11-03-d-grammar-when-1/REPORT.md | 3 +- crates/grammar-constraints-probe/src/lib.rs | 9 +++++ crates/grammar-constraints-probe/src/when.rs | 3 ++ crates/grammar-constraints-probe/tests/p0.rs | 17 +++++++++ .../grammar-constraints-probe/tests/when.rs | 37 +++++++++++++++++++ 6 files changed, 69 insertions(+), 2 deletions(-) diff --git a/.claude/board/entries/2026-11-03-d-grammar-when-1.md b/.claude/board/entries/2026-11-03-d-grammar-when-1.md index 5503a0a37..f5904d247 100644 --- a/.claude/board/entries/2026-11-03-d-grammar-when-1.md +++ b/.claude/board/entries/2026-11-03-d-grammar-when-1.md @@ -21,7 +21,7 @@ - The cross-row read moves into the producer, which does it once and counted (35 lookups). - **Lab composer (approach C): admit → check description vs witness → lower description ∧ shared WHERE into ONE program.** - Both forms match an independent oracle and the gold. - - 10 negative controls behave as predicted; 9 source disables go red. + - 11 negative controls behave as predicted (incl. a re-sealed same-size layout, from Codex review); 9 source disables go red. ## Open (owner) diff --git a/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md b/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md index 90c7659f2..0d9bfd780 100644 --- a/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md +++ b/.claude/probes/2026-11-03-d-grammar-when-1/REPORT.md @@ -86,7 +86,7 @@ The first typed refusal on each path: - C′ is the only form whose query side matches the rulings as written. It moves the open question to the producer. - C does not win on its own. **C′ = C with a co-addressed description** is the smallest lawful candidate. -## 4. Falsifier (`tests/when.rs`, 16/16; `tests/p0.rs` from #1947 still 12/12) +## 4. Falsifier (`tests/when.rs`, 17/17; `tests/p0.rs` 13/13 incl. #1947's 12) **Setup.** - **Fixtures and gold:** #1947's. @@ -113,6 +113,7 @@ The first typed refusal on each path: | 4 | dependency reversed | no candidate | | 5 | referenced head removed | typed refusal `Map(Unmapped)` at production, never a FALSE role | | 6 | foreign frame | `Stale` | +| 6b | same table re-sealed under a permuted same-size layout (Codex review on #1948) | `PopulationFrame`; the population now keeps the frame it was bound under and both run paths check `Frame::same_issue`. Before the fix this was answered, with bits naming other gids | | 7 | foreign ClassId | `UnknownClass` from `admit` | | 8 | deprel operand removed | `DescriptionMismatch`; under its own binding the instrument 408 becomes a recipient | | 9 | Direction/Purpose | both kept (#1947 rule, same population) | diff --git a/crates/grammar-constraints-probe/src/lib.rs b/crates/grammar-constraints-probe/src/lib.rs index e7d10c203..5669eb66e 100644 --- a/crates/grammar-constraints-probe/src/lib.rs +++ b/crates/grammar-constraints-probe/src/lib.rs @@ -133,12 +133,17 @@ pub struct Population { deprel: Vec, case: Vec, head: Vec, + /// The frame the lanes were bound under; every run must present it. + frame: Frame, } #[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum Refusal { Map(MapRefusal), Read(MapRead), + /// The frame is not the one the population was bound under (the table + /// may have advanced to another layout of the same size). + PopulationFrame, } impl Population { @@ -158,6 +163,7 @@ impl Population { deprel: vec![0; n], case: vec![0; n], head: vec![ROOT; n], + frame: frame.clone(), }; for t in toks { let l = usize::from(map.local(t.gid).map_err(Refusal::Map)?); @@ -539,6 +545,9 @@ impl Rules { if map.len() != pop.n { return Err(Refusal::Map(MapRefusal::OutOfTile)); } + if !frame.same_issue(&pop.frame) { + return Err(Refusal::PopulationFrame); + } let lanes = pop.lanes(); let flanes = pop.foreign_lanes(); let planes = Planes { diff --git a/crates/grammar-constraints-probe/src/when.rs b/crates/grammar-constraints-probe/src/when.rs index 95817f85f..0f38b3ff6 100644 --- a/crates/grammar-constraints-probe/src/when.rs +++ b/crates/grammar-constraints-probe/src/when.rs @@ -415,6 +415,9 @@ impl Composed { lance_graph_dt64::dr::MapRefusal::OutOfTile, ))); } + if !frame.same_issue(&pop.base.frame) { + return Err(RunRefusal::Frame(PopRefusal::PopulationFrame)); + } if pop.lexicon_rev != self.lexicon_rev { return Err(RunRefusal::LexiconRevision { bound: self.lexicon_rev, diff --git a/crates/grammar-constraints-probe/tests/p0.rs b/crates/grammar-constraints-probe/tests/p0.rs index 7ebc5ad67..25ec654cc 100644 --- a/crates/grammar-constraints-probe/tests/p0.rs +++ b/crates/grammar-constraints-probe/tests/p0.rs @@ -273,6 +273,23 @@ fn c7_foreign_frame_refuses() { )); } +/// Control 7b: same table, re-sealed under a permuted same-size layout +/// (Codex #1948): refused, not answered. +#[test] +fn c7b_resealed_same_size_layout_refuses() { + let mut w = world(&A); + let mut gids = fixtures::gids(&A); + gids.reverse(); + let map = lance_graph_dt64::dr::LocalMap::prepare(WIDTH, &gids).unwrap(); + w.table.advance(7, 0, vec![(TILE, Some(map))]); + let resealed = w.table.seal(); + assert!(matches!( + w.rules.run(&w.pop, &w.table, &resealed), + Err(Refusal::PopulationFrame) + )); + assert!(w.rules.run(&w.pop, &w.table, &w.frame).is_ok()); +} + /// Control 8: one required relational operand disabled: deprel. The dative /// instrument `mit dem Löffel` (obl, Dat, under geben) becomes a recipient. #[test] diff --git a/crates/grammar-constraints-probe/tests/when.rs b/crates/grammar-constraints-probe/tests/when.rs index 04a58b472..e32aa0101 100644 --- a/crates/grammar-constraints-probe/tests/when.rs +++ b/crates/grammar-constraints-probe/tests/when.rs @@ -434,6 +434,43 @@ fn n06_foreign_frame() { )); } +/// 6b. Same table, re-sealed under a permuted layout of the same size +/// (Codex #1948). PREDICTED: refused as `PopulationFrame`, never answered +/// with bits that name other gids. +#[test] +fn n06b_resealed_same_size_layout() { + let mut w = world(&A); + let mut gids = fixtures::gids(&A); + gids.reverse(); + let map = + lance_graph_dt64::dr::LocalMap::prepare(grammar_constraints_probe::WIDTH, &gids).unwrap(); + w.table.advance(9, 0, vec![(TILE, Some(map))]); + let resealed = w.table.seal(); + assert_eq!(w.table.map(&resealed, TILE).unwrap().len(), w.pop.base.n); + let r = mref( + &w, + CLASS_COADDR, + &RuleDesc::recipient(), + Physical::CoAddressed, + ); + let mut c = compose( + &w.store, + &r, + &RuleDesc::recipient(), + Physical::CoAddressed, + &w.v, + &w.lex, + ) + .unwrap(); + let plane = all_plane(&w); + assert_eq!( + c.run(&w.pop, &w.table, &resealed, &plane).err(), + Some(RunRefusal::Frame(PopRefusal::PopulationFrame)) + ); + // control: the producing frame still runs + assert!(c.run(&w.pop, &w.table, &w.frame, &plane).is_ok()); +} + /// 7. Foreign classid. PREDICTED: UnknownClass from admit. #[test] fn n07_foreign_class() {