Feat/MULH opcode

[bgillesp]

Implement MULH opcode

Circuit is validated by the following strategy:

1. Compute the signed values associated with rs1, rs2 and rd registers
2. Verify that the product of signed inputs rs1 and rs2 is equal to the result of interpreting rd as the high limb of a 2s complement value with some 32-bit low limb.

The latter value in step 2 is expressed as: the 32-bit signed 2s complement value of the rd register times 2^32, plus the unsigned value of the 32-bit low limb.

The soundness here is a bit subtle. The signed values of 32-bit inputs rs1 and rs2 have values between -2^31 and 2^31 - 1, so their product is constrained to lie between -2^62 + 2^31 and 2^62. In a prime field of size smaller than 2^64, the range of values represented by a 64-bit 2s complement value, integers between -2^63 and 2^63 - 1, have some ambiguity. If p = 2^64 - k, then the values between -2^63 and -2^63 + k - 1 correspond with the values between 2^63 - k and 2^63 - 1.

However, as long as the values required by signed products don't overlap with this ambiguous range, an arbitrary 64-bit 2s complement value can represent a signed 32-bit product in only one way, so there is no ambiguity in the representation. This is the case for the Goldilocks field with order p = 2^64 - 2^32 + 1.

[bgillesp]

The circuit design has been updated from the initial description above; see the doc comment of the MULH circuit constructor for an overview and analysis. This could use a careful look from reviewers, as the design is a bit subtle and relies on the size of the Goldilocks field for correctness.

[matthiasgoergens]

@bgillesp Did you / could you update the PR description to reflect the updated circuit design? Thanks!

[matthiasgoergens]

You can use IsLtConfig::constrain_last_limb from #506 to make this a bit easier to read.

[bgillesp]

See my comment in #506 about making it a separate gadget MSBConfig rather than an extra constructor variant of IsLtConfig, but whatever design we decide I can definitely use it here. Will make the change once #506 is merged with master.

[naure]

Thanks for the documentation of the constraints too!

It helped me to double-check numerically:

# Range of variables:
u32max = 2**32 - 1
pos = 2**31 - 1
neg = -2**31
p = 2**64 - 2**32 + 1 # Goldilocks.

# Range of the constraint:
#          rs1 * rs2 - (rd * 2**32 + low)
greatest = neg * neg - (neg * 2**32 + 0)
smallest = neg * pos - (pos * 2**32 + u32max)
assert -p < smallest < 0 < greatest < p

• The range contains a single instance of 0 mod p so the constraint works the same as in ℤ.
• The constraint is directly a hi/lo decomposition of the product.

[naure]

Beautiful!