@@ -1267,6 +1267,117 @@ mod tests {
12671267 let new_v = Value :: from_padded_bits ( & mut iter, & v. ty ) . unwrap ( ) ;
12681268 assert_eq ! ( v, new_v) ;
12691269 }
1270+
1271+ // --- Bug regression tests for right_shift_1 when new_bit=false ---
1272+ //
1273+ // right_shift_1(inner, bit_offset > 0, new_bit=false) is supposed to insert
1274+ // a 0 (Left tag) at position bit_offset-1 by decrementing bit_offset. The bug
1275+ // is that it clones the Arc without clearing that position, so any pre-existing
1276+ // 1-bit at bit_offset-1 corrupts the Left tag, causing the value to read as
1277+ // Right instead of Left.
1278+ //
1279+ // The dirty bit originates from product sub-value extraction: as_product()
1280+ // returns ValueRef children that share the parent buffer. The right child has
1281+ // bit_offset = parent.bit_offset + left_bit_width, so every 1-bit encoded by
1282+ // the left component sits "before" the right child's logical start. When that
1283+ // right child is later wrapped in Left, right_shift_1 may see a stale 1-bit.
1284+
1285+ /// Simplest direct construction: extract the right sub-value of a product
1286+ /// whose left component has 1-bits, then wrap the sub-value in Left.
1287+ ///
1288+ /// `product(Right(u1(1)), Right(u1(0)))` encodes as [0xE0] at bit_offset=0:
1289+ /// bits 0..=1 = Right(u1(1)) = 1, 1 ← left component
1290+ /// bits 2..=3 = Right(u1(0)) = 1, 0 ← right component (bit_offset=2)
1291+ ///
1292+ /// Wrapping the right sub-value (bit_offset=2 in [0xE0]) in Left calls
1293+ /// right_shift_1(false) which should clear bit 1. The bug leaves bit 1 = 1,
1294+ /// so the result reads as Right instead of Left.
1295+ #[ test]
1296+ fn left_tag_not_corrupted_by_dirty_buffer ( ) {
1297+ let product_val = Value :: product (
1298+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 1 ) ) , // encodes bits 0,1 as 1,1
1299+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 0 ) ) , // starts at bit_offset=2
1300+ ) ;
1301+
1302+ let ( _, right_sub) = product_val. as_product ( ) . unwrap ( ) ;
1303+ // right_sub shares [0xE0]; bit at position 1 (before its start) is 1.
1304+ let right_sub_owned = right_sub. to_value ( ) ;
1305+
1306+ let left_val = Value :: left ( right_sub_owned, Final :: unit ( ) ) ;
1307+
1308+ assert ! (
1309+ left_val. as_left( ) . is_some( ) ,
1310+ "BUG: Left tag corrupted — right_shift_1(false) did not clear dirty bit; \
1311+ value reads as Right instead of Left"
1312+ ) ;
1313+ assert ! (
1314+ left_val. as_right( ) . is_none( ) ,
1315+ "BUG: Left tag corrupted — as_right() should return None for a Left value"
1316+ ) ;
1317+ }
1318+
1319+ /// Verify the dirty-buffer bug at the bit level: the first padded bit of a
1320+ /// Left value must always be 0 (the Left discriminant).
1321+ #[ test]
1322+ fn left_tag_first_padded_bit_is_zero ( ) {
1323+ let product_val = Value :: product (
1324+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 1 ) ) ,
1325+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 0 ) ) ,
1326+ ) ;
1327+
1328+ let ( _, right_sub) = product_val. as_product ( ) . unwrap ( ) ;
1329+ let left_val = Value :: left ( right_sub. to_value ( ) , Final :: unit ( ) ) ;
1330+
1331+ let first_bit = left_val. iter_padded ( ) . next ( ) ;
1332+ assert_eq ! (
1333+ first_bit,
1334+ Some ( false ) ,
1335+ "BUG: first padded bit of Left value is {:?}, expected Some(false)" ,
1336+ first_bit
1337+ ) ;
1338+ }
1339+
1340+ /// End-to-end via prune: pruning can extract a sub-value via to_value() that
1341+ /// shares the parent buffer and has 1-bits before its logical start. When
1342+ /// prune then calls Value::left() on it (Task::MakeLeft), the bug corrupts
1343+ /// the Left tag.
1344+ ///
1345+ /// Original: Left(product(Right(u1(1)), Right(u1(0))))
1346+ /// type: ((u1+u1) * (u1+u1)) + unit
1347+ ///
1348+ /// Pruned to: (unit * (u1+u1)) + unit
1349+ ///
1350+ /// The right component of the inner product keeps its type (u1+u1) unchanged,
1351+ /// so prune returns it via to_value() — sharing the same dirty buffer.
1352+ /// MakeLeft then wraps it, triggering the bug.
1353+ #[ test]
1354+ fn prune_does_not_corrupt_left_tag_via_shared_buffer ( ) {
1355+ let original = Value :: left (
1356+ Value :: product (
1357+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 1 ) ) ,
1358+ Value :: right ( Final :: u1 ( ) , Value :: u1 ( 0 ) ) ,
1359+ ) ,
1360+ Final :: unit ( ) ,
1361+ ) ;
1362+
1363+ // Shrink the left component: (u1+u1)*(u1+u1) → unit*(u1+u1).
1364+ // The right sub-value of the product keeps type u1+u1 (matches exactly),
1365+ // so prune returns it via to_value() with the dirty shared buffer intact.
1366+ let pruned_ty = Final :: sum (
1367+ Final :: product ( Final :: unit ( ) , Final :: sum ( Final :: u1 ( ) , Final :: u1 ( ) ) ) ,
1368+ Final :: unit ( ) ,
1369+ ) ;
1370+
1371+ let pruned = original
1372+ . prune ( & pruned_ty)
1373+ . expect ( "prune returned None; the target type is compatible" ) ;
1374+
1375+ assert ! (
1376+ pruned. as_left( ) . is_some( ) ,
1377+ "BUG: prune corrupted the Left tag — right_shift_1(false) did not clear \
1378+ a dirty bit from the shared product buffer; value reads as Right"
1379+ ) ;
1380+ }
12701381}
12711382
12721383#[ cfg( bench) ]
0 commit comments