From 7fa353614a3bc909a4541ec1479a27971eb14947 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:22:32 +0000 Subject: [PATCH 1/4] board: D-TGA-5D shipped (#1739); IDEAS amendments on X8 and the DR64 certified-compiler row D-TGA-5D said In PR; #1739 merged as 9a458cae. X8: #1740 ran the fresh-frame half; the catalogue multi-binding half is untouched. Certified-compiler row: certify_reassociation (#1707) is an issuer; the single-operand admit_recipe path still refuses. Independent checker, second law and prover revision are still missing. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/IDEAS.md | 2 ++ .claude/board/STATUS_BOARD.md | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/.claude/board/IDEAS.md b/.claude/board/IDEAS.md index 9640dc320..8bb8e7775 100644 --- a/.claude/board/IDEAS.md +++ b/.claude/board/IDEAS.md @@ -283,6 +283,7 @@ deduplicated set where MeTTa returns a bag. `[P2 domain:dr-math D-DRMC]` After X15, `dr-math-binding-probe` admits a recipe only through an opaque `RecipeCertificate` that a certified compiler issues; none exists, so every admission ends in `NoCertifiedCompiler` (`entries/2026-10-22-coresearch-drmc-stack.md` § Applied, #1703). The boundary needs three parts: a typed relational statement language over ClassView domains, egglog laws over it whose proofs a checker independent of the producer re-checks, and a check that the lowering preserves the statement. First law: associativity of Boolean relation composition, already measured as a probe (D-DRMC-5, #1707: 14 orders, one relation). Kill: the statement language cannot type the composition D-DRMC-5 already runs. Scope question for the operator: how far the boundary goes (LEDGER-REVISION-2026-10-23e Q2). +**Amended 2026-10-23 (D-ONNX-RELALG-CAP S0):** "none exists" is scoped too broadly. The single-operand `admit_recipe` path still ends in `NoCertifiedCompiler` (`recipe.rs`). `relcomp::certify_reassociation` (#1707) IS an issuer: it covers associativity of Boolean-Distinct relation composition, egglog-proved, digest-bound (correction #1738), and its certificates re-execute on fresh frames (#1740). Still missing: an independent proof checker; any second law; the multi-binding catalogue; any production path. The egglog dependency floats on `branch = "main"`, and no certificate field names the prover revision. **Fruit:** Heavy **Status:** Open @@ -291,6 +292,7 @@ After X15, `dr-math-binding-probe` admits a recipe only through an opaque `Recip `[P1 domain:dr-math D-DRMC]` Pre-registered in `entries/2026-10-22-coresearch-drmc-stack.md`, none run. X6: `validity: None` must refuse or report `Unattested`, never silently mean all-known. X7: a compile-fail test that no `PopulationReport` → premise conversion exists. X8: two certified bindings for one key (today the first falls back). X16: a law found on class 1 must not reach class 22 (2 counterexamples) unchecked. X18: a census may veto ACT-R eligibility, never qualify it. Each is one falsifier on an existing crate; X6, X7 and X18 are the cheapest. +**Amended 2026-10-23 (D-ONNX-RELALG-CAP S0):** one half of X8 has run. #1740 (`c42140b7`, `dr-math-binding-probe/tests/x8_fresh_frame.rs`, 7/7) re-executes a D-DRMC-5 certificate on independently issued fresh frames with 0 egglog calls. The half named above, two certified bindings for one key in the `egglog-r2il-probe` catalogue (whose `insert` overwrites), is untouched: #1740 changes no catalogue file. X6, X7, X16 and X18 are still unrun. **Fruit:** High-signal **Status:** Open diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 39b1ce932..02810cd3e 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -386,7 +386,7 @@ Plan: `.claude/plans/ce64-hypothesis-layers-v1.md`. Plateau: `.claude/knowledge/ | **D-TGA-3** | rebase (four masks, no data moved) | Queued | rebase-then-squash == from-scratch re-run on v+1, including a deletion in main (retract then re-derive); disables: no stale re-run, no conflict check, no retraction | | **D-TGA-4** | land through the revision gate into the next Lance version (D-HL-8) | Queued | landing a thought that is behind is refused | | **D-TGA-5** | squash_into (partial squash) and blame | Shipped (lab, #1736: `crates/thought-git-probe/src/squash.rs` + `tests/squash_gate.rs`, `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, P8 Commit-only, 6 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | -| **D-TGA-5D** | Probe D: protected readers of a squash (Final / Intermediate / Contradictions / Divergences / Multiplicity) | In PR (lab: `tests/protected_readers.rs`, `entries/2026-10-23-d-tga-5d-protected-readers-preregistration.md`; 7 tests, 5 disables red) | a protected reader the retained data cannot answer refuses the squash; intermediate reads are never retainable | +| **D-TGA-5D** | Probe D: protected readers of a squash (Final / Intermediate / Contradictions / Divergences / Multiplicity) | Shipped (lab, #1739 merged `9a458cae`: `crates/thought-git-probe/src/squash.rs` + `tests/protected_readers.rs`, `entries/2026-10-23-d-tga-5d-protected-readers-preregistration.md`; 7 tests, 5 disables red) | a protected reader the retained data cannot answer refuses the squash; intermediate reads are never retainable | | **D-TGA-6** | MergeQueue | Queued | independent thoughts == landed by hand in FIFO order; a thought reading another negated lands after it; a cycle through negation refused at enqueue | | **D-TGB-0** | thought git basics: fixtures per write-intention outcome, squash-stack and anomaly fixtures, absent-not-zero fixture, from-scratch oracle (`thought-git-basics-v1.md`) | Shipped (lab, #1630; probe `crates/thought-git-probe`, 19 tests; `PREREGISTRATION.md`) | 5 oracle disables verified red-then-green; every signal has a can-fire and a can-stay-silent case on real contract code; the pearl half on edges moves to D-TGB-3 | | **D-TGB-1** | slot pool, autonomous: taken by `branch`, freed by `squash`/`discard`/`land` (the write is the Rubicon decision, 2026-10-20) | Shipped (lab, #1630/#1631; `crates/thought-git-probe/src/slots.rs`). Slot pool only: no production land, rebase or persistence (D-TGB-2..5 Queued) | at 63 taken `branch` picks a FIFO or least-used candidate, squashes it along its dependency chain if it has one, else evicts it (DECISIONS 2026-10-20; was: squash unremarkable first, else refuse); stale handles refused; 6 tests | From 83945785af41d759ff5f1fff21d6a797c8a88c59 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:23:20 +0000 Subject: [PATCH 2/4] board: PR_ARC catch-up #1726-#1741, LATEST_STATE after #1741, D-TGA-5 file attribution Catch-up entries from the merge commits; hygiene-only PRs (#1727, #1728, #1730, #1732-#1735) get none. #1738 is a correction and gets one. D-TGA-5's row named src/squash.rs under #1736; #1736 added only tests/squash_gate.rs, and the gate moved to src/squash.rs in #1739. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/LATEST_STATE.md | 5 +++ .claude/board/PR_ARC_INVENTORY.md | 63 +++++++++++++++++++++++++++++++ .claude/board/STATUS_BOARD.md | 2 +- 3 files changed, 69 insertions(+), 1 deletion(-) diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 802d59aa4..681f89c5a 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,8 @@ +## 2026-10-23 — main after #1741 (merged `59538865`) + +- **On main since #1725:** Palette256 compose and learned-LUT probes (#1726, #1731), the BREADCRUMBS / TORQUE / GOLDSTAUB ledgers and `fruits_index.py` (#1729), the thought-git squash gate and Probe D (#1736, #1739, lab, `thought-git-probe`), the D-DRMC-5 fresh-frame reuse L1 (#1740, lab, `dr-math-binding-probe`), the "no certified compiler" scope correction (#1738), and coresearch maps (#1737, #1741). Per-PR records: `PR_ARC_INVENTORY.md`. +- **Contract inventory delta:** none. Every PR in this range is a lab crate, a probe, a ledger or a board entry. + ## 2026-10-23 — main after #1725 (merged `b342d47c`) - **On main since #1682:** the D-QR plan family (#1660–#1663), D-QSP/D-RFT/D-LFA plans and probes (#1667–#1688), the math-foundry / egglog-r2il arc (#1690–#1699, #1705, #1717), the D-DRMC charter and probes (#1700, #1707, #1708), the Ascent BYODS plan (#1706), the Palette256 evidence and plasticity probes (#1709–#1722), and the decision-side probes P-D4, P-E2, P-D3 with the P-D4 correction (#1723–#1725). Per-PR records: `PR_ARC_INVENTORY.md` catch-up entries. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index a6b3d49ef..3b428e309 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,5 +1,68 @@ + + +## 2026-10-23 — lance-graph PR #1741 (merged `59538865`, branch `board/coresearch-julia-egraphs-20261023`, head `dcef8cc1`) — board: coresearch map — Julia e-graphs vs egglog/datafrog/Ascent; Lisp vs Prolog for MeTTa + +- **Added:** board only. +- **Docs:** entry `2026-10-23-coresearch-julia-egraphs.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1740 (merged `c42140b7`, branch `lab/drmc-l1-x8-fresh-frame-20261023`, head `95b2cb18`) — dr-math-binding-probe: L1, reuse a D-DRMC-5 certificate on a fresh frame (X8) + +- **Added:** `crates/dr-math-binding-probe` (`src/recipe.rs`, `src/relcomp.rs`, `tests/x8_fresh_frame.rs`). +- **Docs:** entries `2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md`, `2026-10-23-drmc-l1-x8-fresh-frame-result.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1739 (merged `9a458cae`, branch `ccr-d3ce1263-ied9yh`, head `52fab2cd`) — thought-git-probe: Probe D (D-TGA-5D), protected readers of a squash + +- **Added:** `crates/thought-git-probe` (`src/lib.rs`, new `src/squash.rs`, `tests/protected_readers.rs`, `tests/squash_gate.rs`); the D-TGA-5 squash gate moved into `src/squash.rs`; probe renamed D-TGA-6 -> D-TGA-5D. +- **Docs:** entry `2026-10-23-d-tga-5d-protected-readers-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1738 (merged `05b3516e`, branch `ccr-d3ce1263-ied9yh`, head `dca7c758`) — correction: "no DR64 certificate" scoped to the single-operand admit_recipe path + +- **Added:** correction in `crates/dr-math-binding-probe/RECIPE_ADMISSION.md` and in `entries/2026-10-23-coresearch-thought-git-markov.md`: `relcomp::certify_reassociation` (#1707) issues certificates; only `admit_recipe` ends in `NoCertifiedCompiler`. No code. +- **Locked / deferred:** see the PR body; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1737 (merged `64bd1902`, branch `board/coresearch-thought-git-markov-20261023`, head `38989f66`) — board: /coresearch map — thought-git accumulation as a large Markov chain (CC2 map and gap map) + +- **Added:** board only. +- **Docs:** entries `2026-10-23-coresearch-thought-git-markov-cc2.md`, `2026-10-23-cc2-proof-compiling-gap-map.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1736 (merged `1b87a27e`, branch `ccr-d3ce1263-ied9yh`, head `6ad966d1`) — probe(D-TGA-5): squash the chain of origin into the most-updated lane, gated on contradiction; blame survives + +- **Added:** `crates/thought-git-probe/tests/squash_gate.rs`; board IDEAS/FRUITS/STATUS_BOARD rows. +- **Docs:** entries `2026-10-23-d-tga-5-squash-gate-preregistration.md`, `2026-10-23-coresearch-thought-git-markov.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1731 (merged `55e6777a`, branch `lab/exo129-learned-lut-composition-20261023`, head `e207e5ca`) — probe(EXO-129): a learned 256×256 table does not compose where the codebook is not closed + +- **Added:** `crates/bgz-tensor/tests/exo129_learned_lut_probe.rs`. +- **Docs:** entry `2026-10-23-exo129-learned-lut-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1729 (merged `8f610a85`, branch `board/ledgers-torque-goldstaub-20261023`, head `4a3685f1`) — board: BREADCRUMBS / TORQUE / GOLDSTAUB ledgers, amended closeout table, generated FRUITS.md + +- **Added:** `.claude/board/{BREADCRUMBS,TORQUE,GOLDSTAUB,FRUITS}.md`; `.claude/tools/append_only_gate.py`, `.claude/tools/fruits_index.py`; `.github/workflows/append-only-gate.yml`; `CLAUDE.md` closeout-table amendment; `.claude/BOOT.md`, `.claude/settings.json`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + +## 2026-10-23 — lance-graph PR #1726 (merged `19c1324a`, branch `lab/ps2-pl3-lut-composition-20261023`, head `9f1370b2`) — probe(P-S2): a Palette256 compose table does not survive two hops + +- **Added:** `crates/bgz-tensor` (`src/attention.rs`, `tests/p_s2_compose_chain_probe.rs`). +- **Docs:** entry `2026-10-23-ps2-compose-chain-preregistration.md`. +- **Locked / deferred:** see the PR body and its board entry; not restated here. +- **Confidence:** CATCH-UP (2026-10-23): recorded from the merge commit, not re-reviewed. + ## 2026-10-23 — lance-graph PR #1725 (merged `b342d47c`, branch `lab/pd4-refit-base-rate-20261022`, head `57fbec40`) — probe(P-D4): refit the base rate inside each bootstrap draw; the post-hoc gate does not pass - **Added:** `crates/causal-edge`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 02810cd3e..4c5f3c376 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -385,7 +385,7 @@ Plan: `.claude/plans/ce64-hypothesis-layers-v1.md`. Plateau: `.claude/knowledge/ | **D-TGA-2** | Read plane R and status | Queued | a read outside R is never reported stale | | **D-TGA-3** | rebase (four masks, no data moved) | Queued | rebase-then-squash == from-scratch re-run on v+1, including a deletion in main (retract then re-derive); disables: no stale re-run, no conflict check, no retraction | | **D-TGA-4** | land through the revision gate into the next Lance version (D-HL-8) | Queued | landing a thought that is behind is refused | -| **D-TGA-5** | squash_into (partial squash) and blame | Shipped (lab, #1736: `crates/thought-git-probe/src/squash.rs` + `tests/squash_gate.rs`, `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, P8 Commit-only, 6 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | +| **D-TGA-5** | squash_into (partial squash) and blame | Shipped (lab, #1736: `crates/thought-git-probe/tests/squash_gate.rs`; the gate moved into `src/squash.rs` in #1739; `entries/2026-10-23-d-tga-5-squash-gate-preregistration.md`; most-updated target, contradiction/divergence gate, blame over lanes, P8 Commit-only, 6 disables red) | blame returns original sources after slot reuse (slot reuse not yet covered) | | **D-TGA-5D** | Probe D: protected readers of a squash (Final / Intermediate / Contradictions / Divergences / Multiplicity) | Shipped (lab, #1739 merged `9a458cae`: `crates/thought-git-probe/src/squash.rs` + `tests/protected_readers.rs`, `entries/2026-10-23-d-tga-5d-protected-readers-preregistration.md`; 7 tests, 5 disables red) | a protected reader the retained data cannot answer refuses the squash; intermediate reads are never retainable | | **D-TGA-6** | MergeQueue | Queued | independent thoughts == landed by hand in FIFO order; a thought reading another negated lands after it; a cycle through negation refused at enqueue | | **D-TGB-0** | thought git basics: fixtures per write-intention outcome, squash-stack and anomaly fixtures, absent-not-zero fixture, from-scratch oracle (`thought-git-basics-v1.md`) | Shipped (lab, #1630; probe `crates/thought-git-probe`, 19 tests; `PREREGISTRATION.md`) | 5 oracle disables verified red-then-green; every signal has a can-fire and a can-stay-silent case on real contract code; the pearl half on edges moves to D-TGB-3 | From ed395380fc7cb51848bac0fa3c0d4ac84368d528 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:35:24 +0000 Subject: [PATCH 3/4] plan(D-ONNX-RELALG-CAP S0): ONNX as import membrane over the existing substrate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Documentation only. ONNX GraphProto stays the graph at the membrane; no new AST, rewrite pass or interpreter. relalg takes only the Boolean/compare/reduce fragment; value maths has no existing home (OP-ONNX-1, operator). Value-indexed ops are refused under ADMISSION B; no float law is admitted; certified applies only to egglog-proved Boolean-Distinct composition associativity (#1707, #1740). The original DR64³ plan was not found (0 files; branch and PR search negative). The DR64³ section is a new, labelled proposal. Open points OP-ONNX-1..14. Board: STATUS_BOARD D-ONNX-0/1/3, INTEGRATION_PLANS, entry 2026-10-23-d-onnx-relalg-cap-s0, entries index regenerated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .claude/board/INTEGRATION_PLANS.md | 4 + .claude/board/STATUS_BOARD.md | 10 + .../2026-10-23-d-onnx-relalg-cap-s0.md | 41 ++++ .claude/board/entries/README.md | 3 +- .claude/plans/d-onnx-relalg-cap-v1.md | 187 ++++++++++++++++++ 5 files changed, 244 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md create mode 100644 .claude/plans/d-onnx-relalg-cap-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index ac14b2832..233d3810c 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,7 @@ +## 2026-10-23 — d-onnx-relalg-cap-v1 — ONNX as an import membrane over the existing substrate → `.claude/plans/d-onnx-relalg-cap-v1.md` + +**Status:** PROPOSAL, documentation only (S0). S1..S5 PLANNED, not authorized. The original DR64³ plan was not found; the DR64³ section is a new, labelled proposal. relalg takes only the Boolean/compare/reduce fragment; the home for value maths is OPEN (OP-ONNX-1), and so is the importer dependency (OP-ONNX-2). Entry: `entries/2026-10-23-d-onnx-relalg-cap-s0.md`. + ## 2026-10-23 — catch-up: plans from #1660–#1708 had no index entry **Status:** INDEX CATCH-UP; no plan status changes. Each status below is the plan's own status line on `main` at `b342d47c`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 4c5f3c376..993e4d72f 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,13 @@ +## D-ONNX-RELALG-CAP — ONNX as import membrane (2026-10-23) + +Plan `d-onnx-relalg-cap-v1.md`, PROPOSAL. Only S0 is in a PR. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-ONNX-0** | S0 capstone plan, coverage matrix, open-points register OP-ONNX-1..14 | In PR (docs only) | consistent with code at `59538865`; no DR64³ claim | +| **D-ONNX-1** | S1 intake probe: ONNX-subset reader with typed refusals; Boolean/compare/reduce fragment onto relalg | Queued (not authorized) | onnxruntime differential (a test, not a proof); waits on OP-ONNX-1, OP-ONNX-2 | +| **D-ONNX-3** | S3 DR64³ R1/R2 contraction probe (new proposal) | Queued (not authorized) | four arms bit-exact; waits on OP-ONNX-4 | + ## D-RFT / D-QSP — ClassView × Quack semantic substrate (2026-10-21) Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quack-postgresql-parity-v1.md`, `d-lfa-lance-graph-flow-rubicon-assimilation-v1.md`; merged). Only the rows below have a claim or evidence; the other D-RFT / D-QSP / D-LFA ids stay as #1667 lists them. diff --git a/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md new file mode 100644 index 000000000..f43696168 --- /dev/null +++ b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md @@ -0,0 +1,41 @@ +# 2026-10-23 — D-ONNX-RELALG-CAP — S0 result: ONNX as import membrane, DR64³ plan not found + +**Status:** S0 documentation; no code. Plan: `.claude/plans/d-onnx-relalg-cap-v1.md`. Read at `origin/main` `59538865`; ONNX facts at upstream commit `0c8af065` (ONNX 1.23.0 = IR 14, ai.onnx opset 28; default domain 203 operators, 155 ops + 48 functions; `ai.onnx.ml` 19). + +## What was searched + +- The repo for `DR64³`, `DR256³`, `64×64×64`, `64x64x64` (`grep -rIl`). +- Branches and PRs: branch `ccr-e97e5d58-1bkumg-cartesian12`; GitHub PR search "cartesian". +- Rust crates for any ONNX dependency (onnx/ort/tract/burn/rten/onnxruntime/wonnx/inkwell/llvm/cranelift) and for `ModelProto`/`GraphProto`/opset in `*.rs`. +- relalg, R2IL, mask-risc, contract set algebra, `dr-math-binding-probe`, `dir-rmap-probe` (read with file:line). + +## What was found + +- DR64³ / DR256³ original plan: NOT FOUND. 0 files contain any of the strings. The branch above is CartesianAddress12/Quad8 shader work. 23 "cartesian" PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. The one 18-bit figure in the repo is the "18-bit hot envelope = 262,144" mailbox working set (`.claude/knowledge/delta-card-addressing-integration-map.md:212`), a working-set size, not an identity. Other 262144 hits are byte counts, CSV values and index spaces. +- The plan's DR64³ section is a NEW, labelled proposal (R1 chain contraction, R2 triangle), not recovered history. Sizes 32 KiB / 2 MiB are arithmetic only. +- No ONNX dependency or parser exists in the Rust tree. onnxruntime 1.29.0 is installed in the container's Python; protoc 3.21.12 is installed; `onnx.reference` cannot run without the C++ extension. +- relalg is single-table Boolean selection plus four I32 aggregates (`crates/lance-graph-relalg/src/ir.rs:47-62`, `:99-110`). The "mathematical polyfill landing zone" proposal holds only for the Boolean/compare/reduce fragment. + +## BLOCKING corrections adopted (opusC) + +1. B1: ONNX is an import membrane only; no new AST, no ONNX rewrite pass or interpreter. "Mathematical polyfill landing zone" is dropped. +2. B2: per-op admission table, default REFUSED; value-derived addressing ops (`Gather*`, `Scatter*`, `NonZero`, `Unique`, `Compress`) refused under ADMISSION B. +3. B3: no float law admitted; float ops lower as written or are refused. +4. B4: every stage has a proof-engine column; "certified" only for egglog-proved Boolean-Distinct composition associativity (#1707, reuse #1740); the "256³ Validate" stage is a differential test. + +## Open points + +- OP-ONNX-1: home for value maths (operator). +- OP-ONNX-2: importer dependency options A-E (operator). +- OP-ONNX-3: DR64³/DR256³ original plan missing. +- OP-ONNX-4: bit-position scan versus D-RU-6 / ADMISSION B. +- OP-ONNX-5: no independent proof checker. +- OP-ONNX-6: certificate rebinding beyond #1740 (focus/scope/ABI/geometry). +- OP-ONNX-7: prover revision not recorded (egglog `branch = "main"`): a certificate-identity gap, not a dependency defect. +- OP-ONNX-8: onnxruntime int32 `ReduceSum` saturation unexplained. +- OP-ONNX-9: `dr-mathematical-compiler-v1.md:79` calls egglog's self-check "independent". +- OP-ONNX-10: `dr-mathematical-compiler-v1.md:19` versus D-RA-2. +- OP-ONNX-11..13: R2 closing-view check placement; `observe_focus` scope omission; refusal granularity and strings in the contract. +- OP-ONNX-14: which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce; the operator rule names them, but only egglog produces one here today. + +D-ONNX-RELALG-CAP | STATUS: open | OUTCOME: S0 plan and this entry; 4 BLOCKING corrections adopted; DR64³ original plan not found | OPEN: OP-ONNX-1..14 diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 970a163ef..83dddd1ad 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. -452 entries, 2026-08-06 .. 2026-10-23. +453 entries, 2026-08-06 .. 2026-10-23. | date | entry id | finding | file | |---|---|---|---| @@ -36,6 +36,7 @@ exactly one of them, never both. | 2026-10-23 | `EXP-DRMC-L1-PREREG` | L1 (CC2 Law Frontier): a certified reassociation reused on a fresh frame (D-DRMC-5 + X8) — pre-registration | [2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md](2026-10-23-drmc-l1-x8-fresh-frame-preregistration.md) | | 2026-10-23 | `D-TGA-5D` | | [2026-10-23-d-tga-5d-protected-readers-preregistration.md](2026-10-23-d-tga-5d-protected-readers-preregistration.md) | | 2026-10-23 | `D-TGA-5` | | [2026-10-23-d-tga-5-squash-gate-preregistration.md](2026-10-23-d-tga-5-squash-gate-preregistration.md) | +| 2026-10-23 | `D-ONNX-RELALG-CAP` | S0 result: ONNX as import membrane, DR64³ plan not found | [2026-10-23-d-onnx-relalg-cap-s0.md](2026-10-23-d-onnx-relalg-cap-s0.md) | | 2026-10-23 | `coresearch-thought-git-markov` | | [2026-10-23-coresearch-thought-git-markov.md](2026-10-23-coresearch-thought-git-markov.md) | | 2026-10-23 | `coresearch-thought-git-markov-cc2` | | [2026-10-23-coresearch-thought-git-markov-cc2.md](2026-10-23-coresearch-thought-git-markov-cc2.md) | | 2026-10-23 | `coresearch-julia-egraphs` | | [2026-10-23-coresearch-julia-egraphs.md](2026-10-23-coresearch-julia-egraphs.md) | diff --git a/.claude/plans/d-onnx-relalg-cap-v1.md b/.claude/plans/d-onnx-relalg-cap-v1.md new file mode 100644 index 000000000..8c88bf6f6 --- /dev/null +++ b/.claude/plans/d-onnx-relalg-cap-v1.md @@ -0,0 +1,187 @@ +# D-ONNX-RELALG-CAP — ONNX as import membrane over the existing substrate (S0) + +**Status:** PROPOSAL, documentation only, 2026-10-23. No code in this plan's PR. Read at `origin/main` `59538865`. ONNX facts are read from the upstream clone at commit `0c8af065` and cited as `onnx::line`. Stages S1..S5 are PLANNED and not authorized. + +**Corrected statement (replaces the original proposal wording).** ONNX is a read-only interchange membrane. An imported model is refused unless every op is in an explicit admitted subset. Admitted ops lower, as written, onto existing contract set-algebra forms and R2IL/Quack/mask-risc terminals through relalg's planning and lowering. Value-indexed ops (`Gather*`, `Scatter*`, `NonZero`, `Unique`, `Compress`), training graphs and float reassociation are refused. The only certified law remains Boolean-Distinct reassociation (egglog, #1707). Every other stage is a differential test. DR64³ and DR256³ are unimplemented proposals with no measured figures. (Source: opusC, "Minimal corrected capstone sentence", adjusted to add `Compress`, which opusA §1 lists as unsupported.) + +**Operator rule (binding), from the brief:** "There is no proof without egglog / eggcc / datafrog / ascent, or at least MeTTa over MORK over a PathMap oracle. Anything planned past it is a hallucination." Hand-written Rust reference evaluators and onnxruntime differentials are TESTS, not proofs. + +**The proposal "lance-graph-relalg is the mathematical polyfill landing zone" holds ONLY for the Boolean/compare/reduce fragment** (opusA §2). Value mathematics (arithmetic, `MatMul`, `Exp`/`Tanh`/`Mish`) has NO existing home. That is an OPEN decision for the operator (OP-ONNX-1), not a gap to fill silently. + +D-RA-2, verbatim (`.claude/plans/d-relalg-unified-v1.md:22`): "D-RA-2 = A: Die kanonische Single-Table-Set-Algebra und ihre Rewrite-Regeln gehören in `lance-graph-contract`. `relalg` behält Lowering und relationale Planung. Keine allgemeine relationale AST für JC oder Quack einführen." + +## 1. What exists + +| Capability | State | Evidence | +|---|---|---| +| relalg `Rel` = All/Empty/Plane/Atom/And/Or/Not; `Measure` = Count/Sum/Min/Max/Keep over I32 lanes | SHIPPED | `crates/lance-graph-relalg/src/ir.rs:47-62`, `:99-110` | +| relalg atoms compare a lane to a constant only (`I32{lane,op,t}`, `U32{lane,eq,v}`) | SHIPPED | `crates/lance-graph-relalg/src/ir.rs:34-39` | +| relalg normalize delegates to the contract set algebra | SHIPPED | `crates/lance-graph-relalg/src/normalize.rs:23-24` | +| relalg lowers through R2IL `FoldDialect` to mask-risc; "recursion (μ) and the hop (preimage) are not built" | SHIPPED / NOT BUILT | `crates/lance-graph-relalg/src/lib.rs:19-21`, `:28-29` | +| relalg is "Not a third frontend syntax" | CHARTER | `crates/lance-graph-relalg/src/lib.rs:23-29` | +| relalg value arithmetic, matmul, nonlinear functions | NOT BUILT | BRIEF verified facts (`join_body.rs` is a GYO alpha-acyclicity check only) | +| mask-risc lanes `I32\|U32\|U64\|Strided`, no float lane | SHIPPED | `crates/lance-graph-mask-risc/src/value.rs:80-88` | +| R2IL scalar arithmetic is scalar×scalar; lane-vs-lane refused `LaneVersusLane` | SHIPPED | `crates/lance-graph-r2il/src/lib.rs:1055-1086` | +| R2IL refuses `BLEND`, `SCATTER_OR` (`Unimplemented`) and unsigned `IntLess`/`IntLessEqual` (`NoUnsignedLaneCompare`) | SHIPPED (refusals) | `crates/lance-graph-r2il/src/lib.rs:37-38`, `:47-51` | +| mask-risc `Terminal::BlendI32` kernel, not wired to relalg | LAB (kernel exists, unwired) | `crates/lance-graph-mask-risc/src/ir.rs:315-318` | +| Boolean-Distinct composition associativity certified by egglog (`admit_composition_assoc`, `prove_reassociation`, `certify_reassociation`) | SHIPPED (lab crate) | `crates/dr-math-binding-probe/src/relcomp.rs:254-262`, `:278-330`, `:421-448` | +| Certificate reuse on fresh frames, 0 egglog calls, 7/7 | SHIPPED (lab, #1740) | `crates/dr-math-binding-probe/tests/x8_fresh_frame.rs`; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | +| DR64 register, `MethodSignature`/`Axis`, `Frame`/`Focus`/`Scope` guards | LAB | `crates/dr-math-binding-probe/src/lib.rs:46-53`, `:179-185` | +| DR256 register (`SLOTS = 256`, `Row = [u64; 4]`), `Qr`, `Composer::compose` | LAB | `crates/dir-rmap-probe/src/focus.rs:55-56`; `src/qr.rs:49-67`; `src/compose.rs:269-341` | +| Independent proof checker | BLOCKED (none exists) | BRIEF; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` ("no independent proof checker") | +| eggcc | BLOCKED (docs/.arxiv only, no code) | BRIEF | +| datafrog, ascent, crepe, MORK, PathMap | LAB (deps/oracles) | BRIEF (crepe-plan-probe, lance-graph-metta, mork-pathmap-probe) | +| ONNX importer (any ONNX crate, `ModelProto`/`GraphProto`/`opset` in `*.rs`) | NOT BUILT | BRIEF: no crate depends on onnx/ort/tract/burn/rten/onnxruntime/wonnx/inkwell/llvm/cranelift; no `ModelProto`/`GraphProto`/opset in `*.rs` | +| bool-tensor ⇄ mask-plane pack/unpack | NOT FOUND (grep only) | opusA §1 facts, §6 item 5 | +| DR64³ / DR256³ plan or code | NOT FOUND | §6 below; BRIEF | + +## 2. Six distinct concerns and their owner surface + +| Concern | Owner surface in this repo | Source | +|---|---|---| +| Graph interchange | ONNX `ModelProto`/`GraphProto` read at the membrane only; no new AST | opusC B1; `onnx:docs/IR.md:35` | +| Mathematical semantics | `lance-graph-contract` set algebra (single-table); mathematical truth is the contract's | `crates/lance-graph-contract/src/set_algebra.rs:1-25`; `.claude/board/entries/2026-10-20-six-decisions.md` §2 | +| Addressing and binding | DR64 `MethodSignature`/`Axis`/`Frame`/`Focus`/`Scope` (lab); ClassView; ADMISSION = B | `crates/dr-math-binding-probe/src/lib.rs:19-53`; `.claude/plans/d-relalg-unified-v1.md:15-19` | +| Physical execution | R2IL `FoldDialect` → mask-risc; `ndarray::simd` kernels; Quack | `crates/lance-graph-relalg/src/lib.rs:19-21`; `crates/lance-graph-quack/src/lib.rs:15` | +| Learned transitions | typed methods over declared relationships, never a source of mathematical truth (operator rule in BRIEF); CausalEdge64 plasticity; ONNX `training_info` refused | BRIEF; `crates/causal-edge/src/layout.rs:38`; `onnx:docs/IR.md:110,515` | +| Proof and certification | egglog certificate for Boolean-Distinct composition only | `crates/dr-math-binding-probe/src/relcomp.rs:254-262`, `:421-448` | + +## 3. ONNX coverage matrix (family level) + +Facts: default domain 203 operators (155 ops + 48 functions), `ai.onnx.ml` 19; ai.onnx opset 28 is the highest with a schema; IR 14 (scoutB §2-3; `onnx:docs/Versioning.md:204` row `1.23.0|14|28|5|1`). Classes: **D** directly representable (restricted), **C** compositionally representable, **K** needs a specialized physical kernel, **P** needs a mathematical polyfill (no home), **X** external backend, **R** refused. Default for every op not named here is **R**. + +Restriction for every D/C row: rank-1, length = `n_rows`, no broadcasting, int32/uint32/bool only, scalar constant right operand (opusA §1, last paragraph). Broadcasting is declared multidirectional (`onnx:docs/Operators.md:659`, `:14877`, `:20384`, `:45053`). + +| Family | Class | Lands on | Semantic difference | +|---|---|---|---| +| `Not`, `And`, `Or` (bool) | D | `Rel::Not/And/Or` → `Measure::Keep` → `INT_NOT/AND/OR` (`crates/lance-graph-relalg/src/lower.rs:138-141`, `:183-192`) | broadcasting refused; bytes⇄bits pack is new intake code | +| `Xor` | C | `(a∧¬b)∨(¬a∧b)`; contract `SetExpr` has no Xor variant (`crates/lance-graph-contract/src/set_algebra.rs:135-147`) | result set identical (two-valued) | +| `Equal`, `Less`, `Greater`, `LessOrEqual`, `GreaterOrEqual`, int32 vs scalar constant | D | `Atom::I32` (`crates/lance-graph-relalg/src/ir.rs:17-36`; `lower.rs:233-257`) | `LessOrEqual`/`GreaterOrEqual` are ONNX functions (`onnx:docs/Operators.md:183,191`): match by op name, do not expand. Output is a mask, not tensor(bool) bytes | +| `Equal` uint32 vs scalar | D | `Atom::U32{eq}` (`ir.rs:38`) | — | +| `Less`/`Greater` on uint32; lane-vs-lane; float/fp16/bf16/double; int8/16/64; string | R | refused `NoUnsignedLaneCompare` (`crates/lance-graph-r2il/src/lib.rs:49-50`); no float lane (`crates/lance-graph-mask-risc/src/value.rs:80-88`) | float NaN is two-valued false, not UNKNOWN: relalg's NNF `Not` push-down is unsound with NaN (opusC N1; `crates/lance-graph-relalg/tests/rewrites.rs:452`, `:314`). Float comparisons do not enter `Rel`/`SetExpr` | +| `ReduceSum` int32, all axes | C, only in the non-overflow domain | `Measure::Sum` → `Answer::Sum(i64)` (`lower.rs:121-125`, `:26`) | three overflow semantics: ONNX output dtype = input dtype (`onnx:docs/Operators.md:32053-32054`); reference wraps (`onnx:onnx/reference/ops/op_reduce_sum.py:26`); onnxruntime 1.29.0 observed saturating (mechanism OPEN); relalg widens to i64. Out-of-i32 result → refusal `OverflowDomain` | +| `ReduceSum` partial axes; uint32/int64/float | R | Sum is I32-lane only (`ir.rs:103`) | — | +| `ReduceMin`/`ReduceMax` int32, all axes | C | `Measure::Min/Max` → `Option` (`lower.rs:126-137`, `:28-30`) | empty reduction: ONNX yields dtype max/min (`onnx:docs/Operators.md:31444`; `onnx:onnx/reference/ops/op_reduce_min.py:38-44`); adapter `None → i32::MAX/MIN`. Float NaN propagation not representable | +| `ReduceSum(Cast(cond, INT64))` row-count pattern | C | `Measure::Count` → `POP_COUNT` (`lower.rs:117-120`) | exact 2-node pattern; output int64 | +| `Where` | K (blocked) | `Terminal::BlendI32` (`crates/lance-graph-mask-risc/src/ir.rs:315-318`); R2IL refuses `BLEND` (`crates/lance-graph-r2il/src/lib.rs:37-38`) | I32 lanes, lane-vs-lane, value-producing; outside `Rel` | +| `Gather`, `GatherElements`, `GatherND`, `ScatterElements` and other Scatter*, `NonZero`, `Unique`, `Compress`, `TopK` indices, any index-tensor input | R (ADMISSION B) | none | value-derived addressing: `onnx:docs/Operators.md:15895` (Gather), `:36661-36667` (ScatterElements), `:26543-26544` (NonZero), `:44310-44316` (Unique). ADMISSION = B: "A position derived from another relational column or table is not admissible as a read address" (`.claude/board/entries/2026-10-20-six-decisions.md` §1). `Compress` writes compacted values; `Keep` writes a mask only (`ir.rs:108-109`) | +| `Add/Sub/Mul/Div/Mod/Pow/Neg/Abs`, elementwise | P | none (R2IL arithmetic is scalar×scalar; `INT_SUB` unchecked at `crates/lance-graph-r2il/src/lib.rs:1080`, ADD/MULT checked at `:1063-1064`) | home OPEN (OP-ONNX-1) | +| `MatMul`, `Gemm`, `Einsum` | K / X | `ndarray::simd::gemm_f64_tiled` is f64 only (ndarray `src/simd.rs:684-697`); f32 delegates to the external `matrixmultiply` crate (`:690`) | ONNX `MatMul` is a sum-product over numeric dtypes, not Boolean composition; no float law is admitted (§4). Boolean relation composition is `relcomp::compose`, which no ONNX op names | +| `Exp`, `Log`, `Tanh`, `Sigmoid`, `Erf`, trig | P | `simd_exp_f32` is a clamped approximation, `#[allow(dead_code)]` (ndarray `src/simd.rs:540-552`); `simd_ln_f32` is a scalar loop (`:610-615`) | numpy ULP semantics are not identical; no `tanh` found (grep only) | +| `Mish`, `Gelu`, `Softmax`, `Relu`, `LayerNormalization` (48 Function-table rows, `onnx:docs/Operators.md:169-218`) | P | bottoms out in Exp/Tanh/Log/Mul | functions may be inlined (`onnx:docs/IR.md:35`) | +| `Shape`, `Size`, `Reshape`, `Squeeze`, `Unsqueeze`, `Flatten`, `Identity`, `Constant` | OPEN | none | intake-time folding possible; unverified | +| `If`, `Loop`, `Scan`, `Sequence*`, `Optional*`, `String*`, `Random*`, `ImageDecoder`, `Quantize/Dequantize*`, `Conv*`, `*Pool`, RNN/LSTM/GRU, `ai.onnx.ml.*` | R / X | none | control flow and subgraphs are a computational-graph format (`onnx:docs/IR.md:35,181-212`) | + +**Per-op admission table (opusC B2).** Each ONNX op is classed CO-ADDRESSED (element-wise, `Not/And/Or`, `Equal` over same-table lanes) / SAME-TABLE-SEEK-UNDER-B (only with an `attest_cost` witness, which has no contract type yet: `.claude/board/ISSUES.md:23-45`) / REFUSED. Default is REFUSED. + +## 4. Intake: what must survive, and how to word compatibility + +Fields that must survive (proto2, `onnx:onnx/onnx.proto:9`). Missing or unknown identity/version → refuse, never default: +- Identity/version: `ModelProto.ir_version` `:453`; `opset_import` `:463` → `OperatorSetIdProto.domain` `:949`, `.version` `:953`; `NodeProto.op_type` `:233`, `.domain` `:235`, `.overload` `:237`. The (domain, opset) resolution rule is OPEN (not read). +- Local functions: `ModelProto.functions` `:522` → `FunctionProto.name` `:965`, `domain` `:1013`, `overload` `:1017`, `opset_import` `:1009`, `attribute`/`attribute_proto` `:983`/`:989`, `node` `:992`, `value_info` `:1023`. +- Types/shapes: `ValueInfoProto.type` `:210` → `TypeProto.Tensor.elem_type` `:860`, `shape` `:861`; `Dimension.dim_value`/`dim_param`/`denotation` `:838-846`. A symbolic `dim_param` must bind to the table's `n_rows`, or refuse. +- Tensors: `GraphProto.initializer` `:576`, `sparse_initializer` `:579`; `TensorProto.dims` `:673`, `data_type` `:677`, `raw_data` `:766`, `external_data` `:777`, `data_location` `:788`. +- Attributes: `AttributeProto.name` `:164`, `type` `:181`, `ref_attr_name` `:170`, values `:184-200`. Unknown attribute on a known op → refuse. +- Annotations round-trip, not dropped: `metadata_props` (Model `:493`, Graph `:599`, Node `:246`, ValueInfo `:214`, Tensor `:805`, Function `:1026`); `doc_string` (Model `:487`, Graph `:582`, Node `:243`, ValueInfo `:212`, Attribute `:173`, Tensor `:741`, Function `:994`); `producer_name/version` `:468`/`:473`; `quantization_annotation` `:596`. +- `training_info` is refused on import (opusC N5; `onnx:docs/IR.md:110,515`). No initializer value is ever a law premise: initializers are data; laws are `AdmittedLaw` values (`crates/dr-math-binding-probe/src/relcomp.rs:254`). + +Typed refusal shape (proposal modelled on `RelError`, `crates/lance-graph-relalg/src/lower.rs:49-54`, and `FoldError`, `crates/lance-graph-r2il/src/lib.rs:201`): `Refusal { node: u32, domain, op_type, opset: i64, reason }`, `reason` ∈ {UnknownDomain, OpsetUnsupported, UnsupportedOp, UnsupportedDtype(elem_type), Broadcast, RankNotOne, DimUnbound(dim_param), UnknownAttribute(name), OverflowDomain, NoUnsignedCompare, ControlFlow, ExternalData, TrainingInfo, ValueIndexedAddress}. Whether strings may enter the contract is OPEN (`crates/lance-graph-relalg/src/ir.rs:1-4` forbids strings in the IR). Never coerce, never partial-run. Whole-graph versus per-node refusal is OPEN. + +**Wording rule (opusC N2).** Do not write "ONNX-compatible". The ONNX IR says "An implementation must support all operators in the set or reject the model" (`onnx:docs/IR.md:80`) and lists "operators that all implementations MUST support" (`onnx:docs/IR.md:67`). The claim is: "ONNX-subset reader that refuses everything else" — it imports IR ≤14, ai.onnx opset N, the listed op subset, and rejects any model whose `opset_import` names an op outside it. "Compatible" is unearned without upstream backend tests per claimed op (`onnx:docs/OnnxBackendTest.md`). + +**No float law.** No float law is admitted. Float ONNX ops lower only as written (fixed evaluation order, analogue of `run_as_written`, `crates/lance-graph-relalg/src/lower.rs:96`) or are refused. Reassociation is admitted for Boolean-Distinct relations only (#1707). The egglog rule set is structural (`crates/dr-math-binding-probe/src/relcomp.rs:283-285`); its soundness rests on OR/AND associativity, which IEEE-754 `+`/`*` lack. No ONNX statement fixing a float summation order was found (OPEN). + +**No ONNX-level rewrite pass (opusC C1).** No ONNX graph optimizer (constant folding, fusion, shape-inference passes) and no ONNX interpreter beside mask-risc. The only rewrites are contract set-algebra and egglog-admitted laws. + +**Palette256 (opusC N4).** ONNX ops never consume or produce Palette256 values except as opaque u8 codes passed through. Forbidden conversions: Palette256 → float to feed an ONNX op; a stored Fisher-z or cosine column produced by an ONNX graph; a generic ONNX distance op over u8 codes (`.claude/board/ISSUES.md:3629-3651`). Codebook attestation has no contract type yet (`.claude/board/ISSUES.md:23-45`). + +## 5. Importer dependency options — OPEN for the operator; no decision + +Facts: nothing in the repo parses ONNX. `prost = "0.13"` is optional in `crates/cognitive-shader-driver/Cargo.toml:255`, enabled only by feature `grpc` (`:282`), under a "NEVER in production binary" comment (`:250`). `protoc` 3.21.12 is installed in the container (`/usr/bin/protoc`). + +| Option | Cost | Risk | +|---|---|---| +| A. prost(-build) codegen from `onnx.proto` | new build dep, protoc at build time | proto2 handling in prost: OPEN; whether an AdaWorldAPI prost fork exists: OPEN (lance-graph CLAUDE.md fork policy) | +| B. hand-written wire reader for the ~15 fields S1 needs | zero deps, hundreds of LOC | a second partial proto decoder to maintain | +| C. existing ONNX crate (tract-onnx, candle-onnx, onnx-protobuf) | brings its own proto, often a runtime | an executor arrives with the parser (none present today) | +| D. no parser in S1: build the graph in-test from Rust values mirroring the proto subset | none | intake of real files untested in S1 | +| E. Python-side intake, scratch only | none in repo | test-only, cannot ship | + +Correction to the brief (opusA §5): onnxruntime 1.29.0 IS installed in the container's Python (not in the Rust tree). `onnx.reference` cannot run in the clone because `import onnx` needs the C++ extension (`onnx:onnx/__init__.py:82`). Either oracle is a differential test, not a proof. + +## 6. DR64³ / DR256³ + +**Original plan: NOT FOUND.** Negative-search evidence (BRIEF): no `DR64³`, `DR256³`, `64×64×64` or `64x64x64` string anywhere in the repo (`grep -rIl`, 0 files). Branch `ccr-e97e5d58-1bkumg-cartesian12` is CartesianAddress12/Quad8 shader work, not the plan. GitHub PR search "cartesian": 23 PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. `.claude/knowledge/delta-card-addressing-integration-map.md:212` has an "18-bit hot envelope = 262,144 ... CONCURRENT mailbox working set", a working-set size and not a DR64³ identity. 262,144 = 2¹⁸ coincides arithmetically; the coincidence licenses nothing and no 18-bit DR64³ identity is defined. + +**What DR64 and DR256 are today:** DR64 `Operand { rows: &[u64; 64], validity }` (`crates/dr-math-binding-probe/src/lib.rs:192-195`), composition `relcomp::compose` (`relcomp.rs:211-222`), `Chain` guards (`relcomp.rs:136-173`). DR256 `Row = [u64; 4]` (`crates/dir-rmap-probe/src/focus.rs:55-56`), `Composer::compose` (`compose.rs:269-341`), guard by `prep::Witness` (`prep.rs:71-85`), no `MethodSignature`/`Axis` typing. + +**NEW PROPOSAL (from opusB §2), not recovered history.** "DR64³" is the logical index cube X×Y×Z (64 each) over which a contraction of typed DR64 views ranges. It is never a stored object. +- (R1) Chain contraction `R: X→Y`, `S: Y→Z`, `(R∘S)[i,k] = ∃j R[i,j] ∧ S[j,k]`. This is `relcomp::compose` today (`relcomp.rs:211-222`); nothing is new except the name. +- (R2) Triangle `(R∘S) ∧ Q` with `Q: X→Z`. Needs one new check not in `Chain` (adjacency only, `relcomp.rs:161-165`): `Q.row == R.row` and `Q.column == S.column`. Whether it belongs in `Chain` or a separate admission type: OPEN. +- Guards applying unchanged: same frame issue and still current (`lib.rs:123-140`, `relcomp.rs:151,166`), same focus (`:154`), same scope (`:157`), domain adjacency (`:161-165`), TwoValued + Distinct only (`:148`, `lib.rs:255`), only `BooleanCompose` admitted (`:254-262`). +- Not allowed: a new identity encoding (no packed `(i,j,k)` id); any CausalEdge64 change (S/P/O bytes are palette indices, `crates/causal-edge/src/edge.rs:141-143`); a new executor; a gather-shaped hop (`crates/lance-graph-mask-risc/src/graph_hop.rs:1-13`); Bag through the DR64 binder (`lib.rs:255`); any claim that 64³ is implemented. +- Sizes, arithmetic only, computed not measured: 64³ bits = 262,144 bits = 32 KiB; 256³ bits = 16,777,216 bits = 2 MiB. The cube must not be materialized; no measurement shows it cheaper (OPEN). No throughput figure is given for either. + +**OPEN tension (bit-position scan).** `relcomp::compose` scans set bits for positions (`trailing_zeros`, `crates/dr-math-binding-probe/src/relcomp.rs:215-218`) and DR256 `compose` does the same (`crates/dir-rmap-probe/src/compose.rs:239-247`, `:304`, `:315`), while `crates/dir-rmap-probe/src/qr.rs:21-23` states "no loop scans set bits for a position (the D-RU-6 address rule)". Whether position-scanning inside one co-addressed frame is the forbidden gather (ADMISSION B, `.claude/board/ISSUES.md:26`) is not ruled anywhere found. + +**DR256³ preconditions (opusB §5), none met:** DR64³ R1/R2 pass the S3 arms with the R2IL arm measured; a DR256 binder with DR64 typing (`prep.rs:71-85`); a certificate route at 256 (no egglog dep in `dir-rmap-probe`); materialization stays refused (precedent `crates/cognitive-shader-driver/src/immaterial_needle.rs:55-67`); `TooLarge` (`qr.rs:94-96`) refuses on every axis; CausalEdge64 S/P/O bytes are not DR256³ coordinates; cross-width transfer (256 → 64) has no code, only DR64→DR64 reuse exists (#1740). + +## 7. Stages + +"Proof engine" values: egglog-certified (only `LawShape::BooleanCompose`), differential test (oracle named), none. "Certified" may appear only in the first case (opusC B4). The operator rule names egglog, eggcc, datafrog, ascent and MeTTa over MORK over a PathMap oracle as the engines a proof may come from. Today only egglog produces a proof object in this repo. eggcc has no code. datafrog and Ascent are dev-dependency oracles here and emit no provenance; their tuple-comparison oracle role was withdrawn on 2026-10-21 (`.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md:64-65`). A stage that wants them as its proof engine must first show what proof object they produce (OPEN, OP-ONNX-14). + +| Stage | Deliverable | Gate | Proof engine | Prerequisite | Status | +|---|---|---|---|---|---| +| S0 | this plan + board entry | review | none | none | this PR | +| S1 | ONNX intake probe, subset reader with typed `Refusal`; Boolean/compare/reduce fragment lowered onto relalg | S1 falsifier below | differential test (onnxruntime 1.29.0; numpy reference semantics) | importer decision (OP-ONNX-2) | PLANNED, not authorized | +| S2 | admission table and value-maths decision recorded | operator ruling | none | OP-ONNX-1 | PLANNED, not authorized | +| S3 | DR64³ R1/R2 contraction probe, three arms | S3 falsifier below | egglog-certified for reassociation only; all else differential test | S2; OP-ONNX-4, OP-ONNX-5 | PLANNED, not authorized | +| S4 | learned-transition boundary: ONNX `training_info` refused; plasticity typed as method, never premise; Palette256 forbidden conversions enforced | refusal tests with disable runs | none (refusals are tests) | S1 | PLANNED, not authorized | +| S5 | export/codegen evaluation | review | none | S1..S4 | PLANNED, not authorized | + +The 64³ Explore → 256³ Validate → Certified Method → 64³ Reuse progression: the "256³ Validate" step is a differential test and must be named so (opusC B4). It has no proof engine today. + +**S1 falsifier (opusA §5).** Fixture: one table, `n_rows ∈ {0, 1, 63, 64, 65, 1000}`, lane `x: int32` (incl. i32::MIN/MAX), lane `k: uint32`, one bool plane `b`, symbolic dim `N`. +- Positive: G1 `Less(x,c)`; G2 `And(Less(x,c), Not(b))`; G3 `ReduceSum(Cast(G2, INT64))`; G4 `ReduceMin(x)`, `ReduceMax(x)` (N=0 → i32::MAX/MIN via adapter); G5 `Equal(k,v)`. relalg output equals onnxruntime output; mask words equal packed bools. +- Negative (named `Refusal`, never an answer): `Tanh(x)`; `Less` on float; `Less` on uint32; `Less(x,x)` lane-vs-lane; broadcast `[N]` vs `[N,1]`; unknown domain; `ReduceSum` whose i64 result leaves i32. +- Silent twin: every positive graph yields zero refusals; in-range `ReduceSum` does not raise `OverflowDomain`; `metadata_props`/`doc_string` still lower and round-trip unchanged. +- Disable runs (commit first, assert the patch applied): `Less→Le`; drop the dtype check; map empty Min `None→0`; delete the overflow guard; skip `Not`. Each must turn a named test red. + +**S3 falsifier (opusB §4).** Fixture: three bound DR64 views on one `FrameStore` seal, one focus, one scope, axes X→Y→Z(→W); seeded fill as `crates/dr-math-binding-probe/tests/relcomp.rs:61`. Arms, bit-exact over all 64 rows: (1) `Chain::eval` over every order (`relcomp.rs:184-201`); (2) a co-addressed R2IL program (`exists(intersect(R_row_i, S_col_k))`, needs `S` transposed first, a preparation cost reported separately per D-RU-6, `.claude/plans/d-relalg-unified-v1.md:205`), which does not exist; (3) an independent scalar pair-enumeration oracle (`tests/relcomp.rs:78-91`), a differential test; (4) reassociation equality via the egglog certificate only (`relcomp.rs:421-448`). Costs reported separately (bind; transpose; steady contraction; result materialization; cold egglog) in ns/µs only. Refusals needing can-fire and can-stay-silent cases: `DifferentFrame` (`relcomp.rs:151-153`), `StaleFrame` (`:166-168`), `DomainMismatch` (`:161-165`), `BagNeedsMultiplicity` (`lib.rs:255-257`), focus/scope moved (`relcomp.rs:154-159`), `NotThisChain` (`:185-187`), and the R2 closing-view axis mismatch (does not exist; must be added and disable-verified). + +## 8. What ONNX reuse eliminates, and what it does not + +- ONNX replaces at most an interchange AST. It does not remove the proof-side term language: egglog needs its own datatype (`crates/dr-math-binding-probe/src/relcomp.rs:283-285`) and ONNX has no rewrite or proof semantics (opusC N7). +- The #1741 Julia-map conclusions P-J1..P-J4 stay open: typed egglog rules via the Rust API, keep `ProofStore`, a standalone replay checker (entry `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md`). X4 (rules as typed values) and X12 (keep the proof DAG) are proof-side work ONNX does not touch. Anchor A2 ("internal proof representation chosen by measurement") is not pre-decided as "ONNX + relalg" and remains open (same entry). +- Certificate reuse is shown only for `source` changes with the same focus, scope and ABI (`crates/dr-math-binding-probe/tests/x8_fresh_frame.rs:17-19,40-46`); refusals at `:211`, `:226`, `:245`. + +## 9. Open-points register + +| ID | Question | Owner | Dependency | Evidence | Falsifier | Decision | Status | +|---|---|---|---|---|---|---|---| +| OP-ONNX-1 | Home for value maths (arithmetic, MatMul, Exp/Tanh/Mish): relalg cannot take it without a new IR | operator | none | opusA §2; D-RA-2 `.claude/plans/d-relalg-unified-v1.md:22`; `crates/lance-graph-relalg/src/lib.rs:25-29` | any proposal adding value-producing nodes to `Rel` | none | OPEN | +| OP-ONNX-2 | Importer dependency (options A-E) | operator | OP-ONNX-1 for scope | §5 above | S1 reads real ONNX bytes | none | OPEN | +| OP-ONNX-3 | DR64³/DR256³ original plan missing | operator | none | §6 negative search (BRIEF) | the plan is located | none | OPEN | +| OP-ONNX-4 | Does bit-position scanning in one co-addressed frame violate ADMISSION B / D-RU-6? | operator | none | `relcomp.rs:215-218`; `compose.rs:239-247`; `qr.rs:21-23`; `.claude/board/ISSUES.md:26` | a ruling | none | OPEN | +| OP-ONNX-5 | Independent proof checker; none exists | plan owner | #1741 P-J4 | `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | a replay checker that rejects a tampered proof | none | OPEN | +| OP-ONNX-6 | Cross-focus/scope/ABI rebinding of certificates beyond #1740 | plan owner | S3 | `tests/x8_fresh_frame.rs:17-19,40-46`; opusC N3 | reuse across stores with different focus/scope/geometry | none | OPEN | +| OP-ONNX-7 | Prover revision not recorded in the certificate (egglog `branch = "main"`). Floating deps are per repo pin policy, so this is a certificate-identity gap, not a dependency defect | plan owner | none | `crates/dr-math-binding-probe/Cargo.toml`; opusC N3 | certificate carries the egglog revision | none | OPEN | +| OP-ONNX-8 | Why onnxruntime 1.29.0 saturates int32 `ReduceSum` (observed in 2 cases) | S1 | S1 | opusA §5 | a third case or the kernel source | none | OPEN | +| OP-ONNX-9 | `.claude/plans/dr-mathematical-compiler-v1.md:79` calls egglog's self-check "independent" (wording defect) | owner of that plan | none | `relcomp.rs:269,290` ("egglog checks every proof it returns") | the wording is corrected | none | OPEN | +| OP-ONNX-10 | `.claude/plans/dr-mathematical-compiler-v1.md:19` "RelAlg/typed AST expresses admissible mathematics" versus D-RA-2; whether it predates 2026-10-20 | owner of that plan | OP-ONNX-1 | opusC B1 | the plan line is reconciled | none | OPEN | +| OP-ONNX-11 | R2 closing-view typing check: in `Chain` or a separate admission type | S3 | S3 | opusB §2 | disable-verified refusal | none | OPEN | +| OP-ONNX-12 | `observe_focus` omits a scope refusal; intended? | plan owner | none | `crates/dr-math-binding-probe/src/population.rs:45-58` | a ruling | none | OPEN | +| OP-ONNX-14 | Which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce, so they can serve as a stage's proof engine | operator | none | `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md:64-65,94` | an exported, replayable derivation | none | OPEN | +| OP-ONNX-13 | Whole-graph versus per-node refusal; strings in the contract | operator | S1 | §4; `ir.rs:1-4` | a ruling | none | OPEN | + +## 10. Housekeeping + +SAFE NOW (done in this PR, commits `7fa35361` and `83945785`): D-TGA-5D status; `IDEAS.md` amendments X8 and the certified-compiler row; PR_ARC catch-up #1726–#1741; LATEST_STATE after #1741; D-TGA-5 file attribution. + +SEPARATE PR: none identified. + +BLOCKED: D-DRMC rows missing from STATUS_BOARD (owner CC2, ask on EXO-50); the `dr-mathematical-compiler-v1.md:79` wording fix (plan owner; OP-ONNX-9). + +## 11. Next gate + +The smallest independently reviewable step is the S1 intake probe, pending the importer decision (OP-ONNX-2) and the value-maths scope ruling (OP-ONNX-1). Nothing past S0 is authorized. From f1f445d3e048325e5104fe0cb6b340276b5bf847 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 23 Oct 2026 19:38:58 +0000 Subject: [PATCH 4/4] plan(D-ONNX-RELALG-CAP S0): cite code by file and symbol, not by line number citation-decay flagged 44 new line-number citations in the S0 plan and entry. The repo's rule is a stable anchor, not a corrected number, so the citations now name the file and the symbol. External onnx: citations at the pinned upstream commit keep their line numbers. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f --- .../2026-10-23-d-onnx-relalg-cap-s0.md | 8 +- .claude/plans/d-onnx-relalg-cap-v1.md | 132 +++++++++--------- 2 files changed, 70 insertions(+), 70 deletions(-) diff --git a/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md index f43696168..c136d3a12 100644 --- a/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md +++ b/.claude/board/entries/2026-10-23-d-onnx-relalg-cap-s0.md @@ -11,10 +11,10 @@ ## What was found -- DR64³ / DR256³ original plan: NOT FOUND. 0 files contain any of the strings. The branch above is CartesianAddress12/Quad8 shader work. 23 "cartesian" PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. The one 18-bit figure in the repo is the "18-bit hot envelope = 262,144" mailbox working set (`.claude/knowledge/delta-card-addressing-integration-map.md:212`), a working-set size, not an identity. Other 262144 hits are byte counts, CSV values and index spaces. +- DR64³ / DR256³ original plan: NOT FOUND. 0 files contain any of the strings. The branch above is CartesianAddress12/Quad8 shader work. 23 "cartesian" PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. The one 18-bit figure in the repo is the "18-bit hot envelope = 262,144" mailbox working set (`.claude/knowledge/delta-card-addressing-integration-map.md`), a working-set size, not an identity. Other 262144 hits are byte counts, CSV values and index spaces. - The plan's DR64³ section is a NEW, labelled proposal (R1 chain contraction, R2 triangle), not recovered history. Sizes 32 KiB / 2 MiB are arithmetic only. - No ONNX dependency or parser exists in the Rust tree. onnxruntime 1.29.0 is installed in the container's Python; protoc 3.21.12 is installed; `onnx.reference` cannot run without the C++ extension. -- relalg is single-table Boolean selection plus four I32 aggregates (`crates/lance-graph-relalg/src/ir.rs:47-62`, `:99-110`). The "mathematical polyfill landing zone" proposal holds only for the Boolean/compare/reduce fragment. +- relalg is single-table Boolean selection plus four I32 aggregates (`crates/lance-graph-relalg/src/ir.rs`). The "mathematical polyfill landing zone" proposal holds only for the Boolean/compare/reduce fragment. ## BLOCKING corrections adopted (opusC) @@ -33,8 +33,8 @@ - OP-ONNX-6: certificate rebinding beyond #1740 (focus/scope/ABI/geometry). - OP-ONNX-7: prover revision not recorded (egglog `branch = "main"`): a certificate-identity gap, not a dependency defect. - OP-ONNX-8: onnxruntime int32 `ReduceSum` saturation unexplained. -- OP-ONNX-9: `dr-mathematical-compiler-v1.md:79` calls egglog's self-check "independent". -- OP-ONNX-10: `dr-mathematical-compiler-v1.md:19` versus D-RA-2. +- OP-ONNX-9: `dr-mathematical-compiler-v1.md` calls egglog's self-check "independent". +- OP-ONNX-10: `dr-mathematical-compiler-v1.md` versus D-RA-2. - OP-ONNX-11..13: R2 closing-view check placement; `observe_focus` scope omission; refusal granularity and strings in the contract. - OP-ONNX-14: which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce; the operator rule names them, but only egglog produces one here today. diff --git a/.claude/plans/d-onnx-relalg-cap-v1.md b/.claude/plans/d-onnx-relalg-cap-v1.md index 8c88bf6f6..e22bde8de 100644 --- a/.claude/plans/d-onnx-relalg-cap-v1.md +++ b/.claude/plans/d-onnx-relalg-cap-v1.md @@ -8,26 +8,26 @@ **The proposal "lance-graph-relalg is the mathematical polyfill landing zone" holds ONLY for the Boolean/compare/reduce fragment** (opusA §2). Value mathematics (arithmetic, `MatMul`, `Exp`/`Tanh`/`Mish`) has NO existing home. That is an OPEN decision for the operator (OP-ONNX-1), not a gap to fill silently. -D-RA-2, verbatim (`.claude/plans/d-relalg-unified-v1.md:22`): "D-RA-2 = A: Die kanonische Single-Table-Set-Algebra und ihre Rewrite-Regeln gehören in `lance-graph-contract`. `relalg` behält Lowering und relationale Planung. Keine allgemeine relationale AST für JC oder Quack einführen." +D-RA-2, verbatim (`.claude/plans/d-relalg-unified-v1.md`): "D-RA-2 = A: Die kanonische Single-Table-Set-Algebra und ihre Rewrite-Regeln gehören in `lance-graph-contract`. `relalg` behält Lowering und relationale Planung. Keine allgemeine relationale AST für JC oder Quack einführen." ## 1. What exists | Capability | State | Evidence | |---|---|---| -| relalg `Rel` = All/Empty/Plane/Atom/And/Or/Not; `Measure` = Count/Sum/Min/Max/Keep over I32 lanes | SHIPPED | `crates/lance-graph-relalg/src/ir.rs:47-62`, `:99-110` | -| relalg atoms compare a lane to a constant only (`I32{lane,op,t}`, `U32{lane,eq,v}`) | SHIPPED | `crates/lance-graph-relalg/src/ir.rs:34-39` | -| relalg normalize delegates to the contract set algebra | SHIPPED | `crates/lance-graph-relalg/src/normalize.rs:23-24` | -| relalg lowers through R2IL `FoldDialect` to mask-risc; "recursion (μ) and the hop (preimage) are not built" | SHIPPED / NOT BUILT | `crates/lance-graph-relalg/src/lib.rs:19-21`, `:28-29` | -| relalg is "Not a third frontend syntax" | CHARTER | `crates/lance-graph-relalg/src/lib.rs:23-29` | +| relalg `Rel` = All/Empty/Plane/Atom/And/Or/Not; `Measure` = Count/Sum/Min/Max/Keep over I32 lanes | SHIPPED | `crates/lance-graph-relalg/src/ir.rs` | +| relalg atoms compare a lane to a constant only (`I32{lane,op,t}`, `U32{lane,eq,v}`) | SHIPPED | `crates/lance-graph-relalg/src/ir.rs` | +| relalg normalize delegates to the contract set algebra | SHIPPED | `crates/lance-graph-relalg/src/normalize.rs` | +| relalg lowers through R2IL `FoldDialect` to mask-risc; "recursion (μ) and the hop (preimage) are not built" | SHIPPED / NOT BUILT | `crates/lance-graph-relalg/src/lib.rs` | +| relalg is "Not a third frontend syntax" | CHARTER | `crates/lance-graph-relalg/src/lib.rs` | | relalg value arithmetic, matmul, nonlinear functions | NOT BUILT | BRIEF verified facts (`join_body.rs` is a GYO alpha-acyclicity check only) | -| mask-risc lanes `I32\|U32\|U64\|Strided`, no float lane | SHIPPED | `crates/lance-graph-mask-risc/src/value.rs:80-88` | -| R2IL scalar arithmetic is scalar×scalar; lane-vs-lane refused `LaneVersusLane` | SHIPPED | `crates/lance-graph-r2il/src/lib.rs:1055-1086` | -| R2IL refuses `BLEND`, `SCATTER_OR` (`Unimplemented`) and unsigned `IntLess`/`IntLessEqual` (`NoUnsignedLaneCompare`) | SHIPPED (refusals) | `crates/lance-graph-r2il/src/lib.rs:37-38`, `:47-51` | -| mask-risc `Terminal::BlendI32` kernel, not wired to relalg | LAB (kernel exists, unwired) | `crates/lance-graph-mask-risc/src/ir.rs:315-318` | -| Boolean-Distinct composition associativity certified by egglog (`admit_composition_assoc`, `prove_reassociation`, `certify_reassociation`) | SHIPPED (lab crate) | `crates/dr-math-binding-probe/src/relcomp.rs:254-262`, `:278-330`, `:421-448` | +| mask-risc lanes `I32\|U32\|U64\|Strided`, no float lane | SHIPPED | `crates/lance-graph-mask-risc/src/value.rs` | +| R2IL scalar arithmetic is scalar×scalar; lane-vs-lane refused `LaneVersusLane` | SHIPPED | `crates/lance-graph-r2il/src/lib.rs` | +| R2IL refuses `BLEND`, `SCATTER_OR` (`Unimplemented`) and unsigned `IntLess`/`IntLessEqual` (`NoUnsignedLaneCompare`) | SHIPPED (refusals) | `crates/lance-graph-r2il/src/lib.rs` | +| mask-risc `Terminal::BlendI32` kernel, not wired to relalg | LAB (kernel exists, unwired) | `crates/lance-graph-mask-risc/src/ir.rs` | +| Boolean-Distinct composition associativity certified by egglog (`admit_composition_assoc`, `prove_reassociation`, `certify_reassociation`) | SHIPPED (lab crate) | `crates/dr-math-binding-probe/src/relcomp.rs` | | Certificate reuse on fresh frames, 0 egglog calls, 7/7 | SHIPPED (lab, #1740) | `crates/dr-math-binding-probe/tests/x8_fresh_frame.rs`; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | -| DR64 register, `MethodSignature`/`Axis`, `Frame`/`Focus`/`Scope` guards | LAB | `crates/dr-math-binding-probe/src/lib.rs:46-53`, `:179-185` | -| DR256 register (`SLOTS = 256`, `Row = [u64; 4]`), `Qr`, `Composer::compose` | LAB | `crates/dir-rmap-probe/src/focus.rs:55-56`; `src/qr.rs:49-67`; `src/compose.rs:269-341` | +| DR64 register, `MethodSignature`/`Axis`, `Frame`/`Focus`/`Scope` guards | LAB | `crates/dr-math-binding-probe/src/lib.rs` | +| DR256 register (`SLOTS = 256`, `Row = [u64; 4]`), `Qr`, `Composer::compose` | LAB | `crates/dir-rmap-probe/src/focus.rs`; `src/qr.rs`; `src/compose.rs` | | Independent proof checker | BLOCKED (none exists) | BRIEF; `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` ("no independent proof checker") | | eggcc | BLOCKED (docs/.arxiv only, no code) | BRIEF | | datafrog, ascent, crepe, MORK, PathMap | LAB (deps/oracles) | BRIEF (crepe-plan-probe, lance-graph-metta, mork-pathmap-probe) | @@ -40,64 +40,64 @@ D-RA-2, verbatim (`.claude/plans/d-relalg-unified-v1.md:22`): "D-RA-2 = A: Die k | Concern | Owner surface in this repo | Source | |---|---|---| | Graph interchange | ONNX `ModelProto`/`GraphProto` read at the membrane only; no new AST | opusC B1; `onnx:docs/IR.md:35` | -| Mathematical semantics | `lance-graph-contract` set algebra (single-table); mathematical truth is the contract's | `crates/lance-graph-contract/src/set_algebra.rs:1-25`; `.claude/board/entries/2026-10-20-six-decisions.md` §2 | -| Addressing and binding | DR64 `MethodSignature`/`Axis`/`Frame`/`Focus`/`Scope` (lab); ClassView; ADMISSION = B | `crates/dr-math-binding-probe/src/lib.rs:19-53`; `.claude/plans/d-relalg-unified-v1.md:15-19` | -| Physical execution | R2IL `FoldDialect` → mask-risc; `ndarray::simd` kernels; Quack | `crates/lance-graph-relalg/src/lib.rs:19-21`; `crates/lance-graph-quack/src/lib.rs:15` | -| Learned transitions | typed methods over declared relationships, never a source of mathematical truth (operator rule in BRIEF); CausalEdge64 plasticity; ONNX `training_info` refused | BRIEF; `crates/causal-edge/src/layout.rs:38`; `onnx:docs/IR.md:110,515` | -| Proof and certification | egglog certificate for Boolean-Distinct composition only | `crates/dr-math-binding-probe/src/relcomp.rs:254-262`, `:421-448` | +| Mathematical semantics | `lance-graph-contract` set algebra (single-table); mathematical truth is the contract's | `crates/lance-graph-contract/src/set_algebra.rs`; `.claude/board/entries/2026-10-20-six-decisions.md` §2 | +| Addressing and binding | DR64 `MethodSignature`/`Axis`/`Frame`/`Focus`/`Scope` (lab); ClassView; ADMISSION = B | `crates/dr-math-binding-probe/src/lib.rs`; `.claude/plans/d-relalg-unified-v1.md` | +| Physical execution | R2IL `FoldDialect` → mask-risc; `ndarray::simd` kernels; Quack | `crates/lance-graph-relalg/src/lib.rs`; `crates/lance-graph-quack/src/lib.rs` | +| Learned transitions | typed methods over declared relationships, never a source of mathematical truth (operator rule in BRIEF); CausalEdge64 plasticity; ONNX `training_info` refused | BRIEF; `crates/causal-edge/src/layout.rs`; `onnx:docs/IR.md:110,515` | +| Proof and certification | egglog certificate for Boolean-Distinct composition only | `crates/dr-math-binding-probe/src/relcomp.rs` | ## 3. ONNX coverage matrix (family level) Facts: default domain 203 operators (155 ops + 48 functions), `ai.onnx.ml` 19; ai.onnx opset 28 is the highest with a schema; IR 14 (scoutB §2-3; `onnx:docs/Versioning.md:204` row `1.23.0|14|28|5|1`). Classes: **D** directly representable (restricted), **C** compositionally representable, **K** needs a specialized physical kernel, **P** needs a mathematical polyfill (no home), **X** external backend, **R** refused. Default for every op not named here is **R**. -Restriction for every D/C row: rank-1, length = `n_rows`, no broadcasting, int32/uint32/bool only, scalar constant right operand (opusA §1, last paragraph). Broadcasting is declared multidirectional (`onnx:docs/Operators.md:659`, `:14877`, `:20384`, `:45053`). +Restriction for every D/C row: rank-1, length = `n_rows`, no broadcasting, int32/uint32/bool only, scalar constant right operand (opusA §1, last paragraph). Broadcasting is declared multidirectional (`onnx:docs/Operators.md:659`). | Family | Class | Lands on | Semantic difference | |---|---|---|---| -| `Not`, `And`, `Or` (bool) | D | `Rel::Not/And/Or` → `Measure::Keep` → `INT_NOT/AND/OR` (`crates/lance-graph-relalg/src/lower.rs:138-141`, `:183-192`) | broadcasting refused; bytes⇄bits pack is new intake code | -| `Xor` | C | `(a∧¬b)∨(¬a∧b)`; contract `SetExpr` has no Xor variant (`crates/lance-graph-contract/src/set_algebra.rs:135-147`) | result set identical (two-valued) | -| `Equal`, `Less`, `Greater`, `LessOrEqual`, `GreaterOrEqual`, int32 vs scalar constant | D | `Atom::I32` (`crates/lance-graph-relalg/src/ir.rs:17-36`; `lower.rs:233-257`) | `LessOrEqual`/`GreaterOrEqual` are ONNX functions (`onnx:docs/Operators.md:183,191`): match by op name, do not expand. Output is a mask, not tensor(bool) bytes | -| `Equal` uint32 vs scalar | D | `Atom::U32{eq}` (`ir.rs:38`) | — | -| `Less`/`Greater` on uint32; lane-vs-lane; float/fp16/bf16/double; int8/16/64; string | R | refused `NoUnsignedLaneCompare` (`crates/lance-graph-r2il/src/lib.rs:49-50`); no float lane (`crates/lance-graph-mask-risc/src/value.rs:80-88`) | float NaN is two-valued false, not UNKNOWN: relalg's NNF `Not` push-down is unsound with NaN (opusC N1; `crates/lance-graph-relalg/tests/rewrites.rs:452`, `:314`). Float comparisons do not enter `Rel`/`SetExpr` | -| `ReduceSum` int32, all axes | C, only in the non-overflow domain | `Measure::Sum` → `Answer::Sum(i64)` (`lower.rs:121-125`, `:26`) | three overflow semantics: ONNX output dtype = input dtype (`onnx:docs/Operators.md:32053-32054`); reference wraps (`onnx:onnx/reference/ops/op_reduce_sum.py:26`); onnxruntime 1.29.0 observed saturating (mechanism OPEN); relalg widens to i64. Out-of-i32 result → refusal `OverflowDomain` | -| `ReduceSum` partial axes; uint32/int64/float | R | Sum is I32-lane only (`ir.rs:103`) | — | -| `ReduceMin`/`ReduceMax` int32, all axes | C | `Measure::Min/Max` → `Option` (`lower.rs:126-137`, `:28-30`) | empty reduction: ONNX yields dtype max/min (`onnx:docs/Operators.md:31444`; `onnx:onnx/reference/ops/op_reduce_min.py:38-44`); adapter `None → i32::MAX/MIN`. Float NaN propagation not representable | -| `ReduceSum(Cast(cond, INT64))` row-count pattern | C | `Measure::Count` → `POP_COUNT` (`lower.rs:117-120`) | exact 2-node pattern; output int64 | -| `Where` | K (blocked) | `Terminal::BlendI32` (`crates/lance-graph-mask-risc/src/ir.rs:315-318`); R2IL refuses `BLEND` (`crates/lance-graph-r2il/src/lib.rs:37-38`) | I32 lanes, lane-vs-lane, value-producing; outside `Rel` | -| `Gather`, `GatherElements`, `GatherND`, `ScatterElements` and other Scatter*, `NonZero`, `Unique`, `Compress`, `TopK` indices, any index-tensor input | R (ADMISSION B) | none | value-derived addressing: `onnx:docs/Operators.md:15895` (Gather), `:36661-36667` (ScatterElements), `:26543-26544` (NonZero), `:44310-44316` (Unique). ADMISSION = B: "A position derived from another relational column or table is not admissible as a read address" (`.claude/board/entries/2026-10-20-six-decisions.md` §1). `Compress` writes compacted values; `Keep` writes a mask only (`ir.rs:108-109`) | -| `Add/Sub/Mul/Div/Mod/Pow/Neg/Abs`, elementwise | P | none (R2IL arithmetic is scalar×scalar; `INT_SUB` unchecked at `crates/lance-graph-r2il/src/lib.rs:1080`, ADD/MULT checked at `:1063-1064`) | home OPEN (OP-ONNX-1) | -| `MatMul`, `Gemm`, `Einsum` | K / X | `ndarray::simd::gemm_f64_tiled` is f64 only (ndarray `src/simd.rs:684-697`); f32 delegates to the external `matrixmultiply` crate (`:690`) | ONNX `MatMul` is a sum-product over numeric dtypes, not Boolean composition; no float law is admitted (§4). Boolean relation composition is `relcomp::compose`, which no ONNX op names | -| `Exp`, `Log`, `Tanh`, `Sigmoid`, `Erf`, trig | P | `simd_exp_f32` is a clamped approximation, `#[allow(dead_code)]` (ndarray `src/simd.rs:540-552`); `simd_ln_f32` is a scalar loop (`:610-615`) | numpy ULP semantics are not identical; no `tanh` found (grep only) | +| `Not`, `And`, `Or` (bool) | D | `Rel::Not/And/Or` → `Measure::Keep` → `INT_NOT/AND/OR` (`crates/lance-graph-relalg/src/lower.rs`) | broadcasting refused; bytes⇄bits pack is new intake code | +| `Xor` | C | `(a∧¬b)∨(¬a∧b)`; contract `SetExpr` has no Xor variant (`crates/lance-graph-contract/src/set_algebra.rs`) | result set identical (two-valued) | +| `Equal`, `Less`, `Greater`, `LessOrEqual`, `GreaterOrEqual`, int32 vs scalar constant | D | `Atom::I32` (`crates/lance-graph-relalg/src/ir.rs`; `lower.rs`) | `LessOrEqual`/`GreaterOrEqual` are ONNX functions (`onnx:docs/Operators.md:183,191`): match by op name, do not expand. Output is a mask, not tensor(bool) bytes | +| `Equal` uint32 vs scalar | D | `Atom::U32{eq}` (`ir.rs`) | — | +| `Less`/`Greater` on uint32; lane-vs-lane; float/fp16/bf16/double; int8/16/64; string | R | refused `NoUnsignedLaneCompare` (`crates/lance-graph-r2il/src/lib.rs`); no float lane (`crates/lance-graph-mask-risc/src/value.rs`) | float NaN is two-valued false, not UNKNOWN: relalg's NNF `Not` push-down is unsound with NaN (opusC N1; `crates/lance-graph-relalg/tests/rewrites.rs`). Float comparisons do not enter `Rel`/`SetExpr` | +| `ReduceSum` int32, all axes | C, only in the non-overflow domain | `Measure::Sum` → `Answer::Sum(i64)` (`lower.rs`) | three overflow semantics: ONNX output dtype = input dtype (`onnx:docs/Operators.md:32053-32054`); reference wraps (`onnx:onnx/reference/ops/op_reduce_sum.py:26`); onnxruntime 1.29.0 observed saturating (mechanism OPEN); relalg widens to i64. Out-of-i32 result → refusal `OverflowDomain` | +| `ReduceSum` partial axes; uint32/int64/float | R | Sum is I32-lane only (`ir.rs`) | — | +| `ReduceMin`/`ReduceMax` int32, all axes | C | `Measure::Min/Max` → `Option` (`lower.rs`) | empty reduction: ONNX yields dtype max/min (`onnx:docs/Operators.md:31444`; `onnx:onnx/reference/ops/op_reduce_min.py:38-44`); adapter `None → i32::MAX/MIN`. Float NaN propagation not representable | +| `ReduceSum(Cast(cond, INT64))` row-count pattern | C | `Measure::Count` → `POP_COUNT` (`lower.rs`) | exact 2-node pattern; output int64 | +| `Where` | K (blocked) | `Terminal::BlendI32` (`crates/lance-graph-mask-risc/src/ir.rs`); R2IL refuses `BLEND` (`crates/lance-graph-r2il/src/lib.rs`) | I32 lanes, lane-vs-lane, value-producing; outside `Rel` | +| `Gather`, `GatherElements`, `GatherND`, `ScatterElements` and other Scatter*, `NonZero`, `Unique`, `Compress`, `TopK` indices, any index-tensor input | R (ADMISSION B) | none | value-derived addressing: `onnx:docs/Operators.md:15895` (Gather) (ScatterElements) (NonZero) (Unique). ADMISSION = B: "A position derived from another relational column or table is not admissible as a read address" (`.claude/board/entries/2026-10-20-six-decisions.md` §1). `Compress` writes compacted values; `Keep` writes a mask only (`ir.rs`) | +| `Add/Sub/Mul/Div/Mod/Pow/Neg/Abs`, elementwise | P | none (R2IL arithmetic is scalar×scalar; `INT_SUB` unchecked at `crates/lance-graph-r2il/src/lib.rs`, ADD/MULT checked at) | home OPEN (OP-ONNX-1) | +| `MatMul`, `Gemm`, `Einsum` | K / X | `ndarray::simd::gemm_f64_tiled` is f64 only (ndarray `src/simd.rs`); f32 delegates to the external `matrixmultiply` crate | ONNX `MatMul` is a sum-product over numeric dtypes, not Boolean composition; no float law is admitted (§4). Boolean relation composition is `relcomp::compose`, which no ONNX op names | +| `Exp`, `Log`, `Tanh`, `Sigmoid`, `Erf`, trig | P | `simd_exp_f32` is a clamped approximation, `#[allow(dead_code)]` (ndarray `src/simd.rs`); `simd_ln_f32` is a scalar loop | numpy ULP semantics are not identical; no `tanh` found (grep only) | | `Mish`, `Gelu`, `Softmax`, `Relu`, `LayerNormalization` (48 Function-table rows, `onnx:docs/Operators.md:169-218`) | P | bottoms out in Exp/Tanh/Log/Mul | functions may be inlined (`onnx:docs/IR.md:35`) | | `Shape`, `Size`, `Reshape`, `Squeeze`, `Unsqueeze`, `Flatten`, `Identity`, `Constant` | OPEN | none | intake-time folding possible; unverified | | `If`, `Loop`, `Scan`, `Sequence*`, `Optional*`, `String*`, `Random*`, `ImageDecoder`, `Quantize/Dequantize*`, `Conv*`, `*Pool`, RNN/LSTM/GRU, `ai.onnx.ml.*` | R / X | none | control flow and subgraphs are a computational-graph format (`onnx:docs/IR.md:35,181-212`) | -**Per-op admission table (opusC B2).** Each ONNX op is classed CO-ADDRESSED (element-wise, `Not/And/Or`, `Equal` over same-table lanes) / SAME-TABLE-SEEK-UNDER-B (only with an `attest_cost` witness, which has no contract type yet: `.claude/board/ISSUES.md:23-45`) / REFUSED. Default is REFUSED. +**Per-op admission table (opusC B2).** Each ONNX op is classed CO-ADDRESSED (element-wise, `Not/And/Or`, `Equal` over same-table lanes) / SAME-TABLE-SEEK-UNDER-B (only with an `attest_cost` witness, which has no contract type yet: `.claude/board/ISSUES.md`) / REFUSED. Default is REFUSED. ## 4. Intake: what must survive, and how to word compatibility Fields that must survive (proto2, `onnx:onnx/onnx.proto:9`). Missing or unknown identity/version → refuse, never default: -- Identity/version: `ModelProto.ir_version` `:453`; `opset_import` `:463` → `OperatorSetIdProto.domain` `:949`, `.version` `:953`; `NodeProto.op_type` `:233`, `.domain` `:235`, `.overload` `:237`. The (domain, opset) resolution rule is OPEN (not read). -- Local functions: `ModelProto.functions` `:522` → `FunctionProto.name` `:965`, `domain` `:1013`, `overload` `:1017`, `opset_import` `:1009`, `attribute`/`attribute_proto` `:983`/`:989`, `node` `:992`, `value_info` `:1023`. -- Types/shapes: `ValueInfoProto.type` `:210` → `TypeProto.Tensor.elem_type` `:860`, `shape` `:861`; `Dimension.dim_value`/`dim_param`/`denotation` `:838-846`. A symbolic `dim_param` must bind to the table's `n_rows`, or refuse. -- Tensors: `GraphProto.initializer` `:576`, `sparse_initializer` `:579`; `TensorProto.dims` `:673`, `data_type` `:677`, `raw_data` `:766`, `external_data` `:777`, `data_location` `:788`. -- Attributes: `AttributeProto.name` `:164`, `type` `:181`, `ref_attr_name` `:170`, values `:184-200`. Unknown attribute on a known op → refuse. -- Annotations round-trip, not dropped: `metadata_props` (Model `:493`, Graph `:599`, Node `:246`, ValueInfo `:214`, Tensor `:805`, Function `:1026`); `doc_string` (Model `:487`, Graph `:582`, Node `:243`, ValueInfo `:212`, Attribute `:173`, Tensor `:741`, Function `:994`); `producer_name/version` `:468`/`:473`; `quantization_annotation` `:596`. -- `training_info` is refused on import (opusC N5; `onnx:docs/IR.md:110,515`). No initializer value is ever a law premise: initializers are data; laws are `AdmittedLaw` values (`crates/dr-math-binding-probe/src/relcomp.rs:254`). +- Identity/version: `ModelProto.ir_version`; `opset_import` → `OperatorSetIdProto.domain`, `.version`; `NodeProto.op_type`, `.domain`, `.overload`. The (domain, opset) resolution rule is OPEN (not read). +- Local functions: `ModelProto.functions` → `FunctionProto.name`, `domain`, `overload`, `opset_import`, `attribute`/`attribute_proto`/, `node`, `value_info`. +- Types/shapes: `ValueInfoProto.type` → `TypeProto.Tensor.elem_type`, `shape`; `Dimension.dim_value`/`dim_param`/`denotation`. A symbolic `dim_param` must bind to the table's `n_rows`, or refuse. +- Tensors: `GraphProto.initializer`, `sparse_initializer`; `TensorProto.dims`, `data_type`, `raw_data`, `external_data`, `data_location`. +- Attributes: `AttributeProto.name`, `type`, `ref_attr_name`, values. Unknown attribute on a known op → refuse. +- Annotations round-trip, not dropped: `metadata_props` (Model, Graph, Node, ValueInfo, Tensor, Function); `doc_string` (Model, Graph, Node, ValueInfo, Attribute, Tensor, Function); `producer_name/version`/; `quantization_annotation`. +- `training_info` is refused on import (opusC N5; `onnx:docs/IR.md:110,515`). No initializer value is ever a law premise: initializers are data; laws are `AdmittedLaw` values (`crates/dr-math-binding-probe/src/relcomp.rs`). -Typed refusal shape (proposal modelled on `RelError`, `crates/lance-graph-relalg/src/lower.rs:49-54`, and `FoldError`, `crates/lance-graph-r2il/src/lib.rs:201`): `Refusal { node: u32, domain, op_type, opset: i64, reason }`, `reason` ∈ {UnknownDomain, OpsetUnsupported, UnsupportedOp, UnsupportedDtype(elem_type), Broadcast, RankNotOne, DimUnbound(dim_param), UnknownAttribute(name), OverflowDomain, NoUnsignedCompare, ControlFlow, ExternalData, TrainingInfo, ValueIndexedAddress}. Whether strings may enter the contract is OPEN (`crates/lance-graph-relalg/src/ir.rs:1-4` forbids strings in the IR). Never coerce, never partial-run. Whole-graph versus per-node refusal is OPEN. +Typed refusal shape (proposal modelled on `RelError`, `crates/lance-graph-relalg/src/lower.rs`, and `FoldError`, `crates/lance-graph-r2il/src/lib.rs`): `Refusal { node: u32, domain, op_type, opset: i64, reason }`, `reason` ∈ {UnknownDomain, OpsetUnsupported, UnsupportedOp, UnsupportedDtype(elem_type), Broadcast, RankNotOne, DimUnbound(dim_param), UnknownAttribute(name), OverflowDomain, NoUnsignedCompare, ControlFlow, ExternalData, TrainingInfo, ValueIndexedAddress}. Whether strings may enter the contract is OPEN (`crates/lance-graph-relalg/src/ir.rs` forbids strings in the IR). Never coerce, never partial-run. Whole-graph versus per-node refusal is OPEN. **Wording rule (opusC N2).** Do not write "ONNX-compatible". The ONNX IR says "An implementation must support all operators in the set or reject the model" (`onnx:docs/IR.md:80`) and lists "operators that all implementations MUST support" (`onnx:docs/IR.md:67`). The claim is: "ONNX-subset reader that refuses everything else" — it imports IR ≤14, ai.onnx opset N, the listed op subset, and rejects any model whose `opset_import` names an op outside it. "Compatible" is unearned without upstream backend tests per claimed op (`onnx:docs/OnnxBackendTest.md`). -**No float law.** No float law is admitted. Float ONNX ops lower only as written (fixed evaluation order, analogue of `run_as_written`, `crates/lance-graph-relalg/src/lower.rs:96`) or are refused. Reassociation is admitted for Boolean-Distinct relations only (#1707). The egglog rule set is structural (`crates/dr-math-binding-probe/src/relcomp.rs:283-285`); its soundness rests on OR/AND associativity, which IEEE-754 `+`/`*` lack. No ONNX statement fixing a float summation order was found (OPEN). +**No float law.** No float law is admitted. Float ONNX ops lower only as written (fixed evaluation order, analogue of `run_as_written`, `crates/lance-graph-relalg/src/lower.rs`) or are refused. Reassociation is admitted for Boolean-Distinct relations only (#1707). The egglog rule set is structural (`crates/dr-math-binding-probe/src/relcomp.rs`); its soundness rests on OR/AND associativity, which IEEE-754 `+`/`*` lack. No ONNX statement fixing a float summation order was found (OPEN). **No ONNX-level rewrite pass (opusC C1).** No ONNX graph optimizer (constant folding, fusion, shape-inference passes) and no ONNX interpreter beside mask-risc. The only rewrites are contract set-algebra and egglog-admitted laws. -**Palette256 (opusC N4).** ONNX ops never consume or produce Palette256 values except as opaque u8 codes passed through. Forbidden conversions: Palette256 → float to feed an ONNX op; a stored Fisher-z or cosine column produced by an ONNX graph; a generic ONNX distance op over u8 codes (`.claude/board/ISSUES.md:3629-3651`). Codebook attestation has no contract type yet (`.claude/board/ISSUES.md:23-45`). +**Palette256 (opusC N4).** ONNX ops never consume or produce Palette256 values except as opaque u8 codes passed through. Forbidden conversions: Palette256 → float to feed an ONNX op; a stored Fisher-z or cosine column produced by an ONNX graph; a generic ONNX distance op over u8 codes (`.claude/board/ISSUES.md`). Codebook attestation has no contract type yet (`.claude/board/ISSUES.md`). ## 5. Importer dependency options — OPEN for the operator; no decision -Facts: nothing in the repo parses ONNX. `prost = "0.13"` is optional in `crates/cognitive-shader-driver/Cargo.toml:255`, enabled only by feature `grpc` (`:282`), under a "NEVER in production binary" comment (`:250`). `protoc` 3.21.12 is installed in the container (`/usr/bin/protoc`). +Facts: nothing in the repo parses ONNX. `prost = "0.13"` is optional in `crates/cognitive-shader-driver/Cargo.toml`, enabled only by feature `grpc`, under a "NEVER in production binary" comment. `protoc` 3.21.12 is installed in the container (`/usr/bin/protoc`). | Option | Cost | Risk | |---|---|---| @@ -111,24 +111,24 @@ Correction to the brief (opusA §5): onnxruntime 1.29.0 IS installed in the cont ## 6. DR64³ / DR256³ -**Original plan: NOT FOUND.** Negative-search evidence (BRIEF): no `DR64³`, `DR256³`, `64×64×64` or `64x64x64` string anywhere in the repo (`grep -rIl`, 0 files). Branch `ccr-e97e5d58-1bkumg-cartesian12` is CartesianAddress12/Quad8 shader work, not the plan. GitHub PR search "cartesian": 23 PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. `.claude/knowledge/delta-card-addressing-integration-map.md:212` has an "18-bit hot envelope = 262,144 ... CONCURRENT mailbox working set", a working-set size and not a DR64³ identity. 262,144 = 2¹⁸ coincides arithmetically; the coincidence licenses nothing and no 18-bit DR64³ identity is defined. +**Original plan: NOT FOUND.** Negative-search evidence (BRIEF): no `DR64³`, `DR256³`, `64×64×64` or `64x64x64` string anywhere in the repo (`grep -rIl`, 0 files). Branch `ccr-e97e5d58-1bkumg-cartesian12` is CartesianAddress12/Quad8 shader work, not the plan. GitHub PR search "cartesian": 23 PRs, none is a DR64³ plan. The 12-stage PR sequence is not found. `.claude/knowledge/delta-card-addressing-integration-map.md` has an "18-bit hot envelope = 262,144 ... CONCURRENT mailbox working set", a working-set size and not a DR64³ identity. 262,144 = 2¹⁸ coincides arithmetically; the coincidence licenses nothing and no 18-bit DR64³ identity is defined. -**What DR64 and DR256 are today:** DR64 `Operand { rows: &[u64; 64], validity }` (`crates/dr-math-binding-probe/src/lib.rs:192-195`), composition `relcomp::compose` (`relcomp.rs:211-222`), `Chain` guards (`relcomp.rs:136-173`). DR256 `Row = [u64; 4]` (`crates/dir-rmap-probe/src/focus.rs:55-56`), `Composer::compose` (`compose.rs:269-341`), guard by `prep::Witness` (`prep.rs:71-85`), no `MethodSignature`/`Axis` typing. +**What DR64 and DR256 are today:** DR64 `Operand { rows: &[u64; 64], validity }` (`crates/dr-math-binding-probe/src/lib.rs`), composition `relcomp::compose` (`relcomp.rs`), `Chain` guards (`relcomp.rs`). DR256 `Row = [u64; 4]` (`crates/dir-rmap-probe/src/focus.rs`), `Composer::compose` (`compose.rs`), guard by `prep::Witness` (`prep.rs`), no `MethodSignature`/`Axis` typing. **NEW PROPOSAL (from opusB §2), not recovered history.** "DR64³" is the logical index cube X×Y×Z (64 each) over which a contraction of typed DR64 views ranges. It is never a stored object. -- (R1) Chain contraction `R: X→Y`, `S: Y→Z`, `(R∘S)[i,k] = ∃j R[i,j] ∧ S[j,k]`. This is `relcomp::compose` today (`relcomp.rs:211-222`); nothing is new except the name. -- (R2) Triangle `(R∘S) ∧ Q` with `Q: X→Z`. Needs one new check not in `Chain` (adjacency only, `relcomp.rs:161-165`): `Q.row == R.row` and `Q.column == S.column`. Whether it belongs in `Chain` or a separate admission type: OPEN. -- Guards applying unchanged: same frame issue and still current (`lib.rs:123-140`, `relcomp.rs:151,166`), same focus (`:154`), same scope (`:157`), domain adjacency (`:161-165`), TwoValued + Distinct only (`:148`, `lib.rs:255`), only `BooleanCompose` admitted (`:254-262`). -- Not allowed: a new identity encoding (no packed `(i,j,k)` id); any CausalEdge64 change (S/P/O bytes are palette indices, `crates/causal-edge/src/edge.rs:141-143`); a new executor; a gather-shaped hop (`crates/lance-graph-mask-risc/src/graph_hop.rs:1-13`); Bag through the DR64 binder (`lib.rs:255`); any claim that 64³ is implemented. +- (R1) Chain contraction `R: X→Y`, `S: Y→Z`, `(R∘S)[i,k] = ∃j R[i,j] ∧ S[j,k]`. This is `relcomp::compose` today (`relcomp.rs`); nothing is new except the name. +- (R2) Triangle `(R∘S) ∧ Q` with `Q: X→Z`. Needs one new check not in `Chain` (adjacency only, `relcomp.rs`): `Q.row == R.row` and `Q.column == S.column`. Whether it belongs in `Chain` or a separate admission type: OPEN. +- Guards applying unchanged: same frame issue and still current (`lib.rs`, `relcomp.rs`), same focus, same scope, domain adjacency, TwoValued + Distinct only (`lib.rs`), only `BooleanCompose` admitted. +- Not allowed: a new identity encoding (no packed `(i,j,k)` id); any CausalEdge64 change (S/P/O bytes are palette indices, `crates/causal-edge/src/edge.rs`); a new executor; a gather-shaped hop (`crates/lance-graph-mask-risc/src/graph_hop.rs`); Bag through the DR64 binder (`lib.rs`); any claim that 64³ is implemented. - Sizes, arithmetic only, computed not measured: 64³ bits = 262,144 bits = 32 KiB; 256³ bits = 16,777,216 bits = 2 MiB. The cube must not be materialized; no measurement shows it cheaper (OPEN). No throughput figure is given for either. -**OPEN tension (bit-position scan).** `relcomp::compose` scans set bits for positions (`trailing_zeros`, `crates/dr-math-binding-probe/src/relcomp.rs:215-218`) and DR256 `compose` does the same (`crates/dir-rmap-probe/src/compose.rs:239-247`, `:304`, `:315`), while `crates/dir-rmap-probe/src/qr.rs:21-23` states "no loop scans set bits for a position (the D-RU-6 address rule)". Whether position-scanning inside one co-addressed frame is the forbidden gather (ADMISSION B, `.claude/board/ISSUES.md:26`) is not ruled anywhere found. +**OPEN tension (bit-position scan).** `relcomp::compose` scans set bits for positions (`trailing_zeros`, `crates/dr-math-binding-probe/src/relcomp.rs`) and DR256 `compose` does the same (`crates/dir-rmap-probe/src/compose.rs`), while `crates/dir-rmap-probe/src/qr.rs` states "no loop scans set bits for a position (the D-RU-6 address rule)". Whether position-scanning inside one co-addressed frame is the forbidden gather (ADMISSION B, `.claude/board/ISSUES.md`) is not ruled anywhere found. -**DR256³ preconditions (opusB §5), none met:** DR64³ R1/R2 pass the S3 arms with the R2IL arm measured; a DR256 binder with DR64 typing (`prep.rs:71-85`); a certificate route at 256 (no egglog dep in `dir-rmap-probe`); materialization stays refused (precedent `crates/cognitive-shader-driver/src/immaterial_needle.rs:55-67`); `TooLarge` (`qr.rs:94-96`) refuses on every axis; CausalEdge64 S/P/O bytes are not DR256³ coordinates; cross-width transfer (256 → 64) has no code, only DR64→DR64 reuse exists (#1740). +**DR256³ preconditions (opusB §5), none met:** DR64³ R1/R2 pass the S3 arms with the R2IL arm measured; a DR256 binder with DR64 typing (`prep.rs`); a certificate route at 256 (no egglog dep in `dir-rmap-probe`); materialization stays refused (precedent `crates/cognitive-shader-driver/src/immaterial_needle.rs`); `TooLarge` (`qr.rs`) refuses on every axis; CausalEdge64 S/P/O bytes are not DR256³ coordinates; cross-width transfer (256 → 64) has no code, only DR64→DR64 reuse exists (#1740). ## 7. Stages -"Proof engine" values: egglog-certified (only `LawShape::BooleanCompose`), differential test (oracle named), none. "Certified" may appear only in the first case (opusC B4). The operator rule names egglog, eggcc, datafrog, ascent and MeTTa over MORK over a PathMap oracle as the engines a proof may come from. Today only egglog produces a proof object in this repo. eggcc has no code. datafrog and Ascent are dev-dependency oracles here and emit no provenance; their tuple-comparison oracle role was withdrawn on 2026-10-21 (`.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md:64-65`). A stage that wants them as its proof engine must first show what proof object they produce (OPEN, OP-ONNX-14). +"Proof engine" values: egglog-certified (only `LawShape::BooleanCompose`), differential test (oracle named), none. "Certified" may appear only in the first case (opusC B4). The operator rule names egglog, eggcc, datafrog, ascent and MeTTa over MORK over a PathMap oracle as the engines a proof may come from. Today only egglog produces a proof object in this repo. eggcc has no code. datafrog and Ascent are dev-dependency oracles here and emit no provenance; their tuple-comparison oracle role was withdrawn on 2026-10-21 (`.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md`). A stage that wants them as its proof engine must first show what proof object they produce (OPEN, OP-ONNX-14). | Stage | Deliverable | Gate | Proof engine | Prerequisite | Status | |---|---|---|---|---|---| @@ -147,32 +147,32 @@ The 64³ Explore → 256³ Validate → Certified Method → 64³ Reuse progress - Silent twin: every positive graph yields zero refusals; in-range `ReduceSum` does not raise `OverflowDomain`; `metadata_props`/`doc_string` still lower and round-trip unchanged. - Disable runs (commit first, assert the patch applied): `Less→Le`; drop the dtype check; map empty Min `None→0`; delete the overflow guard; skip `Not`. Each must turn a named test red. -**S3 falsifier (opusB §4).** Fixture: three bound DR64 views on one `FrameStore` seal, one focus, one scope, axes X→Y→Z(→W); seeded fill as `crates/dr-math-binding-probe/tests/relcomp.rs:61`. Arms, bit-exact over all 64 rows: (1) `Chain::eval` over every order (`relcomp.rs:184-201`); (2) a co-addressed R2IL program (`exists(intersect(R_row_i, S_col_k))`, needs `S` transposed first, a preparation cost reported separately per D-RU-6, `.claude/plans/d-relalg-unified-v1.md:205`), which does not exist; (3) an independent scalar pair-enumeration oracle (`tests/relcomp.rs:78-91`), a differential test; (4) reassociation equality via the egglog certificate only (`relcomp.rs:421-448`). Costs reported separately (bind; transpose; steady contraction; result materialization; cold egglog) in ns/µs only. Refusals needing can-fire and can-stay-silent cases: `DifferentFrame` (`relcomp.rs:151-153`), `StaleFrame` (`:166-168`), `DomainMismatch` (`:161-165`), `BagNeedsMultiplicity` (`lib.rs:255-257`), focus/scope moved (`relcomp.rs:154-159`), `NotThisChain` (`:185-187`), and the R2 closing-view axis mismatch (does not exist; must be added and disable-verified). +**S3 falsifier (opusB §4).** Fixture: three bound DR64 views on one `FrameStore` seal, one focus, one scope, axes X→Y→Z(→W); seeded fill as `crates/dr-math-binding-probe/tests/relcomp.rs`. Arms, bit-exact over all 64 rows: (1) `Chain::eval` over every order (`relcomp.rs`); (2) a co-addressed R2IL program (`exists(intersect(R_row_i, S_col_k))`, needs `S` transposed first, a preparation cost reported separately per D-RU-6, `.claude/plans/d-relalg-unified-v1.md`), which does not exist; (3) an independent scalar pair-enumeration oracle (`tests/relcomp.rs`), a differential test; (4) reassociation equality via the egglog certificate only (`relcomp.rs`). Costs reported separately (bind; transpose; steady contraction; result materialization; cold egglog) in ns/µs only. Refusals needing can-fire and can-stay-silent cases: `DifferentFrame` (`relcomp.rs`), `StaleFrame`, `DomainMismatch`, `BagNeedsMultiplicity` (`lib.rs`), focus/scope moved (`relcomp.rs`), `NotThisChain`, and the R2 closing-view axis mismatch (does not exist; must be added and disable-verified). ## 8. What ONNX reuse eliminates, and what it does not -- ONNX replaces at most an interchange AST. It does not remove the proof-side term language: egglog needs its own datatype (`crates/dr-math-binding-probe/src/relcomp.rs:283-285`) and ONNX has no rewrite or proof semantics (opusC N7). +- ONNX replaces at most an interchange AST. It does not remove the proof-side term language: egglog needs its own datatype (`crates/dr-math-binding-probe/src/relcomp.rs`) and ONNX has no rewrite or proof semantics (opusC N7). - The #1741 Julia-map conclusions P-J1..P-J4 stay open: typed egglog rules via the Rust API, keep `ProofStore`, a standalone replay checker (entry `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md`). X4 (rules as typed values) and X12 (keep the proof DAG) are proof-side work ONNX does not touch. Anchor A2 ("internal proof representation chosen by measurement") is not pre-decided as "ONNX + relalg" and remains open (same entry). -- Certificate reuse is shown only for `source` changes with the same focus, scope and ABI (`crates/dr-math-binding-probe/tests/x8_fresh_frame.rs:17-19,40-46`); refusals at `:211`, `:226`, `:245`. +- Certificate reuse is shown only for `source` changes with the same focus, scope and ABI (`crates/dr-math-binding-probe/tests/x8_fresh_frame.rs`); refusals at. ## 9. Open-points register | ID | Question | Owner | Dependency | Evidence | Falsifier | Decision | Status | |---|---|---|---|---|---|---|---| -| OP-ONNX-1 | Home for value maths (arithmetic, MatMul, Exp/Tanh/Mish): relalg cannot take it without a new IR | operator | none | opusA §2; D-RA-2 `.claude/plans/d-relalg-unified-v1.md:22`; `crates/lance-graph-relalg/src/lib.rs:25-29` | any proposal adding value-producing nodes to `Rel` | none | OPEN | +| OP-ONNX-1 | Home for value maths (arithmetic, MatMul, Exp/Tanh/Mish): relalg cannot take it without a new IR | operator | none | opusA §2; D-RA-2 `.claude/plans/d-relalg-unified-v1.md`; `crates/lance-graph-relalg/src/lib.rs` | any proposal adding value-producing nodes to `Rel` | none | OPEN | | OP-ONNX-2 | Importer dependency (options A-E) | operator | OP-ONNX-1 for scope | §5 above | S1 reads real ONNX bytes | none | OPEN | | OP-ONNX-3 | DR64³/DR256³ original plan missing | operator | none | §6 negative search (BRIEF) | the plan is located | none | OPEN | -| OP-ONNX-4 | Does bit-position scanning in one co-addressed frame violate ADMISSION B / D-RU-6? | operator | none | `relcomp.rs:215-218`; `compose.rs:239-247`; `qr.rs:21-23`; `.claude/board/ISSUES.md:26` | a ruling | none | OPEN | +| OP-ONNX-4 | Does bit-position scanning in one co-addressed frame violate ADMISSION B / D-RU-6? | operator | none | `relcomp.rs`; `compose.rs`; `qr.rs`; `.claude/board/ISSUES.md` | a ruling | none | OPEN | | OP-ONNX-5 | Independent proof checker; none exists | plan owner | #1741 P-J4 | `.claude/board/entries/2026-10-23-drmc-l1-x8-fresh-frame-result.md` | a replay checker that rejects a tampered proof | none | OPEN | -| OP-ONNX-6 | Cross-focus/scope/ABI rebinding of certificates beyond #1740 | plan owner | S3 | `tests/x8_fresh_frame.rs:17-19,40-46`; opusC N3 | reuse across stores with different focus/scope/geometry | none | OPEN | +| OP-ONNX-6 | Cross-focus/scope/ABI rebinding of certificates beyond #1740 | plan owner | S3 | `tests/x8_fresh_frame.rs`; opusC N3 | reuse across stores with different focus/scope/geometry | none | OPEN | | OP-ONNX-7 | Prover revision not recorded in the certificate (egglog `branch = "main"`). Floating deps are per repo pin policy, so this is a certificate-identity gap, not a dependency defect | plan owner | none | `crates/dr-math-binding-probe/Cargo.toml`; opusC N3 | certificate carries the egglog revision | none | OPEN | | OP-ONNX-8 | Why onnxruntime 1.29.0 saturates int32 `ReduceSum` (observed in 2 cases) | S1 | S1 | opusA §5 | a third case or the kernel source | none | OPEN | -| OP-ONNX-9 | `.claude/plans/dr-mathematical-compiler-v1.md:79` calls egglog's self-check "independent" (wording defect) | owner of that plan | none | `relcomp.rs:269,290` ("egglog checks every proof it returns") | the wording is corrected | none | OPEN | -| OP-ONNX-10 | `.claude/plans/dr-mathematical-compiler-v1.md:19` "RelAlg/typed AST expresses admissible mathematics" versus D-RA-2; whether it predates 2026-10-20 | owner of that plan | OP-ONNX-1 | opusC B1 | the plan line is reconciled | none | OPEN | +| OP-ONNX-9 | `.claude/plans/dr-mathematical-compiler-v1.md` calls egglog's self-check "independent" (wording defect) | owner of that plan | none | `relcomp.rs` ("egglog checks every proof it returns") | the wording is corrected | none | OPEN | +| OP-ONNX-10 | `.claude/plans/dr-mathematical-compiler-v1.md` "RelAlg/typed AST expresses admissible mathematics" versus D-RA-2; whether it predates 2026-10-20 | owner of that plan | OP-ONNX-1 | opusC B1 | the plan line is reconciled | none | OPEN | | OP-ONNX-11 | R2 closing-view typing check: in `Chain` or a separate admission type | S3 | S3 | opusB §2 | disable-verified refusal | none | OPEN | -| OP-ONNX-12 | `observe_focus` omits a scope refusal; intended? | plan owner | none | `crates/dr-math-binding-probe/src/population.rs:45-58` | a ruling | none | OPEN | -| OP-ONNX-14 | Which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce, so they can serve as a stage's proof engine | operator | none | `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md:64-65,94` | an exported, replayable derivation | none | OPEN | -| OP-ONNX-13 | Whole-graph versus per-node refusal; strings in the contract | operator | S1 | §4; `ir.rs:1-4` | a ruling | none | OPEN | +| OP-ONNX-12 | `observe_focus` omits a scope refusal; intended? | plan owner | none | `crates/dr-math-binding-probe/src/population.rs` | a ruling | none | OPEN | +| OP-ONNX-14 | Which proof object datafrog, Ascent or MeTTa/MORK/PathMap would produce, so they can serve as a stage's proof engine | operator | none | `.claude/board/entries/2026-10-23-coresearch-julia-egraphs.md` | an exported, replayable derivation | none | OPEN | +| OP-ONNX-13 | Whole-graph versus per-node refusal; strings in the contract | operator | S1 | §4; `ir.rs` | a ruling | none | OPEN | ## 10. Housekeeping @@ -180,7 +180,7 @@ SAFE NOW (done in this PR, commits `7fa35361` and `83945785`): D-TGA-5D status; SEPARATE PR: none identified. -BLOCKED: D-DRMC rows missing from STATUS_BOARD (owner CC2, ask on EXO-50); the `dr-mathematical-compiler-v1.md:79` wording fix (plan owner; OP-ONNX-9). +BLOCKED: D-DRMC rows missing from STATUS_BOARD (owner CC2, ask on EXO-50); the `dr-mathematical-compiler-v1.md` wording fix (plan owner; OP-ONNX-9). ## 11. Next gate