check for x < m

evm/src/cpu/kernel/asm/bignum/modmul.asm

@@ -7,6 +7,7 @@
 // Both scratch_2 and scratch_3 have size 2*length and be initialized with zeroes.
 
 // The prover provides x := (a * b) % m, which is the output of this function.
+// We first check that x < m.
 // The prover also provides k := (a * b) / m, stored in scratch space.
 // We then check that x + k * m = a * b, by computing both of those using
 // bignum arithmetic, storing the results in scratch space.
@@ -43,7 +44,24 @@ modmul_remainder_loop:
     // stack: i, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
     POP
 
+    // stack: len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
+
     // STEP 2:
+    // We check that x < m.
+
+    PUSH modmul_return_1
+    DUP5
+    DUP7
+    DUP4
+    // stack: len, out_loc, m_loc, modmul_return_1, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
+    // Should return 1 iff the value at out_loc > the value at m_loc; in other words, if x < m.
+    %jump(cmp_bignum)
+modmul_return_1:
+    // stack: cmp_result, len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
+    PUSH 1
+    %assert_eq
+
+    // STEP 3:
     // The prover provides k := (a * b) / m, which we store in scratch_1.
 
     // stack: len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
@@ -75,25 +93,25 @@ modmul_quotient_loop:
     %pop2
     // stack: len, a_loc, b_loc, m_loc, out_loc, s1, s2, s3, retdest
 
-    // STEP 3:
+    // STEP 4:
     // We calculate x + k * m.
 
-    // STEP 3.1:
+    // STEP 4.1:
     // Multiply k with m and store k * m in scratch_2.
-    PUSH modmul_return_1
+    PUSH modmul_return_2
     %stack (return, len, a, b, m, out, s1, s2) -> (len, s1, m, s2, return, len, a, b, out, s2)
-    // stack: len, s1, m_loc, s2, modmul_return_1, len, a_loc, b_loc, out_loc, s2, s3, retdest
+    // stack: len, s1, m_loc, s2, modmul_return_2, len, a_loc, b_loc, out_loc, s2, s3, retdest
     %jump(mul_bignum)
-modmul_return_1:
+modmul_return_2:
     // stack: len, a_loc, b_loc, out_loc, s2, s3, retdest
 
-    // STEP 3.2:
+    // STEP 4.2:
     // Add x into k * m (in scratch_2).
-    PUSH modmul_return_2
+    PUSH modmul_return_3
     %stack (return, len, a, b, out, s2) -> (len, s2, out, return, len, a, b, s2)
-    // stack: len, s2, out_loc, modmul_return_2, len, a_loc, b_loc, s2, s3, retdest
+    // stack: len, s2, out_loc, modmul_return_3, len, a_loc, b_loc, s2, s3, retdest
     %jump(add_bignum)
-modmul_return_2:
+modmul_return_3:
     // stack: carry, len, a_loc, b_loc, s2, s3, retdest
     ISZERO
     %jumpi(no_carry)
@@ -143,18 +161,18 @@ increment_loop:
 no_carry:
     // stack: len, a_loc, b_loc, s2, s3, retdest
 
-    // STEP 4:
+    // STEP 5:
     // We calculate a * b.
 
     // Multiply a with b and store a * b in scratch_3.
-    PUSH modmul_return_3
+    PUSH modmul_return_4
     %stack (return, len, a, b, s2, s3) -> (len, a, b, s3, return, len, s2, s3)
-    // stack: len, a_loc, b_loc, s3, modmul_return_3, len, s2, s3, retdest
+    // stack: len, a_loc, b_loc, s3, modmul_return_4, len, s2, s3, retdest
     %jump(mul_bignum)
-modmul_return_3:
+modmul_return_4:
     // stack: len, s2, s3, retdest
 
-    // STEP 5:
+    // STEP 6:
     // Check that x + k * m = a * b.
 
     // Walk through scratch_2 and scratch_3, checking that they are equal.