From 7bbbb917c20445193cca97bac98fdc8e920dd974 Mon Sep 17 00:00:00 2001 From: MesTTo Date: Tue, 23 Jun 2026 20:02:49 +1000 Subject: [PATCH] Add BindingSpace trie trace replay shape --- kernel/src/binding_space.rs | 240 ++++++++++++++++++++++++++++++++++++ 1 file changed, 240 insertions(+) diff --git a/kernel/src/binding_space.rs b/kernel/src/binding_space.rs index d955b239..341821cc 100644 --- a/kernel/src/binding_space.rs +++ b/kernel/src/binding_space.rs @@ -279,6 +279,45 @@ pub struct TrieJoinTraceSummary { pub cursor_nexts: usize, } +/// Replayable prefix tree reconstructed from a trie-join trace. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct TrieJoinTraceReplayShape { + /// Locally validated aggregate trace summary. + pub summary: TrieJoinTraceSummary, + /// Root variable-depth context, absent only for zero-variable traces. + pub root: Option, +} + +/// One replay node for a variable-depth domain intersection. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct TrieJoinTraceReplayNode { + /// Original trace step index. + pub step_index: usize, + /// Depth in the global variable order. + pub level: usize, + /// Variable intersected at this depth. + pub variable: BindingVar, + /// Values already bound before this depth. + pub bound_prefix: BindingRow, + /// Relation index numbers whose trie domains constrained this variable. + pub participating_relations: Box<[usize]>, + /// Domain length contributed by each participating relation. + pub relation_domain_lens: Box<[usize]>, + /// Values that survived the intersection at this context. + pub intersection: Box<[TermId]>, + /// Per-survivor continuation in traversal order. + pub branches: Box<[TrieJoinTraceReplayBranch]>, +} + +/// One survivor from a replay node's domain intersection. +#[derive(Clone, Debug, Eq, PartialEq)] +pub struct TrieJoinTraceReplayBranch { + /// Bound value for the node variable. + pub value: TermId, + /// Child context after binding `value`, or `None` at leaf depth. + pub child: Option>, +} + /// Shape error found while summarizing a trie-join trace. #[derive(Clone, Copy, Debug, Eq, PartialEq)] pub enum TrieJoinTraceShapeError { @@ -330,6 +369,28 @@ pub enum TrieJoinTraceShapeError { expected: usize, actual: usize, }, + /// A replay step appears at a different variable depth than traversal order expects. + ReplayLevelMismatch { + step: usize, + expected: usize, + actual: usize, + }, + /// A replay step is missing for a reachable bound prefix. + MissingReplayStep { + level: usize, + bound_prefix_len: usize, + }, + /// A locally valid step belongs to a different bound-prefix branch. + BoundPrefixValueMismatch { + step: usize, + position: usize, + expected: TermId, + actual: TermId, + }, + /// Steps remain after replaying every reachable branch. + TrailingReplayStep { step: usize }, + /// Leaf replay count disagrees with the trace candidate total. + CandidateBindingMismatch { expected: usize, actual: usize }, } /// One variable-depth domain intersection observed while tracing LFTJ traversal. @@ -466,6 +527,122 @@ impl TrieJoinTrace { Ok(summary) } + + /// Reconstructs the variable-prefix replay tree represented by this trace. + /// + /// `summarize` checks each step independently. This method additionally + /// checks that the steps form the preorder traversal that an LFTJ-style + /// cursor would replay: each survivor at a non-leaf depth must be followed + /// by exactly one child context whose bound prefix extends the parent. + pub fn replay_shape(&self) -> Result { + let summary = self.summarize()?; + + if self.variable_order.is_empty() { + if !self.steps.is_empty() { + return Err(TrieJoinTraceShapeError::TrailingReplayStep { step: 0 }); + } + if self.candidate_bindings != 1 { + return Err(TrieJoinTraceShapeError::CandidateBindingMismatch { + expected: self.candidate_bindings, + actual: 1, + }); + } + return Ok(TrieJoinTraceReplayShape { + summary, + root: None, + }); + } + + let mut step_index = 0; + let mut candidate_bindings = 0; + let root = self.replay_node(0, &[], &mut step_index, &mut candidate_bindings)?; + + if step_index != self.steps.len() { + return Err(TrieJoinTraceShapeError::TrailingReplayStep { step: step_index }); + } + if candidate_bindings != self.candidate_bindings { + return Err(TrieJoinTraceShapeError::CandidateBindingMismatch { + expected: self.candidate_bindings, + actual: candidate_bindings, + }); + } + + Ok(TrieJoinTraceReplayShape { + summary, + root: Some(root), + }) + } + + fn replay_node( + &self, + level: usize, + expected_prefix: &[TermId], + step_index: &mut usize, + candidate_bindings: &mut usize, + ) -> Result { + let current_step = *step_index; + let Some(step) = self.steps.get(current_step) else { + return Err(TrieJoinTraceShapeError::MissingReplayStep { + level, + bound_prefix_len: expected_prefix.len(), + }); + }; + + if step.level != level { + return Err(TrieJoinTraceShapeError::ReplayLevelMismatch { + step: current_step, + expected: level, + actual: step.level, + }); + } + + for (position, (&expected, &actual)) in expected_prefix + .iter() + .zip(step.bound_prefix.iter()) + .enumerate() + { + if expected != actual { + return Err(TrieJoinTraceShapeError::BoundPrefixValueMismatch { + step: current_step, + position, + expected, + actual, + }); + } + } + + *step_index += 1; + let leaf = level + 1 == self.variable_order.len(); + let mut branches = Vec::with_capacity(step.intersection.len()); + for &value in step.intersection.iter() { + let child = if leaf { + *candidate_bindings += 1; + None + } else { + let mut child_prefix = Vec::with_capacity(expected_prefix.len() + 1); + child_prefix.extend_from_slice(expected_prefix); + child_prefix.push(value); + Some(Box::new(self.replay_node( + level + 1, + &child_prefix, + step_index, + candidate_bindings, + )?)) + }; + branches.push(TrieJoinTraceReplayBranch { value, child }); + } + + Ok(TrieJoinTraceReplayNode { + step_index: current_step, + level: step.level, + variable: step.variable, + bound_prefix: step.bound_prefix.clone(), + participating_relations: step.participating_relations.clone(), + relation_domain_lens: step.relation_domain_lens.clone(), + intersection: step.intersection.clone(), + branches: branches.into_boxed_slice(), + }) + } } /// Minimal LFTJ-style cursor over one ordered variable domain. @@ -1285,6 +1462,30 @@ mod tests { && step.participating_relations.as_ref() == [1] && step.relation_domain_lens.as_ref() == [2] && step.intersection.as_ref() == [t(100), t(101)])); + + let replay = trace.replay_shape().unwrap(); + assert_eq!(replay.summary, trace.summarize().unwrap()); + let root = replay.root.as_ref().unwrap(); + assert_eq!(root.step_index, 0); + assert_eq!(root.variable, v(1)); + assert_eq!(root.intersection.as_ref(), [t(10)]); + assert_eq!(root.branches.len(), 1); + assert_eq!(root.branches[0].value, t(10)); + + let x_node = root.branches[0].child.as_ref().unwrap(); + assert_eq!(x_node.step_index, 1); + assert_eq!(x_node.variable, v(0)); + assert_eq!(x_node.bound_prefix.as_ref(), [t(10)]); + assert_eq!(x_node.intersection.as_ref(), [t(1), t(2)]); + assert_eq!(x_node.branches.len(), 2); + + for branch in x_node.branches.iter() { + let z_node = branch.child.as_ref().unwrap(); + assert_eq!(z_node.variable, v(2)); + assert_eq!(z_node.bound_prefix.as_ref(), [t(10), branch.value]); + assert_eq!(z_node.intersection.as_ref(), [t(100), t(101)]); + assert!(z_node.branches.iter().all(|leaf| leaf.child.is_none())); + } } #[test] @@ -1306,6 +1507,45 @@ mod tests { ); } + #[test] + fn trie_join_trace_replay_rejects_missing_child_context() { + let left = relation(&[0, 1], &[&[1, 10], &[2, 10]]); + let right = relation(&[1, 2], &[&[10, 100], &[10, 101]]); + let variable_order = [v(1), v(0), v(2)]; + let mut trace = trie_join_trace(&[left, right], &variable_order).unwrap(); + + trace.steps = trace.steps[..trace.steps.len() - 1] + .to_vec() + .into_boxed_slice(); + + assert_eq!( + trace.replay_shape().unwrap_err(), + TrieJoinTraceShapeError::MissingReplayStep { + level: 2, + bound_prefix_len: 2, + } + ); + } + + #[test] + fn trie_join_trace_replay_rejects_wrong_bound_prefix_branch() { + let left = relation(&[0, 1], &[&[1, 10], &[2, 10]]); + let right = relation(&[1, 2], &[&[10, 100], &[10, 101]]); + let variable_order = [v(1), v(0), v(2)]; + let mut trace = trie_join_trace(&[left, right], &variable_order).unwrap(); + trace.steps[2].bound_prefix[1] = t(2); + + assert_eq!( + trace.replay_shape().unwrap_err(), + TrieJoinTraceShapeError::BoundPrefixValueMismatch { + step: 2, + position: 1, + expected: t(1), + actual: t(2), + } + ); + } + #[test] fn cursor_leapfrog_intersection_uses_monotone_seek_contract() { let left = [t(1), t(3), t(5), t(8)];