Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@
| **D-ONNX-INTAKE-4** | S4 numeric/quantization parity for real model blockers | Queued (conditional; not authorized) | IntegerExact / bounded FP / SourceParity / CertifiedMath kept distinct |
| **D-ONNX-INTAKE-5** | S5 whole-model forward pass and cost closure | Goal, not authorized | outputs vs ORT under declared tolerance; every cost stage reported |
| **D-TRACT-HARVEST-0** | ONNX graph as a DR#3 graph (nodes Identity, values Property, dep = do_ ∘ read_by) resolved through a DT64 ON×WHEN×DO registry (op signature → classid → native DO); Tract cold facts; ORT (optimizer off) oracle; `crates/tract-harvest-probe` | Lab probe implemented (this PR, redesigned to the graph); plan [d-tract-harvest-0-native-algebra-bridge-v1.md](../plans/d-tract-harvest-0-native-algebra-bridge-v1.md) §0 | 26 tests, 13 disable runs red; full model 4,146/7,620 nodes WHEN-true with inference-stage facts (§0.1), 0 refused for missing facts, >64 positions untiled, first unregistered groups Unsqueeze/Shape/Gather/Concat/MatMul |
| **D-TRACT-SHAPE-1** | Cold shape-subgraph folding (Const/Shape/Symbolic/Data classes; fold through the node's own WHEN/DO; stale-input refusal), shape-op registrations (Shape, Gather i64, Unsqueeze, Concat, Reshape, Cast i64, Erf via `vserf`, scalar-Y Where via `blend_i32_scalar`), producer-checked Tract fact admission | **In PR** (lab probe); plan [d-tract-harvest-0-native-algebra-bridge-v1.md](../plans/d-tract-harvest-0-native-algebra-bridge-v1.md) §0.2 | 40 tests, 9 disable runs red; Jina [1,10] coverage 4,146/0/3,474 → 6,404/56/1,160, 4,440 nodes fold in 7.3 ms; remaining blocker int64 shape arithmetic (owner decision) |
| **D-TRACT-SHAPE-1** | Cold shape-subgraph folding (Const/Shape/Symbolic/Data classes; fold through the node's own WHEN/DO; stale-input refusal), shape-op registrations (Shape, Gather i64, Unsqueeze, Concat, Reshape, Cast i64, Erf via `vserf`, scalar-Y Where via `blend_i32_scalar`), producer-checked Tract fact admission | **Shipped** #1853 + follow-up In PR (lab probe); plan [d-tract-harvest-0-native-algebra-bridge-v1.md](../plans/d-tract-harvest-0-native-algebra-bridge-v1.md) §0.2–§0.3 | #1853 merged (40 tests, 9 disable runs red; coverage 4,146/0/3,474 → 6,404/56/1,160). Follow-up **In PR**: registry v3 (int64 compares/Where, ConstantOfShape, Expand), optional-output producer test; coverage 6,581/114/925; int64 Mul/Div/Add/Sub/Range refused pending the ndarray ask (plan §0.3) |

## D-TFLP — TFLite models on the native polyfill: int8 codes as Palette256 (2026-10-25)

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -11,3 +11,7 @@ A Tract fact is admitted only from the value's source-producer outlet (a matchin
Fixtures (ORT 1.29.0 `ORT_DISABLE_ALL`): shape chain bit-exact; Erf ≤ 2 ULP vs ORT and f64 over 4,115 points. 40 tests; 9 disable runs red.

**OPEN:** int64 shape-arithmetic semantics (owner, then ndarray ask); axis as DO parameter vs classid per axis; `vserf` ~4x slower than Tract's erf; ConstantOfShape/Expand via ndarray core not yet registered; multi-tile and MatMul gates unchanged.

**Follow-up (after #400 / #1853):** registry v3 adds int64 Equal/LessOrEqual (#400 compares), int64 Where (`blend_i64[_scalar]`), ConstantOfShape (`from_elem`), Expand (`broadcast`). Optional-output fixture (`LSTM ["", "Y_h"]`) pins that `source_producers` follows Tract's compacted outlet numbering and admits `Y_h`'s fact, not the omitted `Y`'s. Jina coverage 6,404/56/1,160 → 6,581/114/925. Remaining int64 arithmetic (Mul/Div/Add/Sub/Range) is refused; exact checked signatures and the `i64_arith` fixture are the ndarray ask (plan §0.3).

**Hardening + census:** explicit ONNX-position → Tract-slot mapping (`tract_slot`), source-bound facts (`merged_for`), collision/stale/tail-bit/ConstantOfShape/Expand tests (55 green, 5 more disable runs red). Jina census: 6,581/114/925, 4,499 folded; the 56 blocked Reshapes all wait on int64 `Mul`; not folded = 2,461 runtime + 660 shape-only blocked.
36 changes: 36 additions & 0 deletions .claude/plans/d-tract-harvest-0-native-algebra-bridge-v1.md
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,42 @@ Tests (40, all green): `shape_chain_folds_and_the_data_nodes_run_against_ort`, `
- `ConstantOfShape` and `Expand` map onto ndarray `from_elem` / `broadcast` and are not registered yet.
- Multi-tile orchestration and full Jina MatMul execution remain separate gates.

### 0.3 After #400 / #1853 (2026-10-30)

Owner decisions: int64 shape arithmetic GO under checked, fail-closed admission (Div truncates toward zero; a zero divisor or an overflow refuses); an axis stays a guarded parameter of one method unless a different axis changes the behaviour law; ConstantOfShape and Expand registered on existing ndarray capabilities; Erf numerically accepted as Bounded, its performance open.

**Registry v3.** int64 `Equal` 0x0F70 and `LessOrEqual` 0x0F71 (ndarray #400 `eq/le_i64_pair_to_mask`, scalar right side `eq/le_i64_to_mask`; a same-shape or one-element right side only, other broadcasts not admitted), int64 `Where` 0x0F72 (`blend_i64` / `blend_i64_scalar`), `ConstantOfShape` 0x0F73 (`ArrayD::from_elem` of the value attribute, constant non-negative shape), `Expand` int64/f32 0x0F74/0x0F75 (`ndarray` `broadcast` to the multidirectional broadcast). Fixture `shape_i64`: every int64 node over `Shape(F)` folds, `Expand(F)` runs, every output equals ORT.

**Optional output slots.** Tract numbers a node's outlets after dropping empty output names (`onnx/src/model.rs:150`). Fixtures `lstm_skip` (`LSTM` outputs `["", "Y_h"]`) and `lstm_full` pin that `source_producers` names slot 0 resp. 1 for `Y_h` and that the admitted fact is `Y_h`'s (ORT `[1,1,2]`), not the omitted `Y`'s (`[5,1,1,2]`). Disable run (count empty slots): red.

**Coverage, Jina pinned `[1,10]`:** 6,404 / 56 / 1,160 → **6,581 / 114 / 925**; 4,499 nodes fold. The 114 not-true: Reshape 56 and Expand 57 UNKNOWN (target computed by unregistered int64 arithmetic), LessOrEqual 1 not admitted (a `[S,1]` vs `[1,S]` broadcast). Unregistered shape-class nodes left: Mul 115, Div 56, Range 4, Add 1, plus Cast to bool/float 2, And, Cos, Sin, MatMul, Transpose 1 each.

**ndarray ask (D-TRACT-SHAPE-1, after #400).** #400 already supplies the int64 compares (`eq/lt/le/gt/ge_i64[_pair]_to_mask`) and `blend_i64[_scalar]`; they are registered. What is missing, by exact signature (fail-closed: `Err` and an unchanged `dst` content contract is not required, but no partial result may be returned as success):

```rust
pub enum IntArithError { Overflow { index: usize }, DivideByZero { index: usize }, ZeroStep }
pub fn add_i64_checked(a: &[i64], b: &[i64], dst: &mut [i64]) -> Result<(), IntArithError>;
pub fn sub_i64_checked(a: &[i64], b: &[i64], dst: &mut [i64]) -> Result<(), IntArithError>;
pub fn mul_i64_checked(a: &[i64], b: &[i64], dst: &mut [i64]) -> Result<(), IntArithError>;
/// Truncates toward zero; `i64::MIN / -1` is Overflow.
pub fn div_i64_trunc_checked(a: &[i64], b: &[i64], dst: &mut [i64]) -> Result<(), IntArithError>;
// one-element right side, as blend_i64_scalar
pub fn add_i64_scalar_checked(a: &[i64], b: i64, dst: &mut [i64]) -> Result<(), IntArithError>;
pub fn sub_i64_scalar_checked(a: &[i64], b: i64, dst: &mut [i64]) -> Result<(), IntArithError>;
pub fn mul_i64_scalar_checked(a: &[i64], b: i64, dst: &mut [i64]) -> Result<(), IntArithError>;
pub fn div_i64_trunc_scalar_checked(a: &[i64], b: i64, dst: &mut [i64]) -> Result<(), IntArithError>;
/// ONNX Range: max(ceil((limit - start) / delta), 0) elements; delta 0 is ZeroStep.
pub fn range_i64_checked(start: i64, limit: i64, delta: i64) -> Result<Vec<i64>, IntArithError>;
```

Accuracy: exact (integers). Panics only on a length mismatch, as the #400 kernels. Fixtures: `crates/tract-harvest-probe/fixtures/tiny/i64_arith.onnx` with ORT `ORT_DISABLE_ALL` outputs in `ort.json` (`Div([-7, 7], [2, 3]) = [-3, 2]`, `Mul([2, 3], [3, -4]) = [6, -12]`, `Add([2, 3], [-5, 10]) = [-3, 13]`, `Sub = [7, -7]`, `Range(0, 3, 1) = [0, 1, 2]`); refusal cases ORT does not cover: `add(i64::MAX, 1)`, `mul(i64::MIN, -1)`, `div(i64::MIN, -1)`, `div(x, 0)`, `range(0, 5, 0)` each `Err`; `div(-7, 2) = -3`, `div(7, -2) = -3`, `range(5, 0, -2) = [5, 3, 1]`, `range(0, 0, 1) = []`. Test `int64_arithmetic_is_refused_until_checked_words_exist` pins the current refusal.

Disable runs (each red): Equal kernel replaced by `le`; slot counted over empty outputs; general broadcast admitted; broadcast mismatch accepted; ConstantOfShape ignoring its value. 46 tests green.

**Hardening (same PR).** `source_producers` enumerates each node's ONNX output positions first and maps a position to Tract's slot with `dr3::tract_slot` (named outputs before it). `FactSources` records the source it was read from; `merged_for` refuses facts of another model. Tests: `["", "Y"]` and multi-output mapping; producer collisions (two producers, a value that is also an input or initializer, duplicate node names, unnamed node without a first output); a fact from a renamed producer; facts of another model; int64 compares and Where over 70 elements (tail bits clear, scalar and pair); ConstantOfShape (default float 0, empty shape gives a scalar, zero dims, bool fill, 1-D shape input, K3 refusals) and Expand (multidirectional broadcast). Disable runs (each red): ONNX position used as the slot; no binding check; collisions keep a producer; bool fill tail bits; ConstantOfShape rank. 55 tests green.

**Census (Jina, `[1,10]`, `examples/shape_census.rs`).** WHEN-true / not-true / unregistered **6,581 / 114 / 925** (registry v1 4,146 / 0 / 3,474; v2 6,404 / 56 / 1,160). Cold-folded nodes 4,499 (v2 4,440, +59 ConstantOfShape; v1 plan had no folding). **The 56 Reshapes blocked in v2 still do not resolve: the first unregistered op their target depends on is int64 `Mul` in all 56.** Not folded: runtime 2,461 (Mul 450, Add 253, MatMul 252, Cast 228, Reshape 170, Slice 140, Transpose 140, Div/Pow/ReduceMean/Sqrt 113 each, …) and shape-only blocked 660 (Unsqueeze 181, Cast 119, Mul 117, Equal 58, Where 58, Concat 57, Div 56, Range 4, …). The integration acceptance (a whole shape-arithmetic chain folding or executing through admitted methods and matching ORT) waits on the checked int64 words; `i64_arith` is its fixture. No full Jina runtime is started.

## 1. The acceptance chain, demonstrated

The chain under test: a source-attested ONNX subgraph is imported by Tract, admitted, lowered onto existing native methods, executed without Tract, and verified against ONNX Runtime (ORT). The chain holds for both fixtures: fixture A (tiny, synthetic) is bit-exact, and fixture B (a real model slice) is bounded. The numbers are in §4. Nothing here is certified, production or merged.
Expand Down
99 changes: 99 additions & 0 deletions crates/tract-harvest-probe/examples/shape_census.rs
Original file line number Diff line number Diff line change
Expand Up @@ -98,8 +98,107 @@ fn main() {
for op in OPS {
println!(" {op:>10} {:?}", cov.get(*op));
}
let not_true: Vec<_> = cov
.iter()
.filter(|(_, c)| c[1] > 0)
.map(|(k, c)| (k.as_str(), c[1]))
.collect();
println!(" WHEN not true by op: {not_true:?}");
println!("foldable by dependency but not folded:");
for (why, c) in by {
println!(" {c:>5} {why}");
}

// The Reshapes whose WHEN is not TRUE: which unregistered ops their
// target depends on (the first unregistered or unfolded-unregistered
// ancestors along the target input).
let producer: std::collections::HashMap<&str, usize> = src
.nodes
.iter()
.enumerate()
.flat_map(|(i, n)| n.outputs.iter().map(move |o| (o.as_str(), i)))
.collect();
let mut consts: std::collections::HashMap<&str, &tract_harvest_probe::value::Value> = src
.initializers
.iter()
.filter_map(|i| i.value.as_ref().map(|v| (i.name.as_str(), v)))
.collect();
for (k, v) in &f.values {
consts.insert(k.as_str(), v);
}
let mut blocked_reshape = 0;
let mut roots = std::collections::BTreeMap::<String, usize>::new();
for n in src.nodes.iter().filter(|n| n.op_type == "Reshape") {
let args: Vec<_> = n.inputs.iter().map(|i| facts.get(i)).collect();
let Some(r) = reg.lookup(n, &args) else {
continue;
};
let c = n
.inputs
.iter()
.map(|i| consts.get(i.as_str()).copied())
.collect();
if (r.when)(&registry::NodeView {
node: n,
args,
consts: c,
}) == registry::K3::True
{
continue;
}
blocked_reshape += 1;
let mut stack = vec![n.inputs[1].as_str()];
let mut seen = std::collections::HashSet::new();
let mut found = std::collections::BTreeSet::new();
while let Some(v) = stack.pop() {
if consts.contains_key(v) || !seen.insert(v) {
continue;
}
let Some(&p) = producer.get(v) else { continue };
let pn = &src.nodes[p];
let pargs: Vec<_> = pn.inputs.iter().map(|i| facts.get(i)).collect();
if reg.lookup(pn, &pargs).is_none() {
found.insert(format!(
"{}({:?})",
pn.op_type,
registry::signature_dtype(pn, &pargs, Some(0)).unwrap()
));
} else {
stack.extend(pn.inputs.iter().map(String::as_str));
}
}
*roots
.entry(found.into_iter().collect::<Vec<_>>().join(" + "))
.or_default() += 1;
}
println!("Reshape with WHEN not TRUE: {blocked_reshape}; unregistered ops their target depends on: {roots:?}");
// Not folded: runtime (reads an input value) vs shape-only (blocked).
let mut runtime = std::collections::BTreeMap::<&str, usize>::new();
let mut shape_only = std::collections::BTreeMap::<&str, usize>::new();
for (i, n) in src.nodes.iter().enumerate() {
if f.nodes.contains(&i) {
continue;
}
let m = if node_dep[i] >= fold::Dep::Symbolic {
&mut runtime
} else {
&mut shape_only
};
*m.entry(n.op_type.as_str()).or_default() += 1;
}
fn top<'a>(m: &std::collections::BTreeMap<&'a str, usize>) -> Vec<(&'a str, usize)> {
let mut v: Vec<_> = m.iter().map(|(k, c)| (*k, *c)).collect();
v.sort_by(|a, b| b.1.cmp(&a.1));
v
}
println!(
"not folded: runtime {} nodes {:?}",
runtime.values().sum::<usize>(),
top(&runtime)
);
println!(
"not folded: shape-only (blocked) {} nodes {:?}",
shape_only.values().sum::<usize>(),
top(&shape_only)
);
}
Binary file not shown.
Binary file not shown.
Binary file not shown.
80 changes: 80 additions & 0 deletions crates/tract-harvest-probe/fixtures/tiny/ort.json
Original file line number Diff line number Diff line change
Expand Up @@ -138,6 +138,86 @@
"neg_concat": {
"sha256": "f92f5872d18536685cf38fa0a627ceb7fdd7fda6bf908113d1127358c647aed2",
"ort_error": "Fail: [ONNXRuntimeError] : 1 : FAIL : Node (n_concat) Op (Concat) [ShapeInferenceError] Can't merge shape info. Both inferred and declared dimension have values but they differ. Inferred=2 Declared=3 Dimens"
},
"shape_i64": {
"sha256": "19d1dd7da1b55a36b977d582f8a4b3f4a26b6ffc5bc571027701c9f7352a230b",
"ort": {
"W": {
"shape": [2],
"dtype": "int64",
"bits": [2,7]
},
"LE": {
"shape": [2],
"dtype": "bool",
"bits": [1,0]
},
"CS": {
"shape": [2,3],
"dtype": "int64",
"bits": [5,5,5,5,5,5]
},
"ER": {
"shape": [2,3],
"dtype": "int64",
"bits": [1,2,3,1,2,3]
},
"EF": {
"shape": [2,2,3],
"dtype": "float32",
"bits": [1069547520,3196059648,1077936128,1036831949,1088421888,3223322624,1069547520,3196059648,1077936128,1036831949,1088421888,3223322624]
}
}
},
"lstm_skip": {
"sha256": "e979463f372fd8bfa4cb2ca46a06c4459f5866786f2b593933e9f34d8f5819f4",
"ort": {
"Y_h": {
"shape": [1,1,2],
"dtype": "float32",
"bits": [1049333655,1049333655]
}
}
},
"lstm_full": {
"sha256": "3d5456afad55b4f5fb01ba3c81ed6f7123d72e028f22e6ed5ad00c6a85286ce1",
"ort": {
"Y_h": {
"shape": [1,1,2],
"dtype": "float32",
"bits": [1049333655,1049333655]
}
}
},
"i64_arith": {
"sha256": "042a71f755ea7ef7ffe16ef1a3dd57bcdadbc3ee5f4b752d5dbc1de9543399db",
"ort": {
"DV": {
"shape": [2],
"dtype": "int64",
"bits": [-3,2]
},
"ML": {
"shape": [2],
"dtype": "int64",
"bits": [6,-12]
},
"AD": {
"shape": [2],
"dtype": "int64",
"bits": [-3,13]
},
"SB": {
"shape": [2],
"dtype": "int64",
"bits": [7,-7]
},
"RG": {
"shape": [3],
"dtype": "int64",
"bits": [0,1,2]
}
}
}
},
"erf_sweep": {
Expand Down
Binary file not shown.
Loading
Loading