diff --git a/ceno_zkvm/src/chip_handler.rs b/ceno_zkvm/src/chip_handler.rs index 24c3e3647..e10ed4fed 100644 --- a/ceno_zkvm/src/chip_handler.rs +++ b/ceno_zkvm/src/chip_handler.rs @@ -24,18 +24,16 @@ pub trait RegisterChipOperations, N: FnOnce( prev_ts: Expression, ts: Expression, values: &V, - ) -> Result, ZKVMError>; + ) -> Result<(Expression, ExprLtConfig), ZKVMError>; #[allow(clippy::too_many_arguments)] fn register_write>>>( &mut self, name_fn: N, register_id: &WitIn, - prev_rs1_ts: Expression, - prev_rs2_ts: Expression, prev_ts: Expression, ts: Expression, prev_values: &V, values: &V, - ) -> Result<(Expression, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError>; + ) -> Result<(Expression, ExprLtConfig), ZKVMError>; } diff --git a/ceno_zkvm/src/chip_handler/register.rs b/ceno_zkvm/src/chip_handler/register.rs index 87b4f2eda..bdc978710 100644 --- a/ceno_zkvm/src/chip_handler/register.rs +++ b/ceno_zkvm/src/chip_handler/register.rs @@ -20,7 +20,7 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe prev_ts: Expression, ts: Expression, values: &V, - ) -> Result, ZKVMError> { + ) -> Result<(Expression, ExprLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = cb.rlc_chip_record( @@ -30,7 +30,7 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe ))], vec![register_id.expr()], values.expr(), - vec![prev_ts], + vec![prev_ts.clone()], ] .concat(), ); @@ -50,12 +50,11 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe cb.write_record(|| "write_record", write_record)?; // assert prev_ts < current_ts - // TODO implement lt gadget - // let is_lt = prev_ts.lt(self, ts)?; - // self.require_one(is_lt)?; + let lt_cfg = cb.less_than(|| "prev_ts < ts", prev_ts, ts.clone(), Some(true))?; + let next_ts = ts + 1.into(); - Ok(next_ts) + Ok((next_ts, lt_cfg)) }) } @@ -63,13 +62,11 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe &mut self, name_fn: N, register_id: &WitIn, - prev_rs1_ts: Expression, - prev_rs2_ts: Expression, prev_ts: Expression, ts: Expression, prev_values: &V, values: &V, - ) -> Result<(Expression, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError> { + ) -> Result<(Expression, ExprLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = cb.rlc_chip_record( @@ -98,16 +95,11 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe cb.read_record(|| "read_record", read_record)?; cb.write_record(|| "write_record", write_record)?; - let lt_rs1_cfg = - cb.less_than(|| "prev_rs1_ts < ts", prev_rs1_ts, ts.clone(), Some(true))?; - let lt_rs2_cfg = - cb.less_than(|| "prev_rs2_ts < ts", prev_rs2_ts, ts.clone(), Some(true))?; - let lt_prev_ts_cfg = - cb.less_than(|| "prev_rd_ts < ts", prev_ts, ts.clone(), Some(true))?; + let lt_cfg = cb.less_than(|| "prev_ts < ts", prev_ts, ts.clone(), Some(true))?; let next_ts = ts + 1.into(); - Ok((next_ts, lt_rs1_cfg, lt_rs2_cfg, lt_prev_ts_cfg)) + Ok((next_ts, lt_cfg)) }) } } diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs index 62e866d33..1be3ec599 100644 --- a/ceno_zkvm/src/instructions/riscv/addsub.rs +++ b/ceno_zkvm/src/instructions/riscv/addsub.rs @@ -103,21 +103,19 @@ fn add_sub_gadget( let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; - let ts = circuit_builder.register_read( + let (ts, lt_rs1_cfg) = circuit_builder.register_read( || "read_rs1", &rs1_id, prev_rs1_ts.expr(), cur_ts.expr(), &addend_0, )?; - let ts = + let (ts, lt_rs2_cfg) = circuit_builder.register_read(|| "read_rs2", &rs2_id, prev_rs2_ts.expr(), ts, &addend_1)?; - let (ts, lt_rs1_cfg, lt_rs2_cfg, lt_prev_ts_cfg) = circuit_builder.register_write( + let (ts, lt_prev_ts_cfg) = circuit_builder.register_write( || "write_rd", &rd_id, - prev_rs1_ts.expr(), - prev_rs2_ts.expr(), prev_rd_ts.expr(), ts, &prev_rd_value, @@ -193,18 +191,18 @@ impl Instruction for AddInstruction { set_val!(instance, config.prev_rd_ts, 2); ExprLtInput { - lhs: 2, // rs1 - rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 + lhs: 2, // rs1 + rhs: 3, // cur_ts } .assign(instance, &config.lt_rs1_cfg); ExprLtInput { - lhs: 2, // rs2 - rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 + lhs: 2, // rs2 + rhs: 4, // cur_ts } .assign(instance, &config.lt_rs2_cfg); ExprLtInput { - lhs: 2, // rd - rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 + lhs: 2, // rd + rhs: 5, // cur_ts } .assign(instance, &config.lt_prev_ts_cfg); diff --git a/ceno_zkvm/src/instructions/riscv/blt.rs b/ceno_zkvm/src/instructions/riscv/blt.rs index 3872ddd2c..b60f7db06 100644 --- a/ceno_zkvm/src/instructions/riscv/blt.rs +++ b/ceno_zkvm/src/instructions/riscv/blt.rs @@ -18,6 +18,7 @@ use crate::{ }; use super::{ + config::ExprLtConfig, constants::{OPType, OpcodeType, RegUInt, RegUInt8, PC_STEP_SIZE}, RIVInstruction, }; @@ -38,6 +39,8 @@ pub struct InstructionConfig { pub prev_rs1_ts: WitIn, pub prev_rs2_ts: WitIn, pub is_lt: UIntLtConfig, + pub lt_rs1_cfg: ExprLtConfig, + pub lt_rs2_cfg: ExprLtConfig, } pub struct BltInput { @@ -174,14 +177,14 @@ fn blt_gadget( let lhs = RegUInt::from_u8_limbs(circuit_builder, &lhs_limb8); let rhs = RegUInt::from_u8_limbs(circuit_builder, &rhs_limb8); - let ts = circuit_builder.register_read( + let (ts, lt_rs1_cfg) = circuit_builder.register_read( || "read ts for lhs", &rs1_id, prev_rs1_ts.expr(), cur_ts.expr(), &lhs, )?; - let ts = circuit_builder.register_read( + let (ts, lt_rs2_cfg) = circuit_builder.register_read( || "read ts for rhs", &rs2_id, prev_rs2_ts.expr(), @@ -207,6 +210,8 @@ fn blt_gadget( prev_rs1_ts, prev_rs2_ts, is_lt, + lt_rs1_cfg, + lt_rs2_cfg, }) }