chore: Fix constraints typos in RV32IM extension (#1406)

Removed unnecessary or duplicated constraints in the RV32IM extension.

Author: manh9203

extensions/rv32im/circuit/src/adapters/alu.rs

@@ -155,10 +155,7 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> for Rv32BaseAluAdapterAir {
         );
         self.bitwise_lookup_bus
             .send_range(rs2_limbs[0].clone(), rs2_limbs[1].clone())
-            .eval(
-                builder,
-                not(local.rs2_as) * ctx.instruction.is_valid.clone(),
-            );
+            .eval(builder, ctx.instruction.is_valid.clone() - local.rs2_as);
 
         self.memory_bridge
             .read(

extensions/rv32im/circuit/src/adapters/loadstore.rs

@@ -216,6 +216,8 @@ impl<AB: InteractionBuilder> VmAdapterAir<AB> for Rv32LoadStoreAdapterAir {
         // This constraint ensures that the memory write only occurs when `is_valid == 1`.
         builder.assert_bool(write_count);
         builder.when(write_count).assert_one(is_valid.clone());
+
+        // Constrain that if `is_valid == 1` and `write_count == 0`, then `is_load == 1` and `rd_rs2_ptr == x0`
         builder
             .when(is_valid.clone() - write_count)
             .assert_one(is_load.clone());

extensions/rv32im/circuit/src/divrem/core.rs

@@ -232,7 +232,8 @@ where
         // Note:
         // - q_sum is guaranteed to be non-zero if q is non-zero since we've range checked each
         // limb of q to be within [0, 2^LIMB_BITS) already.
-        // - If q is zero and q_ext satisfies the constraint b = c * q + r, then q_sign must be 0.
+        // - If q is zero and q_ext satisfies the constraint
+        // sign_extend(b) = sign_extend(c) * sign_extend(q) + sign_extend(r), then q_sign must be 0.
         // Thus, we do not need additional constraints in case q is zero.
         let nonzero_q = q.iter().fold(AB::Expr::ZERO, |acc, q| acc + *q);
         builder.assert_bool(cols.q_sign);

extensions/rv32im/circuit/src/loadstore/core.rs

@@ -197,7 +197,7 @@ where
                             prev_data[i]
                         }
                     + opcode_when(&[StoreH2])
-                        * if i + 2 < NUM_CELLS / 2 {
+                        * if i - 2 < NUM_CELLS / 2 {
                             read_data[i - 2]
                         } else {
                             prev_data[i]