Replaced the placeholders/comments in the for the word alignment constraint functionality #2

rajat-sharma-Dev · 2025-12-08T19:02:02Z

Replaced the placeholders in the memory alighment checks in crates/air/src/cpu.rs and memory.rs with actual working code for halfword(divisible by 2) and fullword(address divisible by 4) and also added the tests for the same. The tests are passing with all the edge cases also tested. Now the function correctly check if the address is a fullword address(last 2 bits 00) and returns based on that and the same for halfword contraints. This was done so that now this can be RISC-V compliance, Prevents malicious provers from claiming misaligned access succeeded and Programs that violate alignment rules will be rejected.

…rate with actual working code for halfword(divisible by 2) and fullword(address divisible by 4) and also added the tests for the same

this-vishalsingh · 2025-12-10T11:56:14Z

Replaced the placeholders in the memory alighment checks in crates/air/src/cpu.rs and memory.rs with actual working code for halfword(divisible by 2) and fullword(address divisible by 4) and also added the tests for the same. The tests are passing with all the edge cases also tested. Now the function correctly check if the address is a fullword address(last 2 bits 00) and returns based on that and the same for halfword contraints. This was done so that now this can be RISC-V compliance, Prevents malicious provers from claiming misaligned access succeeded and Programs that violate alignment rules will be rejected.

thanks for the contribution @rajat-sharma-Dev! The logic in memory.rs looks correct.

Quick question: the tests use CpuAir::word_alignment_constraint but you updated MemoryAir::word_alignment_constraint. Should the tests point to MemoryAir
instead, or did you plan to update CpuAir as well?

rajat-sharma-Dev · 2025-12-10T15:22:05Z

I updated both [CpuAir::word_alignment_constraint] (in [cpu.rs]) and MemoryAir::word_alignment_constraint (in [memory.rs]) with the same working implementation. The tests use [CpuAir] because that's where the tests module lives.

Both implementations are identical:

[cpu.rs]lines 707-722: [CpuAir::word_alignment_constraint]
[memory.rs] lines 54-66: MemoryAir::word_alignment_constraint
I also added [halfword_alignment_constraint] to [CpuAir] (lines 734-749 in [cpu.rs]).

The reason both exist is that alignment can be checked at either the CPU level (during instruction execution) or at the memory level (during memory access). I kept them consistent so either can be used depending on where the prover integrates the check.

Let me know if you'd prefer me to:

Remove one and keep only the other or add tests for MemoryAir as well or add [halfword_alignment_constraint] to MemoryAir too for consistency

Copilot

Pull request overview

This PR replaces placeholder alignment constraint code with implementations that check word (4-byte) and halfword (2-byte) memory alignment for RISC-V compliance. However, the implementations use non-algebraic operations that are incompatible with STARK proof systems.

Key Changes:

Implemented word alignment constraints checking addresses are divisible by 4
Implemented halfword alignment constraints checking addresses are divisible by 2
Added comprehensive test suite covering aligned/misaligned addresses and edge cases

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
crates/air/src/memory.rs	Replaced placeholder with word alignment constraint using integer division to compute remainder
crates/air/src/cpu.rs	Replaced placeholders with word and halfword alignment constraints using integer division; removed old placeholder tests and added 13 new comprehensive alignment tests

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

Copilot · 2025-12-13T07:35:26Z

crates/air/src/cpu.rs

+        // Check 2-byte alignment: addr % 2 == 0
+        // In M31 field: compute addr_lo mod 2
+        // We extract bottom bit by: addr_lo - 2 * floor(addr_lo / 2)

-        // Placeholder
-        is_half_access * (addr_lo - addr_lo)
+        let two = M31::new(2);
+        let quotient = M31::new(addr_lo.as_u32() / 2);  // Integer division
+        let remainder = addr_lo - quotient * two;       // addr_lo % 2
+
+        // Constraint: when is_half_access = 1, remainder must be 0
+        // If remainder != 0 (i.e., odd address), constraint is non-zero → proof fails
+        is_half_access * remainder


This implementation breaks the algebraic constraint system. The function uses integer division on the underlying u32 value (addr_lo.as_u32() / 2), which cannot be proven in a STARK system because it's not an algebraic operation over the M31 field.

In a STARK proof system, constraints must be expressed as polynomials over the field. To check halfword alignment, you need to:

Add a witness column for the low bit of addr_lo

Add a range constraint to ensure this bit is binary: bit0 * (1 - bit0) = 0

Verify the reconstruction: addr_lo = quotient * 2 + bit0

