feat: implement shift constraints and alignment checks #3

rajat-sharma-Dev · 2025-12-10T07:48:13Z

Problem
Shift instructions (SLL, SRL, SRA, SLLI, SRLI, SRAI) had stub implementations returning [M31::ZERO]
Alignment constraints were placeholders that always passed
Project required nightly Rust for Plonky3 compatibility
Changes
Implemented full shift constraints with bit decomposition verification
Added working word/halfword alignment constraints
Added shift witness columns: [shamt], rs1_bits[32], rd_bits[32]
Created [rust-toolchain.toml] with nightly channel
Added 16 shift tests
Files Modified
[rv32im.rs] - shift constraints + tests
[cpu.rs] - alignment constraints
[memory.rs] - alignment constraints
[cpu.rs] - shift witness population
[trace.rs] - shift witness fields
[columns.rs] - shift columns

- Add full SLL/SRL/SRA/SLLI/SRLI/SRAI constraint implementations - Replace alignment constraint stubs with working implementations - Add shift witness columns (shamt, rs1_bits, rd_bits) - Add nightly toolchain for Plonky3 compatibility - Add 16 shift tests, all 512 tests pass

Copilot

Pull request overview

This PR implements shift instruction constraints and memory alignment checks for a RISC-V ZK-VM, transitioning from stub implementations to full constraint verification. The implementation adds bit decomposition witnesses for shift operations and algebraic constraints for memory alignment.

Key changes:

Implemented 6 shift instruction constraints (SLL, SRL, SRA, SLLI, SRLI, SRAI) using bit decomposition
Added word (4-byte) and halfword (2-byte) alignment constraints for memory operations
Added rust-toolchain.toml specifying nightly Rust for Plonky3 compatibility

Reviewed changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 28 comments.

Show a summary per file

File	Description
rust-toolchain.toml	Specifies nightly Rust toolchain for project
crates/trace/src/columns.rs	Adds shift witness columns (shamt, rd_bits) to trace
crates/executor/src/trace.rs	Adds shift witness fields to TraceRow structure
crates/executor/src/cpu.rs	Populates shift witnesses during instruction execution
crates/air/src/rv32im.rs	Implements shift constraints with bit decomposition and adds 16 tests
crates/air/src/memory.rs	Implements word alignment constraint
crates/air/src/cpu.rs	Implements word and halfword alignment constraints with tests

Critical Issues Found: The implementation has significant soundness problems. The alignment and shift constraints use as_u32() to extract field element values and perform operations in the u32 domain, which breaks the algebraic constraint system's soundness. Additionally, bit witnesses lack boolean constraints, allowing malicious provers to provide non-binary values. Several witness columns are defined but unused, wasting resources. These issues must be addressed before the constraints can be considered secure.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2025-12-13T13:56:23Z

crates/air/src/rv32im.rs

    #[inline]
    pub fn sll_constraint(row: &CpuTraceRow) -> M31 {
-        row.is_sll * M31::ZERO // Needs bit decomposition
+        if row.is_sll == 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 rd_full = row.rd_val_lo + row.rd_val_hi * two_16;
+
+        // Verify shamt extraction: shamt = rs2 & 0x1F
+        let rs2_low_5_bits = row.rs2_val_lo.as_u32() & 0x1F;
+        let shamt_check = row.shamt - M31::new(rs2_low_5_bits);
+
+        // Verify bit decomposition and shift operation
+        let mut rs1_reconstructed = M31::ZERO;
+        let mut result_reconstructed = M31::ZERO;
+        let shamt_val = row.shamt.as_u32() as usize;
+
+        for i in 0..32usize {
+            let pow2 = if i < 31 {
+                M31::new(1 << i)
+            } else {
+                M31::new(1u32 << 31)
+            };
+            rs1_reconstructed += row.rs1_bits[i] * pow2;
+
+            // Shift left: result_bit[i] = input_bit[i - shamt] if i >= shamt, else 0
+            let expected_bit = if i >= shamt_val && (i - shamt_val) < 32 {
+                row.rs1_bits[i - shamt_val]
+            } else {
+                M31::ZERO
+            };
+            result_reconstructed += expected_bit * pow2;
+        }
+
+        row.is_sll * (
+            shamt_check +
+            (rs1_full - rs1_reconstructed) +
+            (rd_full - result_reconstructed)
+        )
    }


Missing boolean constraint for bit witnesses. The rs1_bits[i] values must be constrained to be binary (0 or 1) using constraints like rs1_bits[i] * (1 - rs1_bits[i]) = 0. Without this, a malicious prover could provide non-binary values that would make the bit reconstruction check pass with incorrect values.

This same issue applies to all shift constraints (SLL, SRL, SRA, SLLI, SRLI, SRAI) that use bit decomposition.

Copilot · 2025-12-13T13:56:23Z

crates/air/src/rv32im.rs

+        row.is_srl * (
+            shamt_check +
+            (rs1_full - rs1_reconstructed) +
+            (rd_full - result_reconstructed)


Missing boolean constraints for rs1_bits in the SRL constraint. Same issue as SLL - bit witnesses must be constrained to binary values.

Suggested change

row.is_srl * (

shamt_check +

(rs1_full - rs1_reconstructed) +

(rd_full - result_reconstructed)

// Enforce booleanity of rs1_bits: each bit must be 0 or 1

let mut rs1_bits_bool = M31::ZERO;

for i in 0..32 {

let b = row.rs1_bits[i];

rs1_bits_bool += b * (b - M31::ONE);

}

row.is_srl * (

shamt_check +

(rs1_full - rs1_reconstructed) +

(rd_full - result_reconstructed) +

rs1_bits_bool

Copilot · 2025-12-13T13:56:23Z

crates/air/src/rv32im.rs

+        row.is_sra * (
+            shamt_check +
+            (rs1_full - rs1_reconstructed) +
+            (rd_full - result_reconstructed)


Missing boolean constraints for rs1_bits in the SRA constraint. Same issue as other shift constraints - bit witnesses must be constrained to binary values.

Suggested change

row.is_sra * (

shamt_check +

(rs1_full - rs1_reconstructed) +

(rd_full - result_reconstructed)

// Enforce booleanity of rs1_bits: each bit must be 0 or 1

let mut rs1_bits_bool = M31::ZERO;

for i in 0..32 {

let b = row.rs1_bits[i];

rs1_bits_bool += b * (b - M31::ONE);

}

row.is_sra * (

shamt_check +

(rs1_full - rs1_reconstructed) +

(rd_full - result_reconstructed) +

rs1_bits_bool

Copilot · 2025-12-13T13:56:24Z

crates/air/src/rv32im.rs

+            result_reconstructed += expected_bit * pow2;
+        }
+
+        row.is_slli * (shamt_check + (rs1_full - rs1_reconstructed) + (rd_full - result_reconstructed))


Missing boolean constraints for rs1_bits in the SLLI constraint. Bit witnesses must be constrained to binary values.

Suggested change

row.is_slli * (shamt_check + (rs1_full - rs1_reconstructed) + (rd_full - result_reconstructed))

// Enforce booleanity of rs1_bits: each bit must be 0 or 1

let mut rs1_bits_bool = M31::ZERO;

for i in 0..32usize {

let bit = row.rs1_bits[i];

rs1_bits_bool += bit * (bit - M31::ONE);

}

row.is_slli * (shamt_check + (rs1_full - rs1_reconstructed) + (rd_full - result_reconstructed) + rs1_bits_bool)

Copilot · 2025-12-13T13:56:24Z

crates/air/src/rv32im.rs

+    pub sll_bits: [M31; 32],     // SLL result bits
+    pub srl_bits: [M31; 32],     // SRL result bits  
+    pub sra_bits: [M31; 32],     // SRA result bits


The witness columns sll_bits, srl_bits, and sra_bits are defined but never used in the constraints. The shift constraints recompute the expected result bits from the input bits rather than using these witness arrays. These unused columns waste prover time and verifier resources. Either use these witnesses in the constraints or remove them from the structure.

Copilot · 2025-12-13T13:56:29Z

crates/air/src/rv32im.rs

+        let imm_low_5_bits = row.imm.as_u32() & 0x1F;
+        let shamt_check = row.shamt - M31::new(imm_low_5_bits);


Same issue - shamt verification uses as_u32() to extract immediate's low 5 bits in the u32 domain, and there's no range constraint on shamt.

Copilot · 2025-12-13T13:56:29Z

crates/air/src/rv32im.rs

+    }
 }


Inconsistent indentation - the closing brace should align with the function definition above it, not have extra indentation.

Suggested change

}

}

}

}

Copilot · 2025-12-13T13:56:29Z

crates/air/src/rv32im.rs

+
+        // Verify shift left: result_bit[i] = input_bit[i - shamt] if i >= shamt, else 0
+        let mut result_reconstructed = M31::ZERO;
+        let shamt_val = row.shamt.as_u32() as usize;


Same soundness issue - unconstrained use of shamt_val extracted via as_u32() for array indexing in SLLI constraint.

Suggested change

let shamt_val = row.shamt.as_u32() as usize;

let shamt_val = (row.shamt.as_u32() & 0x1F) as usize;

Copilot · 2025-12-13T13:56:30Z

crates/air/src/rv32im.rs

+
+        // Verify shift right logical: result_bit[i] = input_bit[i + shamt] if (i + shamt) < 32, else 0
+        let mut result_reconstructed = M31::ZERO;
+        let shamt_val = row.shamt.as_u32() as usize;


Same soundness issue - unconstrained use of shamt_val extracted via as_u32() for array indexing in SRLI constraint.

Suggested change

let shamt_val = row.shamt.as_u32() as usize;

let shamt_val = (row.shamt.as_u32() & 0x1F) as usize;

Copilot · 2025-12-13T13:56:30Z

crates/air/src/rv32im.rs

+
+        // Verify arithmetic shift right: result_bit[i] = input_bit[i + shamt] if (i + shamt) < 32, else sign_bit
+        let mut result_reconstructed = M31::ZERO;
+        let shamt_val = row.shamt.as_u32() as usize;


Same soundness issue - unconstrained use of shamt_val extracted via as_u32() for array indexing in SRAI constraint.

Suggested change

let shamt_val = row.shamt.as_u32() as usize;

let shamt_val = (row.shamt.as_u32() & 0x1F) as usize;

this-vishalsingh requested a review from Copilot December 13, 2025 13:43

Copilot started reviewing on behalf of this-vishalsingh December 13, 2025 13:43 View session

Copilot AI reviewed Dec 13, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: implement shift constraints and alignment checks #3

feat: implement shift constraints and alignment checks #3

Uh oh!

rajat-sharma-Dev commented Dec 10, 2025

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Copilot AI Dec 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

-        row.is_slli * (shamt_check + (rs1_full - rs1_reconstructed) + (rd_full - result_reconstructed))
+        // Enforce booleanity of rs1_bits: each bit must be 0 or 1
+        let mut rs1_bits_bool = M31::ZERO;
+        for i in 0..32usize {
+            let bit = row.rs1_bits[i];
+            rs1_bits_bool += bit * (bit - M31::ONE);
+        }
+        row.is_slli * (shamt_check + (rs1_full - rs1_reconstructed) + (rd_full - result_reconstructed) + rs1_bits_bool)

		let imm_low_5_bits = row.imm.as_u32() & 0x1F;
		let shamt_check = row.shamt - M31::new(imm_low_5_bits);

-    }
-}
+}
+}

	let shamt_val = row.shamt.as_u32() as usize;
	let shamt_val = (row.shamt.as_u32() & 0x1F) as usize;

feat: implement shift constraints and alignment checks #3

Are you sure you want to change the base?

feat: implement shift constraints and alignment checks #3

Uh oh!

Conversation

rajat-sharma-Dev commented Dec 10, 2025

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 13, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant