diff --git a/.claude/plans/d-nam-1-native-method-crosswalk-spec-v1.md b/.claude/plans/d-nam-1-native-method-crosswalk-spec-v1.md new file mode 100644 index 000000000..d8537cb5e --- /dev/null +++ b/.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. diff --git a/.claude/specs/d-nam-method-crosswalk-v1.json b/.claude/specs/d-nam-method-crosswalk-v1.json new file mode 100644 index 000000000..37c044fbe --- /dev/null +++ b/.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" + ] + } + ] +} diff --git a/tools/d_nam_validate_crosswalk.py b/tools/d_nam_validate_crosswalk.py new file mode 100644 index 000000000..9b22e1765 --- /dev/null +++ b/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())