The alignment constraint becomes: is_half_access * bit0 = 0

While the tests pass with concrete values, this implementation will fail when used in actual proof generation because the prover cannot generate a valid polynomial trace for the non-algebraic division operation.

Copilot · 2025-12-13T07:35:26Z

crates/air/src/memory.rs

+        // Check 4-byte alignment: addr % 4 == 0
+        // In M31 field: compute addr_lo mod 4
+        // We extract bottom 2 bits by: addr_lo - 4 * floor(addr_lo / 4)
+
+        let four = M31::new(4);
+        let quotient = M31::new(addr_lo.as_u32() / 4);  // Integer division
+        let remainder = addr_lo - quotient * four;       // addr_lo % 4
+
+        // Constraint: when is_word = 1, remainder must be 0
+        // If remainder != 0, constraint is non-zero → proof fails
+        is_word * remainder


This implementation breaks the algebraic constraint system. The function uses integer division on the underlying u32 value (addr_lo.as_u32() / 4), which cannot be proven in a STARK system because it's not an algebraic operation over the M31 field.

In a STARK proof system, constraints must be expressed as polynomials over the field. To check alignment, you need to:

Add witness columns for the bit decomposition of the low 2 bits of addr_lo

Add range constraints to ensure these bits are binary (each bit b satisfies: b * (1 - b) = 0)

Verify the reconstruction: addr_lo = quotient * 4 + bit1 * 2 + bit0

The alignment constraint becomes: is_word * (bit1 + bit0) = 0

While the tests pass with concrete values, this implementation will fail when used in actual proof generation because the prover cannot generate a valid polynomial trace for the non-algebraic division operation.

Copilot · 2025-12-13T07:35:26Z

crates/air/src/cpu.rs

+        // Check 4-byte alignment: addr % 4 == 0
+        // In M31 field: compute addr_lo mod 4
+        // We extract bottom 2 bits by: addr_lo - 4 * floor(addr_lo / 4)

-        // Simplified: Check addr_lo mod 4 via auxiliary witness
-        // For now, placeholder assuming alignment is pre-checked
-        is_word_access * (addr_lo - addr_lo) // Identity
+        let four = M31::new(4);
+        let quotient = M31::new(addr_lo.as_u32() / 4);  // Integer division
+        let remainder = addr_lo - quotient * four;       // addr_lo % 4
+
+        // Constraint: when is_word_access = 1, remainder must be 0
+        // If remainder != 0, constraint is non-zero → proof fails
+        is_word_access * remainder


This implementation breaks the algebraic constraint system. The function uses integer division on the underlying u32 value (addr_lo.as_u32() / 4), which cannot be proven in a STARK system because it's not an algebraic operation over the M31 field.

In a STARK proof system, constraints must be expressed as polynomials over the field. To check alignment, you need to:

Add witness columns for the bit decomposition of the low 2 bits of addr_lo

Add range constraints to ensure these bits are binary (each bit b satisfies: b * (1 - b) = 0)

Verify the reconstruction: addr_lo = quotient * 4 + bit1 * 2 + bit0

The alignment constraint becomes: is_word_access * (bit1 + bit0) = 0

While the tests pass with concrete values, this implementation will fail when used in actual proof generation because the prover cannot generate a valid polynomial trace for the non-algebraic division operation.

Copilot

Pull request overview

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

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

Copilot · 2025-12-15T16:30:53Z

crates/air/src/memory.rs

