check intmul doesn't overflow modulo 2^128-1

Author: johnstonljoseph

crates/examples/snapshots/ethsign.snap

@@ -2,7 +2,7 @@ ethsign circuit
 --
 Number of gates: 265672
 Number of evaluation instructions: 311772
-Number of AND constraints: 335708
+Number of AND constraints: 361166
 Number of MUL constraints: 25458
 Length of value vec: 524288
   Constants: 82

crates/examples/snapshots/zklogin.snap

@@ -2,7 +2,7 @@ zklogin circuit
 --
 Number of gates: 462908
 Number of evaluation instructions: 550412
-Number of AND constraints: 577527
+Number of AND constraints: 604407
 Number of MUL constraints: 26880
 Length of value vec: 1048576
   Constants: 710

crates/frontend/src/compiler/gate/imul.rs

@@ -2,7 +2,7 @@
 //! Uses the MulConstraint: X * Y = (HI << 64) | LO
 
 use crate::compiler::{
-	constraint_builder::ConstraintBuilder,
+	constraint_builder::{ConstraintBuilder, sll},
 	gate::opcode::OpcodeShape,
 	gate_graph::{Gate, GateData, GateParam, Wire},
 };
@@ -27,6 +27,19 @@ pub fn constrain(_gate: Gate, data: &GateData, builder: &mut ConstraintBuilder)
 
 	// Create MulConstraint: X * Y = (HI << 64) | LO
 	builder.mul().a(*x).b(*y).hi(*hi).lo(*lo).build();
+
+	// To guard against overflow modulo 2^128-1, turns out an additional check
+	// is required and sufficient:
+	// x[0] * y[0] = lo[0]
+	// meaning we're verifying integer multiplication on the least significant bits.
+	// We extract the least significant bits by moving them to the most significant positions
+	// and then put them through an AND constraint.
+	builder
+		.and()
+		.a(sll(*x, 63))
+		.b(sll(*y, 63))
+		.c(sll(*lo, 63))
+		.build();
 }
 
 pub fn emit_eval_bytecode(