From 1646da31769e23d989d4b72b56f7a481836e6dcd Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Thu, 8 Aug 2024 09:36:52 +0800 Subject: [PATCH] fix proper ts and pc counting --- ceno_zkvm/src/chip_handler.rs | 12 +++---- ceno_zkvm/src/chip_handler/register.rs | 30 +++++++++++----- ceno_zkvm/src/instructions/riscv/add.rs | 48 +++++++++++++------------ ceno_zkvm/src/instructions/riscv/mod.rs | 1 + 4 files changed, 54 insertions(+), 37 deletions(-) diff --git a/ceno_zkvm/src/chip_handler.rs b/ceno_zkvm/src/chip_handler.rs index aeff825d9..d0a43b870 100644 --- a/ceno_zkvm/src/chip_handler.rs +++ b/ceno_zkvm/src/chip_handler.rs @@ -30,17 +30,17 @@ pub trait RegisterChipOperations { fn register_read( &mut self, register_id: &WitIn, - prev_ts: &TSUInt, - ts: &TSUInt, + prev_ts: &mut TSUInt, + ts: &mut TSUInt, values: &UInt64, - ) -> Result<(), ZKVMError>; + ) -> Result; fn register_write( &mut self, register_id: &WitIn, - prev_ts: &TSUInt, - ts: &TSUInt, + prev_ts: &mut TSUInt, + ts: &mut TSUInt, prev_values: &UInt64, values: &UInt64, - ) -> Result<(), ZKVMError>; + ) -> Result; } diff --git a/ceno_zkvm/src/chip_handler/register.rs b/ceno_zkvm/src/chip_handler/register.rs index fa54f6d6f..16fae6629 100644 --- a/ceno_zkvm/src/chip_handler/register.rs +++ b/ceno_zkvm/src/chip_handler/register.rs @@ -2,7 +2,7 @@ use ff_ext::ExtensionField; use singer_utils::structs::RAMType; use crate::{ - circuit_builder::CircuitBuilder, + circuit_builder::{self, CircuitBuilder}, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, structs::{TSUInt, UInt64}, @@ -14,10 +14,10 @@ impl RegisterChipOperations for CircuitBuilder { fn register_read( &mut self, register_id: &WitIn, - prev_ts: &TSUInt, - ts: &TSUInt, + prev_ts: &mut TSUInt, + ts: &mut TSUInt, values: &UInt64, - ) -> Result<(), ZKVMError> { + ) -> Result { // READ (a, v, t) let read_record = self.rlc_chip_record( [ @@ -44,17 +44,23 @@ impl RegisterChipOperations for CircuitBuilder { ); self.read_record(read_record)?; self.write_record(write_record)?; - Ok(()) + + // assert prev_ts < current_ts + let is_lt = prev_ts.lt(self, ts)?; + self.require_one(is_lt)?; + let next_ts = ts.add_const(self, 1.into())?; + + Ok(next_ts) } fn register_write( &mut self, register_id: &WitIn, - prev_ts: &TSUInt, - ts: &TSUInt, + prev_ts: &mut TSUInt, + ts: &mut TSUInt, prev_values: &UInt64, values: &UInt64, - ) -> Result<(), ZKVMError> { + ) -> Result { // READ (a, v, t) let read_record = self.rlc_chip_record( [ @@ -81,6 +87,12 @@ impl RegisterChipOperations for CircuitBuilder { ); self.read_record(read_record)?; self.write_record(write_record)?; - Ok(()) + + // assert prev_ts < current_ts + let is_lt = prev_ts.lt(self, ts)?; + self.require_one(is_lt)?; + let next_ts = ts.add_const(self, 1.into())?; + + Ok(next_ts) } } diff --git a/ceno_zkvm/src/instructions/riscv/add.rs b/ceno_zkvm/src/instructions/riscv/add.rs index b402d7bb4..bb3ad79a4 100644 --- a/ceno_zkvm/src/instructions/riscv/add.rs +++ b/ceno_zkvm/src/instructions/riscv/add.rs @@ -13,6 +13,8 @@ use crate::{ structs::{PCUInt, TSUInt, UInt64}, }; +use super::constants::RISCV64_PC_STEP_SIZE; + pub struct AddInstruction; pub struct InstructionConfig { @@ -40,16 +42,13 @@ impl Instruction for AddInstruction { circuit_builder: &mut CircuitBuilder, ) -> Result, ZKVMError> { let pc = PCUInt::new(circuit_builder); - let memory_ts = TSUInt::new(circuit_builder); + let mut memory_ts = TSUInt::new(circuit_builder); let clk = circuit_builder.create_witin(); // state in circuit_builder.state_in(&pc, &memory_ts, clk.expr())?; - let next_pc = pc.add_const(circuit_builder, 1.into())?; - let next_memory_ts = memory_ts.add_const(circuit_builder, 1.into())?; - - circuit_builder.state_out(&next_pc, &next_memory_ts, clk.expr() + 1.into())?; + let next_pc = pc.add_const(circuit_builder, RISCV64_PC_STEP_SIZE.into())?; // Execution result = addend0 + addend1, with carry. let prev_rd_memory_value = UInt64::new(circuit_builder); @@ -60,38 +59,43 @@ impl Instruction for AddInstruction { let computed_outcome = addend_0.add(circuit_builder, &addend_1)?; outcome.eq(circuit_builder, &computed_outcome)?; - // TODO rs1_id, rs2_id, rd_id should be byte code lookup + // TODO rs1_id, rs2_id, rd_id should be bytecode lookup let rs1_id = circuit_builder.create_witin(); let rs2_id = circuit_builder.create_witin(); let rd_id = circuit_builder.create_witin(); circuit_builder.assert_u5(rs1_id.expr())?; circuit_builder.assert_u5(rs2_id.expr())?; circuit_builder.assert_u5(rd_id.expr())?; - let prev_rs1_memory_ts = TSUInt::new(circuit_builder); - let prev_rs2_memory_ts = TSUInt::new(circuit_builder); - let prev_rd_memory_ts = TSUInt::new(circuit_builder); - - let is_lt_0 = prev_rs1_memory_ts.lt(circuit_builder, &memory_ts)?; - let is_lt_1 = prev_rs2_memory_ts.lt(circuit_builder, &memory_ts)?; - let is_lt_2 = prev_rd_memory_ts.lt(circuit_builder, &memory_ts)?; - // less than = true - circuit_builder.require_one(is_lt_0)?; - circuit_builder.require_one(is_lt_1)?; - circuit_builder.require_one(is_lt_2)?; + let mut prev_rs1_memory_ts = TSUInt::new(circuit_builder); + let mut prev_rs2_memory_ts = TSUInt::new(circuit_builder); + let mut prev_rd_memory_ts = TSUInt::new(circuit_builder); - circuit_builder.register_read(&rs1_id, &prev_rs1_memory_ts, &memory_ts, &addend_0)?; + let mut memory_ts = circuit_builder.register_read( + &rs1_id, + &mut prev_rs1_memory_ts, + &mut memory_ts, + &addend_0, + )?; - circuit_builder.register_read(&rs2_id, &prev_rs2_memory_ts, &memory_ts, &addend_1)?; + let mut memory_ts = circuit_builder.register_read( + &rs2_id, + &mut prev_rs2_memory_ts, + &mut memory_ts, + &addend_1, + )?; - circuit_builder.register_write( + let memory_ts = circuit_builder.register_write( &rd_id, - &prev_rd_memory_ts, - &memory_ts, + &mut prev_rd_memory_ts, + &mut memory_ts, &prev_rd_memory_value, &computed_outcome, )?; + let next_memory_ts = memory_ts.add_const(circuit_builder, 1.into())?; + circuit_builder.state_out(&next_pc, &next_memory_ts, clk.expr() + 1.into())?; + Ok(InstructionConfig { pc, memory_ts, diff --git a/ceno_zkvm/src/instructions/riscv/mod.rs b/ceno_zkvm/src/instructions/riscv/mod.rs index cced7b48f..59189a19d 100644 --- a/ceno_zkvm/src/instructions/riscv/mod.rs +++ b/ceno_zkvm/src/instructions/riscv/mod.rs @@ -1 +1,2 @@ pub mod add; +mod constants;