@@ -53,11 +53,16 @@ impl MemoryAir {
    /// For word access: addr mod 4 = 0.
    #[inline]
    pub fn word_alignment_constraint(addr_lo: M31, is_word: M31) -> M31 {


The function signature is missing the quotient parameter. For proper AIR constraints, the quotient must be provided as a witnessed value from the trace. The signature should be: pub fn word_alignment_constraint(addr_lo: M31, quotient: M31, is_word: M31) -> M31, and the function should return a constraint verifying addr_lo = quotient * 4 + remainder. An additional constraint is needed to ensure remainder ∈ {0,1,2,3}.

Copilot · 2025-12-15T16:30:54Z

crates/air/src/memory.rs

+        let four = M31::new(4);
+        let quotient = M31::new(addr_lo.as_u32() / 4);  // Integer division
+        let remainder = addr_lo - quotient * four;       // addr_lo % 4


Critical security vulnerability: The quotient is computed outside the constraint system using non-deterministic integer division. This allows a malicious prover to choose any quotient value, making the remainder always appear valid. In AIR/STARK systems, all constraint evaluations must be polynomial expressions over witnessed values. The quotient should be provided as an auxiliary witness column in the trace, and the constraint should verify the decomposition: addr_lo = quotient * 4 + remainder, along with a range check ensuring remainder ∈ {0,1,2,3}. The current implementation defeats the security purpose of alignment checking.

Copilot · 2025-12-15T16:30:54Z

crates/air/src/cpu.rs

+        let four = M31::new(4);
+        let quotient = M31::new(addr_lo.as_u32() / 4);  // Integer division
+        let remainder = addr_lo - quotient * four;       // addr_lo % 4


Critical security vulnerability: The quotient is computed outside the constraint system using non-deterministic integer division. This allows a malicious prover to choose any quotient value, making the remainder always appear valid. In AIR/STARK systems, all constraint evaluations must be polynomial expressions over witnessed values. The quotient should be provided as an auxiliary witness column in the trace, and the constraint should verify the decomposition: addr_lo = quotient * 4 + remainder, along with a range check ensuring remainder ∈ {0,1,2,3}. The current implementation defeats the security purpose of alignment checking.

Copilot · 2025-12-15T16:30:54Z

crates/air/src/cpu.rs

+        let two = M31::new(2);
+        let quotient = M31::new(addr_lo.as_u32() / 2);  // Integer division
+        let remainder = addr_lo - quotient * two;       // addr_lo % 2


Critical security vulnerability: The quotient is computed outside the constraint system using non-deterministic integer division. This allows a malicious prover to choose any quotient value, making the remainder always appear valid. In AIR/STARK systems, all constraint evaluations must be polynomial expressions over witnessed values. The quotient should be provided as an auxiliary witness column in the trace, and the constraint should verify the decomposition: addr_lo = quotient * 2 + remainder, along with a range check ensuring remainder ∈ {0,1}. The current implementation defeats the security purpose of alignment checking.

Copilot · 2025-12-15T16:30:54Z

crates/air/src/cpu.rs

+    #[test]
+    fn test_word_alignment_valid_aligned() {
+        // Test word access at aligned address (divisible by 4)
+        let addr = 0x1000u32;  // Binary: ...0000 (last 2 bits = 00)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_word = M31::ONE;
+
+        let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+        assert_eq!(constraint, M31::ZERO, 
+            "Word access at aligned address 0x{:X} should pass", addr);
+    }
+
+    #[test]
+    fn test_word_alignment_invalid_offset_1() {
+        // Test word access at misaligned address (offset by 1 byte)
+        let addr = 0x1001u32;  // Binary: ...0001 (last 2 bits = 01)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_word = M31::ONE;
+
+        let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+        assert_ne!(constraint, M31::ZERO, 
+            "Word access at misaligned address 0x{:X} should FAIL", addr);
+    }
+
+    #[test]
+    fn test_word_alignment_invalid_offset_2() {
+        // Test word access at misaligned address (offset by 2 bytes)
+        let addr = 0x1002u32;  // Binary: ...0010 (last 2 bits = 10)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_word = M31::ONE;
+
+        let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+        assert_ne!(constraint, M31::ZERO, 
+            "Word access at misaligned address 0x{:X} should FAIL", addr);
+    }
+
+    #[test]
+    fn test_word_alignment_invalid_offset_3() {
+        // Test word access at misaligned address (offset by 3 bytes)
+        let addr = 0x1003u32;  // Binary: ...0011 (last 2 bits = 11)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_word = M31::ONE;
+
+        let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+        assert_ne!(constraint, M31::ZERO, 
+            "Word access at misaligned address 0x{:X} should FAIL", addr);
+    }
+
+    #[test]
+    fn test_word_alignment_multiple_aligned() {
+        // Test multiple aligned addresses
+        let aligned_addrs = [0x0000, 0x0004, 0x0008, 0x1000, 0x2004, 0xFFF0];
+
+        for addr in aligned_addrs {
+            let addr_lo = M31::new(addr & 0xFFFF);
+            let is_word = M31::ONE;
+
+            let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+            assert_eq!(constraint, M31::ZERO, 
+                "Word access at aligned address 0x{:X} should pass", addr);
+        }
+    }
+
+    #[test]
+    fn test_word_alignment_disabled() {
+        // Test that constraint is disabled when is_word = 0
+        let addr = 0x1001u32;  // Misaligned
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_word = M31::ZERO;  // Not a word access
+
+        let constraint = CpuAir::word_alignment_constraint(addr_lo, is_word);
+
+        assert_eq!(constraint, M31::ZERO, 
+            "Constraint should be disabled when is_word = 0");
+    }
+
+    #[test]
+    fn test_halfword_alignment_valid_even() {
+        // Test halfword access at even address (divisible by 2)
+        let addr = 0x1000u32;  // Binary: ...0000 (last bit = 0)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_half = M31::ONE;
+
+        let constraint = CpuAir::halfword_alignment_constraint(addr_lo, is_half);
+
+        assert_eq!(constraint, M31::ZERO, 
+            "Halfword access at even address 0x{:X} should pass", addr);
+    }
+
+    #[test]
+    fn test_halfword_alignment_valid_even_2() {
+        // Test halfword access at another even address
+        let addr = 0x1002u32;  // Binary: ...0010 (last bit = 0)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_half = M31::ONE;
+
+        let constraint = CpuAir::halfword_alignment_constraint(addr_lo, is_half);
+
+        assert_eq!(constraint, M31::ZERO, 
+            "Halfword access at even address 0x{:X} should pass", addr);
+    }
+
+    #[test]
+    fn test_halfword_alignment_invalid_odd() {
+        // Test halfword access at odd address
+        let addr = 0x1001u32;  // Binary: ...0001 (last bit = 1)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_half = M31::ONE;
+
+        let constraint = CpuAir::halfword_alignment_constraint(addr_lo, is_half);
+
+        assert_ne!(constraint, M31::ZERO, 
+            "Halfword access at odd address 0x{:X} should FAIL", addr);
+    }
+
+    #[test]
+    fn test_halfword_alignment_invalid_odd_2() {
+        // Test halfword access at another odd address
+        let addr = 0x1003u32;  // Binary: ...0011 (last bit = 1)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_half = M31::ONE;
+
+        let constraint = CpuAir::halfword_alignment_constraint(addr_lo, is_half);
+
+        assert_ne!(constraint, M31::ZERO, 
+            "Halfword access at odd address 0x{:X} should FAIL", addr);
+    }
+
+    #[test]
+    fn test_halfword_alignment_disabled() {
+        // Test that constraint is disabled when is_half = 0
+        let addr = 0x1001u32;  // Odd (misaligned for halfword)
+        let addr_lo = M31::new(addr & 0xFFFF);
+        let is_half = M31::ZERO;  // Not a halfword access
+
+        let constraint = CpuAir::halfword_alignment_constraint(addr_lo, is_half);
+
+        assert_eq!(constraint, M31::ZERO, 
+            "Constraint should be disabled when is_half = 0");
+    }


The alignment tests only verify the constraint function logic in isolation, but don't test the actual security property. Since the quotient is computed non-deterministically (outside the constraint system), a malicious prover could pass these tests while bypassing alignment checks in an actual proof. Tests should verify that the constraints properly constrain the witness columns, ideally by attempting to forge a proof with misaligned access and verifying it fails.

Replaced the placeholders in the memory alighment checks in the air c…

3175ef2

…rate with actual working code for halfword(divisible by 2) and fullword(address divisible by 4) and also added the tests for the same

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

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

this-vishalsingh requested a review from x-senpai-x December 13, 2025 07:33

Copilot AI reviewed Dec 13, 2025

View reviewed changes

this-vishalsingh requested a review from Copilot December 15, 2025 15:49

Copilot started reviewing on behalf of this-vishalsingh December 15, 2025 15:49 View session

Copilot AI reviewed Dec 15, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Replaced the placeholders/comments in the for the word alignment constraint functionality #2

Replaced the placeholders/comments in the for the word alignment constraint functionality #2

Uh oh!

rajat-sharma-Dev commented Dec 8, 2025

Uh oh!

this-vishalsingh commented Dec 10, 2025

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 left a comment

Uh oh!

Copilot AI Dec 15, 2025

Uh oh!

Copilot AI Dec 15, 2025

Uh oh!

Copilot AI Dec 15, 2025

Uh oh!

Copilot AI Dec 15, 2025

Uh oh!

Copilot AI Dec 15, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Replaced the placeholders/comments in the for the word alignment constraint functionality #2

Are you sure you want to change the base?

Replaced the placeholders/comments in the for the word alignment constraint functionality #2

Uh oh!

Conversation

rajat-sharma-Dev commented Dec 8, 2025

Uh oh!

this-vishalsingh commented Dec 10, 2025

Uh oh!

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 left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Dec 15, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 15, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 15, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 15, 2025

Choose a reason for hiding this comment

Uh oh!

Copilot AI Dec 15, 2025

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants