tract-harvest-probe: DR64 is global to local; the codebook spans mask blocks

.claude/board/STATUS_BOARD.md

@@ -91,7 +91,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 (one ONNX lens classid; each op signature a field under it labelling a classid-free algebra address → native DO, #1870); 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 | **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.4 | #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. Checked int64 follow-up **In PR** (plan §0.4): registry v4, int64 Add/Sub/Mul/Div/Range on ndarray #401; `i64_arith` folds and matches ORT; Jina 6,871/1/748, all shape-dependent Reshapes fold; remaining shape-only blockers are the rotary-embedding chain, And, one broadcast LessOrEqual. Rotary follow-up **In PR** (plan §0.5): registry v5 (Cast i64→f32/bool, MatMul f32, Transpose, Cos/Sin, And, any-broadcast compares), pinned external inv_freq; Jina rotary fold matches ORT ≤ 1 ULP; Jina 7,274/0/346, 0 shape-only nodes blocked (#1858 merged). Bind-store consumer follow-up **In PR** (plan §0.6): `bind::route` / `bind::resolve` split the registry into DR64 route and DT64 bind store; equal to `lookup` on all tiny fixtures; Jina 7,274 routed+resolved / 346 unrouted (#1865 merged). **Correction In PR** (plan §0.7): one classid is the ONNX codebook lens; op signatures are items `MethodKey { lens, ordinal }` (registry v6). **Field view** #1867 merged (plan §0.8); ONNX is one classid (`ONNX_LENS`), per-op ids purged from the plan text and from D-DT64-6 A.2 (In PR): registry v7 splits lens-agnostic algebra addresses (`methods`) from the lens's labelled fields (`regs`) and its `WideFieldMask` (`exposed`) |
+| **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.4 | #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. Checked int64 follow-up **In PR** (plan §0.4): registry v4, int64 Add/Sub/Mul/Div/Range on ndarray #401; `i64_arith` folds and matches ORT; Jina 6,871/1/748, all shape-dependent Reshapes fold; remaining shape-only blockers are the rotary-embedding chain, And, one broadcast LessOrEqual. Rotary follow-up **In PR** (plan §0.5): registry v5 (Cast i64→f32/bool, MatMul f32, Transpose, Cos/Sin, And, any-broadcast compares), pinned external inv_freq; Jina rotary fold matches ORT ≤ 1 ULP; Jina 7,274/0/346, 0 shape-only nodes blocked (#1858 merged). Bind-store consumer follow-up **In PR** (plan §0.6): `bind::route` / `bind::resolve` split the registry into DR64 route and DT64 bind store; equal to `lookup` on all tiny fixtures; Jina 7,274 routed+resolved / 346 unrouted (#1865 merged). **Correction In PR** (plan §0.7): one classid is the ONNX codebook lens; op signatures are items `MethodKey { lens, ordinal }` (registry v6). **Field view** #1867 merged (plan §0.8); ONNX is one classid (`ONNX_LENS`), per-op ids purged from the plan text and from D-DT64-6 A.2 (#1870 merged); **DR64 global to local In PR** (plan §0.9, #1872): graphs and codebook beyond 64/256 positions, full Jina builds and schedules over 391 tiles: registry v7 splits lens-agnostic algebra addresses (`methods`) from the lens's labelled fields (`regs`) and its `WideFieldMask` (`exposed`) |
 
 ## D-TFLP — TFLite models on the native polyfill: int8 codes as Palette256 (2026-10-25)
 

.claude/board/entries/2026-10-30-d-tract-shape-1-cold-shape-folding.md

@@ -25,3 +25,5 @@ Fixtures (ORT 1.29.0 `ORT_DISABLE_ALL`): shape chain bit-exact; Erf ≤ 2 ULP vs
 **CORRECTION (plan §0.7):** a classid is a codebook lens, not a codebook item. The per-op-signature classids (0x0F01…0x0F82) in every paragraph above are superseded: registry v6 reads the ONNX op codebook through one lens (`ONNX_LENS`) and addresses each signature as `MethodKey { lens, ordinal }`, ordinal = position. Bind-store routes carry the key; `resolve` fails as Route / Lens / Item. Results unchanged; 2 disable runs red.
 
 **Field view (plan §0.8):** registry v7 follows ClassView + `WideFieldMask` (the Redmine ERB field-view pattern). `methods` are lens-agnostic algebra addresses, one DO body each; `regs` are the lens's fields, labelling one address each with a signature and its WHEN; `exposed` is the lens's `WideFieldMask`. A field outside the mask neither matches nor resolves, and `Registry::revision()` (version + exposed positions) keys the frame and the routes. 48 fields share fewer addresses. Jina unchanged; 4 disable runs red.
+
+**DR64 global to local (plan §0.9):** `OnnxGraph::build` no longer refuses graphs beyond one tile. Positions map to (tile, local bit); `on`/`do_`/`dep` are `Tiled` relations composed tile by tile with the one DR64 kernel; the only ceiling is 65,536 positions. Full Jina (7,620 nodes, 7,939 values) builds, its tiled `dep` (391 tiles) equals the source edges, and it schedules. The registry's exposure mask is blocked by 256, so the codebook reaches 65,536 fields. 3 disable runs red.

.claude/plans/d-tract-harvest-0-native-algebra-bridge-v1.md

@@ -263,6 +263,18 @@ The user said the classid + `WideFieldMask` ergonomics is the Redmine ERB field-
 
 **Open.** The WHEN guards are on the fields. Some are only meaningful for one address, for example a Reshape guard over its target shape. Whether a guard belongs with its field or its address is not settled here. `exposed` is set to full by `build`, and no production lens is minted.
 
+### 0.9 DR64 is global to local; the codebook spans mask blocks (2026-10-30)
+
+The user: "the codebook should not be limited to 64 if Jina asks for more" and "DR64 is global to local, not a rejection to access 64k soa". `OnnxGraph::build` refused any graph beyond one 64 × 64 tile (`TileOverflow`). That was wrong.
+
+- **Graph.** A global position `p` is bit `p % 64` of tile `p / 64`. `on` and `do_` are `dr3::Tiled` relations: their non-empty DR64 tiles, keyed `(row tile, column tile)`. `dep = do_ ∘ read_by` composes tile by tile with the same `relcomp::compose` kernel, and `schedule` reads `dep`'s pairs. The only refusal left is the u16 address width (`Refusal::AddressOverflow`, 65,536 positions per axis).
+- **Jina, measured.** The full graph (7,620 nodes, 7,939 values) builds; its tiled `dep` (391 tiles, 9,176 edges) equals the source edges; it schedules, and every edge runs forward.
+- **Codebook.** One `WideFieldMask` position is a `u8`, so the exposure mask stopped the lens at 256 fields. `Registry::exposed` is now a list of masks: field `o` is position `o % 256` of block `o / 256`, up to 65,536 fields. `Registry::expose` shows or hides one field.
+
+**Tests.** `graphs_beyond_one_tile_lay_over_tiles` (200-node chain over four Identity tiles, with a cross-tile edge), `codebook_spans_mask_blocks` (600 fields over three blocks), and the full-graph Jina assertions. Disable runs, each red: compose restricted to the diagonal column tile; `exposes` reading block 0 only; `set` dropping cross-tile bits.
+
+**Not yet.** `plan::resolve` still refuses Jina at its first unregistered node (346 remain); tiling removes the size refusal, not the coverage gap.
+
 ## 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.

crates/tract-harvest-probe/src/bind.rs

@@ -43,8 +43,8 @@ pub enum Unresolved {
 }
 
 /// Bind every node by signature once, keeping only its codebook key. The
-/// binder reads per-value facts, not a tile: a node position is the source
-/// node index, so a graph larger than one 64-node tile routes too.
+/// binder reads per-value facts: a node position is the global source node
+/// index, the same one the DR64 tiles map to local bits.
 /// Initializers without a fact get their protobuf dtype and dims, as in
 /// `fold`.
 pub fn route(src: &SourceInventory, facts: &HashMap<String, Fact>, registry: &Registry) -> Routes {

crates/tract-harvest-probe/src/dr3.rs

@@ -1,7 +1,12 @@
 //! An ONNX graph as a DR#3 graph (user decision 2026-10-30): every node is an
 //! **Identity** position, every tensor value (graph input, initializer, node
-//! output) a **Property** position, and the dataflow is two relations over one
-//! 64 × 64 tile:
+//! output) a **Property** position, and the dataflow is two relations:
+//!
+//! DR64 is global to local, not a size limit. A global position `p` lives in
+//! tile `p / 64` at local bit `p % 64`; a relation is the set of its non-empty
+//! 64 × 64 tiles ([`Tiled`]), and composition composes tile by tile with the
+//! one DR64 kernel. The only ceiling is the address width: 65,536 positions
+//! per axis.
 //!
 //! - `on[node]`: the Property positions the node reads (its ON);
 //! - `do_[node]`: the Property positions the node writes (its DO).
@@ -32,14 +37,84 @@ use crate::value::{DType, Value};
 /// Positions per axis in one DR64 tile.
 pub const TILE: usize = 64;
 
+/// Positions per axis a graph may address (the u16 address width).
+pub const MAX_POSITIONS: usize = 1 << 16;
+
+/// A Boolean relation over global positions, held as its non-empty 64 × 64
+/// DR64 tiles keyed `(row tile, column tile)`.
+#[derive(Debug, Clone, Default, PartialEq, Eq)]
+pub struct Tiled {
+    pub tiles: std::collections::BTreeMap<(u16, u16), Rows>,
+}
+
+impl Tiled {
+    pub fn set(&mut self, i: usize, j: usize) {
+        let t = self
+            .tiles
+            .entry(((i / TILE) as u16, (j / TILE) as u16))
+            .or_insert([0; 64]);
+        t[i % TILE] |= 1 << (j % TILE);
+    }
+
+    pub fn contains(&self, i: usize, j: usize) -> bool {
+        self.tiles
+            .get(&((i / TILE) as u16, (j / TILE) as u16))
+            .is_some_and(|t| t[i % TILE] >> (j % TILE) & 1 == 1)
+    }
+
+    /// Every `(i, j)` in the relation, global positions.
+    pub fn pairs(&self) -> impl Iterator<Item = (usize, usize)> + '_ {
+        self.tiles.iter().flat_map(|(&(ti, tj), t)| {
+            t.iter().enumerate().flat_map(move |(r, &row)| {
+                let mut bits = row;
+                std::iter::from_fn(move || {
+                    (bits != 0).then(|| {
+                        let c = bits.trailing_zeros() as usize;
+                        bits &= bits - 1;
+                        (ti as usize * TILE + r, tj as usize * TILE + c)
+                    })
+                })
+            })
+        })
+    }
+
+    pub fn transpose(&self) -> Tiled {
+        Tiled {
+            tiles: self
+                .tiles
+                .iter()
+                .map(|(&(ti, tj), t)| ((tj, ti), transpose(t)))
+                .collect(),
+        }
+    }
+
+    /// `out = self ∘ other`: tile `(ti, tj)` is the OR over `k` of the DR64
+    /// composition of tile `(ti, k)` with tile `(k, tj)`.
+    pub fn compose(&self, other: &Tiled, work: &mut Work) -> Tiled {
+        let mut out = Tiled::default();
+        for (&(ti, k), a) in &self.tiles {
+            for (&(_, tj), b) in other.tiles.range((k, 0)..=(k, u16::MAX)) {
+                let c = compose(a, b, work);
+                if c.iter().any(|&r| r != 0) {
+                    let o = out.tiles.entry((ti, tj)).or_insert([0; 64]);
+                    for (x, y) in o.iter_mut().zip(c) {
+                        *x |= y;
+                    }
+                }
+            }
+        }
+        out
+    }
+}
+
 /// The graph on its two axes.
 pub struct OnnxGraph {
     /// Identity axis: node index in source order.
     pub nodes: usize,
     /// Property axis: value names, position = index.
     pub props: Vec<String>,
-    pub on: Rows,
-    pub do_: Rows,
+    pub on: Tiled,
+    pub do_: Tiled,
     /// Ordered arguments per node (`None`: an omitted optional input).
     pub args: Vec<Vec<Option<usize>>>,
     /// Ordered outputs per node.
@@ -67,10 +142,10 @@ fn transpose(r: &Rows) -> Rows {
 }
 
 impl OnnxGraph {
-    /// Lay the source graph onto the tile. `facts` is keyed by value name.
+    /// Lay the source graph onto DR64 tiles. `facts` is keyed by value name.
     pub fn build(src: &SourceInventory, facts: &HashMap<String, Fact>) -> Result<Self, Refusal> {
-        if src.nodes.len() > TILE {
-            return Err(Refusal::TileOverflow {
+        if src.nodes.len() > MAX_POSITIONS {
+            return Err(Refusal::AddressOverflow {
                 axis: "Identity",
                 count: src.nodes.len(),
             });
@@ -105,20 +180,20 @@ impl OnnxGraph {
                     .collect::<Vec<_>>(),
             );
         }
-        if props.len() > TILE {
-            return Err(Refusal::TileOverflow {
+        if props.len() > MAX_POSITIONS {
+            return Err(Refusal::AddressOverflow {
                 axis: "Property",
                 count: props.len(),
             });
         }
 
-        let (mut on, mut do_) = ([0u64; 64], [0u64; 64]);
+        let (mut on, mut do_) = (Tiled::default(), Tiled::default());
         for (n, (a, o)) in args.iter().zip(&outs).enumerate() {
             for &p in a.iter().flatten() {
-                on[n] |= 1 << p;
+                on.set(n, p);
             }
             for &p in o {
-                do_[n] |= 1 << p;
+                do_.set(n, p);
             }
         }
 
@@ -167,20 +242,26 @@ impl OnnxGraph {
     }
 
     /// `dep[i]` has bit `j` iff node `i` writes a value node `j` reads.
-    pub fn dep(&self) -> (Rows, Work) {
+    pub fn dep(&self) -> (Tiled, Work) {
         let mut w = Work::default();
-        let d = compose(&self.do_, &transpose(&self.on), &mut w);
+        let d = self.do_.compose(&self.on.transpose(), &mut w);
         (d, w)
     }
 
     /// The same relation computed directly from the source edges, for the
     /// check that the composition is the dataflow and nothing else.
-    pub fn dep_from_edges(&self) -> Rows {
-        let mut d = [0u64; 64];
+    pub fn dep_from_edges(&self) -> Tiled {
+        let mut producer: HashMap<usize, Vec<usize>> = HashMap::new();
         for (i, o) in self.outs.iter().enumerate() {
-            for (j, a) in self.args.iter().enumerate() {
-                if a.iter().flatten().any(|p| o.contains(p)) {
-                    d[i] |= 1 << j;
+            for &p in o {
+                producer.entry(p).or_default().push(i);
+            }
+        }
+        let mut d = Tiled::default();
+        for (j, a) in self.args.iter().enumerate() {
+            for p in a.iter().flatten() {
+                for &i in producer.get(p).into_iter().flatten() {
+                    d.set(i, j);
                 }
             }
         }
@@ -192,27 +273,26 @@ impl OnnxGraph {
     pub fn schedule(&self) -> Result<Vec<usize>, Refusal> {
         let (dep, _) = self.dep();
         let mut indeg = vec![0usize; self.nodes];
-        for row in dep.iter().take(self.nodes) {
-            let mut bits = *row;
-            while bits != 0 {
-                indeg[bits.trailing_zeros() as usize] += 1;
-                bits &= bits - 1;
-            }
+        let mut succ: Vec<Vec<usize>> = vec![Vec::new(); self.nodes];
+        for (i, j) in dep.pairs() {
+            indeg[j] += 1;
+            succ[i].push(j);
         }
-        let mut done = 0u64;
+        let mut ready: std::collections::BTreeSet<usize> =
+            (0..self.nodes).filter(|&n| indeg[n] == 0).collect();
         let mut order = Vec::with_capacity(self.nodes);
-        while order.len() < self.nodes {
-            let next = (0..self.nodes)
-                .find(|&n| done & (1 << n) == 0 && indeg[n] == 0)
-                .ok_or(Refusal::Cycle)?;
-            done |= 1 << next;
+        while let Some(next) = ready.pop_first() {
             order.push(next);
-            let mut bits = dep[next];
-            while bits != 0 {
-                indeg[bits.trailing_zeros() as usize] -= 1;
-                bits &= bits - 1;
+            for &j in &succ[next] {
+                indeg[j] -= 1;
+                if indeg[j] == 0 {
+                    ready.insert(j);
+                }
             }
         }
+        if order.len() < self.nodes {
+            return Err(Refusal::Cycle);
+        }
         Ok(order)
     }
 }
@@ -658,6 +738,51 @@ mod tests {
         assert_eq!(why[2], ("d", "source producer not unique"));
     }
 
+    /// DR64 is global to local: a 200-node chain (four Identity tiles, five
+    /// Property tiles) builds, `dep` composed tile by tile equals the source
+    /// edges including a cross-tile edge, and the schedule is the chain order.
+    #[test]
+    fn graphs_beyond_one_tile_lay_over_tiles() {
+        use crate::source::SourceNode;
+        const N: usize = 200;
+        let nodes: Vec<SourceNode> = (0..N)
+            .map(|i| SourceNode {
+                name: format!("n{i}"),
+                op_type: if i == N - 1 { "Add" } else { "Abs" }.into(),
+                domain: String::new(),
+                inputs: if i == 0 {
+                    vec!["x".into()]
+                } else if i == N - 1 {
+                    vec![format!("v{}", i - 1), "v0".into()]
+                } else {
+                    vec![format!("v{}", i - 1)]
+                },
+                outputs: vec![format!("v{i}")],
+                attributes: vec![],
+                attrs: vec![],
+            })
+            .collect();
+        let src = SourceInventory {
+            nodes,
+            inputs: vec!["x".into()],
+            model_sha256: String::new(),
+            inlined: vec![],
+            ir_version: 8,
+            opsets: vec![],
+            initializers: vec![],
+            outputs: vec![format!("v{}", N - 1)],
+        };
+        let g = OnnxGraph::build(&src, &HashMap::new()).unwrap();
+        assert_eq!((g.nodes, g.props.len()), (N, N + 1));
+        let (dep, work) = g.dep();
+        assert_eq!(dep, g.dep_from_edges());
+        assert!(dep.tiles.len() > 1 && work.row_ors > 0);
+        assert_eq!(dep.pairs().count(), N);
+        assert!(dep.contains(0, N - 1), "cross-tile edge v0 -> last");
+        assert!(dep.contains(63, 64), "edge across a tile boundary");
+        assert_eq!(g.schedule().unwrap(), (0..N).collect::<Vec<_>>());
+    }
+
     /// Tract's naming: a named node, else its first output; a duplicated
     /// name or an unnamed node without a first output has no producer.
     #[test]