Implement LT & GT opcode

[scroll-dev]

The design of LT & GT can refer to this doc.

This PR is ready for review. @han0110 @ChihChengLiang @miha-stopar

[miha-stopar]

Nice work! I only have one consideration - we would need to have carry * (1 - carry) constraint too, right?

[gaswhat]

@miha-stopar Thanks. I think it is not necessary to check if carry belongs to [0, 1]. Since we already checked a bytes, b bytes, and c bytes are within [0, 255] range, the arithematic constraint with carry (e.g., line 157 in comparator.rs) should be enough to imply that carry can only be 0 or 1. Correct me if I miss something.

[miha-stopar]

@gaswhat My consideration is that one could set carry so big that rhs wraps around the field modulus so that rhs = lhs + field modulus, which would make the check below to pass. Wouldn't be that possible?

rhs = rhs + carry.expr() * exponent;
lt_constraints.push(lhs - rhs);

[ChihChengLiang]

Great work. I added some documentation suggestions and nitpicks.

[ChihChengLiang]

Nitpick: Using minus sign for bullet points could be confusing sometimes.

Suggested change

	// - a < b, a + c = b, result = 1, is_zero(sumc) = 0
	// - a = b, a + c = b, result = 0, is_zero(sumc) = 1
	// - a > b, a + c = b + 2^256, result = 0, is_zero(sumc) = 0
	// a < b, a + c = b, result = 1, is_zero(sumc) = 0
	// a = b, a + c = b, result = 0, is_zero(sumc) = 1
	// a > b, a + c = b + 2^256, result = 0, is_zero(sumc) = 0

[gaswhat]

Updated.

[ChihChengLiang]

Agree with @miha-stopar that we should constrain the carry.
It is hard to find a falsifying example, but we couldn't see a way to justify that carry is binary.
At least for this particular check, it's easy to pass carry=(256^16)^(-1) that still satisfies the equation.

// a[15..0] + c[15..0] = carry * 256^16 + b[15..0] 

[miha-stopar]

Regarding the carry - I think it might be possible to set a > b and result = 1 (result 1 means a < b) following the next steps:

• set a[i] > b[i] for 15 < i < 32 (makes a > b)
• set c[0] = 1 (to avoid sum_c != 0 constraint to fail) and c[i] = 0 for i > 0
• set carry = b[16] + b[17]*256 + ... b[31]*256^15 - a[16] - a[17]*256 - ... - a[31]*256^15 - 1 (this last 1 is for c[0])
• in the previous steps we ensured that the second lhs - rhs constraint holds
• if we chose carry in the third step to be carry * 256^16 < 256^16 (after wrapping over the field modulus), we can choose a[i], b[i], c[i] for i < 16 such that lhs = rhs + carry * 256^16 (we can just set b[i] and c[i] to 0 and set a[i] to be: a[0] + a[1]*256 + ... a[15]*256^15 = carry * 256^16 mod field_modulus)

It's difficult to find carry such that: carry * 256^16 < 256^16, but it might be possible and for this reason I think we should add a constraint for a carry to be 0 or 1.

[gaswhat]

@ChihChengLiang @miha-stopar Thanks for the thoughts on the carry check. I agree with that we should add a constraint for carry. And I've added it the new commits. Please take a look again. Thank you for your reviews.

[ChihChengLiang]

Thank @gaswhat for the update. The commented issues are all addressed. Waiting for a final look from @miha-stopar.

[miha-stopar]

Looks great to me!