diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index e17a7ed00..63b29e25c 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -4,7 +4,8 @@ | D-id | Deliverable | Status | Gate | |---|---|---|---| -| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 11 Clingo goldens exact; holdings lens with Set/Bag projection; 6 disable runs | In PR | lab only | +| D-MIST-NATIVE-0 | Kripke `holds` + rule/origin lineage as a least fixpoint over `relcomp::compose`; 11 Clingo goldens exact; holdings lens with Set/Bag projection; 6 disable runs | Shipped (#1873) | lab only | +| D-MIST-NATIVE-1a | HHTL16 Register128 rows replace the name interner: world/proposition/rule nodes as 512-byte rows (16 Morton8x8 columns, identity + up to 15 addresses), classid per population on `RegisterLanes`, accessibility derived from world rows, every compose through `bind_dr64` + `relcomp::Chain`; no String in solved state (compile-time guard); 18 tests + 2 compile_fail doctests; 7 disable runs | In PR | lab only | | D-MIST-NATIVE-1 | `lance-graph-mistaber`: onnx-shaped ALIAS/INLINE/REFUSE facade (plan §3) | Queued | production home for `compose` (plan Q1) | | D-MIST-NATIVE-2 | lineage origins into `SupportLedger` (`EvidenceSourceId`, `TextAttested`) | Queued | after D-MIST-NATIVE-1 | | D-MIST-NATIVE-3 | axes past 64 (worlds, propositions, rules) | Queued | refused today | diff --git a/.claude/board/entries/2026-10-30-d-mist-native-1a-hhtl16-rows.md b/.claude/board/entries/2026-10-30-d-mist-native-1a-hhtl16-rows.md new file mode 100644 index 000000000..4754b9465 --- /dev/null +++ b/.claude/board/entries/2026-10-30-d-mist-native-1a-hhtl16-rows.md @@ -0,0 +1,12 @@ +# 2026-10-30 — D-MIST-NATIVE-1a: HHTL16 Register128 rows replace the name interner + +**Status:** LAB, measured by tests. Plan: `.claude/plans/d-mistaber-native-v1.md` §9. + +- The Kripke probe holds no String in its solved state. World, proposition and rule nodes are 512-byte rows in the HHTL16 format: Register0/Register1, 16 Morton8x8 columns, column 0 the identity, columns 1..=15 addresses. +- The classid is per population, on `RegisterLanes`; the row bytes carry none. +- Accessibility is derived from world rows, and a 16th parent is refused. +- `holds ∘ children` goes through `bind_dr64` and `relcomp::Chain`. +- 11 goldens exact; 18 tests and 2 `compile_fail` doctests; 7 disable runs red. +- Known limit: the binding is a typing guard, so swapping `Chain` for raw `compose` turns nothing red. Only the mistyped-signature disable (D4) shows the path is live. + +STATUS: measured | OUTCOME: Mistaber nodes as HHTL16 rows, no Strings, typed DR64 binding | OPEN: whether the row key also carries the address; real concept ids from the OGAR codebook. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 755adcead..9528d2c31 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -512 entries, 2026-08-06 .. 2026-10-30. +513 entries, 2026-08-06 .. 2026-10-30. | date | entry id | finding | file | |---|---|---|---| @@ -33,6 +33,7 @@ exactly one of them, never both. | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) | | 2026-10-30 | `D-TRACT-SHAPE-1` | | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) | | 2026-10-30 | `D-TRACT-HARVEST-0` | | [2026-10-30-d-tract-harvest-0-native-algebra-bridge.md](2026-10-30-d-tract-harvest-0-native-algebra-bridge.md) | +| 2026-10-30 | `D-MIST-NATIVE-1a` | | [2026-10-30-d-mist-native-1a-hhtl16-rows.md](2026-10-30-d-mist-native-1a-hhtl16-rows.md) | | 2026-10-30 | `D-MIST-NATIVE-0` | | [2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md](2026-10-30-d-mist-native-0-kripke-fixpoint-over-dr64.md) | | 2026-10-30 | `D-LITHO` | | [2026-10-30-d-litho-photolithography-contract.md](2026-10-30-d-litho-photolithography-contract.md) | | 2026-10-30 | `D-LITHO-1` | | [2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md](2026-10-30-d-litho-1-xlog-register-steps-and-bag-fixture.md) | diff --git a/.claude/plans/d-mistaber-native-v1.md b/.claude/plans/d-mistaber-native-v1.md index 18671adde..62f62eb92 100644 --- a/.claude/plans/d-mistaber-native-v1.md +++ b/.claude/plans/d-mistaber-native-v1.md @@ -74,7 +74,7 @@ A lens row is one (mode, source rule), or one (mode) with empty rule fields when ## 5. Evidence (D-MIST-NATIVE-0) -`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 12 tests. +`cargo test --release --manifest-path crates/mistaber-kripke-probe/Cargo.toml`: 18 tests + 2 doctests (since §9). Goldens: F1-modes, F1-reversed, F2-cycle, F5-gates, F6-undeclared-child, C-mammal-C2/C4/C6/C6i, E-xlog-plain/override. All are exact, compared as sorted lists, so a duplicate atom would also fail. @@ -129,3 +129,40 @@ Contracting V or O over the third axis (OR over `z`) gives the `holds` register So "the third axis is a relation ordinal" covers L and not V or O. Closing NFR-OP-2 stays the DR owner's decision. **Size.** Dense, each cube is 32 KiB of bits, 96 KiB for the three. The probe stores only O and L, and only as many slices as there are worlds and rules. V is never stored, because every V slice is one `compose` row read. Nothing here allocates a cube. + +## 9. D-MIST-NATIVE-1a: HHTL16 rows replace the name interner (2026-10-30) + +**Status:** LAB, in PR. The probe holds no names in its solved state. Names live only in `src/membrane.rs`, which parses the goldens and renders atoms. + +- **Rows** (`src/rows.rs`). World, proposition and rule nodes are 512-byte `NodeRow`s in the HHTL16 opt-in format. `Register0` holds the x bytes and `Register1` the y bytes. Column k is `Morton8x8::from_xy(R0[k], R1[k])`. Column 0 is the node's identity; columns 1..=15 are addresses, which for a world are its parents. Address = first-appearance ordinal + 1, so no two collide and none is unbound. +- **Classid per population.** Each population is bound once: `Activation` → `resolve_for_context(concept, Register128 slab)` → `bind_register128(Two)`. The concept lives on `RegisterLanes::concept()`. The key, edges and value bytes carry no classid. Concepts are lab stand-ins `0x7F11..13`; none is minted. +- **Accessibility is derived** from world rows (`Kb::derive_children`, its only writer). A 16th parent is refused with `TooManyParents { parents }`. Global address → local 0..64 goes through `hhtl16::LocalMap`, which refuses a 65th node, a duplicate or an unmapped address. +- **Binding.** The accessibility register and the three input registers are bound through `bind_dr64`. Every `holds ∘ children` step runs through `relcomp::Chain::new(..).eval(..)`. The fixpoint and lineage algebra are unchanged. +- **No-String guard.** A doc-hidden `AddressOnly` trait plus an exhaustive destructure of `Kb`, `Holdings`, `Mode` and `Population`. A String field fails to compile, and two `compile_fail` doctests show the bound can fire. + +**Tests:** 18 tests and 2 doctests. All 11 goldens stay exact. New tests cover: + +- rows round-tripping through `get`/`set`; +- a two-parent world deriving the old accessibility; +- the 16th parent being refused; +- the classid being on the lanes and not in the rows; +- `LocalMap` refusals. + +**Disable runs** (committed first, each then broken, red, restored): + +| # | breakage | red | +|---|---|---| +| D1 | read only parent column 1 | goldens, diamond Set/Bag, two-parent derivation, contraction, classid test | +| D2 | truncate parents instead of refusing | `a_16th_parent_is_refused` (`left: None`) | +| D3 | classid minted into the key | `the_classid_lives_on_the_lanes_not_in_the_rows` | +| D4 | accessibility signature typed Property × Identity | 12 tests (the `Chain` typing refuses `holds ∘ children`) | +| D5 | address without `+1` | round-trip, goldens and 7 others | +| D6 | accessibility orientation reversed | goldens, orientation, contraction and 5 others | +| D7 | a `NameTable` field on `Kb` | compile errors E0063 and E0027 (exhaustive destructure) | + +Known limit: replacing `hop` with raw `compose` turns nothing red. The binding is a typing guard, not semantics, and D4 is the only proof that the path is live. + +**Open (operator):** + +- the row key is all zero, so identity exists only in column 0. Should the key also carry the address? +- a real binding takes concept ids from the OGAR codebook through hotplug. diff --git a/crates/mistaber-kripke-probe/src/lib.rs b/crates/mistaber-kripke-probe/src/lib.rs index c0cf365b6..4cb44f5bc 100644 --- a/crates/mistaber-kripke-probe/src/lib.rs +++ b/crates/mistaber-kripke-probe/src/lib.rs @@ -1,9 +1,15 @@ -//! D-MIST-NATIVE-0: Mistaber's Kripke holding rules as a least fixpoint over -//! the existing DR64 Boolean relation register. +//! D-MIST-NATIVE-0/1a: Mistaber's Kripke holding rules as a least fixpoint +//! over the existing DR64 Boolean relation register, on HHTL16 node rows. //! //! Plan: `.claude/plans/d-mistaber-native-v1.md`. Reference answers: Clingo //! golden files exported by `AdaWorldAPI/mistaber-rs` (`goldens/SOURCE`). //! +//! # Identity +//! +//! A node is an address, never a name. Each population (world, proposition, +//! rule) is a set of [`rows::NodeRow`](lance_graph_contract::canonical_node::NodeRow)s +//! in the HHTL16 format of [`rows`]; names live only in [`membrane`]. +//! //! # The fixpoint //! //! Upstream `kripke_rules.lp` makes `holds` recursive through @@ -17,8 +23,8 @@ //! ``` //! //! with `H` a proposition × world relation and `children` the world × world -//! relation `parent → child`. Each step is one -//! [`compose`](dr_math_binding_probe::relcomp::compose) plus an AND-NOT: no new +//! relation `parent → child`, derived from the parent addresses in the world +//! rows. Each step is one DR64-bound composition plus an AND-NOT: no new //! algebra. The two lineages (`holds_via_rule`'s source rule and //! `inheritance_source`'s origin) are the same fixpoint gated by the final //! `H`, one per rule or origin. @@ -26,7 +32,7 @@ //! # The holdings lens //! //! Holdings are read through one lens whose fields are [`HOLDINGS_FIELDS`]. -//! A predicate is a [`WideFieldMask`] selection over it: `holds/2` selects +//! A predicate is a [`WideFieldMask`](lance_graph_contract::class_view::WideFieldMask) selection over it: `holds/2` selects //! proposition and world, `holds_via/3` adds the mode, `holds_via_rule/5` //! adds both rules. Selecting fewer fields can make two lens rows equal, so //! the projection is [`Projection::Set`] (Datalog: one fact) or @@ -36,12 +42,26 @@ //! # Not covered, refused //! //! Anything that is not one fixpoint of facts: a fact kind outside the Kripke -//! inputs, more than 64 worlds, propositions or rules (one register), and a -//! selection that is not one of the three predicates. +//! inputs, more than 64 worlds, propositions or rules (one register), more +//! than 15 parents of one world (one row), and a selection that is not one of +//! the three predicates. #![forbid(unsafe_code)] -use dr_math_binding_probe::relcomp::{Rows, Work, compose}; -use lance_graph_contract::class_view::WideFieldMask; +pub mod membrane; +pub mod rows; + +use dr_math_binding_probe::hhtl16::{LocalMap, MapRefusal}; +use dr_math_binding_probe::relcomp::{Chain, RelExpr, Rows, Work}; +use dr_math_binding_probe::{ + Axis, AxisKind, BoundDr64, Focus, FrameRevisions, FrameStore, Guards, MethodSignature, Operand, + Scope, bind_dr64, +}; +use lance_graph_contract::canonical_node::NodeRow; +use lance_graph_contract::morton8x8::Morton8x8; +use lance_graph_contract::register128::RegisterLanes; + +pub use membrane::{Golden, Intake, NameTable, Pop, Relation, intake, intake_under, parse_golden}; +use rows::{COLUMNS, Population, UNBOUND, columns, identity}; /// The slot count of one register axis. pub const SLOTS: usize = 64; @@ -60,8 +80,8 @@ const F_MODE: u8 = 2; const F_IMMEDIATE: u8 = 3; const F_SOURCE: u8 = 4; -/// The immediate rule upstream attributes every inherited holding to. -const INHERIT_RULE: &str = "r_kripke_inherit"; +const FOCUS: Focus = Focus { revision: 1 }; +const SCOPE: Scope = Scope { id: 1 }; /// Why an input or a selection is refused. #[derive(Clone, Debug, PartialEq, Eq)] @@ -72,6 +92,14 @@ pub enum Refusal { Arity(String), /// More than [`SLOTS`] distinct values on one axis. TooMany(&'static str), + /// The same address twice in one population. + Duplicate(&'static str), + /// An address no row of the population holds. + Unmapped(&'static str), + /// A world with more parents than one row holds. + TooManyParents { parents: usize }, + /// The register rails could not be bound. + Register(lance_graph_contract::hotplug::ActivationDrift), /// A golden line that is neither header, fact nor atom. Format(String), /// A field selection that is not `holds/2`, `holds_via/3` or @@ -88,48 +116,48 @@ pub enum Projection { Bag, } -#[derive(Default)] -struct Interner(Vec); - -impl Interner { - fn id(&mut self, name: &str, axis: &'static str) -> Result { - if let Some(i) = self.0.iter().position(|n| n == name) { - return Ok(i); - } - if self.0.len() == SLOTS { - return Err(Refusal::TooMany(axis)); - } - self.0.push(name.to_owned()); - Ok(self.0.len() - 1) - } -} +/// Types that hold addresses and numbers, never names. +#[doc(hidden)] +pub trait AddressOnly {} -/// A golden file: its fixture id, input facts and expected atoms. -pub struct Golden { - pub fixture_id: String, - pub facts: Vec>, - pub atoms: Vec, -} - -/// Parse one golden TSV. -pub fn parse_golden(text: &str) -> Result { - let mut g = Golden { - fixture_id: String::new(), - facts: Vec::new(), - atoms: Vec::new(), - }; - for line in text.lines() { - let mut cols = line.split('\t'); - match cols.next() { - Some("# fixture") => g.fixture_id = cols.next().unwrap_or_default().to_owned(), - Some(h) if h.starts_with('#') => {} - Some("fact") => g.facts.push(cols.map(str::to_owned).collect()), - Some("atom") => g.atoms.push(cols.collect::>().join("\t")), - _ => return Err(Refusal::Format(line.to_owned())), - } - } - Ok(g) +macro_rules! address_only { + ($($t:ty),* $(,)?) => { $(impl AddressOnly for $t {})* }; } +address_only!( + u8, + u16, + u32, + u64, + usize, + bool, + Morton8x8, + NodeRow, + RegisterLanes, + LocalMap, + FrameStore, + Work, + ModeTag, + Population, + Kb, + Mode, +); +impl AddressOnly for [T; N] {} +impl AddressOnly for Vec {} +impl AddressOnly for Option {} +impl AddressOnly for &T {} +impl AddressOnly for Holdings<'_> {} + +/// Compiles only for address-only types. +/// +/// ```compile_fail +/// mistaber_kripke_probe::assert_address_only::(); +/// ``` +/// +/// ```compile_fail +/// mistaber_kripke_probe::assert_address_only::>(); +/// ``` +#[doc(hidden)] +pub fn assert_address_only() {} fn or(a: &Rows, b: &Rows) -> Rows { std::array::from_fn(|i| a[i] | b[i]) @@ -157,90 +185,198 @@ fn bits(mut x: u64) -> impl Iterator { }) } -/// The Kripke inputs, one register per relation. +fn prepare(p: &Population, axis: &'static str) -> Result { + let ids: Vec = p + .rows + .iter() + .map(|r| u64::from(identity(&p.lanes, r).code())) + .collect(); + LocalMap::prepare(&ids).map_err(|e| match e { + MapRefusal::TooMany => Refusal::TooMany(axis), + MapRefusal::Duplicate => Refusal::Duplicate(axis), + _ => Refusal::Unmapped(axis), + }) +} + +fn local(map: &LocalMap, a: Morton8x8, axis: &'static str) -> Result { + map.local(u64::from(a.code())) + .map(usize::from) + .map_err(|_| Refusal::Unmapped(axis)) +} + +fn global(map: &LocalMap, local: usize) -> Morton8x8 { + let g = map.global(local as u8).expect("a mapped local position"); + Morton8x8::from_code(g as u16) +} + +/// The Kripke inputs: three populations of rows, their local maps, and one +/// register per relation. pub struct Kb { - worlds: Interner, - props: Interner, - rules: Interner, + worlds: Population, + props: Population, + rules: Population, + world_map: LocalMap, + prop_map: LocalMap, + rule_map: LocalMap, world_set: u64, asserts: Rows, endorses: Rows, overridden: Rows, - /// Row `parent`, bit `child`: `accessible(child, parent)`. + /// Row `parent`, bit `child`: derived from the parent addresses in the + /// world rows, nowhere else. children: Rows, asserts_rule: Vec, endorses_rule: Vec, + store: FrameStore, } impl Kb { /// Load fact tuples (`kind, args…`). Refuses any fact kind the Kripke /// rules do not read. - pub fn load(facts: &[Vec]) -> Result { + pub fn load(facts: &[Vec]) -> Result<(Self, NameTable), Refusal> { + let (taken, names) = intake(facts)?; + Ok((Self::assemble(taken)?, names)) + } + + /// Map each population to local positions and fill the relation + /// registers. The 64-slot limit is enforced here, by the local maps. + pub fn assemble(i: Intake) -> Result { + let world_map = prepare(&i.worlds, "world")?; + let prop_map = prepare(&i.props, "proposition")?; + let rule_map = prepare(&i.rules, "rule")?; let mut kb = Kb { - worlds: Interner::default(), - props: Interner::default(), - rules: Interner::default(), + store: FrameStore::new(FrameRevisions { + source: 1, + relation_map: 1, + coordinates: world_map.digest(), + }), world_set: 0, asserts: [0; SLOTS], endorses: [0; SLOTS], overridden: [0; SLOTS], children: [0; SLOTS], - asserts_rule: Vec::new(), - endorses_rule: Vec::new(), + asserts_rule: vec![[0; SLOTS]; rule_map.len()], + endorses_rule: vec![[0; SLOTS]; rule_map.len()], + worlds: i.worlds, + props: i.props, + rules: i.rules, + world_map, + prop_map, + rule_map, }; - for f in facts { - let (kind, args) = f.split_first().ok_or(Refusal::Format(String::new()))?; - let want = match kind.as_str() { - "world" => 1, - "asserts" | "endorses" | "accessible" => 2, - "override" | "asserts_rule" | "endorses_rule" => 3, - _ => return Err(Refusal::UnknownFact(kind.clone())), - }; - if args.len() != want { - return Err(Refusal::Arity(kind.clone())); - } - match kind.as_str() { - "world" => kb.world_set |= 1 << kb.worlds.id(&args[0], "world")?, - "accessible" => { - let child = kb.worlds.id(&args[0], "world")?; - let parent = kb.worlds.id(&args[1], "world")?; - kb.children[parent] |= 1 << child; + kb.derive_children()?; + for rel in &i.relations { + match *rel { + Relation::Declared { world } => { + kb.world_set |= 1 << local(&kb.world_map, world, "world")?; } - _ => { - let w = kb.worlds.id(&args[0], "world")?; - let p = kb.props.id(&args[1], "proposition")?; - match kind.as_str() { - "asserts" => kb.asserts[p] |= 1 << w, - "endorses" => kb.endorses[p] |= 1 << w, - "override" => kb.overridden[p] |= 1 << w, - _ => { - let r = kb.rules.id(&args[2], "rule")?; - for v in [&mut kb.asserts_rule, &mut kb.endorses_rule] { - v.resize(kb.rules.0.len(), [0; SLOTS]); - } - let table = if kind == "asserts_rule" { - &mut kb.asserts_rule - } else { - &mut kb.endorses_rule - }; - table[r][p] |= 1 << w; - } - } + Relation::Asserts { world, prop } => { + let (lw, lp) = kb.cell(world, prop)?; + kb.asserts[lp] |= 1 << lw; + } + Relation::Endorses { world, prop } => { + let (lw, lp) = kb.cell(world, prop)?; + kb.endorses[lp] |= 1 << lw; + } + Relation::Overridden { world, prop } => { + let (lw, lp) = kb.cell(world, prop)?; + kb.overridden[lp] |= 1 << lw; + } + Relation::AssertsRule { world, prop, rule } => { + let (lw, lp) = kb.cell(world, prop)?; + let lr = local(&kb.rule_map, rule, "rule")?; + kb.asserts_rule[lr][lp] |= 1 << lw; + } + Relation::EndorsesRule { world, prop, rule } => { + let (lw, lp) = kb.cell(world, prop)?; + let lr = local(&kb.rule_map, rule, "rule")?; + kb.endorses_rule[lr][lp] |= 1 << lw; } } } Ok(kb) } + /// Local `(world, proposition)` positions of one cell. + fn cell(&self, world: Morton8x8, prop: Morton8x8) -> Result<(usize, usize), Refusal> { + Ok(( + local(&self.world_map, world, "world")?, + local(&self.prop_map, prop, "proposition")?, + )) + } + + /// The only writer of `children`: every bound column of a world row after + /// column 0 is a parent of the world in column 0. + fn derive_children(&mut self) -> Result<(), Refusal> { + for row in &self.worlds.rows { + let cols = columns(&self.worlds.lanes, row); + let lw = local(&self.world_map, cols[0], "world")?; + for a in cols[1..COLUMNS].iter().filter(|a| **a != UNBOUND) { + let lp = local(&self.world_map, *a, "world")?; + self.children[lp] |= 1 << lw; + } + } + Ok(()) + } + + pub fn world_address(&self, local: usize) -> Morton8x8 { + global(&self.world_map, local) + } + + pub fn prop_address(&self, local: usize) -> Morton8x8 { + global(&self.prop_map, local) + } + + pub fn rule_address(&self, local: usize) -> Morton8x8 { + global(&self.rule_map, local) + } + + pub fn world_count(&self) -> usize { + self.world_map.len() + } + + pub fn prop_count(&self) -> usize { + self.prop_map.len() + } + + pub fn rule_count(&self) -> usize { + self.rules.rows.len() + } + /// Solve: the holds fixpoint, then both lineages. pub fn solve(&self) -> Holdings<'_> { + let (wc, pc) = (self.worlds.lanes.concept(), self.props.lanes.concept()); + let w_axis = Axis { + class: wc, + kind: AxisKind::Identity, + }; + let p_axis = Axis { + class: pc, + kind: AxisKind::Property, + }; + let m_access = MethodSignature::presence(wc, 0, w_axis, w_axis); + let m_holds = MethodSignature::presence(pc, 0, p_axis, w_axis); + let m_asserts = MethodSignature::presence(pc, 1, p_axis, w_axis); + let m_endorses = MethodSignature::presence(pc, 2, p_axis, w_axis); + let m_overridden = MethodSignature::presence(pc, 3, p_axis, w_axis); + let guards = Guards { + frame: self.store.seal(), + focus: FOCUS, + scope: SCOPE, + }; + let access = bind(&self.store, &guards, m_access, &self.children); + let asserts = bind(&self.store, &guards, m_asserts, &self.asserts); + let endorses = bind(&self.store, &guards, m_endorses, &self.endorses); + let overridden = bind(&self.store, &guards, m_overridden, &self.overridden); let mut work = Work::default(); - let block = or(&or(&self.asserts, &self.endorses), &self.overridden); - let direct = and_row(&or(&self.asserts, &self.endorses), self.world_set); - let (holds, steps) = lfp(&direct, None, &self.children, &block, &mut work); - let lineage = - |base: &Rows, work: &mut Work| lfp(base, Some(&holds), &self.children, &block, work).0; - let sources = (0..self.rules.0.len()) + let block = or(&or(asserts.rows, endorses.rows), overridden.rows); + let direct = and_row(&or(asserts.rows, endorses.rows), self.world_set); + let hop = |from: &Rows, work: &mut Work| -> Rows { + hop(&self.store, &guards, m_holds, &access, from, work) + }; + let (holds, steps) = lfp(&direct, None, &hop, &block, &mut work); + let lineage = |base: &Rows, work: &mut Work| lfp(base, Some(&holds), &hop, &block, work).0; + let sources = (0..self.rule_count()) .map(|r| { let base = and_row( &or(&self.asserts_rule[r], &self.endorses_rule[r]), @@ -249,7 +385,7 @@ impl Kb { lineage(&base, &mut work) }) .collect(); - let origins = (0..self.worlds.0.len()) + let origins = (0..self.world_count()) .map(|o| lineage(&and_row(&direct, 1 << o), &mut work)) .collect(); Holdings { @@ -265,19 +401,61 @@ impl Kb { } } +/// Bind one register through the DR64 admission. +fn bind<'a>( + store: &FrameStore, + guards: &Guards, + m: MethodSignature, + rows: &'a Rows, +) -> BoundDr64<'a> { + bind_dr64( + store, + m, + m, + guards, + (FOCUS, SCOPE), + Operand { + rows, + validity: None, + }, + ) + .expect("a register of this store binds under its own frame") +} + +/// `from ∘ children` as a typed two-operand chain. +fn hop( + store: &FrameStore, + guards: &Guards, + m_holds: MethodSignature, + children: &BoundDr64<'_>, + from: &Rows, + work: &mut Work, +) -> Rows { + let chain = Chain::new( + store, + vec![bind(store, guards, m_holds, from), children.clone()], + ) + .expect("holds ∘ children is typed"); + let (rows, w) = chain + .eval(&RelExpr::comp(RelExpr::Leaf(0), RelExpr::Leaf(1))) + .expect("the order covers the chain"); + work.row_ors += w.row_ors; + rows +} + /// `X = base ∪ ((gate(X) ∘ children) ∧ ¬block)` to its least fixpoint. /// `gate = None` gates by `X` itself; `Some(h)` gates by `X ∧ h`. fn lfp( base: &Rows, gate: Option<&Rows>, - children: &Rows, + hop: &dyn Fn(&Rows, &mut Work) -> Rows, block: &Rows, work: &mut Work, ) -> (Rows, usize) { let mut cur = *base; for step in 1..=SLOTS + 1 { let from = gate.map_or(cur, |h| and(&cur, h)); - let next = or(base, &and_not(&compose(&from, children, work), block)); + let next = or(base, &and_not(&hop(&from, work), block)); if next == cur { return (cur, step); } @@ -288,9 +466,18 @@ fn lfp( ) } +/// Which holding a [`Mode`] is. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +enum ModeTag { + Asserted, + Endorsed, + /// Inherited from the world at this local position. + Inherited(usize), +} + /// One holding mode: its cells, and per rule the cells that rule supports. struct Mode { - label: String, + tag: ModeTag, cells: Rows, rules: Vec, } @@ -327,14 +514,6 @@ pub struct Holdings<'a> { } impl Holdings<'_> { - fn w(&self, i: usize) -> &str { - &self.kb.worlds.0[i] - } - - fn p(&self, i: usize) -> &str { - &self.kb.props.0[i] - } - /// `holds_via(inherited(parent), p, ·)` as a world mask. fn inherited_from(&self, parent: usize, p: usize) -> u64 { if self.holds[p] >> parent & 1 == 0 { @@ -347,26 +526,20 @@ impl Holdings<'_> { /// under that mode. fn modes(&self) -> Vec { let kb = self.kb; - let n = kb.props.0.len(); - let direct = |table: &Rows, rules: &[Rows]| Mode { + let n = kb.prop_count(); + let direct = |tag, table: &Rows, rules: &[Rows]| Mode { + tag, cells: and_row(table, kb.world_set), rules: rules .iter() .map(|r| and(r, &and_row(table, kb.world_set))) .collect(), - label: String::new(), }; let mut out = vec![ - Mode { - label: "asserted".to_owned(), - ..direct(&kb.asserts, &kb.asserts_rule) - }, - Mode { - label: "endorsed".to_owned(), - ..direct(&kb.endorses, &kb.endorses_rule) - }, + direct(ModeTag::Asserted, &kb.asserts, &kb.asserts_rule), + direct(ModeTag::Endorsed, &kb.endorses, &kb.endorses_rule), ]; - for par in 0..kb.worlds.0.len() { + for par in 0..kb.world_count() { let cells: Rows = std::array::from_fn(|p| { if p < n { self.inherited_from(par, p) @@ -382,181 +555,13 @@ impl Holdings<'_> { }) .collect(); out.push(Mode { - label: format!("inherited({})", self.w(par)), + tag: ModeTag::Inherited(par), cells, rules, }); } out } - - /// How many lens rows hold `p` in `w`: the multiplicity a bag projection - /// to `holds/2` reports. A lens row is one (mode, source rule); a holding - /// with no rule is one row with empty rule fields. - pub fn bag_multiplicity(&self, prop: &str, world: &str) -> usize { - let (Some(p), Some(w)) = ( - self.kb.props.0.iter().position(|n| n == prop), - self.kb.worlds.0.iter().position(|n| n == world), - ) else { - return 0; - }; - self.modes().iter().map(|m| m.rows(p, w)).sum() - } - - /// Materialize one predicate as atoms: a [`WideFieldMask`] selection over - /// [`HOLDINGS_FIELDS`]. For the test oracle only. - pub fn materialize_selection( - &self, - sel: &WideFieldMask, - proj: Projection, - ) -> Result, Refusal> { - let has = |f| sel.has(f); - let base = has(F_PROP) && has(F_WORLD); - let mut out = Vec::new(); - match ( - base, - has(F_MODE), - has(F_IMMEDIATE), - has(F_SOURCE), - sel.count(), - ) { - (true, false, false, false, 2) => match proj { - Projection::Set => { - for p in 0..self.kb.props.0.len() { - for w in bits(self.holds[p]) { - out.push(format!("holds({},{})", self.p(p), self.w(w))); - } - } - } - Projection::Bag => { - for m in self.modes() { - for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { - for w in bits(row) { - for _ in 0..m.rows(p, w) { - out.push(format!("holds({},{})", self.p(p), self.w(w))); - } - } - } - } - } - }, - (true, true, false, false, 3) => { - for m in self.modes() { - for (p, &row) in m.cells.iter().enumerate().take(self.kb.props.0.len()) { - for w in bits(row) { - let copies = match proj { - Projection::Set => 1, - Projection::Bag => m.rows(p, w), - }; - for _ in 0..copies { - out.push(format!( - "holds_via({},{},{})", - m.label, - self.p(p), - self.w(w) - )); - } - } - } - } - } - (true, true, true, true, 5) => self.rule_atoms(&mut out), - _ => return Err(Refusal::Selection), - } - Ok(out) - } - - fn rule_atoms(&self, out: &mut Vec) { - let kb = self.kb; - for (r, rule) in kb.rules.0.iter().enumerate() { - for (mode, table) in [ - ("asserted", &kb.asserts_rule[r]), - ("endorsed", &kb.endorses_rule[r]), - ] { - for (p, &row) in table.iter().enumerate().take(kb.props.0.len()) { - for w in bits(row & kb.world_set) { - out.push(format!( - "holds_via_rule({mode},{},{},{rule},{rule})", - self.p(p), - self.w(w) - )); - } - } - } - for par in 0..kb.worlds.0.len() { - for p in 0..kb.props.0.len() { - if self.sources[r][p] >> par & 1 == 1 { - for w in bits(self.inherited_from(par, p)) { - out.push(format!( - "holds_via_rule(inherited({}),{},{},{INHERIT_RULE},{rule})", - self.w(par), - self.p(p), - self.w(w) - )); - } - } - } - } - } - } - - /// Every Kripke atom the golden files carry, sorted. `proj` applies to - /// `holds/2`, the only selection where rows can coincide. - pub fn materialize_atoms(&self, proj: Projection) -> Vec { - let sel = |f: &[u8]| WideFieldMask::from_positions(f); - let mut out = Vec::new(); - for (s, pr) in [ - (sel(&[F_PROP, F_WORLD]), proj), - (sel(&[F_PROP, F_WORLD, F_MODE]), Projection::Set), - ( - sel(&[F_PROP, F_WORLD, F_MODE, F_IMMEDIATE, F_SOURCE]), - Projection::Set, - ), - ] { - out.extend( - self.materialize_selection(&s, pr) - .expect("a supported selection"), - ); - } - let kb = self.kb; - for p in 0..kb.props.0.len() { - let inherited: u64 = (0..kb.worlds.0.len()) - .map(|par| self.inherited_from(par, p)) - .fold(0, |a, b| a | b); - let moderate: u64 = bits(self.direct[p]) - .map(|par| self.inherited_from(par, p)) - .fold(0, |a, b| a | b); - let strong = self.direct[p]; - for (level, m) in [ - ("strong", strong), - ("moderate", moderate), - ("weak", inherited & !strong & !moderate), - ] { - for w in bits(m) { - out.push(format!( - "holding_strength({level},{},{})", - self.p(p), - self.w(w) - )); - } - } - for (o, cells) in self.origins.iter().enumerate() { - for w in bits(cells[p]) { - out.push(format!( - "inheritance_source({},{},{})", - self.p(p), - self.w(w), - self.w(o) - )); - } - } - for w in bits(kb.overridden[p]) { - out.push(format!("overridden({},{})", self.p(p), self.w(w))); - } - } - out.sort(); - out - } } #[cfg(test)] @@ -577,6 +582,15 @@ mod tests { .collect() } + fn fact(parts: &[&str]) -> Vec { + parts.iter().map(|s| (*s).to_owned()).collect() + } + + fn local_of(map: &LocalMap, names: &NameTable, pop: Pop, name: &str) -> usize { + let a = names.address_of(pop, name).expect(name); + usize::from(map.local(u64::from(a.code())).expect(name)) + } + /// The probe's lineage already lives on three 64 x 64 x 64 index spaces, /// each a stack of 64 x 64 registers (row = proposition, bit = world) /// along a third axis: @@ -594,9 +608,9 @@ mod tests { use lance_graph_contract::morton8x8::Morton8x8; let (mut two_parents, mut two_origins) = (false, false); for g in all_goldens() { - let kb = Kb::load(&g.facts).unwrap(); + let (kb, _names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); - let nw = kb.worlds.0.len(); + let nw = kb.world_count(); let v: Vec = (0..nw) .map(|par| std::array::from_fn(|p| h.inherited_from(par, p))) .collect(); @@ -614,7 +628,7 @@ mod tests { } for cube in [&v, &h.origins, &h.sources] { for slice in cube.iter() { - for p in 0..kb.props.0.len() { + for p in 0..kb.prop_count() { for w in 0..nw { let code = Morton8x8::from_xy(p as u8, w as u8); let bit = slice[p] >> w & 1 == 1; @@ -635,21 +649,160 @@ mod tests { // F5: r_orphan has a rule companion but no assertion, so p holds // nowhere. Its lineage must stay at its own cell, not flow to a. let g = parse_golden(include_str!("../goldens/F5-gates.tsv")).unwrap(); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); - let r = kb.rules.0.iter().position(|n| n == "r_orphan").unwrap(); - let p = kb.props.0.iter().position(|n| n == "p").unwrap(); - let base = kb.worlds.0.iter().position(|n| n == "base").unwrap(); + let r = local_of(&kb.rule_map, &names, Pop::Rule, "r_orphan"); + let p = local_of(&kb.prop_map, &names, Pop::Proposition, "p"); + let base = local_of(&kb.world_map, &names, Pop::World, "base"); assert_eq!(h.holds[p], 0); assert_eq!(h.sources[r][p], 1 << base); // Every lineage cell outside the base lies inside holds. for s in h.sources.iter().chain(&h.origins) { for (i, row) in s.iter().enumerate() { - let base_row = (0..kb.rules.0.len()) + let base_row = (0..kb.rule_count()) .map(|r| (kb.asserts_rule[r][i] | kb.endorses_rule[r][i]) & kb.world_set) .fold(h.direct[i], |a, b| a | b); assert_eq!(row & !base_row & !h.holds[i], 0); } } } + + /// Destructures each struct exhaustively (no `..`), so adding a field + /// that is not address-only, or any field at all, stops compiling here. + fn fields_are_address_only(kb: &Kb, h: &Holdings<'_>, m: &Mode, p: &Population) { + fn ok(_: &T) {} + let Kb { + worlds, + props, + rules, + world_map, + prop_map, + rule_map, + world_set, + asserts, + endorses, + overridden, + children, + asserts_rule, + endorses_rule, + store, + } = kb; + ok(worlds); + ok(props); + ok(rules); + ok(world_map); + ok(prop_map); + ok(rule_map); + ok(world_set); + ok(asserts); + ok(endorses); + ok(overridden); + ok(children); + ok(asserts_rule); + ok(endorses_rule); + ok(store); + let Holdings { + kb, + block, + direct, + holds, + sources, + origins, + steps, + work, + } = h; + ok(kb); + ok(block); + ok(direct); + ok(holds); + ok(sources); + ok(origins); + ok(steps); + ok(work); + let Mode { tag, cells, rules } = m; + ok(tag); + ok(cells); + ok(rules); + let Population { lanes, rows } = p; + ok(lanes); + ok(rows); + } + + /// FAILS IF a String, a `NameTable` or a `Golden` becomes a field of + /// `Kb`, `Holdings`, `Mode` or `Population` (compile error), or the bound + /// stops rejecting `String` (the two compile_fail doctests on + /// `assert_address_only`). + #[test] + fn the_solved_state_holds_no_string() { + let g = all_goldens() + .into_iter() + .find(|g| g.fixture_id == "F1-modes") + .unwrap(); + let (kb, _names) = Kb::load(&g.facts).unwrap(); + let h = kb.solve(); + let modes = h.modes(); + fields_are_address_only(&kb, &h, &modes[0], &kb.worlds); + assert!(modes.len() > 2, "inherited modes exist"); + } + + /// FAILS IF a world with two parents does not get both as in-row + /// addresses that derive to exactly the old accessibility register. + #[test] + fn a_world_with_two_parents_derives_the_old_accessibility() { + let facts = vec![ + fact(&["world", "base"]), + fact(&["world", "mechaber"]), + fact(&["world", "rema"]), + fact(&["world", "ashk_ah"]), + fact(&["accessible", "mechaber", "base"]), + fact(&["accessible", "rema", "base"]), + fact(&["accessible", "ashk_ah", "mechaber"]), + fact(&["accessible", "ashk_ah", "rema"]), + fact(&["asserts", "mechaber", "p"]), + fact(&["asserts", "rema", "q"]), + ]; + let oracle = |facts: &[Vec], label: &str| { + let (kb, names) = Kb::load(facts).unwrap(); + let mut pairs = std::collections::BTreeSet::new(); + for f in facts.iter().filter(|f| f[0] == "accessible") { + let c = local_of(&kb.world_map, &names, Pop::World, &f[1]); + let p = local_of(&kb.world_map, &names, Pop::World, &f[2]); + assert_eq!(kb.children[p] >> c & 1, 1, "{label}: {} <- {}", f[1], f[2]); + pairs.insert((c, p)); + } + let total: u32 = kb.children.iter().map(|r| r.count_ones()).sum(); + assert_eq!(total as usize, pairs.len(), "{label}"); + kb + }; + let kb = oracle(&facts, "ashk_ah"); + let (_, names) = Kb::load(&facts).unwrap(); + let atoms = kb.solve().materialize_atoms(&names, Projection::Set); + for a in [ + "holds(p,ashk_ah)", + "holds(q,ashk_ah)", + "holds_via(inherited(rema),q,ashk_ah)", + ] { + assert!(atoms.contains(&a.to_owned()), "{a}"); + } + let mut with_edges = 0; + for g in all_goldens() { + let kb = oracle(&g.facts, &g.fixture_id); + with_edges += usize::from(kb.children.iter().any(|r| *r != 0)); + } + assert!(with_edges > 0, "some golden has accessibility"); + + // Accessibility is not a relation: this match stops compiling if an + // accessible variant is added. + let (taken, _) = intake(&facts).unwrap(); + for rel in &taken.relations { + match rel { + Relation::Declared { .. } + | Relation::Asserts { .. } + | Relation::Endorses { .. } + | Relation::Overridden { .. } + | Relation::AssertsRule { .. } + | Relation::EndorsesRule { .. } => {} + } + } + } } diff --git a/crates/mistaber-kripke-probe/src/membrane.rs b/crates/mistaber-kripke-probe/src/membrane.rs new file mode 100644 index 000000000..e718647b3 --- /dev/null +++ b/crates/mistaber-kripke-probe/src/membrane.rs @@ -0,0 +1,470 @@ +//! The membrane: the only module that holds names. +//! +//! Names enter here (the golden parse, the fact tuples) and leave here (the +//! atom renderer). Inside, a node is an address in an HHTL16 row. The +//! [`NameTable`] is never held by [`Kb`] or [`Holdings`]. + +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_contract::morton8x8::Morton8x8; + +use crate::rows::{ + COLUMNS, Concepts, MAX_PARENTS, Population, address, bind_populations, blank_row, write_columns, +}; +use crate::{ + F_IMMEDIATE, F_MODE, F_PROP, F_SOURCE, F_WORLD, Holdings, Kb, Mode, ModeTag, Projection, + Refusal, bits, +}; + +/// The immediate rule upstream attributes every inherited holding to. +const INHERIT_RULE: &str = "r_kripke_inherit"; + +/// A golden file: its fixture id, input facts and expected atoms. +pub struct Golden { + pub fixture_id: String, + pub facts: Vec>, + pub atoms: Vec, +} + +/// Parse one golden TSV. +pub fn parse_golden(text: &str) -> Result { + let mut g = Golden { + fixture_id: String::new(), + facts: Vec::new(), + atoms: Vec::new(), + }; + for line in text.lines() { + let mut cols = line.split('\t'); + match cols.next() { + Some("# fixture") => g.fixture_id = cols.next().unwrap_or_default().to_owned(), + Some(h) if h.starts_with('#') => {} + Some("fact") => g.facts.push(cols.map(str::to_owned).collect()), + Some("atom") => g.atoms.push(cols.collect::>().join("\t")), + _ => return Err(Refusal::Format(line.to_owned())), + } + } + Ok(g) +} + +/// The three populations. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Pop { + World, + Proposition, + Rule, +} + +impl Pop { + fn axis(self) -> &'static str { + match self { + Pop::World => "world", + Pop::Proposition => "proposition", + Pop::Rule => "rule", + } + } +} + +/// Names by first-appearance ordinal, one list per population. Lives only at +/// the membrane. +#[derive(Default)] +pub struct NameTable { + worlds: Vec, + props: Vec, + rules: Vec, +} + +impl NameTable { + fn list(&self, pop: Pop) -> &Vec { + match pop { + Pop::World => &self.worlds, + Pop::Proposition => &self.props, + Pop::Rule => &self.rules, + } + } + + /// First-appearance ordinal of `name`. Refuses only when the ordinal + /// space is exhausted; the 64-slot limit belongs to the local map. + fn ordinal(&mut self, pop: Pop, name: &str) -> Result { + let list = match pop { + Pop::World => &mut self.worlds, + Pop::Proposition => &mut self.props, + Pop::Rule => &mut self.rules, + }; + if let Some(i) = list.iter().position(|n| n == name) { + return Ok(i as u16); + } + if list.len() >= usize::from(u16::MAX) { + return Err(Refusal::TooMany(pop.axis())); + } + list.push(name.to_owned()); + Ok((list.len() - 1) as u16) + } + + pub fn address_of(&self, pop: Pop, name: &str) -> Option { + let i = self.list(pop).iter().position(|n| n == name)?; + Some(address(i as u16)) + } + + pub fn name(&self, pop: Pop, a: Morton8x8) -> &str { + &self.list(pop)[usize::from(a.code()) - 1] + } +} + +/// One input relation, over addresses. Accessibility is not here: it lives +/// only in world rows. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Relation { + Declared { + world: Morton8x8, + }, + Asserts { + world: Morton8x8, + prop: Morton8x8, + }, + Endorses { + world: Morton8x8, + prop: Morton8x8, + }, + Overridden { + world: Morton8x8, + prop: Morton8x8, + }, + AssertsRule { + world: Morton8x8, + prop: Morton8x8, + rule: Morton8x8, + }, + EndorsesRule { + world: Morton8x8, + prop: Morton8x8, + rule: Morton8x8, + }, +} + +/// Facts taken in: three populations of rows and the non-accessibility +/// relations over their addresses. +pub struct Intake { + pub worlds: Population, + pub props: Population, + pub rules: Population, + pub relations: Vec, +} + +/// [`intake_under`] with the lab concepts. +pub fn intake(facts: &[Vec]) -> Result<(Intake, NameTable), Refusal> { + intake_under(facts, Concepts::LAB) +} + +/// Take fact tuples (`kind, args...`) in under `c`. Refuses any fact kind the +/// Kripke rules do not read, and a world with more than [`MAX_PARENTS`] +/// parents. +pub fn intake_under(facts: &[Vec], c: Concepts) -> Result<(Intake, NameTable), Refusal> { + let mut names = NameTable::default(); + let mut relations = Vec::new(); + let mut parents: Vec> = Vec::new(); + for f in facts { + let (kind, args) = f.split_first().ok_or(Refusal::Format(String::new()))?; + let want = match kind.as_str() { + "world" => 1, + "asserts" | "endorses" | "accessible" => 2, + "override" | "asserts_rule" | "endorses_rule" => 3, + _ => return Err(Refusal::UnknownFact(kind.clone())), + }; + if args.len() != want { + return Err(Refusal::Arity(kind.clone())); + } + match kind.as_str() { + "world" => { + let w = names.ordinal(Pop::World, &args[0])?; + relations.push(Relation::Declared { world: address(w) }); + } + "accessible" => { + let child = names.ordinal(Pop::World, &args[0])?; + let parent = names.ordinal(Pop::World, &args[1])?; + if parents.len() <= usize::from(child) { + parents.resize(usize::from(child) + 1, Vec::new()); + } + let ps = &mut parents[usize::from(child)]; + if !ps.contains(&parent) { + ps.push(parent); + } + } + _ => { + let w = names.ordinal(Pop::World, &args[0])?; + let p = names.ordinal(Pop::Proposition, &args[1])?; + let (world, prop) = (address(w), address(p)); + relations.push(match kind.as_str() { + "asserts" => Relation::Asserts { world, prop }, + "endorses" => Relation::Endorses { world, prop }, + "override" => Relation::Overridden { world, prop }, + _ => { + let rule = address(names.ordinal(Pop::Rule, &args[2])?); + if kind == "asserts_rule" { + Relation::AssertsRule { world, prop, rule } + } else { + Relation::EndorsesRule { world, prop, rule } + } + } + }); + } + } + } + parents.resize(names.worlds.len(), Vec::new()); + let [wl, pl, rl] = bind_populations(&c)?; + let mut worlds = Population { + lanes: wl, + rows: Vec::new(), + }; + for (o, ps) in parents.iter().enumerate() { + if ps.len() > MAX_PARENTS { + return Err(Refusal::TooManyParents { parents: ps.len() }); + } + let cols: Vec = std::iter::once(address(o as u16)) + .chain(ps.iter().map(|&p| address(p))) + .collect(); + debug_assert!(cols.len() <= COLUMNS); + let mut row = blank_row(); + write_columns(&wl, &mut row, &cols); + worlds.rows.push(row); + } + let single = |lanes, n: usize| { + let mut p = Population { + lanes, + rows: Vec::new(), + }; + for o in 0..n { + let mut row = blank_row(); + write_columns(&lanes, &mut row, &[address(o as u16)]); + p.rows.push(row); + } + p + }; + let props = single(pl, names.props.len()); + let rules = single(rl, names.rules.len()); + Ok(( + Intake { + worlds, + props, + rules, + relations, + }, + names, + )) +} + +impl Mode { + fn label(&self, names: &NameTable, kb: &Kb) -> String { + match self.tag { + ModeTag::Asserted => "asserted".to_owned(), + ModeTag::Endorsed => "endorsed".to_owned(), + ModeTag::Inherited(par) => { + format!( + "inherited({})", + names.name(Pop::World, kb.world_address(par)) + ) + } + } + } +} + +impl Holdings<'_> { + fn wn<'n>(&self, names: &'n NameTable, i: usize) -> &'n str { + names.name(Pop::World, self.kb.world_address(i)) + } + + fn pn<'n>(&self, names: &'n NameTable, i: usize) -> &'n str { + names.name(Pop::Proposition, self.kb.prop_address(i)) + } + + /// How many lens rows hold `prop` in `world`: the multiplicity a bag + /// projection to `holds/2` reports. A lens row is one (mode, source + /// rule); a holding with no rule is one row with empty rule fields. + pub fn bag_multiplicity(&self, names: &NameTable, prop: &str, world: &str) -> usize { + let local = |pop, map: &dyn Fn(u64) -> Option, name: &str| { + names + .address_of(pop, name) + .and_then(|a| map(u64::from(a.code()))) + }; + let kb = self.kb; + let (Some(p), Some(w)) = ( + local(Pop::Proposition, &|g| kb.prop_map.local(g).ok(), prop), + local(Pop::World, &|g| kb.world_map.local(g).ok(), world), + ) else { + return 0; + }; + self.modes() + .iter() + .map(|m| m.rows(usize::from(p), usize::from(w))) + .sum() + } + + /// Materialize one predicate as atoms: a [`WideFieldMask`] selection over + /// [`HOLDINGS_FIELDS`](crate::HOLDINGS_FIELDS). For the test oracle only. + pub fn materialize_selection( + &self, + names: &NameTable, + sel: &WideFieldMask, + proj: Projection, + ) -> Result, Refusal> { + let has = |f| sel.has(f); + let base = has(F_PROP) && has(F_WORLD); + let kb = self.kb; + let mut out = Vec::new(); + match ( + base, + has(F_MODE), + has(F_IMMEDIATE), + has(F_SOURCE), + sel.count(), + ) { + (true, false, false, false, 2) => match proj { + Projection::Set => { + for p in 0..kb.prop_count() { + for w in bits(self.holds[p]) { + out.push(format!( + "holds({},{})", + self.pn(names, p), + self.wn(names, w) + )); + } + } + } + Projection::Bag => { + for m in self.modes() { + for (p, &row) in m.cells.iter().enumerate().take(kb.prop_count()) { + for w in bits(row) { + for _ in 0..m.rows(p, w) { + out.push(format!( + "holds({},{})", + self.pn(names, p), + self.wn(names, w) + )); + } + } + } + } + } + }, + (true, true, false, false, 3) => { + for m in self.modes() { + let label = m.label(names, kb); + for (p, &row) in m.cells.iter().enumerate().take(kb.prop_count()) { + for w in bits(row) { + let copies = match proj { + Projection::Set => 1, + Projection::Bag => m.rows(p, w), + }; + for _ in 0..copies { + out.push(format!( + "holds_via({},{},{})", + label, + self.pn(names, p), + self.wn(names, w) + )); + } + } + } + } + } + (true, true, true, true, 5) => self.rule_atoms(names, &mut out), + _ => return Err(Refusal::Selection), + } + Ok(out) + } + + fn rule_atoms(&self, names: &NameTable, out: &mut Vec) { + let kb = self.kb; + for r in 0..kb.rule_count() { + let rule = names.name(Pop::Rule, kb.rule_address(r)); + for (mode, table) in [ + ("asserted", &kb.asserts_rule[r]), + ("endorsed", &kb.endorses_rule[r]), + ] { + for (p, &row) in table.iter().enumerate().take(kb.prop_count()) { + for w in bits(row & kb.world_set) { + out.push(format!( + "holds_via_rule({mode},{},{},{rule},{rule})", + self.pn(names, p), + self.wn(names, w) + )); + } + } + } + for par in 0..kb.world_count() { + for p in 0..kb.prop_count() { + if self.sources[r][p] >> par & 1 == 1 { + for w in bits(self.inherited_from(par, p)) { + out.push(format!( + "holds_via_rule(inherited({}),{},{},{INHERIT_RULE},{rule})", + self.wn(names, par), + self.pn(names, p), + self.wn(names, w) + )); + } + } + } + } + } + } + + /// Every Kripke atom the golden files carry, sorted. `proj` applies to + /// `holds/2`, the only selection where rows can coincide. + pub fn materialize_atoms(&self, names: &NameTable, proj: Projection) -> Vec { + let sel = |f: &[u8]| WideFieldMask::from_positions(f); + let mut out = Vec::new(); + for (s, pr) in [ + (sel(&[F_PROP, F_WORLD]), proj), + (sel(&[F_PROP, F_WORLD, F_MODE]), Projection::Set), + ( + sel(&[F_PROP, F_WORLD, F_MODE, F_IMMEDIATE, F_SOURCE]), + Projection::Set, + ), + ] { + out.extend( + self.materialize_selection(names, &s, pr) + .expect("a supported selection"), + ); + } + let kb = self.kb; + for p in 0..kb.prop_count() { + let inherited: u64 = (0..kb.world_count()) + .map(|par| self.inherited_from(par, p)) + .fold(0, |a, b| a | b); + let moderate: u64 = bits(self.direct[p]) + .map(|par| self.inherited_from(par, p)) + .fold(0, |a, b| a | b); + let strong = self.direct[p]; + for (level, m) in [ + ("strong", strong), + ("moderate", moderate), + ("weak", inherited & !strong & !moderate), + ] { + for w in bits(m) { + out.push(format!( + "holding_strength({level},{},{})", + self.pn(names, p), + self.wn(names, w) + )); + } + } + for (o, cells) in self.origins.iter().enumerate() { + for w in bits(cells[p]) { + out.push(format!( + "inheritance_source({},{},{})", + self.pn(names, p), + self.wn(names, w), + self.wn(names, o) + )); + } + } + for w in bits(kb.overridden[p]) { + out.push(format!( + "overridden({},{})", + self.pn(names, p), + self.wn(names, w) + )); + } + } + out.sort(); + out + } +} diff --git a/crates/mistaber-kripke-probe/src/rows.rs b/crates/mistaber-kripke-probe/src/rows.rs new file mode 100644 index 000000000..da922aabc --- /dev/null +++ b/crates/mistaber-kripke-probe/src/rows.rs @@ -0,0 +1,119 @@ +//! HHTL16 node rows, address-only. +//! +//! One node is one [`NodeRow`] whose `Register0` rail holds the `x` bytes and +//! whose `Register1` rail the `y` bytes of sixteen [`Morton8x8`] columns. +//! Column 0 is the node's own identity; columns 1..=15 hold the addresses of +//! other nodes (a world's parents). Code 0 (`(0, 0)`) is unbound. +//! +//! The row carries no name and no classid: the classid is the concept of the +//! [`RegisterLanes`] the population was resolved under. + +use lance_graph_contract::canonical_node::{NodeGuid, NodeRow, ReadMode, TailVariant, ValueSchema}; +use lance_graph_contract::hotplug::{Activation, SlabDeclaration, SlabReading}; +use lance_graph_contract::morton8x8::Morton8x8; +use lance_graph_contract::register128::{Register128, RegisterLanes, RegisterRails}; +use lance_graph_contract::soa_envelope::ENVELOPE_LAYOUT_VERSION; + +use crate::Refusal; + +/// Columns per row. +pub const COLUMNS: usize = 16; +/// Parents one world row can hold (column 0 is the identity). +pub const MAX_PARENTS: usize = COLUMNS - 1; +/// The empty column. +pub const UNBOUND: Morton8x8 = Morton8x8::from_xy(0, 0); + +/// Lab stand-ins (same 0x7F range as xlog-relcomp-probe/tests/dto_binding.rs); +/// not minted. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Concepts { + pub world: u16, + pub proposition: u16, + pub rule: u16, +} + +impl Concepts { + pub const LAB: Concepts = Concepts { + world: 0x7F11, + proposition: 0x7F12, + rule: 0x7F13, + }; +} + +/// One bound population: its lanes and its rows. +pub struct Population { + pub lanes: RegisterLanes, + pub rows: Vec, +} + +/// Address rule: population-local ordinal `o` (first appearance) maps to +/// Morton code `o + 1`. `from_code` is a bijection on `u16` and `o + 1 >= 1`, +/// so two ordinals never collide and no identity is ever [`UNBOUND`]. The +/// address is meaningful only under its population's concept. +pub fn address(ordinal: u16) -> Morton8x8 { + Morton8x8::from_code(ordinal + 1) +} + +const SLAB: SlabDeclaration = SlabDeclaration { + reading: SlabReading::Register128, + value_schema: ValueSchema::Full, + layout_version: ENVELOPE_LAYOUT_VERSION, +}; + +/// One activation declaring all three concepts, then resolve and bind two +/// register rails per concept. Order: `[world, proposition, rule]`. +pub fn bind_populations(c: &Concepts) -> Result<[RegisterLanes; 3], Refusal> { + let concepts = [c.world, c.proposition, c.rule]; + let activation = Activation::new( + Vec::new(), + Vec::new(), + concepts + .iter() + .map(|&k| (k, ReadMode::PLUG_AND_PLAY_V3)) + .collect(), + ); + let mut out = Vec::with_capacity(3); + for k in concepts { + let lanes = activation + .resolve_for_context(k, Some(&SLAB)) + .and_then(|r| r.bind_register128(RegisterRails::Two)) + .map_err(Refusal::Register)?; + out.push(lanes); + } + Ok([out[0], out[1], out[2]]) +} + +/// An all-zero V3 row: key minted through `mint_for`, empty edges, empty value. +pub fn blank_row() -> NodeRow { + NodeRow { + key: NodeGuid::mint_for(TailVariant::V3, NodeGuid::CLASSID_DEFAULT, 0, 0, 0, 0, 0, 0), + edges: Default::default(), + value: [0; 480], + } +} + +/// `R0[k] = cols[k].x()`, `R1[k] = cols[k].y()` for `k < cols.len()`; the +/// remaining columns stay `(0, 0)`. Callers refuse more than [`COLUMNS`] +/// columns first. +pub fn write_columns(lanes: &RegisterLanes, row: &mut NodeRow, cols: &[Morton8x8]) { + assert!(cols.len() <= COLUMNS, "a row holds {COLUMNS} columns"); + let (mut xs, mut ys) = ([0u8; COLUMNS], [0u8; COLUMNS]); + for (k, a) in cols.iter().enumerate() { + xs[k] = a.x(); + ys[k] = a.y(); + } + assert!(lanes.set(row, 0, Register128(xs)), "rail 0 granted"); + assert!(lanes.set(row, 1, Register128(ys)), "rail 1 granted"); +} + +/// Column `k` is `Morton8x8::from_xy(R0[k], R1[k])`. +pub fn columns(lanes: &RegisterLanes, row: &NodeRow) -> [Morton8x8; COLUMNS] { + let xs = lanes.get(row, 0).expect("rail 0 granted").0; + let ys = lanes.get(row, 1).expect("rail 1 granted").0; + std::array::from_fn(|k| Morton8x8::from_xy(xs[k], ys[k])) +} + +/// Column 0: the node's own address. +pub fn identity(lanes: &RegisterLanes, row: &NodeRow) -> Morton8x8 { + columns(lanes, row)[0] +} diff --git a/crates/mistaber-kripke-probe/tests/goldens.rs b/crates/mistaber-kripke-probe/tests/goldens.rs index 1ff5cdbec..53ba5188f 100644 --- a/crates/mistaber-kripke-probe/tests/goldens.rs +++ b/crates/mistaber-kripke-probe/tests/goldens.rs @@ -36,8 +36,8 @@ fn every_golden_is_reproduced_exactly() { // Anti-vacuity: the eleven exported fixtures, not an empty directory. assert_eq!(all.len(), 11); for g in &all { - let kb = Kb::load(&g.facts).expect(&g.fixture_id); - let got = kb.solve().materialize_atoms(Projection::Set); + let (kb, names) = Kb::load(&g.facts).expect(&g.fixture_id); + let got = kb.solve().materialize_atoms(&names, Projection::Set); assert_eq!(got, sorted(g.atoms.clone()), "{}", g.fixture_id); } } @@ -62,9 +62,9 @@ fn the_goldens_are_not_trivial() { fn orientation_is_load_bearing() { let a = golden("F1-modes"); let b = golden("F1-reversed"); - let (ka, kb) = (Kb::load(&a.facts).unwrap(), Kb::load(&b.facts).unwrap()); - let sa = ka.solve().materialize_atoms(Projection::Set); - let sb = kb.solve().materialize_atoms(Projection::Set); + let ((ka, na), (kb, nb)) = (Kb::load(&a.facts).unwrap(), Kb::load(&b.facts).unwrap()); + let sa = ka.solve().materialize_atoms(&na, Projection::Set); + let sb = kb.solve().materialize_atoms(&nb, Projection::Set); assert!(sa.contains(&"holds(p,a)".to_owned())); assert!(!sb.contains(&"holds(p,a)".to_owned())); } @@ -72,9 +72,9 @@ fn orientation_is_load_bearing() { #[test] fn a_cycle_supports_nothing_and_terminates() { let g = golden("F2-cycle"); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); - let got = h.materialize_atoms(Projection::Set); + let got = h.materialize_atoms(&names, Projection::Set); let held: Vec<_> = got.iter().filter(|a| a.starts_with("holds(")).collect(); assert_eq!(held, ["holds(t,z)"]); assert!(h.steps <= 4, "{} steps", h.steps); @@ -84,18 +84,25 @@ fn a_cycle_supports_nothing_and_terminates() { fn set_projection_is_required_on_the_diamond() { // p holds in d by inherited(a) and inherited(b): two lens rows, one fact. let g = golden("F1-modes"); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); - assert_eq!(h.bag_multiplicity("p", "d"), 2); - assert_eq!(h.bag_multiplicity("p", "a"), 1); + assert_eq!(h.bag_multiplicity(&names, "p", "d"), 2); + assert_eq!(h.bag_multiplicity(&names, "p", "a"), 1); let sel = WideFieldMask::from_positions(&[0, 1]); - let set = h.materialize_selection(&sel, Projection::Set).unwrap(); - let bag = h.materialize_selection(&sel, Projection::Bag).unwrap(); + let set = h + .materialize_selection(&names, &sel, Projection::Set) + .unwrap(); + let bag = h + .materialize_selection(&names, &sel, Projection::Bag) + .unwrap(); let count = |v: &[String]| v.iter().filter(|a| *a == "holds(p,d)").count(); assert_eq!(count(&set), 1); assert_eq!(count(&bag), 2); // The bag reading does not reproduce the golden. - assert_ne!(h.materialize_atoms(Projection::Bag), sorted(g.atoms)); + assert_ne!( + h.materialize_atoms(&names, Projection::Bag), + sorted(g.atoms) + ); } #[test] @@ -103,11 +110,11 @@ fn bag_and_set_agree_where_every_holding_has_one_lens_row() { // Silence twin: one mode and one source rule per holding, so the two // projections coincide. let g = golden("C-mammal-C4"); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); assert_eq!( - h.materialize_atoms(Projection::Bag), - h.materialize_atoms(Projection::Set) + h.materialize_atoms(&names, Projection::Bag), + h.materialize_atoms(&names, Projection::Set) ); } @@ -135,12 +142,12 @@ fn a_65th_world_is_refused_not_wrapped() { #[test] fn a_selection_that_is_no_predicate_is_refused() { let g = golden("F1-modes"); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); for f in [&[0u8][..], &[0, 2], &[0, 1, 3], &[0, 1, 2, 4]] { let sel = WideFieldMask::from_positions(f); assert_eq!( - h.materialize_selection(&sel, Projection::Set), + h.materialize_selection(&names, &sel, Projection::Set), Err(Refusal::Selection), "{f:?}" ); @@ -153,12 +160,12 @@ fn bag_counts_lens_rows_not_modes() { // (r_base_p, r_b_endorse): two lens rows, one holds_via fact, one holds // fact. g holds in a with no rule at all: one lens row, empty rule fields. let g = golden("F1-modes"); - let kb = Kb::load(&g.facts).unwrap(); + let (kb, names) = Kb::load(&g.facts).unwrap(); let h = kb.solve(); - assert_eq!(h.bag_multiplicity("p", "e"), 2); - assert_eq!(h.bag_multiplicity("g", "a"), 1); + assert_eq!(h.bag_multiplicity(&names, "p", "e"), 2); + assert_eq!(h.bag_multiplicity(&names, "g", "a"), 1); let count = |sel: &[u8], proj, atom: &str| { - h.materialize_selection(&WideFieldMask::from_positions(sel), proj) + h.materialize_selection(&names, &WideFieldMask::from_positions(sel), proj) .unwrap() .iter() .filter(|a| *a == atom) @@ -173,6 +180,7 @@ fn bag_counts_lens_rows_not_modes() { assert_eq!( sorted( h.materialize_selection( + &names, &WideFieldMask::from_positions(&[0, 1, 2, 3, 4]), Projection::Set ) @@ -180,6 +188,7 @@ fn bag_counts_lens_rows_not_modes() { ), sorted( h.materialize_selection( + &names, &WideFieldMask::from_positions(&[0, 1, 2, 3, 4]), Projection::Bag ) diff --git a/crates/mistaber-kripke-probe/tests/rows.rs b/crates/mistaber-kripke-probe/tests/rows.rs new file mode 100644 index 000000000..2eb77d787 --- /dev/null +++ b/crates/mistaber-kripke-probe/tests/rows.rs @@ -0,0 +1,208 @@ +//! The HHTL16 node rows: identity and parents as addresses, classid on the +//! lanes, and the refusals that name their population. + +use std::collections::BTreeSet; +use std::fs; +use std::path::PathBuf; + +use lance_graph_contract::canonical_node::NodeRow; +use mistaber_kripke_probe::rows::{ + COLUMNS, Concepts, MAX_PARENTS, Population, UNBOUND, address, columns, identity, write_columns, +}; +use mistaber_kripke_probe::{Golden, Kb, Pop, Refusal, intake, intake_under, parse_golden}; + +fn goldens() -> Vec { + let dir = PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("goldens"); + let mut out: Vec = fs::read_dir(&dir) + .expect("goldens/") + .map(|e| e.expect("entry").path()) + .filter(|p| p.extension().is_some_and(|x| x == "tsv")) + .map(|p| parse_golden(&fs::read_to_string(p).expect("read")).expect("parse")) + .collect(); + out.sort_by(|a, b| a.fixture_id.cmp(&b.fixture_id)); + out +} + +fn fact(parts: &[&str]) -> Vec { + parts.iter().map(|s| (*s).to_owned()).collect() +} + +fn f1() -> Golden { + goldens() + .into_iter() + .find(|g| g.fixture_id == "F1-modes") + .expect("F1-modes") +} + +/// FAILS IF identity or parents are not written to the rails, are dropped or +/// extra, or x and y are swapped. +#[test] +fn rows_round_trip_identity_and_parents() { + let all = goldens(); + assert_eq!(all.len(), 11); + let mut parent_columns = 0; + for g in &all { + let (i, names) = intake(&g.facts).expect(&g.fixture_id); + for (pop, p) in [ + (Pop::World, &i.worlds), + (Pop::Proposition, &i.props), + (Pop::Rule, &i.rules), + ] { + for (o, row) in p.rows.iter().enumerate() { + let id = identity(&p.lanes, row); + assert_eq!(id, address(o as u16), "{} {pop:?} {o}", g.fixture_id); + assert_ne!(id, UNBOUND); + assert_eq!( + names.address_of(pop, names.name(pop, id)), + Some(id), + "{} {pop:?} {o}", + g.fixture_id + ); + let r0 = p.lanes.get(row, 0).expect("rail 0"); + let r1 = p.lanes.get(row, 1).expect("rail 1"); + assert_eq!(p.lanes.get(row, 2), None); + let cols = columns(&p.lanes, row); + assert_eq!(cols.len(), COLUMNS); + for (k, c) in cols.iter().enumerate() { + assert_eq!(r0.0[k], c.x(), "{} {pop:?} {o} x{k}", g.fixture_id); + assert_eq!(r1.0[k], c.y(), "{} {pop:?} {o} y{k}", g.fixture_id); + } + let held: BTreeSet = cols[1..] + .iter() + .filter(|a| **a != UNBOUND) + .map(|a| a.code()) + .collect(); + let want: BTreeSet = if pop == Pop::World { + let me = names.name(Pop::World, id); + g.facts + .iter() + .filter(|f| f[0] == "accessible" && f[1] == me) + .map(|f| names.address_of(Pop::World, &f[2]).expect("parent").code()) + .collect() + } else { + BTreeSet::new() + }; + assert_eq!(held, want, "{} {pop:?} {o}", g.fixture_id); + // The unbound tail is contiguous: nothing past the parents. + let bound = cols[1..].iter().filter(|a| **a != UNBOUND).count(); + assert_eq!(bound, want.len()); + assert!(cols[1 + bound..].iter().all(|a| *a == UNBOUND)); + parent_columns += held.len(); + } + } + } + // Anti-vacuity: some world really has parents. + assert!(parent_columns > 0); +} + +fn parent_fixture(parents: usize) -> Vec> { + let mut facts = vec![fact(&["world", "c"])]; + for i in 0..parents { + let w = format!("w{i}"); + facts.push(fact(&["world", &w])); + facts.push(fact(&["accessible", "c", &w])); + facts.push(fact(&["asserts", &w, "p"])); + } + facts +} + +/// FAILS IF a 16th parent is truncated instead of refused, or if 15 are not +/// all carried. +#[test] +fn a_16th_parent_is_refused() { + assert_eq!(MAX_PARENTS, 15); + let (kb, names) = Kb::load(&parent_fixture(15)).expect("15 parents fit"); + let atoms = kb + .solve() + .materialize_atoms(&names, mistaber_kripke_probe::Projection::Set); + let via = atoms + .iter() + .filter(|a| a.starts_with("holds_via(inherited(") && a.ends_with(",p,c)")) + .count(); + assert_eq!(via, 15); + assert_eq!( + Kb::load(&parent_fixture(16)).err(), + Some(Refusal::TooManyParents { parents: 16 }) + ); +} + +/// FAILS IF a classid reaches the key, the edges or the rails, or the lanes +/// do not carry the concept they were resolved under. +#[test] +fn the_classid_lives_on_the_lanes_not_in_the_rows() { + let other = Concepts { + world: 0x7F21, + proposition: 0x7F22, + rule: 0x7F23, + }; + let g = f1(); + let (a, _) = intake_under(&g.facts, Concepts::LAB).unwrap(); + let (b, _) = intake_under(&g.facts, other).unwrap(); + let pops = |i: &mistaber_kripke_probe::Intake| { + [i.worlds.rows.len(), i.props.rows.len(), i.rules.rows.len()] + }; + assert_eq!(pops(&a), pops(&b)); + let pairs: [(&Population, &Population, u16, u16); 3] = [ + (&a.worlds, &b.worlds, Concepts::LAB.world, other.world), + ( + &a.props, + &b.props, + Concepts::LAB.proposition, + other.proposition, + ), + (&a.rules, &b.rules, Concepts::LAB.rule, other.rule), + ]; + for (pa, pb, ca, cb) in pairs { + assert_eq!(pa.lanes.concept(), ca); + assert_eq!(pb.lanes.concept(), cb); + assert_ne!(ca, cb); + assert!(!pa.rows.is_empty()); + let r0 = pa.lanes.rail_range(0).unwrap(); + let r1 = pa.lanes.rail_range(1).unwrap(); + for (ra, rb) in pa.rows.iter().zip(&pb.rows) { + assert_eq!(ra.key.as_bytes(), rb.key.as_bytes()); + assert_eq!(ra.edges.as_bytes(), rb.edges.as_bytes()); + assert_eq!(ra.value, rb.value); + assert_eq!(ra.key.as_bytes(), &[0u8; 16]); + assert_eq!(ra.edges.as_bytes(), &[0u8; 16]); + for (at, byte) in ra.value.iter().enumerate() { + if !r0.contains(&at) && !r1.contains(&at) { + assert_eq!(*byte, 0, "value byte {at}"); + } + } + } + } + for (c, name) in [(Concepts::LAB, "lab"), (other, "other")] { + let (i, names) = intake_under(&g.facts, c).unwrap(); + let kb = Kb::assemble(i).expect(name); + let got = kb + .solve() + .materialize_atoms(&names, mistaber_kripke_probe::Projection::Set); + let mut want = g.atoms.clone(); + want.sort(); + assert_eq!(got, want, "{name}"); + } +} + +/// FAILS IF the 64 limit is enforced anywhere but the local map, or a +/// duplicate or an unknown address is not named by its population. +#[test] +fn local_map_refusals_name_their_population() { + let facts: Vec> = (0..65) + .map(|i| fact(&["world", &format!("w{i}")])) + .collect(); + let (i, _) = intake(&facts).expect("intake does not enforce 64"); + assert_eq!(i.worlds.rows.len(), 65); + assert_eq!(Kb::assemble(i).err(), Some(Refusal::TooMany("world"))); + + let g = f1(); + let (mut i, _) = intake(&g.facts).unwrap(); + let again: NodeRow = i.worlds.rows[0]; + i.worlds.rows.push(again); + assert_eq!(Kb::assemble(i).err(), Some(Refusal::Duplicate("world"))); + + let (mut i, _) = intake(&g.facts).unwrap(); + let lanes = i.worlds.lanes; + write_columns(&lanes, &mut i.worlds.rows[0], &[address(0), address(200)]); + assert_eq!(Kb::assemble(i).err(), Some(Refusal::Unmapped("world"))); +}