Fix underconstrained sign function.

[davidnevadoc]

Description

The sign function in maingate returns the parity of a field element.
In order to do this for an element x it exhibits that x = 2 * k + sign. Where sign is 0 or 1 and k is an auxiliary witness.
However, k needs to be range checked so that this equation doesn't wrap around, inverting the sign.

Note: It would be great to find a way to implement this function without the need for range checks, but I haven't been able to do so.
Any suggestions in this direction are greatly appreciated.

Changes

• sign has been moved from maingate to integer
• An extra range check on the auxiliary witness has been added.
• Update toolchain

[han0110]

I think it's okay to check only the sign of least significant limb if the value is in canonical form (reduced), but in the original impl we are using the least significant limb of unreduced a, which might have alias.

I think we could fix this by change:

-        self.assert_in_field(ctx, a)?;
+        let a = &self.reduce_if_limb_values_exceeds_reduced(ctx, a)?;
+        let a = &self.reduce_if_max_operand_value_exceeds(ctx, a)?;

Does this make sense @kilic? And I'm not sure if we need to do assert_in_field or not, I thought by design all AssignedInteger should be already checked in field.

[davidnevadoc]

I think we need to assert_in_field. The core issue being that for any given x we have that sign(x) != sign(p+x) so we want to ensure that the value of our input is always in the [0, p) range, which is what assert_in_field checks. cc @han0110

[han0110]

The core issue being that for any given x we have that sign(x) != sign(p+x) so we want to ensure that the value of our input is always in the [0, p) range

Yes, we need to make sure it's in canonical form, otherwise the sign will be different. So the original api seems incorrect because it might use the unreduced integer to retrieve the sign (the integer is reduced in assert_in_field). So my fix above is to call the reduce inside the sign function.

Just checked the impl again, I agree that we need to call assert_in_field, but I still doubt if there could be reduced integer not in field.

[kilic]

So my fix above is to call the reduce inside the sign function.

@han0110 @davidnevadoc reduce function is lazy it does not enforce the reduction into field but enforces to be in next power of two of the modulus. To be sound assert_in_field after reduction is required. At this point we may consider combining reduction and field assertation if there is some optimisation

[kilic]

Another way to work around this problem is to use NativeRepresentation instead of LimbRepresentation in the transcript so that we can get rid of sign function according to this observations https://hackmd.io/@sinka/ryLBduu79

[han0110]

reduce function is lazy it does not enforce the reduction into field but enforces to be in next power of two of the modulus

I see now, thanks for explaination