Summary
Two families of helper routines violate stack-discipline invariants at their parameter boundaries:
-
lshift_prevent_overflow(bits = 0)
Assumes its limb shifters populate the altstack with $N_\text{LIMBS}-1$ intermediates, then unconditionally executes
for _ in 1..Self::N_LIMBS {
OP_FROMALTSTACK
}
When bits = 0, neither limb_lshift_without_carry(0) nor limb_lshift_with_carry(0) ever perform an OP_TOALTSTACK, leaving the altstack empty.
The result is an immediate underflow or silent stack-shape corruption when those pops execute.
Expected behavior: shifting by 0 should be a semantic no-op that leaves both primary and altstack states unchanged.
-
*_to_*_bits_toaltstack (bit-extraction helpers)
The little-endian variant under-pushes for num_bits ≤ 1 (no OP_TOALTSTACK executed when num_bits = 1), while the big-endian variant still pushes even when num_bits = 0.
Both violate the contract “push exactly num_bits bits to altstack,” producing asymmetric over- or underflows when callers symmetrically pop num_bits items.
Expected behavior: for any num_bits ≥ 0, push precisely num_bits bits and restore an empty altstack on return.
Collectively, these boundary errors break stack-shape consistency guarantees and can lead to latent faults in composed arithmetic macros relying on strict altstack balancing.
Acknowledgements: This issue was identified using Pomelo (https://eprint.iacr.org/2024/1768) by the UCSB/Nubit team. We also acknowledge [BitVM #360](BitVM/BitVM#360) for first flagging potential problems in the limb_to_le_bits* family.
Summary
Two families of helper routines violate stack-discipline invariants at their parameter boundaries:
lshift_prevent_overflow(bits = 0)Assumes its limb shifters populate the
altstackwithWhen
bits = 0, neitherlimb_lshift_without_carry(0)norlimb_lshift_with_carry(0)ever perform anOP_TOALTSTACK, leaving thealtstackempty.The result is an immediate underflow or silent stack-shape corruption when those pops execute.
Expected behavior: shifting by 0 should be a semantic no-op that leaves both primary and
altstackstates unchanged.*_to_*_bits_toaltstack(bit-extraction helpers)The little-endian variant under-pushes for
num_bits ≤ 1(noOP_TOALTSTACKexecuted whennum_bits = 1), while the big-endian variant still pushes even whennum_bits = 0.Both violate the contract “push exactly
num_bitsbits toaltstack,” producing asymmetric over- or underflows when callers symmetrically popnum_bitsitems.Expected behavior: for any
num_bits ≥ 0, push preciselynum_bitsbits and restore an emptyaltstackon return.Collectively, these boundary errors break stack-shape consistency guarantees and can lead to latent faults in composed arithmetic macros relying on strict
altstackbalancing.Acknowledgements: This issue was identified using Pomelo (https://eprint.iacr.org/2024/1768) by the UCSB/Nubit team. We also acknowledge [BitVM #360](BitVM/BitVM#360) for first flagging potential problems in the
limb_to_le_bits*family.