spec(D-NAM-1): versioned native method DTO crosswalk and normalization gates

.claude/plans/d-nam-1-native-method-crosswalk-spec-v1.md

@@ -0,0 +1,53 @@
+# D-NAM-1 — Typed native method normalization and versioned DTO crosswalk
+
+**2026-10-25 • ENGINEERING SPEC + STATIC CANDIDATE CROSSWALK VALIDATOR / PROPOSED**. Parent: [D-NAM capstone](d-nam-native-algebra-dto-capstone-v1.md), [EXO-152](https://linear.app/exo-red/issue/EXO-152). Independent implementation later; no contract ABI edit in this PR.
+
+## Artifacts actually included in this draft PR (offline-only)
+
+- `.claude/specs/d-nam-method-crosswalk-v1.json`: machine-readable **CANDIDATE** rows for four existing native anchors and ONNX/TFLite/MLIR/RelAlg readings. No external operator is tagged `admitted`; unspecified external versions remain `null`.
+- `tools/d_nam_validate_crosswalk.py`: **static manifest linter**, no runtime import/dispatch. It refuses duplicate native IDs, missing dialect readings/negative cases, unreasoned refusals, and any `admitted` row missing a pinned version, independent oracle and evidence.
+- Review command: `python3 tools/d_nam_validate_crosswalk.py`. This validates manifest shape only, **not** operator equivalence, Rust integration, ONNX/TFLite compatibility or CI coverage. A code owner must verify and run it separately before promotion.
+
+**This is the first small tooling implementation; no production Rust method binding or DTO executor has been added.**
+
+## Purpose
+Construct the *smallest declarative mapping* that says a dialect operator (or finite operator pattern) means an existing native method/composition under explicit guards. Do not build new `Method` enum until auditing existing ClassView/method signature/ogar-r2il opcode identity; do not create another generic AST. Method identity is source-owned; DTO names are aliases with evidence.
+
+## Existing owners to reuse
+- `lance-graph-onnx/src/lib.rs`: root exact ALIAS/INLINE, `bounded::tanh_f32/exp_f32`; `ReduceSum` and `sum_where_greater_i32`.
+- `lance-graph-relalg/src/ir.rs`: `Rel::Atom`, `Measure`, single-table relations; `lower.rs` executes R2IL FoldDialect.
+- `lance-graph-quack/src/bind.rs`: compile names/values to numeric references once.
+- `lance-graph-contract` D-RA-2 set algebra rules, `lance-graph-r2il` procedure call/readings, `lance-graph-mask-risc` numeric/mask terminals, `ndarray::simd` actual kernels.
+- Linear [EXO-86](https://linear.app/exo-red/issue/EXO-86), [EXO-115](https://linear.app/exo-red/issue/EXO-115), [EXO-102](https://linear.app/exo-red/issue/EXO-102).
+
+## Minimal schema: versioned crosswalk row (not a new runtime type yet)
+| Field | Semantic obligation |
+|---|---|
+| native anchor | symbol / admitted composition, repo commit + owner |
+| dialect selector | ONNX domain+opset+op_type; TFLite builtin opcode+schema/model version; MLIR dialect+op/traits; SQL dialect/null/multiplicity |
+| operand contract | dtype, rank, logical shape, symbolic dims, strides, axis, broadcast, scalar-vs-lane |
+| result demand | scalar/value lane/packed mask/materialized values, keepdims and output shape |
+| carrier & law | Bool/Distinct, Bag, SQL K3, i32 sum, FP32, quantized; semiring; legal reordering |
+| effects / authority | read/write alias, scope, same-table seek vs forbidden cross-table gather |
+| route | DIRECT native symbol / COMPOSE existing polyfill / REFUSE; selected at cold bind |
+| evidence | pinned upstream spec, direct-native test, independent oracle, negative controls and measured cost |
+| reverse export | explicitly supported, conditional, or refused; never inferred from import success |
+
+External node and model identity are *provenance*, not the native object's identity. Prepared route identity must reflect native frame/codebook/operand validity under D-NFR; do not use shape alone for compiled palette caches.
+
+## Worked normalization groups (candidate / narrow acceptance only)
+1. `X > t`: `ONNX Greater`, `TFLite GREATER`, MLIR `arith.cmpi sgt`, `Rel::i32(Gt)`; only rank-1 i32 vs scalar threshold, same element count and signed comparison. Native `gt_i32_to_mask`. Result packed mask is **internal**, TFLite/ONNX external BOOL formats need boundary packing/unpacking.
+2. `select(mask,X,0)`: ONNX `Where`, TFLite `SELECT_V2`, MLIR `arith.select`; native `blend_i32` where shapes/dtypes/order agree. This is a **value** operation, not `Rel::Keep`.
+3. `Σ_i select(X_i>t,X_i,0)`: composition `gt_i32_to_mask + masked_sum_i32`; ONNX `Greater/Where/ReduceSum`, TFLite candidate `GREATER/SELECT_V2/SUM`, and single-table RelAlg predicate + `Measure::Sum`. Guard integer range and shape; direct native i64 fold must not silently become ONNX/TFLite i32 result.
+4. `tanh(x)`: ONNX bounded alias `ndarray::hpc::vml::vstanh` (#1758); TFLite `TANH` as separate dialect numeric policy and quantization; MLIR `math.tanh` candidate. **Outside** Boolean RelAlg; approximate bound is not an algebraic rewrite law.
+
+**Counterexample inputs before admission:** empty n, SIMD tails n=1,15,16,17,63,64,65, nonzero threshold, signed MIN/MAX, sum beyond i32, false-vs-unknown SQL NULL, mismatched broadcast, f32 signed zero and NaN, TFLite bool layout, different opcode versions. Prove tests are non-vacuous and failures are informative.
+
+## Implementation ownership and acceptance
+- Proposed owner of crosswalk **source data**: one static declarative file generated/reviewed at cold time and consumed only by external DTO adapters; choose location after inspecting existing method registry, do not duplicate it.
+- Never dispatch by ONNX/TFLite name in the hot loop; native methods are selected once. No dynamic string matching in SoA/DR/R2IL execution.
+- D-RA-2 stays fixed. Normalize relational subset via contract's set rules, as scoped by EXO-115; value math stays ndarray/native numeric methods, not `Rel`.
+- Gate D-NAM-1: owner-reviewed table of at least four rows with native anchors, exact version keys, typed positive+negative fixture, tests run by future code PR, plus a no-new-IR dependency graph. Unknown external version means REFUSE. An unexecuted spec does not satisfy the test gate.
+
+## Kill criteria
+If the plan requires a general AST or per-call registry; if unknown ops fall through; if method identity is guessed by matching shape; if K3/Bag/FP semantics are merged; or if one polyfill cannot reproduce the independent oracle, stop and split the candidate rather than weakening its contract.

.claude/specs/d-nam-method-crosswalk-v1.json

@@ -0,0 +1,180 @@
+{
+  "schema": "d-nam-crosswalk-v1",
+  "status": "CANDIDATES_ONLY_NOT_A_RUNTIME",
+  "generated_at": "2026-10-25",
+  "owner": "EXO-152",
+  "source_prs": [
+    1752,
+    1753,
+    1754,
+    1758
+  ],
+  "methods": [
+    {
+      "native_id": "cmp.i32.gt_scalar",
+      "carrier": "i32",
+      "native_anchor": "ndarray::simd::gt_i32_to_mask",
+      "semantic": "signed rank-1 i32 lane comparison against one scalar threshold, result internal packed mask",
+      "readings": [
+        {
+          "dialect": "ONNX",
+          "expression": "Greater(X, threshold)",
+          "status": "candidate",
+          "version": null,
+          "notes": "threshold broadcasting and external BOOL packing to be verified"
+        },
+        {
+          "dialect": "TFLite",
+          "expression": "GREATER(X, threshold)",
+          "status": "candidate",
+          "version": null,
+          "notes": "builtin opcode options and TFLite BOOL storage to be verified"
+        },
+        {
+          "dialect": "MLIR",
+          "expression": "arith.cmpi sgt",
+          "status": "candidate",
+          "version": null,
+          "notes": "signed predicate and indexing domain required"
+        },
+        {
+          "dialect": "RelAlg",
+          "expression": "Rel::i32(lane, Cmp::Gt, threshold)",
+          "status": "candidate",
+          "version": "repo main 2026-10-25",
+          "notes": "only same-table i32 lane"
+        }
+      ],
+      "refusal": [
+        "non-i32 input",
+        "lane-vs-lane comparison",
+        "unproven broadcast shape",
+        "SQL UNKNOWN folded to false"
+      ]
+    },
+    {
+      "native_id": "select.i32.mask",
+      "carrier": "i32",
+      "native_anchor": "ndarray::simd::blend_i32",
+      "semantic": "for each same-address slot, mask bit selects X else Y; internal mask packed",
+      "readings": [
+        {
+          "dialect": "ONNX",
+          "expression": "Where(C, X, Y)",
+          "status": "candidate",
+          "version": null,
+          "notes": "exact shape/broadcast restrictions need validation"
+        },
+        {
+          "dialect": "TFLite",
+          "expression": "SELECT_V2(C, X, Y)",
+          "status": "candidate",
+          "version": null,
+          "notes": "same ranks/shapes and bool bytes require explicit mapping"
+        },
+        {
+          "dialect": "MLIR",
+          "expression": "arith.select",
+          "status": "candidate",
+          "version": null,
+          "notes": "value op, not set membership"
+        },
+        {
+          "dialect": "RelAlg",
+          "expression": "unrepresentable as Rel::Keep (mask only)",
+          "status": "refused",
+          "version": "repo main 2026-10-25",
+          "reason": "RelAlg::Keep emits mask, not selected i32 values"
+        }
+      ],
+      "refusal": [
+        "non-i32 values",
+        "shape mismatch",
+        "mask tail bits not zero"
+      ]
+    },
+    {
+      "native_id": "fold.i32.sum_where_gt",
+      "carrier": "i32/i64 accumulator",
+      "native_anchor": "ndarray::simd::gt_i32_to_mask + ndarray::simd::masked_sum_i32",
+      "semantic": "sum selected i32 values with i64 internal sum; external i32 result only if range guard passes",
+      "readings": [
+        {
+          "dialect": "ONNX",
+          "expression": "Greater -> Where(X, 0) -> ReduceSum",
+          "status": "candidate",
+          "version": null,
+          "notes": "rank one, reduction axes/keepdims/output dtype and overflow guard required"
+        },
+        {
+          "dialect": "TFLite",
+          "expression": "GREATER -> SELECT_V2(X, 0) -> SUM",
+          "status": "candidate",
+          "version": null,
+          "notes": "operator versions, keep_dims, zero-fill and dtype semantics require pinned oracle"
+        },
+        {
+          "dialect": "MLIR",
+          "expression": "linalg.generic guarded reduction",
+          "status": "candidate",
+          "version": null,
+          "notes": "reduction loop and index map must agree"
+        },
+        {
+          "dialect": "RelAlg",
+          "expression": "Rel::i32(lane, Gt, threshold) + Measure::Sum(lane)",
+          "status": "candidate",
+          "version": "repo main 2026-10-25",
+          "notes": "same table with Boolean selection; external output narrowing guarded"
+        }
+      ],
+      "refusal": [
+        "sum exceeds i32 for i32 result",
+        "NULL/Bag semantics differ",
+        "unknown empty-axes handling",
+        "wrong mask scope"
+      ]
+    },
+    {
+      "native_id": "value.f32.tanh_bounded",
+      "carrier": "f32",
+      "native_anchor": "ndarray::hpc::vml::vstanh",
+      "semantic": "bounded f32 elementwise tanh, preserves tested IEEE special values; no Boolean algebra law",
+      "readings": [
+        {
+          "dialect": "ONNX",
+          "expression": "Tanh",
+          "status": "candidate",
+          "version": null,
+          "notes": "lance-graph-onnx::bounded::tanh_f32 merged via #1758; pin ONNX operator version"
+        },
+        {
+          "dialect": "TFLite",
+          "expression": "TANH",
+          "status": "candidate",
+          "version": null,
+          "notes": "f32 only candidate; quantized TANH is not an alias"
+        },
+        {
+          "dialect": "MLIR",
+          "expression": "math.tanh",
+          "status": "candidate",
+          "version": null,
+          "notes": "numerical accuracy and rounding policy required"
+        },
+        {
+          "dialect": "RelAlg",
+          "expression": "none (outside set algebra)",
+          "status": "refused",
+          "version": "repo main 2026-10-25",
+          "reason": "Rel does not carry f32 value arithmetic"
+        }
+      ],
+      "refusal": [
+        "quantized tanh conflated with f32",
+        "tanh floated into Rel",
+        "unbounded approximation claimed exact"
+      ]
+    }
+  ]
+}

tools/d_nam_validate_crosswalk.py

@@ -0,0 +1,66 @@
+#!/usr/bin/env python3
+"""Validate D-NAM's *documentation* crosswalk, not semantic equivalence.
+
+No external dependencies; used at review time. Does not import or dispatch ONNX,
+TFLite, MLIR, Quack, R2IL or ndarray and grants no operator admission.
+"""
+import json
+from pathlib import Path
+import sys
+
+ROOT = Path(__file__).resolve().parents[1]
+DEFAULT = ROOT / ".claude/specs/d-nam-method-crosswalk-v1.json"
+DIALECTS = {"ONNX", "TFLite", "MLIR", "RelAlg"}
+STATES = {"candidate", "admitted", "refused"}
+
+
+def validate(obj):
+    if obj.get("schema") != "d-nam-crosswalk-v1":
+        raise ValueError("unsupported crosswalk schema")
+    methods = obj.get("methods")
+    if not isinstance(methods, list) or not methods:
+        raise ValueError("no native methods")
+    ids = set()
+    for method in methods:
+        ident = method.get("native_id")
+        if not isinstance(ident, str) or not ident or ident in ids:
+            raise ValueError(f"invalid/duplicate native_id: {ident!r}")
+        ids.add(ident)
+        if not method.get("native_anchor") or not method.get("semantic"):
+            raise ValueError(f"{ident}: missing native anchor or semantics")
+        dialects = set()
+        for row in method.get("readings", []):
+            d = row.get("dialect")
+            state = row.get("status")
+            if d not in DIALECTS or d in dialects:
+                raise ValueError(f"{ident}: unknown/duplicate dialect {d!r}")
+            dialects.add(d)
+            if state not in STATES or not row.get("expression"):
+                raise ValueError(f"{ident}/{d}: incomplete reading")
+            if state == "admitted" and (not row.get("version") or not row.get("oracle") or not row.get("evidence")):
+                raise ValueError(f"{ident}/{d}: admitted requires pinned version, independent oracle and evidence")
+            if state == "refused" and not row.get("reason"):
+                raise ValueError(f"{ident}/{d}: refusal requires reason")
+        if dialects != DIALECTS:
+            raise ValueError(f"{ident}: expected all four dialect readings")
+        if not method.get("refusal"):
+            raise ValueError(f"{ident}: missing negative cases")
+    if len(ids) != 4:
+        raise ValueError(f"expected four seed methods, got {len(ids)}")
+    return len(ids)
+
+
+def main():
+    path = Path(sys.argv[1]) if len(sys.argv) > 1 else DEFAULT
+    try:
+        obj = json.loads(path.read_text(encoding="utf-8"))
+        count = validate(obj)
+    except (OSError, ValueError, json.JSONDecodeError) as exc:
+        print(f"D-NAM crosswalk REFUSE: {exc}", file=sys.stderr)
+        return 1
+    print(f"D-NAM crosswalk schema OK ({count} candidates; NOT semantic admission)")
+    return 0
+
+
+if __name__ == "__main__":
+    raise SystemExit(main())