Skip to content

fix(bitmachine): fix frame data offsets send to tracker (fixes Execution reached a pruned branch)#362

Open
stringhandler wants to merge 1 commit intoBlockstreamResearch:masterfrom
stringhandler:fix/frame-fix-2
Open

fix(bitmachine): fix frame data offsets send to tracker (fixes Execution reached a pruned branch)#362
stringhandler wants to merge 1 commit intoBlockstreamResearch:masterfrom
stringhandler:fix/frame-fix-2

Conversation

@stringhandler
Copy link
Copy Markdown
Contributor

Fixes some bugs where the data sent from the bitmachine to trackers would not start at the current cursor, resulting in some random junk being seen by the tracker. This doesn't have an effect on full programs, but when pruning this seems to generate an incorrect pruning, as seen in #337.

The following code now prunes and runs correctly:

fn add(elt: u32, acc: u32) -> u32 {
    let (_, sum): (bool, u32) = jet::add_32(elt, acc);
    sum
}

fn main() {
    let list: List<u32, 4> = list![5];
    let result: u32 = fold::<add, 4>(list, 0);
    assert!(jet::eq_32(result, 5));
}

Whereas previously it would fail on Execution failed: Execution reached a pruned branch: fd6503b9fd020b8d4ed75deb14cc05bbcb91da392ba4b675f2b2345dabb1cde5

Some excerpts from StderrTracker:

// Before fix
[  45] exec iden 2^32 → 2^32
       input 0x00000002
       output 0x00000005
       
// After fix
   [  45] exec iden 2^32 → 2^32
       input 0x00000005
       output 0x00000005

/// Before fix
[  46] exec iden (2^64? × 2^32?) × 1 → (2^64? × 2^32?) × 1
       input ((L(ε),R(0x00000005)),ε)
       output ((L(ε),L(ε)),ε)
       
// After fix
[  46] exec iden (2 × 2^32?) × 1 → (2 × 2^32?) × 1
       input ((0b0,R(0x00000005)),ε)
       output ((0b0,R(0x00000005)),ε)

I haven't tried it on @KyrylR 's specific SHRINCS test on that issue.

NOTE: I have based this off an older commit so I could test it with SimplicityHL, which doesn't compile with the latest rust-simplicity

NOTE: the unit test is written by Claude (Happy to remove it if needed)

…ker 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.
@apoelstra
Copy link
Copy Markdown
Collaborator

apoelstra commented May 6, 2026

In a4cbd56:

Let's just delete as_bit_iter. In the one place it's still called it's right after out_frame.reset_cursor() so it's equivalent to the new as_bit_iter_from_cursor.

Comment thread src/bit_machine/mod.rs
// The read frame cursor is where the node's input begins.
// The write frame cursor is where the node's output begins.
let input_frame = self.read.last().map(Frame::shallow_copy);
let output_frame = self.write.last().map(Frame::shallow_copy);
Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In a4cbd56:

I think this new output_frame binding is unnecessary, but I like having it, because it borrows self.write for almost the entire interpreter function, guaranteeing that nothing in there modifies self.write.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants