Release v0.3.1

Cargo.toml

@@ -19,7 +19,7 @@ exclude = ["prover-benches"]
 
 [workspace.package]
 edition = "2021"
-version = "0.3.0"
+version = "0.3.1"
 authors = ["The Nexus Team <hello@nexus.xyz>"]
 homepage = "https://nexus.xyz/"
 repository = "https://github.com/nexus-xyz/nexus-zkvm/"

cli/src/command/host.rs

@@ -22,7 +22,7 @@ pub fn handle_command(args: HostArgs) -> anyhow::Result<()> {
 
     if rev.is_none() && tag.is_none() {
         // default to current release
-        tag = Some(String::from("0.3.0"));
+        tag = Some(String::from("0.3.1"));
     }
 
     setup_crate(path, rev, tag)

prover/src/chips/cpu.rs

@@ -507,23 +507,16 @@ impl MachineChip for CpuChip {
                     - pc_carry[0].clone()),
         );
 
-        // Setting pc_next = pc when is_sys_halt=1 or pc_next = pc+4 for other flags
-        // pc_carry_{2,4} used for carry handling
-        // is_type_sys・(4・(1-is_sys_halt) + pc_1 + pc_2·2^8 - pc_carry_1·2^16 - (pc_next_1 + pc_next_2·2^8) = 0
-        eval.add_constraint(
-            is_type_sys.clone()
-                * (E::F::from(BaseField::from(4)) * (E::F::one() - is_sys_halt.clone())
-                    + pc[0].clone()
-                    + pc[1].clone() * BaseField::from(1 << 8)
-                    - pc_carry[0].clone() * BaseField::from(1 << 16)
-                    - (pc_next[0].clone() + pc_next[1].clone() * BaseField::from(1 << 8))),
-        );
-        // is_type_sys・(pc_3 + pc_4·2^8 + pc_carry_1 - pc_carry_2·2^16 - (pc_next_3 + pc_next_1·2^8)) = 0
-        eval.add_constraint(
-            is_type_sys.clone()
-                * (pc[2].clone() + pc[3].clone() * BaseField::from(1 << 8) + pc_carry[0].clone()
-                    - pc_carry[1].clone() * BaseField::from(1 << 16)
-                    - (pc_next[2].clone() + pc_next[3].clone() * BaseField::from(1 << 8))),
-        );
+        // Setting pc_next = pc when is_sys_halt=1 and is_type_sys=1
+        // All the other syscalls except halt are handled in the constraints with is_pc_incremented flag.
+        for limb_idx in (0..WORD_SIZE).step_by(2) {
+            eval.add_constraint(
+                is_type_sys.clone()
+                    * is_sys_halt.clone()
+                    * (pc[limb_idx].clone() + pc[limb_idx + 1].clone() * BaseField::from(1 << 8)
+                        - (pc_next[limb_idx].clone()
+                            + pc_next[limb_idx + 1].clone() * BaseField::from(1 << 8))),
+            );
+        }
     }
 }

prover/src/chips/instructions/add.rs

@@ -1,5 +1,4 @@
-use num_traits::Zero;
-use stwo_prover::constraint_framework::EvalAtRow;
+use stwo_prover::{constraint_framework::EvalAtRow, core::fields::FieldExpOps};
 
 use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE};
 
