fix: set 'different_signs' column only for signed instructions

valida-xyz · May 4, 2024 · aaa207a · aaa207a
1 parent ee93d2d
commit aaa207a
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 7 deletions.
diff --git a/alu_u32/src/lt/mod.rs b/alu_u32/src/lt/mod.rs
@@ -97,10 +97,12 @@ impl Lt32Chip {
             Operation::Lt32(a, b, c) => {
                 cols.is_lt = F::one();
                 self.set_cols(cols, a, b, c);
+                cols.different_signs = F::zero();
             }
             Operation::Lte32(a, b, c) => {
                 cols.is_lte = F::one();
                 self.set_cols(cols, a, b, c);
+                cols.different_signs = F::zero();
             }
             Operation::Slt32(a, b, c) => {
                 cols.is_slt = F::one();

diff --git a/alu_u32/src/lt/stark.rs b/alu_u32/src/lt/stark.rs
@@ -92,9 +92,18 @@ where
         builder.assert_eq(top_comp_1, local.input_1[0]);
         builder.assert_eq(top_comp_2, local.input_2[0]);
 
+        let is_signed = local.is_slt + local.is_sle;
+        let is_unsigned = AB::Expr::one() - is_signed.clone();
+        let same_sign = AB::Expr::one() - local.different_signs;
+        let are_equal = AB::Expr::one() - flag_sum.clone();
+
+        builder
+            .when(is_unsigned.clone())
+            .assert_zero(local.different_signs);
+
         // Check that `different_signs` is set correctly by comparing sign bits.
         builder
-            .when(local.byte_flag[0])
+            .when(is_signed.clone())
             .when_ne(local.top_bits_1[7], local.top_bits_2[7])
             .assert_eq(local.different_signs, AB::Expr::one());
         builder
@@ -111,11 +120,6 @@ where
         builder.assert_bool(local.is_sle);
         builder.assert_bool(local.is_lt + local.is_lte + local.is_slt + local.is_sle);
 
-        let is_signed = local.is_slt + local.is_sle;
-        let is_unsigned = AB::Expr::one() - is_signed;
-        let same_sign = AB::Expr::one() - local.different_signs;
-        let are_equal = AB::Expr::one() - flag_sum.clone();
-
         // Output constraints
         // Case 0: input_1 > input_2 as unsigned ints; equivalently, local.bits[8] == 1
         //  when both inputs have the same sign, signed and unsigned inequality agree.

diff --git a/basic/tests/test_prover.rs b/basic/tests/test_prover.rs
@@ -290,6 +290,7 @@ fn signed_inequality_program<Val: PrimeField32 + TwoAdicField>() -> Vec<Instruct
     // slt32 24(fp), -1, -12(fp), 1, 0
     // slt32 28(fp), -8(fp), -12(fp), 0, 0
     // slt32 32(fp), -8(fp), -4(fp), 0, 0
+
     program.extend([
         InstructionWord {
             opcode: <Slt32Instruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
@@ -370,7 +371,7 @@ fn signed_inequality_program<Val: PrimeField32 + TwoAdicField>() -> Vec<Instruct
         // stop 0, 0, 0, 0, 0
         InstructionWord {
             opcode: <StopInstruction as Instruction<BasicMachine<Val>, Val>>::OPCODE,
-            operands: Operands::default(),
+            operands: Operands([0, 0, 0, 0, 0]),
         },
     ]);