dt64: lane binding refuses a predicate change at a bound position (D-DRDT-SPLIT-1 S8)

.claude/plans/dr-widefieldmask-dt-classview-v1.md

@@ -384,7 +384,7 @@ the question.
 | S5 | Bind-time admission for the four direct paths, with the executor census test | v2 cut 4; W2, W13 | EXO-253, EXO-245, EXO-246 | red on a planted call site | needs council |
 | S6 | Behaviour as classes that outlives the process: binding digest recorded with the execution and the DR version; typed lane interpretation from the class | v2 cut 7; W5; G5 | EXO-199, EXO-225, EXO-221, EXO-202, EXO-247 | replay falsifier (row 17) red first | needs council |
 | S7 | The versioned DR × DT mappings over D-NFR-1 (identities, properties, source positions, class binding, criteria), keyed onto the shipped `MapTable` log (D-DR-VMAP, #1923, `RouteVersion`), no new store instance, handed out by reference; contents stay with the source owner; per-request masks stay outside | §1b; W5 | EXO-253, EXO-220 | D-NFR-1 first: bind, seal, execute, advance one revision, gates: mapping N replayed reproduces the same assignment (identities, properties, source positions) bit for bit; over unchanged contents the result is bit-equal too; over changed contents with unchanged positions the assignment is unchanged and the values follow the source; a mapping whose positions or identities do not match the source refuses; then the same for a mapping kept in the store; authorization checked independently | lab code |
-| S8 | Close the reorder gap on the hot check (D-DT64-7 L5d), keyed on revision, not a digest | W2 | EXO-199 | the pinned test turns red-to-green; an unchanged view still admits; at most a few ns per check | dt64 |
+| S8 | Close the reorder gap on the hot check (D-DT64-7 L5d), by comparing the predicate IRI recorded at bind time at each bound position (no hashing on the hot path; a revision key alone cannot see a reorder that keeps the field count) | W2 | EXO-199 | the pinned test turns red-to-green; an unchanged view and a label-only rename still admit; check cost measured (whole check, not the increment) | dt64 |
 
 Order: S1 (finish) and S2 now. S4 next (a consumer is waiting on EXO-243
 and EXO-244). Then D-NFR-1 and S7, S3 and S8 in parallel. S5 and S6 need

crates/lance-graph-dt64/examples/lane_check_cost.rs

@@ -0,0 +1,216 @@
+//! Cost of the hot `LaneBinding::check`, per check and per bound lane.
+//!
+//! Run: `cargo run --release -p lance-graph-dt64 --example lane_check_cost`
+//!
+//! The "before" figure (no per-position predicate compare) is obtained by
+//! applying the disable edit that turns the guard condition in
+//! `LaneBinding::check` into `if false {` and re-running. The numbers are a
+//! report, not an assertion: the example does not fail on a threshold.
+
+use std::hint::black_box;
+use std::time::Instant;
+
+use lance_graph_contract::class_view::{ClassId, ClassView, WideFieldMask};
+use lance_graph_contract::ontology::{DisplayTemplate, FieldRef};
+use lance_graph_dt64::dr::{Frame, FrameRevisions, FrameStore, Scope};
+use lance_graph_dt64::{
+    BindStore, ClassSchema, CoordSpace, Extent, LaneAddr, LaneBinding, LaneRefusal, LaneRequest,
+    LaneSource, RouteAt, SchemaRev,
+};
+
+const CLASS: u32 = 0x0C1A_0001;
+const VIEW_CLASS: ClassId = 0x0C1A;
+const POSITION: u16 = 5;
+const FIELDS: usize = 16;
+const SPACE: CoordSpace = CoordSpace {
+    population: 1,
+    coordinates: 1,
+};
+const READER: Scope = Scope { id: 7 };
+
+struct View(Vec<FieldRef>);
+
+impl View {
+    fn sixteen() -> View {
+        View(
+            (0..FIELDS)
+                .map(|i| {
+                    FieldRef::new(
+                        format!("https://example.org/dir/attribute{i:02}"),
+                        format!("Attribute {i:02}"),
+                    )
+                })
+                .collect(),
+        )
+    }
+}
+
+impl ClassView for View {
+    fn fields(&self, class: ClassId) -> &[FieldRef] {
+        if class == VIEW_CLASS {
+            &self.0
+        } else {
+            &[]
+        }
+    }
+    fn template(&self, _class: ClassId) -> DisplayTemplate {
+        DisplayTemplate::Detail
+    }
+    fn dolce_category_id(&self, _class: ClassId) -> u8 {
+        0
+    }
+}
+
+/// Positional source: field `n` lives in lane `n`; the basis is ignored.
+struct Source {
+    map: [LaneAddr; FIELDS],
+    lanes: Vec<i32>,
+    frames: FrameStore,
+}
+
+impl Source {
+    fn new() -> Source {
+        let map = core::array::from_fn(|i| LaneAddr {
+            space: SPACE,
+            lane: i as u16,
+            scope: READER,
+        });
+        Source {
+            map,
+            lanes: vec![1, 2, 3, 4],
+            frames: FrameStore::new(FrameRevisions {
+                source: 1,
+                relation_map: 1,
+                coordinates: 1,
+            }),
+        }
+    }
+}
+
+impl LaneSource for Source {
+    type Lane<'a> = &'a [i32];
+    fn lane_of(
+        &self,
+        _class: u32,
+        _rev: SchemaRev,
+        field: u8,
+        _basis: &FieldRef,
+        _frame: &Frame,
+    ) -> Option<LaneAddr> {
+        Some(self.map[usize::from(field)])
+    }
+    fn borrow(&self, _addr: &LaneAddr) -> Option<&[i32]> {
+        Some(&self.lanes[..])
+    }
+    fn frames(&self) -> &FrameStore {
+        &self.frames
+    }
+}
+
+fn bind(
+    store: &BindStore,
+    view: &View,
+    source: &Source,
+    frame: &Frame,
+    route: RouteAt,
+    k: usize,
+) -> LaneBinding {
+    let positions: Vec<u8> = (0..k as u8).collect();
+    let mask = WideFieldMask::from_positions(&positions);
+    store
+        .bind_lanes(
+            view,
+            source.frames(),
+            source,
+            LaneRequest {
+                route,
+                rev: SchemaRev(1),
+                fields: &mask,
+                frame,
+                scope: READER,
+                selection: SPACE,
+            },
+        )
+        .expect("bind")
+}
+
+/// Minimum over 7 repetitions of 2,000,000 calls, in nanoseconds per call.
+fn time<F: FnMut() -> bool>(mut call: F) -> f64 {
+    for _ in 0..100_000 {
+        black_box(call());
+    }
+    let mut best = f64::MAX;
+    for _ in 0..7 {
+        let start = Instant::now();
+        for _ in 0..2_000_000u32 {
+            black_box(call());
+        }
+        let ns = start.elapsed().as_nanos() as f64 / 2_000_000.0;
+        if ns < best {
+            best = ns;
+        }
+    }
+    best
+}
+
+fn main() {
+    let view = View::sixteen();
+    let mut store = BindStore::new();
+    store
+        .register(
+            &view,
+            CLASS,
+            ClassSchema {
+                schema_rev: SchemaRev(1),
+                field_count: FIELDS,
+                extent: Extent::DR64_CUBE,
+            },
+            Vec::new(),
+        )
+        .expect("register");
+    let version = store.route(POSITION, CLASS).expect("route");
+    let route = RouteAt {
+        position: POSITION,
+        version,
+    };
+    let source = Source::new();
+    let frame = source.frames().seal();
+
+    for k in [1usize, 4, 16] {
+        let binding = bind(&store, &view, &source, &frame, route, k);
+        assert!(binding
+            .check(&store, &view, source.frames(), &source)
+            .is_ok());
+        let ns = time(|| {
+            black_box(&binding)
+                .check(
+                    black_box(&store),
+                    black_box(&view),
+                    source.frames(),
+                    black_box(&source),
+                )
+                .is_ok()
+        });
+        println!(
+            "lane_check k={k:<2} ns_per_check={ns:.2}  ns_per_lane={:.2}",
+            ns / k as f64
+        );
+    }
+
+    let binding = bind(&store, &view, &source, &frame, route, 1);
+    let mut swapped = View::sixteen();
+    swapped.0.swap(0, 1);
+    let refused = binding.check(&store, &swapped, source.frames(), &source);
+    assert!(matches!(refused, Err(LaneRefusal::PredicateChanged { .. })));
+    let ns = time(|| {
+        black_box(&binding)
+            .check(
+                black_box(&store),
+                black_box(&swapped),
+                source.frames(),
+                black_box(&source),
+            )
+            .is_err()
+    });
+    println!("lane_check k=1 refused ns_per_check={ns:.2}");
+}

crates/lance-graph-dt64/src/lane.rs

@@ -6,7 +6,7 @@
 //! owner says, through [`LaneSource`], which of its own lanes holds a field
 //! and in whose row order. [`BindStore::bind_lanes`] joins that answer with
 //! the class route and the source frame into a [`LaneBinding`], which holds
-//! addresses only, never a value.
+//! addresses and the bound predicate identities, never a value.
 //!
 //! The class route and the frame are checked as a pair: the route against
 //! this store's own route log, the frame against the [`FrameStore`] that
@@ -131,8 +131,14 @@ pub enum LaneRefusal {
     /// The store binds the class over another basis than the one this binding
     /// was made against. A store never changes a bound class (D5), so this
     /// fires only when the binding is checked against ANOTHER store; it says
-    /// nothing about the view, which the hot check does not re-hash.
+    /// nothing about the view; a view that changed at a bound position is
+    /// `PredicateChanged`.
     StoreBasisMismatch { class: u32 },
+    /// The view names another predicate at a bound position than the one the
+    /// binding was made over. Compared per bound field by `predicate_iri`,
+    /// without hashing; a label-only rename does not fire it, and a change
+    /// at a position the binding did not bind does not either.
+    PredicateChanged { class: u32, field: u8 },
     /// The source maps the field to another lane than it did at bind.
     MappingChanged { field: u8 },
     /// The source no longer holds the lane.
@@ -148,7 +154,8 @@ impl From<Refusal> for LaneRefusal {
 }
 
 /// A validated set of lane addresses for one class under one route and one
-/// frame. Holds addresses only.
+/// frame. Holds addresses and, per bound field, the predicate identity it was
+/// bound over. Never a value.
 #[derive(Debug, Clone)]
 pub struct LaneBinding {
     class: u32,
@@ -159,6 +166,10 @@ pub struct LaneBinding {
     selection: CoordSpace,
     fields: WideFieldMask,
     lanes: Vec<(u8, LaneAddr)>,
+    /// Parallel to `lanes`: the `predicate_iri` each bound field had in the
+    /// witnessed basis at bind. An identity, never a value. The hot check
+    /// compares the view's field at each bound position against it.
+    predicates: Vec<Box<str>>,
     /// The witness of the basis the class was bound with when this binding
     /// was made: one `u128`, compared on the hot path without hashing.
     basis: crate::BasisDigest,
@@ -189,6 +200,7 @@ impl BindStore {
             .bound_basis(class)
             .ok_or(Refusal::UnknownClass(class))?;
         let mut lanes = Vec::with_capacity(req.fields.count() as usize);
+        let mut predicates = Vec::with_capacity(req.fields.count() as usize);
         for field in 0..=u8::MAX {
             if !req.fields.has(field) {
                 continue;
@@ -201,6 +213,7 @@ impl BindStore {
                 .ok_or(LaneRefusal::Unbound { class, field })?;
             admit_lane(field, &addr, req.scope, req.selection)?;
             lanes.push((field, addr));
+            predicates.push(Box::<str>::from(field_ref.predicate_iri.as_str()));
         }
         Ok(LaneBinding {
             class,
@@ -211,6 +224,7 @@ impl BindStore {
             selection: req.selection,
             fields: req.fields.clone(),
             lanes,
+            predicates,
             basis,
         })
     }
@@ -296,14 +310,15 @@ impl LaneBinding {
     /// Hot: the bind's checks again, without allocating and without hashing
     /// the basis. The frame against its store; the route against the store's
     /// CURRENT version (a re-route since the bind is refused); the store's
-    /// basis witness against the one recorded at bind (a `u128` compare); the
-    /// view's basis at the bound revision by revision and field count only;
-    /// and every lane against what the source maps now.
+    /// basis witness against the one recorded at bind (one `u128`); the
+    /// view's basis at the bound revision by revision and field count; each
+    /// bound position's `predicate_iri` against the one recorded at bind (a
+    /// string compare, no hashing); and every lane against what the source
+    /// maps now.
     ///
-    /// NOT checked here: that `view` still has the ordered predicates it had
-    /// at bind. A same-count reorder in the view after the bind is caught only
-    /// when the source maps lanes by predicate (`MappingChanged`); a
-    /// positional source passes it. Re-bind after any basis change.
+    /// NOT checked here: positions the binding did not bind. A same-count
+    /// change confined to unbound positions passes this check and is refused
+    /// by `BindStore::resolve`.
     pub fn check<V: ClassView + ?Sized, S: LaneSource>(
         &self,
         store: &BindStore,
@@ -314,18 +329,17 @@ impl LaneBinding {
         source_owns(frames, source)?;
         frames.check(&self.frame).map_err(LaneRefusal::Frame)?;
         current_route(store, self.route.position, self.class)?;
-        // Revision and count only: the ordered predicate witness was checked
-        // when the binding was made (bind_lanes resolves through the
-        // witnessed `resolve`), and re-hashing the basis here would put
-        // schema hashing on the hot path. A basis that changes order after
-        // the bind is caught below only when the source maps lanes by
-        // predicate (D-LANESOCK-3, `MappingChanged`); re-bind after any
-        // basis change. (D-DT64-7 L5d decides whether the R2IL arm re-binds.)
+        // Revision and count here: the whole-basis witness was checked when
+        // the binding was made (bind_lanes resolves through the witnessed
+        // `resolve`), and re-hashing the basis would put schema hashing on
+        // the hot path. The bound positions are compared below, each against
+        // the predicate recorded at bind, so a reorder that moves a bound
+        // field is refused even when the source maps lanes by position.
         let (fields, bound) = store.resolve_counted(view, self.class, self.rev)?;
         if bound != self.basis {
             return Err(LaneRefusal::StoreBasisMismatch { class: self.class });
         }
-        for (field, addr) in &self.lanes {
+        for ((field, addr), bound_iri) in self.lanes.iter().zip(&self.predicates) {
             let field = *field;
             let field_ref = fields
                 .get(usize::from(field))
@@ -343,6 +357,12 @@ impl LaneBinding {
                     })
                 }
             }
+            if field_ref.predicate_iri.as_str() != &**bound_iri {
+                return Err(LaneRefusal::PredicateChanged {
+                    class: self.class,
+                    field,
+                });
+            }
             admit_lane(field, addr, self.scope, self.selection)?;
         }
         Ok(())