Function simt_sequential_fma_to_bounded 

pub fn simt_sequential_fma_to_bounded(width: u32) -> BoundedExpr

The BoundedExpr of the SEQUENTIAL shift-add multiply a·x, UNROLLED over width bits, for single-lane inputs a = in0, x = in1. This is the exact combinational image of the SequentialFma FSM’s width-step recurrence: acc += (x[i] ? a<<i : 0) for i in 0..width. Our own certified SAT proves this shift-add equals the hardware a*x for ALL inputs — so the strategy switch is FREE (no divergence). b and the predicate are the same tail the other strategies share, already certified by gpu_kernel_is_certified_equal_to_the_vm_element_op / gpu_predication_is_certified.