Constraints for MULH & MULHSU #536
Conversation
vivekvpandya
requested review from
matthiasgoergens,
spiral-ladder and
sai-deng
… to multiplier_abs
checking product is zero or not.
vivekvpandya
force-pushed
the
vivek/mulh_3
branch
from
2ce6561 to
1abf9f0
Compare
|
This also contains fixes from https://github.com/0xmozak/mozak-vm/pull/539/files. So first we need to merge https://github.com/0xmozak/mozak-vm/pull/539/files to main. |
like https://github.com/0xmozak/mozak-vm/pull/540/files happens. Use signed_diff() instead of op_diff().
new column res_when_prod_negative.
| } | ||
|
|
||
| // Make sure res_when_prod_negative is computed correctly. |
There was a problem hiding this comment.
In the doc, you mentioned "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."
Why do we need sign of product be positive? We only need the correct destination value, right?
There was a problem hiding this comment.
yes we need only correct destination value.
when result is zero but product sign is negative then in field (0xFFFF_FFFF - high_limb + 1) becomes 0x1_0000_0000, if we ignore anything above 32 bits it gives correct answer but that is not possible in field.
So I have to handle that as special case.
There was a problem hiding this comment.
Just wondering if you change the constraints to
// if product is zero:
// destination == 0 (which is same as high_limb)
// else
// if product has negative sign:
// destination == 2's complement of high_limb
// else
// destination == high_limb
Will the constraints be simpler?
There was a problem hiding this comment.
it will be still degree 4 constraint. To make it degree 3 I have to create column res_when_not_zero, which is analogous to res_when_negative.
So which one you prefer @sai-deng ?
circuits/src/cpu/mul.rs
Outdated
| &[], | ||
| &[(6, a as u32), (7, b)], | ||
| ); | ||
| let (res, _overflow) = i64::from(a).overflowing_mul(i64::from(b)); |
There was a problem hiding this comment.
You can just use wrapping_mul in this case?
| @@ -23,8 +23,8 @@ use crate::cpu::stark::is_binary; | |||
| /// | |||
| /// TODO: range check these two linear combinations of columns: | |||
| /// ```ignore | |||
| /// lv.op1_full_range() + lv.is_signed() * CpuState::<P>::shifted(31); | |||
| /// lv.op2_full_range() + lv.is_signed() * CpuState::<P>::shifted(31); | |||
| /// lv.op1_full_range() + lv.is_op1_signed() * CpuState::<P>::shifted(31); | |||
There was a problem hiding this comment.
Just implement the TODO instead of fixing it up?
There was a problem hiding this comment.
just curious why its not implemented on main? Anything is missing for implementation and this PR add that part?
There was a problem hiding this comment.
Also I think this comment is wrong or I am not understanding it correctly.
op1_full_range() = op1_value - op1_sign_bit * shifted(32)
so here should be checking op1_value == op1_full_range() + op1_sign_bit() * shifted(32) right?
the comment uses shifted(31) that seems incorrect.
|
Closing this as #556 is already in main. |
Discussion explaining constraints: https://github.com/orgs/0xmozak/discussions/538