@@ -18,7 +17,7 @@ use crate::{
 pub struct AddChip;
 
 pub struct ExecutionResult {
-    carry_bits: BoolWord,
+    carry_bits: [bool; 2], // carry bits for 16-bit boundaries
     sum_bytes: Word,
 }
 
@@ -50,6 +49,7 @@ impl ExecuteChip for AddChip {
 
         // Recompute 32-bit result from 8-bit limbs.
         let (sum_bytes, carry_bits) = add_with_carries(value_b, value_c);
+        let carry_bits = [carry_bits[1], carry_bits[3]];
 
         ExecutionResult {
             carry_bits,
@@ -107,20 +107,30 @@ impl MachineChip for AddChip {
         let value_c = trace_eval!(trace_eval, ValueC);
         let value_a = trace_eval!(trace_eval, ValueA);
 
-        for i in 0..WORD_SIZE {
-            let carry = i
-                .checked_sub(1)
-                .map(|j| carry_flag[j].clone())
-                .unwrap_or(E::F::zero());
-
-            // ADD a, b, c
-            // rdval[i] + h1[i] * 2^8 = rs1val[i] + rs2val[i] + h1[i - 1]
-            eval.add_constraint(
-                is_add.clone()
-                    * (value_a[i].clone() + carry_flag[i].clone() * modulus.clone()
-                        - (value_b[i].clone() + value_c[i].clone() + carry)),
-            );
-        }
+        // rdval[0] + rdval[1] * 256 + h1[0] * 2^{16} = rs1val[0] + rs1val[1] * 256 + rs2val[0] + rs2val[1] * 256
+        eval.add_constraint(
+            is_add.clone()
+                * (value_a[0].clone()
+                    + value_a[1].clone() * modulus.clone()
+                    + carry_flag[0].clone() * modulus.clone().pow(2)
+                    - (value_b[0].clone()
+                        + value_b[1].clone() * modulus.clone()
+                        + value_c[0].clone()
+                        + value_c[1].clone() * modulus.clone())),
+        );
+
+        // rdval[2] + rdval[3] * 256 + h1[1] * 2^{16} = rs1val[2] + rs1val[3] * 256 + rs2val[2] + rs2val[3] * 256 + h1[0]
+        eval.add_constraint(
+            is_add.clone()
+                * (value_a[2].clone()
+                    + value_a[3].clone() * modulus.clone()
+                    + carry_flag[1].clone() * modulus.clone().pow(2)
+                    - (value_b[2].clone()
+                        + value_b[3].clone() * modulus.clone()
+                        + value_c[2].clone()
+                        + value_c[3].clone() * modulus.clone()
+                        + carry_flag[0].clone())),
+        );
     }
 }
 

prover/src/chips/instructions/auipc.rs

@@ -1,14 +1,14 @@
-use stwo_prover::constraint_framework::EvalAtRow;
+use stwo_prover::{constraint_framework::EvalAtRow, core::fields::FieldExpOps};
 
-use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE};
+use nexus_vm::riscv::BuiltinOpcode;
 
 use crate::{
     column::Column::{self, *},
     components::AllLookupElements,
     trace::{
         eval::{trace_eval, TraceEval},
         sidenote::SideNote,
-        BoolWord, ProgramStep, TracesBuilder, Word,
+        ProgramStep, TracesBuilder, Word,
     },
     traits::{ExecuteChip, MachineChip},
 };
@@ -17,7 +17,7 @@ use super::add;
 
 pub struct ExecutionResult {
     pub value_a: Word,
-    pub carry_bits: BoolWord,
+    pub carry_bits: [bool; 2], // carry bits for 16-bit boundaries
 }
 
 pub struct AuipcChip;
@@ -31,6 +31,7 @@ impl ExecuteChip for AuipcChip {
 
         // value_a = pc + (imm << 12)
         let (value_a, carry_bits) = add::add_with_carries(pc, imm);
+        let carry_bits = [carry_bits[1], carry_bits[3]];
 
         ExecutionResult {
             value_a,
@@ -81,24 +82,30 @@ impl MachineChip for AuipcChip {
         let [is_auipc] = trace_eval!(trace_eval, Column::IsAuipc);
 
         // Setting a_val = pc + c_val
-        // is_auipc・(pc_1 + c_val_1 - carry_1·2^8 - a_val_1) = 0
-        // is_auipc・(pc_2 + c_val_2 + carry_1 - carry_2·2^8 - a_val_2) = 0
-        // is_auipc・(pc_3 + c_val_3 + carry_2 - carry_3·2^8 - a_val_3) = 0
-        // is_auipc・(pc_4 + c_val_4 + carry_3 - carry_4·2^8 - a_val_4) = 0
+        // is_auipc・(pc_1 + pc_2 * 256 + c_val_1 + c_val_2 * 256 - carry_1·2^{16} - a_val_1 - a_val_2 * 256) = 0
         eval.add_constraint(
             is_auipc.clone()
-                * (pc[0].clone() + value_c[0].clone()
-                    - carry_bits[0].clone() * modulus.clone()
-                    - value_a[0].clone()),
+                * (pc[0].clone()
+                    + pc[1].clone() * modulus.clone()
+                    + value_c[0].clone()
+                    + value_c[1].clone() * modulus.clone()
+                    - carry_bits[0].clone() * modulus.clone().pow(2)
+                    - value_a[0].clone()
+                    - value_a[1].clone() * modulus.clone()),
+        );
+
+        // is_auipc・(pc_3 + pc_4 * 256 + c_val_3 + c_val_4 * 256 + carry_1 - carry_2·2^{16} - a_val_3 - a_val_4 * 256) = 0
+        eval.add_constraint(
+            is_auipc.clone()
+                * (pc[2].clone()
+                    + pc[3].clone() * modulus.clone()
+                    + value_c[2].clone()
+                    + value_c[3].clone() * modulus.clone()
+                    + carry_bits[0].clone()
+                    - carry_bits[1].clone() * modulus.clone().pow(2)
+                    - value_a[2].clone()
+                    - value_a[3].clone() * modulus.clone()),
         );
-        for i in 1..WORD_SIZE {
-            eval.add_constraint(
-                is_auipc.clone()
-                    * (pc[i].clone() + value_c[i].clone() + carry_bits[i - 1].clone()
-                        - carry_bits[i].clone() * modulus.clone()
-                        - value_a[i].clone()),
-            );
-        }
     }
 }
 

prover/src/chips/instructions/beq.rs

@@ -1,18 +1,21 @@
 use num_traits::One;
 use stwo_prover::{
     constraint_framework::EvalAtRow,
-    core::fields::m31::{BaseField, M31},
+    core::fields::{
+        m31::{BaseField, M31},
+        FieldExpOps,
+    },
 };
 
-use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE};
+use nexus_vm::riscv::BuiltinOpcode;
 
 use crate::{
     column::Column::{self, *},
     components::AllLookupElements,
     trace::{
         eval::{trace_eval, TraceEval},
         sidenote::SideNote,
-        BoolWord, ProgramStep, TracesBuilder, Word,
+        ProgramStep, TracesBuilder, Word,
     },
     traits::{ExecuteChip, MachineChip},
 };
@@ -24,7 +27,7 @@ pub struct ExecutionResult {
     pub neq_12_flag: bool,     // Flag indicating if (a_val_1, a_val_2) != (b_val_1, b_val_2)
     pub neq_34_flag: bool,     // Flag indicating if (a_val_3, a_val_4) != (b_val_3, b_val_4)
     pub result: Word,          // Next program counter (pc_next)
-    pub carry_bits: BoolWord,  // Carry bits for addition
+    pub carry_bits: [bool; 2], // Carry bits for addition at 16-bit boundaries
     pub neq_aux: [M31; 2],     // Difference between a_val and b_val
     pub neq_aux_inv: [M31; 2], // Inverse of the difference
 }
@@ -92,6 +95,8 @@ impl ExecuteChip for BeqChip {
         let neq_aux = [neq_12_flag_aux, neq_34_flag_aux];
         let neq_aux_inv = [neq_12_flag_aux_inv, neq_34_flag_aux_inv];
 
+        let carry_bits = [carry_bits[1], carry_bits[3]];
+
         ExecutionResult {
             neq_flag,
             neq_12_flag,
@@ -227,29 +232,31 @@ impl MachineChip for BeqChip {
         // pc_next=pc+c_val if neq_flag = 0
         // pc_next=pc+4 	if neq_flag = 1
         // carry_{1,2,3,4} used for carry handling
-        // is_beq・((1 - neq_flag)・c_val_1 + neq_flag・4 + pc_1 - carry_1·2^8 - pc_next_1) = 0
+        // is_beq・((1 - neq_flag)・(c_val_1 + c_val_2 * 256) + neq_flag・4 + pc_1 + pc_2 * 256 - carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) = 0
         eval.add_constraint(
             is_beq.clone()
-                * ((E::F::one() - neq_flag[0].clone()) * value_c[0].clone()
+                * ((E::F::one() - neq_flag[0].clone())
+                    * (value_c[0].clone() + value_c[1].clone() * modulus.clone())
                     + neq_flag[0].clone() * E::F::from(4u32.into())
                     + pc[0].clone()
-                    - carry_bits[0].clone() * modulus.clone()
-                    - pc_next[0].clone()),
+                    + pc[1].clone() * modulus.clone()
+                    - carry_bits[0].clone() * modulus.clone().pow(2)
+                    - pc_next[0].clone()
+                    - pc_next[1].clone() * modulus.clone()),
         );
 
-        // is_beq・((1 - neq_flag)・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0
-        // is_beq・((1 - neq_flag)・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0
-        // is_beq・((1 - neq_flag)・c_val_4 + pc_4 + carry_3 - carry_4·2^8 - pc_next_4) = 0
-        for i in 1..WORD_SIZE {
-            eval.add_constraint(
-                is_beq.clone()
-                    * ((E::F::one() - neq_flag[0].clone()) * value_c[i].clone()
-                        + pc[i].clone()
-                        + carry_bits[i - 1].clone()
-                        - carry_bits[i].clone() * modulus.clone()
-                        - pc_next[i].clone()),
-            );
-        }
+        // is_beq・((1 - neq_flag)・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_2 - carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0
+        eval.add_constraint(
+            is_beq.clone()
+                * ((E::F::one() - neq_flag[0].clone())
+                    * (value_c[2].clone() + value_c[3].clone() * modulus.clone())
+                    + pc[2].clone()
+                    + pc[3].clone() * modulus.clone()
+                    + carry_bits[0].clone()
+                    - carry_bits[1].clone() * modulus.clone().pow(2)
+                    - pc_next[2].clone()
+                    - pc_next[3].clone() * modulus.clone()),
+        );
 
         // carry_{1,2,3,4} ∈ {0,1} is enforced in RangeBoolChip
     }