Skip to content

Value::prune corrupts sum tag bits when prepending Left (0) tagΒ #337

@KyrylR

Description

@KyrylR

With a help of Claude and insight from @topologoanatom and @gerau, here what I have found and tested:

When Value::prune creates a Left value by calling Value::left(), the resulting value can have corrupted tag bits. This causes ReachedPrunedBranch errors during execution when the BitMachine reads the wrong branch selector.

In src/value.rs, the right_shift_1 function has an optimization bug. When prepending a 0 bit (for Left values) and bit_offset > 0, it simply decrements the bit_offset without clearing the existing bit:

} else {
    // ...and if we are inserting a 0 we don't even need to allocate a new [u8]
    (Arc::clone(inner), bit_offset - 1)
}

The bug is triggered when:

  1. A witness value like Left(Right(data)) is pruned to a smaller type
  2. The pruning creates nested Left/Right wrappers via Value::left() and Value::right()
  3. The inner value's bit representation has a 1 at the position where the outer 0 tag should be inserted

This happened in the #333, where the program was with complex sum types that have multiple execution paths, where pruning converts Case nodes to AssertL/AssertR.

Possible fix

Check if the bit at new_bit_offset is already 0 before skipping allocation. If it's 1, allocate and clear it:

} else {
    let new_bit_offset = bit_offset - 1;
    let byte_idx = new_bit_offset / 8;
    let bit_mask = 1 << (7 - new_bit_offset % 8);
    if (inner[byte_idx] & bit_mask) == 0 {
        // The bit is already 0, no need to allocate
        (Arc::clone(inner), new_bit_offset)
    } else {
        // The bit is 1, we need to clear it to insert a 0
        let mut bx: Box<[u8]> = inner.as_ref().into();
        bx[byte_idx] &= !bit_mask;
        (bx.into(), new_bit_offset)
    }
}

With the fix above the bug described in the #333 does not happen

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions