From 4f667ef2d43202c8315ce03037b4b3b3eff8a9da Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 13:58:31 +0000 Subject: [PATCH 1/6] board: #1884 merged (PR_ARC, LATEST_STATE, D-XLOG-NATIVE-5/6 shipped) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/board/LATEST_STATE.md | 6 ++++++ .claude/board/PR_ARC_INVENTORY.md | 11 +++++++++++ .claude/board/STATUS_BOARD.md | 4 ++-- 3 files changed, 19 insertions(+), 2 deletions(-) diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index b0bbdd076..3ba773792 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,9 @@ +## 2026-10-31 — main after #1884 (merged `d3c2a29`) + +- `xlog-relcomp-probe` executes its admitted chain on `ndarray::simd`, binds the bag count through `lance-graph-dt64`, and pins the Epi5 reading of XLOG results. Lab only. +- Plans D-SOC-FENCE and D-DYNBAG are on main, plan only. +- No contract type changed. + ## 2026-10-31 — main after #1880 (merged `4d677ba`) - Mistaber makor citations are addressed through `deepnsm-v2` `hydrate` (`NiblePath`, no classid). `deepnsm-v2` is the grammar and language intake arm. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index 596116d7b..70d036658 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,3 +1,14 @@ +## 2026-10-31 — lance-graph PR #1884 (merged `d3c2a29`, branch `ccr-85acaff0-oszq40`, head `1e85104`) — xlog-relcomp-probe: ndarray::simd execution, binding through lance-graph-dt64, Epi5 reading; plans D-SOC-FENCE and D-DYNBAG + +- **Added:** + - `xlog-relcomp-probe/src/native.rs`: the admitted two-atom chain's support and bag count on `ndarray::simd` (`eq_u32_to_mask`, `mask_scatter_or_u32`, `mask_and`, `masked_group_count_u32` ×2, `checked_binary_i64(Mul)`), Y axis on `dt64::dr::LocalMap` (up to 256); `admit_count` for XLOG's `count` rule. + - `tests/dto_binding.rs` rewritten onto `BindStore`, `dt64::dr::FrameStore` and `MethodRef`; `tests/epi5_reading.rs` (an XLOG base fact reads `Direct × Open`, a composed edge `IndirectKnown × Open`). + - `facts()` drops repeated base tuples (XLOG's loader treats a base relation as a set; Codex P2). + - Plans: `d-xlog-native-v1.md` Amendments A and B, `d-soc-fence-v1.md` (one place per concern, CI fence), `d-dynbag-holographic-bags-v1.md` (DR{dynamic bag}, semiring readings, PostgreSQL endgame). +- **Locked:** none in production; lab probe only. +- **Known defect, carried to main:** `native.rs` calls `ndarray::simd` fold words directly, bypassing Quack and mask-risc. It is the first named D-SOC-FENCE violation, to be fixed by D-DYNBAG-0. +- **Confidence:** probe suites green locally (gate_b 18, litho 12 + 1 ignored, dto_binding 4, epi5_reading 4, gate_g 3); 8 disable runs red. The probe has no CI line. Workspace CI green on the head. + ## 2026-10-31 — lance-graph PR #1880 (merged `4d677ba`, branch `claude/mistaber-ruff-harvest-9gtxd4`, head `7b8d4b6`) — D-MIST-NATIVE-1b: makor citations addressed via deepnsm-v2 hydrate, no classid - **Added:** `mistaber-kripke-probe/fixtures/makor.tsv`, 141 real `makor` citations from the compiled Mistaber ontology. `src/makor.rs` lays them over a Yoreh De'ah outline (siman = chapter, seif = verse) with `deepnsm-v2` `hydrate`: each citation is a `Spo` at its seif's `NiblePath`, with no classid, `promote`, key or `NodeRow`. `tests/makor.rs` adds 8 tests. CI paths now include `deepnsm-v2` and its dependencies. Plan §10; entry `2026-10-31-d-mist-native-1b-makor-hydrate.md`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 934091086..8a46fdce7 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -50,8 +50,8 @@ Plan: `.claude/plans/d-soc-fence-v1.md`. Plan only; nothing runs yet. | D-XLOG-NATIVE-2 | test masked_group_count_u32 keyed by one table's column against the RIR walk, with the out-of-universe refusal | Queued | N2, N3 | | D-XLOG-NATIVE-3 | ask the ndarray / mask-risc owners for a native home for the many-to-many join (fixture: Gate B) | Queued | owner decision | | D-XLOG-NATIVE-4 | create `crates/lance-graph-xlog` (ndarray only, no `xlog-*` dep, no plan type) once plan §4 holds | Queued | N1–N5 | -| D-XLOG-NATIVE-6 | probe executes on `ndarray::simd` (`src/native.rs`): support via `eq_u32_to_mask` / `mask_scatter_or_u32` / `mask_and`, bag count via `masked_group_count_u32` ×2 + `checked_binary_i64`; DR `LocalMap` up to 256; register path kept as differential (plan Amendment B) | In PR | lab probe | -| D-XLOG-NATIVE-5 | bag count bound through the production bind store (`lance-graph-dt64` + `dt64::dr`), polyfill words by position; Epi5 reading of XLOG results pinned (plan Amendment A) | In PR | lab execution only | +| D-XLOG-NATIVE-6 | probe executes on `ndarray::simd` (`src/native.rs`): support via `eq_u32_to_mask` / `mask_scatter_or_u32` / `mask_and`, bag count via `masked_group_count_u32` ×2 + `checked_binary_i64`; DR `LocalMap` up to 256; register path kept as differential (plan Amendment B) | Shipped (#1884) | lab probe; layering fix is D-DYNBAG-0 | +| D-XLOG-NATIVE-5 | bag count bound through the production bind store (`lance-graph-dt64` + `dt64::dr`), polyfill words by position; Epi5 reading of XLOG results pinned (plan Amendment A) | Shipped (#1884) | lab execution only | ## D-LITHO — the photolithography contract (2026-10-30) From f3b2cfe8c7da8e3070f98f8cf459e542503b5fab Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 14:13:02 +0000 Subject: [PATCH 2/6] plans: D-DYNBAG-0 actual vs target ownership and data flow; D-XLOG-NATIVE Amendment C MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit D-DYNBAG §17 adopts the operator's architecture (Quack/relalg describe, mask-risc evaluates, ndarray::simd computes under mask-risc), diagrams the merged #1884 flow against the target, lists the exact existing APIs, labels seven missing integrations, and states the D-DYNBAG-0 gates. D-XLOG-NATIVE's direct-ndarray rule is struck in place and superseded by Amendment C. Docs only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/plans/d-dynbag-holographic-bags-v1.md | 98 ++++++++++++++++++- .claude/plans/d-xlog-native-v1.md | 14 ++- 2 files changed, 109 insertions(+), 3 deletions(-) diff --git a/.claude/plans/d-dynbag-holographic-bags-v1.md b/.claude/plans/d-dynbag-holographic-bags-v1.md index 4c850722b..e9fc805b9 100644 --- a/.claude/plans/d-dynbag-holographic-bags-v1.md +++ b/.claude/plans/d-dynbag-holographic-bags-v1.md @@ -366,7 +366,7 @@ From PR #1884, `tests/epi5_reading.rs`: | Wave | D-id | Work | Gate (falsifier) | Depends on | Tier | |---|---|---|---|---|---| -| 0 | D-DYNBAG-0 | Fix PR #1884's layering: XLOG intake as lanes (sets), support and bag count through Quack → mask-risc, oracles by folds, cost probe gains native and Quack columns | all existing Gate B / litho tests green; register differential unchanged; disable runs red; `native.rs` no longer calls `ndarray::simd` fold words | operator go-ahead on #1884 | Opus orchestrates; Sonnet implements from spec | +| 0 | D-DYNBAG-0 | (§17) Fix PR #1884's layering: XLOG intake as lanes (sets), support and bag count through Quack → mask-risc, oracles by folds, cost probe gains native and Quack columns | all existing Gate B / litho tests green; register differential unchanged; disable runs red; `native.rs` no longer calls `ndarray::simd` fold words | operator go-ahead on #1884 | Opus orchestrates; Sonnet implements from spec | | 1 | D-DYNBAG-1 | ℕ-compose probe: `matmul_i8_to_i32` over two DR64² tiles for `p(X, Z)` | §7.5: equality with both oracles, B projection equals `relcomp::compose`, disable runs red; timed vs `relcomp::compose` in ns | D-DYNBAG-0 | Sonnet; Opus reviews | | 2 | D-DYNBAG-2 | Semiring parameter in relalg's `Rel` (B, ℕ) and Quack's surface; typed refusal for unsupported (op, K) | B/ℕ projection property holds for every admitted op; an unsupported pair is refused, never a fallback to B | D-DYNBAG-1 | relalg / Quack owners | | 3 | D-DYNBAG-3 | Missing ℕ words, backend-first: masked select over i64, elementwise min, truncated minus, i64 compare-to-mask, i64 masked sum; and, if §7.4 measures it necessary, a bit-packed i1 × i1 → i32 product | each word with can-fire and can-stay-silent tests in its owner crate | D-DYNBAG-2 | mask-risc / ndarray owners | @@ -440,3 +440,99 @@ This plan only notes where it would sit: the "edge" row of §8, and the PostgreS - `crates/xlog-relcomp-probe` (PR #1884): native path, binding, Epi5 tests. - `crates/lance-graph-cypher-quack`: the SQL probe's template. - EXO-50: the membrane reference note (2026-10-31). + +--- + +## 17. D-DYNBAG-0: adopted architecture, actual vs target (2026-10-31, before coding) + +**DECISION (operator, 2026-10-31).** XLOG consumes tuples as a logical polyfill over DT64-addressed relational projections. Quack/RelAlg describe the relation; mask-risc evaluates the bound operations; `ndarray::simd` computes only under mask-risc. A tuple is a coordinate binding, never a stored row. XLOG owns no tuple evaluator and builds no intermediate tuple collection. No new architecture, planner, runtime, tensor store or row engine is introduced: the work is wiring what exists, and labelling what does not. + +### 17.1 Ownership + +| concern | owner | XLOG's part | +|---|---|---| +| description | XLOG RIR (frontend), then Quack `Query` / `GroupBy` | admits a shape; never executes | +| addressing | `lance_graph_dt64::dr`: `LocalMap`, `FrameStore`, `Guards`; one map per axis | none | +| binding | `lance_graph_dt64`: `BindStore`, `MethodBinding`, `MethodRef`, `AlgebraRef`, `ClassView` | names its lens | +| semiring | the bound method (B support vs ℕ multiplicity) | never the frame | +| evaluation | `lance-graph-mask-risc::execute_into` | none | +| compute | `ndarray::simd`, called by mask-risc | none | + +### 17.2 Actual data flow (PR #1884, as merged) + +``` +XLOG compile ─► RIR ─► admit / admit_count (ok) + │ +facts() ─► Vec<(u32,u32)> (dedup'd) ← owned tuples after intake + │ +LocalMap::prepare per call ← rebuilt per query + │ +native.rs ─► ndarray::simd directly ← D-SOC-FENCE fold-evaluator violation + eq_u32_to_mask, mask_scatter_or_u32, mask_and, + masked_group_count_u32, checked_binary_i64 + │ +ids() / nonzero() ─► addressed result + +BindStore + FrameStore: only in tests/dto_binding.rs, never on the path above. +``` + +The admission and the computation are separate. A binding is resolved in a test and then ignored; the counts are computed whether or not it admits. Replacing the ndarray calls one-for-one would keep that separation, so D-DYNBAG-0 closes the chain rather than swapping calls. + +### 17.3 Target data flow + +``` +XLOG compile ─► RIR ─► admit / admit_count + │ + ├─► intake (one named function): facts → u32 lanes, once; sets + │ + ├─► dr: LocalMap for Y prepared once, digest sealed into the frame; + │ FrameStore::check / Guards::check before every reuse + │ + ├─► BindStore::resolve → admit(MethodRef) → MethodBinding + │ (Population, AlgebraRef words: GROUP_COUNT, MUL_I64) + │ + ├─► Quack description, per side (left r(X,Y), right s(Y,Z)): + │ Filter: Cmp(free, Eq x) | Plane(live) + │ Agg::GroupReduce { key: GroupAddr::Local(y_local), agg: GroupAgg::Count } + │ lower(&Query) → Program + │ + ├─► mask-risc execute_into(Program, Planes{lanes}, Foreign::none, Scratch, Out::I64(n_y)) + │ → deg_l[y], deg_r[y] (each is the demanded result of its program) + │ + ├─► combine (MISSING-3 below): ℕ = deg_l × deg_r ; B = (deg_l>0) ∧ (deg_r>0) + │ + └─► addressed result: LocalMap::global over nonzero slots, at the boundary only +``` + +### 17.4 Existing APIs used (read 2026-10-31) + +- **Quack** (`lance-graph-quack/src/lib.rs`): `Filter::{Cmp, Plane, EqU32Via, Semijoin, And, Or, Not}`; `Query { filter, agg }`; `Agg::GroupReduce { key: GroupAddr::Local(Col), agg: GroupAgg::Count }` (one program, `Out::I64` sized to the group universe, key past it dropped); `Agg::ScatterOrU32 { fk, out_rows }` (legal only as the demanded result); `lower`, `lower_group_by_semantic`. +- **Quack bind** (`bind.rs`): `trait Binder { table, live, field, code }`, `Draft::bind` (single table). Implementations exist in `lance-graph-glove-parity` (`CanonicalBinder`), `lance-graph-sap`, `lance-graph-dir-sim`, `lance-graph-report` tests; none is backed by `BindStore`. +- **mask-risc** (`ir.rs`, `exec.rs`): `execute_into(&Program, &Planes, &Foreign, &mut Scratch, Out)`, `Planes { n_rows, masks, lanes }`, `Terminal::GroupReduce` / `GroupFold::Count`, `Terminal::ScatterOrU32`. +- **DT64** (`lib.rs`): `BindStore::{route, resolve, resolve_algebra, admit}`, `MethodBinding`, `MethodRef`, `AlgebraRef { lens, word }`. +- **DR** (`dr.rs`): `LocalMap::{prepare, local, global, len, lookups, digest}` (lookups counted; digest is the frame's coordinates revision), `FrameStore::{seal, advance, check}`, `Guards::check`. +- **relalg**: `Rel` / `Measure` / `Query` are single-table; `join_body::is_alpha_acyclic` is the only join-body tool. + +### 17.5 Missing integrations (labelled; none worked around) + +| id | missing | owner | D-DYNBAG-0 behaviour | +|---|---|---|---| +| MISSING-1 | `AlgebraRef` word → Quack `Agg`/`GroupAgg` mapping (the polyfill lens's words have no Quack reading) | DT64 + Quack | a probe-local table over the two words in use, refusing any other word; filed for the owner | +| MISSING-2 | a `Binder` backed by `BindStore` + `ClassView` (existing binders are catalogue-specific) | Quack bind + DT64 | reconcile, not add: decide whether `CanonicalBinder`'s shape is the template. No new catalogue in the probe | +| MISSING-3 | a post-terminal combine of two group sinks: i64 elementwise multiply and i64 compare-to-mask (both listed in Wave 3) | mask-risc / ndarray | `checked_binary_i64` stays the one direct call (D-SOC-FENCE §6), TRACKED; B is derived from the two degree sinks, never from a scatter mask fed to a second program | +| MISSING-4 | two-relation support as ONE description: relalg has no join IR; `Filter::Semijoin` needs a resident `ForeignPlane`, never a lowered output | relalg / Quack | not built; the per-side degree route above is exact for the admitted chain only | +| MISSING-5 | a reuse cache for prepared `LocalMap`s keyed by frame | DT64 `dr` | the probe holds one map and checks the frame per query; a test asserts `lookups` does not grow with query count beyond intake | +| MISSING-6 | `p(X, Z)` and n-ary witnesses (ℕ-compose) | Wave 1 | refused with a typed refusal; `q(Y)` support is never offered as proof of `p(X, Z)` | +| MISSING-7 | multi-tile global → (tile, local) map | Wave 4 | width 64 or 256; past it, `MapRefusal` | + +### 17.6 Acceptance gates for D-DYNBAG-0 + +1. One connected chain in a test: compile → admit → resolve/bind → Quack `Query` → `lower` → `execute_into` → addressed result. Unbinding the method (retract the route) refuses the computation, not just the test. +2. No owned tuples after intake: `facts()` output is consumed by the intake function only. +3. No unguarded global → local rebuild per query (MISSING-5 test). +4. Support and multiplicity distinct, with XLOG's exact `count` semantics; base relations as sets. +5. Gate B, bag-count, stale-frame and disable tests stay meaningful: each disable run (drop the frame check, drop the admission, swap Count for a scatter) goes red. +6. `q(Y)` is never reported for `p(X, Z)` (MISSING-6 refusal tested). +7. `native.rs` names no `ndarray::simd` fold word; only `checked_binary_i64` remains, listed as TRACKED. + +**REVISIT WHEN:** MISSING-3 or MISSING-4 lands in its owner crate; the TRACKED call is then deleted. diff --git a/.claude/plans/d-xlog-native-v1.md b/.claude/plans/d-xlog-native-v1.md index 2d2088f09..f043ae97f 100644 --- a/.claude/plans/d-xlog-native-v1.md +++ b/.claude/plans/d-xlog-native-v1.md @@ -1,10 +1,10 @@ # D-XLOG-NATIVE — XLOG plan vocabulary over the ndarray::simd polyfill (the algebra under lance-graph-onnx) -**Status:** PROPOSED. The crosswalk (§2) is docs only; it decides whether a `lance-graph-xlog` crate, wired like `lance-graph-onnx`, is worth creating. Amendment A (2026-10-31) records what moved since: the binding now names mask-risc's op vocabulary, the probe binds through the production bind store, and XLOG results have a stated Epi5 reading. +**Status:** PROPOSED. Amendment C supersedes the direct-ndarray rule. The crosswalk (§2) is docs only; it decides whether a `lance-graph-xlog` crate, wired like `lance-graph-onnx`, is worth creating. Amendment A (2026-10-31) records what moved since: the binding now names mask-risc's op vocabulary, the probe binds through the production bind store, and XLOG results have a stated Epi5 reading. **Date:** 2026-10-30. **Parent work:** D-XLOG-DR64-0 (#1857), D-LITHO-1 (#1861, #1864; D-LITHO is now folded into D-DT64-6 Amendment A). **Precedent:** [D-ONNX-NATIVE](d-onnx-native-v1.md). -**Rule.** XLOG is a vocabulary over the same algebra `lance-graph-onnx` sits on: the `ndarray::simd` polyfill. The path would be `XLOG plan node → existing ndarray::simd function` and nothing else, exactly as `ONNX operator → existing native function`. Where both vocabularies name the same operation (`And`, `Or`, `Not`, `Greater`, `Equal`, masked sums), both facades alias the same native symbol. There is no plan type, interpreter, fixpoint engine, mask-risc program or graph database. The lowering from XLOG's compiled plan stays in `crates/xlog-relcomp-probe`, outside the workspace, and becomes the crate's caller and oracle harness. mask-risc and relalg are cross-checks, as they are for `lance-graph-onnx` (dev-dependencies only). +**Rule.** ⊘ *Superseded 2026-10-31 by the D-SOC-FENCE ownership rule (Amendment C).* The original text read: "XLOG is a vocabulary over the same algebra `lance-graph-onnx` sits on: the `ndarray::simd` polyfill. The path would be `XLOG plan node → existing ndarray::simd function` and nothing else … mask-risc and relalg are cross-checks." That made `ndarray::simd` the call path for folds, which bypasses the one evaluator. **Current rule:** XLOG plan nodes are described in Quack/relalg, evaluated by `lance-graph-mask-risc`, and computed by `ndarray::simd` only under mask-risc. Elementwise (non-fold) aliases shared with `lance-graph-onnx` stay `ndarray::simd` symbols, as D-ONNX-NATIVE sanctions. **Scope boundaries:** - The crate depends on `ndarray` only, on the coordinate `lance-graph-onnx` uses. It takes no `xlog-*` dependency: `xlog-core` pins arrow 60, the lance stack arrow 58 (D-XLOG-DR64-1). Only lane slices, constants and masks cross, never XLOG or arrow values. @@ -142,6 +142,8 @@ Status of every row: **name-checked, not tested.** Each native target is a funct ## Amendment B (2026-10-31): execution on the `ndarray::simd` polyfill +> ⊘ **Superseded by Amendment C** on ownership: the table below records what `native.rs` does today, not the architecture. Its fold calls are a D-SOC-FENCE `fold-evaluator` violation, fixed by D-DYNBAG-0. + Operator: refactor XLOG onto the `ndarray::simd` polyfill (CubeCL as an intermediary only in the worst case). It was not needed: every function below is on the `ndarray::simd` facade, including `checked_binary_i64` (ndarray #407, merged and read in the checkout). `crates/xlog-relcomp-probe/src/native.rs` is now the probe's execution path for the admitted two-atom chain. Each step is one function: @@ -163,3 +165,11 @@ Effect on §2: - The two-atom many-to-many chain projected onto Y (support and bag count) now has a native home. Its rows move from NATIVE to INLINE: they are tested against both oracles. - Still NATIVE: a many-to-many join whose answer keeps both ends (X, Z), and chains of more than two atoms. - §4 condition 2 holds for the projected chain only. + +## Amendment C (2026-10-31): the D-SOC-FENCE ownership rule + +- **Folds** (group count, scatter, masked sums, popcount terminals) are described in Quack (`Query`, `GroupBy`, `Agg::GroupReduce`) or relalg and evaluated by mask-risc `execute_into`. `ndarray::simd` is never called for them from XLOG or its probe. +- **Elementwise aliases** (`mask_and/or/not`, `*_to_mask`) shared with `lance-graph-onnx` remain `ndarray::simd` symbols, the D-ONNX-NATIVE sanction. +- **No mask-risc word yet:** `checked_binary_i64` is the one direct call, TRACKED in D-SOC-FENCE until mask-risc gains an i64 combine (D-DYNBAG §17.5 MISSING-3). +- In §2, the `ndarray::simd` column is what mask-risc calls, not what XLOG calls. The NATIVE / INLINE categories now mean "has a mask-risc program", not "has an ndarray function". +- The work is D-DYNBAG-0 (`d-dynbag-holographic-bags-v1.md` §17). From a495017d08dbdb417b28025712a289f3a7e5d489 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 14:20:12 +0000 Subject: [PATCH 3/6] plans: cross-frontend projection crosswalk; common ownership rule in D-SOC-FENCE MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit D-DYNBAG §18 maps XLOG, ONNX/Tract, SQL/R2IL, egglog-MLIR, Codegraph and Scallop onto the five projections (coordinate, field, method, relational, consumer), classifies each capability, and records the gaps per owning crate. Main finding: nothing executes a DT64 MethodBinding; only the Tract probe dispatches through the binding it resolved, via its own registry. D-SOC-FENCE's bind-store row now covers method admission and gains a procedure-reading row and the common ownership rule. Docs only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- ...-31-cross-frontend-projection-crosswalk.md | 14 +++++ .claude/board/entries/README.md | 3 +- .claude/plans/d-dynbag-holographic-bags-v1.md | 61 +++++++++++++++++++ .claude/plans/d-soc-fence-v1.md | 7 ++- 4 files changed, 82 insertions(+), 3 deletions(-) create mode 100644 .claude/board/entries/2026-10-31-cross-frontend-projection-crosswalk.md diff --git a/.claude/board/entries/2026-10-31-cross-frontend-projection-crosswalk.md b/.claude/board/entries/2026-10-31-cross-frontend-projection-crosswalk.md new file mode 100644 index 000000000..cc6e4b554 --- /dev/null +++ b/.claude/board/entries/2026-10-31-cross-frontend-projection-crosswalk.md @@ -0,0 +1,14 @@ +# D-DYNBAG-X: cross-frontend projection crosswalk + +**Date 2026-10-31 · D-id D-DYNBAG-0 (scope) · Status OPEN (map, no code)** + +Read-only harvest of XLOG, ONNX/Tract, SQL/R2IL, egglog-MLIR, Codegraph (rust-analyzer + Charon) and Scallop against DT64, ClassView, Quack, relalg, R2IL and mask-risc. The full table and the gaps are in `.claude/plans/d-dynbag-holographic-bags-v1.md` §18. + +- **MEASURED (read):** no component executes a DT64 `MethodBinding`; `BindStore::admit`/`resolve` have no production caller (`lance-graph-dt64/src/lib.rs:796`; only dt64 tests and `xlog-relcomp-probe/tests/dto_binding.rs`). +- **MEASURED (read):** the Tract probe is the one place where the resolved binding is the one dispatched (`tract-harvest-probe/src/plan.rs:116-128,171,204`), but through its own `Registry`, not `BindStore`. +- **MEASURED (read):** `admit` checks method id, `SigRev` and guard witness only (`lib.rs:796-822`); it cannot refuse on an effect or on POSSIBLE/UNKNOWN evidence. +- **MEASURED (read):** "project" means columns (XLOG RIR), rows kept as a mask (relalg `Keep`, Quack `Rows`) and field labels (`ClassView::project`, 64-bit `FieldMask` only; `Resolved::field_view`, `WideFieldMask`). Three owners' words, not one operation. +- **OPEN:** the executor seam that turns an admitted binding into the Quack/R2IL description that runs (§18.4 X1); without it no two consumers share a binding contract. +- **Address idea `[DD:CC][F###]`:** the concept half is domain:concept, not domain:app (`ogar_codebook.rs:179`); the low half is the app lens (`0x0000`–`0x000C`, V3 marker `0x1000`). A per-method slot in the classid would be a second spelling of `MethodRef { class, MethodId }`, which DT64 rules out ("a codebook item never gets a classid", `lib.rs:51-65`). PROPOSED only; OGAR decision. + +**Fruit:** X2 (effect/evidence refusal in `admit`) is small, owned by DT64, and unblocks the codegraph fixture. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index dd2adb759..c70ff8f9e 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -523 entries, 2026-08-06 .. 2026-10-31. +524 entries, 2026-08-06 .. 2026-10-31. | date | entry id | finding | file | |---|---|---|---| @@ -36,6 +36,7 @@ exactly one of them, never both. | 2026-10-31 | `D-SAG-6-1-CHECKLIST` | | [2026-10-31-d-sag-6-1-checklist.md](2026-10-31-d-sag-6-1-checklist.md) | | 2026-10-31 | `D-MIST-NATIVE-1b` | | [2026-10-31-d-mist-native-1b-makor-hydrate.md](2026-10-31-d-mist-native-1b-makor-hydrate.md) | | 2026-10-31 | `D-DT64-6-DR` | | [2026-10-31-d-dt64-6-dr-addressing-module.md](2026-10-31-d-dt64-6-dr-addressing-module.md) | +| 2026-10-31 | `D-DYNBAG-X` | | [2026-10-31-cross-frontend-projection-crosswalk.md](2026-10-31-cross-frontend-projection-crosswalk.md) | | 2026-10-30 | `D-XLOG-NATIVE-0` | | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) | | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) | | 2026-10-30 | `D-TRACT-SHAPE-1` | | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) | diff --git a/.claude/plans/d-dynbag-holographic-bags-v1.md b/.claude/plans/d-dynbag-holographic-bags-v1.md index e9fc805b9..ffa5441b6 100644 --- a/.claude/plans/d-dynbag-holographic-bags-v1.md +++ b/.claude/plans/d-dynbag-holographic-bags-v1.md @@ -536,3 +536,64 @@ XLOG compile ─► RIR ─► admit / admit_count 7. `native.rs` names no `ndarray::simd` fold word; only `checked_binary_i64` remains, listed as TRACKED. **REVISIT WHEN:** MISSING-3 or MISSING-4 lands in its owner crate; the TRACKED call is then deleted. + +--- + +## 18. Cross-frontend projection crosswalk (2026-10-31, before coding) + +**DECISION (operator).** XLOG is the first consumer of the projection capability, not its owner. A consumer requests a typed, versioned projection over existing DR/DT64 coordinates and method bindings. A tuple is a coordinate binding; a method is a typed behavioural binding. No frontend owns a projection runtime. Quack (relational description) and R2IL (`FoldDialect` procedures) are both legitimate surfaces, both converging on mask-risc. BindStore resolves and validates; it never executes. + +Evidence: four read-only harvests at `d3c2a29`/`f3b2cfe`, each claim cited file:line and spot-checked by the orchestrator. Classes: VERIFIED (production + test), LAB, PROPOSED (plan only), MISSING (nothing found in the searched space). + +### 18.1 The five projections are distinct, and "project" means three things + +| projection | existing carrier | class | +|---|---|---| +| coordinate (global → local, revision) | `dt64::dr::{LocalMap, FrameStore, Guards}`; `LocalMap::digest` as the frame's coordinates revision | VERIFIED | +| field (meaning × mask → labels/lanes) | `ClassView::project(class, FieldMask)` (`class_view.rs:1079`, **64-bit `FieldMask` only**); `dt64::Resolved::field_view(&WideFieldMask)` (labels, no values) | VERIFIED; no lane borrowing from either | +| method (MethodRef → ON/WHEN/DO, algebra words) | `dt64::MethodBinding { on, when, reads, effects, population, truth, demand }` (`lib.rs:197`); `admit` (`:796`) checks id, `SigRev`, guard witness | VERIFIED as description; **no executor of a `MethodBinding` exists anywhere**; `admit`/`resolve` have no production caller | +| relational (select/join/fold/group/witness) | Quack `Query`/`GroupBy`/`Agg`; relalg `Rel` (single-table, `Measure::Keep`); R2IL `FoldDialect` + `procs` | VERIFIED; no join IR (relalg), semijoin needs resident foreign planes (Quack) | +| consumer (XLOG bindings, SQL results, codegraph relations, R2IL procedures, MLIR exprs) | per frontend, below | mostly LAB / PROPOSED | + +"Project" is not one operation: XLOG `RirNode::Project` selects/computes **columns** (and runs on GPU in xlog-runtime); relalg `Measure::Keep` and Quack `Agg::Rows` keep **rows** as a mask; `ClassView::project` and `field_view` select **fields as labels**. No meaning selects methods (that is `Resolved::methods_on`). Do not unify them under a "Project" opcode. + +### 18.2 Crosswalk + +| frontend / source IR | projection entrypoint | identity & revision witness | method resolution | lowering | execution owner | output demand | present → gap | +|---|---|---|---|---|---|---|---| +| **XLOG** (`RirNode`) | `admit` / `admit_count` (structural match) | `LocalMap` digest (LAB); BindStore route log in a test only | `BindStore::admit(MethodRef::of(XLOG, …))` in `dto_binding.rs` — **asserted, never drives execution** | none: `native.rs` calls `ndarray::simd` | ndarray direct (D-SOC-FENCE violation) | support mask, per-Y count | LAB → §17: binding must select the Quack program that runs | +| **ONNX / Tract** (protobuf + Tract facts) | `plan::resolve` → `Plan::run` | `FrameRevisions{source sha256, relation_map=registry.revision(), coordinates}`, checked every run (`plan.rs:57-68,171`) | own `Registry` (ON × WHEN(K3) × DO), selected binding **is** the one dispatched (`plan.rs:116-128,204`) | cold shape fold; one native fn per node | `lance-graph-onnx` aliases of `ndarray::simd`/`hpc` | every value by name | LAB precedent for binding-drives-execution; gap: own registry not DT64 `BindStore`, lab lens `0x0F00` in Geo domain | +| **SQL / PostgreSQL** | Quack `lower`/`lower_fused`, `Filter::sql_where` (K3); `lance_graph_r2il::procs` | MISSING in code (D-QSP proposes a version-attested codebook witness) | `procs` are Rust functions; ClassView method ordinal PROPOSED | R2IL → `MaskOp` → mask-risc `Program` | mask-risc `execute_into` (`r2il lib.rs:716`) | scalar per fold, `GROUP_SUM`, `KEEP` | VERIFIED fold path; gaps: executable `PROC_DEF` (OPEN in OGAR), bag/join carrier, nullable arithmetic, frontends not yet routed through procs | +| **egglog-MLIR / DialEgg** | `egglog-r2il-probe::lower_and_run` (scalar) | egglog proof self-check + independent i128 oracle | `RuleId` = law × `Arith` domain (refuses reassociation for Checked/Ieee) | `INT_MULT` over empty planes | FoldDialect scalar arm | one scalar | LAB; external `mlir-egglog` admits rewrites with no evidence (float reassociation unconditional) and runs via LLVM — not a model to adopt | +| **Codegraph** (rust-analyzer HIR + Charon LLBC) | `sag-ra-probe` → `llbc_calls.py` → `span_join.py` → `project_rows.py` (TSV) | moniker (candidate only) + FNV body digest + `RESOLVE` move witness → `sid-N`; revision caller-recorded | rust-analyzer impls; Charon `Fun`/`Clause`/`Dyn`/`TraitImpl` | none | none (R2IL `FoldDialect` not connected) | `ProposedMethod` (PROPOSED, no type) | LAB; WITNESSED/POSSIBLE/UNKNOWN preserved in rows; gaps listed in 18.4 | +| **Scallop** (Datalog + provenance tags) | none in lance-graph | none | `Provenance` impls (unit, boolean, natural, top-k proofs) | none | Scallop's interpreter | tagged relations | external VERIFIED; natural's `saturated` is always `true`, so recursive bag counts stop early | + +### 18.3 What two consumers already share (and what they do not) + +- **Shared and real:** DR coordinates + frame witness (XLOG uses `LocalMap`; Tract uses its own `FrameStore` revisions) and mask-risc as the evaluator (SQL via R2IL; XLOG once §17 lands). +- **Not shared:** method binding. Tract executes through its own registry; DT64 `BindStore` is wired to nothing that executes. The integration proof the operator asks for is therefore not yet possible with existing code: no two consumers obtain their executed method through the same `BindStore`. + +### 18.4 Gaps for owning crates (recorded, not built in D-DYNBAG-0) + +| id | gap | owner | +|---|---|---| +| X1 | an executor seam: something that takes an admitted `MethodBinding` and selects the existing Quack/R2IL description that runs (Tract's `plan.rs:204` is the precedent shape) | DT64 + Quack/R2IL; decision needed | +| X2 | `admit` checks id, `SigRev`, guard only; it cannot refuse on an effect or on POSSIBLE/UNKNOWN evidence, so an effectful codegraph method would be admitted if registered | DT64 | +| X3 | `ClassView::project` takes `FieldMask` (64); DT64 uses `WideFieldMask` | contract | +| X4 | no Quack `Binder` backed by `BindStore`/`ClassView` (8 impls, none) | Quack bind + DT64 | +| X5 | method identity: `MethodId` is registrant-chosen; codegraph `sid-N` → `MethodId` mint does not exist and needs owner approval; impl/closure identity open | DT64 + OGAR (O2 in the logic-compiler RFC) | +| X6 | codegraph revision witness inside the tools (workspace digest, features, target) | sag-ra-probe | +| X7 | executable `PROC_DEF`/`PROC_CALL` | OGAR `ogar-loco` | +| X8 | Tract registry → DT64 `BindStore`; lab lens `0x0F00` minted in OGAR | tract probe + OGAR | +| X9 | bag/support carrier across procedures (SQL D-QSP-2, XLOG ℕ) | relalg/Quack/mask-risc (Wave 2-3) | + +### 18.5 Integration proof, restated against what exists + +- **A (XLOG):** buildable inside D-DYNBAG-0 once the executed Quack program is selected by the admitted binding (§17.6 gate 1). Oracles: scalar enumeration and the DR64 register. +- **B (Codegraph):** buildable today only as a hand-fed fixture: rows from the D-SAG-6-2 board entry, pinned `sag_fixture` functions, `tests/law.rs` as the behaviour oracle. Admitting the pure `count_below` and refusing `count_with_tally` / `count_div` / dyn requires X2 (effect/evidence refusal), which does not exist. Wiring to live rust-analyzer/Charon output needs X5, X6. +- **SQL bag fixture:** duplicated base tuples must keep multiplicity; XLOG's intake dedups by design (sets). Needs X9; not in D-DYNBAG-0. +- **Not claimed:** that A and B share one binding contract today. They do only after X1 and X2. + +### 18.6 Scope of D-DYNBAG-0 (unchanged, bounded to XLOG) + +§17 stands. One addition: the binding that selects the executed program is DT64's `MethodBinding` (its `effects` name the polyfill words), and the selection mechanism follows Tract's precedent (resolve once, dispatch through the resolved entry, frame-checked per run) without copying Tract's registry. If X1 needs a type in DT64, D-DYNBAG-0 stops and asks rather than adding it in the probe. diff --git a/.claude/plans/d-soc-fence-v1.md b/.claude/plans/d-soc-fence-v1.md index 979b99902..8f6efc24c 100644 --- a/.claude/plans/d-soc-fence-v1.md +++ b/.claude/plans/d-soc-fence-v1.md @@ -69,12 +69,15 @@ Each row below is a proposal. Wave 0 confirms or corrects it by reading the cite | `query-surface` | `lance-graph-quack` builds Programs and never evaluates them | — | Quack crate docs ("may build a Program and must never evaluate one") | | `selection-description` | `lance-graph-relalg` | — | addendum 8 ("relalg describes") | | `dr-addressing` | `lance_graph_dt64::dr` (`FrameStore`, `Guards`, `Focus`, `Scope`, `LocalMap`, `ClassAxis`) | `dt64::dr` | addendum 12. The `dr-math-binding-probe` copies are `TRACKED` duplicates | -| `bind-store` | `lance-graph-dt64` (`BindStore`, `MethodBinding`, the route log) | `BindStore` | D-DT64-6 D4/D5 | +| `bind-store` | `lance-graph-dt64` (`BindStore`, `MethodBinding`, `MethodRef`, `admit`, the route log); resolves and validates, never executes | `BindStore`; no frontend registry of its own (Tract's `Registry` is `TRACKED` until D-DYNBAG §18 X8) | D-DT64-6 D4/D5; D-DYNBAG §18 | | `method-identity` | **OPEN** (`MethodRef` vs `MethodSignature` vs `MethodKey`, EXO-50) | — | listed with no owner; not enforced until decided | | `classid-split` | `ogar_codebook::{classid_concept, classid_canon, …}`, `dt64::view_class` | those functions; no bit math on a composed classid | `/v3-audit` item 1 | | `epi5-field` | `CausalEdge64::{epistemic_raw5, with_epistemic_raw5}`, `Epi5Declarations::project_state5` | those; no shifts or masks on bits 59..63 elsewhere | `epistemic_state5.rs` module docs | | `presence` | the class's `FieldMask` / `WideFieldMask` | presence bits; never a sentinel value inside a field | `class_view.rs` C2 | | `tuple-template` | relalg (describes) and Quack (surface); the pointer table is `dt64::dr::LocalMap`; one named intake per frontend | descriptions over lanes; no owned row (`Vec<(..)>`, row structs) after intake, in production, probes or oracles | lance-graph CLAUDE.md P0 ("a tuple is a zero-copy fold template"); D-DYNBAG §2, §8 | +| `procedure-reading` | `lance-graph-r2il` (`FoldDialect`, `procs`) over `ogar-loco` control flow | R2IL calls; no frontend opcode loop | `lance-graph-r2il` crate docs | + +**Common ownership rule (2026-10-31, D-DYNBAG §18).** Every frontend (XLOG, SQL, Codegraph, ONNX/Tract, egglog/MLIR, Scallop) is a consumer: it owns its parser and its admission of shapes, nothing else. Coordinates belong to `dt64::dr`; meaning to `ClassView`; method identity and admission to `BindStore`; relational description to Quack/relalg; procedure description to R2IL; evaluation to mask-risc; compute to `ndarray::simd` under mask-risc. A frontend that keeps its own registry, coordinate map, evaluator or tuple store is a `TRACKED` violation with a D-id, never a sanctioned exception. "Project" is not a concern: column selection (XLOG RIR), row keeping (relalg/Quack) and field labelling (ClassView/DT64) are three owners' words and are not merged. `/v3-audit` keeps its own checks. Its item 1 moves into the mapping file, so the rule is written in one place, and the command reads it from there. @@ -109,7 +112,7 @@ Nothing in Waves 0–2 changes production code. Wave 3 is the only wave that tou ## 5. Decisions needed before Wave 0 -1. **Which concerns are in.** The ten rows of §2 are proposals; `method-identity` stays unenforced until EXO-50 decides. +1. **Which concerns are in.** The twelve rows of §2 are proposals; `method-identity` stays unenforced until EXO-50 decides. 2. **Whether `ndarray::hpc::*` imports are violations** in lance-graph (thinking-engine 32, bgz-tensor 13, planner 10). The lance-graph-java and tesseract-rs rule says never; whether lance-graph follows it has not been ruled. 3. **Whether lab probes are in scope.** Proposed: yes, as `TRACKED` entries, so a probe's shortcut is visible rather than exempt. 4. **Tool language.** Proposed: Rust with `syn`, to resolve paths. A Python regex tool would repeat the measured G11 failure. From c322642784cb300123663c6056979aa83d0cc47b Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 14:47:03 +0000 Subject: [PATCH 4/6] =?UTF-8?q?plans:=20D-DYNBAG=20=C2=A719=20polyfill-com?= =?UTF-8?q?position=20invariant=20and=20the=20Wave=200=20boundary?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Records the operator invariant (polyfills are bound recombinations of algebra atoms, not hardcoded sequences), maps it onto existing DT64 APIs, shows R2IL's fold lens is the existing backend-owned atom-to-operator mapping (FnIndex is u8 like AlgebraRef.word), and stops D-DYNBAG-0 at three missing backend capabilities: binding-to-FoldDialect lowering, a keyed-count fold word, and a group-sink combine. Docs only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/plans/d-dynbag-holographic-bags-v1.md | 43 +++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/.claude/plans/d-dynbag-holographic-bags-v1.md b/.claude/plans/d-dynbag-holographic-bags-v1.md index ffa5441b6..dc4ca27c0 100644 --- a/.claude/plans/d-dynbag-holographic-bags-v1.md +++ b/.claude/plans/d-dynbag-holographic-bags-v1.md @@ -597,3 +597,46 @@ Evidence: four read-only harvests at `d3c2a29`/`f3b2cfe`, each claim cited file: ### 18.6 Scope of D-DYNBAG-0 (unchanged, bounded to XLOG) §17 stands. One addition: the binding that selects the executed program is DT64's `MethodBinding` (its `effects` name the polyfill words), and the selection mechanism follows Tract's precedent (resolve once, dispatch through the resolved entry, frame-checked per run) without copying Tract's registry. If X1 needs a type in DT64, D-DYNBAG-0 stops and asks rather than adding it in the probe. + +--- + +## 19. Polyfills are composed, not hardcoded (2026-10-31, operator decision before coding) + +**Invariant.** Class patterns and bound methods are reusable. Polyfills are compositions of existing algebra atoms, never hardcoded sequences. A `WideFieldMask` selects behaviour words inside a declared basis; DR projects their versioned coordinate surface; DT64 gives each consumer its semantic alias and method recipe; Quack or R2IL lowers the admitted description; mask-risc executes. A frontend never owns a fixed execution sequence that bypasses `MethodBinding`. A backend-owned mapping from an admitted atom to an existing operator is legitimate. + +### 19.1 What already provides the composition (read 2026-10-31) + +| need | existing API (`lance-graph-dt64/src/lib.rs`) | +|---|---| +| declare a lens of reusable, classid-free words with arities | `BindStore::declare_algebra` (`:628`), `arity` (`:654`) | +| read a lens's words through its `ClassView` | `BindStore::resolve_algebra` (`:665`) → `Resolved::field_view` | +| which words a consumer class uses, as a mask over the lens | `BindStore::words_used` (`:683`) | +| which classes reuse a word | `BindStore::users_of` (`:700`) | +| the recipe: ordered DO steps, each a word with ordered operands | `MethodBinding::effects` (`:197`), `Effect { target, algebra, args }`, `Arg::{Field, Const}` | +| select behaviour by field | `Resolved::methods_on` (`:451`), `methods_touching` (`:520`) | + +### 19.2 The backend-owned atom → operator mapping already exists, under R2IL + +- `ogar_loco::FnIndex` is a `u8` (`OGAR crates/ogar-loco/src/lib.rs:380`), the same width as `AlgebraRef.word`. +- The R2IL fold reading `CONCEPT_R2IL_FOLD = 0xC401` (`ogar-r2il/src/lib.rs:545`, PROVISIONAL, not in `CODEBOOK`) is a lens whose word positions are R2IL opcodes. +- `lance_graph_r2il::FoldDialect::call` maps each opcode to a mask-risc program (`lance-graph-r2il/src/lib.rs:770`), and `ogar_loco`'s interpreter runs call sequences. + +So `AlgebraRef { lens: compose(0xC401, 0), word: FnIndex.0 }` names an atom the backend already knows how to run. No name-to-operator table exists in mask-risc, Quack or relalg (searched `src/` of all three for `from_name`/`by_name`/`label`/`parse`/`from_str`; none), so the R2IL lens is the only existing one. + +### 19.3 D-DYNBAG-0 stops here: three missing backend capabilities + +| id | missing | owner | why essential | +|---|---|---|---| +| R1 | lowering a `MethodBinding`'s ordered `effects` (`AlgebraRef` under the fold lens, `Arg`s) onto `FoldDialect` calls (this is X1, the executor seam) | `lance-graph-r2il` (the reading's crate; DT64 stays non-executing) | without it the executed path cannot follow the binding; any probe-side sequence would be the frontend-owned recipe this section forbids | +| R2 | a keyed-count fold word (`GROUP_COUNT` → mask-risc `Terminal::GroupReduce { fold: GroupFold::Count }`, which exists) | OGAR `ogar-r2il` opcode table + `lance-graph-r2il` arm | the fold band is `VIA, RANGE, SUM, MIN, MAX, GROUP_SUM, KEY_RUNS, ANY, ALL, KEEP, SCATTER_OR, BLEND` (`ogar-r2il/src/lib.rs:499-525`); no keyed count. `GROUP_SUM` over a fabricated all-ones lane would be a per-row materialization | +| R3 | combining two group sinks: checked i64 multiply (ℕ) and nonzero-to-mask (B) | mask-risc word + R2IL fold word (D-DYNBAG-3) | XLOG's chain is two relations over two tables; the per-Y degrees come from two programs, and support/multiplicity are their combination | + +Also: `0xC401` is provisional; a lab use is fine, a persisted GUID is not until OGAR mints it. + +### 19.4 Wave 0 resumes when + +R1 exists in `lance-graph-r2il` (testable with existing words such as `SUM`, `GROUP_SUM`, `POP_COUNT`, `KEEP`) and R2 lands. Then the XLOG binding's effects are `[GROUP_COUNT(left), GROUP_COUNT(right), combine]`, and the Wave 0 gate is: changing or refusing that binding changes or refuses the executed path. Until R3, the combine step stays the tracked `checked_binary_i64` call. Disable runs, register and scalar oracles, and stale-frame tests are kept unchanged. + +### 19.5 F### (hypothesis, unchanged status) + +`F###` is a candidate compact address space for reusable atoms and compositions, not a spelling of `MethodId`. §19.2 shows atoms already have a compact address (`FnIndex` under a reading's lens) and compositions have one (`MethodBinding::effects` under a consumer classid). Whether a separate region is needed is undemonstrated. No `0xFFFF_F###` classid is minted and the CanonHigh split is unchanged. From 29cdf922c3866db906f53097708715e9fa871c3e Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 15:25:36 +0000 Subject: [PATCH 5/6] =?UTF-8?q?plans:=20D-DYNBAG=20=C2=A720,=20the=20codeg?= =?UTF-8?q?raph=20is=20behind=20execution,=20not=20in=20front=20of=20it?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- .claude/plans/d-dynbag-holographic-bags-v1.md | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/.claude/plans/d-dynbag-holographic-bags-v1.md b/.claude/plans/d-dynbag-holographic-bags-v1.md index dc4ca27c0..f3a46961f 100644 --- a/.claude/plans/d-dynbag-holographic-bags-v1.md +++ b/.claude/plans/d-dynbag-holographic-bags-v1.md @@ -640,3 +640,27 @@ R1 exists in `lance-graph-r2il` (testable with existing words such as `SUM`, `GR ### 19.5 F### (hypothesis, unchanged status) `F###` is a candidate compact address space for reusable atoms and compositions, not a spelling of `MethodId`. §19.2 shows atoms already have a compact address (`FnIndex` under a reading's lens) and compositions have one (`MethodBinding::effects` under a consumer classid). Whether a separate region is needed is undemonstrated. No `0xFFFF_F###` classid is minted and the CanonHigh split is unchanged. + +--- + +## 20. Correction: the codegraph is the inspectable representation behind execution, not its toll gate (2026-10-31, operator) + +**Invariant.** R2IL / the codegraph is never a mandatory execution intermediary. A consumer resolves and binds once (cold) and then runs its own prepared native plan (Quack, mask-risc, `ndarray::simd`) with no codegraph lookup in the hot path. Tract is the precedent: `plan.rs` resolves once and `Plan::run` dispatches the bound entry after a frame check (`tract-harvest-probe/src/plan.rs:116-128,171,204`). No mandatory graph construction per invocation, no mandatory R2IL interpretation of native code, no second runtime. + +Four things stay distinct, and none proves another: + +| layer | answers | today | +|---|---|---| +| source / typed codegraph | which operations and dependencies the program has | r2ssa graphs, the Tract `TypedModel`, D-SAG-6 rows (LAB); the universal addressed codegraph (`0xC402`) is PROPOSED | +| optimized plan + rewrite witnesses | which rules turned it into the executable form | `egglog-r2il-probe` law-gated rewrites (LAB, scalar) | +| runtime execution events | what actually ran, under which frame | R1 `Receipt` (bounded by step count) | +| logical provenance | which rules and facts derived an answer | not built; Soufflé-style lazy reconstruction is the model | + +Keep source operation ids, method signatures, typed operand edges, plan ids, rule ids and version witnesses, so a receipt can be related back to the codegraph. No per-row or per-op hot-path audit; bounded receipts, and reconstruction on demand. + +**Consequences:** +- **R1 (#1892)** is an optional reading: `prepare` (cold) / `run` (hot) / `Receipt`. It is not a dependency of D-DYNBAG-0. +- **D-DYNBAG-0's seam** is binding → prepared native plan. Its missing piece is a backend-owned mapping from a bound word to a Quack aggregate, built at prepare time, not R1. +- **R2 (an R2IL keyed-count word) is dropped for D-DYNBAG-0:** Quack already has `Agg::GroupReduce { Local, Count }`. +- **R3 (combining two group sinks) still stands.** +- **Future:** codegraph relations (`Defines`, `Uses`, `Calls`, `DependsOn`, `Rewrites`, `Emits`, `Executed`, `Derived`) are projections over codegraph addresses for XLOG / Egglog / DialEgg analysis, never a second graph store. From da0911f6d7eca03ceb0baae6955c2d3a382d6760 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 31 Oct 2026 15:35:19 +0000 Subject: [PATCH 6/6] board: co-research map, mandatory codegraph vs lazy reasoning behind DT64 Five scouts, three co-architects. The premise splits: R2IL is one vocabulary with no method identity, so the canonical body belongs in the OGAR IR (ActionDef -> ogar-loco Program) with a derived body revision; DT64 carries a reference; reasoning runs cold; receipts name body, plan and target. Draft #1892 is the reverse translator ruled out today and is marked superseded. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMNZqKXSaeb9g2ypywF --- ...26-10-31-coresearch-mandatory-codegraph.md | 85 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 2 files changed, 87 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-31-coresearch-mandatory-codegraph.md diff --git a/.claude/board/entries/2026-10-31-coresearch-mandatory-codegraph.md b/.claude/board/entries/2026-10-31-coresearch-mandatory-codegraph.md new file mode 100644 index 000000000..632819422 --- /dev/null +++ b/.claude/board/entries/2026-10-31-coresearch-mandatory-codegraph.md @@ -0,0 +1,85 @@ +# Co-research: mandatory codegraph, lazy reasoning behind DT64 + +**Date 2026-10-31 · Status OPEN (exploration map; nothing adopted by the council) · Plan refs: D-DYNBAG §18-§20** + +**Question.** Can "every admitted executable method has a mandatory, versioned, addressable codegraph (proposed: R2IL); execution runs a bound native plan without hot-path graph traversal; reasoning is pushed down lazily through DT64" be made true without duplication? What is the minimal ownership and binding seam? + +**Premise gate (premise-auditor): PREMISE-SPLIT.** The clause "R2IL owns the method representation" is PREMISE-WRONG as filed. R2IL (`ogar-r2il`) is one domain vocabulary: an arity table with no method identity and no revisions (`lib.rs:3-60`). "Codegraph" names two artifacts: +- (a) the static, versioned body (frame); +- (b) the index of executed ops (motion, per run). + +The scouts answered four re-asked questions: Q1 who owns the body, Q2 is the binding a projection of it, Q3 what a receipt carries, Q4 where the cold analysis runs. + +## Inside facts (VERIFIED-IN-CODE) + +- OGAR `ActionDef` holds the body as `body_source: Option`, with no revision and no hash (`ogar-vocab/src/lib.rs:396-457`). +- `ogar-loco::Program` is an executable body form that "does not mint keys" (`program.rs:38-49`). Executable `PROC_DEF` is OPEN. +- DT64 `MethodBinding` is hand-authored. Nothing derives it from an OGAR body (closed search over `lance-graph/crates` and `OGAR/crates`). `MethodRef` cannot name a body. +- Opaque ops are refused everywhere: R2IL `CallOther` has arity `None`; Tract returns `Refusal::Unregistered`. No opaque-node type exists. +- Per-op provenance exists only in r2ssa (`OpArena` `OpOrigin`/`Pass`). +- Content-derived revisions exist only in tract-harvest-probe (`FrameRevisions.source`), a lab crate. + +## Outside evidence (read by section) + +- **Soufflé provenance** (arXiv 1907.05045): each result carries a rule id and a proof height; proof trees are built on demand; overhead 1.27× time and 1.45× memory. +- **MLIR** (arXiv 2002.11054): one IR with many dialects; unknown ops are handled conservatively; effects are declared through traits and interfaces; each op carries a Location as provenance. +- **Incremental CodeQL** (arXiv 2308.09660): results are populated on demand, and incremental reuse works only with stable IDs across commits. +- **PROV-O**: `used`, `wasGeneratedBy`, `hadPlan`. +- **PostgreSQL plan cache**: a plan is re-planned when a recorded dependency changes. +- **ONNX Runtime**: a saved optimized model is valid only for its target, so a receipt must name the target. + +## Exploration map + +| # | idea | bridge | firewall | verdict | probe | +|---|---|---|---|---|---| +| 1 | Canonical method body lives in the OGAR IR (`ActionDef` → `ogar-loco::Program`), written in several vocabularies; R2IL is one of them | OPPORTUNITY | PASS | **ADOPT-NOW as the ownership rule** (doctrine already in OGAR-AS-IR; no code) | P1 | +| 2 | "R2IL owns the method representation" | DROP | TRAP | **SKIP** (contradicts the ruling that R2IL is executed and never pre-converted; R2IL has no identity) | — | +| 3 | Body revision = digest of canonical body bytes, identity only, never a correctness gate; held on the OGAR Core node | OPPORTUNITY | PASS (conditional) | **PROBE** | P2 | +| 4 | DT64 binding footprint derived from the body by a cold lowering outside DT64; DT64 validates (undeclared write refuses, inferred read warns) | WORTH-EXPLORING | CONFLICT (seam: OGAR codegen / lance-graph-ogar adapter) | **PROBE** | P3 | +| 5 | `MethodRef` + `body_rev`, frozen under D5; settle EXO-50 together | OPPORTUNITY | PASS | **PROBE** after P2/P3 (DT64 type change: owner decision) | P4 | +| 6 | Opaque native ops as declared extern words with arity + footprint in the OGAR body IR (never in the R2IL table) | WORTH-EXPLORING | CONFLICT (seam: OGAR body IR only, executed by the native adapter) | **PARK** pending an OGAR ruling | P5 | +| 7 | Receipt per run: `MethodRef`, `body_rev`, `plan_rev`, target, frame/route, output | OPPORTUNITY | PASS (per run, never per row) | **PROBE** | P7 | +| 8 | Re-plan or refuse when a recorded revision changes | WORTH-EXPLORING | PASS | **PARK** (frame/route rechecks exist; body revision depends on 3 and 5) | — | +| 9 | Lazy provenance | WORTH-EXPLORING | CONFLICT if per-row | **ADOPT-NOW as a rule:** the hot path emits only the per-run receipt; proofs are rebuilt cold by replay | — | +| 10 | Cold relational code projections (Defines/Uses/Calls/…) keyed by (MethodRef, body_rev), computed on demand, never stored as authority | WORTH-EXPLORING | CONFLICT if persisted | **PARK** until a body exists | P8 | +| 11 | Persist the e-graph in the IR | DROP | TRAP | **SKIP** | — | +| 12 | "Mandatory codegraph" | OPPORTUNITY as a mandatory body reference at admission | SPLIT | **PROBE** as "mandatory body reference"; **SKIP** as "mandatory R2IL graph" | P9 | +| 13 | #1892: DT64 effects → R2IL lowering | DROP | TRAP | **SKIP**: #1892 is superseded, do not merge. Reusable parts: the `Receipt` shape (re-key to body/plan revision), the `FoldDialect` run path | — | +| 14 | One def-use container for Tract / r2ssa / OnnxGraph | WORTH-EXPLORING | CONFLICT (no new shared type) | **PARK**; if pursued, a ClassView reading over the existing body container | P10 | + +## Minimal seam (proposal, for the operator) + +- **Body.** OGAR owns it. The Core node's `ActionDef` references one `ogar-loco::Program`, written in core words plus vocabulary words (R2IL, relalg, onnx, declared externs). `body_rev` is a digest of the canonical body bytes: an identity, never a gate. `body_source` stays as provenance text. +- **DT64.** Carries a reference, `MethodRef` + `body_rev`. Under D5 a new body means a derived classid plus a re-route. DT64 still executes nothing and gains no dependency on the interpreter. +- **Binding.** ON/WHEN stay authored in DT64. The effects/reads footprint is checked against a footprint derived by a cold lowering outside DT64 (OGAR codegen or the lance-graph-ogar adapter). Full derivation comes later, after P3 measures it. +- **Execution.** Prepare lowers the body once into a native plan with `plan_rev`; the plan is a cache, re-derivable from (`body_rev`, target). Run executes only the plan. Tract's `Plan` is the precedent. +- **Receipt.** One per run: `MethodRef`, `body_rev`, `plan_rev`, target, frame/route, output. Replay refuses on any mismatch, as D-TGB-4 does. +- **Reasoning.** XLOG / Egglog / DialEgg / Datalog run as cold passes keyed by (`MethodRef`, `body_rev`) and read the OGAR body. DT64 hands out the key, never the evaluation. Nothing is persisted as a second store. +- **Opaque ops.** Declared extern words with an arity and a footprint in the body IR. An undeclared op is still refused. + +## Probes (pre-registered; lab only; P2 and P3 first, they gate P4, P7 and P9) + +- **P1** Join an `ActionDef` and its `Program` under (classid, method, `body_rev`) without copying fields. Kill if the Program needs a field that lives only outside OGAR, or if the join needs a new store. +- **P2** Is `body_rev` stable across a no-op re-harvest, and does it change on a one-token semantic edit? Kill on either noise or insensitivity. +- **P3** Derive the binding footprint from `ActionDef` (reads/writes/calls/KausalSpec) and compare it with the hand-authored xlog-relcomp-probe bindings. Kill if any field needs invented information, or if registration refuses it with `UndeclaredRead`. +- **P4** Lab copy of DT64 with `body_rev` on `MethodRef`. Kill if registration needs the copied effects. +- **P5** A deliberately unregistered Jina op as an opaque node. Kill if the analysis silently treats it as pure. +- **P6** No hot-path traversal: lookups per run after bind must be zero, or at least independent of graph size (tiny vs Jina; sag fixture at N vs 16N). Report in ns/µs. +- **P7** Does the receipt tell runs apart when the body or the target changes? Today's `plan_id` would collide when the body changes but the binding does not. +- **P8** r2ssa rows keyed by (MethodRef, `body_rev`, OpOrigin). Kill if OpOrigin is unstable across identical harvests. +- **P9** Census: admitted methods with no OGAR body to point to. If there are more than 0, "mandatory" is a new authoring obligation. +- **P10** One def-use container across Tract / r2ssa / OnnxGraph. Kill if it needs `Any` or a blob. + +## Not searched + +- Translation validation / proof-carrying code (no primary source read). +- egglog and DialEgg papers beyond secondhand summaries. +- semiring provenance (not read). +- ProvONE (fetch failed). +- r2sleigh `r2engine` scheduling cost. +- OGAR `KausalSpec` variant bodies in depth. +- consumer repos (medcare-rs, odoo-rs), to count `ActionDef`s with a `body_source`. + +## Closeout + +PR #1890 | STATUS: open | OUTCOME: exploration map; #1892 marked superseded | OPEN: operator choice of probes; OGAR ruling on opaque extern words; executable `PROC_DEF`; EXO-50 diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c70ff8f9e..afde3629c 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -524 entries, 2026-08-06 .. 2026-10-31. +525 entries, 2026-08-06 .. 2026-10-31. | date | entry id | finding | file | |---|---|---|---| @@ -37,6 +37,7 @@ exactly one of them, never both. | 2026-10-31 | `D-MIST-NATIVE-1b` | | [2026-10-31-d-mist-native-1b-makor-hydrate.md](2026-10-31-d-mist-native-1b-makor-hydrate.md) | | 2026-10-31 | `D-DT64-6-DR` | | [2026-10-31-d-dt64-6-dr-addressing-module.md](2026-10-31-d-dt64-6-dr-addressing-module.md) | | 2026-10-31 | `D-DYNBAG-X` | | [2026-10-31-cross-frontend-projection-crosswalk.md](2026-10-31-cross-frontend-projection-crosswalk.md) | +| 2026-10-31 | `coresearch-mandatory-codegraph` | | [2026-10-31-coresearch-mandatory-codegraph.md](2026-10-31-coresearch-mandatory-codegraph.md) | | 2026-10-30 | `D-XLOG-NATIVE-0` | | [2026-10-30-d-xlog-native-crosswalk.md](2026-10-30-d-xlog-native-crosswalk.md) | | 2026-10-30 | `D-XLOG-DR64-0` | XLOG's CPU frontend lowers onto DR64 relcomp (answer {2}, 2 oracles); its optimizer emits ChainJoin and swapped orders; arrow 60 vs 58 blocks in-tree use; masks lose to scalar on selective data | [2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md](2026-10-30-d-xlog-dr64-0-xlog-rir-over-dr64-relcomp.md) | | 2026-10-30 | `D-TRACT-SHAPE-1` | | [2026-10-30-d-tract-shape-1-cold-shape-folding.md](2026-10-30-d-tract-shape-1-cold-shape-folding.md) |