Skip to content

Commit c32c9e2

Browse files
committed
fix(bit_machine): use cursor position instead of frame start for tracker read iterator
The tracker was receiving a bit iterator anchored at the frame's start rather than the current cursor position. When a `case` node executes inside another `case` or `drop`, the read frame cursor has already advanced past the start, so the tracker read stale bits and recorded the wrong branch. This caused `assertl`/`assertr` pruning to remove the wrong branch after execution. Adds a regression test covering the specific `comp (pair (injl (injr unit)) unit) (case (case unit unit) unit)` pattern that triggered the bug.
1 parent a86927e commit c32c9e2

2 files changed

Lines changed: 40 additions & 1 deletion

File tree

src/bit_machine/frame.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,14 @@ impl Frame {
123123
) -> BitIter<core::iter::Copied<core::slice::Iter<'a, u8>>> {
124124
BitIter::byte_slice_window(data, self.start, self.start + self.len)
125125
}
126+
127+
/// Like [`as_bit_iter`] but starts from the current cursor position rather than the frame start.
128+
pub(super) fn as_bit_iter_from_cursor<'a>(
129+
&self,
130+
data: &'a [u8],
131+
) -> BitIter<core::iter::Copied<core::slice::Iter<'a, u8>>> {
132+
BitIter::byte_slice_window(data, self.cursor, self.start + self.len)
133+
}
126134
}
127135

128136
fn get_indices(cursor: usize) -> (usize, usize) {

src/bit_machine/mod.rs

Lines changed: 32 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -386,7 +386,7 @@ impl BitMachine {
386386
// describes the Bit Machine "input" to the current node,
387387
// no matter the node.
388388
let read_iter = input_frame
389-
.map(|frame| frame.as_bit_iter(&self.data))
389+
.map(|frame| frame.as_bit_iter_from_cursor(&self.data))
390390
.unwrap_or(crate::BitIter::from([].iter().copied()));
391391
// See the docs on `tracker::NodeOutput` for more information about
392392
// this match.
@@ -658,6 +658,37 @@ mod tests {
658658
.exec(&prog, &env)
659659
}
660660

661+
#[test]
662+
#[cfg(feature = "human_encoding")]
663+
fn set_tracker_cursor_regression() {
664+
// When a `case` node executes inside another `case` or `drop`, the read frame cursor
665+
// is no longer at the frame's start. Before this fix, `exec_with_tracker` passed an
666+
// iterator starting at frame.start to the tracker, so `SetTracker` read the wrong bit
667+
// and recorded the wrong branch, leading to an assertl/assertr mismatch after pruning.
668+
//
669+
// Program: comp (pair (injl (injr unit)) unit) (case (case unit unit) unit)
670+
// Intermediate frame bits: [0=L-tag of outer, 1=R-tag of inner]
671+
// Outer case: peek bit 0 = 0 (LEFT), fwd(1), cursor moves to bit 1.
672+
// Inner case: should read bit 1 = 1 (RIGHT).
673+
// Bug: tracker received iterator from bit 0, read 0 (LEFT) → pruned wrong branch.
674+
use crate::human_encoding::Forest;
675+
use crate::types;
676+
use std::collections::HashMap;
677+
678+
types::Context::with_context(|ctx| {
679+
let s = "main := comp (pair (injl (injr unit)) unit) (case (case unit unit) unit)";
680+
let program = Forest::<crate::jet::Core>::parse(s)
681+
.expect("parse")
682+
.to_witness_node(&ctx, &HashMap::new())
683+
.expect("main root")
684+
.finalize_pruned(&CoreEnv::new())
685+
.expect("finalize and prune");
686+
let mut mac = BitMachine::for_program(&program).expect("for_program");
687+
mac.exec(&program, &CoreEnv::new())
688+
.expect("pruned execution should succeed");
689+
});
690+
}
691+
661692
#[test]
662693
#[cfg(feature = "elements")]
663694
fn crash_regression1() {

0 commit comments

Comments
 (0)