Constraints related to multiplication instructions in 32 bit RiscV M extension

[vivekvpandya]

OPCODE	SEMANTICS	RESULT
MUL	unsigned * unsigned	low 32 bits
MULHU	unsigned * unsigned	high 32 bits
MULH	signed * signed	high 32 bits
MULHSU	signed * unsigned	high 32 bits

Check appendix A for maximum and minimum values in various possible configurations and those fits well with Goldilock Field.

Constraints for MUL and MULHU

Basic constraints:
multiplicand * multiplier = low_32_bits + 2^32 * high_32_bits
range_check(low_32_bits)
range_check(high_32_bits)

A small caveat:
For Goldilock prime, 2^32 * 0XFFFF_FFFF == -1
if high_32_bits value is 0XFFFF_FFFF then above constraint will behave like multiplicand * multiplier = low_limb - 1

However largest possible result for unsigned * unsigned for 32 bits is u32::MAX * u32::MAX = 0xFFFF_FFFE_0000_0001
so high_32_bits for MUL and MULH can never be 0xFFFF_FFFF for any valid case. Hence we add additional constraint for checking that too.

Constraints for MULH and MULHSU

Basic constraints:
As these both operations can have signed value as result, we have following idea:

1. Compute product of absolute values of multiplicand and multiplier.
2. if original result have sign then take 2's complement of result computed in 1) otherwise no change.
3. Destination is high_bits from result computed in 2)

Above algorithm can be checked to work for all cases with simple rust test shown in appendix C.

A small caveat:
For case where result is 0 but any one operand has negative value, destination = 0, low_32_bits = 0, high_32_bits = 0 sign of product is negative so it needs 2's complement
high_32_bits_2s_complement = u32::MAX - high_32_bits + 1 ( add 1 only if carried from complemented of low_32_bits, see appendix B)
high_32_bits_2s_complement = 0x1_0000_0000
In primitive arithmetic we just take bits 0..31 and that turns out to be 0 which is same has destination.
However we can't just take 0..31 bits in field arithmetic. So we handled this as special case when product is zero but one of operand has sign bit 1.

And hence we get following constraint in code

    // if product has negative sign:
    //   if product is zero:
    //     destination == 0 (which is same as high_limb)
    //   else
    //     destination == 2's complement of high_limb
    // else
    //   destination == high_limb
    //
    // NOTE: For MULHU it's always the case that product has positive sign.
    // And we assert that above in constraints for product_sign.
    yield_constr.constraint(
        (lv.inst.ops.mulh + lv.inst.ops.mulhu)
            * (lv.product_sign
                * (lv.product_zero * (destination - high_limb)
                    + (P::ONES - lv.product_zero)
                        * (destination
                            - (P::Scalar::from_noncanonical_u64(0xFFFF_FFFF) - high_limb
                                + lv.product_low_bits_zero)))
                + (P::ONES - lv.product_sign) * (destination - high_limb)),
    );

Appendix

A)
Maximum and minimum possible values:

MAX 4294967295 (0xFFFFFFFF), MAX 4294967295 (0xFFFFFFFF), MULHU RES 18446744065119617025 (0xFFFFFFFE00000001)
MAX 2147483647 (0x7FFFFFFF), MIN -2147483648 (0xFFFFFFFF80000000), MULH RES -4611686016279904256 (0xC000000080000000)
MAX 2147483647 (0x7FFFFFFF), MAX 2147483647 (0x7FFFFFFF), MULH RES 4611686014132420609 (0x3FFFFFFF00000001)
MIN -2147483648 (0xFFFFFFFF80000000), MIN -2147483648 (0xFFFFFFFF80000000), MULH RES 4611686018427387904 (0x4000000000000000)
MIN -2147483648 (0xFFFFFFFF80000000), MAX 4294967295 (0xFFFFFFFF), MULHSU RES -9223372034707292160 (0xFFFFFFFFFFFFFFFF8000000080000000)
MAX 2147483647 (0x7FFFFFFF), MAX 4294967295 (0xFFFFFFFF), MULHSU RES 9223372030412324865 (0x7FFFFFFE80000001)

Goldilock Prime p=18446744069414584321=0xFFFFFFFF00000001 so all above values can be handled by GoldiLock Field.

B)
When we want 2's complement of high_32_bits we can use following equation

0xFFFF_FFFF - high_32_bits (+ 1 if 2's complement of low_32_bit is 0x1_0000_0000)

above case only happens if low_32_limbs is 0 and this u32::MAX - 0 + 1 == 0x1_0000_0000

C)

#[test]
fn prove_mulh(a in u32_extra(), b in u32_extra()) {
    let _ = env_logger::try_init();
    let ai = i64::from(a as i32);
    let bi = i64::from(b as i32);
    let sign_a = i64::from(ai < 0);
    let sign_b = i64::from(bi < 0);
    let ip = ai * bi;
    let (l, h) = a.widening_mul(b);
    let (l_abs, h_abs) = (ai.abs() as u32).widening_mul(bi.abs() as u32);
    prop_assert_eq!(l, ip as u32);
    
    let is_res_negative = sign_a + sign_b;
    let expected_res = ((ip >> 32) & 0xFFFF_FFFF) as u32;

    if is_res_negative == 1 {
        let h_abs_ones_complement  =  u32::MAX - h_abs;
        let l_abs_ones_complement = u32::MAX - l_abs;
        let (_l_abs_twos_complement, overflow) = l_abs_ones_complement.overflowing_add(1_u32);
        let (h_abs_twos_complement, _overflow) = h_abs_ones_complement.overflowing_add(overflow as u32);
        prop_assert_eq!(expected_res - h_abs_twos_complement, 0);
    } else {
        prop_assert_eq!(expected_res.saturating_sub(h_abs), 0);
    }
}

[matthiasgoergens]

What's the maximum degree of the constraints you propose here?

[vivekvpandya]

With extra column to store result when product is negative, we get it 3. See #536

[matthiasgoergens]

Could you please update the text above to reflect that? The constraint in 'A small caveat' seems to have a degree higher than 3?