From 06f9c4bfc7a5ce660f966debc296cc524420fdad Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 3 Nov 2026 18:16:32 +0000 Subject: [PATCH] D-COGNITIVE-POLYFILL P0: four frontends over one native algebra (lab) Lab probe crates/cognitive-polyfill-probe (own workspace, excluded from the root workspace) plus a source-backed crosswalk of MORK, MeTTa, Narsese and Atomese against the existing DR / Quack / xlog / NAL / mask-risc stack. - The ground, bounded, conjunctive subset common to all four runs as one mask-risc program (out[a] AND inn[c] AND W) over borrowed rows of a DR W64 tile: 12/12 tests, 125 cases agree with an independent oracle, 0 bytes allocated on the hot path, 6 source disables red. - Routing a selection by global id is required; a raw local join is wrong. - Set and Bag diverge (2 vs 3); the existing Bag route is lance_graph_xlog::bag_count (EXO-108 / MISSING-3). - A NAL belief is not an edge without a projection policy. - First break per language: MeTTa D-MTP-1 refuses non-functional relations and Hyperon's BindingsSet is a multiset; MORK builds its own JoinDomain; Narsese needs the product compound (R10); no Classic AtomSpace source. No production change, no parser, no admission. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMLBmi7EtDd15CGwGb8 --- .../2026-11-03-d-cognitive-polyfill-p0.md | 28 ++ .claude/board/entries/README.md | 3 +- .../2026-11-03-d-cognitive-polyfill/REPORT.md | 207 ++++++++ Cargo.toml | 3 + crates/cognitive-polyfill-probe/Cargo.toml | 20 + crates/cognitive-polyfill-probe/src/lib.rs | 432 +++++++++++++++++ crates/cognitive-polyfill-probe/tests/p0.rs | 446 ++++++++++++++++++ 7 files changed, 1138 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-11-03-d-cognitive-polyfill-p0.md create mode 100644 .claude/probes/2026-11-03-d-cognitive-polyfill/REPORT.md create mode 100644 crates/cognitive-polyfill-probe/Cargo.toml create mode 100644 crates/cognitive-polyfill-probe/src/lib.rs create mode 100644 crates/cognitive-polyfill-probe/tests/p0.rs diff --git a/.claude/board/entries/2026-11-03-d-cognitive-polyfill-p0.md b/.claude/board/entries/2026-11-03-d-cognitive-polyfill-p0.md new file mode 100644 index 000000000..fd2d49255 --- /dev/null +++ b/.claude/board/entries/2026-11-03-d-cognitive-polyfill-p0.md @@ -0,0 +1,28 @@ +# D-COGNITIVE-POLYFILL P0: four frontends, one native algebra (2026-11-03) + +**Status:** measured, lab only. Probe `crates/cognitive-polyfill-probe` (own workspace); report `.claude/probes/2026-11-03-d-cognitive-polyfill/REPORT.md`. No production change. + +## Measured + +- The relational subset common to MORK, MeTTa, Narsese and Atomese is a ground, bounded, conjunctive one. A scoped two-hop EXISTS/COUNT over it runs as ONE mask-risc program over borrowed rows of a DR W64 tile. Results: + - 12/12 tests; 125 cases agree with an independent oracle; + - 0 bytes allocated per hot run; + - 6 source disables red, each with its anchor asserted. +- Routing a selection by global id is required: joining on raw local positions gives the wrong answer (c04). +- The Set fold cannot answer the Bag question (2 vs 3, c08). The existing Bag route is `lance_graph_xlog::bag_count` (TRACKED MISSING-3, EXO-108). +- Existence of a NAL belief is not an edge. Existence projection and truth projection disagree on the same beliefs (c09). + +## Where each language leaves the subset + +- MeTTa: + - D-MTP-1 covers functional relations only and refuses the fixture with `SecondFact`. + - `BindingsSet` is a multiset (hyperon `matcher.rs:883`). +- MORK: the space is a Set (`set_val`, `space.rs:1561`). D-MPS-8 builds its own `JoinDomain`, beside DR. +- Narsese: cannot spell a binary relation without the product compound (R10). +- Atomese: no Classic AtomSpace source within reach. + +## Open (owner) + +- **W-1:** one cold symbol → DR id step for MeTTa/MORK. Today xlog takes pre-localized `u32`, MORK builds its own `JoinDomain`, and NAL uses `u16` terms. +- **W-2:** `Guards::check` needs a `FrameStore`, but `MapTable` keeps its store private. +- EXO-46, EXO-108, R10, the NAL → edge projection policy. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index e75c83f56..a23d95764 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. -562 entries, 2026-08-06 .. 2026-11-03. +563 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-COGNITIVE-POLYFILL` | | [2026-11-03-d-cognitive-polyfill-p0.md](2026-11-03-d-cognitive-polyfill-p0.md) | | 2026-11-03 | `D-BAG-FOLD` | | [2026-11-03-d-bag-fold-witnessed-existential.md](2026-11-03-d-bag-fold-witnessed-existential.md) | | 2026-11-03 | `D-BAG-FOLD-V4` | | [2026-11-03-d-bag-fold-v4-attested-lens-gated-exec.md](2026-11-03-d-bag-fold-v4-attested-lens-gated-exec.md) | | 2026-11-03 | `D-BAG-FOLD-V3` | | [2026-11-03-d-bag-fold-v3-production-witnesses.md](2026-11-03-d-bag-fold-v3-production-witnesses.md) | diff --git a/.claude/probes/2026-11-03-d-cognitive-polyfill/REPORT.md b/.claude/probes/2026-11-03-d-cognitive-polyfill/REPORT.md new file mode 100644 index 000000000..ea0f81392 --- /dev/null +++ b/.claude/probes/2026-11-03-d-cognitive-polyfill/REPORT.md @@ -0,0 +1,207 @@ +# D-COGNITIVE-POLYFILL P0 — four frontends, one native algebra + +**Date:** 2026-11-03. **Status:** LAB PROBE + SOURCE AUDIT. Nothing here changes +a production crate, ships a parser or admits a path. The probe is +`crates/cognitive-polyfill-probe` (own workspace, excluded from the main one). + +**Question:** how much of MORK, MeTTa, Narsese and Atomese can lower through the +existing DR / Quack / RelAlg / R2IL / mask-risc / ndarray stack, and where does +each one first need something that stack does not have? + +**Short answer:** +- Only the **ground, bounded, conjunctive relational subset** is common to all + four. It already lowers today: + - `lance-graph-xlog::support` / `bag_count` answer the chain shape + `q(Y) :- r(X,Y), s(Y,Z)`; + - this probe answers the scoped EXISTS/COUNT form in one mask-risc program. +- What each language adds beyond that subset is different semantics, not a + different engine: + - MeTTa: binding multisets and evaluation; + - Narsese: compound terms and truth laws; + - Atomese: typed nested links and Values; + - MORK: rewriting into a Set space. +- The first missing piece is the same for MeTTa and MORK: the cold step that + turns symbols into DR global ids and back. It has no home. + +--- + +## A. Reuse map (verified in source) + +| Native capability | Where | Serves | +|---|---|---| +| DR identity: `LocalMap` global↔local, `MapTable` frames, `locate` | `lance-graph-dt64/src/dr.rs:556`, `:805`, `:955` | all four (term ids) | +| Chain support + Bag count over a DR Y map | `lance-graph-xlog/src/lib.rs:255` (`support`), `:280` (`bag_count`) | MeTTa/MORK/Atomese 2-atom chains, XLOG | +| Co-addressed presence AND (leapfrog's first level), bag-count fold | `mork-pathmap-probe/src/join.rs:1-45`, `:512` (`joint`) | MORK-shaped conjunctive bodies (lab, not admitted) | +| Two-hop functional join via Quack `Semijoin` + datafrog oracle | `lance-graph-metta/examples/join_probe.rs` (D-MTP-1) | MeTTa, **functional relations only** | +| α-acyclic vs cyclic body test (GYO) | `lance-graph-relalg/src/join_body.rs:21` | routing any conjunctive body | +| Sealed-order apertures, Question / TruthAtLeast / Choice / Revision as prepared programs | `lance-graph-nal/src/lib.rs`, `src/nal.rs:159-387` | Narsese atomic statements | +| ONNX ALIAS/INLINE over native functions | `lance-graph-onnx/src/lib.rs:1-25` | ONNX numerics only; no symbolic semantics | +| Tract harvest → DR³ + operator registry (lab) | `tract-harvest-probe` (plan status: LAB PROBE IMPLEMENTED) | ONNX graphs; TFLite is PROPOSAL only (`d-tflp-…-capstone-v1/v2`) | + +Re-run on this checkout (`origin/main` `ebbdb27`): +- `lance-graph-nal`: 19 passed; +- `lance-graph-metta`: 13 passed; +- `mork-pathmap-probe`: 47 passed (MORK/PathMap as oracles). + +## B. Semantic compatibility matrix + +Codes: CON = existing and connected · UNW = existing but unwired · LAB = lab only · +NAT = native composition possible · NEW = a new semantic contract is required · +OWN = owner decision · UP = upstream only · REF = refuse · NV = not verified. + +| Capability | MORK | MeTTa | Narsese | Atomese | Native substrate | +|---|---|---|---|---|---| +| Identity / symbol binding | NEW: symbol → DR id step (`Tag` byte encoding, MORK `expr/src/lib.rs:91`) | NEW: same (D-MTP-2) | LAB: `u16` term addresses in `guid()`, `nal/src/lib.rs:157`; not DR ids | NEW | DR `LocalMap`: CON | +| Atomic ground facts | UP | UP (`SpaceMut::add`, hyperon-space `lib.rs:237`) | LAB (`Beliefs::seal`) | NV (no AtomSpace source in reach) | CON | +| Typed relations | UP | UP (untyped by default) | copula enum only | NEW | ClassView: CON; per-relation class check: LAB (this probe) | +| WHERE / selection | NAT | NAT | LAB (aperture = sealed key prefix) | NAT | Quack `Keep`: CON; cross-frame routing: LAB (this probe, #1943) | +| Shared-variable join (2 atoms) | LAB (D-MPS-8) | LAB (D-MTP-1, functional only) | REF: needs `(*,A,B)` compound | NAT | xlog `support`: CON | +| Repeated-variable equality `R($x,$x)` | UP | UP (`match_atoms`, matcher.rs:1050) | n/a | UP | NAT (diagonal), not built | +| Set semantics | UP (space is `PathMap<()>`, `set_val`, space.rs:1561) | — | — | NV | `Count`/`Any`: CON | +| Bag / multiple bindings | — | UP: `BindingsSet` is a `SmallVec` multiset (matcher.rs:883), GroundingSpace `ALLOW_DUPLICATION`; PeTTa backtracks (bag) | — | NV | xlog `bag_count` + TRACKED `checked_binary_i64` (EXO-108 / MISSING-3) | +| Ordered nested terms | UP | UP | REF in crate (R10) | NEW | REF | +| Hyperedges targeting edges | UP | UP | — | NEW | NEW | +| Structural unification | UP | UP (loops filtered after the match, no occurs check, matcher.rs:1084) | — | UP | REF (P2) | +| Substitution / construction | UP | UP | — | UP | NEW (it creates structure) | +| Nondeterministic evaluation | UP | UP | — | — | REF (no second interpreter) | +| Rewrite rules | UP (`exec`, space.rs:1902) | UP | — | — | PARK | +| Recursive closure | UP (`metta_calculus`) | UP | — | UP | OWN (EXO-73); relalg `μ` not built (`relalg/src/lib.rs:28`) | +| Frequency / confidence | — | — | LAB (`Beliefs` f, c lanes) | NV (TruthValue) | the I32 lanes exist | +| Evidence provenance / revision | — | — | LAB (W3: 4 evidence classes, `Revision`) | — | grouped fold: CON | +| Temporal inference | — | — | NEW | — | NV | +| Type / guard admission | — | UP (type checker) | global, no class check (by design) | NEW | dt64 `Guards`: CON; see W-2 | +| Mutations / frames | UP | UP | `seal` only | UP | `MapTable::advance`: CON | +| Native terminal result | — | — | `Count`, `Max`, revision | — | `Any`/`Count`/`Keep`/`MaskedSum`: CON | + +**What is not common** (this keeps the matrix from reading as "all four are +equivalent"): +- **Narsese cannot spell the common test at all.** A binary relation needs + the product compound `<(*, A, B) --> R>`, which the NAL crate refuses as + ledger R10 (`nal/src/lib.rs:91`). `B>, C> ⊢ C>` is deduction: + it carries a truth value, so it is not an existence test. +- **Classic Atomese is not reachable in source here.** No OpenCog AtomSpace + code exists in the four upstream repos. The only Atomese-shaped text is + MeTTa-encoded: `hyperon-experimental/python/tests/scripts/a2_opencoggy.metta:8-12`. + +## C. P0 falsifier — results + +**Fixture:** +- facts `R(A,B) R(B,C) R(C,D) R(A,E)`, with one DR W64 tile `[A,B,C,D,E]`; +- MeTTa `(, (R A $y) (R $y C))`, MORK `(exec P (, (R A $y) (R $y C)) …)` and + the Atomese projection all hand-lower to one `Pattern`; +- native arm: `Any`/`Count`/`Keep` over `out[a] ∧ inn[c] ∧ W`, one mask-risc + program over borrowed rows. + +**Oracle:** an independent nested loop over the borrowed fact slice. + +**Result: 12/12 tests green** (`cargo test --manifest-path +crates/cognitive-polyfill-probe/Cargo.toml`). clippy `-D warnings` and fmt are +clean. + +| # | check | result | +|---|---|---| +| 1 | 125 cases (5×5 pairs × 5 WHERE subsets), `Any` and `Count` vs oracle | agree; both answers present | +| 2 | delete `R(B,C)` | A→?→C flips to false | +| 3 | delete `R(C,D)` | A→?→C and A→?→D unchanged; control B→?→D flips | +| 4 | B at local 2 in S1 and local 0 in S2; relation tile has B at 1 | both route to bit 1, answer true; **raw local join gives false** (bit 2 is C there); an unheld id reported as `dropped` | +| 5 | DR round trip `global(local(g)) == g` | holds; an unmapped id is refused | +| 6 | foreign frame on ingest, prepare, route | `Stale` each; control routes | +| 7 | wrong relation; scope via dt64 `Guards` | `WrongRelation`; `ScopeChanged` | +| 8 | `R(A,B)`×2, `R(B,C)`, `R(A,E)`, `R(E,C)` | Set 2, Bag 3: the Set fold cannot answer Bag | +| 9 | NAL beliefs ` f=1`, ` f=0 c=0.9` | existence projection says A→?→C true, truth projection false; a confidence-only revision moves no edge | +| 10 | free endpoint, `R($x,$x)`, nested / Narsese product, two relations, one atom | each refused with its own reason | +| 11 | program without `inn[c]` | A→?→D: false becomes true | +| 12 | 1000 hot runs | 0 bytes allocated (per-thread counter) | +| 13 | no copied upstream index | structural: planes are `&relation.out[i..i+1]` / `&relation.inn[..]`; `inn` is a derived index built at ingest (cost noted) | +| 14 | no second evaluator | structural: `execute_into` is the only evaluator called | + +**Source disable runs.** Each anchor was asserted present before patching, and +each patch was reverted: + +| disable | result | +|---|---| +| join operand | 6 tests red | +| selection routing | c04 red | +| repeated-variable refusal | c10 red | +| Bag multiplicity | c08 red | +| WHERE operand | c01, c04 red | +| frame check in `prepare` | c06 red | + +**First failure per language (where the common subset ends):** +- **MeTTa:** + - D-MTP-1's `Relation2::ingest` refuses this fixture with + `SecondFact { subject: A }` (`join_probe.rs:61`): the D-MTP-1 path covers + functional relations only. + - The general route is `xlog::support`, which takes `&[(u32,u32)]` tuples + and already-local ids. + - Missing: the Space adapter that maps `Space::query`'s `BindingsSet` + multiset onto a Set/Bag choice (D-MTP-2). +- **MORK:** the symbol → DR id step. D-MPS-8's `JoinTable` builds its own + value-sorted `JoinDomain`; that is a second identity space beside DR, which + D-RMAP-1 already flags as unadmitted. +- **Narsese:** the product compound term (R10). Atomic inheritance questions + already run natively. +- **Atomese:** no source to verify against; only a typed-projection proposal + is possible. + +## D. Findings that need an owner + +- **W-1 (wire): one term-resolution step for symbol frontends.** MeTTa and MORK + symbols need a cold, once-per-frame map `symbol → DR global → local`, with + the inverse for binding emission. + - Today this is done three different ways: xlog takes pre-localized + `u32`; D-MPS-8 builds its own `JoinDomain`; NAL uses `u16` terms. + - Owner: the DR contract (EXO-46) and the GPT-07 proposal (OGAR owns the + codebook). +- **W-2 (small gap): `Guards::check` needs a `FrameStore`, but `MapTable`'s + store is private** (`dr.rs:806`). A frame sealed from a `MapTable` therefore + cannot be guard-checked for Scope against its own store. The probe checks + scope on a separate store (c07). +- **W-3: routing a selection across frames is per frame, not per query.** This + is the D-GLOBAL-WHERE finding (#1943); c04 re-confirms it from the + frontend side. +- **Set vs Bag must be declared per frontend, not inferred:** + - MORK's space is a Set; + - Hyperon's default space and PeTTa's `match` are Bags; + - NAL evidence is neither: it is weighted, with its own duplicate rule. + - EXO-108 owns the Bag product. +- **NAL → relation projection is an owner decision** (c09). Existence of a + belief is not an edge; any threshold is policy. + +## E. Minimal roadmap (ranked) + +1. **WIRE, low risk.** Bind the MeTTa/MORK 2-atom chain to the existing + `lance_graph_xlog::support` / `bag_count`, after a cold symbol→DR step + (W-1). Owner: DR + D-MTP-2. + - Falsifier: c01–c08 rerun against xlog instead of this probe's program, + plus Hyperon's golden corpus. +2. **PROBE.** The D-MTP-2 `LanceSpace`, read-only and non-recursive: does + `Space::query` receive whole conjunctions (`complex_query`, + hyperon-space `lib.rs:340`) or single conjuncts? Report the multiset vs + Set choice. +3. **PROBE (P2).** Bounded structural matching (`f(X, g(X))`): can a cold + matcher lower its surviving constraints to DR relations? No native + unification without an owner decision. +4. **OWNER DECISION.** Narsese compound terms (R10), and the NAL → edge + projection policy. +5. **PARK.** + - recursion (EXO-73); + - rewriting / `exec`; + - nondeterministic evaluation; + - Classic AtomSpace; + - TFLite (PROPOSAL only). + +**Verdicts:** +- **REUSE NOW:** DR `LocalMap`/`MapTable`; xlog `support`/`bag_count`; Quack + `Any`/`Count`/`Keep`; relalg `is_alpha_acyclic`; NAL Question/Choice/Revision; + ONNX aliases. +- **WIRE:** symbol → DR term resolution (W-1); MeTTa/MORK chain → xlog. +- **PROBE:** `LanceSpace` multiset boundary; bounded structural matching. +- **OWNER DECISION:** EXO-46 selection sharing; EXO-108 Bag product; R10 + compounds; NAL projection; W-2. +- **PARK:** recursion, rewrite, evaluation, AtomSpace, TFLite runtime. +- **SKIP:** + - a second term store; + - a copied AtomSpace; + - a new interpreter; + - a mask-risc opcode for AND/OR/COUNT, which already exist. diff --git a/Cargo.toml b/Cargo.toml index b1e281752..668599923 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -138,6 +138,9 @@ exclude = [ # D-MTP-1: its own workspace root (datafrog oracle is a git dev-dependency). # `cargo test --manifest-path crates/lance-graph-metta/Cargo.toml`. "crates/lance-graph-metta", + # D-COGNITIVE-POLYFILL P0 lab probe; own workspace root. + # `cargo test --manifest-path crates/cognitive-polyfill-probe/Cargo.toml`. + "crates/cognitive-polyfill-probe", "crates/symbiont", # OGAR (Open Graph of Active Record) activation crate — re-exports OGAR's full # AR surface (ogar-vocab Class/codebook + ogar-class-view impl ClassView + diff --git a/crates/cognitive-polyfill-probe/Cargo.toml b/crates/cognitive-polyfill-probe/Cargo.toml new file mode 100644 index 000000000..aa6142365 --- /dev/null +++ b/crates/cognitive-polyfill-probe/Cargo.toml @@ -0,0 +1,20 @@ +[package] +name = "cognitive-polyfill-probe" +version = "0.0.0" +edition = "2021" +publish = false +description = "D-COGNITIVE-POLYFILL P0 lab falsifier: the relational subset common to MORK, MeTTa, Narsese and Atomese (a scoped two-hop existential over ground facts) run through existing DR addressing (lance-graph-dt64) and one mask-risc program. Lab only; nothing here is wired into Quack, R2IL or production." + +# Its OWN workspace root, like lance-graph-nal / lance-graph-metta. Verify via +# cargo test --manifest-path crates/cognitive-polyfill-probe/Cargo.toml +[workspace] + +[dependencies] +# DR identity: LocalMap (global <-> local), MapTable frames, Guards/Scope. +lance-graph-dt64 = { path = "../lance-graph-dt64" } +# The only bulk engine. +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } + +# One ndarray package identity: point mask-risc's git coordinate at the sibling. +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "../../../ndarray" } diff --git a/crates/cognitive-polyfill-probe/src/lib.rs b/crates/cognitive-polyfill-probe/src/lib.rs new file mode 100644 index 000000000..6a44f316b --- /dev/null +++ b/crates/cognitive-polyfill-probe/src/lib.rs @@ -0,0 +1,432 @@ +//! D-COGNITIVE-POLYFILL P0 — four frontends, one native algebra (LAB ONLY). +//! +//! STATUS: PROBE. Nothing here is wired into Quack, R2IL, RelAlg or any +//! production path, and nothing here parses a language. Each frontend's query +//! is hand-lowered into one [`Pattern`], the way D-MTP-1 +//! (`lance-graph-metta/examples/join_probe.rs`) hand-lowers its MeTTa query. +//! +//! # The common subproblem +//! +//! Ground facts of one binary relation `R`, and the bounded existential +//! "is there a `y` in the selection `W` with `R(a, y)` and `R(y, c)`": +//! +//! | frontend | spelling of the same subproblem | +//! |---|---| +//! | MeTTa (Hyperon) | `(match &self (, (R A $y) (R $y C)) $y)` | +//! | MORK | `(exec P (, (R A $y) (R $y C)) (, (hit $y)))` | +//! | Atomese (typed projection) | `(EvaluationLink (PredicateNode "R") (ListLink A $y))` ∧ `(… (ListLink $y C))` | +//! | Narsese | NO direct spelling: a relation `R(A, B)` needs the product term `<(*, A, B) --> R>`, a compound term the NAL crate refuses (ledger R10); ` ?x>` is one statement, and `B>, C> ⊢ C>` is an INFERENCE with a truth value, not an existence test. | +//! +//! These are equivalent only on this subset. The probe does not claim language +//! equivalence; it measures where each frontend first needs something the +//! substrate does not have. +//! +//! # Native arm +//! +//! - Identity: one DR tile ([`lance_graph_dt64::dr::LocalMap`], `Width::W64`) +//! under a [`MapTable`] frame. Every term is a `u64` global id; its column in +//! the planes is its local position in that tile. +//! - Relation: per source a presence word over targets (`out`), and per target +//! a presence word over sources (`inn`), both laid out by the same tile's +//! local positions. `inn` is a derived index built once at ingest (the +//! co-addressed second side, the same shape as `mork-pathmap-probe::join::Side`); +//! it is not a second authority and is rebuilt with `out`. +//! - Query: `Any` / `Count` over `out[a] ∧ inn[c] ∧ W` — ONE mask-risc program, +//! prepared once, run over borrowed slices of the relation's own storage. No +//! triple, no pair, no `(x, y, z)` row is formed. +//! - Selection routing: a selection from another tile is routed into the +//! relation tile ONCE per frame pair ([`Selection::route`]); joining on raw +//! local positions is a different (wrong) answer. +//! +//! # What does not lower +//! +//! [`lower`] refuses every pattern outside the subset with a reason: repeated +//! variables, free endpoints (binding enumeration), nested terms, a second +//! relation name. Bag multiplicity is answered by a lab fold over the kept +//! mask ([`Relation::bag_derivations`]); the existing native route for it is +//! `lance_graph_xlog::bag_count` (EXO-108 / MISSING-3), see that method. + +#![forbid(unsafe_code)] + +use lance_graph_dt64::dr::{Frame, LocalMap, MapRead, MapRefusal, MapTable, TileId, Width}; +use lance_graph_mask_risc::{ + execute_into, words_for, Foreign, MaskOp, Operand, Out, Planes, Program, Scratch, Terminal, + Value, +}; + +/// The one tile every probe relation lives in. +pub const TILE: TileId = 0; +/// Tile width: 64 positions, so one presence row is one `u64` word. +pub const WIDTH: Width = Width::W64; + +// --------------------------------------------------------------------------- +// Frontend descriptor +// --------------------------------------------------------------------------- + +/// One argument of an atom. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Term { + /// A ground identity (already resolved to its global id). + Ground(u64), + /// A variable, numbered by the frontend. + Var(u8), + /// A nested term `f(args…)` — structural, never a relation lookup. + Nested { functor: u64, args: Vec }, +} + +/// `rel(args…)`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Atom { + pub rel: u64, + pub args: Vec, +} + +/// A conjunctive query: every atom must hold; `answer` names the variable +/// reported (it is only ever existentially counted here). +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Pattern { + pub atoms: Vec, +} + +/// The one shape this probe lowers: `R(a, $y) ∧ R($y, c)`, `$y ∈ W`. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Hop2 { + pub rel: u64, + pub src: u64, + pub dst: u64, +} + +/// Why a pattern was not lowered. Every refusal is a semantic boundary the +/// report names; none is approximated. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Refusal { + /// Not exactly two binary atoms. + Arity, + /// The two atoms name different relations (a cross-relation join is + /// lowerable in principle, but not by this probe). + TwoRelations, + /// A nested term: structural unification, not relational lookup (P2). + NestedTerm, + /// The same variable twice in one atom (`R($x, $x)`): diagonal equality. + RepeatedVariable, + /// An endpoint is a variable: the answer is a binding enumeration, not an + /// existence fold. + FreeEndpoint, + /// The atoms do not share their middle variable in the `R(a,$y) R($y,c)` + /// order. + NotAChain, +} + +/// Lower a pattern into the one shape the native arm runs, or refuse. +pub fn lower(p: &Pattern) -> Result { + for atom in &p.atoms { + for t in &atom.args { + if matches!(t, Term::Nested { .. }) { + return Err(Refusal::NestedTerm); + } + } + if let [Term::Var(a), Term::Var(b)] = atom.args.as_slice() { + if a == b { + return Err(Refusal::RepeatedVariable); + } + } + } + let [first, second] = p.atoms.as_slice() else { + return Err(Refusal::Arity); + }; + if first.args.len() != 2 || second.args.len() != 2 { + return Err(Refusal::Arity); + } + if first.rel != second.rel { + return Err(Refusal::TwoRelations); + } + match (&first.args[..], &second.args[..]) { + ([Term::Ground(src), Term::Var(y1)], [Term::Var(y2), Term::Ground(dst)]) if y1 == y2 => { + Ok(Hop2 { + rel: first.rel, + src: *src, + dst: *dst, + }) + } + ([Term::Var(_), _], _) | (_, [_, Term::Var(_)]) => Err(Refusal::FreeEndpoint), + _ => Err(Refusal::NotAChain), + } +} + +// --------------------------------------------------------------------------- +// Relation over one DR tile +// --------------------------------------------------------------------------- + +/// Why the native arm refused to answer. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum NativeRefusal { + /// A term has no local position in the relation tile. + Map(MapRefusal), + /// The tile could not be read under the frame (foreign frame, no tile). + Read(MapRead), + /// The query names another relation than the one bound. + WrongRelation { bound: u64, asked: u64 }, + /// The selection frame does not belong to the selection table. + SelectionRead(MapRead), +} + +/// One binary relation, laid out over the local positions of one DR tile. +pub struct Relation { + rel: u64, + /// `out[local(s)]`: bit `local(t)` set when `R(s, t)`. + out: Vec, + /// `inn[local(t)]`: bit `local(s)` set when `R(s, t)` (derived index). + inn: Vec, + /// Derivation count of each fact, `mult[local(s) * 64 + local(t)]`. + /// Only the Bag fold reads it. + mult: Vec, +} + +impl Relation { + /// Ingest ground facts under `frame` of `table`. Duplicate facts collapse + /// in `out`/`inn` (Set) and are counted in `mult` (Bag). + pub fn ingest( + rel: u64, + table: &MapTable, + frame: &Frame, + facts: &[(u64, u64)], + ) -> Result { + let map = table.map(frame, TILE).map_err(NativeRefusal::Read)?; + let n = WIDTH.positions(); + let mut out = vec![0u64; n]; + let mut inn = vec![0u64; n]; + let mut mult = vec![0u32; n * n]; + for &(s, t) in facts { + let ls = usize::from(map.local(s).map_err(NativeRefusal::Map)?); + let lt = usize::from(map.local(t).map_err(NativeRefusal::Map)?); + out[ls] |= 1 << lt; + inn[lt] |= 1 << ls; + mult[ls * n + lt] += 1; + } + Ok(Self { + rel, + out, + inn, + mult, + }) + } + + /// The relation's own `out` row of `local` — borrowed, never copied. + pub fn out_row(&self, local: u8) -> &[u64] { + let i = usize::from(local); + &self.out[i..i + 1] + } + + /// The relation's own `inn` row of `local` — borrowed, never copied. + pub fn inn_row(&self, local: u8) -> &[u64] { + let i = usize::from(local); + &self.inn[i..i + 1] + } + + /// Bag answer: Σ over kept witnesses `y` of `mult(a,y) · mult(y,c)`. + /// + /// LAB FOLD, not a mask-risc terminal: mask-risc folds one lane under a + /// mask (`MaskedSumI32`) but has no product of two lanes. The existing + /// native route for the same Bag answer is `lance_graph_xlog::bag_count` + /// (two `GroupReduce` degree sinks, then the TRACKED + /// `checked_binary_i64(Mul)`, `d-dynbag-holographic-bags-v1.md` §17.5 + /// MISSING-3); EXO-108 owns closing it. This fold only checks that the Set + /// fold cannot answer the Bag question. + pub fn bag_derivations(&self, src: u8, dst: u8, kept: u64) -> u64 { + let n = WIDTH.positions(); + let (a, c) = (usize::from(src), usize::from(dst)); + let mut total = 0u64; + let mut bits = kept; + while bits != 0 { + let y = bits.trailing_zeros() as usize; + bits &= bits - 1; + total += u64::from(self.mult[a * n + y]) * u64::from(self.mult[y * n + c]); + } + total + } +} + +// --------------------------------------------------------------------------- +// Selection (virtual WHERE) and its DR routing +// --------------------------------------------------------------------------- + +/// A WHERE selection held in ITS OWN tile's local positions (another frame, +/// another order). +pub struct Selection { + pub mask: u64, +} + +impl Selection { + /// Route this selection into the relation tile: once per frame pair, by + /// global identity. A global the relation tile does not hold is dropped + /// (it cannot be a witness there) and reported. + pub fn route( + &self, + sel_table: &MapTable, + sel_frame: &Frame, + rel_table: &MapTable, + rel_frame: &Frame, + ) -> Result { + let from = sel_table + .map(sel_frame, TILE) + .map_err(NativeRefusal::SelectionRead)?; + let to = rel_table + .map(rel_frame, TILE) + .map_err(NativeRefusal::Read)?; + let mut mask = 0u64; + let mut dropped = 0u32; + let mut bits = self.mask; + while bits != 0 { + let local = bits.trailing_zeros() as u8; + bits &= bits - 1; + let Some(global) = from.global(local) else { + continue; + }; + match to.local(global) { + Ok(l) => mask |= 1 << l, + Err(_) => dropped += 1, + } + } + Ok(Routed { mask, dropped }) + } +} + +/// A selection in the relation tile's coordinates. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Routed { + pub mask: u64, + /// Selected identities the relation tile does not hold. + pub dropped: u32, +} + +// --------------------------------------------------------------------------- +// The prepared native query +// --------------------------------------------------------------------------- + +/// Which fold the program ends in. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Fold { + /// EXISTS. + Any, + /// Distinct witnesses (Set). + Count, + /// The witness mask itself, for the Bag fold. + Keep, +} + +/// `out[a] ∧ inn[c] ∧ W` — one program, compiled once. +pub struct Prepared { + pub hop: Hop2, + pub src: u8, + pub dst: u8, + program: Program, + scratch: Scratch<'static>, + kept: Vec, + /// Lab switch for the disable run: `false` drops the `inn[c]` operand, + /// i.e. removes the join. Never `false` outside a test. + pub join: bool, +} + +impl Prepared { + /// Resolve the query's identities under the relation frame and build the + /// program. Cold: once per (query, frame). + pub fn prepare( + hop: Hop2, + relation: &Relation, + table: &MapTable, + frame: &Frame, + fold: Fold, + ) -> Result { + if hop.rel != relation.rel { + return Err(NativeRefusal::WrongRelation { + bound: relation.rel, + asked: hop.rel, + }); + } + let map = table.map(frame, TILE).map_err(NativeRefusal::Read)?; + let src = map.local(hop.src).map_err(NativeRefusal::Map)?; + let dst = map.local(hop.dst).map_err(NativeRefusal::Map)?; + Ok(Self { + hop, + src, + dst, + program: Self::program(fold, true), + scratch: Scratch::new(words_for(WIDTH.positions()), 2), + kept: vec![0; words_for(WIDTH.positions())], + join: true, + }) + } + + fn program(fold: Fold, join: bool) -> Program { + // Plane 0 = out[a], plane 1 = inn[c], plane 2 = W. + let mut ops = Vec::new(); + if join { + ops.push(MaskOp::And { + a: Operand::Plane(0), + b: Operand::Plane(1), + dst: 0, + }); + ops.push(MaskOp::And { + a: Operand::Scratch(0), + b: Operand::Plane(2), + dst: 0, + }); + } else { + ops.push(MaskOp::And { + a: Operand::Plane(0), + b: Operand::Plane(2), + dst: 0, + }); + } + let mask = Operand::Scratch(0); + let terminal = match fold { + Fold::Any => Terminal::Any { mask }, + Fold::Count => Terminal::Count { mask }, + Fold::Keep => Terminal::Keep { mask }, + }; + Program::new(ops, terminal) + } + + /// Disable the join (lab falsifier only): rebuild the program without + /// `inn[c]`. + pub fn without_join(mut self, fold: Fold) -> Self { + self.join = false; + self.program = Self::program(fold, false); + self + } + + /// Hot: run the kept program over borrowed rows of `relation` and the + /// routed selection. Allocates nothing. + pub fn run(&mut self, relation: &Relation, selection: &Routed) -> Value { + let w = [selection.mask]; + let masks: [&[u64]; 3] = [relation.out_row(self.src), relation.inn_row(self.dst), &w]; + let planes = Planes { + n_rows: WIDTH.positions(), + masks: &masks, + lanes: &[], + }; + let out = Out::Mask(&mut self.kept); + execute_into( + &self.program, + &planes, + &Foreign::NONE, + &mut self.scratch, + out, + ) + .expect("probe program is valid") + } + + /// The witness mask a [`Fold::Keep`] run wrote (relation-tile positions). + pub fn kept(&self) -> u64 { + self.kept[0] + } +} + +/// Build a DR tile `[globals…]` in a fresh table and seal its frame. +pub fn tile(source: u64, globals: &[u64]) -> (MapTable, Frame) { + let mut t = MapTable::new(source, 0); + let map = LocalMap::prepare(WIDTH, globals).expect("probe tile"); + t.advance(source, 0, vec![(TILE, Some(map))]); + let f = t.seal(); + (t, f) +} diff --git a/crates/cognitive-polyfill-probe/tests/p0.rs b/crates/cognitive-polyfill-probe/tests/p0.rs new file mode 100644 index 000000000..bf9d5148b --- /dev/null +++ b/crates/cognitive-polyfill-probe/tests/p0.rs @@ -0,0 +1,446 @@ +//! D-COGNITIVE-POLYFILL P0 falsifier. Numbering follows the brief's §5 list. +//! +//! The oracle is an independent nested loop over the borrowed fact slice. It +//! counts and tests existence; it never builds rows. + +use std::alloc::{GlobalAlloc, Layout, System}; +use std::cell::Cell; + +use cognitive_polyfill_probe::*; +use lance_graph_dt64::dr::{ + Focus, FrameRevisions, FrameStore, GuardRefusal, Guards, MapRead, MapRefusal, Scope, +}; +use lance_graph_mask_risc::Value; + +// --- allocation counter (check 12) ----------------------------------------- + +// Per thread, so parallel tests do not count into each other. +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 A: Counting = Counting; + +// --- fixture --------------------------------------------------------------- + +const R: u64 = 1000; +const S: u64 = 1001; // another relation name +const PRODUCT: u64 = 2000; // Narsese `(*, …)` functor +const A_: u64 = 10; +const B: u64 = 11; +const C: u64 = 12; +const D: u64 = 13; +const E: u64 = 14; +const Z1: u64 = 90; +const Z2: u64 = 91; +const IDS: [u64; 5] = [A_, B, C, D, E]; +const FACTS: [(u64, u64); 4] = [(A_, B), (B, C), (C, D), (A_, E)]; + +fn hop(src: u64, dst: u64) -> Hop2 { + Hop2 { rel: R, src, dst } +} + +/// Independent oracle: Set (distinct witnesses) and Bag (derivations). +fn oracle(facts: &[(u64, u64)], src: u64, dst: u64, allowed: &dyn Fn(u64) -> bool) -> (u64, u64) { + let mut set = 0u64; + let mut bag = 0u64; + for &y in &IDS { + if !allowed(y) { + continue; + } + let left = facts.iter().filter(|&&f| f == (src, y)).count() as u64; + let right = facts.iter().filter(|&&f| f == (y, dst)).count() as u64; + if left > 0 && right > 0 { + set += 1; + } + bag += left * right; + } + (set, bag) +} + +fn world(facts: &[(u64, u64)]) -> (MapTable, Frame, Relation) { + let (t, f) = tile(1, &IDS); + let r = Relation::ingest(R, &t, &f, facts).unwrap(); + (t, f, r) +} + +use lance_graph_dt64::dr::{Frame, MapTable}; + +/// A selection in the relation tile's own coordinates, by global ids. +fn sel_in_rel(t: &MapTable, f: &Frame, ids: &[u64]) -> Routed { + let m = t.map(f, TILE).unwrap(); + let mut mask = 0u64; + for &g in ids { + mask |= 1 << m.local(g).unwrap(); + } + Routed { mask, dropped: 0 } +} + +fn exists(facts: &[(u64, u64)], src: u64, dst: u64, w: &[u64]) -> bool { + let (t, f, r) = world(facts); + let mut p = Prepared::prepare(hop(src, dst), &r, &t, &f, Fold::Any).unwrap(); + p.run(&r, &sel_in_rel(&t, &f, w)) == Value::Bool(true) +} + +// --- 1: equivalent answers on the common subset ---------------------------- + +/// MeTTa `(, (R A $y) (R $y C))`, MORK `(exec P (, (R A $y) (R $y C)) …)` and +/// the Atomese typed projection all hand-lower to this one pattern. +fn chain(src: u64, dst: u64) -> Pattern { + Pattern { + atoms: vec![ + Atom { + rel: R, + args: vec![Term::Ground(src), Term::Var(0)], + }, + Atom { + rel: R, + args: vec![Term::Var(0), Term::Ground(dst)], + }, + ], + } +} + +#[test] +fn c01_common_subset_agrees_with_oracle_exhaustively() { + let subsets: [&[u64]; 5] = [&IDS, &[B], &[E], &[], &[B, E]]; + let mut checked = 0; + for &src in &IDS { + for &dst in &IDS { + let h = lower(&chain(src, dst)).unwrap(); + assert_eq!(h, hop(src, dst)); + for w in subsets { + let (t, f, r) = world(&FACTS); + let sel = sel_in_rel(&t, &f, w); + let (set, _) = oracle(&FACTS, src, dst, &|y| w.contains(&y)); + let mut any = Prepared::prepare(h, &r, &t, &f, Fold::Any).unwrap(); + let mut cnt = Prepared::prepare(h, &r, &t, &f, Fold::Count).unwrap(); + assert_eq!( + any.run(&r, &sel), + Value::Bool(set > 0), + "{src}->?->{dst} W={w:?}" + ); + assert_eq!(cnt.run(&r, &sel), Value::Count(set as usize)); + checked += 1; + } + } + } + assert_eq!(checked, 125); + // anti-vacuity: the fixture has both answers + assert!(exists(&FACTS, A_, C, &IDS)); + assert!(!exists(&FACTS, A_, D, &IDS)); +} + +// --- 2/3: support edge vs unrelated edge ----------------------------------- + +#[test] +fn c02_deleting_the_supporting_edge_flips_the_answer() { + assert!(exists(&FACTS, A_, C, &IDS)); + let without: Vec<_> = FACTS.iter().copied().filter(|&e| e != (B, C)).collect(); + assert!(!exists(&without, A_, C, &IDS)); +} + +#[test] +fn c03_deleting_an_unrelated_edge_changes_nothing() { + let without: Vec<_> = FACTS.iter().copied().filter(|&e| e != (C, D)).collect(); + for &(s, d) in &[(A_, C), (A_, D), (B, D)] { + let before = exists(&FACTS, s, d, &IDS); + let after = exists(&without, s, d, &IDS); + if (s, d) == (B, D) { + // B->C->D uses the deleted edge: the control that it is not inert + assert!(before && !after); + } else { + assert_eq!(before, after, "{s}->?->{d}"); + } + } +} + +// --- 4/5: two selections, one global B at different local positions -------- + +#[test] +fn c04_two_selections_route_to_the_same_relation_coordinates() { + let (t, f, r) = world(&FACTS); // B is local 1 here + let (s1t, s1f) = tile(2, &[Z1, Z2, B]); // B is local 2 + let (s2t, s2f) = tile(3, &[B, Z1]); // B is local 0 + let s1 = Selection { mask: 1 << 2 }; + let s2 = Selection { mask: 1 << 0 }; + assert_ne!(s1.mask, s2.mask, "same identity, different local position"); + + let r1 = s1.route(&s1t, &s1f, &t, &f).unwrap(); + let r2 = s2.route(&s2t, &s2f, &t, &f).unwrap(); + assert_eq!(r1.mask, r2.mask); + assert_eq!(r1.mask, 1 << 1); + + let mut p = Prepared::prepare(hop(A_, C), &r, &t, &f, Fold::Any).unwrap(); + assert_eq!(p.run(&r, &r1), Value::Bool(true)); + assert_eq!(p.run(&r, &r2), Value::Bool(true)); + + // Joining on raw local positions is a different, wrong answer: s1's bit 2 + // is C in the relation tile, not B. + let raw = Routed { + mask: s1.mask, + dropped: 0, + }; + assert_eq!(p.run(&r, &raw), Value::Bool(false)); + + // A selected identity the relation tile does not hold is reported. + let s3 = Selection { + mask: (1 << 0) | (1 << 2), + }; // Z1 and B + assert_eq!(s3.route(&s1t, &s1f, &t, &f).unwrap().dropped, 1); +} + +#[test] +fn c05_dr_round_trip() { + let (t, f) = tile(1, &IDS); + let m = t.map(&f, TILE).unwrap(); + for &g in &IDS { + assert_eq!(m.global(m.local(g).unwrap()), Some(g)); + } + assert_eq!(m.local(Z1), Err(MapRefusal::Unmapped)); +} + +// --- 6: wrong frame -------------------------------------------------------- + +#[test] +fn c06_foreign_frame_refuses_everywhere() { + let (t, f, r) = world(&FACTS); + let (_other, foreign) = tile(1, &IDS); // same content, another table + assert!(matches!( + Relation::ingest(R, &t, &foreign, &FACTS), + Err(NativeRefusal::Read(MapRead::Stale(_))) + )); + assert!(matches!( + Prepared::prepare(hop(A_, C), &r, &t, &foreign, Fold::Any), + Err(NativeRefusal::Read(MapRead::Stale(_))) + )); + let (st, sf) = tile(2, &[B]); + let s = Selection { mask: 1 }; + assert!(matches!( + s.route(&st, &foreign, &t, &f), + Err(NativeRefusal::SelectionRead(MapRead::Stale(_))) + )); + assert!( + s.route(&st, &sf, &t, &f).is_ok(), + "control: the right frames route" + ); +} + +// --- 7: wrong relation / class, wrong scope -------------------------------- + +#[test] +fn c07_wrong_relation_and_wrong_scope_refuse() { + let (t, f, r) = world(&FACTS); + assert_eq!( + Prepared::prepare( + Hop2 { + rel: S, + src: A_, + dst: C + }, + &r, + &t, + &f, + Fold::Any + ) + .err(), + Some(NativeRefusal::WrongRelation { bound: R, asked: S }) + ); + // Scope is dt64's own guard. NOTE: `Guards::check` takes a `FrameStore`, + // and `MapTable` keeps its store private, so a MapTable frame cannot be + // guard-checked: this guard runs on its own store (finding W-2). + let store = FrameStore::new(FrameRevisions { + source: 1, + relation_map: 0, + coordinates: 0, + }); + let g = Guards { + frame: store.seal(), + focus: Focus { revision: 0 }, + scope: Scope { id: 7 }, + }; + assert_eq!( + g.check(&store, (Focus { revision: 0 }, Scope { id: 7 })), + Ok(()) + ); + assert_eq!( + g.check(&store, (Focus { revision: 0 }, Scope { id: 8 })), + Err(GuardRefusal::ScopeChanged) + ); +} + +// --- 8: Set versus Bag ------------------------------------------------------ + +#[test] +fn c08_duplicate_derivations_split_set_from_bag() { + let facts = [(A_, B), (A_, B), (B, C), (A_, E), (E, C)]; + let (t, f, r) = world(&facts); + let all = sel_in_rel(&t, &f, &IDS); + let (set, bag) = oracle(&facts, A_, C, &|_| true); + assert_eq!( + (set, bag), + (2, 3), + "fixture: two witnesses, three derivations" + ); + + let mut cnt = Prepared::prepare(hop(A_, C), &r, &t, &f, Fold::Count).unwrap(); + assert_eq!(cnt.run(&r, &all), Value::Count(set as usize)); + + let mut keep = Prepared::prepare(hop(A_, C), &r, &t, &f, Fold::Keep).unwrap(); + keep.run(&r, &all); + let kept = keep.kept(); + assert_eq!(kept.count_ones() as u64, set); + assert_eq!(r.bag_derivations(keep.src, keep.dst, kept), bag); + assert_ne!(set, bag, "a Set fold cannot answer the Bag question"); +} + +// --- 9: NAL truth is not a Boolean edge ------------------------------------- + +/// A NAL-shaped belief ` p>` with frequency and confidence codes. +#[derive(Clone, Copy)] +struct Belief { + s: u64, + p: u64, + f: u8, + c: u8, +} + +#[test] +fn c09_a_belief_is_not_an_edge_without_a_projection_policy() { + // Strong NEGATIVE evidence that B --> C: f = 0, c = 0.9. + let beliefs = [ + Belief { + s: A_, + p: B, + f: 255, + c: 230, + }, + Belief { + s: B, + p: C, + f: 0, + c: 230, + }, + ]; + // Projection 1: "a belief row exists" -> edge. + let existence: Vec<_> = beliefs.iter().map(|b| (b.s, b.p)).collect(); + // Projection 2: "f >= 0.5" -> edge. + let thresholded: Vec<_> = beliefs + .iter() + .filter(|b| b.f >= 128) + .map(|b| (b.s, b.p)) + .collect(); + let by_existence = exists(&existence, A_, C, &IDS); + let by_truth = exists(&thresholded, A_, C, &IDS); + assert!( + by_existence && !by_truth, + "the two projections disagree on the same beliefs" + ); + // A revision that only raises confidence changes no Boolean edge under + // either projection: the relational substrate cannot see revision. + let revised = [ + beliefs[0], + Belief { + c: 250, + ..beliefs[1] + }, + ]; + assert_ne!( + revised[1].c, beliefs[1].c, + "anti-vacuity: the revision changed the truth value" + ); + let thresholded2: Vec<_> = revised + .iter() + .filter(|b| b.f >= 128) + .map(|b| (b.s, b.p)) + .collect(); + assert_eq!(thresholded, thresholded2); +} + +// --- 10: unsupported shapes refuse ----------------------------------------- + +#[test] +fn c10_unsupported_patterns_refuse_with_a_reason() { + let v = |i| Term::Var(i); + let g = Term::Ground; + let p = |atoms: Vec| Pattern { atoms }; + let at = |rel, args| Atom { rel, args }; + // free endpoint: binding enumeration + assert_eq!( + lower(&p(vec![at(R, vec![v(1), v(0)]), at(R, vec![v(0), g(C)])])), + Err(Refusal::FreeEndpoint) + ); + // repeated variable: R($x, $x) + assert_eq!( + lower(&p(vec![at(R, vec![v(0), v(0)]), at(R, vec![v(0), g(C)])])), + Err(Refusal::RepeatedVariable) + ); + // structural: f(X, g(X)) / Narsese product <(*, A, $y) --> R> + let nested = Term::Nested { + functor: PRODUCT, + args: vec![g(A_), v(0)], + }; + assert_eq!( + lower(&p(vec![at(R, vec![nested, g(C)]), at(R, vec![v(0), g(C)])])), + Err(Refusal::NestedTerm) + ); + // two relations + assert_eq!( + lower(&p(vec![at(R, vec![g(A_), v(0)]), at(S, vec![v(0), g(C)])])), + Err(Refusal::TwoRelations) + ); + // one atom + assert_eq!( + lower(&p(vec![at(R, vec![g(A_), v(0)])])), + Err(Refusal::Arity) + ); + // not a chain: R(A,$y) R(C,$y) + assert_eq!( + lower(&p(vec![at(R, vec![g(A_), v(0)]), at(R, vec![g(C), v(0)])])), + Err(Refusal::FreeEndpoint) + ); + // control: the chain lowers + assert!(lower(&chain(A_, C)).is_ok()); +} + +// --- 11: the join is load-bearing ------------------------------------------- + +#[test] +fn c11_disabling_the_join_changes_the_answer() { + let (t, f, r) = world(&FACTS); + let all = sel_in_rel(&t, &f, &IDS); + let mut p = Prepared::prepare(hop(A_, D), &r, &t, &f, Fold::Any).unwrap(); + assert_eq!(p.run(&r, &all), Value::Bool(false)); + let mut nj = Prepared::prepare(hop(A_, D), &r, &t, &f, Fold::Any) + .unwrap() + .without_join(Fold::Any); + assert_eq!(nj.run(&r, &all), Value::Bool(true)); +} + +// --- 12: zero allocation on the hot path ------------------------------------ + +#[test] +fn c12_hot_run_allocates_nothing() { + let (t, f, r) = world(&FACTS); + let all = sel_in_rel(&t, &f, &IDS); + let mut p = Prepared::prepare(hop(A_, C), &r, &t, &f, Fold::Count).unwrap(); + let _ = p.run(&r, &all); // warm + let before = BYTES.with(|b| b.get()); + let mut n = 0usize; + for _ in 0..1000 { + if let Value::Count(c) = p.run(&r, &all) { + n += c; + } + } + let after = BYTES.with(|b| b.get()); + assert_eq!(n, 1000); + assert_eq!(after - before, 0, "hot run allocated"); +}