…tion should consist of just writing "register_width = 64" in Arith/DettmanMultiplcation. something broke.

…s it originally was.

function did rather unreasonable things when the limbwidth was fractional.

In this commit, I tried to fix this issue, but I ended up making the
reduce_carry_borrow function pretty obnoxious.  Also, fixing this issue
requires somewhat strange (and strong) hypotheses on the weight function.
We'd want, for instance,

(weight (2 * limbs - 2) / weight (limbs - 2)) mod s = 0.

I plan to revert my changes (from this commit) to the reduce_carry_borrow
function, so that it will continue to do unreasonable things given fractional
limbwidths.  This was not worth it.

… change anything

…tation. wrote some (messy) arithmetic proofs. still more proofs to go in Arithmetic/DettmanMultiplication.v. Then need to change PushButtonSynthesis appropriately.

…s to Arithmetic/DettmanMultiplication.v

Replaced a bunch of references to (Z.log2_up s) with (Z.log2 s), since (in
the dettman_multiplication_mod_ops module) we now stipulate that s is a power
of 2.

…iminated the unnecessary 64-bit mask, but it also caused weird stuff to happen and killed off a bunch of 52-bit masks. Where'd they go? idk.

… own pass now.

It now comes later in the rewriting process.
Apparently it's important that it comes after the fancy stuff.
For reasons that I don't understand, proofs in Barrett256 and Montgomery256 break if
I put it before.

In this commit, I just removed the bit about dead code elimination that I
added in BoundsPipeline.v.
The C code synthesizes without error now, at least.
I haven't built everything yet, so we'll see if things actually work nicely.

by removing the dead-code-elimination thing]