`Value::prune` corrupts sum tag bits when prepending Left (0) tag

[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

[roconnor-blockstream]

Yeah, the assumption that unused bits in the array backing are always 0 does seem to be faulty. In particular to_value() will clone a value by copying the entire inner array backing, which can have other unused bits set or not set.

I'm no Rust expert, but I'd be inclined to write that whole bit_offset > 0 branch to refactor common code:

    let new_bit_offset = bit_offset - 1;
    let byte_idx = new_bit_offset / 8;
    let mut bx: Box<[u8]> = inner.as_ref().into();
    let bit_mask = 1 << (7 - new_bit_offset % 8);
    if new_bit {
        bx[byte_idx] |= bit_mask;
    } else {
        bx[byte_idx] &= !bit_mask;
    }
    (bx.into(), new_bit_offset)

[topologoanatom]

Another possible fix is to ensure proper cleanup of offset bits higher up in the call tree. The right_shift_1() function is used only in the left() and right() functions, which in turn depend on product(). One approach is to clean the offset bits in product(), for example:

fn product(
    left: Option<(&Arc<[u8]>, usize)>,
    left_bit_length: usize,
    right: Option<(&Arc<[u8]>, usize)>,
    right_bit_length: usize,
) -> (Arc<[u8]>, usize) {
    if left_bit_length == 0 {
        if let Some((right, right_bit_offset)) = right {
            (Arc::clone(right), right_bit_offset) // may contain garbage bits
        } else if right_bit_length == 0 {
            (Arc::new([]), 0)
        } else {
            (Arc::from(vec![0; right_bit_length.div_ceil(8)]), 0)
        }
    ...

A second approach, as @roconnor-blockstream mentioned, is to clean the offset bits in the to_value() function. Both approaches fix the issue described in #333, but I think cleaning them in product() is more correct from a design standpoint.

Here is code for both solutions https://gist.github.com/topologoanatom/5cf8551918d9d0fd5c7788e90e65aecd

[apoelstra]

So, there's actually a general problem here which is that when we parse a value from the bit machine using from_padded_bits we capture the padding bits verbatim and store them, and then we treat them as normative. Every other constructor zeros them out (or rather, never gives the user an opportunity to provide "padding bits" at all).

So there are two problems:

• In some cases we assume they're zero, leading to this original bug.
• Even if we don't assume they're zero, we use them in the derived impls of PartialEq, Hash, Debug, etc

The current value.rs was written in #266 and #269. Curiously in the commit message for 09cdded I mention the Eq issue but don't seem to consider it a bug (I also say that it was "already the case" that the user could add padding which would cause equality-checks to fail, but this isn't really true -- before #266 we used a recursive Rust type for Value which had no room for padding. See 7cb40f5 which made this change.)

The way I see it, we have a few ways forward:

• Zero out the padding in from_padded_bits and have an internal invariant that padding bits are always zero. This will definitely kill this class of bug, at the cost of losing the original padding bits (but did these ever matter? I don't think so)
• Attempt to correct for padding in PartialEq, Display, prune and every other method. This seems like it'd be slower than the above solution and also like it'd be hard to do a complete job of it.
• Internally use the compact encoding rather than the padded encoding. I suspect this will greatly complicate our constructors and not be any faster than the first solution.

So my proposal is to change from_padded_bits to iterate through the type to identify padding bits and set these to zero on construction. We will need to be careful about 0-width types which have enormous representations.

[topologoanatom]

So, there's actually a general problem here which is that when we parse a value from the bit machine using from_padded_bits we capture the padding bits verbatim and store them, and then we treat them as normative. Every other constructor zeros them out (or rather, never gives the user an opportunity to provide "padding bits" at all).

So there are two problems:

• In some cases we assume they're zero, leading to this original bug.
• Even if we don't assume they're zero, we use them in the derived impls of PartialEq, Hash, Debug, etc

The current value.rs was written in #266 and #269. Curiously in the commit message for 09cdded I mention the Eq issue but don't seem to consider it a bug (I also say that it was "already the case" that the user could add padding which would cause equality-checks to fail, but this isn't really true -- before #266 we used a recursive Rust type for Value which had no room for padding. See 7cb40f5 which made this change.)

The way I see it, we have a few ways forward:

• Zero out the padding in from_padded_bits and have an internal invariant that padding bits are always zero. This will definitely kill this class of bug, at the cost of losing the original padding bits (but did these ever matter? I don't think so)
• Attempt to correct for padding in PartialEq, Display, prune and every other method. This seems like it'd be slower than the above solution and also like it'd be hard to do a complete job of it.
• Internally use the compact encoding rather than the padded encoding. I suspect this will greatly complicate our constructors and not be any faster than the first solution.

So my proposal is to change from_padded_bits to iterate through the type to identify padding bits and set these to zero on construction. We will need to be careful about 0-width types which have enormous representations.

I'm working on implementing the padding bit zeroing in from_padded_bits as you suggested. I want to clarify your vision for the type-iteration approach since I've encountered an ambiguity with Sum types.

When we have Sum(Left, Right) where left.bit_width != right.bit_width, the smaller variant will have trailing padding in the shared space.

When iterating through the type alone (without inspecting the tag bit value), we cannot determine whether tail bits are padding or data.

Did you intend to:

• Only zero bits that are provably padding in all possible variants, accepting that some padding remains non-zero?
• Read the tag bit during iteration to determine which variant is active, then zero the inactive variant's space?

Something else I'm missing?

[apoelstra]

When iterating through the type alone (without inspecting the tag bit value), we cannot determine whether tail bits are padding or data.

I think we have to iterate through the provided bitstream and the type simultaneously, so that we have access to the tag bit value and can determine what's padding and what's not. (It might be that we have to the existing "copy all the bits" parser and then do a second pass afterward.)

I asked Claude to write this code and what it produced was annoyingly long so I didn't review it, hoping that a human could produce something smaller and more elegant...but it might not be possible. It's an annoyingly complicated thing to do.

[topologoanatom]

When iterating through the type alone (without inspecting the tag bit value), we cannot determine whether tail bits are padding or data.

I think we have to iterate through the provided bitstream and the type simultaneously, so that we have access to the tag bit value and can determine what's padding and what's not. (It might be that we have to the existing "copy all the bits" parser and then do a second pass afterward.)

I asked Claude to write this code and what it produced was annoyingly long so I didn't review it, hoping that a human could produce something smaller and more elegant...but it might not be possible. It's an annoyingly complicated thing to do.

Thanks, that clears up my confusion

[topologoanatom]

When iterating through the type alone (without inspecting the tag bit value), we cannot determine whether tail bits are padding or data.

I think we have to iterate through the provided bitstream and the type simultaneously, so that we have access to the tag bit value and can determine what's padding and what's not. (It might be that we have to the existing "copy all the bits" parser and then do a second pass afterward.)

I asked Claude to write this code and what it produced was annoyingly long so I didn't review it, hoping that a human could produce something smaller and more elegant...but it might not be possible. It's an annoyingly complicated thing to do.

I tried implementing zeroing logic for from_padded_bits (latest commits on PR branch). It passes regression tests, but fuzz found inputs where pruning fails; the same goes for the original HL script.

This problem disappears when combining both padding cleanup in from_padded_bits with in product cleanup (the original PR changes). I reckon from_padded_bits is not the only source of stale bits.

[apoelstra]

Hmm. I suppose it could be that the pruning itself causes previously non-stale bits to become stale (and then these stale bits to become "non-stale" again, incorrectly).

fuzz found inputs where pruning fails; the same goes for the original HL script.

What does this fuzz test do? What does "pruning fails" mean?

Maybe the correct solution is to change the internal representation to use the compact encoding (and then change the sum/product constructors to copy bits). Maybe my Arc<[u8]> bit-reuse shenanigans were too clever to work..

[topologoanatom]

What does this fuzz test do? What does "pruning fails" mean?

I meant the prune_value fuzz test that you added recently along with the regression tests.

[apoelstra]

Ah, right, I had forgotten that I'd pushed that. Ok, frustrating.

After thinking about this some more, I think we need to overhaul Value to internally store the compact encoding rather than the padded encoding. I think my choice in #266 to use the padded encoding was a mistake (even though it makes use on the bit machine super fast since we can just copy bits with no re-encoding).

[KyrylR]

Same problem was in sphincs_main.simf, but this time the tracker was the reason for the bug.

You can use this command to reproduce the bug:

cargo run -p cli -- basic transfer-native \
  --broadcast \
  --utxo 5f7f7dfbc5961285a092ad8d7059ab57b5e8b72205995917c35ac26ebe3788d7:0 \
  --to-address tex1p9sv7g8tyljjymz4t6zyjpvepw44f9wfjxskvyjlczqjdw7rrykqsl9hwe7 \
  --send-sats 1234 \
  --fee-sats 4200

After long debugging session, AI summary:

• Tracker input bits were sampled from frame start.
• Runtime Case/Assert branch bits are sampled from frame cursor (peek_bit).
• When cursor != start, pruning decisions can be wrong.

Fixes:

// old tracker input construction
let read_iter = input_frame.map(|frame| frame.as_bit_iter(&self.data));

// runtime branch sampling
let choice_bit = in_frame.peek_bit(&self.data); // uses cursor

Minimal fix:

// frame.rs
pub(super) fn as_bit_iter_from_cursor<'a>(&self, data: &'a [u8]) -> BitIter<_> {
    BitIter::byte_slice_window(data, self.cursor, self.start + self.len)
}

// mod.rs
let read_iter = input_frame
    .map(|frame| frame.as_bit_iter_from_cursor(&self.data))
    .unwrap_or(crate::BitIter::from([].iter().copied()));

So , tracker start/cursor mismatch was sufficient to cause ReachedPrunedBranch (the tracker cursor alignment problem).

I also applied the fix in frame clearing (bit-precise zeroing for non-byte-aligned frame regions) that was discussion above

Links:
https://github.com/BlockstreamResearch/rust-simplicity/blob/master/src/bit_machine/frame.rs#L132
https://github.com/BlockstreamResearch/rust-simplicity/blob/master/src/bit_machine/mod.rs#L794
https://github.com/BlockstreamResearch/rust-simplicity/blob/master/src/bit_machine/mod.rs#L555
https://github.com/BlockstreamResearch/rust-simplicity/blob/master/src/node/redeem.rs#L379

Final transaction: https://liquid.network/testnet/tx/950ed8da73eb963fd82b79a82b83a1c3ae857d870d776a2b6438bcd69313bffa

[KyrylR]

Fix in simplicity contracts (added patch): BlockstreamResearch/simplicity-contracts@b0d377a

Also all changes to the rust-simplicity: https://github.com/KyrylR/rust-simplicity/tree/prune-bug-fix

     Running `target/debug/simplicity-cli basic transfer-native --broadcast --utxo '0481428bab32d6298b9ed01bff7d29a4fe1ff600fff7addfcfd5a2d289868e59:0' --to-address tex1p9sv7g8tyljjymz4t6zyjpvepw44f9wfjxskvyjlczqjdw7rrykqsl9hwe7 --send-sats 1234 --fee-sats 4200`
[crates/cli/src/commands/basic.rs:191:17] get_sphincs_main_address(&x_only_public_key, NETWORK)? = tex1pmlut89y22mcla602f7dgwuljkdhd5up2aax9szcrqa6pgt4a4ngqgxu7pm
Broadcasted txid: dc6e943efa6be7b2154ffcddc722ae73b78256d7d967aa3901d0df06dab210b4

Successful tx: https://liquid.network/testnet/tx/dc6e943efa6be7b2154ffcddc722ae73b78256d7d967aa3901d0df06dab210b4