diff --git a/ceno_zkvm/src/chip_handler.rs b/ceno_zkvm/src/chip_handler.rs index 8d16f342d..991fad3d7 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}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, instructions::riscv::constants::UINT_LIMBS, }; @@ -34,7 +34,7 @@ pub trait RegisterChipOperations, N: FnOnce( prev_ts: Expression, ts: Expression, value: RegisterExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError>; + ) -> Result<(Expression, AssertLtConfig), ZKVMError>; #[allow(clippy::too_many_arguments)] fn register_write( @@ -45,7 +45,7 @@ pub trait RegisterChipOperations, N: FnOnce( ts: Expression, prev_values: RegisterExpr, value: RegisterExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError>; + ) -> Result<(Expression, AssertLtConfig), ZKVMError>; } /// The common representation of a memory address. @@ -62,7 +62,7 @@ pub trait MemoryChipOperations, N: FnOnce() prev_ts: Expression, ts: Expression, value: MemoryExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError>; + ) -> Result<(Expression, AssertLtConfig), ZKVMError>; #[allow(clippy::too_many_arguments)] fn memory_write( @@ -73,5 +73,5 @@ pub trait MemoryChipOperations, N: FnOnce() ts: Expression, prev_values: MemoryExpr, value: MemoryExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError>; + ) -> Result<(Expression, AssertLtConfig), ZKVMError>; } diff --git a/ceno_zkvm/src/chip_handler/memory.rs b/ceno_zkvm/src/chip_handler/memory.rs index 3b6b2ec53..2969eeb7a 100644 --- a/ceno_zkvm/src/chip_handler/memory.rs +++ b/ceno_zkvm/src/chip_handler/memory.rs @@ -3,7 +3,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::Expression, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, instructions::riscv::constants::UINT_LIMBS, structs::RAMType, }; @@ -19,7 +19,7 @@ impl, N: FnOnce() -> NR> MemoryChipOperation prev_ts: Expression, ts: Expression, value: MemoryExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError> { + ) -> Result<(Expression, AssertLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = [ @@ -39,7 +39,7 @@ impl, N: FnOnce() -> NR> MemoryChipOperation cb.write_record(|| "write_record", RAMType::Memory, write_record)?; // assert prev_ts < current_ts - let lt_cfg = AssertLTConfig::construct_circuit( + let lt_cfg = AssertLtConfig::construct_circuit( cb, || "prev_ts < ts", prev_ts, @@ -61,7 +61,7 @@ impl, N: FnOnce() -> NR> MemoryChipOperation ts: Expression, prev_values: MemoryExpr, value: MemoryExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError> { + ) -> Result<(Expression, AssertLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = [ @@ -80,7 +80,7 @@ impl, N: FnOnce() -> NR> MemoryChipOperation cb.read_record(|| "read_record", RAMType::Memory, read_record)?; cb.write_record(|| "write_record", RAMType::Memory, write_record)?; - let lt_cfg = AssertLTConfig::construct_circuit( + let lt_cfg = AssertLtConfig::construct_circuit( cb, || "prev_ts < ts", prev_ts, diff --git a/ceno_zkvm/src/chip_handler/register.rs b/ceno_zkvm/src/chip_handler/register.rs index d2f1ebf14..c85060cc6 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}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, instructions::riscv::constants::UINT_LIMBS, structs::RAMType, }; @@ -21,7 +21,7 @@ impl, N: FnOnce() -> NR> RegisterChipOperati prev_ts: Expression, ts: Expression, value: RegisterExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError> { + ) -> Result<(Expression, AssertLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) let read_record = [ @@ -43,7 +43,7 @@ impl, N: FnOnce() -> NR> RegisterChipOperati cb.write_record(|| "write_record", RAMType::Register, write_record)?; // assert prev_ts < current_ts - let lt_cfg = AssertLTConfig::construct_circuit( + let lt_cfg = AssertLtConfig::construct_circuit( cb, || "prev_ts < ts", prev_ts, @@ -65,7 +65,7 @@ impl, N: FnOnce() -> NR> RegisterChipOperati ts: Expression, prev_values: RegisterExpr, value: RegisterExpr, - ) -> Result<(Expression, AssertLTConfig), ZKVMError> { + ) -> Result<(Expression, AssertLtConfig), ZKVMError> { assert!(register_id.expr().degree() <= 1); self.namespace(name_fn, |cb| { // READ (a, v, t) @@ -87,7 +87,7 @@ impl, N: FnOnce() -> NR> RegisterChipOperati cb.read_record(|| "read_record", RAMType::Register, read_record)?; cb.write_record(|| "write_record", RAMType::Register, write_record)?; - let lt_cfg = AssertLTConfig::construct_circuit( + let lt_cfg = AssertLtConfig::construct_circuit( cb, || "prev_ts < ts", prev_ts, diff --git a/ceno_zkvm/src/gadgets/div.rs b/ceno_zkvm/src/gadgets/div.rs index c9d86ab87..91f4b42f1 100644 --- a/ceno_zkvm/src/gadgets/div.rs +++ b/ceno_zkvm/src/gadgets/div.rs @@ -10,13 +10,13 @@ use crate::{ witness::LkMultiplicity, }; -use super::AssertLTConfig; +use super::AssertLtConfig; /// divide gadget #[derive(Debug, Clone)] pub struct DivConfig { pub dividend: UInt, - pub r_lt: AssertLTConfig, + pub r_lt: AssertLtConfig, pub intermediate_mul: UInt, } @@ -35,7 +35,7 @@ impl DivConfig { let (dividend, intermediate_mul) = divisor.mul_add(|| "divisor * outcome + r", cb, quotient, remainder, true)?; - let r_lt = AssertLTConfig::construct_circuit( + let r_lt = AssertLtConfig::construct_circuit( cb, || "remainder < divisor", remainder.value(), diff --git a/ceno_zkvm/src/gadgets/is_lt.rs b/ceno_zkvm/src/gadgets/is_lt.rs index 3885b7257..ff0fe3989 100644 --- a/ceno_zkvm/src/gadgets/is_lt.rs +++ b/ceno_zkvm/src/gadgets/is_lt.rs @@ -19,9 +19,9 @@ use crate::{ use super::SignedExtendConfig; #[derive(Debug, Clone)] -pub struct AssertLTConfig(InnerLtConfig); +pub struct AssertLtConfig(InnerLtConfig); -impl AssertLTConfig { +impl AssertLtConfig { pub fn construct_circuit< E: ExtensionField, NR: Into + Display + Clone, diff --git a/ceno_zkvm/src/gadgets/mod.rs b/ceno_zkvm/src/gadgets/mod.rs index 60846581e..0f21b3ce2 100644 --- a/ceno_zkvm/src/gadgets/mod.rs +++ b/ceno_zkvm/src/gadgets/mod.rs @@ -5,7 +5,7 @@ mod signed_ext; pub use div::DivConfig; pub use is_lt::{ - AssertLTConfig, AssertSignedLtConfig, InnerLtConfig, IsLtConfig, SignedLtConfig, cal_lt_diff, + AssertLtConfig, AssertSignedLtConfig, InnerLtConfig, IsLtConfig, SignedLtConfig, cal_lt_diff, }; pub use is_zero::{IsEqualConfig, IsZeroConfig}; pub use signed_ext::SignedExtendConfig; diff --git a/ceno_zkvm/src/instructions/riscv/ecall/halt.rs b/ceno_zkvm/src/instructions/riscv/ecall/halt.rs index 47ed7b9b7..70338e3d6 100644 --- a/ceno_zkvm/src/instructions/riscv/ecall/halt.rs +++ b/ceno_zkvm/src/instructions/riscv/ecall/halt.rs @@ -3,7 +3,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{ToExpr, WitIn}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, instructions::{ Instruction, riscv::{ @@ -21,7 +21,7 @@ use std::{marker::PhantomData, mem::MaybeUninit}; pub struct HaltConfig { ecall_cfg: EcallInstructionConfig, prev_x10_ts: WitIn, - lt_x10_cfg: AssertLTConfig, + lt_x10_cfg: AssertLtConfig, } pub struct HaltInstruction(PhantomData); diff --git a/ceno_zkvm/src/instructions/riscv/ecall_insn.rs b/ceno_zkvm/src/instructions/riscv/ecall_insn.rs index 3bd2faa1e..0457979c7 100644 --- a/ceno_zkvm/src/instructions/riscv/ecall_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/ecall_insn.rs @@ -5,7 +5,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, set_val, tables::InsnRecord, witness::LkMultiplicity, @@ -18,7 +18,7 @@ pub struct EcallInstructionConfig { pub pc: WitIn, pub ts: WitIn, prev_x5_ts: WitIn, - lt_x5_cfg: AssertLTConfig, + lt_x5_cfg: AssertLtConfig, } impl EcallInstructionConfig { diff --git a/ceno_zkvm/src/instructions/riscv/insn_base.rs b/ceno_zkvm/src/instructions/riscv/insn_base.rs index bcdae575f..3f71b6b20 100644 --- a/ceno_zkvm/src/instructions/riscv/insn_base.rs +++ b/ceno_zkvm/src/instructions/riscv/insn_base.rs @@ -12,7 +12,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, set_val, uint::Value, witness::LkMultiplicity, @@ -77,7 +77,7 @@ impl StateInOut { pub struct ReadRS1 { pub id: WitIn, pub prev_ts: WitIn, - pub lt_cfg: AssertLTConfig, + pub lt_cfg: AssertLtConfig, _field_type: PhantomData, } @@ -131,7 +131,7 @@ impl ReadRS1 { pub struct ReadRS2 { pub id: WitIn, pub prev_ts: WitIn, - pub lt_cfg: AssertLTConfig, + pub lt_cfg: AssertLtConfig, _field_type: PhantomData, } @@ -186,7 +186,7 @@ pub struct WriteRD { pub id: WitIn, pub prev_ts: WitIn, pub prev_value: UInt, - pub lt_cfg: AssertLTConfig, + pub lt_cfg: AssertLtConfig, } impl WriteRD { @@ -246,7 +246,7 @@ impl WriteRD { #[derive(Debug)] pub struct ReadMEM { pub prev_ts: WitIn, - pub lt_cfg: AssertLTConfig, + pub lt_cfg: AssertLtConfig, _field_type: PhantomData, } @@ -301,7 +301,7 @@ impl ReadMEM { #[derive(Debug)] pub struct WriteMEM { pub prev_ts: WitIn, - pub lt_cfg: AssertLTConfig, + pub lt_cfg: AssertLtConfig, } impl WriteMEM { diff --git a/ceno_zkvm/src/instructions/riscv/shift.rs b/ceno_zkvm/src/instructions/riscv/shift.rs index 5b8735311..365afe786 100644 --- a/ceno_zkvm/src/instructions/riscv/shift.rs +++ b/ceno_zkvm/src/instructions/riscv/shift.rs @@ -7,7 +7,7 @@ use crate::{ Value, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::{AssertLTConfig, SignedExtendConfig}, + gadgets::{AssertLtConfig, SignedExtendConfig}, instructions::Instruction, set_val, }; @@ -26,7 +26,7 @@ pub struct ShiftConfig { pow2_rs2_low5: WitIn, outflow: WitIn, - assert_lt_config: AssertLTConfig, + assert_lt_config: AssertLtConfig, // SRA signed_extend_config: Option>, @@ -90,7 +90,7 @@ impl Instruction for ShiftLogicalInstru let rs2_high = UInt::new(|| "rs2_high", circuit_builder)?; let outflow = circuit_builder.create_witin(|| "outflow"); - let assert_lt_config = AssertLTConfig::construct_circuit( + let assert_lt_config = AssertLtConfig::construct_circuit( circuit_builder, || "outflow < pow2_rs2_low5", outflow.expr(), diff --git a/ceno_zkvm/src/instructions/riscv/shift_imm.rs b/ceno_zkvm/src/instructions/riscv/shift_imm.rs index 4e2700914..080a8a6ae 100644 --- a/ceno_zkvm/src/instructions/riscv/shift_imm.rs +++ b/ceno_zkvm/src/instructions/riscv/shift_imm.rs @@ -4,7 +4,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::{AssertLTConfig, SignedExtendConfig}, + gadgets::{AssertLtConfig, SignedExtendConfig}, instructions::{ Instruction, riscv::{constants::UInt, i_insn::IInstructionConfig}, @@ -24,7 +24,7 @@ pub struct ShiftImmConfig { rs1_read: UInt, rd_written: UInt, outflow: WitIn, - assert_lt_config: AssertLTConfig, + assert_lt_config: AssertLtConfig, // SRAI is_lt_config: Option>, @@ -83,7 +83,7 @@ impl Instruction for ShiftImmInstructio let rd_written = UInt::new(|| "rd_written", circuit_builder)?; let outflow = circuit_builder.create_witin(|| "outflow"); - let assert_lt_config = AssertLTConfig::construct_circuit( + let assert_lt_config = AssertLtConfig::construct_circuit( circuit_builder, || "outflow < imm", outflow.expr(), diff --git a/ceno_zkvm/src/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index ccd8e0a07..b84e94148 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -1213,7 +1213,7 @@ mod tests { ROMType::U5, error::ZKVMError, expression::{ToExpr, WitIn}, - gadgets::{AssertLTConfig, IsLtConfig}, + gadgets::{AssertLtConfig, IsLtConfig}, set_val, witness::{LkMultiplicity, RowMajorMatrix}, }; @@ -1357,7 +1357,7 @@ mod tests { struct AssertLtCircuit { pub a: WitIn, pub b: WitIn, - pub lt_wtns: AssertLTConfig, + pub lt_wtns: AssertLtConfig, } struct AssertLtCircuitInput { @@ -1369,7 +1369,7 @@ mod tests { fn construct_circuit(cb: &mut CircuitBuilder) -> Result { let a = cb.create_witin(|| "a"); let b = cb.create_witin(|| "b"); - let lt_wtns = AssertLTConfig::construct_circuit(cb, || "lt", a.expr(), b.expr(), 1)?; + let lt_wtns = AssertLtConfig::construct_circuit(cb, || "lt", a.expr(), b.expr(), 1)?; Ok(Self { a, b, lt_wtns }) } diff --git a/ceno_zkvm/src/uint.rs b/ceno_zkvm/src/uint.rs index 193d34f13..97ece7193 100644 --- a/ceno_zkvm/src/uint.rs +++ b/ceno_zkvm/src/uint.rs @@ -8,7 +8,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::{UtilError, ZKVMError}, expression::{Expression, ToExpr, WitIn}, - gadgets::{AssertLTConfig, SignedExtendConfig}, + gadgets::{AssertLtConfig, SignedExtendConfig}, instructions::riscv::constants::UInt, utils::add_one_to_big_num, witness::LkMultiplicity, @@ -83,7 +83,7 @@ pub struct UIntLimbs { // We don't need `overflow` witness since the last element of `carries` represents it. pub carries: Option>, // for carry range check using lt tricks - pub carries_auxiliary_lt_config: Option>, + pub carries_auxiliary_lt_config: Option>, } impl UIntLimbs { @@ -131,7 +131,7 @@ impl UIntLimbs { pub fn from_witins_unchecked( limbs: Vec, carries: Option>, - carries_auxiliary_lt_config: Option>, + carries_auxiliary_lt_config: Option>, ) -> Self { assert!(limbs.len() == Self::NUM_LIMBS); if let Some(carries) = &carries { diff --git a/ceno_zkvm/src/uint/arithmetic.rs b/ceno_zkvm/src/uint/arithmetic.rs index dfe33b076..5e48b0319 100644 --- a/ceno_zkvm/src/uint/arithmetic.rs +++ b/ceno_zkvm/src/uint/arithmetic.rs @@ -7,7 +7,7 @@ use crate::{ circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::AssertLTConfig, + gadgets::AssertLtConfig, instructions::riscv::config::IsEqualConfig, }; @@ -137,7 +137,7 @@ impl UIntLimbs { .iter() .enumerate() .map(|(i, carry)| { - AssertLTConfig::construct_circuit( + AssertLtConfig::construct_circuit( circuit_builder, || format!("carry_{i}_in_less_than"), carry.expr(), @@ -145,7 +145,7 @@ impl UIntLimbs { Self::MAX_DEGREE_2_MUL_CARRY_U16_LIMB, ) }) - .collect::, ZKVMError>>()?; + .collect::, ZKVMError>>()?; // creating a witness constrained as expression to reduce overall degree let mut swap_witin = |name: &str,