diff --git a/Cargo.toml b/Cargo.toml index e4a2f515f..ae788fcac 100644 --- a/Cargo.toml +++ b/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 "] homepage = "https://nexus.xyz/" repository = "https://github.com/nexus-xyz/nexus-zkvm/" diff --git a/cli/src/command/host.rs b/cli/src/command/host.rs index a384cfaa4..6cc69563a 100644 --- a/cli/src/command/host.rs +++ b/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) diff --git a/prover/src/chips/cpu.rs b/prover/src/chips/cpu.rs index dfd440ceb..cdd32a01c 100644 --- a/prover/src/chips/cpu.rs +++ b/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))), + ); + } } } diff --git a/prover/src/chips/instructions/add.rs b/prover/src/chips/instructions/add.rs index 3769022f2..44a2d61b5 100644 --- a/prover/src/chips/instructions/add.rs +++ b/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())), + ); } } diff --git a/prover/src/chips/instructions/auipc.rs b/prover/src/chips/instructions/auipc.rs index f5bacd23d..af5453f39 100644 --- a/prover/src/chips/instructions/auipc.rs +++ b/prover/src/chips/instructions/auipc.rs @@ -1,6 +1,6 @@ -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, *}, @@ -8,7 +8,7 @@ use crate::{ 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()), - ); - } } } diff --git a/prover/src/chips/instructions/beq.rs b/prover/src/chips/instructions/beq.rs index 75eb4978f..374b14c78 100644 --- a/prover/src/chips/instructions/beq.rs +++ b/prover/src/chips/instructions/beq.rs @@ -1,10 +1,13 @@ 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, *}, @@ -12,7 +15,7 @@ use crate::{ 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 } diff --git a/prover/src/chips/instructions/bge.rs b/prover/src/chips/instructions/bge.rs index c29fa373f..743deb43a 100644 --- a/prover/src/chips/instructions/bge.rs +++ b/prover/src/chips/instructions/bge.rs @@ -1,5 +1,5 @@ use num_traits::One; -use stwo_prover::constraint_framework::EvalAtRow; +use stwo_prover::{constraint_framework::EvalAtRow, core::fields::FieldExpOps}; use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE}; @@ -9,7 +9,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -18,9 +18,9 @@ use super::add::{self}; pub struct ExecutionResult { pub diff_bytes: Word, - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // at 16-bit boundaries pub pc_next: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], pub lt_flag: bool, pub h2: Word, pub h3: Word, @@ -47,6 +47,8 @@ impl ExecuteChip for BgeChip { (true, false) => true, }; + let borrow_bits = [borrow_bits[1], borrow_bits[3]]; + // lt_flag is equal to result let (pc_next, carry_bits) = if result { // a < b is true: pc_next = pc + 4 @@ -62,6 +64,8 @@ impl ExecuteChip for BgeChip { h2[WORD_SIZE - 1] &= 0x7f; h3[WORD_SIZE - 1] &= 0x7f; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { diff_bytes, borrow_bits, @@ -134,30 +138,35 @@ impl MachineChip for BgeChip { let diff_bytes = trace_eval!(trace_eval, Column::Helper1); let pc_next = trace_eval!(trace_eval, Column::PcNext); let [is_bge] = trace_eval!(trace_eval, Column::IsBge); - let ltu_flag = borrow_bits[3].clone(); + let ltu_flag = borrow_bits[1].clone(); let [lt_flag] = trace_eval!(trace_eval, Column::LtFlag); let h2 = trace_eval!(trace_eval, Column::Helper2); let h3 = trace_eval!(trace_eval, Column::Helper3); let [sgn_a] = trace_eval!(trace_eval, Column::SgnA); let [sgn_b] = trace_eval!(trace_eval, Column::SgnB); - // is_bge・(a_val_1 - b_val_1 - h1_1 + borrow_1・2^8) = 0 - // is_bge・(a_val_2 - b_val_2 - h1_2 + borrow_2・2^8 - borrow_1) = 0 - // is_bge・(a_val_3 - b_val_3 - h1_3 + borrow_3・2^8 - borrow_2) = 0 - // is_bge・(a_val_4 - b_val_4 - h1_4 + ltu_flag・2^8 - borrow_3) = 0 + // is_bge・(a_val_1 + a_val_2 * 256 - b_val_1 - b_val_2 * 256 - h1_1 - h1_2 * 256 + borrow_1・2^{16}) = 0 eval.add_constraint( is_bge.clone() - * (value_a[0].clone() - value_b[0].clone() - diff_bytes[0].clone() - + borrow_bits[0].clone() * modulus.clone()), + * (value_a[0].clone() + value_a[1].clone() * modulus.clone() + - value_b[0].clone() + - value_b[1].clone() * modulus.clone() + - diff_bytes[0].clone() + - diff_bytes[1].clone() * modulus.clone() + + borrow_bits[0].clone() * modulus.clone().pow(2)), + ); + + // is_bge・(a_val_3 + a_val_4 * 256 - b_val_3 - b_val_4 * 256 - h1_3 - h1_4 * 256 + borrow_2・2^{16} - borrow_1) = 0 + eval.add_constraint( + is_bge.clone() + * (value_a[2].clone() + value_a[3].clone() * modulus.clone() + - value_b[2].clone() + - value_b[3].clone() * modulus.clone() + - diff_bytes[2].clone() + - diff_bytes[3].clone() * modulus.clone() + + borrow_bits[1].clone() * modulus.clone().pow(2) + - borrow_bits[0].clone()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bge.clone() - * (value_a[i].clone() - value_b[i].clone() - diff_bytes[i].clone() - + borrow_bits[i].clone() * modulus.clone() - - borrow_bits[i - 1].clone()), - ); - } // is_bge・ (h2 + sgna・2^7 - a_val_4) = 0 // is_bge・ (h3 + sgnb・2^7 - b_val_4) = 0 @@ -185,28 +194,31 @@ impl MachineChip for BgeChip { // Setting pc_next based on comparison result // pc_next=pc+c_val if lt_flag = 0 // pc_next=pc+4 if lt_flag = 1 - // is_bge・((1 - lt_flag)・c_val_1 + lt_flag・4 + pc_1 - carry_1·2^8 - pc_next_1) =0 - // is_bge・((1 - lt_flag)・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0 - // is_bge・((1 - lt_flag)・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0 - // is_bge・((1 - lt_flag)・c_val_4 + pc_4 + carry_3 - carry_4·2^8 - pc_next_4) = 0 + // is_bge・((1 - lt_flag)・(c_val_1 + c_val_2 * 256) + lt_flag・4 + pc_1 + pc_2 * 256 - carry_2·2^{16} - pc_next_1 - pc_next_2 * 256) = 0 eval.add_constraint( is_bge.clone() - * ((E::F::one() - lt_flag.clone()) * value_c[0].clone() + * ((E::F::one() - lt_flag.clone()) + * (value_c[0].clone() + value_c[1].clone() * modulus.clone()) + lt_flag.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_bge・((1 - lt_flag)・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_2 - carry_4·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_bge.clone() + * ((E::F::one() - lt_flag.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()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bge.clone() - * ((E::F::one() - lt_flag.clone()) * value_c[i].clone() - + pc[i].clone() - + carry_bits[i - 1].clone() - - carry_bits[i].clone() * modulus.clone() - - pc_next[i].clone()), - ); - } } } diff --git a/prover/src/chips/instructions/bgeu.rs b/prover/src/chips/instructions/bgeu.rs index 04b514e77..09d2be281 100644 --- a/prover/src/chips/instructions/bgeu.rs +++ b/prover/src/chips/instructions/bgeu.rs @@ -1,7 +1,7 @@ use num_traits::One; -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, *}, @@ -9,7 +9,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -18,9 +18,9 @@ use super::add::{self}; pub struct ExecutionResult { pub diff_bytes: Word, - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // At 16-bit boundaries. pub pc_next: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], // At 16-bit boundaries. } pub struct BgeuChip; @@ -45,6 +45,9 @@ impl ExecuteChip for BgeuChip { add::add_with_carries(pc, imm) }; + let borrow_bits = [borrow_bits[1], borrow_bits[3]]; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { diff_bytes, borrow_bits, @@ -105,48 +108,55 @@ impl MachineChip for BgeuChip { let diff_bytes = trace_eval!(trace_eval, Column::Helper1); let pc_next = trace_eval!(trace_eval, Column::PcNext); let [is_bgeu] = trace_eval!(trace_eval, Column::IsBgeu); - let ltu_flag = borrow_bits[3].clone(); + let ltu_flag = borrow_bits[1].clone(); - // is_bgeu・(a_val_1 - b_val_1 - h1_1 + borrow_1・2^8) = 0 - // is_bgeu・(a_val_2 - b_val_2 - h1_2 + borrow_2・2^8 - borrow_1) = 0 - // is_bgeu・(a_val_3 - b_val_3 - h1_3 + borrow_3・2^8 - borrow_2) = 0 - // is_bgeu・(a_val_4 - b_val_4 - h1_4 + ltu_flag・2^8 - borrow_3) = 0 + // is_bgeu・(a_val_1 + a_val_2 * 256 - b_val_1 - b_val_2 * 256 - h1_1 - h1_2 * 256 + borrow_1・2^{16}) = 0 eval.add_constraint( is_bgeu.clone() - * (value_a[0].clone() - value_b[0].clone() - diff_bytes[0].clone() - + borrow_bits[0].clone() * modulus.clone()), + * (value_a[0].clone() + value_a[1].clone() * modulus.clone() + - value_b[0].clone() + - value_b[1].clone() * modulus.clone() + - diff_bytes[0].clone() + - diff_bytes[1].clone() * modulus.clone() + + borrow_bits[0].clone() * modulus.clone().pow(2)), + ); + + // is_bgeu・(a_val_3 + a_val_4 * 256 - b_val_3 - b_val_4 * 256 - h1_3 - h1_4 * 256 + borrow_2・2^{16} - borrow_1) = 0 + eval.add_constraint( + is_bgeu.clone() + * (value_a[2].clone() + value_a[3].clone() * modulus.clone() + - value_b[2].clone() + - value_b[3].clone() * modulus.clone() + - diff_bytes[2].clone() + - diff_bytes[3].clone() * modulus.clone() + + borrow_bits[1].clone() * modulus.clone().pow(2) + - borrow_bits[0].clone()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bgeu.clone() - * (value_a[i].clone() - value_b[i].clone() - diff_bytes[i].clone() - + borrow_bits[i].clone() * modulus.clone() - - borrow_bits[i - 1].clone()), - ); - } - // is_bgeu・( (1 - ltu_flag)・c_val_1 + ltu_flag・4 + pc_1 - carry_1·2^8 - pc_next_1) =0 - // is_bgeu・( (1 - ltu_flag)・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0 - // is_bgeu・( (1 - ltu_flag)・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0 - // is_bgeu・( (1 - ltu_flag)・c_val_4 + pc_4 + carry_3 - carry_4·2^8 - pc_next_4) = 0 + // is_bgeu・( (1 - ltu_flag)・(c_val_1 + c_val_2 * 256) + ltu_flag・4 + pc_1 + pc_2 * 256 - carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) =0 eval.add_constraint( is_bgeu.clone() - * ((E::F::one() - ltu_flag.clone()) * value_c[0].clone() + * ((E::F::one() - ltu_flag.clone()) + * (value_c[0].clone() + value_c[1].clone() * modulus.clone()) + ltu_flag.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_bgeu・( (1 - ltu_flag)・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_1 - carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_bgeu.clone() + * ((E::F::one() - ltu_flag.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()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bgeu.clone() - * ((E::F::one() - ltu_flag.clone()) * value_c[i].clone() - + pc[i].clone() - + carry_bits[i - 1].clone() - - carry_bits[i].clone() * modulus.clone() - - pc_next[i].clone()), - ); - } } } diff --git a/prover/src/chips/instructions/blt.rs b/prover/src/chips/instructions/blt.rs index 2a8cae4e1..b5b0c4f08 100644 --- a/prover/src/chips/instructions/blt.rs +++ b/prover/src/chips/instructions/blt.rs @@ -1,5 +1,8 @@ use num_traits::One; -use stwo_prover::constraint_framework::EvalAtRow; +use stwo_prover::{ + constraint_framework::EvalAtRow, + core::fields::{m31::BaseField, FieldExpOps}, +}; use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE}; @@ -9,7 +12,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -18,9 +21,9 @@ use super::add::{self}; pub struct ExecutionResult { pub diff_bytes: Word, - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // At 16-bit boudaries. pub pc_next: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], // At 16-bit boundaries pub lt_flag: bool, pub h2: Word, pub h3: Word, @@ -61,6 +64,9 @@ impl ExecuteChip for BltChip { h2[WORD_SIZE - 1] &= 0x7f; h3[WORD_SIZE - 1] &= 0x7f; + let borrow_bits = [borrow_bits[1], borrow_bits[3]]; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { diff_bytes, borrow_bits, @@ -103,8 +109,6 @@ impl MachineChip for BltChip { traces.fill_columns(row_idx, diff_bytes, Column::Helper1); traces.fill_columns(row_idx, borrow_bits, Column::BorrowFlag); - traces.fill_columns(row_idx, vm_step.get_sgn_a(), Column::SgnA); - traces.fill_columns(row_idx, vm_step.get_sgn_b(), Column::SgnB); traces.fill_columns(row_idx, h2, Column::Helper2); traces.fill_columns(row_idx, h3, Column::Helper3); traces.fill_columns(row_idx, lt_flag, Column::LtFlag); @@ -123,7 +127,7 @@ impl MachineChip for BltChip { _lookup_elements: &AllLookupElements, ) { let modulus = E::F::from(256u32.into()); - let modulus_7 = E::F::from(128u32.into()); + let modulus_7_inv = E::F::from(BaseField::from(128u32).inverse()); let value_a = trace_eval!(trace_eval, ValueA); let value_b = trace_eval!(trace_eval, ValueB); let value_c = trace_eval!(trace_eval, ValueC); @@ -133,42 +137,37 @@ impl MachineChip for BltChip { let diff_bytes = trace_eval!(trace_eval, Column::Helper1); let pc_next = trace_eval!(trace_eval, Column::PcNext); let [is_blt] = trace_eval!(trace_eval, Column::IsBlt); - let ltu_flag = borrow_bits[3].clone(); + let ltu_flag = borrow_bits[1].clone(); let [lt_flag] = trace_eval!(trace_eval, Column::LtFlag); let h2 = trace_eval!(trace_eval, Column::Helper2); let h3 = trace_eval!(trace_eval, Column::Helper3); - let [sgn_a] = trace_eval!(trace_eval, Column::SgnA); - let [sgn_b] = trace_eval!(trace_eval, Column::SgnB); - - // is_blt・(a_val_1 - b_val_1 - h1_1 + borrow_1・2^8) = 0 - // is_blt・(a_val_2 - b_val_2 - h1_2 + borrow_2・2^8 - borrow_1) = 0 - // is_blt・(a_val_3 - b_val_3 - h1_3 + borrow_3・2^8 - borrow_2) = 0 - // is_blt・(a_val_4 - b_val_4 - h1_4 + ltu_flag・2^8 - borrow_3) = 0 - eval.add_constraint( - is_blt.clone() - * (value_a[0].clone() - value_b[0].clone() - diff_bytes[0].clone() - + borrow_bits[0].clone() * modulus.clone()), - ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_blt.clone() - * (value_a[i].clone() - value_b[i].clone() - diff_bytes[i].clone() - + borrow_bits[i].clone() * modulus.clone() - - borrow_bits[i - 1].clone()), - ); - } + // sgn_a is taken to be abbreviation of (a_val_4 - h2) / 2^7 + let sgn_a = + (value_a[WORD_SIZE - 1].clone() - h2[WORD_SIZE - 1].clone()) * modulus_7_inv.clone(); + // sgn_b is taken to be abbreviation of (b_val_4 - h3) / 2^7 + let sgn_b = + (value_b[WORD_SIZE - 1].clone() - h3[WORD_SIZE - 1].clone()) * modulus_7_inv.clone(); - // is_blt・ (h2 + sgna・2^7 - a_val_4) = 0 - // is_blt・ (h3 + sgnb・2^7 - b_val_4) = 0 + // is_blt・(a_val_1 + a_val_2 * 256 - b_val_1 - b_val_2 * 256 - h1_1 - h1_2 * 256 + borrow_1・2^{16}) = 0 eval.add_constraint( is_blt.clone() - * (h2[WORD_SIZE - 1].clone() + sgn_a.clone() * modulus_7.clone() - - value_a[WORD_SIZE - 1].clone()), + * (value_a[0].clone() + value_a[1].clone() * modulus.clone() + - value_b[0].clone() + - value_b[1].clone() * modulus.clone() + - diff_bytes[0].clone() + - diff_bytes[1].clone() * modulus.clone() + + borrow_bits[0].clone() * modulus.clone().pow(2)), ); + // is_blt・(a_val_3 + a_val_4 * 256 - b_val_3 - b_val_4 * 256 - h1_3 - h1_4 * 256 + borrow_2・2^{16} - borrow_1) = 0 eval.add_constraint( is_blt.clone() - * (h3[WORD_SIZE - 1].clone() + sgn_b.clone() * modulus_7.clone() - - value_b[WORD_SIZE - 1].clone()), + * (value_a[2].clone() + value_a[3].clone() * modulus.clone() + - value_b[2].clone() + - value_b[3].clone() * modulus.clone() + - diff_bytes[2].clone() + - diff_bytes[3].clone() * modulus.clone() + + borrow_bits[1].clone() * modulus.clone().pow(2) + - borrow_bits[0].clone()), ); // is_blt・ (sgna・(1-sgnb) + ltu_flag・(sgna・sgnb+(1-sgna)・(1-sgnb)) - lt_flag) =0 @@ -184,28 +183,33 @@ impl MachineChip for BltChip { // Setting pc_next based on comparison result // pc_next=pc+c_val if lt_flag = 1 // pc_next=pc+4 if lt_flag = 0 - // is_blt・(lt_flag・c_val_1 + (1-lt_flag)・4 + pc_1 - carry_1·2^8 - pc_next_1) =0 - // is_blt・(lt_flag・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0 - // is_blt・(lt_flag・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0 - // is_blt・(lt_flag・c_val_4 + pc_4 + carry_3 - carry_4·2^8 - pc_next_4) = 0 + // is_blt・(lt_flag・(c_val_1 + c_val_2 * 256) + (1-lt_flag)・4 + pc_1 + pc_2 * 256 - carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) =0 eval.add_constraint( is_blt.clone() - * (lt_flag.clone() * value_c[0].clone() + * (lt_flag.clone() * (value_c[0].clone() + value_c[1].clone() * modulus.clone()) + (E::F::one() - lt_flag.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()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_blt.clone() - * (lt_flag.clone() * value_c[i].clone() - + pc[i].clone() - + carry_bits[i - 1].clone() - - carry_bits[i].clone() * modulus.clone() - - pc_next[i].clone()), - ); - } + // is_blt・(lt_flag・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_1 - carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_blt.clone() + * (lt_flag.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()), + ); + + // sgn_a is 0 or 1 + eval.add_constraint(is_blt.clone() * (sgn_a.clone() * (E::F::one() - sgn_a.clone()))); + // sgn_b is 0 or 1 + eval.add_constraint(is_blt * (sgn_b.clone() * (E::F::one() - sgn_b.clone()))); } } diff --git a/prover/src/chips/instructions/bltu.rs b/prover/src/chips/instructions/bltu.rs index bb3303a57..12ac51c15 100644 --- a/prover/src/chips/instructions/bltu.rs +++ b/prover/src/chips/instructions/bltu.rs @@ -1,7 +1,7 @@ use num_traits::One; -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, *}, @@ -9,7 +9,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -18,9 +18,9 @@ use super::add::{self}; pub struct ExecutionResult { pub diff_bytes: Word, - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // At 16-bit boundaries pub pc_next: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], // At 16-bit boundaries } pub struct BltuChip; @@ -45,6 +45,9 @@ impl ExecuteChip for BltuChip { add::add_with_carries(pc, 4u32.to_le_bytes()) }; + let borrow_bits = [borrow_bits[1], borrow_bits[3]]; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { diff_bytes, borrow_bits, @@ -105,48 +108,52 @@ impl MachineChip for BltuChip { let diff_bytes = trace_eval!(trace_eval, Column::Helper1); let pc_next = trace_eval!(trace_eval, Column::PcNext); let [is_bltu] = trace_eval!(trace_eval, Column::IsBltu); - let ltu_flag = borrow_bits[3].clone(); + let ltu_flag = borrow_bits[1].clone(); - // is_bltu・(a_val_1 - b_val_1 - h1_1 + borrow_1・2^8) = 0 - // is_bltu・(a_val_2 - b_val_2 - h1_2 + borrow_2・2^8 - borrow_1) = 0 - // is_bltu・(a_val_3 - b_val_3 - h1_3 + borrow_3・2^8 - borrow_2) = 0 - // is_bltu・(a_val_4 - b_val_4 - h1_4 + ltu_flag・2^8 - borrow_3) = 0 + // is_bltu・(a_val_1 + a_val_2 * 256 - b_val_1 - b_val_2 * 256 - h1_1 - h1_2 * 256 + borrow_1・2^{16}) = 0 eval.add_constraint( is_bltu.clone() - * (value_a[0].clone() - value_b[0].clone() - diff_bytes[0].clone() - + borrow_bits[0].clone() * modulus.clone()), + * (value_a[0].clone() + value_a[1].clone() * modulus.clone() + - value_b[0].clone() + - value_b[1].clone() * modulus.clone() + - diff_bytes[0].clone() + - diff_bytes[1].clone() * modulus.clone() + + borrow_bits[0].clone() * modulus.clone().pow(2)), + ); + // is_bltu・(a_val_3 + a_val_4 * 256 - b_val_3 - b_val_4 * 256 - h1_3 - h1_4 * 256 + borrow_2・2^{16} - borrow_1) = 0 + eval.add_constraint( + is_bltu.clone() + * (value_a[2].clone() + value_a[3].clone() * modulus.clone() + - value_b[2].clone() + - value_b[3].clone() * modulus.clone() + - diff_bytes[2].clone() + - diff_bytes[3].clone() * modulus.clone() + + borrow_bits[1].clone() * modulus.clone().pow(2) + - borrow_bits[0].clone()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bltu.clone() - * (value_a[i].clone() - value_b[i].clone() - diff_bytes[i].clone() - + borrow_bits[i].clone() * modulus.clone() - - borrow_bits[i - 1].clone()), - ); - } - // is_bltu・(ltu_flag・c_val_1 + (1-ltu_flag)・4 + pc_1 - carry_1·2^8 - pc_next_1) =0 - // is_bltu・(ltu_flag・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0 - // is_bltu・(ltu_flag・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0 - // is_bltu・(ltu_flag・c_val_4 + pc_4 + carry_3 - carry_4·2^8 - pc_next_4) = 0 + // is_bltu・(ltu_flag・(c_val_1 + c_val_2 * 256) + (1-ltu_flag)・4 + pc_1 + pc_2 * 256 - carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) =0 eval.add_constraint( is_bltu.clone() - * (ltu_flag.clone() * value_c[0].clone() + * (ltu_flag.clone() * (value_c[0].clone() + value_c[1].clone() * modulus.clone()) + (E::F::one() - ltu_flag.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_bltu・(ltu_flag・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_1 - carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_bltu.clone() + * (ltu_flag.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()), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - is_bltu.clone() - * (ltu_flag.clone() * value_c[i].clone() - + pc[i].clone() - + carry_bits[i - 1].clone() - - carry_bits[i].clone() * modulus.clone() - - pc_next[i].clone()), - ); - } } } diff --git a/prover/src/chips/instructions/bne.rs b/prover/src/chips/instructions/bne.rs index 768557c65..c29228a59 100644 --- a/prover/src/chips/instructions/bne.rs +++ b/prover/src/chips/instructions/bne.rs @@ -1,10 +1,13 @@ 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, *}, @@ -12,7 +15,7 @@ use crate::{ 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 pub neq_aux: [M31; 2], // Difference between a_val and b_val pub neq_aux_inv: [M31; 2], // Inverse of the difference } @@ -51,6 +54,7 @@ impl ExecuteChip for BneChip { } else { add::add_with_carries(pc, imm) }; + let carry_bits = [carry_bits[1], carry_bits[3]]; let neq_flag = value_a != value_b; let neq_12_flag = value_a_l != value_b_l; @@ -226,30 +230,32 @@ impl MachineChip for BneChip { // Setting pc_next based on comparison result // pc_next=pc+c_val if neq_flag = 1 // pc_next=pc+4 if neq_flag = 0 - // carry_{1,2,3,4} used for carry handling - // is_bne・(neq_flag・c_val_1 + (1-neq_flag)・4 + pc_1 - carry_1·2^8 - pc_next_1) = 0 + // carry_{2,4} used for carry handling + // is_bne・(neq_flag・(c_val_1 + c_val_2 * 256) + (1-neq_flag)・4 + pc_1 + pc_2 * 256 - carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) = 0 eval.add_constraint( is_bne.clone() - * (neq_flag[0].clone() * value_c[0].clone() - + (E::F::one() - neq_flag[0].clone()) * E::F::from(4u32.into()) + * (neq_flag[0].clone() + * (value_c[0].clone() + value_c[1].clone() * modulus.clone()) + + (E::F::one() - neq_flag[0].clone()) * E::F::from(BaseField::from(4u32)) + 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_bne・(neq_flag・c_val_2 + pc_2 + carry_1 - carry_2·2^8 - pc_next_2) = 0 - // is_bne・(neq_flag・c_val_3 + pc_3 + carry_2 - carry_3·2^8 - pc_next_3) = 0 - // is_bne・(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_bne.clone() - * (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_bne・(neq_flag・(c_val_3 + c_val_4 * 256) + pc_3 + pc_4 * 256 + carry_1 - carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_bne.clone() + * (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 } diff --git a/prover/src/chips/instructions/jal.rs b/prover/src/chips/instructions/jal.rs index 4774f8e9f..ee6983765 100644 --- a/prover/src/chips/instructions/jal.rs +++ b/prover/src/chips/instructions/jal.rs @@ -1,6 +1,6 @@ -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, *}, @@ -8,7 +8,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -17,9 +17,9 @@ use super::add; pub struct ExecutionResult { pub pc_next: Word, - pub pc_carry_bits: BoolWord, + pub pc_carry_bits: [bool; 2], // At 16-bit boundaries pub value_a: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], // At 16-bit boundaries } pub struct JalChip; @@ -36,6 +36,9 @@ impl ExecuteChip for JalChip { let (pc_next, pc_carry_bits) = add::add_with_carries(pc, imm); let (value_a, carry_bits) = add::add_with_carries(pc, 4u32.to_le_bytes()); + let pc_carry_bits = [pc_carry_bits[1], pc_carry_bits[3]]; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { pc_next, pc_carry_bits, @@ -94,49 +97,50 @@ impl MachineChip for JalChip { let [is_jal] = trace_eval!(trace_eval, Column::IsJal); // a_val=pc+4 - // carry1_{1,2,3,4} used for carry handling - // is_jal・(4 + pc_1 - carry1_1·2^8 - a_val_1) = 0 - // is_jal・(pc_2 + carry1_1 - carry1_2·2^8 - a_val_2) = 0 - // is_jal・(pc_3 + carry1_2 - carry1_3·2^8 - a_val_3) = 0 - // is_jal・(pc_4 + carry1_3 - carry1_4·2^8 - a_val_4) = 0 - + // carry1_{2,4} used for carry handling + // is_jal・(4 + pc_1 + pc_2 * 256 - carry1_1·2^{16} - a_val_1 - a_val_2 * 256) = 0 eval.add_constraint( is_jal.clone() - * (E::F::from(4.into()) + pc[0].clone() - - carry_bits[0].clone() * modulus.clone() - - value_a[0].clone()), + * (E::F::from(4.into()) + pc[0].clone() + pc[1].clone() * modulus.clone() + - carry_bits[0].clone() * modulus.clone().pow(2) + - value_a[0].clone() + - value_a[1].clone() * modulus.clone()), + ); + // is_jal・(pc_3 + pc_4 * 256 + carry1_1 - carry1_2·2^{16} - a_val_3 - a_val_4 * 256) = 0 + eval.add_constraint( + is_jal.clone() + * (pc[2].clone() + pc[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_jal.clone() - * (pc[i].clone() + carry_bits[i - 1].clone() - - carry_bits[i].clone() * modulus.clone() - - value_a[i].clone()), - ); - } // Setting pc_next based on comparison result // pc_next=pc+c_val - // pc_carry_{1,2,3,4} used for carry handling - // is_jal・(c_val_1 + pc_1 - pc_carry_1·2^8 - pc_next_1) = 0 - // is_jal・(c_val_2 + pc_2 + pc_carry_1 - pc_carry_2·2^8 - pc_next_2) = 0 - // is_jal・(c_val_3 + pc_3 + pc_carry_2 - pc_carry_3·2^8 - pc_next_3) = 0 - // is_jal・(c_val_4 + pc_4 + pc_carry_3 - pc_carry_4·2^8 - pc_next_4) = 0 + // pc_carry_{2,4} used for carry handling + // is_jal・(c_val_1 + c_val_2 * 256 + pc_1 + pc_2 * 256 - pc_carry_1·2^{16} - pc_next_1 - pc_next_2 * 256) = 0 eval.add_constraint( is_jal.clone() - * (value_c[0].clone() + pc[0].clone() - - pc_carry_bits[0].clone() * modulus.clone() - - pc_next[0].clone()), + * (value_c[0].clone() + + value_c[1].clone() * modulus.clone() + + pc[0].clone() + + pc[1].clone() * modulus.clone() + - pc_carry_bits[0].clone() * modulus.clone().pow(2) + - pc_next[0].clone() + - pc_next[1].clone() * modulus.clone()), + ); + // is_jal・(c_val_3 + c_val_4 * 256 + pc_3 + pc_4 * 256 + pc_carry_1 - pc_carry_2·2^{16} - pc_next_3 - pc_next_4 * 256) = 0 + eval.add_constraint( + is_jal.clone() + * (value_c[2].clone() + + value_c[3].clone() * modulus.clone() + + pc[2].clone() + + pc[3].clone() * modulus.clone() + + pc_carry_bits[0].clone() + - pc_carry_bits[1].clone() * modulus.clone().pow(2) + - pc_next[2].clone() + - pc_next[3].clone() * modulus.clone()), ); - - for i in 1..WORD_SIZE { - eval.add_constraint( - is_jal.clone() - * (value_c[i].clone() + pc[i].clone() + pc_carry_bits[i - 1].clone() - - pc_carry_bits[i].clone() * modulus.clone() - - pc_next[i].clone()), - ); - } } } diff --git a/prover/src/chips/instructions/jalr.rs b/prover/src/chips/instructions/jalr.rs index 9fff41494..37a22d6bf 100644 --- a/prover/src/chips/instructions/jalr.rs +++ b/prover/src/chips/instructions/jalr.rs @@ -8,7 +8,7 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; @@ -20,9 +20,9 @@ pub struct ExecutionResult { pub pc_next_aux: Word, pub qt_aux: u8, pub rem_aux: bool, - pub pc_carry_bits: BoolWord, + pub pc_carry_bits: [bool; 2], // At 16-bit boundaries pub value_a: Word, - pub carry_bits: BoolWord, + pub carry_bits: [bool; 2], // At 16-bit boundaries } pub struct JalrChip; @@ -53,6 +53,9 @@ impl ExecuteChip for JalrChip { let (value_a, carry_bits) = add::add_with_carries(pc, 4u32.to_le_bytes()); + let pc_carry_bits = [pc_carry_bits[1], pc_carry_bits[3]]; + let carry_bits = [carry_bits[1], carry_bits[3]]; + ExecutionResult { pc_next, pc_next_aux, @@ -128,20 +131,20 @@ impl MachineChip for JalrChip { // a_val=pc+4 // carry1_{1,2,3,4} used for carry handling - // is_jalr・(4 + pc_1 + pc_2 * 256 - carry1_2·2^{16} - a_val_1 - a_val_2 * 256) = 0 - // is_jalr・(pc_3 + pc_3 * 256 + carry1_2 - carry1_4·2^{16} - a_val_3 - a_val_4 * 256) = 0 + // is_jalr・(4 + pc_1 + pc_2 * 256 - carry1_1·2^{16} - a_val_1 - a_val_2 * 256) = 0 + // is_jalr・(pc_3 + pc_3 * 256 + carry1_1 - carry1_2·2^{16} - a_val_3 - a_val_4 * 256) = 0 eval.add_constraint( is_jalr.clone() * (E::F::from(4.into()) + pc[0].clone() + pc[1].clone() * modulus.clone() - - carry_bits[1].clone() * modulus.clone().pow(2) + - carry_bits[0].clone() * modulus.clone().pow(2) - value_a[0].clone() - value_a[1].clone() * modulus.clone()), ); eval.add_constraint( is_jalr.clone() - * (pc[2].clone() + pc[3].clone() * modulus.clone() + carry_bits[1].clone() - - carry_bits[3].clone() * modulus.clone().pow(2) + * (pc[2].clone() + pc[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()), ); @@ -149,15 +152,15 @@ impl MachineChip for JalrChip { // Setting pc_next // pc_next_aux = b_val + c_val // pc_carry_{1,2,3,4} used for carry handling - // is_jalr・(c_val_1 + c_val_2 * 256 + b_val_1 + b_val_2 * 256 - pc_carry_2·2^{16} - pc_next_aux_1 - pc_next_aux_2 * 256) = 0 - // is_jalr・(c_val_3 + c_val_4 * 256 + b_val_3 + b_val_4 * 256 + pc_carry_2 - pc_carry_4·2^{16} - pc_next_aux_3 - pc_next_aux_4 * 256) = 0 + // is_jalr・(c_val_1 + c_val_2 * 256 + b_val_1 + b_val_2 * 256 - pc_carry_1·2^{16} - pc_next_aux_1 - pc_next_aux_2 * 256) = 0 + // is_jalr・(c_val_3 + c_val_4 * 256 + b_val_3 + b_val_4 * 256 + pc_carry_1 - pc_carry_2·2^{16} - pc_next_aux_3 - pc_next_aux_4 * 256) = 0 eval.add_constraint( is_jalr.clone() * (value_c[0].clone() + value_c[1].clone() * modulus.clone() + value_b[0].clone() + value_b[1].clone() * modulus.clone() - - pc_carry_bits[1].clone() * modulus.clone().pow(2) + - pc_carry_bits[0].clone() * modulus.clone().pow(2) - pc_next_aux[0].clone() - pc_next_aux[1].clone() * modulus.clone()), ); @@ -167,8 +170,8 @@ impl MachineChip for JalrChip { + value_c[3].clone() * modulus.clone() + value_b[2].clone() + value_b[3].clone() * modulus.clone() - + pc_carry_bits[1].clone() - - pc_carry_bits[3].clone() * modulus.clone().pow(2) + + pc_carry_bits[0].clone() + - pc_carry_bits[1].clone() * modulus.clone().pow(2) - pc_next_aux[2].clone() - pc_next_aux[3].clone() * modulus.clone()), ); diff --git a/prover/src/chips/instructions/load_store.rs b/prover/src/chips/instructions/load_store.rs index 9b4eac85d..fe68a761b 100644 --- a/prover/src/chips/instructions/load_store.rs +++ b/prover/src/chips/instructions/load_store.rs @@ -27,7 +27,7 @@ use crate::{ FinalizedTraces, PreprocessedTraces, ProgramStep, TracesBuilder, Word, }, traits::MachineChip, - virtual_column::{VirtualColumn, VirtualColumnForSum}, + virtual_column::{IsLoad, IsTypeS, VirtualColumn, VirtualColumnForSum}, }; use super::add::add_with_carries; @@ -194,33 +194,38 @@ impl MachineChip for LoadStoreChip { let ram1_ts_prev_aux = trace_eval!(trace_eval, Ram1TsPrevAux); let helper1 = trace_eval!(trace_eval, Column::Helper1); let [ram1_accessed] = Ram1Accessed::eval(trace_eval); - // ram1_ts_prev_aux_1 + 1 + ram1_ts_prev_1 = clk_1 + h1_1・2^8 (conditioned on ram1_accessed != 0) + // ram1_ts_prev_aux_1 + ram1_ts_prev_aux_2 * 256 + 1 + ram1_ts_prev_1 + ram1_ts_prev_2 * 256 = clk_1 + clk_2 * 256 + h1_2・2^16 + // (conditioned on ram1_accessed != 0) eval.add_constraint( ram1_accessed.clone() - * (ram1_ts_prev_aux[0].clone() + E::F::one() + ram1_ts_prev[0].clone() + * (ram1_ts_prev_aux[0].clone() + + ram1_ts_prev_aux[1].clone() * BaseField::from(1 << 8) + + E::F::one() + + ram1_ts_prev[0].clone() + + ram1_ts_prev[1].clone() * BaseField::from(1 << 8) - clk[0].clone() - - helper1[0].clone() * BaseField::from(1 << 8)), + - clk[1].clone() * BaseField::from(1 << 8) + - helper1[1].clone() * BaseField::from(1 << 16)), ); - // ram1_ts_prev_aux_2 + h1_1 + ram1_ts_prev_2 = clk_2 + h1_2・2^8 (conditioned on ram1_accessed != 0) - // ram1_ts_prev_aux_3 + h1_2 + ram1_ts_prev_3 = clk_3 + h1_3・2^8 (conditioned on ram1_accessed != 0) - // ram1_ts_prev_aux_4 + h1_3 + ram1_ts_prev_4 = clk_4 + h1_4・2^8 (conditioned on ram1_accessed != 0) - for i in 1..WORD_SIZE { - eval.add_constraint( - ram1_accessed.clone() - * (ram1_ts_prev_aux[i].clone() - + helper1[i - 1].clone() - + ram1_ts_prev[i].clone() - - clk[i].clone() - - helper1[i].clone() * BaseField::from(1 << 8)), - ); - } - // h1_1・(h1_1 - 1) = 0; h1_2・(h1_2 - 1) = 0 (conditioned on ram1_accessed != 0) - // h1_3・(h1_3 - 1) = 0; h1_4 = 0 (conditioned on ram1_accessed != 0) - for helper_limb in helper1.iter().take(WORD_SIZE - 1) { - eval.add_constraint( - helper_limb.clone() * (helper_limb.clone() - E::F::one()) * ram1_accessed.clone(), - ); - } + // ram1_ts_prev_aux_3 + ram1_ts_prev_aux_4 * 256 + h1_2 + ram1_ts_prev_3 + ram1_ts_prev_4 * 256 = clk_3 + clk_4 * 256 + h1_4・2^16 + // (conditioned on ram1_accessed != 0) + eval.add_constraint( + ram1_accessed.clone() + * (ram1_ts_prev_aux[2].clone() + + ram1_ts_prev_aux[3].clone() * BaseField::from(1 << 8) + + helper1[1].clone() + + ram1_ts_prev[2].clone() + + ram1_ts_prev[3].clone() * BaseField::from(1 << 8) + - clk[2].clone() + - clk[3].clone() * BaseField::from(1 << 8) + - helper1[3].clone() * BaseField::from(1 << 16)), + ); + + // h1_2・(h1_2 - 1) = 0 (conditioned on ram1_accessed != 0) + eval.add_constraint( + helper1[1].clone() * (helper1[1].clone() - E::F::one()) * ram1_accessed.clone(), + ); + // h1_4 = 0 (conditioned on ram1_accessed != 0) eval.add_constraint(helper1[WORD_SIZE - 1].clone() * ram1_accessed.clone()); // Computing ram2_ts_prev_aux = clk - 1 - ram2_ts_prev @@ -229,33 +234,38 @@ impl MachineChip for LoadStoreChip { let ram2_ts_prev_aux = trace_eval!(trace_eval, Ram2TsPrevAux); let helper2 = trace_eval!(trace_eval, Column::Helper2); let [ram2_accessed] = Ram2Accessed::eval(trace_eval); - // ram2_ts_prev_aux_1 + 1 + ram2_ts_prev_1 = clk_1 + h2_1・2^8 (conditioned on ram2_accessed != 0) + // ram2_ts_prev_aux_1 + ram2_ts_prev_aux_2 * 256 + 1 + ram2_ts_prev_1 + ram2_ts_prev_2 * 256 = clk_1 + clk_2 * 256 + h2_2・2^{16} + // (conditioned on ram2_accessed != 0) eval.add_constraint( ram2_accessed.clone() - * (ram2_ts_prev_aux[0].clone() + E::F::one() + ram2_ts_prev[0].clone() + * (ram2_ts_prev_aux[0].clone() + + ram2_ts_prev_aux[1].clone() * BaseField::from(1 << 8) + + E::F::one() + + ram2_ts_prev[0].clone() + + ram2_ts_prev[1].clone() * BaseField::from(1 << 8) - clk[0].clone() - - helper2[0].clone() * BaseField::from(1 << 8)), + - clk[1].clone() * BaseField::from(1 << 8) + - helper2[1].clone() * BaseField::from(1 << 16)), ); - // ram2_ts_prev_aux_2 + h2_1 + ram2_ts_prev_2 = clk_2 + h2_2・2^8 (conditioned on ram2_accessed != 0) - // ram2_ts_prev_aux_3 + h2_2 + ram2_ts_prev_3 = clk_3 + h2_3・2^8 (conditioned on ram2_accessed != 0) - // ram2_ts_prev_aux_4 + h2_3 + ram2_ts_prev_4 = clk_4 + h2_4・2^8 (conditioned on ram2_accessed != 0) - for i in 1..WORD_SIZE { - eval.add_constraint( - ram2_accessed.clone() - * (ram2_ts_prev_aux[i].clone() - + helper2[i - 1].clone() - + ram2_ts_prev[i].clone() - - clk[i].clone() - - helper2[i].clone() * BaseField::from(1 << 8)), - ); - } - // h2_1・(h2_1 - 1) = 0; h2_2・(h2_2 - 1) = 0 (conditioned on ram2_accessed != 0) - // h2_3・(h2_3 - 1) = 0; h2_4 = 0 (conditioned on ram2_accessed != 0) - for helper2_limb in helper2.iter().take(WORD_SIZE - 1) { - eval.add_constraint( - helper2_limb.clone() * (helper2_limb.clone() - E::F::one()) * ram2_accessed.clone(), - ); - } + // ram2_ts_prev_aux_3 + ram2_ts_prev_aux_4 * 256 + h2_2 + ram2_ts_prev_3 + ram2_ts_prev_4 * 256 = clk_3 + clk_4 * 256 + h2_4・2^{16} + // (conditioned on ram2_accessed != 0) + eval.add_constraint( + ram2_accessed.clone() + * (ram2_ts_prev_aux[2].clone() + + ram2_ts_prev_aux[3].clone() * BaseField::from(1 << 8) + + helper2[1].clone() + + ram2_ts_prev[2].clone() + + ram2_ts_prev[3].clone() * BaseField::from(1 << 8) + - clk[2].clone() + - clk[3].clone() * BaseField::from(1 << 8) + - helper2[3].clone() * BaseField::from(1 << 16)), + ); + + // h2_2・(h2_2 - 1) = 0 (conditioned on ram2_accessed != 0) + eval.add_constraint( + helper2[1].clone() * (helper2[1].clone() - E::F::one()) * ram2_accessed.clone(), + ); + // h2_4 = 0 (conditioned on ram2_accessed != 0) eval.add_constraint(helper2[WORD_SIZE - 1].clone() * ram2_accessed.clone()); // Computing ram3_ts_prev_aux = clk - 1 - ram3_ts_prev @@ -264,35 +274,37 @@ impl MachineChip for LoadStoreChip { let ram3_ts_prev_aux = trace_eval!(trace_eval, Ram3TsPrevAux); let helper3 = trace_eval!(trace_eval, Column::Helper3); let [ram3_4_accessed] = Ram3_4Accessed::eval(trace_eval); - // ram3_ts_prev_aux_1 + 1 + ram3_ts_prev_1 = clk_1 + h3_1・2^8 (conditioned on ram3_accessed != 0) + // ram3_ts_prev_aux_1 + ram3_ts_prev_aux_2 * 256 + 1 + ram3_ts_prev_1 + ram3_ts_prev_2 * 256 = clk_1 + clk_2 * 256 + h3_2・2^{16} + // (conditioned on ram3_accessed != 0) eval.add_constraint( ram3_4_accessed.clone() - * (ram3_ts_prev_aux[0].clone() + E::F::one() + ram3_ts_prev[0].clone() + * (ram3_ts_prev_aux[0].clone() + + ram3_ts_prev_aux[1].clone() * BaseField::from(1 << 8) + + E::F::one() + + ram3_ts_prev[0].clone() + + ram3_ts_prev[1].clone() * BaseField::from(1 << 8) - clk[0].clone() - - helper3[0].clone() * BaseField::from(1 << 8)), + - clk[1].clone() * BaseField::from(1 << 8) + - helper3[1].clone() * BaseField::from(1 << 16)), ); - // ram3_ts_prev_aux_2 + h3_1 + ram3_ts_prev_2 = clk_2 + h3_2・2^8 (conditioned on ram3_accessed != 0) - // ram3_ts_prev_aux_3 + h3_2 + ram3_ts_prev_3 = clk_3 + h3_3・2^8 (conditioned on ram3_accessed != 0) - // ram3_ts_prev_aux_4 + h3_3 + ram3_ts_prev_4 = clk_4 + h3_4・2^8 (conditioned on ram3_accessed != 0) - for i in 1..WORD_SIZE { - eval.add_constraint( - ram3_4_accessed.clone() - * (ram3_ts_prev_aux[i].clone() - + helper3[i - 1].clone() - + ram3_ts_prev[i].clone() - - clk[i].clone() - - helper3[i].clone() * BaseField::from(1 << 8)), - ); - } - // h3_1・(h3_1 - 1) = 0; h3_2・(h3_2 - 1) = 0 (conditioned on ram3_accessed != 0) - // h3_3・(h3_3 - 1) = 0; h3_4 = 0 (conditioned on ram3_accessed != 0) - for helper3_limb in helper3.iter().take(WORD_SIZE - 1) { - eval.add_constraint( - helper3_limb.clone() - * (helper3_limb.clone() - E::F::one()) - * ram3_4_accessed.clone(), - ); - } + // ram3_ts_prev_aux_3 + ram3_ts_prev_aux_4 * 256 + h3_2 + ram3_ts_prev_3 + ram3_ts_prev_4 * 256 = clk_3 + clk_4 * 256 + h3_4・2^{16} + // (conditioned on ram3_accessed != 0) + eval.add_constraint( + ram3_4_accessed.clone() + * (ram3_ts_prev_aux[2].clone() + + ram3_ts_prev_aux[3].clone() * BaseField::from(1 << 8) + + helper3[1].clone() + + ram3_ts_prev[2].clone() + + ram3_ts_prev[3].clone() * BaseField::from(1 << 8) + - clk[2].clone() + - clk[3].clone() * BaseField::from(1 << 8) + - helper3[3].clone() * BaseField::from(1 << 16)), + ); + // h3_2・(h3_2 - 1) = 0 (conditioned on ram3_accessed != 0) + eval.add_constraint( + helper3[1].clone() * (helper3[1].clone() - E::F::one()) * ram3_4_accessed.clone(), + ); + // h3_4 = 0 (conditioned on ram3_accessed != 0) eval.add_constraint(helper3[WORD_SIZE - 1].clone() * ram3_4_accessed.clone()); // Computing ram4_ts_prev_aux = clk - 1 - ram4_ts_prev @@ -302,31 +314,200 @@ impl MachineChip for LoadStoreChip { let helper4 = trace_eval!(trace_eval, Column::Helper4); eval.add_constraint( ram3_4_accessed.clone() - * (ram4_ts_prev_aux[0].clone() + E::F::one() + ram4_ts_prev[0].clone() + * (ram4_ts_prev_aux[0].clone() + + ram4_ts_prev_aux[1].clone() * BaseField::from(1 << 8) + + E::F::one() + + ram4_ts_prev[0].clone() + + ram4_ts_prev[1].clone() * BaseField::from(1 << 8) - clk[0].clone() - - helper4[0].clone() * BaseField::from(1 << 8)), + - clk[1].clone() * BaseField::from(1 << 8) + - helper4[1].clone() * BaseField::from(1 << 16)), ); - for i in 1..WORD_SIZE { - eval.add_constraint( - ram3_4_accessed.clone() - * (ram4_ts_prev_aux[i].clone() - + helper4[i - 1].clone() - + ram4_ts_prev[i].clone() - - clk[i].clone() - - helper4[i].clone() * BaseField::from(1 << 8)), - ); - } - // h4_1・(h4_1 - 1) = 0; h4_2・(h4_2 - 1) = 0 (conditioned on ram4_accessed != 0) - // h4_3・(h4_3 - 1) = 0; h4_4 = 0 (conditioned on ram4_accessed != 0) - for helper_4_limb in helper4.iter().take(WORD_SIZE - 1) { - eval.add_constraint( - helper_4_limb.clone() - * (helper_4_limb.clone() - E::F::one()) - * ram3_4_accessed.clone(), - ); - } + eval.add_constraint( + ram3_4_accessed.clone() + * (ram4_ts_prev_aux[2].clone() + + ram4_ts_prev_aux[3].clone() * BaseField::from(1 << 8) + + helper4[1].clone() + + ram4_ts_prev[2].clone() + + ram4_ts_prev[3].clone() * BaseField::from(1 << 8) + - clk[2].clone() + - clk[3].clone() * BaseField::from(1 << 8) + - helper4[3].clone() * BaseField::from(1 << 16)), + ); + // h4_2・(h4_2 - 1) = 0 (conditioned on ram4_accessed != 0) + eval.add_constraint( + helper4[1].clone() * (helper4[1].clone() - E::F::one()) * ram3_4_accessed.clone(), + ); + // h4_4 = 0 (conditioned on ram4_accessed != 0) eval.add_constraint(helper4[WORD_SIZE - 1].clone() * ram3_4_accessed.clone()); + let ram_base_addr = trace_eval!(trace_eval, Column::RamBaseAddr); + let carry_flag = trace_eval!(trace_eval, Column::CarryFlag); + let value_b = trace_eval!(trace_eval, Column::ValueB); + let value_c = trace_eval!(trace_eval, Column::ValueC); + let value_a = trace_eval!(trace_eval, Column::ValueA); + let [is_load] = IsLoad::eval(trace_eval); + // Constrain the value of RamBaseAddr in case of load operations + // is_load * (ram_base_addr_1 + ram_base_addr_2 * 256 - value_b_1 - value_b_2 * 256 - value_c_1 - value_c_2 * 256 + carry_1 * 2^{16}) = 0 + eval.add_constraint( + is_load.clone() + * (ram_base_addr[0].clone() + ram_base_addr[1].clone() * BaseField::from(1 << 8) + - value_b[0].clone() + - value_b[1].clone() * BaseField::from(1 << 8) + - value_c[0].clone() + - value_c[1].clone() * BaseField::from(1 << 8) + + carry_flag[0].clone() * BaseField::from(1 << 16)), + ); + // is_load * (ram_base_addr_3 + ram_base_addr_4 * 256 - carry_1 - value_b_3 - value_b_4 * 256 - value_c_3 - value_c_4 * 256 + carry_2 * 2^{16}) = 0 + eval.add_constraint( + is_load.clone() + * (ram_base_addr[2].clone() + ram_base_addr[3].clone() * BaseField::from(1 << 8) + - carry_flag[0].clone() + - value_b[2].clone() + - value_b[3].clone() * BaseField::from(1 << 8) + - value_c[2].clone() + - value_c[3].clone() * BaseField::from(1 << 8) + + carry_flag[1].clone() * BaseField::from(1 << 16)), + ); + + // Constrain the value of RamBaseAddr in case of store operations + let [is_store] = IsTypeS::eval(trace_eval); + // is_store * (ram_base_addr_1 + ram_base_addr_2 * 256 - value_a_1 - value_a_2 * 256 - value_c_1 - value_c_2 * 256 + carry_1 * 2^{16}) = 0 + eval.add_constraint( + is_store.clone() + * (ram_base_addr[0].clone() + ram_base_addr[1].clone() * BaseField::from(1 << 8) + - value_a[0].clone() + - value_a[1].clone() * BaseField::from(1 << 8) + - value_c[0].clone() + - value_c[1].clone() * BaseField::from(1 << 8) + + carry_flag[0].clone() * BaseField::from(1 << 16)), + ); + // is_store * (ram_base_addr_3 + ram_base_addr_4 * 256 - carry_1 - value_a_3 - value_a_4 * 256 - value_c_3 - value_c_4 * 256 + carry_2 * 2^{16}) = 0 + eval.add_constraint( + is_store.clone() + * (ram_base_addr[2].clone() + ram_base_addr[3].clone() * BaseField::from(1 << 8) + - carry_flag[0].clone() + - value_a[2].clone() + - value_a[3].clone() * BaseField::from(1 << 8) + - value_c[2].clone() + - value_c[3].clone() * BaseField::from(1 << 8) + + carry_flag[1].clone() * BaseField::from(1 << 16)), + ); + + let [ram1_val_prev] = trace_eval!(trace_eval, Ram1ValPrev); + let [ram2_val_prev] = trace_eval!(trace_eval, Ram2ValPrev); + let [ram1_val_cur] = trace_eval!(trace_eval, Ram1ValCur); + let [ram2_val_cur] = trace_eval!(trace_eval, Ram2ValCur); + // In case of load instruction, the previous and the current values should be the same + // is_load * (ram1_val_prev + ram2_val_prev * 256 - ram1_val_cur - ram2_val_cur * 256) = 0 + eval.add_constraint( + is_load.clone() + * (ram1_val_prev.clone() + ram2_val_prev.clone() * BaseField::from(1 << 8) + - ram1_val_cur.clone() + - ram2_val_cur.clone() * BaseField::from(1 << 8)), + ); + let [ram3_val_prev] = trace_eval!(trace_eval, Ram3ValPrev); + let [ram4_val_prev] = trace_eval!(trace_eval, Ram4ValPrev); + let [ram3_val_cur] = trace_eval!(trace_eval, Ram3ValCur); + let [ram4_val_cur] = trace_eval!(trace_eval, Ram4ValCur); + // is_load * (ram3_val_prev + ram4_val_prev * 256 - ram3_val_cur - ram4_val_cur * 256) = 0 + eval.add_constraint( + is_load.clone() + * (ram3_val_prev.clone() + ram4_val_prev.clone() * BaseField::from(1 << 8) + - ram3_val_cur.clone() + - ram4_val_cur.clone() * BaseField::from(1 << 8)), + ); + + // In case of LW instruction, ValueA should be equal to the loaded values in Ram{1,2,3,4}ValPrev + let [is_lw] = trace_eval!(trace_eval, IsLw); + // is_lw * (value_a_1 + value_a_2 * 256 - ram1_val_prev + ram2_val_prev * 256) = 0 + eval.add_constraint( + is_lw.clone() + * (value_a[0].clone() + value_a[1].clone() * BaseField::from(1 << 8) + - ram1_val_prev.clone() + - ram2_val_prev.clone() * BaseField::from(1 << 8)), + ); + // is_lw * (value_a_3 + value_a_4 * 256 - ram3_val_prev + ram4_val_prev * 256) = 0 + eval.add_constraint( + is_lw.clone() + * (value_a[2].clone() + value_a[3].clone() * BaseField::from(1 << 8) + - ram3_val_prev + - ram4_val_prev * BaseField::from(1 << 8)), + ); + + // In case of LHU instruction, ValueA[0..=1] should be equal to the loaded values in Ram{1,2}ValPrev + let [is_lhu] = trace_eval!(trace_eval, IsLhu); + // is_lhu * (value_a_1 + value_a_2 * 256 - ram1_val_prev + ram2_val_prev * 256) = 0 + eval.add_constraint( + is_lhu.clone() + * (value_a[0].clone() + value_a[1].clone() * BaseField::from(1 << 8) + - ram1_val_prev.clone() + - ram2_val_prev.clone() * BaseField::from(1 << 8)), + ); + // is_lhu * (value_a_3 + value_a_4 * 256) = 0 + eval.add_constraint( + is_lhu.clone() * (value_a[2].clone() + value_a[3].clone() * BaseField::from(1 << 8)), + ); + + // In case of LH instruction, Ram2ValPrev & 0x7f should be stored in QtAux + // The sign bit of Ram2ValPrev should be (Ram2ValPrev - QtAux) / 128 + let inv_128 = BaseField::from(128).inverse(); + let [is_lh] = trace_eval!(trace_eval, IsLh); + let [sign_removed] = trace_eval!(trace_eval, Column::QtAux); + let sign_bit = (ram2_val_prev.clone() - sign_removed.clone()) * inv_128; + // The sign bit should be zero or one. + // is_lh * sign_bit * (sign_bit - 1) = 0 + eval.add_constraint(is_lh.clone() * sign_bit.clone() * (sign_bit.clone() - E::F::one())); + // is_lh * (value_a_1 + value_a_2 * 256 - ram1_val_prev + ram2_val_prev * 256) = 0 + eval.add_constraint( + is_lh.clone() + * (value_a[0].clone() + value_a[1].clone() * BaseField::from(1 << 8) + - ram1_val_prev.clone() + - ram2_val_prev.clone() * BaseField::from(1 << 8)), + ); + // is_lh * (value_a_3 + value_a_4 * 256 - sign_bit * (2^16 - 1)) = 0 + eval.add_constraint( + is_lh.clone() + * (value_a[2].clone() + value_a[3].clone() * BaseField::from(1 << 8) + - sign_bit.clone() * (E::F::from(BaseField::from(1 << 16)) - E::F::one())), + ); + + // In case of LBU instruction ValueA[0] should be equal to the loaded values in Ram1ValPrev + let [is_lbu] = trace_eval!(trace_eval, IsLbu); + // is_lbu * (value_a_1 + value_a_2 * 256 - ram1_val_prev) = 0 // No ram2_val_prev + eval.add_constraint( + is_lbu.clone() + * (value_a[0].clone() + value_a[1].clone() * BaseField::from(1 << 8) + - ram1_val_prev.clone()), + ); + // is_lbu * (value_a_3 + value_a_4 * 256) = 0 + eval.add_constraint( + is_lbu.clone() * (value_a[2].clone() + value_a[3].clone() * BaseField::from(1 << 8)), + ); + + // In case of LB instruction, Ram1ValPrev & 0x7f should be stored in QtAux + // The sign bit of Ram1ValPrev should be (Ram1ValPrev - QtAux) / 128 + let [is_lb] = trace_eval!(trace_eval, IsLb); + let [sign_removed] = trace_eval!(trace_eval, Column::QtAux); + let sign_bit = (ram1_val_prev.clone() - sign_removed.clone()) * inv_128; + // The sign bit should be zero or one. + // is_lb * sign_bit * (sign_bit - 1) = 0 + eval.add_constraint(is_lb.clone() * sign_bit.clone() * (sign_bit.clone() - E::F::one())); + // is_lb * (value_a_1 + value_a_2 * 256 - ram1_val_prev - sign_bit * 127 * 128) = 0 + eval.add_constraint( + is_lb.clone() + * (value_a[0].clone() + value_a[1].clone() * BaseField::from(1 << 8) + - ram1_val_prev.clone() + - sign_bit.clone() + * E::F::from(BaseField::from(255) * BaseField::from(1 << 8))), + ); + // is_lb * (value_a_3 + value_a_4 * 256 - sign_bit * (2^16 - 1)) = 0 + eval.add_constraint( + is_lb.clone() + * (value_a[2].clone() + value_a[3].clone() * BaseField::from(1 << 8) + - sign_bit.clone() * (E::F::from(BaseField::from(1 << 16)) - E::F::one())), + ); + let lookup_elements: &LoadStoreLookupElements = lookup_elements.as_ref(); Self::constrain_add_initial_values(eval, trace_eval, lookup_elements); @@ -416,6 +597,7 @@ impl LoadStoreChip { add_with_carries(value_a, offset) }; traces.fill_columns(row_idx, ram_base_address, Column::RamBaseAddr); + let carry_bits = [carry_bits[1], carry_bits[3]]; traces.fill_columns(row_idx, carry_bits, Column::CarryFlag); let clk = row_idx as u32 + 1; for memory_record in vm_step.step.memory_records.iter() { @@ -453,12 +635,22 @@ impl LoadStoreChip { match memory_record.get_size() { MemAccessSize::Byte => { assert_eq!(cur_value_extended & 0xff, memory_record.get_value() & 0xff); + traces.fill_columns( + row_idx, + (cur_value_extended & 0x7f) as u8, + Column::QtAux, + ); } MemAccessSize::HalfWord => { assert_eq!( cur_value_extended & 0xffff, memory_record.get_value() & 0xffff ); + traces.fill_columns( + row_idx, + ((cur_value_extended >> 8) & 0x7f) as u8, + Column::QtAux, + ); } MemAccessSize::Word => { assert_eq!(cur_value_extended, memory_record.get_value()); diff --git a/prover/src/chips/instructions/slt.rs b/prover/src/chips/instructions/slt.rs index 413441a88..aabd5439a 100644 --- a/prover/src/chips/instructions/slt.rs +++ b/prover/src/chips/instructions/slt.rs @@ -1,5 +1,5 @@ -use num_traits::{One, Zero}; -use stwo_prover::constraint_framework::EvalAtRow; +use num_traits::One; +use stwo_prover::{constraint_framework::EvalAtRow, core::fields::FieldExpOps}; use nexus_vm::{riscv::BuiltinOpcode, WORD_SIZE}; @@ -10,13 +10,13 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; pub struct ExecutionResult { - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // for 16-bit boundaries pub diff_bytes: Word, pub result: Word, } @@ -37,7 +37,7 @@ impl ExecuteChip for SltChip { let sgn_c = program_step.get_sgn_c(); let result = match (sgn_b, sgn_c) { - (false, false) | (true, true) => [borrow_bits[3] as u8, 0, 0, 0], + (false, false) | (true, true) => [borrow_bits[1] as u8, 0, 0, 0], (false, true) => [0, 0, 0, 0], (true, false) => [1, 0, 0, 0], }; @@ -123,21 +123,26 @@ impl MachineChip for SltChip { let helper2_val = trace_eval!(trace_eval, Helper2); let helper3_val = trace_eval!(trace_eval, Helper3); - for i in 0..WORD_SIZE { - let prev_borrow = i - .checked_sub(1) - .map(|j| borrow_flag[j].clone()) - .unwrap_or(E::F::zero()); - - // SLT a, b, c - // h_1[i] - borrow[i] * 2^8 = rs1val[i] - rs2val[i] - borrow[i - 1] - eval.add_constraint( - is_slt.clone() - * (helper1_val[i].clone() - - borrow_flag[i].clone() * modulus.clone() - - (value_b[i].clone() - value_c[i].clone() - prev_borrow)), - ); - } + // h_1[0] + h_1[1] * 256 - borrow[0] * 2^{16} = rs1val[0] + rs1val[1] * 256 - rs2val[i] - rs2val[1] * 256 + eval.add_constraint( + is_slt.clone() + * (helper1_val[0].clone() + helper1_val[1].clone() * modulus.clone() + - borrow_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())), + ); + + // h_1[2] + h_1[3] * 256 - borrow[1] * 2^{16} = rs1val[2] + rs1val[3] * 256 - rs2val[2] - rs2val[3] * 256 - borrow[0] + eval.add_constraint( + is_slt.clone() + * (helper1_val[2].clone() + helper1_val[3].clone() * modulus.clone() + - borrow_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() + - borrow_flag[0].clone())), + ); // Computing a_val from sltu_flag (borrow_flag[3]) and sign bits sgnb and sgnc // is_slt・ (sgnb・(1-sgnc) + ltu_flag・(sgnb・sgnc+(1-sgnb)・(1-sgnc)) - a_val_1) =0 @@ -149,7 +154,7 @@ impl MachineChip for SltChip { eval.add_constraint( is_slt.clone() * (sgn_b[0].clone() * (E::F::one() - sgn_c[0].clone()) - + borrow_flag[3].clone() + + borrow_flag[1].clone() * (sgn_b[0].clone() * sgn_c[0].clone() + (E::F::one() - sgn_b[0].clone()) * (E::F::one() - sgn_c[0].clone())) diff --git a/prover/src/chips/instructions/sltu.rs b/prover/src/chips/instructions/sltu.rs index feb8e624f..246a5cfa1 100644 --- a/prover/src/chips/instructions/sltu.rs +++ b/prover/src/chips/instructions/sltu.rs @@ -1,7 +1,6 @@ -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}; +use nexus_vm::riscv::BuiltinOpcode; use crate::{ chips::SubChip, @@ -10,13 +9,13 @@ use crate::{ trace::{ eval::{trace_eval, TraceEval}, sidenote::SideNote, - BoolWord, ProgramStep, TracesBuilder, Word, + ProgramStep, TracesBuilder, Word, }, traits::{ExecuteChip, MachineChip}, }; pub struct ExecutionResult { - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // for 16-bit boundaries pub diff_bytes: Word, pub result: Word, } @@ -31,7 +30,7 @@ impl ExecuteChip for SltuChip { borrow_bits, diff_bytes, } = SubChip::execute(program_step); - let result = [borrow_bits[3] as u8, 0, 0, 0]; + let result = [borrow_bits[1] as u8, 0, 0, 0]; ExecutionResult { borrow_bits, diff_bytes, @@ -89,30 +88,36 @@ impl MachineChip for SltuChip { let value_a = trace_eval!(trace_eval, ValueA); let helper1_val = trace_eval!(trace_eval, Helper1); - // Assert boorrow_flag[3] is equal to value_a[0]. + // Assert boorrow_flag[1] is equal to value_a[0]. // So the last iteration of the loop below match - // is_sltu・(b_val_4 - c_val_4 - h1_4 + a_val_1・2^8 - borrow_3) = 0 - eval.add_constraint(is_sltu.clone() * (borrow_flag[3].clone() - value_a[0].clone())); - - for i in 0..WORD_SIZE { - let borrow = i - .checked_sub(1) - .map(|j| borrow_flag[j].clone()) - .unwrap_or(E::F::zero()); - - // SLTU a, b, c - // h_1[i] - h1[i] * 2^8 = rs1val[i] - rs2val[i] - borrow[i - 1] - eval.add_constraint( - is_sltu.clone() - * (helper1_val[i].clone() - - borrow_flag[i].clone() * modulus.clone() - - (value_b[i].clone() - value_c[i].clone() - borrow)), - ); + // is_sltu・(b_val_4 - c_val_4 - h1_4 + a_val_1・2^8 - borrow_1) = 0 + eval.add_constraint(is_sltu.clone() * (borrow_flag[1].clone() - value_a[0].clone())); + + // h_1[0] + h_1[1] * 256 - borrow[0] * 2^{16} = rs1val[0] + rs1val[1] * 256 - rs2val[0] - rs2val[1] * 256 + eval.add_constraint( + is_sltu.clone() + * (helper1_val[0].clone() + helper1_val[1].clone() * modulus.clone() + - borrow_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())), + ); + // h_1[2] + h_1[3] * 256 - borrow[1] * 2^{16} = rs1val[2] + rs1val[3] * 256 - rs2val[2] - rs2val[3] * 256 - borrow[0] + eval.add_constraint( + is_sltu.clone() + * (helper1_val[2].clone() + helper1_val[3].clone() * modulus.clone() + - borrow_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() + - borrow_flag[0].clone())), + ); + for (i, value_a_byte) in value_a.iter().enumerate() { // value_a[0] is constrained to be equal to the borrow flag, which is in {0, 1}. // Constraint value_a[1..=3] to equal 0. if i != 0 { - eval.add_constraint(is_sltu.clone() * value_a[i].clone()); + eval.add_constraint(is_sltu.clone() * value_a_byte.clone()); } } } diff --git a/prover/src/chips/instructions/sub.rs b/prover/src/chips/instructions/sub.rs index 5dc9536e2..cb049455a 100644 --- a/prover/src/chips/instructions/sub.rs +++ b/prover/src/chips/instructions/sub.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 SubChip; pub struct ExecutionResult { - pub borrow_bits: BoolWord, + pub borrow_bits: [bool; 2], // for 16-bit boundaries pub diff_bytes: Word, } @@ -55,6 +54,8 @@ impl ExecuteChip for SubChip { let (diff_bytes, borrow_bits) = subtract_with_borrow(value_b, value_c); + let borrow_bits = [borrow_bits[1], borrow_bits[3]]; + ExecutionResult { borrow_bits, diff_bytes, @@ -113,21 +114,26 @@ impl MachineChip for SubChip { let value_c = trace_eval!(trace_eval, ValueC); let value_a = trace_eval!(trace_eval, ValueA); - for i in 0..WORD_SIZE { - let borrow = i - .checked_sub(1) - .map(|j| borrow_flag[j].clone()) - .unwrap_or(E::F::zero()); - - // SUB a, b, c - // rdval[i] - h1[i] * 2^8 = rs1val[i] - rs2val[i] - h1[i - 1] - eval.add_constraint( - is_sub.clone() - * (value_a[i].clone() - - borrow_flag[i].clone() * modulus.clone() - - (value_b[i].clone() - value_c[i].clone() - borrow)), - ); - } + // rdval[0] + rdval[1] * 256 - h1[0] * 2^{16} = rs1val[0] + rs1val[1] * 256 - rs2val[0] - rs2val[1] * 256 + eval.add_constraint( + is_sub.clone() + * (value_a[0].clone() + value_a[1].clone() * modulus.clone() + - borrow_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[2] * 256 - h1[0] + eval.add_constraint( + is_sub.clone() + * (value_a[2].clone() + value_a[3].clone() * modulus.clone() + - borrow_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() + - borrow_flag[0].clone())), + ); } } diff --git a/prover/src/chips/memory_check/program_mem_check.rs b/prover/src/chips/memory_check/program_mem_check.rs index 8ce4beb24..6796e9f44 100644 --- a/prover/src/chips/memory_check/program_mem_check.rs +++ b/prover/src/chips/memory_check/program_mem_check.rs @@ -87,11 +87,11 @@ impl MachineChip for ProgramMemCheckChip { // Use accessed_program_memory sidenote to fill in the final program memory contents if row_idx == traces.num_rows() - 1 { for (pc, counter) in side_note.program_mem_check.last_access_counter.iter() { - let traget_row_idx = side_note + let target_row_idx = side_note .program_mem_check .find_row_idx(*pc) .expect("Pc not found in program trace"); - traces.fill_columns(traget_row_idx, *counter, Column::FinalPrgMemoryCtr); + traces.fill_columns(target_row_idx, *counter, Column::FinalPrgMemoryCtr); } } } @@ -140,7 +140,7 @@ impl MachineChip for ProgramMemCheckChip { ); // subtract program memory access, previous counter reads - // For each access, a tuple of the form (address, instruction_as_word, previous_couter) is subtracted. + // For each access, a tuple of the form (address, instruction_as_word, previous_counter) is subtracted. Self::subtract_access(logup_trace_gen, original_traces, lookup_element); // add program memory access, new counter write backs @@ -182,7 +182,7 @@ impl MachineChip for ProgramMemCheckChip { + E::F::one())), ); - // prg_cur_ctr[2] + prg_cur_ctr[3] * 256 + prg_ctr_carry[1] * 2^{16} = prg_prev_ctr[2] + prg_prev_ctr[3] * 256 + prg_ctr_carry[1] + // prg_cur_ctr[2] + prg_cur_ctr[3] * 256 + prg_ctr_carry[1] * 2^{16} = prg_prev_ctr[2] + prg_prev_ctr[3] * 256 + prg_ctr_carry[0] eval.add_constraint( (E::F::one() - is_padding.clone()) * (prg_cur_ctr[2].clone() @@ -198,7 +198,7 @@ impl MachineChip for ProgramMemCheckChip { // Logup constraints // add initial digest - // For each used Pc, oen tuple (address, instruction_as_word, 0u32) is added. + // For each used Pc, one tuple (address, instruction_as_word, 0u32) is added. Self::constrain_add_initial_digest(eval, trace_eval, lookup_elements); // subtract final digest @@ -206,7 +206,7 @@ impl MachineChip for ProgramMemCheckChip { Self::constrain_subtract_final_digest(eval, trace_eval, lookup_elements); // subtract program memory access, previous counter reads - // For each access, one tuple (address, instruction_as_word, previous_couter) is subtracted. + // For each access, one tuple (address, instruction_as_word, previous_counter) is subtracted. Self::constrain_subtract_access(eval, trace_eval, lookup_elements); // add program memory access, new counter write backs @@ -219,6 +219,7 @@ impl ProgramMemCheckChip { /// Fills the interaction trace columns for adding the initial content of the program memory: /// * 1 / lookup_element.combine(tuple) is added for each instruction /// where tuples contain (the address, the whole word of the instruction, 0u32). + /// The address and the instruction word are stored in two halfwords in little endian. /// /// The initial content of the memory is located on rows where PrgMemoryFlag is 1. fn add_initial_digest( @@ -228,24 +229,27 @@ impl ProgramMemCheckChip { lookup_element: &ProgramCheckLookupElements, ) { let [prg_memory_flag] = program_traces.get_base_column(ProgramColumn::PrgMemoryFlag); - let prg_memory_pc = program_traces.get_base_column::(ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each + let prg_memory_pc = + program_traces.get_base_column::(ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each let prg_memory_word = - program_traces.get_base_column::(ProgramColumn::PrgMemoryWord); + program_traces.get_base_column::(ProgramColumn::PrgMemoryWord); // The counter is not used because initially the counters are zero. let mut logup_col_gen = logup_trace_gen.new_col(); // Add (Pc, prg_memory_word, 0u32) for vec_row in 0..(1 << (original_traces.log_size() - LOG_N_LANES)) { let mut tuple = vec![]; - for prg_memory_pc_byte in prg_memory_pc.iter() { - tuple.push(prg_memory_pc_byte.data[vec_row]); + for prg_memory_pc_halfword in prg_memory_pc.iter() { + tuple.push(prg_memory_pc_halfword.data[vec_row]); } - assert_eq!(tuple.len(), WORD_SIZE); - for prg_memory_byte in prg_memory_word.iter() { - tuple.push(prg_memory_byte.data[vec_row]); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for prg_memory_halfword in prg_memory_word.iter() { + tuple.push(prg_memory_halfword.data[vec_row]); } // Initial counter is zero tuple.extend_from_slice(&[PackedBaseField::zero(); WORD_SIZE]); - assert_eq!(tuple.len(), WORD_SIZE + WORD_SIZE + WORD_SIZE); + assert_eq!(tuple.len(), WORD_SIZE_HALVED + WORD_SIZE_HALVED + WORD_SIZE); let numerator = prg_memory_flag.data[vec_row]; logup_col_gen.write_frac( vec_row, @@ -265,21 +269,23 @@ impl ProgramMemCheckChip { lookup_elements: &ProgramCheckLookupElements, ) { let [prg_memory_flag] = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryFlag); + // Two limbs of 16 bits each let prg_memory_pc = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each let prg_memory_word = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryWord); // Add (Pc, prg_memory_word, 0u32) let mut tuple = vec![]; - for prg_memory_pc_byte in prg_memory_pc.into_iter() { - tuple.push(prg_memory_pc_byte); + for prg_memory_pc_halfword in prg_memory_pc.into_iter() { + tuple.push(prg_memory_pc_halfword); } - assert_eq!(tuple.len(), WORD_SIZE); - for prg_memory_byte in prg_memory_word.into_iter() { - tuple.push(prg_memory_byte); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for prg_memory_halfword in prg_memory_word.into_iter() { + tuple.push(prg_memory_halfword); } for _ in 0..WORD_SIZE { tuple.extend_from_slice(&[E::F::zero()]); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), WORD_SIZE_HALVED + WORD_SIZE_HALVED + WORD_SIZE); let numerator = prg_memory_flag; eval.add_to_relation(RelationEntry::new( @@ -292,6 +298,7 @@ impl ProgramMemCheckChip { /// For the final content of the program memory, subtract in the interaction trace: /// * 1 / lookup_element.combine(tuple) for each instruction /// where tuples contain (the address, the whole word of the instruction, final counter value). + /// The address and the instruction word are stored in two halfwords in little endian. /// /// The information about the final content of the program memory is located on rows with PrgMemoryFlag set to 1. /// Most columns are the same as the initial program memory content. @@ -303,27 +310,30 @@ impl ProgramMemCheckChip { lookup_element: &ProgramCheckLookupElements, ) { let [prg_memory_flag] = program_traces.get_base_column(ProgramColumn::PrgMemoryFlag); - let prg_memory_pc = program_traces.get_base_column::(ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each + let prg_memory_pc = + program_traces.get_base_column::(ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each let prg_memory_word = - program_traces.get_base_column::(ProgramColumn::PrgMemoryWord); + program_traces.get_base_column::(ProgramColumn::PrgMemoryWord); let prg_memory_ctr = original_traces.get_base_column::(Column::FinalPrgMemoryCtr); let mut logup_col_gen = logup_trace_gen.new_col(); // Subtract (Pc, prg_memory_word, 0u32) for vec_row in 0..(1 << (original_traces.log_size() - LOG_N_LANES)) { let mut tuple = vec![]; - for prg_memory_pc_byte in prg_memory_pc.iter() { - tuple.push(prg_memory_pc_byte.data[vec_row]); + for prg_memory_pc_halfword in prg_memory_pc.into_iter() { + tuple.push(prg_memory_pc_halfword.data[vec_row]); } - assert_eq!(tuple.len(), WORD_SIZE); - for prg_memory_byte in prg_memory_word.iter() { - tuple.push(prg_memory_byte.data[vec_row]); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for prg_memory_halfword in prg_memory_word.into_iter() { + tuple.push(prg_memory_halfword.data[vec_row]); } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_memory_ctr_byte in prg_memory_ctr.iter() { tuple.push(prg_memory_ctr_byte.data[vec_row]); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = prg_memory_flag.data[vec_row]; logup_col_gen.write_frac( vec_row, @@ -343,22 +353,24 @@ impl ProgramMemCheckChip { lookup_elements: &ProgramCheckLookupElements, ) { let [prg_memory_flag] = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryFlag); + // Two limbs of 16 bits each let prg_memory_pc = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryPc); + // Two limbs of 16 bits each let prg_memory_word = program_trace_eval!(trace_eval, ProgramColumn::PrgMemoryWord); let prg_memory_ctr = trace_eval!(trace_eval, Column::FinalPrgMemoryCtr); let mut tuple = vec![]; - for prg_memory_pc_byte in prg_memory_pc.into_iter() { - tuple.push(prg_memory_pc_byte); + for prg_memory_pc_halfword in prg_memory_pc.into_iter() { + tuple.push(prg_memory_pc_halfword); } - assert_eq!(tuple.len(), WORD_SIZE); - for prg_memory_byte in prg_memory_word.into_iter() { - tuple.push(prg_memory_byte); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for prg_memory_halfword in prg_memory_word.into_iter() { + tuple.push(prg_memory_halfword) } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_memory_ctr_byte in prg_memory_ctr.into_iter() { tuple.push(prg_memory_ctr_byte); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = prg_memory_flag; eval.add_to_relation(RelationEntry::new( lookup_elements, @@ -370,6 +382,7 @@ impl ProgramMemCheckChip { /// On each program memory access: /// * 1 / lookup_element.combine(tuple_old) is subtracted /// where tuples contain (the address, the whole word of the instruction, previous counter value). + /// The address and the instruction word are stored in two halfwords in little endian. /// /// The numerator is zero on the padding rows, so that the row doesn't contribute to the logup sum. fn subtract_access( @@ -382,20 +395,23 @@ impl ProgramMemCheckChip { let pc = original_traces.get_base_column::(Column::Pc); let instruction_word = original_traces.get_base_column::(Column::InstrVal); let mut logup_col_gen = logup_trace_gen.new_col(); + let modulo = PackedBaseField::from(BaseField::from(1u32 << 8)); for vec_row in 0..(1 << (original_traces.log_size() - LOG_N_LANES)) { let mut tuple = vec![]; - for pc_byte in pc.iter() { - tuple.push(pc_byte.data[vec_row]); + for pc_byte in pc.chunks(2) { + tuple.push(pc_byte[0].data[vec_row] + pc_byte[1].data[vec_row] * modulo); } - assert_eq!(tuple.len(), WORD_SIZE); - for instruction_byte in instruction_word.iter() { - tuple.push(instruction_byte.data[vec_row]); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for instruction_byte in instruction_word.chunks(2) { + tuple.push( + instruction_byte[0].data[vec_row] + instruction_byte[1].data[vec_row] * modulo, + ); } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_prev_ctr_byte in prg_prev_ctr.iter() { tuple.push(prg_prev_ctr_byte.data[vec_row]); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = PackedBaseField::one() - is_padding.data[vec_row]; logup_col_gen.write_frac( vec_row, @@ -419,18 +435,19 @@ impl ProgramMemCheckChip { let pc = trace_eval!(trace_eval, Column::Pc); let instruction_word = trace_eval!(trace_eval, Column::InstrVal); let mut tuple = vec![]; - for pc_byte in pc.into_iter() { - tuple.push(pc_byte); + let modulo = E::F::from((1u32 << 8).into()); + for pc_byte in pc.chunks(2) { + tuple.push(pc_byte[0].clone() + pc_byte[1].clone() * modulo.clone()); } - assert_eq!(tuple.len(), WORD_SIZE); - for instruction_byte in instruction_word.into_iter() { - tuple.push(instruction_byte); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for instruction_byte in instruction_word.chunks(2) { + tuple.push(instruction_byte[0].clone() + instruction_byte[1].clone() * modulo.clone()); } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_prev_ctr_byte in prg_prev_ctr.into_iter() { tuple.push(prg_prev_ctr_byte); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = E::F::one() - is_padding; eval.add_to_relation(RelationEntry::new( @@ -456,20 +473,23 @@ impl ProgramMemCheckChip { let pc = original_traces.get_base_column::(Column::Pc); let instruction_word = original_traces.get_base_column::(Column::InstrVal); let mut logup_col_gen = logup_trace_gen.new_col(); + let modulo = PackedBaseField::from(BaseField::from(1u32 << 8)); for vec_row in 0..(1 << (original_traces.log_size() - LOG_N_LANES)) { let mut tuple = vec![]; - for pc_byte in pc.iter() { - tuple.push(pc_byte.data[vec_row]); + for pc_byte in pc.chunks(2) { + tuple.push(pc_byte[0].data[vec_row] + pc_byte[1].data[vec_row] * modulo); } - assert_eq!(tuple.len(), WORD_SIZE); - for instruction_byte in instruction_word.iter() { - tuple.push(instruction_byte.data[vec_row]); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for instruction_byte in instruction_word.chunks(2) { + tuple.push( + instruction_byte[0].data[vec_row] + instruction_byte[1].data[vec_row] * modulo, + ); } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_prev_ctr_byte in prg_cur_ctr.iter() { tuple.push(prg_prev_ctr_byte.data[vec_row]); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = PackedBaseField::one() - is_padding.data[vec_row]; logup_col_gen.write_frac( vec_row, @@ -492,19 +512,20 @@ impl ProgramMemCheckChip { let prg_cur_ctr = trace_eval!(trace_eval, Column::ProgCtrCur); let pc = trace_eval!(trace_eval, Column::Pc); let instruction_word = trace_eval!(trace_eval, Column::InstrVal); + let modulo = E::F::from((1u32 << 8).into()); let mut tuple = vec![]; - for pc_byte in pc.into_iter() { - tuple.push(pc_byte); + for pc_byte in pc.chunks(2) { + tuple.push(pc_byte[0].clone() + pc_byte[1].clone() * modulo.clone()); } - assert_eq!(tuple.len(), WORD_SIZE); - for instruction_byte in instruction_word.into_iter() { - tuple.push(instruction_byte); + assert_eq!(tuple.len(), WORD_SIZE_HALVED); + for instruction_byte in instruction_word.chunks(2) { + tuple.push(instruction_byte[0].clone() + instruction_byte[1].clone() * modulo.clone()); } - assert_eq!(tuple.len(), 2 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED); for prg_prev_ctr_byte in prg_cur_ctr.into_iter() { tuple.push(prg_prev_ctr_byte); } - assert_eq!(tuple.len(), 3 * WORD_SIZE); + assert_eq!(tuple.len(), 2 * WORD_SIZE_HALVED + WORD_SIZE); let numerator = E::F::one() - is_padding; eval.add_to_relation(RelationEntry::new( lookup_elements, diff --git a/prover/src/chips/range_check/range128.rs b/prover/src/chips/range_check/range128.rs index 8302c9881..98fe9b335 100644 --- a/prover/src/chips/range_check/range128.rs +++ b/prover/src/chips/range_check/range128.rs @@ -64,6 +64,10 @@ impl MachineChip for Range128Chip { let [is_sra] = traces.column(row_idx, Column::IsSra); let [h2_sra, _, _, _] = traces.column(row_idx, Helper2); fill_main_col(h2_sra, is_sra, side_note); + let [is_lh] = traces.column(row_idx, Column::IsLh); + fill_main_col(qt_aux, is_lh, side_note); + let [is_lb] = traces.column(row_idx, Column::IsLb); + fill_main_col(qt_aux, is_lb, side_note); } /// Fills the whole interaction trace in one-go using SIMD in the stwo-usual way /// @@ -109,6 +113,15 @@ impl MachineChip for Range128Chip { logup_trace_gen, lookup_element, ); + let [is_lh] = original_traces.get_base_column(Column::IsLh); + let [is_lb] = original_traces.get_base_column(Column::IsLb); + check_col( + qt_aux, + &[is_lh, is_lb], + original_traces.log_size(), + logup_trace_gen, + lookup_element, + ); } fn add_constraints( @@ -141,7 +154,7 @@ impl MachineChip for Range128Chip { eval.add_to_relation(RelationEntry::new( lookup_elements, numerator.into(), - &[qt_aux], + &[qt_aux.clone()], )); let [is_sra] = trace_eval.column_eval(Column::IsSra); @@ -153,6 +166,16 @@ impl MachineChip for Range128Chip { numerator.into(), &[h2_sra], )); + + let [is_lh] = trace_eval.column_eval(Column::IsLh); + let [is_lb] = trace_eval.column_eval(Column::IsLb); + let numerator = is_lh.clone() + is_lb.clone(); + + eval.add_to_relation(RelationEntry::new( + lookup_elements, + numerator.into(), + &[qt_aux], + )); } } diff --git a/prover/src/chips/range_check/range_bool.rs b/prover/src/chips/range_check/range_bool.rs index 86043432b..f63f0d3a5 100644 --- a/prover/src/chips/range_check/range_bool.rs +++ b/prover/src/chips/range_check/range_bool.rs @@ -16,7 +16,6 @@ use crate::{ trace::{eval::TraceEval, sidenote::SideNote, ProgramStep, TracesBuilder}, traits::MachineChip, virtual_column::{self, VirtualColumn}, - WORD_SIZE, }; /// A Chip for range-checking values for {0, 1} @@ -74,8 +73,15 @@ const CHECKED_SINGLE: [Column; 48] = [ ShiftBit5, RamInitFinalFlag, ]; -const CHECKED_WORD: [Column; 2] = [CarryFlag, BorrowFlag]; -const CHECKED_HALF_WORD: [Column; 5] = [PcCarry, CH1Minus, CH2Minus, CH3Minus, ProgCtrCarry]; +const CHECKED_HALF_WORD: [Column; 7] = [ + CarryFlag, + PcCarry, + CH1Minus, + CH2Minus, + CH3Minus, + ProgCtrCarry, + BorrowFlag, +]; const TYPE_R_CHECKED_SINGLE: [Column; 3] = [OpC4, OpA0, OpB0]; const TYPE_I_NO_SHIFT_SINGLE: [Column; 3] = [OpC11, OpA0, OpB0]; const TYPE_I_SHIFT_SINGLE: [Column; 3] = [OpC4, OpA0, OpB0]; @@ -145,13 +151,6 @@ impl MachineChip for RangeBoolChip { let [col] = trace_eval.column_eval(col); eval.add_constraint(is_type_s.clone() * col.clone() * (col - E::F::one())); } - - for col_word in CHECKED_WORD.into_iter() { - let col_word = trace_eval.column_eval::(col_word); - for limb in col_word.into_iter() { - eval.add_constraint(limb.clone() * (limb - E::F::one())); - } - } } } @@ -168,7 +167,7 @@ mod test { use crate::traits::MachineChip; use nexus_vm::emulator::{Emulator, HarvardEmulator}; - use nexus_vm::WORD_SIZE; + use stwo_prover::constraint_framework::TraceLocationAllocator; use stwo_prover::core::prover::prove; @@ -187,10 +186,6 @@ mod test { for col in CHECKED_SINGLE.into_iter() { traces.fill_columns(row_idx, b, col); } - for word in CHECKED_WORD.into_iter() { - let b_word = [b; WORD_SIZE]; - traces.fill_columns(row_idx, b_word, word); - } RangeBoolChip::fill_main_trace( &mut traces, @@ -216,10 +211,6 @@ mod test { for col in CHECKED_SINGLE.into_iter() { traces.fill_columns(row_idx, b, col); } - for word in CHECKED_WORD.into_iter() { - let b_word = [b; WORD_SIZE]; - traces.fill_columns(row_idx, b_word, word); - } RangeBoolChip::fill_main_trace( &mut traces, diff --git a/prover/src/column.rs b/prover/src/column.rs index 7eaaf6046..17fa67cb3 100644 --- a/prover/src/column.rs +++ b/prover/src/column.rs @@ -41,12 +41,11 @@ pub enum Column { /// The register-index or the immediate value of the third operand of the instruction. Immediate values are zero-extended out of the effective bits. #[size = 1] OpC, - - /// Additional columns for carrying limbs. - #[size = 4] + /// Columns for carry flags at 16-bit boundaries. + #[size = 2] CarryFlag, - /// Subtraction columns for borrow limbs. - #[size = 4] + /// Columns for borrow flags at 16-bit boundaries. + #[size = 2] BorrowFlag, /// Is operand op_c an immediate value? #[size = 1] @@ -494,11 +493,11 @@ pub enum Column { #[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, ColumnsEnum)] #[column_derive(string_id)] pub enum ProgramColumn { - /// Program memory content: every Pc in the program memory - #[size = 4] + /// Program memory content: every Pc in the program memory, stored in two 16-bit limbs + #[size = 2] PrgMemoryPc, - /// Program memory content: Instruction word at PrgMemoryPc - #[size = 4] + /// Program memory content: Instruction word at PrgMemoryPc, stored in two 16-bit limbs + #[size = 2] PrgMemoryWord, /// Program memory content: 1 means the row contains real PrgMemory*. 0 otherwise. #[size = 1] diff --git a/prover/src/machine.rs b/prover/src/machine.rs index df39e64bd..08d747707 100644 --- a/prover/src/machine.rs +++ b/prover/src/machine.rs @@ -126,11 +126,9 @@ impl Machine { ) -> Result { let num_steps = trace.get_num_steps(); let program_len = view.get_program_memory().program.len(); - let memory_len = view.get_initial_memory().len() - + view.get_exit_code().len() - + view.get_public_output().len(); + let tracked_ram_size = view.view_tracked_ram_size(); - let log_size = Self::max_log_size(&[num_steps, program_len, memory_len]) + let log_size = Self::max_log_size(&[num_steps, program_len, tracked_ram_size]) .max(PreprocessedTraces::MIN_LOG_SIZE); let extensions_iter = BASE_EXTENSIONS.iter().chain(extensions); diff --git a/prover/src/trace/program_trace.rs b/prover/src/trace/program_trace.rs index 3a518e181..2e26f873f 100644 --- a/prover/src/trace/program_trace.rs +++ b/prover/src/trace/program_trace.rs @@ -70,8 +70,19 @@ impl ProgramTracesBuilder { *pc as usize, "The program is assumed to be in contiguous memory." ); - ret.fill_program_columns(row_idx, *pc, ProgramColumn::PrgMemoryPc); - ret.fill_program_columns(row_idx, *instruction_word, ProgramColumn::PrgMemoryWord); + let (pc_low, pc_high) = (*pc & 0xFFFF, *pc >> 16); + ret.fill_program_columns( + row_idx, + [pc_low, pc_high].map(BaseField::from), + ProgramColumn::PrgMemoryPc, + ); + let (instruction_low, instruction_high) = + (*instruction_word & 0xFFFF, *instruction_word >> 16); + ret.fill_program_columns( + row_idx, + [instruction_low, instruction_high].map(BaseField::from), + ProgramColumn::PrgMemoryWord, + ); ret.fill_program_columns(row_idx, true, ProgramColumn::PrgMemoryFlag); } diff --git a/prover/src/trace/utils.rs b/prover/src/trace/utils.rs index 87bb972c2..8adc7a9db 100644 --- a/prover/src/trace/utils.rs +++ b/prover/src/trace/utils.rs @@ -42,6 +42,12 @@ impl IntoBaseFields<{ N }> for [u8; N] { } } +impl IntoBaseFields for [BaseField; N] { + fn into_base_fields(self) -> [BaseField; N] { + self + } +} + impl IntoBaseFields<{ WORD_SIZE }> for WordWithEffectiveBits { fn into_base_fields(self) -> [BaseField; WORD_SIZE] { self.0.into_base_fields() diff --git a/sdk/Cargo.toml b/sdk/Cargo.toml index 0054ed7d6..5a230178c 100644 --- a/sdk/Cargo.toml +++ b/sdk/Cargo.toml @@ -12,6 +12,7 @@ categories = { workspace = true } [dependencies] serde.workspace = true +nexus-common = { path = "../common" } nexus-core = { path = "../core" } nexus-sdk-macros = { path = "./macros" } diff --git a/sdk/README.md b/sdk/README.md index a7981bbae..67b919679 100644 --- a/sdk/README.md +++ b/sdk/README.md @@ -17,7 +17,7 @@ $ rustup target add riscv32i-unknown-none-elf Then, install the Nexus zkVM: ```shell -$ rustup run nightly-2025-01-02 cargo install --git https://github.com/nexus-xyz/nexus-zkvm cargo-nexus --tag 'v0.3.0' +$ rustup run nightly-2025-01-02 cargo install --git https://github.com/nexus-xyz/nexus-zkvm cargo-nexus --tag 'v0.3.1' ``` And verify the installation: diff --git a/sdk/src/traits.rs b/sdk/src/traits.rs index f2d96bf20..e81817c5f 100644 --- a/sdk/src/traits.rs +++ b/sdk/src/traits.rs @@ -1,5 +1,6 @@ use crypto::digest::{Digest, OutputSizeUser}; use crypto_common::generic_array::{ArrayLength, GenericArray}; +use nexus_common::constants::WORD_SIZE; use serde::{de::DeserializeOwned, Serialize}; use std::path::Path; @@ -88,11 +89,15 @@ impl CheckedView for nexus_core::nvm::View { expected_public_output, ); + let static_memory_size = + (&expected_elf.rom_image.len() + &expected_elf.ram_image.len()) * WORD_SIZE; + Self::new( &Some(*memory_layout), &Vec::new(), &program_memory, &initial_memory, + memory_layout.tracked_ram_size(static_memory_size), &exit_code, &output_memory, &expected_ad.to_vec(), diff --git a/specification/zkvm-spec-3.0.pdf b/specification/zkvm-spec-3.0.pdf index ead5b4614..7a9753e7c 100644 Binary files a/specification/zkvm-spec-3.0.pdf and b/specification/zkvm-spec-3.0.pdf differ diff --git a/vm/src/emulator/executor.rs b/vm/src/emulator/executor.rs index a335e00ef..97a1e09cb 100644 --- a/vm/src/emulator/executor.rs +++ b/vm/src/emulator/executor.rs @@ -745,6 +745,12 @@ impl Emulator for HarvardEmulator { Vec::new() }; + let input_size = rom_iter.len() + self.static_ram_image.len() + public_input.len(); + let tracked_ram_size = self + .memory_stats + .get_tracked_ram_size(input_size as u32, output_memory.len() as u32) + as usize; + View { memory_layout: None, debug_logs, @@ -766,6 +772,7 @@ impl Emulator for HarvardEmulator { .chain(ram_iter) .chain(public_input) .collect(), + tracked_ram_size, exit_code, output_memory, associated_data: Vec::new(), @@ -1227,6 +1234,10 @@ impl Emulator for LinearEmulator { ) .unwrap_or_default(); + let tracked_ram_size = self + .memory_layout + .tracked_ram_size(self.initial_static_ram_image.len() + rom_initialization.len()); + View { memory_layout: Some(self.memory_layout), debug_logs, @@ -1256,6 +1267,7 @@ impl Emulator for LinearEmulator { .chain(ram_iter) .chain(public_input_iter) .collect(), + tracked_ram_size, exit_code, output_memory, associated_data, diff --git a/vm/src/emulator/layout.rs b/vm/src/emulator/layout.rs index b67e1bc47..bf1c8276f 100644 --- a/vm/src/emulator/layout.rs +++ b/vm/src/emulator/layout.rs @@ -294,4 +294,38 @@ impl LinearMemoryLayout { pub fn stack_top(&self) -> u32 { self.stack_top - WORD_SIZE as u32 } + + pub fn tracked_ram_size(&self, static_memory_size: usize) -> usize { + let stack_size: usize = + self.stack_top + .checked_sub(self.stack_bottom) + .expect("stack top should be above stack bottom") as usize; + let heap_size = self + .heap + .checked_sub(self.heap_start()) + .expect("heap should be above heap start") as usize; + let public_input_size = + self.public_input_end() + .checked_sub(self.public_input_start()) + .expect("public input end should be above public input start") as usize; + let public_output_size = self + .public_output_end() + .checked_sub(self.public_output_start()) + .expect("public output end should be above public output start") + as usize; + let exit_code_size = WORD_SIZE; + // program, registers, and ad are not under RAM checking. omitted. + let total = [ + static_memory_size, + stack_size, + heap_size, + public_input_size, + public_output_size, + exit_code_size, + ] + .iter() + .try_fold(0usize, |acc, &val| acc.checked_add(val)) + .expect("overflow"); + total + } } diff --git a/vm/src/emulator/memory_stats.rs b/vm/src/emulator/memory_stats.rs index 62a5869a1..ad049d5d6 100644 --- a/vm/src/emulator/memory_stats.rs +++ b/vm/src/emulator/memory_stats.rs @@ -115,6 +115,17 @@ impl MemoryStats { ad_size, ) } + + /// Returns the total number of addresses under RAM memory checking. + pub fn get_tracked_ram_size(&self, input_size: u32, output_size: u32) -> u32 { + let heap_size = self.max_heap_access - self.heap_bottom; + let stack_size = self.stack_top - self.min_stack_access; + let total = [heap_size, stack_size, input_size, output_size] + .iter() + .try_fold(0u32, |acc, &val| acc.checked_add(val)) + .expect("overflow"); + total + } } #[cfg(test)] diff --git a/vm/src/emulator/utils.rs b/vm/src/emulator/utils.rs index 4fa40974d..a333533d2 100644 --- a/vm/src/emulator/utils.rs +++ b/vm/src/emulator/utils.rs @@ -189,6 +189,8 @@ pub struct View { pub(crate) debug_logs: Vec>, pub(crate) program_memory: ProgramInfo, pub(crate) initial_memory: Vec, + /// The number of all addresses under RAM memory checking + pub(crate) tracked_ram_size: usize, pub(crate) exit_code: Vec, pub(crate) output_memory: Vec, // todo: incorporate into initial memory @@ -197,11 +199,13 @@ pub struct View { impl View { /// Construct a view out of its raw parts. + #[allow(clippy::too_many_arguments)] // extra thought needed what's the best approach to reduce args pub fn new( memory_layout: &Option, debug_logs: &Vec>, program_memory: &ProgramInfo, initial_memory: &Vec, + tracked_ram_size: usize, exit_code: &Vec, output_memory: &Vec, associated_data: &Vec, @@ -211,6 +215,7 @@ impl View { debug_logs: debug_logs.to_owned(), program_memory: program_memory.to_owned(), initial_memory: initial_memory.to_owned(), + tracked_ram_size, exit_code: exit_code.to_owned(), output_memory: output_memory.to_owned(), associated_data: associated_data.to_owned(), @@ -247,6 +252,11 @@ impl View { .map(|layout| io_entries_into_vec(layout.public_output_start(), &self.output_memory)) } + /// Return the number of all addresses under RAM memory checking. + pub fn view_tracked_ram_size(&self) -> usize { + self.tracked_ram_size + } + /// Return the raw bytes of the associated data, if any. pub fn view_associated_data(&self) -> Option> { if self.memory_layout.is_some() {