Fix M31 field arithmetic collision in bitwise constraint verification

[Copilot]

The bitwise constraint functions (and_constraint, or_constraint, xor_constraint, and their immediate variants) attempted to reconstruct 32-bit values using bit 31 with weight 2^31 in M31 field arithmetic. Since 2^31 ≡ 1 (mod 2^31-1), this created exploitable collisions where distinct 32-bit values like 0x00000001 and 0x80000000 both mapped to M31(1), allowing forged proofs for incorrect bitwise operations.

Changes

• Constraint functions: Modified 6 functions to use only bits 0-30, removing bit 31 handling

  • and_constraint, or_constraint, xor_constraint
  • andi_constraint, ori_constraint, xori_constraint

• Tests: Added validation that values exceeding 31-bit range fail verification

Before/After

// Before: Attempted to handle bit 31 separately
for i in 0..31 {
    rs1_reconstructed += row.rs1_bits[i] * M31::new(1 << i);
}
let pow2_30 = M31::new(1 << 30);
rs1_reconstructed += row.rs1_bits[31] * pow2_30 * M31::new(2);  // 2^31 ≡ 1 (mod 2^31-1)

// After: Only use bits 0-30 to avoid field overflow
for i in 0..31 {
    rs1_reconstructed += row.rs1_bits[i] * M31::new(1 << i);
}

Operations now treat values as signed 31-bit, preventing the collision attack while maintaining correct verification for the representable range.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Issue in M31 Field Arithmetic in xor_constraint Constraint Verification</issue_title>
<issue_description>## Summary

The xor_constraint constraint verification function in rv32im.rs uses M31 (Mersenne prime field mod 2³¹ - 1) arithmetic to validate 32-bit RISC-V XOR operations. The problem stems from a fundamental mathematical incompatibility: attempting to represent all 32-bit integers (0 to 2³² - 1) within a field that can only uniquely represent values 0 to 2³¹ - 2. This creates exploitable collisions that allow attackers to forge valid-looking proofs for incorrect XOR computations. Also, this issue persists in and_constraint and or_constraint, but here is considered only the xor_constraint function.

Vulnerability Details

The code attempts to reconstruct 32-bit integers from their bit decomposition within M31:

#[inline]
pub fn xor_constraint(row: &CpuTraceRow) -> M31 {
    if row.is_xor == M31::ZERO {
        return M31::ZERO;
    }

    let two_16 = M31::new(1 << 16);
    let rs1_full = row.rs1_val_lo + row.rs1_val_hi * two_16;
    let rs2_full = row.rs2_val_lo + row.rs2_val_hi * two_16;
    let rd_full = row.rd_val_lo + row.rd_val_hi * two_16;

    let mut rs1_reconstructed = M31::ZERO;
    let mut rs2_reconstructed = M31::ZERO;
    let mut rd_reconstructed = M31::ZERO;
    let mut xor_check = M31::ZERO;

@>  for i in 0..31 {
@>      let pow2 = M31::new(1 << i);
@>      rs1_reconstructed += row.rs1_bits[i] * pow2;
        rs2_reconstructed += row.rs2_bits[i] * pow2;
        rd_reconstructed += row.xor_bits[i] * pow2;
        // XOR logic: xor_bit = a + b - 2ab
        let expected_xor = row.rs1_bits[i] + row.rs2_bits[i] - M31::new(2) * row.rs1_bits[i] * row.rs2_bits[i];
        xor_check += row.xor_bits[i] - expected_xor;
    }
    // Bit 31
@>  let pow2_30 = M31::new(1 << 30);
@>  rs1_reconstructed += row.rs1_bits[31] * pow2_30 * M31::new(2);
    rs2_reconstructed += row.rs2_bits[31] * pow2_30 * M31::new(2);
    rd_reconstructed += row.xor_bits[31] * pow2_30 * M31::new(2);
    let expected_xor = row.rs1_bits[31] + row.rs2_bits[31] - M31::new(2) * row.rs1_bits[31] * row.rs2_bits[31];
    xor_check += row.xor_bits[31] - expected_xor;

    row.is_xor * (
        (rs1_full - rs1_reconstructed) +
        (rs2_full - rs2_reconstructed) +
        xor_check +
        (rd_full - rd_reconstructed)
    )
}

For bit 31, the code computes:
2³⁰ × 2 = 2³¹ in field arithmetic, but 2³¹ mod (2³¹ - 1) = 1. This means bit 31 contributes a weight of 1, not 2³¹ as intended in integer arithmetic.

Mathematical Analysis

Integer reconstruction (intended):
value = Σ(bit[i] × 2^i) for i=0 to 31 = bit[0]×1 + bit[1]×2 + ... + bit[31]×2,147,483,648
Actual M31 reconstruction:
value_m31 = Σ(bit[i] × 2^i) for i=0 to 30, plus bit[31]×1 = bit[0]×1 + bit[1]×2 + ... + bit[30]×1,073,741,824 + bit[31]×1

Multiple distinct 32-bit values collapse to the same M31 representation:

32-bit Value	Binary Representation	M31 Value
0x00000001	00000000...00000001	1
0x80000000	10000000...00000000	1
0x80000001	10000000...00000001	2
0x00000002	00000000...00000010	2

General pattern:
value (32-bit) ≡ (value mod (2³¹ - 1)) (in M31). Values that differ by 2³¹ - 1 collide: 0 and 2,147,483,647, 1 and 2,147,483,648, etc.

The user can claim rs1 = 0x80000000, but providing bits for rs1 = [0,0,...,0,1] (appears to be bit 31 set). M31 reconstruction passes: 0 + 0 + ... + 1 = 1
Also, it can be claimed rs1 = 0x00000001, but providing bits for rs1 = [1,0,...,0,0] (appears to be bit 0 set). M31 reconstruction passes: 1 + 0 + ... + 0 = 1. Both pass the constraint rs1_full - rs1_reconstructed = 0 in M31, despite representing different integers.

Recommendation

Only use bits 0-30, treating RISC-V operations as signed 31-bit.
</issue_description>

<agent_instructions>Review the issue and judge it and reply it. </agent_instructions>

Comments on the Issue (you are @copilot in this section)

• Fixes Issue in M31 Field Arithmetic in xor_constraint Constraint Verification #11

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.