From 0bba26fb7dc8229dbb0e1aba69bfb33c5eb4deec Mon Sep 17 00:00:00 2001 From: "sm.wu" Date: Mon, 16 Sep 2024 16:43:41 +0800 Subject: [PATCH] add/sub -> rtype gadget to build circuit --- ceno_emul/src/lib.rs | 4 +- ceno_emul/src/rv32im.rs | 4 +- ceno_zkvm/src/instructions/riscv.rs | 6 +- ceno_zkvm/src/instructions/riscv/addsub.rs | 313 ++++++------------ ceno_zkvm/src/instructions/riscv/blt.rs | 7 +- ceno_zkvm/src/instructions/riscv/config.rs | 6 +- ceno_zkvm/src/instructions/riscv/constants.rs | 29 -- ceno_zkvm/src/instructions/riscv/gadgets.rs | 191 +++++++++++ 8 files changed, 306 insertions(+), 254 deletions(-) create mode 100644 ceno_zkvm/src/instructions/riscv/gadgets.rs diff --git a/ceno_emul/src/lib.rs b/ceno_emul/src/lib.rs index c5359e442..8b011a5be 100644 --- a/ceno_emul/src/lib.rs +++ b/ceno_emul/src/lib.rs @@ -11,7 +11,9 @@ mod vm_state; pub use vm_state::VMState; mod rv32im; -pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnKind}; +pub use rv32im::{ + DecodedInstruction, EmuContext, FastDecodeEntry, InsnCategory, InsnKind, RV32IM_ISA, +}; mod elf; pub use elf::Program; diff --git a/ceno_emul/src/rv32im.rs b/ceno_emul/src/rv32im.rs index 08f21302d..9ad5385a3 100644 --- a/ceno_emul/src/rv32im.rs +++ b/ceno_emul/src/rv32im.rs @@ -175,7 +175,7 @@ pub enum InsnKind { } #[derive(Clone, Copy, Debug)] -struct FastDecodeEntry { +pub struct FastDecodeEntry { pub kind: InsnKind, category: InsnCategory, pub opcode: u32, @@ -282,7 +282,7 @@ const fn insn( type InstructionTable = [FastDecodeEntry; 48]; type FastInstructionTable = [u8; 1 << 10]; -const RV32IM_ISA: InstructionTable = [ +pub const RV32IM_ISA: InstructionTable = [ insn(InsnKind::INVALID, InsnCategory::Invalid, 0x00, 0x0, 0x00), insn(InsnKind::ADD, InsnCategory::Compute, 0x33, 0x0, 0x00), insn(InsnKind::SUB, InsnCategory::Compute, 0x33, 0x0, 0x20), diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs index bef83bd52..6c6306876 100644 --- a/ceno_zkvm/src/instructions/riscv.rs +++ b/ceno_zkvm/src/instructions/riscv.rs @@ -1,4 +1,4 @@ -use constants::OpcodeType; +use ceno_emul::{FastDecodeEntry, InsnKind, RV32IM_ISA}; use ff_ext::ExtensionField; use super::Instruction; @@ -7,10 +7,12 @@ pub mod addsub; pub mod blt; pub mod config; pub mod constants; +mod gadgets; #[cfg(test)] mod test; pub trait RIVInstruction: Instruction { - const OPCODE_TYPE: OpcodeType; + const INST_KIND: InsnKind; + const OPCODE_TYPE: FastDecodeEntry = RV32IM_ISA[Self::INST_KIND as usize]; } diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs index 5525fdfec..8da9a1cc7 100644 --- a/ceno_zkvm/src/instructions/riscv/addsub.rs +++ b/ceno_zkvm/src/instructions/riscv/addsub.rs @@ -1,26 +1,16 @@ -use std::marker::PhantomData; +use std::{marker::PhantomData, ops::Deref}; -use ceno_emul::StepRecord; +use ceno_emul::{InsnKind, StepRecord}; use ff_ext::ExtensionField; use itertools::Itertools; use super::{ - config::ExprLtConfig, - constants::{ - OPType, OpcodeType, RegUInt, FUNCT3_ADD_SUB, FUNCT7_ADD, FUNCT7_SUB, OPCODE_OP, - PC_STEP_SIZE, - }, + constants::RegUInt, + gadgets::{RTypeGadget, RTypeInstructionConfig}, RIVInstruction, }; use crate::{ - chip_handler::{GlobalStateRegisterMachineChipOperations, RegisterChipOperations}, - circuit_builder::CircuitBuilder, - error::ZKVMError, - expression::{ToExpr, WitIn}, - instructions::{riscv::config::ExprLtInput, Instruction}, - set_val, - tables::InsnRecord, - uint::UIntValue, + circuit_builder::CircuitBuilder, error::ZKVMError, instructions::Instruction, uint::UIntValue, witness::LkMultiplicity, }; use core::mem::MaybeUninit; @@ -29,223 +19,118 @@ pub struct AddInstruction(PhantomData); pub struct SubInstruction(PhantomData); #[derive(Debug)] -pub struct InstructionConfig { - pub pc: WitIn, - pub ts: WitIn, - pub prev_rd_value: RegUInt, - pub addend_0: RegUInt, - pub addend_1: RegUInt, - pub outcome: RegUInt, - pub rs1_id: WitIn, - pub rs2_id: WitIn, - pub rd_id: WitIn, - pub prev_rs1_ts: WitIn, - pub prev_rs2_ts: WitIn, - pub prev_rd_ts: WitIn, - pub lt_rs1_cfg: ExprLtConfig, - pub lt_rs2_cfg: ExprLtConfig, - pub lt_prev_ts_cfg: ExprLtConfig, - phantom: PhantomData, +pub struct InstructionConfig(RTypeInstructionConfig); + +impl Deref for InstructionConfig { + type Target = RTypeInstructionConfig; + + fn deref(&self) -> &Self::Target { + &self.0 + } } impl RIVInstruction for AddInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::RType(OPType::Op, 0x000, 0x0000000); + const INST_KIND: InsnKind = InsnKind::ADD; } impl RIVInstruction for SubInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::RType(OPType::Op, 0x000, 0x0100000); + const INST_KIND: InsnKind = InsnKind::SUB; } -fn add_sub_gadget( +fn add_sub_gadget, E: ExtensionField>( circuit_builder: &mut CircuitBuilder, ) -> Result, ZKVMError> { - let pc = circuit_builder.create_witin(|| "pc")?; - let cur_ts = circuit_builder.create_witin(|| "cur_ts")?; - - // state in - circuit_builder.state_in(pc.expr(), cur_ts.expr())?; - - let next_pc = pc.expr() + PC_STEP_SIZE.into(); - - // Execution result = addend0 + addend1, with carry. - let prev_rd_value = RegUInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; - - let (addend_0, addend_1, outcome) = if IS_ADD { - // outcome = addend_0 + addend_1 - let addend_0 = RegUInt::new_unchecked(|| "addend_0", circuit_builder)?; - let addend_1 = RegUInt::new_unchecked(|| "addend_1", circuit_builder)?; - ( - addend_0.clone(), - addend_1.clone(), - addend_0.add(|| "outcome", circuit_builder, &addend_1, true)?, - ) - } else { - // outcome + addend_1 = addend_0 - // outcome is the new value to be updated in register so we need to constrain its range - let outcome = RegUInt::new(|| "outcome", circuit_builder)?; - let addend_1 = RegUInt::new_unchecked(|| "addend_1", circuit_builder)?; - ( - addend_1 - .clone() - .add(|| "addend_0", circuit_builder, &outcome.clone(), true)?, - addend_1, - outcome, - ) - }; - - let rs1_id = circuit_builder.create_witin(|| "rs1_id")?; - let rs2_id = circuit_builder.create_witin(|| "rs2_id")?; - let rd_id = circuit_builder.create_witin(|| "rd_id")?; - - // Fetch the instruction. - circuit_builder.lk_fetch(&InsnRecord::new( - pc.expr(), - OPCODE_OP.into(), - rd_id.expr(), - FUNCT3_ADD_SUB.into(), - rs1_id.expr(), - rs2_id.expr(), - (if IS_ADD { FUNCT7_ADD } else { FUNCT7_SUB }).into(), - ))?; - - let prev_rs1_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; - let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; - let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; - - let (ts, lt_rs1_cfg) = circuit_builder.register_read( - || "read_rs1", - &rs1_id, - prev_rs1_ts.expr(), - cur_ts.expr(), - &addend_0, - )?; - let (ts, lt_rs2_cfg) = - circuit_builder.register_read(|| "read_rs2", &rs2_id, prev_rs2_ts.expr(), ts, &addend_1)?; - - let (ts, lt_prev_ts_cfg) = circuit_builder.register_write( - || "write_rd", - &rd_id, - prev_rd_ts.expr(), - ts, - &prev_rd_value, - &outcome, - )?; - - let next_ts = ts + 1.into(); - circuit_builder.state_out(next_pc, next_ts)?; - - Ok(InstructionConfig { - pc, - ts: cur_ts, - prev_rd_value, - addend_0, - addend_1, - outcome, - rs1_id, - rs2_id, - rd_id, - prev_rs1_ts, - prev_rs2_ts, - prev_rd_ts, - lt_rs1_cfg, - lt_rs2_cfg, - lt_prev_ts_cfg, - phantom: PhantomData, - }) + Ok(InstructionConfig(RTypeGadget::construct_circuit::( + circuit_builder, + |cb| { + Ok(match IC::INST_KIND { + InsnKind::ADD => { + // outcome = addend_0 + addend_1 + let addend_0 = RegUInt::new_unchecked(|| "addend_0", cb)?; + let addend_1 = RegUInt::new_unchecked(|| "addend_1", cb)?; + ( + addend_0.clone(), + addend_1.clone(), + addend_0.add(|| "outcome", cb, &addend_1, true)?, + ) + } + InsnKind::SUB => { + // outcome + addend_1 = addend_0 + // outcome is the new value to be updated in register so we need to constrain its range + let outcome = RegUInt::new(|| "outcome", cb)?; + let addend_1 = RegUInt::new_unchecked(|| "addend_1", cb)?; + ( + addend_1 + .clone() + .add(|| "addend_0", cb, &outcome.clone(), true)?, + addend_1, + outcome, + ) + } + _ => unreachable!(), + }) + }, + )?)) } -fn add_sub_assignment( - config: &InstructionConfig, +fn add_sub_assignment, E: ExtensionField>( + config: &RTypeInstructionConfig, instance: &mut [MaybeUninit], lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - lk_multiplicity.fetch(step.pc().before.0); - set_val!(instance, config.pc, step.pc().before.0 as u64); - set_val!(instance, config.ts, step.cycle()); - let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value); - let rd_prev = UIntValue::new_unchecked(step.rd().unwrap().value.before); - config - .prev_rd_value - .assign_limbs(instance, rd_prev.u16_fields()); - - config - .addend_1 - .assign_limbs(instance, addend_1.u16_fields()); - - if IS_ADD { - // addend_0 + addend_1 = outcome - let addend_0 = UIntValue::new_unchecked(step.rs1().unwrap().value); - config - .addend_0 - .assign_limbs(instance, addend_0.u16_fields()); - let (_, outcome_carries) = addend_0.add(&addend_1, lk_multiplicity, true); - config.outcome.assign_carries( - instance, - outcome_carries - .into_iter() - .map(|carry| E::BaseField::from(carry as u64)) - .collect_vec(), - ); - } else { - // addend_0 = outcome + addend_1 - let outcome = UIntValue::new(step.rd().unwrap().value.after, lk_multiplicity); - config.outcome.assign_limbs(instance, outcome.u16_fields()); - let (_, addend_0_carries) = addend_1.add(&outcome, lk_multiplicity, true); - config.addend_0.assign_carries( - instance, - addend_0_carries - .into_iter() - .map(|carry| E::BaseField::from(carry as u64)) - .collect_vec(), - ); - } - set_val!(instance, config.rs1_id, step.insn().rs1() as u64); - set_val!(instance, config.rs2_id, step.insn().rs2() as u64); - set_val!(instance, config.rd_id, step.insn().rd() as u64); - ExprLtInput { - lhs: step.rs1().unwrap().previous_cycle, - rhs: step.cycle(), - } - .assign(instance, &config.lt_rs1_cfg, lk_multiplicity); - ExprLtInput { - lhs: step.rs2().unwrap().previous_cycle, - rhs: step.cycle() + 1, - } - .assign(instance, &config.lt_rs2_cfg, lk_multiplicity); - ExprLtInput { - lhs: step.rd().unwrap().previous_cycle, - rhs: step.cycle() + 2, - } - .assign(instance, &config.lt_prev_ts_cfg, lk_multiplicity); - set_val!( - instance, - config.prev_rs1_ts, - step.rs1().unwrap().previous_cycle - ); - set_val!( + RTypeGadget::assign( + config, instance, - config.prev_rs2_ts, - step.rs2().unwrap().previous_cycle - ); - set_val!( - instance, - config.prev_rd_ts, - step.rd().unwrap().previous_cycle - ); - Ok(()) + lk_multiplicity, + step, + |config, instance, lk_multiplicity, step, addend_1| { + match IC::INST_KIND { + InsnKind::ADD => { + // addend_0 + addend_1 = outcome + let addend_0 = UIntValue::new_unchecked(step.rs1().unwrap().value); + config + .addend_0 + .assign_limbs(instance, addend_0.u16_fields()); + let (_, outcome_carries) = addend_0.add(addend_1, lk_multiplicity, true); + config.outcome.assign_carries( + instance, + outcome_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } + InsnKind::SUB => { + // addend_0 = outcome + addend_1 + let outcome = UIntValue::new(step.rd().unwrap().value.after, lk_multiplicity); + config.outcome.assign_limbs(instance, outcome.u16_fields()); + let (_, addend_0_carries) = addend_1.add(&outcome, lk_multiplicity, true); + config.addend_0.assign_carries( + instance, + addend_0_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } + _ => unreachable!(), + }; + Ok(()) + }, + ) } impl Instruction for AddInstruction { - // const NAME: &'static str = "ADD"; + type InstructionConfig = InstructionConfig; + fn name() -> String { - "ADD".into() + format!("{:?}", Self::INST_KIND) } - type InstructionConfig = InstructionConfig; fn construct_circuit( circuit_builder: &mut CircuitBuilder, ) -> Result, ZKVMError> { - add_sub_gadget::(circuit_builder) + add_sub_gadget::(circuit_builder) } #[allow(clippy::option_map_unit_fn)] @@ -255,20 +140,20 @@ impl Instruction for AddInstruction { lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - add_sub_assignment::<_, true>(config, instance, lk_multiplicity, step) + add_sub_assignment::(config, instance, lk_multiplicity, step) } } impl Instruction for SubInstruction { - // const NAME: &'static str = "ADD"; - fn name() -> String { - "SUB".into() - } type InstructionConfig = InstructionConfig; fn construct_circuit( circuit_builder: &mut CircuitBuilder, ) -> Result, ZKVMError> { - add_sub_gadget::(circuit_builder) + add_sub_gadget::(circuit_builder) + } + + fn name() -> String { + format!("{:?}", Self::INST_KIND) } #[allow(clippy::option_map_unit_fn)] @@ -278,7 +163,7 @@ impl Instruction for SubInstruction { lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - add_sub_assignment::<_, false>(config, instance, lk_multiplicity, step) + add_sub_assignment::(config, instance, lk_multiplicity, step) } } diff --git a/ceno_zkvm/src/instructions/riscv/blt.rs b/ceno_zkvm/src/instructions/riscv/blt.rs index 30f4cc333..bd5ddaab4 100644 --- a/ceno_zkvm/src/instructions/riscv/blt.rs +++ b/ceno_zkvm/src/instructions/riscv/blt.rs @@ -1,3 +1,4 @@ +use ceno_emul::InsnKind; use goldilocks::SmallField; use std::mem::MaybeUninit; @@ -20,7 +21,7 @@ use crate::{ use super::{ config::ExprLtConfig, - constants::{OPType, OpcodeType, RegUInt, RegUInt8, PC_STEP_SIZE}, + constants::{RegUInt, RegUInt8, PC_STEP_SIZE}, RIVInstruction, }; @@ -141,7 +142,7 @@ impl BltInput { } impl RIVInstruction for BltInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::BType(OPType::Branch, 0x004); + const INST_KIND: InsnKind = InsnKind::BLT; } /// if (rs1 < rs2) PC += sext(imm) @@ -261,7 +262,7 @@ mod test { .unwrap(); MockProver::assert_satisfied( - &mut circuit_builder, + &circuit_builder, &raw_witin .de_interleaving() .into_mles() diff --git a/ceno_zkvm/src/instructions/riscv/config.rs b/ceno_zkvm/src/instructions/riscv/config.rs index 2396475cd..b8513eeb2 100644 --- a/ceno_zkvm/src/instructions/riscv/config.rs +++ b/ceno_zkvm/src/instructions/riscv/config.rs @@ -12,7 +12,7 @@ pub struct IsEqualConfig { pub is_equal: WitIn, } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct MsbConfig { pub msb: WitIn, pub high_limb_no_msb: WitIn, @@ -41,7 +41,7 @@ impl MsbInput<'_> { } } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct UIntLtuConfig { pub indexes: Vec, pub acc_indexes: Vec, @@ -107,7 +107,7 @@ impl UIntLtuInput<'_> { } } -#[derive(Clone)] +#[derive(Clone, Debug)] pub struct UIntLtConfig { pub lhs_msb: MsbConfig, pub rhs_msb: MsbConfig, diff --git a/ceno_zkvm/src/instructions/riscv/constants.rs b/ceno_zkvm/src/instructions/riscv/constants.rs index e8c12cdb0..fe082e6b5 100644 --- a/ceno_zkvm/src/instructions/riscv/constants.rs +++ b/ceno_zkvm/src/instructions/riscv/constants.rs @@ -1,35 +1,6 @@ -use std::fmt; - use crate::uint::UInt; pub use ceno_emul::PC_STEP_SIZE; -pub const OPCODE_OP: usize = 0x33; -pub const FUNCT3_ADD_SUB: usize = 0; -pub const FUNCT7_ADD: usize = 0; -pub const FUNCT7_SUB: usize = 0x20; - -#[allow(clippy::upper_case_acronyms)] -#[derive(Debug, Clone, Copy)] -pub enum OPType { - Op, - Opimm, - Jal, - Jalr, - Branch, -} - -#[derive(Debug, Clone, Copy)] -pub enum OpcodeType { - RType(OPType, usize, usize), // (OP, func3, func7) - BType(OPType, usize), // (OP, func3) -} - -impl fmt::Display for OpcodeType { - fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { - write!(f, "{:?}", self) - } -} - pub const VALUE_BIT_WIDTH: usize = 16; #[cfg(feature = "riv32")] diff --git a/ceno_zkvm/src/instructions/riscv/gadgets.rs b/ceno_zkvm/src/instructions/riscv/gadgets.rs new file mode 100644 index 000000000..3fd163709 --- /dev/null +++ b/ceno_zkvm/src/instructions/riscv/gadgets.rs @@ -0,0 +1,191 @@ +use std::{marker::PhantomData, mem::MaybeUninit}; + +use ceno_emul::{StepRecord, PC_STEP_SIZE}; +use ff_ext::ExtensionField; + +use crate::{ + chip_handler::{GlobalStateRegisterMachineChipOperations, RegisterChipOperations}, + circuit_builder::CircuitBuilder, + error::ZKVMError, + expression::{ToExpr, WitIn}, + instructions::riscv::config::ExprLtInput, + set_val, + tables::InsnRecord, + witness::LkMultiplicity, + UIntValue, +}; + +use super::{config::ExprLtConfig, constants::RegUInt, RIVInstruction}; + +#[derive(Debug)] +pub struct RTypeInstructionConfig { + pub pc: WitIn, + pub ts: WitIn, + pub prev_rd_value: RegUInt, + pub addend_0: RegUInt, + pub addend_1: RegUInt, + pub outcome: RegUInt, + pub rs1_id: WitIn, + pub rs2_id: WitIn, + pub rd_id: WitIn, + pub prev_rs1_ts: WitIn, + pub prev_rs2_ts: WitIn, + pub prev_rd_ts: WitIn, + pub lt_rs1_cfg: ExprLtConfig, + pub lt_rs2_cfg: ExprLtConfig, + pub lt_prev_ts_cfg: ExprLtConfig, + phantom: PhantomData, +} + +pub(crate) struct RTypeGadget(PhantomData); + +impl RTypeGadget { + pub fn construct_circuit>( + circuit_builder: &mut CircuitBuilder, + operands_fn: impl FnOnce( + &mut CircuitBuilder, + ) -> Result<(RegUInt, RegUInt, RegUInt), ZKVMError>, + ) -> Result, ZKVMError> { + let pc = circuit_builder.create_witin(|| "pc")?; + let cur_ts = circuit_builder.create_witin(|| "cur_ts")?; + + // state in + circuit_builder.state_in(pc.expr(), cur_ts.expr())?; + + let next_pc = pc.expr() + PC_STEP_SIZE.into(); + + // Execution result = addend0 + addend1, with carry. + let prev_rd_value = RegUInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; + + let (addend_0, addend_1, outcome) = operands_fn(circuit_builder)?; + + let rs1_id = circuit_builder.create_witin(|| "rs1_id")?; + let rs2_id = circuit_builder.create_witin(|| "rs2_id")?; + let rd_id = circuit_builder.create_witin(|| "rd_id")?; + + // Fetch the instruction. + circuit_builder.lk_fetch(&InsnRecord::new( + pc.expr(), + (IC::OPCODE_TYPE.opcode as usize).into(), + rd_id.expr(), + (IC::OPCODE_TYPE.func3 as usize).into(), + rs1_id.expr(), + rs2_id.expr(), + (IC::OPCODE_TYPE.func7 as usize).into(), + ))?; + + let prev_rs1_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; + let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; + let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; + + let (ts, lt_rs1_cfg) = circuit_builder.register_read( + || "read_rs1", + &rs1_id, + prev_rs1_ts.expr(), + cur_ts.expr(), + &addend_0, + )?; + let (ts, lt_rs2_cfg) = circuit_builder.register_read( + || "read_rs2", + &rs2_id, + prev_rs2_ts.expr(), + ts, + &addend_1, + )?; + + let (ts, lt_prev_ts_cfg) = circuit_builder.register_write( + || "write_rd", + &rd_id, + prev_rd_ts.expr(), + ts, + &prev_rd_value, + &outcome, + )?; + + let next_ts = ts + 1.into(); + circuit_builder.state_out(next_pc, next_ts)?; + + Ok(RTypeInstructionConfig { + pc, + ts: cur_ts, + prev_rd_value, + addend_0, + addend_1, + outcome, + rs1_id, + rs2_id, + rd_id, + prev_rs1_ts, + prev_rs2_ts, + prev_rd_ts, + lt_rs1_cfg, + lt_rs2_cfg, + lt_prev_ts_cfg, + phantom: PhantomData, + }) + } + + pub fn assign( + config: &RTypeInstructionConfig, + instance: &mut [MaybeUninit], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + operands_fn: impl FnOnce( + &RTypeInstructionConfig, + &mut [MaybeUninit], + &mut LkMultiplicity, + &StepRecord, + &UIntValue, // TODO generalize to u64 + ) -> Result<(), ZKVMError>, + ) -> Result<(), ZKVMError> { + lk_multiplicity.fetch(step.pc().before.0); + set_val!(instance, config.pc, step.pc().before.0 as u64); + set_val!(instance, config.ts, step.cycle()); + let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value); + let rd_prev = UIntValue::new_unchecked(step.rd().unwrap().value.before); + config + .prev_rd_value + .assign_limbs(instance, rd_prev.u16_fields()); + + config + .addend_1 + .assign_limbs(instance, addend_1.u16_fields()); + + operands_fn(config, instance, lk_multiplicity, step, &addend_1)?; + + set_val!(instance, config.rs1_id, step.insn().rs1() as u64); + set_val!(instance, config.rs2_id, step.insn().rs2() as u64); + set_val!(instance, config.rd_id, step.insn().rd() as u64); + ExprLtInput { + lhs: step.rs1().unwrap().previous_cycle, + rhs: step.cycle(), + } + .assign(instance, &config.lt_rs1_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rs2().unwrap().previous_cycle, + rhs: step.cycle() + 1, + } + .assign(instance, &config.lt_rs2_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rd().unwrap().previous_cycle, + rhs: step.cycle() + 2, + } + .assign(instance, &config.lt_prev_ts_cfg, lk_multiplicity); + set_val!( + instance, + config.prev_rs1_ts, + step.rs1().unwrap().previous_cycle + ); + set_val!( + instance, + config.prev_rs2_ts, + step.rs2().unwrap().previous_cycle + ); + set_val!( + instance, + config.prev_rd_ts, + step.rd().unwrap().previous_cycle + ); + Ok(()) + } +}