Feat/MULHSU opcode

[bgillesp]

Implements the MULHSU opcode using a circuit design similar to that used by MULH:

1. Map signed and unsigned inputs as corresponding field elements
2. Compute the product of the inputs, and verify that rd can be used as the upper limb for a 64-bit 2s complement signed value equal to this product.

A small complication comes up in this design because of the ambiguity of the representation of a small number of 64-bit signed values as Goldilocks field elements. While this ambiguity did not have an impact on the signed/signed products for the MULH opcode, here the interval of signed/unsigned product values does overlap the ambiguous interval of 64-bit 2s complement values. This is mitigated by explicitly constraining the value of the rd register to be not equal to its maximal signed value (2^31 - 1) by witnessing the inverse of (2^31 - 1) - rd. This makes all remaining valid 64-bit values unambiguously represented, and also still permits representation of all valid signed/unsigned product values. See the module doc comment for mulh.rs for a more complete soundness analysis. (Some extra eyes on this analysis during the review would probably be a good idea, as the details are quite sensitive to the ranges of values and the size of the Goldilocks field.)

This PR additionally refactors the existing MULHU opcode to use an analogous circuit design to this, also requiring a one-element restriction on the value of rd to ensure soundness. This implementation avoids the overhead of using UInt::mul to compute the product explicitly in u16 limbs, which requires additional carry witnesses with range constraints, and should reduce the total number of WitIns needed for the circuit fairly substantially.

[naure]

Thanks for the insightful documentation again.