From 7834bdacad597311f99c7b41eb096b68810b84e0 Mon Sep 17 00:00:00 2001 From: Soham Zemse <22412996+zemse@users.noreply.github.com> Date: Tue, 10 Sep 2024 13:19:43 +0530 Subject: [PATCH] rename LtConfig to UIntLtConfig and Lt2Config to ExprLtConfig --- ceno_zkvm/src/chip_handler.rs | 4 ++-- ceno_zkvm/src/chip_handler/general.rs | 6 ++--- ceno_zkvm/src/chip_handler/register.rs | 4 ++-- ceno_zkvm/src/instructions/riscv/addsub.rs | 16 ++++++------- ceno_zkvm/src/instructions/riscv/blt.rs | 6 ++--- ceno_zkvm/src/instructions/riscv/config.rs | 28 +++++++++++----------- ceno_zkvm/src/scheme/mock_prover.rs | 10 ++++---- ceno_zkvm/src/uint/arithmetic.rs | 10 ++++---- 8 files changed, 42 insertions(+), 42 deletions(-) diff --git a/ceno_zkvm/src/chip_handler.rs b/ceno_zkvm/src/chip_handler.rs index cdc0702d5..24c3e3647 100644 --- a/ceno_zkvm/src/chip_handler.rs +++ b/ceno_zkvm/src/chip_handler.rs @@ -3,7 +3,7 @@ use ff_ext::ExtensionField; use crate::{ error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::config::Lt2Config, + instructions::riscv::config::ExprLtConfig, }; pub mod general; @@ -37,5 +37,5 @@ pub trait RegisterChipOperations, N: FnOnce( ts: Expression, prev_values: &V, values: &V, - ) -> Result<(Expression, Lt2Config, Lt2Config, Lt2Config), ZKVMError>; + ) -> Result<(Expression, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError>; } diff --git a/ceno_zkvm/src/chip_handler/general.rs b/ceno_zkvm/src/chip_handler/general.rs index 3edb2ccf2..8ed114dae 100644 --- a/ceno_zkvm/src/chip_handler/general.rs +++ b/ceno_zkvm/src/chip_handler/general.rs @@ -8,7 +8,7 @@ use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, error::ZKVMError, expression::{Expression, Fixed, ToExpr, WitIn}, - instructions::riscv::config::Lt2Config, + instructions::riscv::config::ExprLtConfig, structs::ROMType, }; @@ -274,7 +274,7 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> { lhs: Expression, rhs: Expression, assert_less_than: Option, - ) -> Result + ) -> Result where NR: Into + Display + Clone, N: FnOnce() -> NR, @@ -328,7 +328,7 @@ impl<'a, E: ExtensionField> CircuitBuilder<'a, E> { cb.require_equal(|| name.clone(), lhs - rhs, diff_expr - is_lt_expr * range)?; - Ok(Lt2Config { is_lt, diff }) + Ok(ExprLtConfig { is_lt, diff }) }, ) } diff --git a/ceno_zkvm/src/chip_handler/register.rs b/ceno_zkvm/src/chip_handler/register.rs index 8802118a2..87b4f2eda 100644 --- a/ceno_zkvm/src/chip_handler/register.rs +++ b/ceno_zkvm/src/chip_handler/register.rs @@ -4,7 +4,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::config::Lt2Config, + instructions::riscv::config::ExprLtConfig, structs::RAMType, }; @@ -69,7 +69,7 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe ts: Expression, prev_values: &V, values: &V, - ) -> Result<(Expression, Lt2Config, Lt2Config, Lt2Config), ZKVMError> { + ) -> Result<(Expression, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = cb.rlc_chip_record( diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs index d664364d1..62e866d33 100644 --- a/ceno_zkvm/src/instructions/riscv/addsub.rs +++ b/ceno_zkvm/src/instructions/riscv/addsub.rs @@ -6,7 +6,7 @@ use ff_ext::ExtensionField; use itertools::Itertools; use super::{ - config::Lt2Config, + config::ExprLtConfig, constants::{OPType, OpcodeType, RegUInt, PC_STEP_SIZE}, RIVInstruction, }; @@ -15,7 +15,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{ToExpr, WitIn}, - instructions::{riscv::config::Lt2Input, Instruction}, + instructions::{riscv::config::ExprLtInput, Instruction}, set_val, uint::UIntValue, }; @@ -38,9 +38,9 @@ pub struct InstructionConfig { pub prev_rs1_ts: WitIn, pub prev_rs2_ts: WitIn, pub prev_rd_ts: WitIn, - pub lt_rs1_cfg: Lt2Config, - pub lt_rs2_cfg: Lt2Config, - pub lt_prev_ts_cfg: Lt2Config, + pub lt_rs1_cfg: ExprLtConfig, + pub lt_rs2_cfg: ExprLtConfig, + pub lt_prev_ts_cfg: ExprLtConfig, phantom: PhantomData, } @@ -192,17 +192,17 @@ impl Instruction for AddInstruction { set_val!(instance, config.prev_rs2_ts, 2); set_val!(instance, config.prev_rd_ts, 2); - Lt2Input { + ExprLtInput { lhs: 2, // rs1 rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 } .assign(instance, &config.lt_rs1_cfg); - Lt2Input { + ExprLtInput { lhs: 2, // rs2 rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 } .assign(instance, &config.lt_rs2_cfg); - Lt2Input { + ExprLtInput { lhs: 2, // rd rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1 } diff --git a/ceno_zkvm/src/instructions/riscv/blt.rs b/ceno_zkvm/src/instructions/riscv/blt.rs index fc0181d4b..696a54262 100644 --- a/ceno_zkvm/src/instructions/riscv/blt.rs +++ b/ceno_zkvm/src/instructions/riscv/blt.rs @@ -10,7 +10,7 @@ use crate::{ error::ZKVMError, expression::{ToExpr, WitIn}, instructions::{ - riscv::config::{LtConfig, LtInput}, + riscv::config::{UIntLtConfig, UIntLtInput}, Instruction, }, set_val, @@ -37,7 +37,7 @@ pub struct InstructionConfig { pub rs2_id: WitIn, pub prev_rs1_ts: WitIn, pub prev_rs2_ts: WitIn, - pub is_lt: LtConfig, + pub is_lt: UIntLtConfig, } pub struct BltInput { @@ -61,7 +61,7 @@ impl BltInput { ) { assert!(!self.lhs_limb8.is_empty() && (self.lhs_limb8.len() == self.rhs_limb8.len())); // TODO: add boundary check for witin - let lt_input = LtInput { + let lt_input = UIntLtInput { lhs_limbs: &self.lhs_limb8, rhs_limbs: &self.rhs_limb8, }; diff --git a/ceno_zkvm/src/instructions/riscv/config.rs b/ceno_zkvm/src/instructions/riscv/config.rs index 913a8bbcc..74d72bf1e 100644 --- a/ceno_zkvm/src/instructions/riscv/config.rs +++ b/ceno_zkvm/src/instructions/riscv/config.rs @@ -42,7 +42,7 @@ impl MsbInput<'_> { } #[derive(Clone)] -pub struct LtuConfig { +pub struct UIntLtuConfig { pub indexes: Vec, pub acc_indexes: Vec, pub byte_diff_inv: WitIn, @@ -51,16 +51,16 @@ pub struct LtuConfig { pub is_ltu: WitIn, } -pub struct LtuInput<'a> { +pub struct UIntLtuInput<'a> { pub lhs_limbs: &'a [u8], pub rhs_limbs: &'a [u8], } -impl LtuInput<'_> { +impl UIntLtuInput<'_> { pub fn assign( &self, instance: &mut [MaybeUninit], - config: &LtuConfig, + config: &UIntLtuConfig, ) -> bool { let mut idx = 0; let mut flag: bool = false; @@ -105,25 +105,25 @@ impl LtuInput<'_> { } #[derive(Clone)] -pub struct LtConfig { +pub struct UIntLtConfig { pub lhs_msb: MsbConfig, pub rhs_msb: MsbConfig, pub msb_is_equal: WitIn, pub msb_diff_inv: WitIn, - pub is_ltu: LtuConfig, + pub is_ltu: UIntLtuConfig, pub is_lt: WitIn, } -pub struct LtInput<'a> { +pub struct UIntLtInput<'a> { pub lhs_limbs: &'a [u8], pub rhs_limbs: &'a [u8], } -impl LtInput<'_> { +impl UIntLtInput<'_> { pub fn assign( &self, instance: &mut [MaybeUninit], - config: &LtConfig, + config: &UIntLtConfig, ) -> bool { let n_limbs = self.lhs_limbs.len(); let lhs_msb_input = MsbInput { @@ -141,7 +141,7 @@ impl LtInput<'_> { let mut rhs_limbs_no_msb = self.rhs_limbs.iter().copied().collect_vec(); rhs_limbs_no_msb[n_limbs - 1] = rhs_high_limb_no_msb; - let ltu_input = LtuInput { + let ltu_input = UIntLtuInput { lhs_limbs: &lhs_limbs_no_msb, rhs_limbs: &rhs_limbs_no_msb, }; @@ -170,18 +170,18 @@ impl LtInput<'_> { } #[derive(Debug)] -pub struct Lt2Config { +pub struct ExprLtConfig { pub is_lt: Option, pub diff: Vec, } -pub struct Lt2Input { +pub struct ExprLtInput { pub lhs: u64, pub rhs: u64, } -impl Lt2Input { - pub fn assign(&self, instance: &mut [MaybeUninit], config: &Lt2Config) { +impl ExprLtInput { + pub fn assign(&self, instance: &mut [MaybeUninit], config: &ExprLtConfig) { if let Some(is_lt) = config.is_lt { set_val!(instance, is_lt, { if self.lhs < self.rhs { 1 } else { 0 } }); } diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index 6df54259c..4f8ca3f01 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -400,7 +400,7 @@ mod tests { error::ZKVMError, expression::{ToExpr, WitIn}, instructions::{ - riscv::config::{Lt2Config, Lt2Input, LtInput}, + riscv::config::{ExprLtConfig, ExprLtInput}, Instruction, }, set_val, @@ -546,7 +546,7 @@ mod tests { struct AssertLtCircuit { pub a: WitIn, pub b: WitIn, - pub lt_wtns: Lt2Config, + pub lt_wtns: ExprLtConfig, } struct AssertLtCircuitInput { @@ -569,7 +569,7 @@ mod tests { ) -> Result<(), ZKVMError> { set_val!(instance, self.a, input.a); set_val!(instance, self.b, input.b); - Lt2Input { + ExprLtInput { lhs: input.a, rhs: input.b, } @@ -663,7 +663,7 @@ mod tests { struct LtCircuit { pub a: WitIn, pub b: WitIn, - pub lt_wtns: Lt2Config, + pub lt_wtns: ExprLtConfig, } struct LtCircuitInput { @@ -686,7 +686,7 @@ mod tests { ) -> Result<(), ZKVMError> { set_val!(instance, self.a, input.a); set_val!(instance, self.b, input.b); - Lt2Input { + ExprLtInput { lhs: input.a, rhs: input.b, } diff --git a/ceno_zkvm/src/uint/arithmetic.rs b/ceno_zkvm/src/uint/arithmetic.rs index caeb59273..6e9b1b609 100644 --- a/ceno_zkvm/src/uint/arithmetic.rs +++ b/ceno_zkvm/src/uint/arithmetic.rs @@ -8,7 +8,7 @@ use crate::{ create_witin_from_expr, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - instructions::riscv::config::{IsEqualConfig, LtConfig, LtuConfig, MsbConfig}, + instructions::riscv::config::{IsEqualConfig, MsbConfig, UIntLtConfig, UIntLtuConfig}, }; impl UInt { @@ -271,7 +271,7 @@ impl UInt { &self, circuit_builder: &mut CircuitBuilder, rhs: &UInt, - ) -> Result { + ) -> Result { let n_bytes = Self::NUM_CELLS; let indexes: Vec = (0..n_bytes) .map(|_| circuit_builder.create_witin(|| "index")) @@ -349,7 +349,7 @@ impl UInt { // circuit_builder.assert_bit(is_ltu.expr())?; // lookup ensure it is bit // now we know the first non-equal byte pairs is (lhs_ne_byte, rhs_ne_byte) circuit_builder.lookup_ltu_limb8(is_ltu.expr(), lhs_ne_byte.expr(), rhs_ne_byte.expr())?; - Ok(LtuConfig { + Ok(UIntLtuConfig { byte_diff_inv, indexes, acc_indexes: si, @@ -363,7 +363,7 @@ impl UInt { &self, circuit_builder: &mut CircuitBuilder, rhs: &UInt, - ) -> Result { + ) -> Result { let is_lt = circuit_builder.create_witin(|| "is_lt")?; circuit_builder.assert_bit(|| "assert_bit", is_lt.expr())?; @@ -389,7 +389,7 @@ impl UInt { + msb_is_equal.expr() * is_ltu.is_ltu.expr() - is_lt.expr(), )?; - Ok(LtConfig { + Ok(UIntLtConfig { lhs_msb, rhs_msb, msb_is_equal,