diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 229b5e7f9..3c99897de 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,6 @@ +## 2026-10-23 — d-native-repr-contract-v1 + d-native-first-dependency-correction-v1 — the native polyfill is the root → `.claude/plans/d-native-repr-contract-v1.md`, `.claude/plans/d-native-first-dependency-correction-v1.md` + +**Status:** D-NFR-0 / D-NFC-0 documentation (DECISION 2026-10-23: corrections to #1746–#1751 and #1750 approved). D-NFR-1..5 PROPOSED, not authorized. ONNX is an external compatibility specification; the R2IL polyfill is the native root; Quack binding + DR64³ + Palette256³ is the intended native representation, with its shipped, lab and missing seams separated. The smallest missing seam is that a Quack-bound query does not know its frame. The #1744 / #1745 / #1750 S0 dispute is not decided. ## 2026-10-23 — d-mpf-math-polyfill-v1 — the mathematical polyfill API, Stage 1 → `.claude/plans/d-mpf-math-polyfill-v1.md` **Status:** D-MPF-1 MEASURED, lab only; D-MPF-2.. PROPOSED. The Stage 1 polyfill API is the shipped R2IL procedure layer plus checked scalar arithmetic over mask-risc, with relalg as the rewriting frontend; no new primitive. One expression matches an independent row loop; at 64 K rows it costs under 1 ns/row, at one word ~600 ns per call. Gaps by counterexample: element-wise arithmetic, unsigned compare, floats, one-word fixed cost. Independent of ONNX and of the S0 drafts. Entry `2026-10-23-d-mpf-1-polyfill-probe.md`. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 313bfb630..d203743b0 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,17 @@ +## D-NFR / D-NFC — native representation contract + dependency correction (2026-10-23) + +Docs only. Plans `d-native-repr-contract-v1.md` (D-NFR) and `d-native-first-dependency-correction-v1.md` (D-NFC). Nothing implemented; no ABI or execution contract changed. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-NFC-0** | one canonical dependency diagram and seven root assumptions, applied as marked supersessions to #1746–#1751 and #1750 | In PR | each affected PR cites the diagram; S0 dispute left open | +| **D-NFR-0** | seam table Quack → DR64³ → Palette256³ → execution, cited to source | In PR | every seam SHIPPED / LAB / PROPOSED / MISSING with its source | +| **D-NFR-1** | lab adapter: a Quack-bound query sealed under a frame | Proposed | after one revision moves, the stored binding is refused with the matching `Refusal`; before, it equals an oracle | +| **D-NFR-2** | codebook generation carried in the frame seal | Proposed | a palette value bound under generation g is refused under g+1 | +| **D-NFR-3** | one DR axis bound to one palette plane under a frame | Proposed | Cartesian and numerical oracles agree; a mismatched codebook is refused | +| **D-NFR-4** | end-to-end acceptance fixture (nine steps, each measured) | Proposed | all nine steps pass, each step's cost reported separately | +| **D-NFR-5** | one binding and one focus reused across several operations | Proposed | reuse saving measured against rebinding and a fused scalar / SIMD baseline, guards run on every use | + ## D-MPF — mathematical polyfill API, Stage 1 (2026-10-23) Lab only (`crates/math-polyfill-probe`). Plan `.claude/plans/d-mpf-math-polyfill-v1.md`; entry `entries/2026-10-23-d-mpf-1-polyfill-probe.md`. diff --git a/.claude/board/entries/2026-10-23-d-nfr-0-native-repr-contract.md b/.claude/board/entries/2026-10-23-d-nfr-0-native-repr-contract.md new file mode 100644 index 000000000..60ce33a26 --- /dev/null +++ b/.claude/board/entries/2026-10-23-d-nfr-0-native-repr-contract.md @@ -0,0 +1,11 @@ +# 2026-10-23 — D-NFR-0 / D-NFC-0: native representation seams and the dependency correction + +**Status:** docs only. Plans `d-native-repr-contract-v1.md`, `d-native-first-dependency-correction-v1.md`. + +- SHIPPED: Quack name → numeric binding, bound once and reused (`bind.rs`); ordered-lane version witness; bgz17 Palette256³ with S/P/O codebooks; R2IL / mask-risc / ndarray execution. +- LAB (`dr-math-binding-probe`, `dir-rmap-probe`): frame seal and stale refusal, focus and scope guards, typed method axes, the 64 × 64 DR register, 256-slot global → local focus, egglog-proved Boolean composition. +- PROPOSED: the DR64³ third axis (no type; the register is DR64²); a production table registrar. +- MISSING: a binding store in Quack; codebook runtime identity; the DR coordinate → palette value binding. +- Smallest missing seam: a Quack-bound query does not know its frame (D-NFR-1). +- The 218 contradiction passages in #1744–#1751 reduce to seven root assumptions (A1–A7), each corrected at its owning PR. +- OPEN: frame-store owner, what the third axis indexes, whether `Witness` and `Frame` become one type, the palette exact/approximate admission rule. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c8d51b72e..d43e6eb05 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. -458 entries, 2026-08-06 .. 2026-10-23. +459 entries, 2026-08-06 .. 2026-10-23. | date | entry id | finding | file | |---|---|---|---| @@ -39,6 +39,7 @@ exactly one of them, never both. | 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 | `E-D-ONNX-RELALG-CAP-S0-1` | | [2026-10-23-d-onnx-relalg-cap-s0-capstone-1750.md](2026-10-23-d-onnx-relalg-cap-s0-capstone-1750.md) | +| 2026-10-23 | `D-NFR-0` | | [2026-10-23-d-nfr-0-native-repr-contract.md](2026-10-23-d-nfr-0-native-repr-contract.md) | | 2026-10-23 | `D-MPF-4` | | [2026-10-23-d-mpf-4-classid-route.md](2026-10-23-d-mpf-4-classid-route.md) | | 2026-10-23 | `D-MPF-2` | | [2026-10-23-d-mpf-2-fixed-cost.md](2026-10-23-d-mpf-2-fixed-cost.md) | | 2026-10-23 | `E-D-MPF-1` | | [2026-10-23-d-mpf-1-polyfill-probe.md](2026-10-23-d-mpf-1-polyfill-probe.md) | diff --git a/.claude/plans/d-native-first-dependency-correction-v1.md b/.claude/plans/d-native-first-dependency-correction-v1.md new file mode 100644 index 000000000..95800878a --- /dev/null +++ b/.claude/plans/d-native-first-dependency-correction-v1.md @@ -0,0 +1,132 @@ +# D-NFC — canonical dependency correction: the native polyfill is the root + +**Status:** DECISION (operator, 2026-10-23: approved the architecture corrections to #1746–#1751 and #1750). Documentation only. Merges nothing, adds no ABI, changes no execution contract. +**Representation contract:** `.claude/plans/d-native-repr-contract-v1.md` (D-NFR). This document cites it for every shipped / lab / missing claim. +**S0 dispute:** #1744, #1745 and #1750 remain competing S0 drafts. This document does not pick one; §6 is a proposal for their owners. + +## 1. The two P0 invariants + +1. **ONNX is an external mathematical compatibility specification.** The existing R2IL mathematical polyfill is the native starting point. No ONNX graph, Tract runtime or Optimum dependency is in the internal execution path. +2. **Quack binding store + DR64³ + Palette256³ is the intended native representation architecture.** DR64³ owns the proposed local relational / focus geometry; Palette256³ owns the proposed associated numerical representation. Existing R2IL, mask-risc, BGZ, Helix and ndarray primitives are reused. Implemented components and unimplemented integration contracts are kept apart (D-NFR §2). + +> We implement ONNX mathematics using our native algebra. We do not implement our native algebra inside ONNX. + +## 2. The canonical dependency diagram + +Every affected PR references this diagram instead of restating its own. + +```text + ARCHITECTURAL DEPENDENCY (each layer needs only the ones above it) + + [1] R2IL mathematical router LAB route per ClassId, once: DIRECT / COMPOSE + │ (ClassId → LazyLock → prebound onto ndarray::simd (via mask-risc where a + │ native callable → kernel) program is needed), LOWER to r2sleigh only + │ for machine semantics, else REFUSE (D-MPF-4; + │ `math-polyfill-probe/examples/classid_route.rs`, + │ #1752). No production ClassId-keyed table + │ exists (seam S17a). + │ strategies beneath it SHIPPED ndarray::simd; mask-risc programs; + │ lance-graph-r2il FoldDialect + procs + [2] Quack binding SHIPPED bind once → numeric Query (S1–S3) + │ binding store / frame validity MISSING (S5; smallest seam = D-NFR-1) + [3] DR64³ relational / focus geometry LAB frame, focus, scope, 64×64 register, + │ 256-slot focus (S6–S12); 3rd axis PROPOSED + [4] Palette256³ numerical representation SHIPPED bgz17 S/P/O codebooks (S13–S14) + │ bound to DR coordinates MISSING (S15 codebook identity, S16 binding) + [5] Native execution SHIPPED mask-risc + ndarray::simd; bgz17 / Helix + │ + [6] egglog transformation + certification LAB Boolean / Distinct laws only (S12) + + External leaf facades (nothing in [1]–[6] depends on them): + + [7] ONNX vocabulary facade DRAFT lance-graph-onnx (#1754): ONNX names + ┄┄> [5] native functions re-exported (ALIAS) or behind a minimal + adapter (INLINE); typed refusals; no + dispatch, no init; depends on ndarray only + [8] Tract / ORT reference comparison, OPTIONAL differential oracles, offline tooling + Optimum model export never in the execution path + + These are architectural dependencies, not a serial schedule: [7] conformance + tests can start now. They test the native layers against ONNX's definitions; + they never define the native representation. +``` + +> ⊘ **Correction to layer [7] (2026-10-23, D-ONNX-NATIVE-0, `.claude/plans/d-onnx-native-v1.md`).** The diagram first drew [7] "ONNX mathematical conformance adapters — PROPOSED, one operator's semantics → native call" inside the vertical chain, between [6] and [8]. That placement read as if the chain passed through ONNX. +> +> - [7] is a **leaf**: an ONNX name maps straight onto an existing native function, and no native layer depends on it. +> - `lance-graph-onnx` (#1754) implements this. Its only normal dependency is `ndarray`; `cargo tree -i` shows nothing depends on it; it has no `LazyLock`, ClassId routing or per-call choice. +> - It does not import R2IL's router [1]. The router and the facade are independent. +> - Which S0 draft documents [7] (§6) is still the owners' decision. #1754 does not decide it. + +> ⊘ **Status of layer [1] (2026-10-23, review on #1753).** The router row first read SHIPPED. Only the strategies beneath it ship: `ndarray::simd`, mask-risc programs, and `lance-graph-r2il`'s FoldDialect and procedures. The ClassId-keyed router exists only as the #1752 lab example; no production table exists (seam S17a). The row now reads LAB, with the strategies on their own SHIPPED line. + +> ⊘ **Correction to layer [1] (2026-10-23, D-MPF-4, `.claude/plans/d-mpf-math-polyfill-v1.md` §10).** Layer [1] first read "R2IL mathematical polyfill — `lance-graph-r2il::procs` + FoldDialect". That equated R2IL with one of its strategies, and the replaced wording stays visible here for that reason. +> +> - **R2IL** is an opcode table (`ogar-r2il`) with two readings: machine (`0xC400`: r2sleigh's `r2conc` / `r2sym`) and fold (`0xC401`: `FoldDialect`). +> - **Layer [1]** is the router. It resolves a route once per ClassId and stores the callable in the binding. `FoldDialect`, mask-risc programs and direct `ndarray::simd` calls are strategies beneath it. +> - **R2Sleigh** is required only for machine semantics: carry/borrow flags, address-space load/store, branches, width-exact integers. No population operation in the current set needs it. +> - **Hard invariant:** ClassId → LazyLock → prepared native dispatch table → direct kernel execution. No per-call registry or hash lookup, backend `match`, capability probe, R2Sleigh decision, dialect reconstruction, ONNX dispatch or CPUID. Quack binding, DR frame/focus/scope and Palette codebook revisions are enforced by rebinding or by a versioned identity check, never by re-routing. + +## 3. Root assumptions behind the contradictions + +The two harvests found 218 tagged passages across #1744–#1751 (119 + 99). They are not 218 contradictions; they follow from seven root assumptions. Each is corrected once, at the PR that owns it. The other PRs point here. + +| id | root assumption (as written in the PRs) | corrected statement | owning PR | where it recurs | +|---|---|---|---|---| +| A1 | the ONNX `ModelProto` / `GraphProto` is the internal graph and interchange representation | native typed expressions and compiled R2IL procedures are the internal contract; an ONNX file is external input, read only by a conformance adapter [7] | S0 (disputed: #1744 / #1745 / #1750) | #1746, #1749, #1751 | +| A2 | native work waits for ONNX intake: an importer, an AdaWorldAPI protobuf fork, one target model | native Stage 1 has no ONNX prerequisite. The importer, protobuf fork and target model gate only an optional external-file adapter | #1746 (S1 intake) | #1744, #1745, #1748, #1749, #1750, #1751 | +| A3 | a benchmark or gate is defined by "one genuine ONNX operator" | benchmarks measure native operations; ONNX conformance is a separate test dimension on the same operations | #1748 | #1749, #1751 | +| A4 | the fallback is the original ONNX graph, or a whole-model delegated ONNX backend | the native fallback is the exact native method (e.g. the tensor arm, or the uncompressed lane). An ONNX model may remain an external validation artifact; it is never the canonical internal fallback | #1746, #1751 | #1750 | +| A5 | DR and Palette are optional physical strategies beneath an ONNX graph | DR64³ is the intended native relational representation and Palette256³ its numerical companion (D-NFR §2). Tensor / DR / hybrid benchmarks compare physical implementations of one native contract; the architectural target is not the benchmark winner | #1747, #1748 | #1745, #1751 | +| A6 | Optimum / ORT tooling sits in the plan of record | Optimum is downstream and optional [8]. Nothing native depends on it | #1751 | #1746, #1748, #1749 | +| A7 | a compiled artifact is identified by ONNX model / layer / node identity | identity is the native binding: Quack resolution under a sealed frame, plus the codebook generation (D-NFR S5, S6, S15). ONNX node identity, where it exists, is external provenance only | #1749 | #1746, #1747, #1751 | + +What the PRs already got right, and is kept unchanged: no new AST or graph format; typed refusals with whole-model `STRICT_NATIVE` refusal; approximate is never silently exact; `ORTQuantizer` is not a BGZ codebook constructor; Burn's dimension-keyed `CompiledLinear` / `CompiledAttention` registration is unsafe without identity binding. + +## 4. Native fallback and exact versus approximate + +- **Exact native operations** (selection, Boolean combination, integer folds on mask-risc) have no fallback: they are the reference. Overflow and division by zero are refused, never wrapped. +- **Approximate native operations** (palette lookup, compiled linear / attention) run only when a binding opts in, and always name their error contract: a CLAM radius is a bound; a rank correlation (ρ) is a quality measurement, not a bound. Their fallback is the exact native method on the uncompressed data, never an ONNX graph. +- **Floating-point operations** run in existing ndarray / bgz / Helix kernels with explicit numerical validation. They carry no algebraic certificate, and none is invented for them. +- **An ONNX model** may be kept as an external validation artifact, compared offline through a reference runtime [8]. + +## 5. Measured baseline that the corrections cite (#1752, draft, pending independent review) + +| path at 64 rows (one mask word) | ns per call | +|---|---:| +| fair scalar `i64` loop, runtime threshold | 12 | +| ndarray compare + masked sum | 39 | +| mask-risc, compiled program | 94–99 | +| R2IL procedure composition | 171–172 | +| ONNX-shaped wrapper (rebinds every call) | 217–234 | +| ClassId-prebound route, guard included (D-MPF-4) | 61–67 | +| ClassId-prebound route, callable alone (D-MPF-4) | 36–39 | + +- The 50 ns one-word target is not met. The ndarray step alone is 39 ns. +- The earlier "1.6× faster than the scalar loop" is SUPERSEDED: it compared against an `i128` filter-chain oracle. A fair `i64` loop is ~3× faster than the fold at 64 K rows. +- At 64 K rows all paths converge on `ndarray::simd::masked_sum_i32`, a scalar set-bit walk. +- The ONNX-shaped wrapper is a diagnostic compatibility boundary, not an architectural layer. +- ⊘ (D-MPF-4) The mask-risc and R2IL-composition rows are what those paths cost when chosen per call. They are not a floor for R2IL routing. A route resolved once per ClassId equals the ndarray row: the callable alone costs 36–39 ns. The frame/focus/scope guard adds 27–28 ns. "R2IL prepared" (FoldDialect's `last_program` kept as a `CompiledProgram`) equals the mask-risc row. + +## 6. S0 reconciliation proposal (owner-facing, not a decision) + +> ⊘ **Outcome (2026-10-23).** The operator merged #1744 and ordered #1745–#1754 merged. #1744's S0 therefore keeps `.claude/plans/d-onnx-relalg-cap-v1.md`. #1750's and #1745's texts, which wrote the same path, were moved unchanged to `d-onnx-relalg-cap-capstone-1750-v1.md` and `d-onnx-relalg-cap-convergence-1745-v1.md`, each with a path note. Where the three S0 documents disagree, this correction governs. The proposal below is kept as written; its "disputed" wording describes the state before that decision. + +The three S0 drafts agree on more than they disagree: no new AST, typed refusals, relalg stays narrow, numerics stay in ndarray. They disagree on who owns the capstone, and all three take A1 and A2 as given. Proposal: + +1. Each owner adopts §1 and §2 by reference, through a marked supersession note on their own branch, and leaves the rest of their draft unchanged. +2. The surviving S0 then documents layer [7] only: the conformance-adapter boundary and its refusal rules. Native stages are owned by D-MPF (#1752) and D-NFR. +3. The owners choose which draft carries [7], or merge the three, on EXO-50. Nothing here decides it. + +## 7. PR cross-reference + +| PR | correction applied (marked supersession, its own plan + description) | +|---|---| +| #1746 | A1, A2, A4: native polyfill API first; ONNX semantics are external mappings; intake prerequisites move to the optional adapter | +| #1747 | A5, A7: DR64³ is the intended native relational representation, not an ONNX optimization | +| #1748 | A3, A5: benchmarks compare physical implementations of native contracts; native methods first | +| #1749 | A1, A7: GraphProto does not own internal representation; Quack + DR64³ + Palette256³ is the internal integration | +| #1750 | A1, A2, A4 (owned): `ModelProto` is not the internal graph; OP-6 / OP-7 gate only the optional adapter | +| #1751 | A4, A6: Optimum downstream and optional; ONNX graph fallback is external interoperability | +| #1752 | none: the shipped polyfill is the root; kept in draft for independent review | +| #1744, #1745 | not edited; §6 proposal | diff --git a/.claude/plans/d-native-repr-contract-v1.md b/.claude/plans/d-native-repr-contract-v1.md new file mode 100644 index 000000000..48c5bb230 --- /dev/null +++ b/.claude/plans/d-native-repr-contract-v1.md @@ -0,0 +1,107 @@ +# D-NFR — native representation contract: Quack → DR64³ → Palette256³ → execution + +**Status:** D-NFR-0 MEASURED-IN-SOURCE (this document, docs only). D-NFR-1.. PROPOSED, none authorized. Read at `origin/main` `f0b046b9f`. +**Scope:** which binding seams of the intended native representation are shipped, lab-only, proposed or missing. It does not implement any of them, change an ABI or an execution contract, or decide the #1744 / #1745 / #1750 S0 ownership dispute. +**Companion:** `.claude/plans/d-native-first-dependency-correction-v1.md` (the canonical dependency order and the PR corrections). This contract comes first; the correction cites it. + +## 0. The two invariants + +1. **ONNX is an external mathematical compatibility specification.** The native starting point is the existing R2IL polyfill (`lance-graph-r2il::procs` + `FoldDialect`, executed by mask-risc over `ndarray::simd`). No ONNX graph, Tract runtime or Optimum dependency is in the internal execution path. +2. **Quack binding + DR64³ + Palette256³ is the intended native representation.** DR64³ owns the proposed local relational / focus geometry. Palette256³ owns the proposed associated numerical representation. Existing R2IL, mask-risc, BGZ, Helix and ndarray primitives are reused. This document separates what is implemented from what is only an integration contract. + +The kernel inventory does not define this architecture. A shipped kernel is evidence about EXECUTION only; it does not establish that a seam exists, or what its semantics are. + +## 1. Status vocabulary + +| status | meaning | +|---|---| +| SHIPPED | in a production crate on `main`, with tests | +| LAB | in a lab/probe crate on `main` (stand-in, not the owner); no production caller | +| PROPOSED | named by a plan; no type exists | +| MISSING | required by the target architecture; no type and no plan owns it | + +Coverage of an OPERATION is reported separately on four axes: **semantic** (its mathematical contract is written down), **executable** (an existing composition computes it), **approximate** (it is computed with a stated error, not exactly), **certified** (an applicable transformation has independently checkable evidence). An operation can be executable without being semantically specified, and specified without being executable. + +## 2. Seam table + +Every row cites the defining source. "Read" means the body was read for this document, not only searched. + +| # | seam | status | source (read) | what it does / does not do | +|---|---|---|---|---| +| S1 | names and literals → numeric identity | SHIPPED | `lance-graph-quack/src/bind.rs`: `Binder`, `Draft::bind`, `BindError` | Resolves table, field and textual literal once through a consumer-owned `Binder` (catalog + codebook). Refusals: `UnknownTable`, `UnknownField`, `UnknownValue` (nothing minted), `KindMismatch`, `OutOfRange`, `WrongTable`. Three-valued NULL handling through `BoundField.validity`. | +| S2 | bound query reused without re-resolution | SHIPPED | `bind.rs` module doc; `lance-graph-mask-risc` `CompiledProgram` | A `Query` "can be lowered and executed any number of times without touching a name, a label or a codebook again". The lowered program can also be kept (`CompiledProgram`, recognition once). | +| S3 | ordered-lane version witness | SHIPPED | `lance-graph-quack/src/lib.rs` (`lane_version`, `OrderedLaneWitness`), contract `ordered_lane` `WitnessError::VersionMismatch` | A range bound on an ordered lane carries the lane's version and order-sensitive digest; a forged or stale witness makes the leaf sweep instead and says why (`a_prefix_aperture_under_a_stale_witness_sweeps_and_says_why`). Covers one lane's order, not a whole binding. | +| S4 | table catalog / physical registration | PROPOSED | `bind.rs`: `Registrar`, `TableDeclaration::register` | "no crate owns a table catalog or storage allocation yet, so `Registrar` has no production implementation". | +| S5 | **binding store**: persisted bindings, frame validity, invalidation | MISSING in Quack | `bind.rs`, `lib.rs` (searched closed: no snapshot / frame / epoch type) | Quack is a binding *membrane*, not a store. The consumer's `Binder` owns ID meaning and "what survives a rename or a re-observation". No Quack type records under which frame a `Query` was bound. | +| S6 | frame: source × relation map × coordinates revisions, seal identity, stale refusal | LAB | `dr-math-binding-probe/src/lib.rs`: `FrameRevisions`, `FrameStore`, `Frame` | "Lab stand-in for the owner of a frame." Frames compare by issue (`Weak::ptr_eq`), never by value; a stale frame names the first revision that moved (`SourceChanged`, `MapChanged`, `CoordinatesChanged`, `FrameResealed`); a foreign store is `ForeignFrame`. No production owner. | +| S7 | focus and scope as separate guards | LAB | same file: `Focus { revision }`, `Scope { id }`, `Guards`, `bind_dr64` | Checked by equality at borrow time (`FocusChanged`, `ScopeChanged`). "Checks seal identity and equality of focus and scope, not their authenticity; a production binder also needs the ClassView registry, the tenant ACL and the source owner." | +| S8 | typed axes, truth and population per method | LAB | same file: `MethodSignature { owner_class, method_ordinal, row: Axis, column: Axis, truth, population }`, `AxisKind::{Identity, Property, Community, Capability}` | `bind_dr64` refuses `MethodChanged`, `AxisChanged`, `SemanticsChanged`, `ThreeValuedNeedsValidity`, `TwoValuedHasNoValidity`, `BagNeedsMultiplicity` (Bag is refused, not supported). | +| S9 | the DR register | LAB | `dr-math-binding-probe/src/relcomp.rs`: `Rows = [u64; 64]`, `compose`, `Chain`, `RelExpr` | One borrowed 64 × 64 Boolean relation register (512 B): two axes (row × column). Composition is OR/AND over set bits. **This is DR64², not DR64³**: no type carries a third axis. | +| S10 | DR64³ third axis (identity × identity × property/relation) | PROPOSED | (no type; closed search over the probe and `dir-rmap-probe`) | The cube is a target, not a type. A stack of S9 registers indexed by a relation/property ordinal is the obvious reading; nothing on `main` fixes it. | +| S11 | global → local focus | LAB | `dir-rmap-probe/src/focus.rs`: `Focus::slots`, `Focus::project`; `prep.rs`: `Witness` | Binds up to 256 group ordinals to local slots for one chain and projects the full B+ closure onto them (4 words per group). Refuses `OutOfFocus`, `Stale`, `TooLarge`, `Duplicate`; completeness through unfocused groups is tested. `Witness` is tied to dir-sim's `VersionStore`, so `dr-math-binding-probe` does not reuse it. A DR256 local domain over one domain (IAM membership), not a general one. | +| S12 | relational certification | LAB | `relcomp.rs`: `admit_composition_assoc`, `AdmittedLaw`, `prove_reassociation`, `EggProof`; `recipe.rs`: `RecipeCertificate`, `admit_recipe` | Associativity of Boolean composition admitted per law shape and proved by egglog, kept as egglog's own `ProofStore` + `ProofId`. Applies to Boolean / Distinct relations only. | +| S13 | Palette256³ codebooks | SHIPPED | `bgz17/src/palette.rs`: `Palette { entries: Vec }`, `PaletteEdge { s_idx, p_idx, o_idx }`; `scope.rs`: `codebook_s/p/o`; `palette_semiring.rs`, `distance_matrix.rs` | ≤256 Base17 (`i16[17]`) archetypes per plane; an edge is three u8 indices, one per S/P/O plane. **The third axis already has a meaning: S, P, O.** Distance matrix, compose and identity via `PaletteSemiring`. | +| S14 | palette quality contract | SHIPPED (stated, per crate) | `bgz17/src/lib.rs` layer table; `bgz-tensor/src/palette.rs` CLAM `radii`; `codebook_calibrated.rs` | bgz17 states measured rank correlation per layer (ρ 0.937 scent, 0.965–0.992 palette, 1.000 exact planes). bgz-tensor keeps a CLAM worst-case radius per entry and a γ+φ-calibrated u8 table. A correlation is a quality measurement, not an error bound; only the CLAM radius is a bound. | +| S15 | codebook runtime identity (family, generation, digest) | MISSING | `Palette`, `CalibratedCodebook` (no such field); `bgz-tensor/src/manifest.rs` `ModelEntry.sha256` | The only digest is per hydrated shard file. Nothing binds a palette index to the codebook generation that issued it, so a stale or foreign codebook cannot be refused at use. | +| S16 | DR coordinate → palette-valued property | MISSING | (no type) | Nothing says which DR axis carries which palette plane, under which frame. ADMISSION B stands: a DR ordinal is never a palette index and a palette index is never a positional gather into another table. | +| S17 | native execution | SHIPPED | `lance-graph-r2il::procs` (~30 procedures), `FoldDialect`, `lance-graph-mask-risc` terminals, `ndarray::simd` | Selection, Boolean combination and integer folds (count, any, all, sum, min, max, group sum, blend, keep). The DR compose kernel in S9 is NOT on mask-risc; it is the probe's own loop. Floats and approximations run in existing ndarray / bgz kernels, outside the fold algebra. | +| S17a | R2IL route per ClassId (DIRECT / COMPOSE / LOWER / REFUSE), resolved once and held in the binding | LAB | `math-polyfill-probe/examples/classid_route.rs` (D-MPF-4) | No production ClassId-keyed table exists. LOWER targets `r2conc::SlabState::step`, machine semantics only. | + +`lance-graph-contract::alpha_focus` and `rubicon_witness` use "focus" for an ATTENTION mask (rung × tenant). That is a different concept from DR's spatial focus; do not cite them for S7 or S11. + +## 3. Reusable bindings versus mutable state + +| kind | what | rule | +|---|---|---| +| reusable, validated once | a bound `Query` (S2); a `CompiledProgram`; a `MethodSignature` declaration | may be cached and reused across calls | +| mutable, re-checked at every use | frame seal (S6), focus revision and scope (S7), lane witness (S3), codebook generation (S15, once it exists) | never cached away. `bind_dr64` re-runs all three checks per borrow, and each is an O(1) pointer or value comparison. | + +The D-MPF-2 measurement (#1752) attributes ~73–78 ns per call to R2IL procedure composition and ~45–63 ns to an ONNX-shaped wrapper that rebinds every call. Reusing a validated binding can only remove the RESOLUTION and PROGRAM-BUILD part of that. It cannot remove the guard checks, and it must not. Until the guard checks are timed separately from program construction, no claim that a boundary can be removed is made. + +> ⊘ (D-MPF-4, #1752 plan §10) "R2IL procedure composition" above is the FoldDialect strategy re-run per call, not R2IL routing. For a fixed query, the existing `last_program()` → `CompiledProgram` facility removes it. A ClassId-prebound route runs at the direct `ndarray::simd` cost plus 27–28 ns for the frame/focus/scope guard. That guard is the one per-run check that must remain, and it is a versioned-identity check, not resolution. + +## 4. The smallest missing seam + +**S5 × S6: a Quack-bound query does not know its frame.** S1–S3 resolve and reuse a binding; S6–S8 guard a DR register against a stale frame, focus or scope. Nothing connects the two. A `Query` executed after its source, relation map or coordinate assignment moved is not refused by anything except S3, which covers only an ordered lane's order. + +Proposed shape, not built (owners: Quack for the binding, the DR owner for the frame, no new ABI): + +- the consumer's `Binder` names the frame revisions it resolved under (source, relation map, coordinates), exactly `FrameRevisions`; +- binding returns the `Query` together with a sealed `Frame` from the frame owner; +- every execution of a stored binding runs the frame check before lowering, and refuses with the existing `Refusal` variants. + +This is one adapter between two types that already exist, not a new store, AST or runtime. It is also the precondition for S15 (a codebook generation is one more revision in the same seal) and S16. + +## 5. Next stages (smallest experiment each; none authorized) + +| D-id | experiment | gate | +|---|---|---| +| D-NFR-0 | this contract | shipped / lab / missing per seam, cited to source | +| D-NFR-1 | the S5 × S6 adapter as a lab probe: bind a Quack `Draft`, seal a frame, execute, advance one revision, execute again | the second execution is refused with the matching `Refusal`; the first equals an independent oracle | +| D-NFR-2 | S15: carry a codebook generation in the frame seal | a palette value bound under generation g is refused under g+1 | +| D-NFR-3 | S16: bind one DR axis to one palette plane (S/P/O) under a frame | an independent Cartesian oracle for coordinates and an independent numerical oracle for values both agree; a mismatched codebook is refused | +| D-NFR-4 | the end-to-end acceptance fixture (§6) | all nine steps, each measured alone | +| D-NFR-5 | one binding and one focus reused across several operations, against rebinding each time and against a fused scalar / SIMD baseline | the reuse saving is measured, guards still run on every use | + +## 6. The acceptance fixture (design only) + +1. Start from a Quack-bound snapshot (S1, S2) under a sealed frame (S6, via D-NFR-1). +2. Resolve typed identities and properties through the consumer `Binder`. +3. Project a local DR view: S11 focus slots, S9 register(s). +4. Select an existing Palette256 value operation (S13) through the D-NFR-3 binding. +5. Execute on mask-risc / ndarray (S17); palette lookups on bgz17. +6. Check coordinates against an independent Cartesian oracle. +7. Check values against an independent numerical oracle, against the stated error contract (S14), never as exact unless the layer is exact. +8. Refuse a stale frame, a moved focus, a changed scope and a mismatched codebook. +9. Report binding, focus construction, folding, SIMD execution and materialization separately. + +No step adds a runtime. + +## 7. Open points + +| id | question | owner | status | +|---|---|---|---| +| NFR-OP-1 | who owns the production frame store (S6): Quack, ClassView, or the source owner? | operator | OPEN | +| NFR-OP-2 | what the DR64³ third axis indexes: relation ordinal, property ordinal, or palette plane | DR owner | OPEN | +| NFR-OP-3 | whether `dir-rmap-probe`'s `Witness` and `dr-math-binding-probe`'s `Frame` become one type | DR owner | OPEN | +| NFR-OP-4 | the exact-versus-approximate admission rule for palette values inside a native fold | bgz owner | OPEN |