diff --git a/Cargo.lock b/Cargo.lock index 3c030bf42..172cfec85 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -310,6 +310,8 @@ version = "0.1.0" dependencies = [ "anyhow", "elf", + "strum 0.25.0", + "strum_macros 0.25.3", "tracing", ] diff --git a/ceno_emul/Cargo.toml b/ceno_emul/Cargo.toml index ed1096822..81730c113 100644 --- a/ceno_emul/Cargo.toml +++ b/ceno_emul/Cargo.toml @@ -6,6 +6,8 @@ license.workspace = true [dependencies] anyhow = { version = "1.0", default-features = false } +strum = "0.25.0" +strum_macros = "0.25.3" tracing = { version = "0.1", default-features = false, features = [ "attributes", ] } diff --git a/ceno_emul/src/lib.rs b/ceno_emul/src/lib.rs index c5359e442..8a21a0ac2 100644 --- a/ceno_emul/src/lib.rs +++ b/ceno_emul/src/lib.rs @@ -11,7 +11,7 @@ mod vm_state; pub use vm_state::VMState; mod rv32im; -pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnKind}; +pub use rv32im::{DecodedInstruction, EmuContext, InsnCodes, InsnCategory, InsnKind}; mod elf; pub use elf::Program; diff --git a/ceno_emul/src/rv32im.rs b/ceno_emul/src/rv32im.rs index 08f21302d..c173f1f21 100644 --- a/ceno_emul/src/rv32im.rs +++ b/ceno_emul/src/rv32im.rs @@ -16,6 +16,7 @@ use anyhow::{anyhow, Result}; use std::sync::OnceLock; +use strum_macros::EnumIter; use super::addr::{ByteAddr, RegIdx, Word, WordAddr, WORD_SIZE}; @@ -121,7 +122,7 @@ pub enum InsnCategory { Invalid, } -#[derive(Clone, Copy, Debug, PartialEq)] +#[derive(Clone, Copy, Debug, PartialEq, EnumIter)] #[allow(clippy::upper_case_acronyms)] pub enum InsnKind { INVALID, @@ -174,8 +175,14 @@ pub enum InsnKind { MRET, } +impl InsnKind { + pub const fn codes(self) -> InsnCodes { + RV32IM_ISA[self as usize] + } +} + #[derive(Clone, Copy, Debug)] -struct FastDecodeEntry { +pub struct InsnCodes { pub kind: InsnKind, category: InsnCategory, pub opcode: u32, @@ -269,8 +276,8 @@ const fn insn( opcode: u32, func3: i32, func7: i32, -) -> FastDecodeEntry { - FastDecodeEntry { +) -> InsnCodes { + InsnCodes { kind, category, opcode, @@ -279,7 +286,7 @@ const fn insn( } } -type InstructionTable = [FastDecodeEntry; 48]; +type InstructionTable = [InsnCodes; 48]; type FastInstructionTable = [u8; 1 << 10]; const RV32IM_ISA: InstructionTable = [ @@ -333,6 +340,15 @@ const RV32IM_ISA: InstructionTable = [ insn(InsnKind::MRET, InsnCategory::System, 0x73, 0x0, 0x18), ]; +#[cfg(test)] +#[test] +fn test_isa_table() { + use strum::IntoEnumIterator; + for kind in InsnKind::iter() { + assert_eq!(kind.codes().kind, kind); + } +} + // RISC-V instruction are determined by 3 parts: // - Opcode: 7 bits // - Func3: 3 bits @@ -373,7 +389,7 @@ impl FastDecodeTable { ((op_high << 5) | (func72bits << 3) | func3) as usize } - fn add_insn(table: &mut FastInstructionTable, insn: &FastDecodeEntry, isa_idx: usize) { + fn add_insn(table: &mut FastInstructionTable, insn: &InsnCodes, isa_idx: usize) { let op_high = insn.opcode >> 2; if (insn.func3 as i32) < 0 { for f3 in 0..8 { @@ -392,7 +408,7 @@ impl FastDecodeTable { } } - fn lookup(&self, decoded: &DecodedInstruction) -> FastDecodeEntry { + fn lookup(&self, decoded: &DecodedInstruction) -> InsnCodes { let isa_idx = self.table[Self::map10(decoded.opcode, decoded.func3, decoded.func7)]; RV32IM_ISA[isa_idx as usize] } diff --git a/ceno_zkvm/src/chip_handler.rs b/ceno_zkvm/src/chip_handler.rs index b3ac7cd52..76739a317 100644 --- a/ceno_zkvm/src/chip_handler.rs +++ b/ceno_zkvm/src/chip_handler.rs @@ -18,23 +18,23 @@ pub trait GlobalStateRegisterMachineChipOperations { } pub trait RegisterChipOperations, N: FnOnce() -> NR> { - fn register_read>>>( + fn register_read( &mut self, name_fn: N, register_id: &WitIn, prev_ts: Expression, ts: Expression, - values: &V, + values: &impl ToExpr>>, ) -> Result<(Expression, ExprLtConfig), ZKVMError>; #[allow(clippy::too_many_arguments)] - fn register_write>>>( + fn register_write( &mut self, name_fn: N, register_id: &WitIn, prev_ts: Expression, ts: Expression, - prev_values: &V, - values: &V, + prev_values: &impl ToExpr>>, + values: &impl ToExpr>>, ) -> Result<(Expression, ExprLtConfig), ZKVMError>; } diff --git a/ceno_zkvm/src/chip_handler/register.rs b/ceno_zkvm/src/chip_handler/register.rs index bdc978710..7efe3bb24 100644 --- a/ceno_zkvm/src/chip_handler/register.rs +++ b/ceno_zkvm/src/chip_handler/register.rs @@ -13,13 +13,13 @@ use super::RegisterChipOperations; impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOperations for CircuitBuilder<'a, E> { - fn register_read>>>( + fn register_read( &mut self, name_fn: N, register_id: &WitIn, prev_ts: Expression, ts: Expression, - values: &V, + values: &impl ToExpr>>, ) -> Result<(Expression, ExprLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) @@ -58,14 +58,14 @@ impl<'a, E: ExtensionField, NR: Into, N: FnOnce() -> NR> RegisterChipOpe }) } - fn register_write>>>( + fn register_write( &mut self, name_fn: N, register_id: &WitIn, prev_ts: Expression, ts: Expression, - prev_values: &V, - values: &V, + prev_values: &impl ToExpr>>, + values: &impl ToExpr>>, ) -> Result<(Expression, ExprLtConfig), ZKVMError> { self.namespace(name_fn, |cb| { // READ (a, v, t) diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs index bef83bd52..3d66f101a 100644 --- a/ceno_zkvm/src/instructions/riscv.rs +++ b/ceno_zkvm/src/instructions/riscv.rs @@ -1,16 +1,14 @@ -use constants::OpcodeType; -use ff_ext::ExtensionField; - -use super::Instruction; +use ceno_emul::InsnKind; pub mod addsub; pub mod blt; pub mod config; pub mod constants; +mod r_insn; #[cfg(test)] mod test; -pub trait RIVInstruction: Instruction { - const OPCODE_TYPE: OpcodeType; +pub trait RIVInstruction { + const INST_KIND: InsnKind; } diff --git a/ceno_zkvm/src/instructions/riscv/addsub.rs b/ceno_zkvm/src/instructions/riscv/addsub.rs index 5525fdfec..4d08945ad 100644 --- a/ceno_zkvm/src/instructions/riscv/addsub.rs +++ b/ceno_zkvm/src/instructions/riscv/addsub.rs @@ -1,284 +1,144 @@ use std::marker::PhantomData; -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, - }, - RIVInstruction, -}; +use super::{constants::RegUInt, r_insn::RInstructionConfig, 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; -pub struct AddInstruction(PhantomData); -pub struct SubInstruction(PhantomData); - +/// This config handles R-Instructions that represent registers values as 2 * u16. #[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 ArithConfig { + r_insn: RInstructionConfig, -impl RIVInstruction for AddInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::RType(OPType::Op, 0x000, 0x0000000); + rs1_read: RegUInt, + rs2_read: RegUInt, + rd_written: RegUInt, } -impl RIVInstruction for SubInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::RType(OPType::Op, 0x000, 0x0100000); -} - -fn add_sub_gadget( - 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())?; +pub struct ArithInstruction(PhantomData<(E, I)>); - 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, - }) +pub struct AddOp; +impl RIVInstruction for AddOp { + const INST_KIND: InsnKind = InsnKind::ADD; } +pub type AddInstruction = ArithInstruction; -fn add_sub_assignment( - config: &InstructionConfig, - 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!( - instance, - config.prev_rs2_ts, - step.rs2().unwrap().previous_cycle - ); - set_val!( - instance, - config.prev_rd_ts, - step.rd().unwrap().previous_cycle - ); - Ok(()) +pub struct SubOp; +impl RIVInstruction for SubOp { + const INST_KIND: InsnKind = InsnKind::SUB; } +pub type SubInstruction = ArithInstruction; -impl Instruction for AddInstruction { - // const NAME: &'static str = "ADD"; - fn name() -> String { - "ADD".into() - } - type InstructionConfig = InstructionConfig; - fn construct_circuit( - circuit_builder: &mut CircuitBuilder, - ) -> Result, ZKVMError> { - add_sub_gadget::(circuit_builder) - } +impl Instruction for ArithInstruction { + type InstructionConfig = ArithConfig; - #[allow(clippy::option_map_unit_fn)] - fn assign_instance( - config: &Self::InstructionConfig, - instance: &mut [MaybeUninit], - lk_multiplicity: &mut LkMultiplicity, - step: &StepRecord, - ) -> Result<(), ZKVMError> { - add_sub_assignment::<_, true>(config, instance, lk_multiplicity, step) - } -} - -impl Instruction for SubInstruction { - // const NAME: &'static str = "ADD"; fn name() -> String { - "SUB".into() + format!("{:?}", I::INST_KIND) } - type InstructionConfig = InstructionConfig; + fn construct_circuit( circuit_builder: &mut CircuitBuilder, - ) -> Result, ZKVMError> { - add_sub_gadget::(circuit_builder) + ) -> Result { + let (rs1_read, rs2_read, rd_written) = match I::INST_KIND { + InsnKind::ADD => { + // rd_written = rs1_read + rs2_read + let rs1_read = RegUInt::new_unchecked(|| "rs1_read", circuit_builder)?; + let rs2_read = RegUInt::new_unchecked(|| "rs2_read", circuit_builder)?; + let rd_written = rs1_read.add(|| "rd_written", circuit_builder, &rs2_read, true)?; + (rs1_read, rs2_read, rd_written) + } + + InsnKind::SUB => { + // rd_written + rs2_read = rs1_read + // rd_written is the new value to be updated in register so we need to constrain its range. + let rd_written = RegUInt::new(|| "rd_written", circuit_builder)?; + let rs2_read = RegUInt::new_unchecked(|| "rs2_read", circuit_builder)?; + let rs1_read = rs2_read.clone().add( + || "rs1_read", + circuit_builder, + &rd_written.clone(), + true, + )?; + (rs1_read, rs2_read, rd_written) + } + + _ => unreachable!("Unsupported instruction kind"), + }; + + let r_insn = RInstructionConfig::::construct_circuit( + circuit_builder, + I::INST_KIND, + &rs1_read, + &rs2_read, + &rd_written, + )?; + + Ok(ArithConfig { + r_insn, + rs1_read, + rs2_read, + rd_written, + }) } - #[allow(clippy::option_map_unit_fn)] fn assign_instance( config: &Self::InstructionConfig, - instance: &mut [MaybeUninit], + instance: &mut [MaybeUninit<::BaseField>], lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - add_sub_assignment::<_, false>(config, instance, lk_multiplicity, step) + config + .r_insn + .assign_instance(instance, lk_multiplicity, step)?; + + let rs2_read = UIntValue::new_unchecked(step.rs2().unwrap().value); + config + .rs2_read + .assign_limbs(instance, rs2_read.u16_fields()); + + match I::INST_KIND { + InsnKind::ADD => { + // rs1_read + rs2_read = rd_written + let rs1_read = UIntValue::new_unchecked(step.rs1().unwrap().value); + config + .rs1_read + .assign_limbs(instance, rs1_read.u16_fields()); + let (_, outcome_carries) = rs1_read.add(&rs2_read, lk_multiplicity, true); + config.rd_written.assign_carries( + instance, + outcome_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } + + InsnKind::SUB => { + // rs1_read = rd_written + rs2_read + let rd_written = UIntValue::new(step.rd().unwrap().value.after, lk_multiplicity); + config + .rd_written + .assign_limbs(instance, rd_written.u16_fields()); + let (_, addend_0_carries) = rs2_read.add(&rd_written, lk_multiplicity, true); + config.rs1_read.assign_carries( + instance, + addend_0_carries + .into_iter() + .map(|carry| E::BaseField::from(carry as u64)) + .collect_vec(), + ); + } + + _ => unreachable!("Unsupported instruction kind"), + }; + + Ok(()) } } diff --git a/ceno_zkvm/src/instructions/riscv/blt.rs b/ceno_zkvm/src/instructions/riscv/blt.rs index 30f4cc333..342bb6090 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, }; @@ -140,8 +141,8 @@ impl BltInput { } } -impl RIVInstruction for BltInstruction { - const OPCODE_TYPE: OpcodeType = OpcodeType::BType(OPType::Branch, 0x004); +impl RIVInstruction for BltInstruction { + const INST_KIND: InsnKind = InsnKind::BLT; } /// if (rs1 < rs2) PC += sext(imm) 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/r_insn.rs b/ceno_zkvm/src/instructions/riscv/r_insn.rs new file mode 100644 index 000000000..61baa02b4 --- /dev/null +++ b/ceno_zkvm/src/instructions/riscv/r_insn.rs @@ -0,0 +1,176 @@ +use ceno_emul::{InsnKind, StepRecord}; +use ff_ext::ExtensionField; + +use super::{ + config::ExprLtConfig, + constants::{RegUInt, PC_STEP_SIZE}, +}; +use crate::{ + chip_handler::{GlobalStateRegisterMachineChipOperations, RegisterChipOperations}, + circuit_builder::CircuitBuilder, + error::ZKVMError, + expression::{Expression, ToExpr, WitIn}, + instructions::riscv::config::ExprLtInput, + set_val, + tables::InsnRecord, + uint::UIntValue, + witness::LkMultiplicity, +}; +use core::mem::MaybeUninit; + +/// This config handles the common part of R-type instructions: +/// - PC, cycle, fetch. +/// - Registers read and write. +/// +/// It does not witness of the register values, nor the actual function (e.g. add, sub, etc). +#[derive(Debug)] +pub struct RInstructionConfig { + pc: WitIn, + ts: WitIn, + rs1_id: WitIn, + rs2_id: WitIn, + rd_id: WitIn, + prev_rd_value: RegUInt, + prev_rs1_ts: WitIn, + prev_rs2_ts: WitIn, + prev_rd_ts: WitIn, + lt_rs1_cfg: ExprLtConfig, + lt_rs2_cfg: ExprLtConfig, + lt_prev_ts_cfg: ExprLtConfig, +} + +impl RInstructionConfig { + pub fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + insn_kind: InsnKind, + rs1_read: &impl ToExpr>>, + rs2_read: &impl ToExpr>>, + rd_written: &impl ToExpr>>, + ) -> Result { + // State in. + let pc = circuit_builder.create_witin(|| "pc")?; + let cur_ts = circuit_builder.create_witin(|| "cur_ts")?; + circuit_builder.state_in(pc.expr(), cur_ts.expr())?; + + // Register indexes. + 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(), + (insn_kind.codes().opcode as usize).into(), + rd_id.expr(), + (insn_kind.codes().func3 as usize).into(), + rs1_id.expr(), + rs2_id.expr(), + (insn_kind.codes().func7 as usize).into(), + ))?; + + // Register state. + 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 prev_rd_value = RegUInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; + + // Register read and write. + let (ts, lt_rs1_cfg) = circuit_builder.register_read( + || "read_rs1", + &rs1_id, + prev_rs1_ts.expr(), + cur_ts.expr(), + rs1_read, + )?; + let (ts, lt_rs2_cfg) = circuit_builder.register_read( + || "read_rs2", + &rs2_id, + prev_rs2_ts.expr(), + ts, + rs2_read, + )?; + let (ts, lt_prev_ts_cfg) = circuit_builder.register_write( + || "write_rd", + &rd_id, + prev_rd_ts.expr(), + ts, + &prev_rd_value, + rd_written, + )?; + + // State out. + let next_pc = pc.expr() + PC_STEP_SIZE.into(); + let next_ts = ts + 1.into(); + circuit_builder.state_out(next_pc, next_ts)?; + + Ok(RInstructionConfig { + pc, + ts: cur_ts, + rs1_id, + rs2_id, + rd_id, + prev_rd_value, + prev_rs1_ts, + prev_rs2_ts, + prev_rd_ts, + lt_rs1_cfg, + lt_rs2_cfg, + lt_prev_ts_cfg, + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit<::BaseField>], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + ) -> Result<(), ZKVMError> { + // State in. + set_val!(instance, self.pc, step.pc().before.0 as u64); + set_val!(instance, self.ts, step.cycle()); + + // Register indexes. + set_val!(instance, self.rs1_id, step.insn().rs1() as u64); + set_val!(instance, self.rs2_id, step.insn().rs2() as u64); + set_val!(instance, self.rd_id, step.insn().rd() as u64); + + // Fetch the instruction. + lk_multiplicity.fetch(step.pc().before.0); + + // Register state. + set_val!( + instance, + self.prev_rs1_ts, + step.rs1().unwrap().previous_cycle + ); + set_val!( + instance, + self.prev_rs2_ts, + step.rs2().unwrap().previous_cycle + ); + set_val!(instance, self.prev_rd_ts, step.rd().unwrap().previous_cycle); + self.prev_rd_value.assign_limbs( + instance, + UIntValue::new_unchecked(step.rd().unwrap().value.before).u16_fields(), + ); + + // Register read and write. + ExprLtInput { + lhs: step.rs1().unwrap().previous_cycle, + rhs: step.cycle(), + } + .assign(instance, &self.lt_rs1_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rs2().unwrap().previous_cycle, + rhs: step.cycle() + 1, + } + .assign(instance, &self.lt_rs2_cfg, lk_multiplicity); + ExprLtInput { + lhs: step.rd().unwrap().previous_cycle, + rhs: step.cycle() + 2, + } + .assign(instance, &self.lt_prev_ts_cfg, lk_multiplicity); + + Ok(()) + } +}