fix sbb subtracting 2^64

[andres-erbsen]

UInt64.toInt returns a non-negative number
BitVec.toInt returns may return a negative number
BitVec.toNat returns a Nat which has saturating subtraction

Let's stick with the Rocq convention of .unsigned and .signed for fixed-width variables, both returning Int

h/t @miriampolzer for asking me about this code

[protz]

Saturating Nat subtraction always trips us, so I'm in support of this. What's up with take vs truncate?

[andres-erbsen]

They're the same function, just take doesn't make me go and look up which end is being truncated. I can put truncate back if you prefer it, or we could do something like truncLsb.

[protz]

I like the consistency. Good for me 👍