diff --git a/.claude/board/FRUITS.md b/.claude/board/FRUITS.md index cabae0e54..025312a67 100644 --- a/.claude/board/FRUITS.md +++ b/.claude/board/FRUITS.md @@ -4,7 +4,7 @@ Generated by `.claude/tools/fruits_index.py --write`. Do not hand-edit: add or change a `**Fruit:**` line on the ledger row and regenerate. CI fails when this file is stale. -Open: 35. Closed: 1. +Open: 36. Closed: 1. ## discovery torque @@ -42,6 +42,7 @@ _none open_ | tier | row | status | ledger | |---|---|---|---| +| High-signal | ISS-MULTIHOP-PRESENCE-ARM-UNRULED — projection or lens for multi-hop existence? (2026-11-03) | OPEN (operator decision). **Basis:** MEASURED (`.claude/probes/2026-11-03-d-bag-fold/`, `entries/2026-11-03-d-bag-fold-witnessed-existential.md`). | `ISSUES.md` | | High-signal | ISS-SOURCE-ROOT-AGENT-OR-REPORT — is a source root the observer or one report? (2026-10-31) | OPEN (operator decision). **Basis:** VERIFIED-IN-CODE (`crates/xlog-relcomp-probe/tests/provenance.rs` `root()` hashes the observer and the report's facts; `unrelated_sources_never_collapse_to_one_root` pins that one observer with two different reports gives two roots). | `ISSUES.md` | | High-signal | ISS-RECIPE-LOCO-VOCABULARY-EXISTS-TWICE — two `impl Vocabulary` claim the same 34 op bytes and disagree (2026-10-26) | OPEN (latent). **Basis:** VERIFIED-IN-CODE (OGAR `crates/ogar-loco/src/nars.rs:133-175`, read at OGAR `68cb29b`; lance-graph `crates/lance-graph-ogar/src/recipe_vocab.rs:134-185`, read at `main` `87b2899b`). | `ISSUES.md` | | High-signal | ISS-SIX-DECISIONS-NOT-EXECUTED-ACTION-GATE — `commit` still fails open where the decision says fail closed (2026-10-23) | OPEN. **Basis:** VERIFIED-IN-CODE (`crates/lance-graph-contract/src/action.rs:266` `pub fn commit`, `:328` `pub fn commit_via`; read at `main` `19c1324a`). | `ISSUES.md` | diff --git a/.claude/board/ISSUES.md b/.claude/board/ISSUES.md index 32adaa089..3e549b85b 100644 --- a/.claude/board/ISSUES.md +++ b/.claude/board/ISSUES.md @@ -1,3 +1,14 @@ +## ISS-MULTIHOP-PRESENCE-ARM-UNRULED — projection or lens for multi-hop existence? (2026-11-03) + +**Status:** OPEN (operator decision). **Basis:** MEASURED (`.claude/probes/2026-11-03-d-bag-fold/`, `entries/2026-11-03-d-bag-fold-witnessed-existential.md`). +**Fruit:** High-signal + +- `∃d R∧S∧T` evaluates in one Program from resident presence in two arms; both match an oracle on 8 cases. +- Arm P (ADMISSION B prepared projection) is gather-free but copies presence bits; the later zero-copy law admits only `$i`. +- Arm L (`$i` + `Filter::Semijoin` over the table's own planes) is zero-copy but executes `MaskOp::Gather`, which waits on call-site classification (EXO-140). +- Both depend on two unenforced invariants: plane order (`ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER`) and presence version (no contract witness). +- **What closes it:** the ruling on P vs L, then a witness naming the aligned planes; the probe's unchecked arms (cases 5, 8) must become refusals. + ## ISS-SOURCE-ROOT-AGENT-OR-REPORT — is a source root the observer or one report? (2026-10-31) **Status:** OPEN (operator decision). **Basis:** VERIFIED-IN-CODE (`crates/xlog-relcomp-probe/tests/provenance.rs` `root()` hashes the observer and the report's facts; `unrelated_sources_never_collapse_to_one_root` pins that one observer with two different reports gives two roots). diff --git a/.claude/board/entries/2026-11-03-d-bag-fold-witnessed-existential.md b/.claude/board/entries/2026-11-03-d-bag-fold-witnessed-existential.md new file mode 100644 index 000000000..acfbf556a --- /dev/null +++ b/.claude/board/entries/2026-11-03-d-bag-fold-witnessed-existential.md @@ -0,0 +1,16 @@ +# 2026-11-03 — D-BAG-FOLD: multi-hop existence from resident presence, no stored relation + +**Status:** MEASURED, lab only (`.claude/probes/2026-11-03-d-bag-fold/`, source `514948203`, rustc 1.99.0). No production change; implementation not authorized. + +- **Falsified.** A key-prefix range is not edge membership. Prefix-only existence says true with R or S deleted. `Count` over a range is not DISTINCT when keys repeat. A concept-only prefix crosses classids. +- **Executed.** `∃d R(a,b(d)) ∧ S(b(d),c(d)) ∧ T(c(d),d)` and the count of distinct valid `d` evaluate in ONE Program, with no composed relation, tuple or mask handoff, in two arms: + - **P:** an ADMISSION B prepared projection of each relation's own presence, then a row-aligned `And → Any/Count`, gather-free. + - **L:** pointer tables `$i` plus `Filter::Semijoin` over the table's own resident planes, zero-copy, executing `MaskOp::Gather`. + + Both arms agree with a nested-loop oracle on 8 cases (each edge deleted, multiple candidates with one or none valid, branch-crossing decoys, another classid, version change). Disabling either Semijoin goes red. +- **Conditional.** Plane order, key uniqueness and presence version are each a silent wrong answer when unchecked (measured). No contract witness covers plane order (`ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER`) or presence version. +- **Blocked by rulings, not capability.** + - Arm P copies presence bits, which ADMISSION B permits and the later zero-copy law does not. + - Arm L needs the `Gather` call-site classification (EXO-140, no owner). + - The DT64 route is refused at `r2il::prepare` (`GuardNotExecutable`), and no admitted DO word shape expresses the conjunction (`xlog::bag_count_admitted` admits only `[GroupCount, GroupCount, MulI64]`). +- **OPEN.** The P-vs-L operator ruling; a plane-naming witness; a mint guard that edges refine their source key. EXO-108 untouched. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index caa886ffc..a32225a22 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -558 entries, 2026-08-06 .. 2026-11-03. +559 entries, 2026-08-06 .. 2026-11-03. | date | entry id | finding | file | |---|---|---|---| +| 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 | `a10-writers-retract-xlog-pr` | | [2026-11-03-a10-writers-retract-xlog-pr.md](2026-11-03-a10-writers-retract-xlog-pr.md) | | 2026-11-02 | `sgr-recovery-gates` | | [2026-11-02-sgr-recovery-gates.md](2026-11-02-sgr-recovery-gates.md) | | 2026-11-02 | `p4-thought-git-codegraph-dt64-review` | | [2026-11-02-p4-thought-git-codegraph-dt64-review.md](2026-11-02-p4-thought-git-codegraph-dt64-review.md) | diff --git a/.claude/probes/2026-11-03-d-bag-fold/ARM-L-DECISION-MEMO.md b/.claude/probes/2026-11-03-d-bag-fold/ARM-L-DECISION-MEMO.md new file mode 100644 index 000000000..208338f1a --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/ARM-L-DECISION-MEMO.md @@ -0,0 +1,247 @@ +# D-BAG-FOLD: decision memo, the zero-copy pointer lens (Arm L) + +**Status:** DECISION PREPARATION. Documentation only. The ruling in §D is +**DRAFT / NOT IN FORCE**. Nothing here admits Arm L, a `MaskOp::Gather` call site, or +any implementation. + +Evidence: this folder (`README.md`, `REPORT.md`, the two probes). Source: +lance-graph `514948203`. Probe commit: `ae885f06a`. + +## Authorities read, by kind + +| record | kind | what it says that bears on Arm L | +|---|---|---| +| `entries/2026-10-20-six-decisions.md` §1 ADMISSION B | BINDING DECISION | Preparation may do "counted, version-witnessed, same-table key-range seeks over an attested sorted key" and "construct a projection for subsequent co-addressed evaluation". "A position derived from another relational column or table is not admissible as a read address". "Execution remains co-addressed." `Semijoin` / `EqU32Via` / `Gather` "need call-site classification". | +| `ISSUES.md` ISS-ADMISSION-PREP-BINDING (RULED) | BINDING (applies B) | The admitted evidence shape: the lookup runs in counted preparation, and "its fold program contains no `Gather` and no scatter terminal (checked on the program, disable-verified)". | +| `ISSUES.md` ISS-GATHER-HOP-1616, GATHER-DECISION | BINDING | `OutgoingHop` (`Gather` over `frontier[sources[i]]`) stays quarantined. It closes only by a rewrite as a co-addressed read `Thought(t)[T_a[i] : T_b[i]]`. | +| #1590 (`entries/2026-10-16-ledger-revision-1582-1591.md`) | BINDING (ban), no DECISION record | Value-derived positional reads banned. Existing gather code untouched. | +| `CLAUDE.md` P0 "There are no boundaries (2026-10-21)" | BINDING DOCTRINE, later than B | Zero copy everywhere. The one materialization is the pointer table `$i`. Everything else is "read in place through `$i`". Whole-template form `"{$i[0]}..{$i[15]}" -f $table{$i[0]}..`: a per-column pointer. | +| `.claude/knowledge/zero-copy-lens-law.md` (2026-07-28/29) | BINDING (operator rulings); several rows CONJECTURE | "Cross-tenant pointers are legitimate; cross-tenant values are not." Pointer projection (`target = cur + off`, computed) vs pointer chasing (loaded, then dereferenced). A stored value that a cast reproduces is a projection and must not be stored. | +| `mask-risc/src/ir.rs` `MaskOp::Gather` doc, `ScatterOrU32` survival | EXECUTABLE SOURCE | `Gather` = `dst[i] = foreign.words[lane_u32[i]]`. **Out of range is the zero-fallback, never an error.** A scattered mask is never an intermediate. | +| `quack/src/lib.rs` `Filter::Semijoin` | EXECUTABLE SOURCE | The foreign plane must be RESIDENT, never a mask another Program produced. `Gather` "may survive as a masking op only when its source is already legitimate resident state, its output is tile-local, and no dynamically-created population mask feeds it". | +| `contract/src/ordered_lane.rs` | EXECUTABLE SOURCE | `SealedFacetLane::seal` / `attest_sorted` (non-decreasing, so **duplicates allowed**); `OrderedLaneWitness {version, n_rows, digest of the key sequence, lens}`; `seek_from` = the witnessed same-table seek; `bound` validates the witness against the lane and checks the lens. | +| ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER | OPEN ISSUE | The witness attests the lane, not the execution row order of other planes. | +| EXO-140 | OPEN, no owner | Classification of the Semijoin / EqU32Via / Gather call sites not started. The classification must say whether each site relies on a frozen-codebook vertical read or on EXO-114's per-version order attest. | +| EXO-46 | OPEN | The counted global→focus binding membrane needs separate production admission. "Do not silently admit or forbid all indexed navigation as one category." | +| EXO-114 | OPEN | Order contract: identity / contiguity / total-order classes. Seek needs a per-sealed-version witness. Lance keeps no order. | +| EXO-105 | OPEN | mask-risc frozen. | +| #1791 | UNRESOLVED PROPOSAL | Witnessed derived population: the only route to reusing a scattered mask. Not authorized. | +| EXO-50 since 2026-10-30 | correspondence | No operator correction touches ADMISSION B, the gather rulings or the zero-copy `$i` rule (checked to 2026-11-03 11:50). | +| This folder, Arm L | LAB EVIDENCE | Oracle-equal on 8 cases; every check is probe-local. | + +## A. Recommendation + +**KEEP ARM L LAB-ONLY, REQUEST OWNER CLASSIFICATION.** + +1. **ADMISSION B's text excludes Arm L as written.** B admits indirection in + preparation only: "execution remains co-addressed". The admitted evidence pattern + requires a fold with no `Gather`. Arm L's `Gather` runs in execution and reads + `R_in[ib[i]]` with `ib[i] ≠ i`. +2. **The later doctrine points the other way.** CLAUDE.md (2026-10-21) makes `$i` the + single sanctioned materialization and reads columns "in place through `$i`", one + pointer per column. That is Arm L's shape. +3. **The two have not been reconciled.** No record states whether reading a resident + plane through `$i` counts as co-addressed execution, and neither text supersedes + the other. This memo does not reconcile them. That is the operator question at the + end. +4. **The index's provenance is undecided, not forbidden.** `ib` comes from the row's + own key, by address arithmetic plus a same-table witnessed seek. It is not an edge + column like `OutgoingHop`'s `sources[i]`. Whether "another relational column" + covers a key-derived pointer lane is exactly EXO-140, which has no owner. +5. **Structural derivation is necessary, not sufficient.** That an index is derived + from structure does not admit the `MaskOp::Gather` that consumes it. Every call + site still needs EXO-140's classification and the witnesses in §C. +6. **Today's source would admit silent wrong answers.** + - `Gather` turns an out-of-range pointer into a silent `false`. + - No contract witness binds the presence planes or the pointer table to a version. + +**Arm P is a negative architectural comparison, not a fallback.** Its shape is the one +B admitted (projection in preparation, gather-free fold), but it copies each presence +bit into a second plane. The zero-copy law treats that as a projection stored beside +the first: a cast through `$i` reproduces it, and no rung is gained. Arm P is kept in +the probe only to show that the conjunction holds without `Gather`. It is not a route +to implement if Arm L is refused. + +## B. Access provenance + +| access form | index producer | index consumer | read position decided by | existing classification | +|---|---|---|---|---| +| Direct co-addressed fold | none: every operand is row `i` | `MaskOp::And/Or/Ternlog`, `Pred::*` | the row itself | ADMITTED (B: "execution remains co-addressed"). v1 method C and v2 Arm P execution. | +| Prepared address lens `$i` | `SealedFacetLane::seek_from` (or `bound`) keyed by the row's own key arithmetic (`parent(key)`), witnessed, counted, in preparation | `MaskOp::Gather` via `Filter::Semijoin` / `EqU32Via`, in execution | the row's own declared address | **AMBIGUOUS, NOT ADMITTED.** B admits the seek in preparation and says nothing to admit the indirect read in execution. CLAUDE.md 2026-10-21 describes reading through `$i`. EXO-140 / EXO-46 open. | +| Value-directed Gather | a relational value lane (`sources[i]`, an fk, a scattered mask) | `MaskOp::Gather`, `ScatterOrU32` hop | another column's or table's value | FORBIDDEN (#1590; GATHER-DECISION; B "not admissible as a read address"; survival law for produced masks). | + +The machine instruction is the same in rows 2 and 3. Only the producer differs, so +a classification must key on the producer, not on the opcode. Row 2 is not thereby +admitted: a lawful producer is one of several required conditions (§C), and none of +them is enforced in source today except the seek itself. + +## C. Witness completeness + +Five properties are easily conflated, and each needs its own witness: + +- **provenance:** where `$i` came from; +- **bounds:** whether `$i[j]` lies inside the plane; +- **ordered-lane identity:** whether the planes are in the order the key witness + certifies; +- **key uniqueness:** whether one address names exactly one row; +- **presence-version invalidation:** whether a presence change retires `$i` and its + witness. + +A key-order witness answers only ordered-lane identity, and only for the key lane. +A key lane can stay unchanged while a presence plane changes (v2 case 8). + +| invariant | producer | witness type | verifying consumer | status today | negative control | +|---|---|---|---|---|---| +| 1. **Provenance:** `$i` derived from the candidate's declared address, never from a value lane | probe `parent()` + seek | none | none | **probe-only** | disable 6 (not built) | +| 2. Seek counted and version-witnessed | `SealedFacetLane::seek_from` | `OrderedLaneWitness` | `SealedFacetLane::validate` | **enforced** for the seek itself (lens, digest, version) | stale witness: `a_prefix_aperture_under_a_stale_witness_sweeps_and_says_why` | +| 3a. **Frame** consistency: `$i`, planes and key lane read in one frame / focus | `FrameStore`; `relcomp::Chain` (lab); `r2il::prepare` → `guards.check(frames, now)` | frame issue / focus | `prepare` (no production caller) | **lab-only** | not built for the lens | +| 3b. **ClassId / codebook** consistency: one classid, one codebook, one lens | `OrderedLaneWitness.lens` | `SemanticLens` | `bound` / `bound_aperture` (`LensMismatch`) | **partial**: lens enforced on the seek; nothing ties the presence planes to that lens | v2 case 7 (probe); `LensMismatch` tests | +| 3c. **Scope** consistency: every pointer target inside the declared scope | `relcomp::Chain` scope check (lab) | scope | none in quack / mask-risc | **probe-only / lab-only** | v2 case 7 cross-class edge refused (probe) | +| 4. Source planes resident, not produced `Keep` | caller | none (doc precondition) | none | **missing** (documented obligation on `Filter::Semijoin`) | disable 5 | +| 5. No intermediate or composed relation | program shape | none | none | **probe-only** | v2 by construction | +| 6. No mask from one program feeds another | program shape | none | none | **probe-only** | survival-law tests cover scatter only | +| 7. **Bounds:** every pointer `< n_rows` | seek result | none | `Gather` **zero-fallback** | **MISSING, and silent**: out of range reads as `false` | disable 3 | +| 8. **Ordered-lane identity:** physical plane order = certified order | `seal` sorts its own keys | `OrderedLaneWitness.digest` (keys only) | none for planes | **MISSING** (ISS-WITNESSED-RANGE…) | disable 1; v2 case 5 | +| 9. **Presence-version invalidation:** a deletion or version change retires `$i` and its witness | `LanceVersion` in the key witness | key lane only | none for presence planes or `$i` | **MISSING** for presence | disable 2; v2 case 8 | +| 10a. **Key uniqueness** in the admitted population | `attest_sorted` | none (non-decreasing passes) | `CountKeyRunsU32` checks order for its own terminal only | **MISSING** as a lens precondition | disable 4; v2 case 6 | +| 10b. Each edge refines its source by exactly one tier | mint / storage | none | none (no guard in quack, mask-risc or lance-graph-xlog) | **probe-only** | v2 case 7 (`NonRefiningEdge`) | + +Totals: one enforced (2), one partial (3b), four missing (4, 7, 8, 9), one missing +as a precondition (10a), six probe-only or lab-only (1, 3a, 3c, 5, 6, 10b). + +## D. Minimal operator ruling — **DRAFT / NOT IN FORCE** + +> **DRAFT / NOT IN FORCE — for operator decision only. Grants no admission and +> authorizes no implementation.** +> +> **ADMISSION B — address-lens clarification (proposed).** In execution, a fold may +> read a resident plane of the same table at `$i[j]` only if every one of these holds +> and is checked by the contract, not by the caller: +> +> 1. **Provenance:** `$i` was produced in preparation by `SealedFacetLane` seeks keyed +> by arithmetic on row `j`'s own key, never by any value lane. +> 2. **Frame, ClassId, codebook and scope:** `$i`, every plane it reads and the key +> lane belong to one frame, one classid, one codebook (lens) and one declared +> scope. Any mismatch is a refusal. +> 3. **Presence version:** `$i`, every plane and the key lane carry one version, and +> a presence change retires `$i`. The fold refuses on any mismatch. +> 4. **Ordered-lane identity:** every plane is attested to be in the key witness's +> order, not only the key lane. +> 5. **Bounds:** every `$i[j]` is checked `< n_rows` before the fold. An out-of-range +> pointer is a refusal, never `Gather`'s zero-fallback. +> 6. **Uniqueness:** the key lane is strictly increasing. +> 7. **Residency:** the read plane is resident, never a mask a program produced. +> 8. **Single program:** one terminal, whose output feeds no other program. +> +> **Remains forbidden:** +> - every `MaskOp::Gather` outside this clause. A structurally derived index is not +> enough on its own; +> - an index produced from any value lane (edge endpoints, foreign keys, codebook +> values) or from another table; +> - an index computed from a mask a program produced, or carried between programs; +> - a scattered mask as an intermediate (`ScatterOrU32` survival unchanged); +> - `OutgoingHop` (quarantine unchanged); +> - any recursive or variable-depth use (EXO-73); +> - any Bag multiplicity claim (EXO-108). +> +> Adds no opcode and no copy. Does not admit Arm P's prepared presence copy. + +## E. Independent falsifier + +### The eight-case oracle results (measured, `v2_witnessed_existential`, 0 mismatches) + +Both arms agree with each other and with a nested-loop oracle in every checked case. +Prefix-only is shown for contrast. + +| case | Arm P / Arm L | oracle | prefix-only | +|---|---|---|---| +| 1 all three edges present | (true, 1) | (true, 1) | true | +| 2a R deleted | (false, 0) | (false, 0) | **true** | +| 2b S deleted | (false, 0) | (false, 0) | **true** | +| 2c T deleted | (false, 0) | (false, 0) | false | +| 3 three candidates, one valid | (true, 1) | (true, 1) | — | +| 3b three candidates, two valid | (true, 2) | (true, 2) | — | +| 4 three candidates, none valid | (false, 0) | (false, 0) | **true** | +| 5 permuted rows | refused (`OrderNotAttested`); unchecked arm (false, 0) | (true, 1) | — | +| 6 duplicate terminal key | refused at seal (`DuplicateKey`); forged witness (true, 2) | (true, 1) | — | +| 7 another class holds the only valid chain | (false, 0); cross-class edge refused (`NonRefiningEdge`) | (false, 0) | — | +| 8 S deleted after preparation | stale refused (`StaleVersion`) in both arms; unchecked stale (true, 1); re-prepared (false, 0) | (false, 0) | — | + +Measured disable runs: removing arm L's `Semijoin` on `S_in`, or the one on `R_in`, +trips the arm-agreement assertion (red). + +### The six disable runs the ruling must turn red + +The smallest admissibility probe is the v2 fixture, with Arm L's checks moved from the +probe into whatever enforces §D. + +| # | disable | required after a ruling | today | +|---|---|---|---| +| 1 | permute a presence plane but not the key lane | refusal | silent false (a key digest cannot see it) | +| 2 | delete a presence bit without a version bump | refusal | silent stale (case 8 unchecked) | +| 3 | `ib[j] = n_rows` | refusal | silent `false` (zero-fallback) | +| 4 | duplicate key | refusal at attest | silent count 2 (case 6 forged) | +| 5 | pass a `Keep` output as the foreign plane | refusal | accepted (doc-only precondition) | +| 6 | fill `ib` from an edge-endpoint value lane | refusal (provenance) | accepted | + +Silence twin: the eight cases above stay equal to the oracle with every check on. +Admitted-shape parity: Arm L ≡ the direct co-addressed fold (v1 method C) on fixed +endpoints. + +Disable 6 is the one that separates a lens from a value-directed gather. Unless it is +refused by something other than the probe's own code, the ruling cannot be checked. + +## F. Unresolved boundaries + +- **EXO-140:** who classifies the `Filter::Semijoin` / `EqU32Via` / `Gather` call + sites, and whether "another relational column" covers a key-derived pointer lane. + Owner: none named. +- **EXO-46:** whether the counted global→focus pointer table may be used in + production execution, and under which witness. Not to be decided as "all indexed + navigation". +- **EXO-114:** per-version order attest. Seek needs total order. Uniqueness is a + separate property no class currently states. +- **EXO-105:** mask-risc frozen. §D condition 5 (refuse out-of-range rather than zero + fall-back) must be met outside mask-risc, by a pre-fold bounds check, unless the + operator unfreezes it. +- **DT64 behaviour admission — independently gated.** Even if Arm L were admitted, a + DT64 method could not yet use it: + - `r2il::prepare` refuses guarded bindings (`GuardNotExecutable`, + `binding.rs:290-291`); + - `xlog::bag_count_admitted` admits only `[GroupCount, GroupCount, MulI64]` + (`lib.rs:399`). + + The smallest missing connection is an admitted DO word shape + `presence-conjunction → Any` whose preparation is this lens. Its falsifier is the + same binding refused under a stale frame (`guards.check`) and under each disable + above. ON stays a change trigger, never the existence test. This route needs its own + operator decision; a ruling on §D does not grant it. +- **Out of scope by construction:** + - arbitrary graph edges (no key arithmetic for the parent); + - variable depth and recursion (EXO-73); + - multiple paths to one endpoint, and Bag multiplicity (EXO-108); + - SCCs. + +## Answer to the key question + +In principle, yes. A certified address lens names where each relation's presence +witness already lives, so the fold can prove the relationship without the relationship +ever being stored. No presence bit is copied; only the pointer table is materialized. + +Today's source does not certify such a lens. It certifies the key order of one lane, +the seek over it, and the lens of that seek. The interpretive question of whether +reading through `$i` is co-addressed execution has no owner. Arm L stays lab-only. + +## Operator question (OPEN) + +**Does a preparation-time, witnessed, same-table address mapping `$i` qualify as +co-addressed execution when the fold subsequently reads resident presence planes +through `$i`, despite lowering to `MaskOp::Gather`?** + +- **If yes:** which exact witnesses are required for provenance, frame (with + ClassId, codebook and scope), ordered-lane identity, presence version, key + uniqueness and bounds? §D is one draft answer. +- **If no:** which existing law excludes it (ADMISSION B's "execution remains + co-addressed", the #1590 ban, or another), and what lawful zero-copy route remains + for multi-hop existence? Arm P's copied projection is not such a route under the + zero-copy law. diff --git a/.claude/probes/2026-11-03-d-bag-fold/README.md b/.claude/probes/2026-11-03-d-bag-fold/README.md new file mode 100644 index 000000000..42e9c440d --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/README.md @@ -0,0 +1,78 @@ +# D-BAG-FOLD evidence: multi-hop existence from resident presence + +**Status:** MEASURED, lab only. No production code changed. mask-risc, Quack and +the xlog cube are consumed unchanged. + +**Source:** lance-graph `514948203` (merge of #1936, = `origin/main` when measured). +ndarray: the sibling checkout at `../ndarray` relative to the repo root +(here a symlink to the AdaWorldAPI/ndarray checkout). Toolchain: `rustc 1.99.0` +(`ndarray 0.17.2` requires it; the repo default 1.97 refuses). + +## Contents + +| path | what | provenance | +|---|---|---| +| `original/COADDRESSED-FOLD.md` | first report + its addendum | session scratchpad, byte copy, sha256 `632f0f9d…677e` | +| `original/SIDE-BOUNDARY.md` | the `Cube::side()` boundary audit | session scratchpad, byte copy, sha256 `5789faf8…300c` | +| `original/cofold-main.rs` | the first probe, unchanged | sha256 `0dde1fb5…5854` | +| `original/cofold-Cargo.toml` | its manifest (absolute paths, scratchpad-only) | sha256 `d9085726…af0c` | +| `probe/src/bin/v1_prefix_vs_presence.rs` | the first probe, byte-identical to `original/cofold-main.rs`, built here with relative paths | — | +| `probe/src/bin/v2_witnessed_existential.rs` | this pass: the existential, eight cases, two arms, oracle | new | +| `REPORT.md` | conclusions | new | +| `ARM-L-DECISION-MEMO.md` | decision preparation for Arm L; the ruling in it is DRAFT / NOT IN FORCE | new | +| `original/ARM-L-DECISION-MEMO.first-draft.md` | the memo as first written, before the operator's revision requests | session scratchpad, byte copy, sha256 `5743b1ee…` | + +The originals are copies of artifacts that existed in this session's scratchpad. +Nothing in `original/` was reconstructed. + +## Run + +```sh +cd .claude/probes/2026-11-03-d-bag-fold/probe +CARGO_PROFILE_DEV_DEBUG=0 cargo +1.99.0 run -q --bin v1_prefix_vs_presence +CARGO_PROFILE_DEV_DEBUG=0 cargo +1.99.0 run -q --bin v2_witnessed_existential # exits 1 on any oracle mismatch +``` + +The probe has its own `[workspace]` table, so the root workspace never builds it. +Set `CARGO_TARGET_DIR` outside the repo; `target/` must not be committed. + +## Expected output (v2, measured) + +``` +1 all present got=Ok((true, 1)) oracle=(true, 1) OK +2a R deleted (prefix-only says true) got=Ok((false, 0)) oracle=(false, 0) OK +2b S deleted (prefix-only says true) got=Ok((false, 0)) oracle=(false, 0) OK +2c T deleted (prefix-only says false) got=Ok((false, 0)) oracle=(false, 0) OK +3 three candidates, one valid got=Ok((true, 1)) oracle=(true, 1) OK +4 three candidates, none valid (prefix-only says true) got=Ok((false, 0)) oracle=(false, 0) OK +3b three candidates, two valid got=Ok((true, 2)) oracle=(true, 2) OK +5 permuted rows, checked: prepare = Some(OrderNotAttested) +5 permuted rows, UNCHECKED arm: Ok((false, 0)) vs oracle (true, 1) +5 sealing a permuted lane: Some(OrderNotAttested) +6 duplicate d1, seal: Some(DuplicateKey) +6 duplicate d1, forged witness: Ok((true, 2)) vs oracle (true, 1) +7 other class holds the only valid chain got=Ok((false, 0)) oracle=(false, 0) OK +7 edge crossing the classid boundary: build = Some("refused (NonRefiningEdge)") +8 before change: Ok((true, 1)) +8 after S(b1,c1) deleted, stale projection, checked: Some(StaleVersion) +8 stale projection, UNCHECKED: Ok((true, 1)) +8 re-prepared at version 2 got=Ok((false, 0)) oracle=(false, 0) OK +8 arm L under the stale witness: Some(StaleVersion) +8 arm L at version 2 got=Ok((false, 0)) oracle=(false, 0) OK +0 mismatches against the oracle +``` + +Every checked case also asserts that the two arms agree. **Disable runs (red):** +removing arm L's `Semijoin` on `S_in`, or the one on `R_in`, trips the +arm-agreement assertion. The `UNCHECKED` lines are the witness-check disables: +each removed check produces a silent wrong answer (cases 5, 6, 8). + +## Limitations + +- Toy fixture: one class, 9–13 nodes, 8-bit tiers, depth fixed at 4. +- The witness is a probe-local mirror of `OrderedLaneWitness` plus a presence + version. Production `SealedFacetLane` and `LanceVersion` were not exercised. +- Edge membership is stamped at the child row, and only one-tier refining edges + are representable. A general graph is outside this layout. +- No timing: correctness only, so the no-ms rule is not engaged and nothing here + is a performance claim. diff --git a/.claude/probes/2026-11-03-d-bag-fold/REPORT.md b/.claude/probes/2026-11-03-d-bag-fold/REPORT.md new file mode 100644 index 000000000..dba78b4da --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/REPORT.md @@ -0,0 +1,123 @@ +# D-BAG-FOLD: can a fold establish a relationship that was never stored? + +Question: `∃d. P(d)`, `P(d) = R(a,b(d)) ∧ S(b(d),c(d)) ∧ T(c(d),d)`, evaluated +natively, with every edge-presence witness preserved and no composed relation +stored. Probe and expected output: `README.md`. + +**Short answer.** Yes, in two lawful-looking arms, both under explicit, +checked witnesses. Each arm meets exactly one gate, and they are different gates: + +- **Arm P (projection).** Gather-free, but it copies presence bits. +- **Arm L (lens).** Zero-copy, but it executes `MaskOp::Gather`. + +Which arm is admitted is an ownership decision, not a missing capability. + +A coordinate locates a candidate. Presence, read inside the fold, decides it. + +## The two arms + +Both arms use the same preparation, and preparation is ADMISSION B's shape +(`entries/2026-10-20-six-decisions.md` §1). It does counted, version-witnessed, +same-table seeks over an attested sorted key, keyed by each candidate's own +address (`parent(d)`, `parent(parent(d))`). + +- **Arm P (projection).** Preparation re-addresses each relation's own presence + onto the candidate coordinates: `R'[j] = R_in[b(d_j)]`, `S'[j]`, `T'[j]`. No + plane is a composition. Execution is one Program, `And(R', S', T') → Any | Count`, + with row-aligned ops only and no `Gather` (asserted). +- **Arm L (lens).** Preparation builds only the pointer tables `$i` (`ib`, `ic`: + the rows of b and c for each row). Execution is one Program over the node lane: + `Range(subtree a) ∧ T_in ∧ Semijoin(ib → R_in) ∧ Semijoin(ic → S_in)`. + `R_in` and `S_in` are the table's own resident planes, read in place. This is + the zero-copy template of `CLAUDE.md` ("reads column 0 from lane A and column 1 + from lane B at position `$i`"). + +## PROVEN (executed against an independent nested-loop oracle) + +| claim | evidence | +|---|---| +| Both arms answer `∃d P(d)` and the count of distinct valid `d` in one Program each, with no stored composition, no tuple and no cross-program mask handoff | v2 cases 1, 2a-c, 3, 3b, 4, 7, 8: 0 mismatches | +| Each edge's presence is load-bearing in the fold | cases 2a-c; arm-L disables of either `Semijoin` go red | +| Branch-crossing decoys are rejected (S under a b without R; T under a c without S) | cases 3 and 4 | +| A chain held entirely by another classid is not counted, and an edge crossing the classid boundary is refused at build | case 7 | +| `Filter::Semijoin` over resident same-table planes runs in today's mask-risc with no change | arm L, `execute_into` with `Foreign` | + +## CONDITIONAL (correct only while a checked invariant holds; silent when the check is removed) + +| invariant | unchecked failure (measured) | who checks it today | +|---|---|---| +| plane order = sealed key order | case 5: `(false,0)` vs oracle `(true,1)` | probe recomputes the key digest. In production it is the caller's documented obligation: `quack/src/lib.rs:859-885`, `ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER` OPEN | +| key uniqueness | case 6: `(true,2)` vs `(true,1)` | probe seal refuses. `CountKeyRunsU32` enforces order for its own terminal only | +| presence/version currency | case 8: stale `(true,1)` after S deleted | probe compares versions. `OrderedLaneWitness` (`contract/src/ordered_lane.rs:51-56`) carries a `LanceVersion` for the key lane, nothing for presence planes | +| edge refines its source (child = one-tier extension) | not representable: build refuses | probe only. No production guard located in quack, mask-risc or lance-graph-xlog (closed set, read for this) | + +## FALSIFIED + +- Prefix-only existence: it says true with R or S deleted (cases 2a, 2b, 4). + Address compatibility is not edge membership. +- `hi − lo` or `Count` as a distinct count when keys can repeat (case 6; v1 case 2). +- A concept-only (16-bit) prefix as a class boundary (v1 case 3). + +## BLOCKED (existing rulings, not missing capability) + +- **Arm L:** it executes `MaskOp::Gather`. ADMISSION B requires call-site + classification of `Filter::Semijoin` / `Pred::EqU32Via` / `MaskOp::Gather` + before any ruling (six-decisions §1), and that classification has no owner + (EXO-140). Whether a same-table, address-derived `$i` counts as "a position + derived from another relational column" is exactly the unanswered question. +- **Arm P:** it copies presence bits into a prepared projection. ADMISSION B + (2026-10-20) permits "construct a projection for subsequent co-addressed + evaluation". The zero-copy law in `CLAUDE.md` (2026-10-21, later) admits only + the pointer table `$i` as a materialization. The two rulings disagree on this + arm; neither supersedes the other in text. +- **Reusing any fold's output mask as the next hop's input** (the recursive + route): the scatter survival law (`ir.rs:329-342`) and #1791 (not authorized). + +## UNKNOWN + +- Arm L's cost, and whether its `Gather` stays tile-local at scale. Not measured; + the no-ms rule applies before any claim. +- Variable path length or depth not fixed by the address: not tested. It needs a + per-depth union, or an unbounded `$i` chain. +- General graphs whose edges do not refine their source key: outside this layout, + so the parent of a node is not address arithmetic. Not shown either way. +- The Bag question (next section): the obstacle is located, not resolved. + +## The Bag question + +Can an admitted DT64 method ask "does this Bag contain a valid three-hop +consequence"? Traced: + +- `MethodBinding` (`dt64/src/lib.rs:197-213`) has ON (change trigger), WHEN + (`Option`) and DO (`effects`). The existence test belongs in WHEN or DO. + It is not ON: ON detects change, not existence. +- WHEN: `r2il::prepare` refuses any guarded binding: `GuardNotExecutable` + (`r2il/src/binding.rs:290-291`). +- DO: the only xlog-admitted Bag method shape is + `[GroupCount, GroupCount, MulI64]`, a two-side count (`xlog/src/lib.rs:384-403`). + No admitted word sequence expresses `And` over three re-addressed presences + followed by `Any`. +- Frames: `prepare` checks `r.guards.check(frames, now)` before anything else + (`binding.rs:284`). + +**Location of the obstacle.** It is not the operand layout: both arms above +show the conjunction is expressible. It is not execution capability: both arms +run on today's executor. It is three things: + +1. **Method binding.** No admitted word shape, and WHEN is not executable. +2. **Witness admission.** No contract witness covers plane order or presence + version. +3. **The P-vs-L ownership ruling.** + +## Smallest missing pieces + +| # | location | owner / contract | smallest missing piece | falsifier | authorized? | +|---|---|---|---|---|---| +| 1 | `quack/src/lib.rs:859-885`, `contract/src/ordered_lane.rs:51` | D-DIAMOND-1, `ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER` | the witness must name the planes it aligns (order + version), checked before execution | v2 case 5 and case 8 unchecked arms must become refusals | no | +| 2 | six-decisions §1 vs `CLAUDE.md` zero-copy law | operator ruling | which arm is lawful: copied projection (P) or `$i` + same-table `Gather` (L) | the same eight cases, under whichever arm is ruled | no; operator decision | +| 3 | `quack` / `mask-risc` call sites of `Gather` / `Semijoin` | EXO-140 (no owner) | classify same-table, address-derived `$i` | arm L green, with the gather classification asserted | no | +| 4 | `r2il/src/binding.rs:290-291`, `xlog/src/lib.rs:399` | DT64 / BindStore | an admitted word shape for presence conjunction → `Any`, or an executable WHEN | a binding that runs v2 case 3 through `prepare`/`run` and is refused for a stale frame | no | +| 5 | layout | storage (mint) | a guard that every stored edge refines its source key | inject a non-refining edge; it must be refused, never stamped | no | + +EXO-108 (Bag multiplicity) is untouched. `Count` here counts distinct valid +endpoints because the keys are unique; it is not a path count. diff --git a/.claude/probes/2026-11-03-d-bag-fold/original/ARM-L-DECISION-MEMO.first-draft.md b/.claude/probes/2026-11-03-d-bag-fold/original/ARM-L-DECISION-MEMO.first-draft.md new file mode 100644 index 000000000..79b906c95 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/original/ARM-L-DECISION-MEMO.first-draft.md @@ -0,0 +1,178 @@ +# D-BAG-FOLD: decision memo, the zero-copy pointer lens (Arm L) + +Read-only. Target: lance-graph PR #1937 at `ae885f06a`, source `514948203`. No source, +plan, Linear or PR state changed. + +## Authorities read, by kind + +| record | kind | what it says that bears on Arm L | +|---|---|---| +| `entries/2026-10-20-six-decisions.md` §1 ADMISSION B | BINDING DECISION | Preparation may do "counted, version-witnessed, same-table key-range seeks over an attested sorted key" and "construct a projection for subsequent co-addressed evaluation". "A position derived from another relational column or table is not admissible as a read address". "Execution remains co-addressed." `Semijoin` / `EqU32Via` / `Gather` "need call-site classification". | +| `ISSUES.md` ISS-ADMISSION-PREP-BINDING (RULED) | BINDING (applies B) | The admitted evidence shape: the lookup runs in counted preparation, and "its fold program contains no `Gather` and no scatter terminal (checked on the program, disable-verified)". | +| `ISSUES.md` ISS-GATHER-HOP-1616, GATHER-DECISION | BINDING | `OutgoingHop` (`Gather` over `frontier[sources[i]]`) stays quarantined. It closes only by a rewrite as a co-addressed read `Thought(t)[T_a[i] : T_b[i]]`. | +| #1590 (`entries/2026-10-16-ledger-revision-1582-1591.md`) | BINDING (ban), no DECISION record | Value-derived positional reads banned. Existing gather code untouched. | +| `CLAUDE.md` P0 "There are no boundaries (2026-10-21)" | BINDING DOCTRINE, later than B | Zero copy everywhere. The one materialization is the pointer table `$i`. Everything else is "read in place through `$i`". Whole-template form `"{$i[0]}..{$i[15]}" -f $table{$i[0]}..`: a per-column pointer. | +| `.claude/knowledge/zero-copy-lens-law.md` (2026-07-28/29) | BINDING (operator rulings); several rows CONJECTURE | "Cross-tenant pointers are legitimate; cross-tenant values are not." Pointer projection (`target = cur + off`, computed) vs pointer chasing (loaded, then dereferenced). A stored value that a cast reproduces is a projection and must not be stored. | +| `mask-risc/src/ir.rs` `MaskOp::Gather` doc, `ScatterOrU32` survival | EXECUTABLE SOURCE | `Gather` = `dst[i] = foreign.words[lane_u32[i]]`. **Out of range is the zero-fallback, never an error.** A scattered mask is never an intermediate. | +| `quack/src/lib.rs` `Filter::Semijoin` | EXECUTABLE SOURCE | The foreign plane must be RESIDENT, never a mask another Program produced. `Gather` "may survive as a masking op only when its source is already legitimate resident state, its output is tile-local, and no dynamically-created population mask feeds it". | +| `contract/src/ordered_lane.rs` | EXECUTABLE SOURCE | `SealedFacetLane::seal` / `attest_sorted` (non-decreasing, so **duplicates allowed**); `OrderedLaneWitness {version, n_rows, digest of the key sequence, lens}`; `seek_from` = the witnessed same-table seek; `bound` validates the witness against the lane and checks the lens. | +| ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER | OPEN ISSUE | The witness attests the lane, not the execution row order of other planes. | +| EXO-140 | OPEN, no owner | Classification of the Semijoin / EqU32Via / Gather call sites not started. The classification must say whether each site relies on a frozen-codebook vertical read or on EXO-114's per-version order attest. | +| EXO-46 | OPEN | The counted global→focus binding membrane needs separate production admission. "Do not silently admit or forbid all indexed navigation as one category." | +| EXO-114 | OPEN | Order contract: identity / contiguity / total-order classes. Seek needs a per-sealed-version witness. Lance keeps no order. | +| EXO-105 | OPEN | mask-risc frozen. | +| #1791 | UNRESOLVED PROPOSAL | Witnessed derived population: the only route to reusing a scattered mask. Not authorized. | +| EXO-50 since 2026-10-30 | correspondence | No operator correction touches ADMISSION B, the gather rulings or the zero-copy `$i` rule (checked to 2026-11-03 11:50). | +| PR #1937 Arm L | LAB EVIDENCE | Oracle-equal on 8 cases; checks are probe-local. | + +## A. Recommendation + +**KEEP ARM L LAB-ONLY, REQUEST OWNER CLASSIFICATION.** + +Reasons, from the records above: + +1. **Admission B's text excludes Arm L as written.** B admits indirection in + preparation only: "execution remains co-addressed". The admitted evidence pattern + requires a fold with no `Gather`. Arm L's `Gather` runs in execution and reads + `R_in[ib[i]]` with `ib[i] ≠ i`. +2. **The later doctrine points the other way.** CLAUDE.md (2026-10-21) makes `$i` the + single sanctioned materialization and reads columns "in place through `$i`", one + pointer per column. That is Arm L's shape. Neither text supersedes the other. +3. **The index's provenance is undecided, not forbidden.** `ib` comes from the row's + own key, by address arithmetic plus a same-table witnessed seek. It is not an edge + column like `OutgoingHop`'s `sources[i]`. Whether "another relational column" + covers a key-derived pointer lane is exactly EXO-140, which has no owner. +4. **Arm L also fails on two enforcement points today:** + - `Gather` turns an out-of-range pointer into a silent `false`; + - no contract witness binds the presence planes or the pointer table to a + version. + + Admitting it now would admit a silent wrong answer. + +**Arm P is weaker, not stronger.** Its shape is the one B admitted (projection in +preparation, gather-free fold), but it copies each presence bit into a second plane. +The zero-copy law calls that a projection stored beside the first. A cast through +`$i` reproduces it, and no rung is gained. So Arm P conflicts with the later rule. +The decision is therefore not "P or L". It is how the 2026-10-21 `$i` rule and B's +"execution remains co-addressed" are reconciled, and Arm L is the shape that +reconciliation would admit. + +## B. Access provenance + +| access form | index producer | index consumer | read position decided by | existing classification | +|---|---|---|---|---| +| Direct co-addressed fold | none: every operand is row `i` | `MaskOp::And/Or/Ternlog`, `Pred::*` | the row itself | ADMITTED (B: "execution remains co-addressed"). v1 method C and v2 Arm P execution. | +| Prepared address lens `$i` | `SealedFacetLane::seek_from` (or `bound`) keyed by the row's own key arithmetic (`parent(key)`), witnessed, counted, in preparation | `MaskOp::Gather` via `Filter::Semijoin` / `EqU32Via`, in execution | the row's own declared address | **AMBIGUOUS.** B admits the seek in preparation and not the indirect read in execution. CLAUDE.md 2026-10-21 admits reading through `$i`. EXO-140 / EXO-46 open. | +| Value-directed Gather | a relational value lane (`sources[i]`, an fk, a scattered mask) | `MaskOp::Gather`, `ScatterOrU32` hop | another column's or table's value | FORBIDDEN (#1590; GATHER-DECISION; B "not admissible as a read address"; survival law for produced masks). | + +The machine instruction is the same in rows 2 and 3. Only the producer differs, so +the classification has to key on the producer, not on the opcode. + +## C. Witness completeness + +| invariant | producer | witness type | verifying consumer | status today | negative control | +|---|---|---|---|---|---| +| 1. `$i` derived from the candidate's declared address | probe `parent()` + seek | none | none | **probe-only** | not built: a pointer lane filled from a value lane must be refused | +| 2. seek counted and version-witnessed | `SealedFacetLane::seek_from` | `OrderedLaneWitness` | `SealedFacetLane::validate` | **enforced** for the seek itself (lens + digest + version) | stale witness: `a_prefix_aperture_under_a_stale_witness_sweeps_and_says_why` | +| 3. frame / ClassId / codebook / scope | `OrderedLaneWitness.lens`; `relcomp::Chain` (lab); `r2il::prepare` → `guards.check(frames, now)` | `SemanticLens`, `FrameStore` | `bound` (lens check); `prepare` (no production caller) | **partial**: lens enforced, frame lab-only | v2 case 7 (probe); `LensMismatch` tests | +| 4. source planes resident, not produced `Keep` | caller | none (doc precondition) | none | **missing** (documented obligation on `Filter::Semijoin`) | not built: a produced mask passed as foreign must be refused | +| 5. no intermediate / composed relation | program shape | none | none | **probe-only** (assert no `Gather` in Arm P; Arm L has none to assert) | v2 by construction | +| 6. no mask from one program feeds another | program shape | none | none | **probe-only** | survival-law tests cover scatter only | +| 7. pointer within attested bounds | seek result | none | `Gather` **zero-fallback** | **MISSING, and silent**: out of range reads as `false` | not built: `ib = n_rows` must refuse, today it answers `false` | +| 8. physical plane order = certified order | `seal` sorts its own keys | `OrderedLaneWitness.digest` (keys only) | none for planes | **MISSING** (ISS-WITNESSED-RANGE…) | v2 case 5 unchecked: `(false,0)` vs `(true,1)` | +| 9. deletion / version invalidates pointer + witness | `LanceVersion` in the key witness | key lane only | none for presence planes or `$i` | **MISSING** for presence | v2 case 8 unchecked: stale `(true,1)` | +| 10a. unique keys in the admitted population | `attest_sorted` | none (non-decreasing passes) | `CountKeyRunsU32` checks order for its own terminal | **MISSING** as a lens precondition | v2 case 6 forged: `(true,2)` vs `(true,1)` | +| 10b. edge refines its source by one tier | mint / storage | none | none (no guard in quack, mask-risc or lance-graph-xlog) | **probe-only** | v2 case 7 (`NonRefiningEdge`) | + +A key-order witness is not a presence-version witness. Rows 8 and 9 fail +independently: the key lane can be untouched while a presence plane changes (case 8). + +## D. Minimal operator ruling (draft, for decision; not in force) + +> **ADMISSION B — address-lens clarification.** In execution, a fold may read a +> resident plane of the same table at `$i[j]` only if every one of these holds: +> +> 1. `$i` was produced in preparation, by `SealedFacetLane` seeks keyed by +> arithmetic on row `j`'s own key under the witnessed lens; +> 2. `$i`, the plane and the key lane carry one version, and the fold refuses on +> any mismatch; +> 3. every `$i[j]` is checked to be `< n_rows` before the fold. An out-of-range +> pointer is a refusal, never `Gather`'s zero-fallback; +> 4. the key lane is strictly increasing, so keys are unique; +> 5. the read plane is resident, never a mask a program produced; +> 6. the program has one terminal, and its output feeds no other program. +> +> **Remains forbidden:** +> - an index produced from any value lane (edge endpoints, foreign keys, codebook +> values) or from another table; +> - an index computed from a mask a program produced, or carried between programs; +> - a scattered mask as an intermediate (`ScatterOrU32` survival unchanged); +> - `OutgoingHop` (quarantine unchanged); +> - any recursive or variable-depth use (EXO-73); +> - any Bag multiplicity claim (EXO-108). +> +> This admits no new opcode and no copy. Arm P's prepared presence copy is not +> admitted by this clause. + +## E. Independent falsifier + +Smallest admissibility probe: the v2 fixture, with Arm L's checks moved out of the +probe into the shape the ruling names. + +Every one of these disables must turn the probe red. Each has been measured today as +a silent answer, or is not yet built: + +| # | disable | expected after the ruling | today | +|---|---|---|---| +| 1 | permute a presence plane but not the key lane | refusal | silent false (case 5 variant; key digest does not see it) | +| 2 | delete a presence bit without a version bump | refusal | silent stale (case 8 unchecked) | +| 3 | `ib[j] = n_rows` | refusal | silent `false` (zero-fallback) | +| 4 | duplicate key | refusal at attest | silent count 2 (case 6 forged) | +| 5 | pass a `Keep` output as the foreign plane | refusal | accepted (doc-only precondition) | +| 6 | fill `ib` from an edge-endpoint value lane | refusal (provenance) | accepted | + +Silence twin: the 8 v2 cases stay equal to the nested-loop oracle with every check +on. The admitted-shape parity is Arm L ≡ the direct co-addressed fold of v1 +method C on fixed endpoints. + +Disable 6 is the one that separates the lens from a value-directed gather. Unless it +is refused by something other than the probe's own code, the ruling cannot be +checked. + +## F. Unresolved boundaries + +- **EXO-140:** who classifies `Filter::Semijoin` / `EqU32Via` / `Gather` call sites, + and whether "another relational column" covers a key-derived pointer lane. + Owner: none named. +- **EXO-46:** whether the counted global→focus pointer table may be used in + production execution, and under which witness. It must not be decided as "all + indexed navigation". +- **EXO-114:** per-version order attest. Seek needs total order. Uniqueness is a + separate property no class currently states. +- **EXO-105:** mask-risc frozen. Rule 3 above (refuse out-of-range rather than + zero-fall back) must be met outside mask-risc, by a pre-fold bounds check, + unless the operator unfreezes it. +- **DT64 behaviour admission:** `r2il::prepare` refuses guarded bindings + (`GuardNotExecutable`, `binding.rs:290-291`), and `xlog::bag_count_admitted` + admits only `[GroupCount, GroupCount, MulI64]` (`lib.rs:399`). The smallest + connection is an admitted DO word shape `presence-conjunction → Any` whose + preparation step is this lens. Its falsifier: the same binding refused under a + stale frame (`guards.check`) and under each disable above. ON stays a change + trigger, never the existence test. +- **Out of scope by construction:** + - arbitrary graph edges (no key arithmetic for the parent); + - variable depth and recursion (EXO-73); + - multiple paths to one endpoint and Bag multiplicity (EXO-108); + - SCCs. + +## Answer to the key question + +Yes, in principle. A certified address lens names where each relation's presence +witness already lives, so the fold proves the relationship without it ever being +stored, and no presence bit is copied. Only the pointer table is materialized. + +Today's source does not certify the lens. It certifies the key order of one lane. +Of the eleven rows in table C, five are missing, four are enforced only by the probe, +one is partial, and only the seek itself is enforced. The +interpretive question is unowned. Arm L stays lab-only until the operator rules on +D and an owner takes EXO-140. diff --git a/.claude/probes/2026-11-03-d-bag-fold/original/COADDRESSED-FOLD.md b/.claude/probes/2026-11-03-d-bag-fold/original/COADDRESSED-FOLD.md new file mode 100644 index 000000000..667a8486c --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/original/COADDRESSED-FOLD.md @@ -0,0 +1,147 @@ +# D-BAG-AWARENESS — co-addressed folding hypothesis (read-only, lance-graph `514948203`) + +Question: can `∃B,C. R(A,B) ∧ S(B,C) ∧ T(C,D)` be evaluated as ONE lawful fold, with no +intermediate stored relation, no computed-mask handoff, no value-directed gather and no +tuple materialization? Governance findings from SIDE-BOUNDARY.md are taken as given. + +## Verdict + +**RESTRICTED.** It is one fold only when the composition was already decided by the +ADDRESS at mint time: each hop is "the target key extends the source key by one tier". +Then the three-hop existential is a single key interval on one sealed lane: one +`Cmp::Range` and a `Count`/`Any` terminal that answers from `hi - lo`. For arbitrary +relations it is **BLOCKED**: every route on record needs a gather, a scattered-mask +intermediate, a stored composed relation, #1791 or a pull lane. + +So co-addressing is a LAYOUT answer for refinement relations and a NEW CAPABILITY for +everything else. Laying the path out at one coordinate for arbitrary R, S, T means +storing R∘S∘T, which is the intermediate relation the hypothesis excludes. + +## Findings + +| # | Claim | Class | Evidence | +|---|---|---|---| +| 1 | `fold_ranges` merges `Range` leaves on the SAME `col` that are direct siblings of one `And`. Nothing else: no cross-column binding, no flattening, no merge across `Or`/`Not`. It cannot state `∃B,C`. | PROVEN for its scope; BLOCKED as a chain mechanism | `quack/src/lib.rs:1932-1983` (doc + body); tests `range_fold_tests` 5094ff | +| 2 | A range can come from an ADDRESS without reading a row: `Filter::prefix_facet` turns a `SemanticPrefix` into `Cmp::Range{lo,hi}` under an `OrderedLaneWitness` the sealed lane accepts. Without a witness it falls back to a `MatchU64` sweep and reports the reason. | PROVEN (single lane) | `lib.rs:888-940`; `an_address_prefix_selects_exactly_a_contiguous_trie_subtree` (3869, two-sided halving); `a_witnessed_prefix_is_a_range_on_either_sweep` (4972) | +| 3 | For refinement relations (`B` has prefix `A`, `C` has prefix `B`, `D` has prefix `C`), `R∘S∘T(a)` = the keys on T's D lane with prefix `a` at depth `d+3`. That is one range, one terminal, zero rows read under `Count`/`Any`. This is the canon's "is_ancestor_of = centroid-tree containment" and "path = HEEL+HIP+TWIG". | RESTRICTED; the collapse is NOT VERIFIED (no test chains relations, it follows from prefix semantics only) | items 1-2; OGAR CLAUDE.md tier interpretation | +| 4 | The plane-order precondition of #2 is unenforced: a `Range` is ordinals in the SEALED lane's order, `Pred::Range` reads no lane, `Planes` carry no order identity. | RESTRICTED (open hazard) | `lib.rs:859-885`; `ISSUES.md:753` `ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER` OPEN | +| 5 | The refinement property itself is not checked anywhere. A relation that is lowered as a prefix but contains one non-refining edge gets a wrong answer, silently. It is a property of the mint, with no guard. | NOT VERIFIED (no guard found in quack, mask-risc or the xlog cube) | absence within those three crates only; open negative, read as "no guard located" | +| 6 | Star joins (one shared center: `R(x,c), S(c,z), T(c,q)`) are expressible co-addressed with no gather: per-side fold, `GroupReduce Count` by slot, `And` of slot planes, bag count as a co-addressed dot product. A CHAIN through two join domains is "not built". | LAB ONLY (correctness measured, ms gate FAILED); chains NOT VERIFIED | `entries/2026-10-21-u4-coaddressed-join.md` (Status, Open: "a chain through two domains is not built") | +| 7 | General composition as a gather-free tile product: `C \|= broadcast(row y of A) & spread(bit y of B)`, a `Ternlog 0xF8` Program per coordinate `y`. Gather-free in execution, disable-verified. But it (a) STORES the intermediate `A∘B` before composing with T, (b) feeds a `Keep` mask back as `Plane(0)` 256 times per tile product from a host loop, (c) copies rows into `bcast`/`spread` buffers. So it breaks no-intermediate, is a computed-mask handoff and materializes copies. | LAB ONLY; fails the hypothesis on three counts | `crepe-plan-probe/examples/walk_tile.rs:20-32, 319-405`; `entries/2026-10-21-d-ru-6-tile-walk-probe.md` (1.0-9.3x slower count-only, ADMISSION B not demonstrated) | +| 8 | Arbitrary R, S, T as one fold. | BLOCKED | needs a gather (#1590 ban, ADMISSION B), a scattered intermediate (`ir.rs:329-342` survival law), a pull lane on the target rows (RF-CHAIN alternative, `cypher-mask-lowering-v2.md:291-292`, not ruled), #1791 (not authorized) or OP-14 (open) | +| 9 | Bag counting over the chain (walk counts). Not addressed by any of the above; a range count is a SET count of distinct D keys, never a path multiplicity. | Separate: EXO-108 stays OPEN | cypher-quack gap doc `lib.rs:172-186` ("needs a foreign-value sum") | + +## Invariants the restricted shape needs (every one is load-bearing) + +1. **Refinement at mint.** Each hop's target key extends its source key by exactly one + tier. This is the whole reason the composition collapses. It is unguarded (#5). +2. **One sealed lane, in execution order.** The final range is ordinals in T's sealed + D lane, and the planes must be that lane's rows in that order (#4, open). +3. **Witness currency.** `OrderedLaneWitness` version and digest match the lane; stale + means sweep, never a silent range (`a_prefix_aperture_under_a_stale_witness_sweeps_and_says_why`). +4. **Prefix, not aperture-with-hole.** A care mask with a hole is a predicate and + always sweeps (`an_aperture_with_a_hole_sweeps_even_under_a_witness`). Still one + fold, but no longer O(1). +5. **ClassView scope.** The carving that makes a byte a tier is per classid + (longest-prefix codebook binding). A chain that crosses classids crosses codebooks, + and nothing shows that the prefix reading survives that. NOT VERIFIED. + +## Failure cases + +- A non-refining edge anywhere in R, S or T: wrong answer, silent (#5). +- Planes not in sealed-lane order: unrelated rows selected, silent (#4). +- Hops with different depths per row (variable-length paths): no single depth, so + there is no single prefix width. Expressible only as an `Or` of ranges, which + `fold_ranges` leaves unmerged. +- Any non-hierarchical relation (cross-links, many-to-many, cycles): not an interval; + falls to #8. +- Bag semantics (how many paths): a range counts distinct keys; EXO-108. +- Star shape: lab only (#6); a chain through two domains is not built. + +## Falsifier (proposed, not built) + +On a sealed fixture with three refinement relations, compute `R∘S∘T` existence as one +`prefix_facet` range plus `Count`, and assert it equals the oracle (`dr-math-binding-probe` +`Chain::eval` or a nested loop). Two disables, both required to go red: + +- (a) permute the planes relative to the seal. If the test stays green, #4 is + confirmed as an undetectable hazard. +- (b) inject one non-refining edge into S. The range answer must diverge from the + oracle. That proves invariant 1 is load-bearing, and it shows a guard is needed. + +Silence twin: the same program on a fixture whose S is genuinely a refinement must stay +equal to the oracle at every depth. + +Nothing was implemented, mask-risc was not touched, nothing pushed. + +--- + +# Addendum: the missing logical invariant, one falsifier (closing) + +Probe: `/tmp/claude-0/-home-user/89dae588-85f2-539f-94b2-003b808f478e/scratchpad/cofold/src/main.rs`. +It sits outside the repo and runs the real `lance_graph_quack::lower` and the real mask-risc +`execute_into`. Run it with `cargo +1.99.0 run` (ndarray 0.17.2 needs rustc 1.99). One row +per node, sorted by key. Key layout: `u64 = classid(32) | t1 | t2 | t3 | t4`, 8 bits per tier. +Presence planes `R_in`, `S_in` and `T_in` mark each edge at its child row. + +Two methods: + +- **P, the single-range reduction from the verdict above:** `Count(T_in ∧ prefix(a))`. +- **C, one fold over co-addressed presence for fixed endpoints a..d:** + `Or(R_in@b, S_in@c, T_in@d)` must select exactly 3 rows. `b` and `c` are prefixes of + the query constant `d`, located by their ordinal in the sealed order. That is + representation translation of a constant, never a value read from a row. One + Program, one terminal, no gather, no produced mask, no intermediate. + +## Measured output + +| case | oracle | P | C | +|---|---|---|---| +| 4 valid hierarchy | true | 1 → true | 3/3 → true | +| **0 R(a,b) present, S(b,c) DELETED, T(c,d) present** | false | **1 → true (FALSE POSITIVE)** | 2/3 → false | +| 0b R deleted | false | 1 → true (false positive) | 2/3 → false | +| 0c T deleted | false | 0 → false | 2/3 → false | +| 1 planes stored reversed against the sealed ordinals | true | 1 → true (the sweep reads the lane) | **1/3 → false, no error raised** | +| 2 D lane `[d, d, d2]` | — | range rows = 3, distinct D = 2 | — | +| 3 other classid, same concept hi u16 and same tiers | — | 40-bit prefix (full classid) = 1; 16-bit prefix (concept only) = 2 | — | + +## Classification + +- **P (single-range reduction): FALSIFIED for its intended hierarchy.** Hierarchical + address compatibility is not relational composition. P reads only T's presence, so a + deleted R or S edge is invisible to it by construction. P would be equivalent only + under prefix-closed edge membership: T present at d implies every ancestor link is + present. No contract states that and no guard enforces it, so P is at best + CONDITIONALLY equivalent under an assumed invariant. In practice it is false: a + deletion breaks the invariant. This supersedes finding #3 above: RESTRICTED is + downgraded to FALSIFIED unless prefix-closed membership is enforced. +- **C (direct conjunction over co-addressed presence): CONDITIONALLY equivalent.** It + matches the oracle on all four presence cases, and each of R, S and T is load-bearing + (0, 0b, 0c). It evaluates the relational conjunction itself in one fold. Its open + assumption is plane order (case 1: a silent wrong answer, the same hazard as + `ISS-WITNESSED-RANGE-DOES-NOT-ATTEST-PLANE-ORDER`). Not PROVEN-under-enforced-invariants + until storage exposes the seal's permutation, or execution checks the lane digest. +- **Distinct count (2): FALSIFIED as stated.** `hi − lo` counts lane rows, not distinct + keys. It equals the distinct count only on a key-unique lane. `Agg::CountDistinctOrderedU32` + is the shipped terminal for that (it enforces key order), and only for u32 lanes. + Path multiplicity remains EXO-108. +- **Cross-ClassId (3): RESTRICTED.** The prefix stays inside one classid only when it + covers all 32 classid bits. A concept-only prefix spans app prefixes, and so spans + their codebooks. Tiers alone cannot distinguish the classes. + +## What this does and does not show about the larger idea + +The single-range shortcut fails. The larger idea survives: a fold CAN evaluate the +relational conjunction directly from co-addressed presence, for fixed endpoints, with +none of the excluded mechanisms (method C). + +**Open, not shown:** the existential `∃B,C,D under a`. That needs, at each candidate d, +its ancestors' presence. In a sorted sparse lane the parent's ordinal is not +address-arithmetic, so that read is either a derived prefix-closed plane (forbidden here) +or a value-positioned read (gather). In a DENSE co-addressed level layout (canon +256-cell tiles), `parent(d)` is a fixed shift. There the check is a broadcast lens of +the level-3 S plane over its 256 children. mask-risc has no such lens op, and +`walk_tile` emulates it with copied `spread` buffers. Status: NOT VERIFIED, and it needs +a mask-risc capability (frozen, EXO-105). + +Investigation closed. No repo files changed, mask-risc untouched, nothing pushed. diff --git a/.claude/probes/2026-11-03-d-bag-fold/original/SIDE-BOUNDARY.md b/.claude/probes/2026-11-03-d-bag-fold/original/SIDE-BOUNDARY.md new file mode 100644 index 000000000..df7b97ed4 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/original/SIDE-BOUNDARY.md @@ -0,0 +1,103 @@ +# D-BAG-AWARENESS · the `Cube::side()` boundary — is the native algebra closed over virtual views? + +Read-only. lance-graph `514948203`. Grades: CODE (coordinator read the lines), TEST (executed here), SCOUT, DECISION, INFERENCE. + +## Verdict + +Composition of virtual relations is **not blocked by mathematics**, and an existing lab abstraction already evaluates `(R∘S)∘T` (and every association order) entirely in registers, against an independent oracle, with no relation registration and no tuples — for the **Boolean** semiring only. What stops the production path is three distinct things, each with its own owner: + +1. **Cube scope (implementation):** `Cube::side` admits only a resident relation or a bound scan as a join operand; a `Join` node is `NotASide` (`lance-graph-xlog/src/cube.rs:422-433`). Nothing in the cube's own contract says why; the module never claims closure over views. +2. **An explicit algebra law (mask-risc / Quack):** a scattered mask "is never an intermediate: a follow-on program or fold that consumes it is the forbidden projection → population → projection shape … a filter through the targets is `Pred::EqU32Via` / `MaskOp::Gather` over a RESIDENT plane" (`lance-graph-mask-risc/src/ir.rs:334-342`). Quack restates it as the precondition of `Filter::Semijoin`: "`foreign` names a RESIDENT plane, never a produced one … a `Keep`-then-`Gather` pipeline across two programs is exactly the forbidden shape" (`lance-graph-quack/src/lib.rs:376-386`); cypher-quack enforces it as a refusal ("WHERE with a hop: … Keep→Semijoin is forbidden", `lance-graph-cypher-quack/src/lib.rs:299-300`). +3. **Semiring scope (explicit, lab):** associativity is admitted only for Boolean composition; Bag (ℕ) and three-valued composition are refused (`LawRefusal::NotBooleanSemiring`, `dr-math-binding-probe/tests/relcomp.rs:266-290`), and a chain of ℕ products is a typed refusal "until a word exists" because inputs exceed `i8` after one hop (`.claude/plans/d-dynbag-holographic-bags-v1.md` §7.3). + +## 1. Operations that accept resident sides only + +| operation | operand | evidence | +|---|---|---| +| `Cube::scan` | `RelId` | `cube.rs:367` | +| `Cube::bind` | a `scan` view only (`NotASide` otherwise) | `cube.rs:376-399` | +| `Cube::join` | each side scan or bind; `Join` → `NotASide` | `cube.rs:403-433` | +| `Cube::closure` / `closure_wide` / `refresh_closure` | `RelId` | `cube.rs:669, 719, 810` | +| Quack `Filter::Semijoin` / mask-risc `MaskOp::Gather` | foreign plane must be RESIDENT | quack `lib.rs:376-391`, ir `:277` | +| mask-risc `Planes` | the table's own lanes + caller-supplied input planes | ir `:73` | + +## 2. Operations that accept lazy views, registers, masks or expression handles + +| operation | accepts | evidence | +|---|---|---| +| `Cube::support` / `bag_count` / `materialize_rows` | one lazy `View` (`Node::Join` of two resident sides) | `cube.rs:642-664, 1010` | +| `bag_count_admitted` | an admitted `MethodBinding` + a two-sided `Intake` | `lance-graph-xlog/src/lib.rs:384` | +| codegraph `impact` | closure registers (`WideRows`), folded with `mask_and` / `mask_andnot` / `intersects` | `lance-graph-codegraph/src/query.rs:239-285` (PROD) | +| `relcomp::Chain::eval(&RelExpr)` | n operands bound to methods, any association order, `[u64; 64]` registers | `dr-math-binding-probe/src/relcomp.rs:120-222` (PROBE) | +| `ncompose::pair_counts` | two DR64² tiles → ℕ counts per `(x, z)` (one hop) | `xlog-relcomp-probe/src/ncompose.rs` (PROBE) | +| `dir-rmap-probe` `Composer::compose` | membership × carriers over one slot coordinate; `Law::Count` and `Law::Exists`; seal + `Stale` witness | `dir-rmap-probe/src/compose.rs:1-40, 250-300` (PROBE) | + +## 3. The exact first operation forcing `R∘S` to become physical before `(R∘S)∘T` + +- In the cube: `Cube::join(view_of(R⋈S), …)` → `side()` → `Err(NotASide)` (`cube.rs:432`). The XLOG polyfill's answer is `materialize_rows` (`xlog-cube/src/lib.rs:747`) → `add_relation` (`:206`). +- In the mask-risc/Quack algebra: the step from B-space to C-space. A two-way join's support is computed entirely in its join-key space (two scatters + AND, `cube.rs:642-650`). Moving on to `T` needs the rows of `S` whose `B` is in that mask — a gather through a **produced** mask, which ir.rs:334-342 forbids. The legal route requires the intermediate projection to be a **resident** plane. +- Note: `Cube::support`'s own `mask_and` of two scatter results is already the shape the Nov 2 archaeology flagged as conflicting with this law (decision D3, "Scattered mask in `support`", OPEN). + +## 4. Classification of the restriction + +| restriction | kind | owner | +|---|---|---| +| `NotASide` | implementation scope of the cube (`Side = (rel, bound)`) | `lance-graph-xlog` (Amendment E: it owns the semantics) | +| produced mask never an intermediate | **explicit algebra law** (mask-risc), enforced in Quack and cypher-quack | mask-risc (frozen absent operator decision and evidence, EXO-105); D3 open | +| Gather / EqU32Via call sites | admission, unclassified, **no owner named** | EXO-140 (ADMISSION B) | +| counted global→focus membrane | operator admission | EXO-46 | +| Bag chain (counts feeding a product) | carrier limit (i8), typed refusal | D-DYNBAG §7.3; EXO-108 (degree-product / foreign-value sum, law 6) | +| associativity outside Boolean | explicit law refusal | `admit_composition_assoc` (lab) | +| iterated composition (recursion) | open decision | EXO-73 | + +Not mathematical: composition is associative in every semiring involved (Boolean and ℕ), and `(R∘S)∘T = R∘(S∘T)` is exactly what relcomp's tests and the egglog proof of every five-chain re-association check. + +## 5. Can a DT64-admitted method consume the composition virtually? + +- Two-way: yes, `bag_count_admitted` (admitted `MethodBinding`, `Population::Bag`, steps `GroupCount, GroupCount, MulI64`), any other step shape → `BoundRefusal::Shape` (`lib.rs:395-397`). Callers: probe + tests. +- n-way: the lab `Chain` binds each operand to a method (`BoundDr64 { method: MethodSignature, frame, focus, scope }`, `dr-math-binding-probe/src/lib.rs:217-224`), but `MethodSignature` is a LAB identity listed for removal in the D-DT64-AUTH census (`lance-graph-r2il/dt64-authority-census.tsv`), not a DT64 `MethodRef`. No production DT64 path consumes a chain. + +## 6. One expression, several readings + +| reading | two-way virtual join (cube) | n-way chain (lab `Chain`) | +|---|---|---| +| Boolean existence | `support` | `eval` → rows; `any` | +| Bag count | `bag_count` (degree product) | refused (`NotBooleanSemiring`); ℕ only one hop (`ncompose`) | +| restriction | `bind` (`col == const`) | operand rows are the caller's; validity plane `BoundDr64::validity` | +| further composition | refused (`NotASide`) | yes, any order | +| difference / negation | `mask_andnot` on the result (codegraph, host side) | not a chain operator | + +## 7. Versions, deletions, speculative frames + +- **Version change:** every cube terminal re-checks its frame (`check_frame`, `cube.rs:458`); a lab `Chain` borrows the `FrameStore`, so advancing the store while a chain is alive does not compile (doc test, `relcomp.rs:124-133`), and a stale issue is `StaleFrame`. Virtual results are recomputed, never patched. +- **Deleted support:** a retire is logged and merged on read; the effective lanes cache is dropped (`invalidate`, `cube.rs:577`), so `support`/`bag_count` see the deletion with nothing to retract. Derived registers that *are* cached (codegraph closures) are refreshed or dropped at commit (`graph.rs:903-912`); a closure row is recomputed for every source that could reach the retired edge (`cube.rs:760-762`). +- **Speculative state:** `Cube::stage` checks a batch "without changing it or the table … no version is issued" (`cube.rs:849-855`), and `stage_closure` gives "the closure of relation `rel` as it will be once `staged` is committed … Changes nothing" (`cube.rs:904-908`): a virtual relation evaluated on an uncommitted state. That is the closest existing THOUGHT-over-sealed-WORLD shape; Thought-Git proper is probe-only. + +## 8. Falsifier (proposed, not implemented) + +`R(A,B) ∘ S(B,C) ∘ T(C,D)` → existence and count, against an independent oracle. + +- **Existence:** relcomp `Chain` with three operands and both association orders vs a scalar oracle; assert equality, non-trivial fixtures (neither empty nor full), and `CubeStats.rows_materialized == 0` / no `add_relation` on any cube involved. Part of this already exists: `every_order_computes_the_same_relation` runs 4- and 5-chains over all 5 / 14 orders. **Run here (TEST):** `cargo test -q --manifest-path crates/dr-math-binding-probe/Cargo.toml --test relcomp` → `13 passed; 0 failed` (lance-graph `514948203`; ndarray sibling `b3d7919` via a temporary symlink, removed after the run, as was the probe's `target/`). That includes the chain-vs-oracle, refusal, Boolean-only associativity and egglog five-chain tests. It does NOT include the 3-relation count arm or the cube arm, which do not exist yet. +- **Count:** the same chain under ℕ. Expected today: typed refusal (`NotBooleanSemiring`, D-DYNBAG §7.3). A pass would require a word that does not exist (foreign-value sum / wider product); the falsifier's job is to show the refusal is the only blocker, by checking `(A·B)·C` against enumeration with a wide-integer oracle in the test itself. +- **Through the cube:** the same fixture via `Cube::join(join(..), ..)` must refuse with `NotASide` — that is the boundary under test, and it must stay red until an owner decides otherwise. +- Disable runs: swap two operands of a non-commutative chain; drop the frame check; feed a produced mask into `Semijoin` (Quack must refuse). + +## 9. Does an existing abstraction already resolve it? + +For Boolean existence: **yes, in the lab** — `relcomp::Chain` + `RelExpr` (register-only, frame-bound, method-bound, associativity admitted and egglog-proved). It is not wired to `Cube`, DR³ tiles beyond 64, or DT64 `MethodRef`. For counts: **no** — refused by law and by carrier, and recorded as gaps (EXO-108; cypher-quack "two or more hops: the walk count needs a foreign-value sum"). + +No new expression engine or view type is justified by this evidence: the Boolean chain abstraction exists; what is missing is its admission into the production identity (DT64) and a decision on the produced-mask law (D3 / EXO-140). + +## 10. Governance addendum (board/plan text, re-read by the coordinator) + +These sharpen §4 and change §9's verdict on the lab chain. + +- **The exact question already has a pending contract.** `dr256-where-capstone-v1.md:40-44`: "A `Keep` mask is a legal projection-space mask: a later program may read it as a plane (`Filter::Plane`). A `ScatterOrU32` mask may not (`ir.rs:329-337`). … The #1791 contract proposal (a witnessed derived population) is the only route to reusing a scattered mask, and it is still not authorized." → A virtual intermediate that a second fold may read is precisely a *witnessed derived population*; its owner route is #1791, unauthorized. +- **The lab chain is itself admission-open.** `ISSUES.md:210` (#1896): `relcomp::compose` evaluates XLOG's linear transitive closure on the DR64 register, "Whether `compose` counts as co-addressed under ADMISSION B is not decided here." And `d-onnx-relalg-cap-capstone-1750-v1.md:474` OP-14: "Does the DR64 `compose` lower to mask-risc without `MaskOp::Gather`? … arm B result `NOT EXPRESSIBLE` … report, do not add an opcode | OPEN". So `Chain` proves the mathematics and the oracle equality (13/13 here), but it runs as a host loop (`acc |= b[bit]`, an indexed read per set bit) that mask-risc cannot express without `Gather`, and its admission is undecided. +- **The gather route is closed by ruling.** The gather ban (#1590, 2026-10-16) and ADMISSION B (`entries/2026-10-20-six-decisions.md` §1): no cross-table value-derived positional reads; Semijoin / EqU32Via / Gather call sites unclassified, no owner (EXO-140, `ISSUES.md:122`). `OutgoingHop` (two `Gather` + `ScatterOrU32`) is quarantined behind an off-by-default feature (`STATUS_BOARD.md:426`). +- **The lawful shape the board already names.** `entries/2026-10-16-synergy-map-since-1579.md:56`: "a hop is a coordinate range and chained hops are range intersections (`fold_ranges`, already shipped); a join is a layout that puts the pair at one coordinate." `cypher-mask-lowering-v2.md` RF-CHAIN: a chain of push hops needs "either a mask-risc ruling that admits a scattered mask as a resident plane, with its own law and falsifier, or a pull lane on the target rows." + +**Revised §9.** For `R∘S∘T` there are exactly two lawful routes on record, both unbuilt for this case: +(a) **co-addressed layout** — the join is a layout; chained hops become range intersections over `fold_ranges` (shipped primitive) or pull lanes on target rows; no produced mask is consumed; +(b) **#1791 witnessed derived population** — an intermediate becomes readable by a second program under a witness; unauthorized. +The lab `Chain` is evidence for the semantics, not an admitted route (OP-14 / ADMISSION B open). `Cube::side`'s `NotASide` is therefore consistent with the standing law, not an accident to remove: lifting it to accept a join view would require one of (a) or (b). diff --git a/.claude/probes/2026-11-03-d-bag-fold/original/cofold-Cargo.toml b/.claude/probes/2026-11-03-d-bag-fold/original/cofold-Cargo.toml new file mode 100644 index 000000000..6e0d7ba81 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/original/cofold-Cargo.toml @@ -0,0 +1,17 @@ +[package] +name = "cofold-probe" +version = "0.0.0" +edition = "2021" +publish = false + +[dependencies] +lance-graph-quack = { path = "/home/user/lance-graph/crates/lance-graph-quack" } +lance-graph-mask-risc = { path = "/home/user/lance-graph/crates/lance-graph-mask-risc" } + +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "/home/user/adaworldapi/ndarray" } + +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "/home/user/lance-graph/crates/lance-graph-contract" } + +[workspace] diff --git a/.claude/probes/2026-11-03-d-bag-fold/original/cofold-main.rs b/.claude/probes/2026-11-03-d-bag-fold/original/cofold-main.rs new file mode 100644 index 000000000..e49d45d7c --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/original/cofold-main.rs @@ -0,0 +1,119 @@ +//! D-BAG co-addressed fold falsifier. Lab probe outside the repo; real Quack lowering, +//! real mask-risc executor. Keys: u64 = classid(32) | t1(8) | t2(8) | t3(8) | t4(8). +use lance_graph_mask_risc::{execute_into, materialize_rows, words_for, Foreign, LaneRef, Out, Planes, Scratch, Value}; +use lance_graph_quack::{lower, Agg, Cmp, Col, Filter, Mask, Query}; + +const KEY: Col = Col(0); +const R_IN: Mask = Mask(0); // R(parent(x), x) present, stamped at the child row x +const S_IN: Mask = Mask(1); +const T_IN: Mask = Mask(2); + +fn key(cls: u32, t: [u8; 4]) -> u64 { + (u64::from(cls) << 32) | (u64::from(t[0]) << 24) | (u64::from(t[1]) << 16) | (u64::from(t[2]) << 8) | u64::from(t[3]) +} + +struct Store { + keys: Vec, // row order as STORED (planes are in this order) + planes: Vec>, +} + +fn plane(n: usize, rows: &[usize]) -> Vec { + let mut w = vec![0u64; words_for(n)]; + for &r in rows { w[r / 64] |= 1 << (r % 64); } + w +} + +impl Store { + /// rows sorted by key (the "seal"); `perm` optionally reorders the stored rows afterwards. + fn new(nodes: &[(u64, bool, bool, bool)], perm: Option<&[usize]>) -> (Store, Vec) { + let mut sorted: Vec<_> = nodes.to_vec(); + sorted.sort_by_key(|n| n.0); + let sealed: Vec = sorted.iter().map(|n| n.0).collect(); + let stored: Vec<_> = match perm { Some(p) => p.iter().map(|&i| sorted[i]).collect(), None => sorted }; + let n = stored.len(); + let pick = |f: fn(&(u64, bool, bool, bool)) -> bool| plane(n, &(0..n).filter(|&i| f(&stored[i])).collect::>()); + let planes = vec![pick(|x| x.1), pick(|x| x.2), pick(|x| x.3)]; + (Store { keys: stored.iter().map(|x| x.0).collect(), planes }, sealed) + } + fn rows(&self, f: Filter) -> Vec { + let q = Query { filter: f, agg: Agg::Rows }; + let prog = lower(&q).expect("lowers"); + let n = self.keys.len(); + let lanes = [LaneRef::U64(&self.keys)]; + let masks: Vec<&[u64]> = self.planes.iter().map(|p| p.as_slice()).collect(); + let pl = Planes { n_rows: n, masks: &masks, lanes: &lanes }; + let mut sc = Scratch::for_program(&prog, n).expect("carves"); + let mut out = vec![0u64; words_for(n)]; + match execute_into(&prog, &pl, &Foreign::NONE, &mut sc, Out::Mask(&mut out)).expect("runs") { + Value::Mask(_) => {} + v => panic!("{v:?}"), + } + materialize_rows(&out, n) // test-side readout only + } +} + +/// Ordinal of `k` in the SEALED order: representation translation of a query +/// constant (the address), never a value read from a relation row. +fn ord(sealed: &[u64], k: u64) -> u32 { sealed.binary_search(&k).expect("node exists") as u32 } +fn single(sealed: &[u64], k: u64) -> Filter { let o = ord(sealed, k); Filter::Cmp(KEY, Cmp::Range { lo: o, hi: o + 1 }) } + +/// METHOD P — the single-range reduction: T-lane rows under prefix(a). +fn method_p(s: &Store, a: u64, bits: u32) -> usize { + s.rows(Filter::And(vec![Filter::Plane(T_IN), Filter::prefix_u64(KEY, a, bits)])).len() +} +/// METHOD C — one fold over co-addressed presence, fixed endpoints a..d: +/// Or(R_in@b, S_in@c, T_in@d) must select exactly 3 rows. b, c are d's own +/// prefixes (address arithmetic on the query constant), not values from any row. +fn method_c(s: &Store, sealed: &[u64], b: u64, c: u64, d: u64) -> usize { + s.rows(Filter::Or(vec![ + Filter::And(vec![Filter::Plane(R_IN), single(sealed, b)]), + Filter::And(vec![Filter::Plane(S_IN), single(sealed, c)]), + Filter::And(vec![Filter::Plane(T_IN), single(sealed, d)]), + ])).len() +} + +fn main() { + let k = 0x0905_000A; + let a = key(k, [1, 0, 0, 0]); + let b = key(k, [1, 2, 0, 0]); + let c = key(k, [1, 2, 3, 0]); + let d = key(k, [1, 2, 3, 4]); + let x = key(k, [9, 9, 0, 0]); // a distractor sibling subtree + let prefix_a = 32 + 8; // classid + tier 1 + + // (key, R_in, S_in, T_in) + let valid = [(a, false, false, false), (b, true, false, false), (c, false, true, false), (d, false, false, true), (x, true, false, false)]; + let mut ce = valid; ce[2].2 = false; // S(b,c) DELETED, T(c,d) still present + + let mut rdel = valid; rdel[1].1 = false; + let mut tdel = valid; tdel[3].3 = false; + for (name, nodes) in [("4 valid hierarchy", &valid[..]), ("0 COUNTEREXAMPLE S deleted", &ce[..]), ("0b R deleted", &rdel[..]), ("0c T deleted", &tdel[..])] { + let (s, sealed) = Store::new(nodes, None); + let oracle = nodes.iter().any(|n| n.0 == b && n.1) && nodes.iter().any(|n| n.0 == c && n.2) && nodes.iter().any(|n| n.0 == d && n.3); + let p = method_p(&s, a, prefix_a); + let cnt = method_c(&s, &sealed, b, c, d); + println!("{name}: oracle={oracle} | P(prefix count)={p} -> says {} | C(presence fold)={cnt}/3 -> says {}", p > 0, cnt == 3); + } + + // 1. permuted rows vs the claimed seal (ordinals from sealed order, planes stored reversed) + let perm: Vec = (0..valid.len()).rev().collect(); + let (s, sealed) = Store::new(&valid, Some(&perm)); + let p = method_p(&s, a, prefix_a); + let cnt = method_c(&s, &sealed, b, c, d); + println!("1 permuted planes: oracle=true | P(sweep reads lane)={p} -> {} | C(sealed-order ranges)={cnt}/3 -> {} (no error raised)", p > 0, cnt == 3); + + // 2. duplicate D keys: a T edge table whose D lane holds d twice + let d2 = key(k, [1, 2, 3, 5]); + let t_rows = [d, d, d2]; + let s = Store { keys: t_rows.to_vec(), planes: vec![plane(3, &[]), plane(3, &[]), plane(3, &[0, 1, 2])] }; + let rows = method_p(&s, a, prefix_a); + let mut distinct = t_rows.to_vec(); distinct.dedup(); + println!("2 duplicate D keys: range rows (hi-lo)={rows}, distinct D={}", distinct.len()); + + // 3. cross-ClassId: same concept (hi u16 0x0905), other app prefix, identical tiers + let other = key(0x0905_000B, [1, 2, 3, 4]); + let mut nodes = valid.to_vec(); nodes.push((other, false, false, true)); + let (s, _) = Store::new(&nodes, None); + println!("3 cross-ClassId: prefix incl. full classid ({}b)={} | concept-only prefix (16b)={} | tiers-only key compare would equal: {}", + prefix_a, method_p(&s, a, prefix_a), method_p(&s, a, 16), (other & 0xFFFF_FFFF) == (d & 0xFFFF_FFFF)); +} diff --git a/.claude/probes/2026-11-03-d-bag-fold/probe/Cargo.toml b/.claude/probes/2026-11-03-d-bag-fold/probe/Cargo.toml new file mode 100644 index 000000000..f0ccf3e31 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/probe/Cargo.toml @@ -0,0 +1,21 @@ +# Evidence probe for D-BAG-FOLD. NOT a workspace member, NOT production code. +# Own [workspace] table so the lance-graph root workspace never builds it. +[package] +name = "d-bag-fold-probe" +version = "0.0.0" +edition = "2021" +publish = false + +[dependencies] +lance-graph-quack = { path = "../../../../crates/lance-graph-quack" } +lance-graph-mask-risc = { path = "../../../../crates/lance-graph-mask-risc" } + +# Same convention as the repo root: ndarray is the sibling checkout `../ndarray` +# of the lance-graph repo root. +[patch."https://github.com/AdaWorldAPI/ndarray"] +ndarray = { path = "../../../../../ndarray" } + +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "../../../../crates/lance-graph-contract" } + +[workspace] diff --git a/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v1_prefix_vs_presence.rs b/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v1_prefix_vs_presence.rs new file mode 100644 index 000000000..e49d45d7c --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v1_prefix_vs_presence.rs @@ -0,0 +1,119 @@ +//! D-BAG co-addressed fold falsifier. Lab probe outside the repo; real Quack lowering, +//! real mask-risc executor. Keys: u64 = classid(32) | t1(8) | t2(8) | t3(8) | t4(8). +use lance_graph_mask_risc::{execute_into, materialize_rows, words_for, Foreign, LaneRef, Out, Planes, Scratch, Value}; +use lance_graph_quack::{lower, Agg, Cmp, Col, Filter, Mask, Query}; + +const KEY: Col = Col(0); +const R_IN: Mask = Mask(0); // R(parent(x), x) present, stamped at the child row x +const S_IN: Mask = Mask(1); +const T_IN: Mask = Mask(2); + +fn key(cls: u32, t: [u8; 4]) -> u64 { + (u64::from(cls) << 32) | (u64::from(t[0]) << 24) | (u64::from(t[1]) << 16) | (u64::from(t[2]) << 8) | u64::from(t[3]) +} + +struct Store { + keys: Vec, // row order as STORED (planes are in this order) + planes: Vec>, +} + +fn plane(n: usize, rows: &[usize]) -> Vec { + let mut w = vec![0u64; words_for(n)]; + for &r in rows { w[r / 64] |= 1 << (r % 64); } + w +} + +impl Store { + /// rows sorted by key (the "seal"); `perm` optionally reorders the stored rows afterwards. + fn new(nodes: &[(u64, bool, bool, bool)], perm: Option<&[usize]>) -> (Store, Vec) { + let mut sorted: Vec<_> = nodes.to_vec(); + sorted.sort_by_key(|n| n.0); + let sealed: Vec = sorted.iter().map(|n| n.0).collect(); + let stored: Vec<_> = match perm { Some(p) => p.iter().map(|&i| sorted[i]).collect(), None => sorted }; + let n = stored.len(); + let pick = |f: fn(&(u64, bool, bool, bool)) -> bool| plane(n, &(0..n).filter(|&i| f(&stored[i])).collect::>()); + let planes = vec![pick(|x| x.1), pick(|x| x.2), pick(|x| x.3)]; + (Store { keys: stored.iter().map(|x| x.0).collect(), planes }, sealed) + } + fn rows(&self, f: Filter) -> Vec { + let q = Query { filter: f, agg: Agg::Rows }; + let prog = lower(&q).expect("lowers"); + let n = self.keys.len(); + let lanes = [LaneRef::U64(&self.keys)]; + let masks: Vec<&[u64]> = self.planes.iter().map(|p| p.as_slice()).collect(); + let pl = Planes { n_rows: n, masks: &masks, lanes: &lanes }; + let mut sc = Scratch::for_program(&prog, n).expect("carves"); + let mut out = vec![0u64; words_for(n)]; + match execute_into(&prog, &pl, &Foreign::NONE, &mut sc, Out::Mask(&mut out)).expect("runs") { + Value::Mask(_) => {} + v => panic!("{v:?}"), + } + materialize_rows(&out, n) // test-side readout only + } +} + +/// Ordinal of `k` in the SEALED order: representation translation of a query +/// constant (the address), never a value read from a relation row. +fn ord(sealed: &[u64], k: u64) -> u32 { sealed.binary_search(&k).expect("node exists") as u32 } +fn single(sealed: &[u64], k: u64) -> Filter { let o = ord(sealed, k); Filter::Cmp(KEY, Cmp::Range { lo: o, hi: o + 1 }) } + +/// METHOD P — the single-range reduction: T-lane rows under prefix(a). +fn method_p(s: &Store, a: u64, bits: u32) -> usize { + s.rows(Filter::And(vec![Filter::Plane(T_IN), Filter::prefix_u64(KEY, a, bits)])).len() +} +/// METHOD C — one fold over co-addressed presence, fixed endpoints a..d: +/// Or(R_in@b, S_in@c, T_in@d) must select exactly 3 rows. b, c are d's own +/// prefixes (address arithmetic on the query constant), not values from any row. +fn method_c(s: &Store, sealed: &[u64], b: u64, c: u64, d: u64) -> usize { + s.rows(Filter::Or(vec![ + Filter::And(vec![Filter::Plane(R_IN), single(sealed, b)]), + Filter::And(vec![Filter::Plane(S_IN), single(sealed, c)]), + Filter::And(vec![Filter::Plane(T_IN), single(sealed, d)]), + ])).len() +} + +fn main() { + let k = 0x0905_000A; + let a = key(k, [1, 0, 0, 0]); + let b = key(k, [1, 2, 0, 0]); + let c = key(k, [1, 2, 3, 0]); + let d = key(k, [1, 2, 3, 4]); + let x = key(k, [9, 9, 0, 0]); // a distractor sibling subtree + let prefix_a = 32 + 8; // classid + tier 1 + + // (key, R_in, S_in, T_in) + let valid = [(a, false, false, false), (b, true, false, false), (c, false, true, false), (d, false, false, true), (x, true, false, false)]; + let mut ce = valid; ce[2].2 = false; // S(b,c) DELETED, T(c,d) still present + + let mut rdel = valid; rdel[1].1 = false; + let mut tdel = valid; tdel[3].3 = false; + for (name, nodes) in [("4 valid hierarchy", &valid[..]), ("0 COUNTEREXAMPLE S deleted", &ce[..]), ("0b R deleted", &rdel[..]), ("0c T deleted", &tdel[..])] { + let (s, sealed) = Store::new(nodes, None); + let oracle = nodes.iter().any(|n| n.0 == b && n.1) && nodes.iter().any(|n| n.0 == c && n.2) && nodes.iter().any(|n| n.0 == d && n.3); + let p = method_p(&s, a, prefix_a); + let cnt = method_c(&s, &sealed, b, c, d); + println!("{name}: oracle={oracle} | P(prefix count)={p} -> says {} | C(presence fold)={cnt}/3 -> says {}", p > 0, cnt == 3); + } + + // 1. permuted rows vs the claimed seal (ordinals from sealed order, planes stored reversed) + let perm: Vec = (0..valid.len()).rev().collect(); + let (s, sealed) = Store::new(&valid, Some(&perm)); + let p = method_p(&s, a, prefix_a); + let cnt = method_c(&s, &sealed, b, c, d); + println!("1 permuted planes: oracle=true | P(sweep reads lane)={p} -> {} | C(sealed-order ranges)={cnt}/3 -> {} (no error raised)", p > 0, cnt == 3); + + // 2. duplicate D keys: a T edge table whose D lane holds d twice + let d2 = key(k, [1, 2, 3, 5]); + let t_rows = [d, d, d2]; + let s = Store { keys: t_rows.to_vec(), planes: vec![plane(3, &[]), plane(3, &[]), plane(3, &[0, 1, 2])] }; + let rows = method_p(&s, a, prefix_a); + let mut distinct = t_rows.to_vec(); distinct.dedup(); + println!("2 duplicate D keys: range rows (hi-lo)={rows}, distinct D={}", distinct.len()); + + // 3. cross-ClassId: same concept (hi u16 0x0905), other app prefix, identical tiers + let other = key(0x0905_000B, [1, 2, 3, 4]); + let mut nodes = valid.to_vec(); nodes.push((other, false, false, true)); + let (s, _) = Store::new(&nodes, None); + println!("3 cross-ClassId: prefix incl. full classid ({}b)={} | concept-only prefix (16b)={} | tiers-only key compare would equal: {}", + prefix_a, method_p(&s, a, prefix_a), method_p(&s, a, 16), (other & 0xFFFF_FFFF) == (d & 0xFFFF_FFFF)); +} diff --git a/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v2_witnessed_existential.rs b/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v2_witnessed_existential.rs new file mode 100644 index 000000000..3986c95b4 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/probe/src/bin/v2_witnessed_existential.rs @@ -0,0 +1,279 @@ +//! D-BAG-FOLD v2: `∃d. R(a,b(d)) ∧ S(b(d),c(d)) ∧ T(c(d),d)` without storing any +//! composed relation. Lab probe, outside every workspace. +//! +//! Shape under test (ADMISSION B, `entries/2026-10-20-six-decisions.md` §1): +//! PREPARE counted, version-witnessed, same-table key seeks over an attested +//! sorted key build a co-addressed PROJECTION: for every candidate d, +//! the presence of each relation's edge re-addressed to d's row. +//! Each plane is ONE relation's own presence; nothing composes here. +//! EXECUTE one Quack-lowered mask-risc Program: And(R', S', T') -> Any / Count. +//! Row-aligned ops only. No Gather, no produced mask, no tuple. +//! ORACLE nested loops over the explicit edge sets, independent of the layout. +//! +//! Key: u64 = classid(32) | t1 | t2 | t3 | t4 (8 bits each, 0 = unused tier). +//! The witness is a probe-local mirror of `OrderedLaneWitness` (version, n_rows, +//! order-sensitive FNV digest of the key sequence) plus the version of the +//! presence planes, which no contract type covers today (see README). +use lance_graph_mask_risc::{execute_into, words_for, Foreign, Out, Planes, Scratch, Value}; +use lance_graph_mask_risc::{ForeignPlane as FP, LaneRef}; +use lance_graph_quack::{lower, Agg, Cmp, Col, Filter, ForeignPlane, Mask, Query}; +use std::collections::BTreeSet; + +type Key = u64; +type Edges = BTreeSet<(Key, Key)>; + +fn key(cls: u32, t: [u8; 4]) -> Key { + (u64::from(cls) << 32) | (u64::from(t[0]) << 24) | (u64::from(t[1]) << 16) | (u64::from(t[2]) << 8) | u64::from(t[3]) +} +fn depth(k: Key) -> usize { (0..4).take_while(|i| (k >> (24 - 8 * i)) & 0xFF != 0).count() } +/// Address arithmetic on a key's own bits; stays inside its classid. +fn parent(k: Key) -> Option { + let d = depth(k); + (d >= 2).then(|| k & !(0xFFu64 << (24 - 8 * (d - 1)))) +} + +#[derive(Debug, PartialEq)] +enum Refuse { StaleVersion, OrderNotAttested, DuplicateKey, NonRefiningEdge((Key, Key)), UnknownNode(Key) } + +#[derive(Clone, Copy, Debug, PartialEq)] +struct Witness { key_version: u64, presence_version: u64, n_rows: usize, digest: u64 } + +fn fnv(keys: &[Key]) -> u64 { + let mut h: u64 = 0xcbf2_9ce4_8422_2325; + for k in keys { for b in k.to_le_bytes() { h ^= u64::from(b); h = h.wrapping_mul(0x0100_0000_01b3); } } + h +} + +/// One table: a node lane plus three presence planes stamped at the CHILD row. +struct Store { key_version: u64, presence_version: u64, keys: Vec, pres: [Vec; 3] } + +impl Store { + /// Builds the layout from explicit edges. An edge the layout cannot place + /// (child is not a one-tier extension of its source) is refused, never dropped. + fn build(nodes: &[Key], rels: [&Edges; 3]) -> Result { + let mut keys = nodes.to_vec(); + keys.sort_unstable(); + let mut pres = [vec![false; keys.len()], vec![false; keys.len()], vec![false; keys.len()]]; + for (r, edges) in rels.iter().enumerate() { + for &(x, y) in edges.iter() { + if parent(y) != Some(x) { return Err(Refuse::NonRefiningEdge((x, y))); } + let i = keys.binary_search(&y).map_err(|_| Refuse::UnknownNode(y))?; + pres[r][i] = true; + } + } + Ok(Store { key_version: 1, presence_version: 1, keys, pres }) + } + /// The seal. Refuses a key lane that is not strictly increasing. + fn seal(&self) -> Result { + if self.keys.windows(2).any(|w| w[0] >= w[1]) { + return Err(if self.keys.windows(2).any(|w| w[0] == w[1]) { Refuse::DuplicateKey } else { Refuse::OrderNotAttested }); + } + Ok(Witness { key_version: self.key_version, presence_version: self.presence_version, n_rows: self.keys.len(), digest: fnv(&self.keys) }) + } +} + +/// Prepared co-addressed projection over the candidate population. +struct Prepared { witness: Witness, planes: [Vec; 3], n: usize, seeks: usize } + +/// `checked = false` skips every witness check: the deliberately broken arm. +fn prepare(s: &Store, w: &Witness, a: Key, checked: bool) -> Result { + if checked { + if w.key_version != s.key_version || w.presence_version != s.presence_version || w.n_rows != s.keys.len() { return Err(Refuse::StaleVersion); } + if fnv(&s.keys) != w.digest { return Err(Refuse::OrderNotAttested); } + } + // Candidate range: depth-4 keys under prefix(a), located by two seeks on the + // attested sorted key (a's subtree is [a, a + 2^(8·(4-depth(a))) ) in key order). + let span = 1u64 << (8 * (4 - depth(a))); + let lo = s.keys.partition_point(|&k| k < a); + let hi = s.keys.partition_point(|&k| k < a + span); + let mut seeks = 2; + let cand: Vec = (lo..hi).filter(|&i| depth(s.keys[i]) == 4).collect(); + let n = cand.len(); + let mut planes = [vec![0u64; words_for(n)], vec![0u64; words_for(n)], vec![0u64; words_for(n)]]; + let mut set = |p: usize, j: usize| planes[p][j / 64] |= 1 << (j % 64); + for (j, &di) in cand.iter().enumerate() { + let d = s.keys[di]; + let c = parent(d).expect("depth 4"); + let b = parent(c).expect("depth 3"); + let find = |k: Key| s.keys.binary_search(&k).ok(); // same-table seek, keyed by d's own address + seeks += 2; + if s.pres[2][di] { set(2, j); } + if let Some(ci) = find(c) { if s.pres[1][ci] { set(1, j); } } + if let Some(bi) = find(b) { if s.pres[0][bi] && parent(b) == Some(a) { set(0, j); } } + } + Ok(Prepared { witness: *w, planes, n, seeks }) +} + +/// One Program. Refuses a projection prepared at another version of the store. +fn execute(s: &Store, p: &Prepared, checked: bool) -> Result<(bool, u64), Refuse> { + if checked && (p.witness.key_version != s.key_version || p.witness.presence_version != s.presence_version) { return Err(Refuse::StaleVersion); } + let f = Filter::And(vec![Filter::Plane(Mask(0)), Filter::Plane(Mask(1)), Filter::Plane(Mask(2))]); + let run = |agg| { + let prog = lower(&Query { filter: f.clone(), agg }).expect("lowers"); + assert!(!format!("{prog:?}").contains("Gather"), "no Gather in the program"); + let masks: Vec<&[u64]> = p.planes.iter().map(|v| v.as_slice()).collect(); + let pl = Planes { n_rows: p.n, masks: &masks, lanes: &[] }; + let mut sc = Scratch::for_program(&prog, p.n.max(1)).expect("carves"); + execute_into(&prog, &pl, &Foreign::NONE, &mut sc, Out::None).expect("runs") + }; + let any = match run(Agg::Any) { Value::Bool(b) => b, v => panic!("{v:?}") }; + let count = match run(Agg::Count) { Value::Count(c) => c as u64, v => panic!("{v:?}") }; + Ok((any, count)) +} + +fn pack(v: &[bool]) -> Vec { + let mut w = vec![0u64; words_for(v.len())]; + for (i, &b) in v.iter().enumerate() { if b { w[i / 64] |= 1 << (i % 64); } } + w +} + +/// ARM L (zero-copy form). Preparation builds only pointer tables `$i` +/// (`ib[row]` = row of grandparent link b, `ic[row]` = row of parent link c), +/// by same-table seeks keyed by the row's own address. Execution is ONE Program +/// over the node lane: Range(subtree a) ∧ T_in ∧ Semijoin(ib → R_in) ∧ +/// Semijoin(ic → S_in). R_in and S_in are the table's own RESIDENT planes, read +/// in place through `$i` by `MaskOp::Gather`. No presence bit is copied. +fn execute_lens(s: &Store, w: &Witness, a: Key) -> Result<(bool, u64), Refuse> { + if w.key_version != s.key_version || w.presence_version != s.presence_version || w.n_rows != s.keys.len() { return Err(Refuse::StaleVersion); } + if fnv(&s.keys) != w.digest { return Err(Refuse::OrderNotAttested); } + let n = s.keys.len(); + let span = 1u64 << (8 * (4 - depth(a))); + let lo = s.keys.partition_point(|&k| k < a) as u32; + let hi = s.keys.partition_point(|&k| k < a + span) as u32; + let find = |k: Option| k.and_then(|k| s.keys.binary_search(&k).ok()); + // A row with no such ancestor points at row 0 (the lane minimum); the + // Range restricts to a's subtree, whose depth-4 rows always have both ancestors. + let ib: Vec = s.keys.iter().map(|&k| find(parent(k).and_then(parent)).unwrap_or(0) as u32).collect(); + let ic: Vec = s.keys.iter().map(|&k| find(parent(k)).unwrap_or(0) as u32).collect(); + let t = pack(&s.pres[2]); + let (r, sp) = (pack(&s.pres[0]), pack(&s.pres[1])); + let f = Filter::And(vec![ + Filter::Cmp(Col(0), Cmp::Range { lo, hi }), + Filter::Plane(Mask(0)), + Filter::Semijoin { fk: Col(0), foreign: ForeignPlane(0) }, + Filter::Semijoin { fk: Col(1), foreign: ForeignPlane(1) }, + ]); + let lanes = [LaneRef::U32(&ib), LaneRef::U32(&ic)]; + let fps = [FP { words: &r, rows: n }, FP { words: &sp, rows: n }]; + let foreign = lance_graph_mask_risc::Foreign { planes: &fps, lanes: &[] }; + let masks: Vec<&[u64]> = vec![&t]; + let pl = Planes { n_rows: n, masks: &masks, lanes: &lanes }; + let run = |agg| { + let prog = lower(&Query { filter: f.clone(), agg }).expect("lowers"); + let mut sc = Scratch::for_program(&prog, n).expect("carves"); + execute_into(&prog, &pl, &foreign, &mut sc, Out::None).expect("runs") + }; + let any = match run(Agg::Any) { Value::Bool(b) => b, v => panic!("{v:?}") }; + let count = match run(Agg::Count) { Value::Count(c) => c as u64, v => panic!("{v:?}") }; + Ok((any, count)) +} + +/// Independent oracle: nested loops over the three edge sets. +fn oracle(a: Key, r: &Edges, s: &Edges, t: &Edges) -> (bool, u64) { + let mut ds = BTreeSet::new(); + for &(x, b) in r { if x != a { continue; } + for &(b2, c) in s { if b2 != b { continue; } + for &(c2, d) in t { if c2 == c { ds.insert(d); } } } } + (!ds.is_empty(), ds.len() as u64) +} +/// The single-range reduction from v1, for contrast: T presence under prefix(a). +fn prefix_only(st: &Store, a: Key) -> bool { + let span = 1u64 << (8 * (4 - depth(a))); + st.keys.iter().zip(&st.pres[2]).any(|(&k, &p)| p && k >= a && k < a + span) +} + +fn main() { + let k = 0x0905_000A; + let a = key(k, [1, 0, 0, 0]); + let (b1, b2) = (key(k, [1, 2, 0, 0]), key(k, [1, 7, 0, 0])); + let (c1, c2, c3) = (key(k, [1, 2, 3, 0]), key(k, [1, 7, 3, 0]), key(k, [1, 2, 8, 0])); + let (d1, d2, d3) = (key(k, [1, 2, 3, 4]), key(k, [1, 7, 3, 4]), key(k, [1, 2, 8, 4])); + let nodes = vec![a, b1, b2, c1, c2, c3, d1, d2, d3]; + let e = |v: &[(Key, Key)]| v.iter().copied().collect::(); + let mut fails = 0; + let mut check = |name: &str, got: Result<(bool, u64), Refuse>, want: (bool, u64)| { + let ok = got.as_ref().map(|g| *g == want).unwrap_or(false); + if !ok { fails += 1; } + println!("{:<58} got={got:?} oracle={want:?} {}", name, if ok { "OK" } else { "MISMATCH" }); + }; + let run = |nodes: &[Key], r: &Edges, s: &Edges, t: &Edges| -> Result<(bool, u64), Refuse> { + let st = Store::build(nodes, [r, s, t])?; + let w = st.seal()?; + let p = prepare(&st, &w, a, true)?; + let v2 = execute(&st, &p, true)?; + let lens = execute_lens(&st, &w, a)?; + assert_eq!(v2, lens, "arm L (Gather through $i) disagrees with arm P (projection)"); + Ok(v2) + }; + + // 1. all three edges present (single path) + let (r, s, t) = (e(&[(a, b1)]), e(&[(b1, c1)]), e(&[(c1, d1)])); + check("1 all present", run(&nodes, &r, &s, &t), oracle(a, &r, &s, &t)); + // 2. each edge deleted independently; prefix-only shown for contrast + for (name, rr, ss, tt) in [("2a R deleted", e(&[]), s.clone(), t.clone()), ("2b S deleted", r.clone(), e(&[]), t.clone()), ("2c T deleted", r.clone(), s.clone(), e(&[]))] { + let st = Store::build(&nodes, [&rr, &ss, &tt]).unwrap(); + check(&format!("{name} (prefix-only says {})", prefix_only(&st, a)), run(&nodes, &rr, &ss, &tt), oracle(a, &rr, &ss, &tt)); + } + // 3. three candidates, exactly one valid; decoys are broken at different hops + // d2: S(b2,c2), T(c2,d2) but no R(a,b2). d3: R(a,b1), T(c3,d3) but no S(b1,c3). + let (r, s, t) = (e(&[(a, b1)]), e(&[(b1, c1), (b2, c2)]), e(&[(c1, d1), (c2, d2), (c3, d3)])); + check("3 three candidates, one valid", run(&nodes, &r, &s, &t), oracle(a, &r, &s, &t)); + // 4. same candidates, none valid + let (r4, s4) = (e(&[(a, b1)]), e(&[(b2, c2)])); + let st = Store::build(&nodes, [&r4, &s4, &t]).unwrap(); + check(&format!("4 three candidates, none valid (prefix-only says {})", prefix_only(&st, a)), run(&nodes, &r4, &s4, &t), oracle(a, &r4, &s4, &t)); + // two valid, to show Count is the number of distinct valid d (keys are unique) + let r5 = e(&[(a, b1), (a, b2)]); + check("3b three candidates, two valid", run(&nodes, &r5, &s, &t), oracle(a, &r5, &s, &t)); + + // 5. permuted physical order against the witness + let mut st = Store::build(&nodes, [&r, &s, &t]).unwrap(); + let w = st.seal().unwrap(); + st.keys.reverse(); + for p in st.pres.iter_mut() { p.reverse(); } + println!("5 permuted rows, checked: prepare = {:?}", prepare(&st, &w, a, true).err()); + let unchecked = prepare(&st, &w, a, false).and_then(|p| execute(&st, &p, false)); + println!("5 permuted rows, UNCHECKED arm: {unchecked:?} vs oracle {:?} (silent wrong answer when the check is removed)", oracle(a, &r, &s, &t)); + println!("5 sealing a permuted lane: {:?}", st.seal().err()); + + // 6. duplicate terminal key + let mut dup = nodes.clone(); dup.push(d1); + let mut st = Store::build(&dup, [&r, &s, &t]).unwrap(); + // a T table holding the edge (c1,d1) twice stamps BOTH rows of d1 + for i in 0..st.keys.len() { if st.keys[i] == d1 { st.pres[2][i] = true; } } + println!("6 duplicate d1, seal: {:?}", st.seal().err()); + let w_forged = Witness { key_version: 1, presence_version: 1, n_rows: st.keys.len(), digest: fnv(&st.keys) }; + let unchecked = prepare(&st, &w_forged, a, true).and_then(|p| execute(&st, &p, false)); + println!("6 duplicate d1, forged witness: {unchecked:?} vs oracle {:?} (Count = rows, not distinct d)", oracle(a, &r, &s, &t)); + + // 7. cross-ClassId: another class (same concept hi u16, other app lo u16), same tiers, + // a fully valid chain of its own; plus an edge crossing the class boundary. + let k2 = 0x0905_000B; + let (a2, b2x, c2x, d2x) = (key(k2, [1, 0, 0, 0]), key(k2, [1, 2, 0, 0]), key(k2, [1, 2, 3, 0]), key(k2, [1, 2, 3, 4])); + let mut n7 = nodes.clone(); n7.extend([a2, b2x, c2x, d2x]); + let (r7, s7, t7) = (e(&[(a, b1), (a2, b2x)]), e(&[(b2x, c2x)]), e(&[(c2x, d2x)])); + // class K has R only; class K2 has a full chain. Query under a (class K) must say false. + check("7 other class holds the only valid chain", run(&n7, &r7, &s7, &t7), oracle(a, &r7, &s7, &t7)); + let cross = e(&[(b1, c2x)]); + println!("7 edge crossing the classid boundary: build = {:?}", Store::build(&n7, [&r7, &cross, &t7]).err().map(|_| "refused (NonRefiningEdge)")); + + // 8. version change after preparation: S(b1,c1) deleted at presence_version 2 + let mut st = Store::build(&nodes, [&r, &s, &t]).unwrap(); + let w = st.seal().unwrap(); + let p = prepare(&st, &w, a, true).unwrap(); + println!("8 before change: {:?}", execute(&st, &p, true)); + let ci = st.keys.binary_search(&c1).unwrap(); + st.pres[1][ci] = false; st.presence_version = 2; + println!("8 after S(b1,c1) deleted, stale projection, checked: {:?}", execute(&st, &p, true).err()); + println!("8 stale projection, UNCHECKED: {:?} (silent stale true)", execute(&st, &p, false)); + let w2 = st.seal().unwrap(); + let p2 = prepare(&st, &w2, a, true).unwrap(); + let s8 = e(&[(b2, c2)]); + check("8 re-prepared at version 2", execute(&st, &p2, true), oracle(a, &r, &s8, &t)); + println!("8 arm L under the stale witness: {:?}", execute_lens(&st, &w, a).err()); + check("8 arm L at version 2", execute_lens(&st, &w2, a), oracle(a, &r, &s8, &t)); + println!("preparation seeks for case 8: {}", p2.seeks); + + println!("\n{} mismatches against the oracle", fails); + std::process::exit(i32::from(fails != 0)); +}