diff --git a/ceno_zkvm/src/instructions/riscv.rs b/ceno_zkvm/src/instructions/riscv.rs index 67fb31cd2..cedf9f96e 100644 --- a/ceno_zkvm/src/instructions/riscv.rs +++ b/ceno_zkvm/src/instructions/riscv.rs @@ -6,13 +6,14 @@ pub mod branch; pub mod config; pub mod constants; pub mod divu; -mod i_insn; pub mod logic; +pub mod shift_imm; pub mod sltu; mod b_insn; +mod i_insn; +mod insn_base; mod r_insn; -pub mod shift_imm; #[cfg(test)] mod test; diff --git a/ceno_zkvm/src/instructions/riscv/b_insn.rs b/ceno_zkvm/src/instructions/riscv/b_insn.rs index 4a282a1af..54a9e53bc 100644 --- a/ceno_zkvm/src/instructions/riscv/b_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/b_insn.rs @@ -5,13 +5,11 @@ use ff_ext::ExtensionField; use super::constants::PC_STEP_SIZE; use crate::{ - chip_handler::{ - GlobalStateRegisterMachineChipOperations, RegisterChipOperations, RegisterExpr, - }, + chip_handler::RegisterExpr, circuit_builder::CircuitBuilder, error::ZKVMError, expression::{Expression, ToExpr, WitIn}, - gadgets::IsLtConfig, + instructions::riscv::insn_base::{ReadRS1, ReadRS2, StateInOut}, set_val, tables::InsnRecord, witness::LkMultiplicity, @@ -36,108 +34,72 @@ use core::mem::MaybeUninit; /// It does _not_ range-check the `branch_taken_bit`. /// It does not witness of the register values, nor the actual function (e.g. BNE). #[derive(Debug)] -pub struct BInstructionConfig { - pc: WitIn, - next_pc: WitIn, - ts: WitIn, - rs1_id: WitIn, - rs2_id: WitIn, - imm: WitIn, - prev_rs1_ts: WitIn, - prev_rs2_ts: WitIn, - lt_rs1_cfg: IsLtConfig, - lt_rs2_cfg: IsLtConfig, +pub struct BInstructionConfig { + pub vm_state: StateInOut, + pub rs1: ReadRS1, + pub rs2: ReadRS2, + pub imm: WitIn, } -impl BInstructionConfig { - pub fn construct_circuit( +impl BInstructionConfig { + pub fn construct_circuit( circuit_builder: &mut CircuitBuilder, insn_kind: InsnKind, rs1_read: RegisterExpr, rs2_read: RegisterExpr, branch_taken_bit: Expression, ) -> 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())?; + // State in and out + let vm_state = StateInOut::construct_circuit(circuit_builder, true)?; - // Register indexes and immediate. - let rs1_id = circuit_builder.create_witin(|| "rs1_id")?; - let rs2_id = circuit_builder.create_witin(|| "rs2_id")?; + // Registers + let rs1 = ReadRS1::construct_circuit(circuit_builder, rs1_read, vm_state.ts)?; + let rs2 = ReadRS2::construct_circuit(circuit_builder, rs2_read, vm_state.ts)?; + + // Immediate let imm = circuit_builder.create_witin(|| "imm")?; - // Fetch the instruction. + // Fetch instruction circuit_builder.lk_fetch(&InsnRecord::new( - pc.expr(), + vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), 0.into(), (insn_kind.codes().func3 as usize).into(), - rs1_id.expr(), - rs2_id.expr(), + rs1.id.expr(), + rs2.id.expr(), imm.expr(), ))?; - // Register state. - let prev_rs1_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; - let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; - - // Register reads. - let (ts, lt_rs1_cfg) = circuit_builder.register_read( - || "read_rs1", - &rs1_id, - prev_rs1_ts.expr(), - cur_ts.expr(), - rs1_read, + // Branch program counter + let pc_offset = branch_taken_bit.clone() * imm.expr() + - branch_taken_bit * PC_STEP_SIZE.into() + + PC_STEP_SIZE.into(); + let next_pc = vm_state.next_pc.unwrap(); + circuit_builder.require_equal( + || "pc_branch", + next_pc.expr(), + vm_state.pc.expr() + pc_offset, )?; - let (_ts, lt_rs2_cfg) = circuit_builder.register_read( - || "read_rs2", - &rs2_id, - prev_rs2_ts.expr(), - ts, - rs2_read, - )?; - - // State out. - let next_pc = { - let pc_offset = branch_taken_bit.clone() * imm.expr() - - branch_taken_bit * PC_STEP_SIZE.into() - + PC_STEP_SIZE.into(); - let next_pc = circuit_builder.create_witin(|| "next_pc")?; - circuit_builder.require_equal(|| "pc_branch", next_pc.expr(), pc.expr() + pc_offset)?; - next_pc - }; - let next_ts = cur_ts.expr() + 4.into(); - circuit_builder.state_out(next_pc.expr(), next_ts)?; Ok(BInstructionConfig { - pc, - next_pc, - ts: cur_ts, - rs1_id, - rs2_id, + vm_state, + rs1, + rs2, imm, - prev_rs1_ts, - prev_rs2_ts, - lt_rs1_cfg, - lt_rs2_cfg, }) } - pub fn assign_instance( + pub fn assign_instance( &self, instance: &mut [MaybeUninit<::BaseField>], lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - // State. - set_val!(instance, self.pc, step.pc().before.0 as u64); - set_val!(instance, self.next_pc, step.pc().after.0 as u64); - set_val!(instance, self.ts, step.cycle()); + self.vm_state.assign_instance(instance, step)?; + self.rs1.assign_instance(instance, lk_multiplicity, step)?; + self.rs2.assign_instance(instance, lk_multiplicity, step)?; - // Register indexes and immediate. - set_val!(instance, self.rs1_id, step.insn().rs1() as u64); - set_val!(instance, self.rs2_id, step.insn().rs2() as u64); + // Immediate set_val!( instance, self.imm, @@ -147,32 +109,6 @@ impl BInstructionConfig { // 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 - ); - - // Register read and write. - self.lt_rs1_cfg.assign_instance( - instance, - lk_multiplicity, - step.rs1().unwrap().previous_cycle, - step.cycle(), - )?; - self.lt_rs2_cfg.assign_instance( - instance, - lk_multiplicity, - step.rs2().unwrap().previous_cycle, - step.cycle() + 1, - )?; - Ok(()) } } diff --git a/ceno_zkvm/src/instructions/riscv/branch/beq_circuit.rs b/ceno_zkvm/src/instructions/riscv/branch/beq_circuit.rs index af63de6c5..30ca13189 100644 --- a/ceno_zkvm/src/instructions/riscv/branch/beq_circuit.rs +++ b/ceno_zkvm/src/instructions/riscv/branch/beq_circuit.rs @@ -17,7 +17,7 @@ use crate::{ }; pub struct BeqConfig { - b_insn: BInstructionConfig, + b_insn: BInstructionConfig, // TODO: Limb decomposition is not necessary. Replace with a single witness. rs1_read: UInt, @@ -78,7 +78,7 @@ impl Instruction for BeqCircuit { ) -> Result<(), ZKVMError> { config .b_insn - .assign_instance::(instance, lk_multiplicity, step)?; + .assign_instance(instance, lk_multiplicity, step)?; let rs1_read = step.rs1().unwrap().value; config diff --git a/ceno_zkvm/src/instructions/riscv/branch/blt.rs b/ceno_zkvm/src/instructions/riscv/branch/blt.rs index 63dd23f2a..8521b8f61 100644 --- a/ceno_zkvm/src/instructions/riscv/branch/blt.rs +++ b/ceno_zkvm/src/instructions/riscv/branch/blt.rs @@ -20,7 +20,7 @@ use ceno_emul::InsnKind; pub struct BltCircuit(PhantomData); pub struct InstructionConfig { - pub b_insn: BInstructionConfig, + pub b_insn: BInstructionConfig, pub read_rs1: UInt, pub read_rs2: UInt, pub is_lt: UIntLtSignedConfig, @@ -90,7 +90,7 @@ impl Instruction for BltCircuit { config .b_insn - .assign_instance::(instance, lk_multiplicity, step)?; + .assign_instance(instance, lk_multiplicity, step)?; Ok(()) } diff --git a/ceno_zkvm/src/instructions/riscv/branch/bltu.rs b/ceno_zkvm/src/instructions/riscv/branch/bltu.rs index c51270c5e..b704d0856 100644 --- a/ceno_zkvm/src/instructions/riscv/branch/bltu.rs +++ b/ceno_zkvm/src/instructions/riscv/branch/bltu.rs @@ -23,7 +23,7 @@ use ceno_emul::InsnKind; pub struct BltuCircuit(PhantomData); pub struct InstructionConfig { - pub b_insn: BInstructionConfig, + pub b_insn: BInstructionConfig, pub read_rs1: UInt, pub read_rs2: UInt, pub is_lt: IsLtConfig, @@ -93,7 +93,7 @@ impl Instruction for BltuCircuit { config .b_insn - .assign_instance::(instance, lk_multiplicity, step)?; + .assign_instance(instance, lk_multiplicity, step)?; Ok(()) } diff --git a/ceno_zkvm/src/instructions/riscv/i_insn.rs b/ceno_zkvm/src/instructions/riscv/i_insn.rs index a1cd8ef43..f7cdca840 100644 --- a/ceno_zkvm/src/instructions/riscv/i_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/i_insn.rs @@ -1,18 +1,13 @@ use ceno_emul::{InsnKind, StepRecord}; use ff_ext::ExtensionField; -use super::constants::{UInt, PC_STEP_SIZE}; use crate::{ - chip_handler::{ - GlobalStateRegisterMachineChipOperations, RegisterChipOperations, RegisterExpr, - }, + chip_handler::RegisterExpr, circuit_builder::CircuitBuilder, error::ZKVMError, - expression::{Expression, ToExpr, WitIn}, - gadgets::IsLtConfig, - set_val, + expression::{Expression, ToExpr}, + instructions::riscv::insn_base::{ReadRS1, StateInOut, WriteRD}, tables::InsnRecord, - uint::Value, witness::LkMultiplicity, }; use core::mem::MaybeUninit; @@ -24,15 +19,9 @@ use core::mem::MaybeUninit; /// It does not witness of the register values, nor the actual function (e.g. srli, addi, etc). #[derive(Debug)] pub struct IInstructionConfig { - pub pc: WitIn, - pub ts: WitIn, - pub rs1_id: WitIn, - pub rd_id: WitIn, - pub prev_rd_value: UInt, - pub prev_rs1_ts: WitIn, - pub prev_rd_ts: WitIn, - pub lt_rs1_cfg: IsLtConfig, - pub lt_rd_cfg: IsLtConfig, + pub vm_state: StateInOut, + pub rs1: ReadRS1, + pub rd: WriteRD, } impl IInstructionConfig { @@ -43,63 +32,27 @@ impl IInstructionConfig { rs1_read: RegisterExpr, rd_written: RegisterExpr, ) -> 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())?; + // State in and out + let vm_state = StateInOut::construct_circuit(circuit_builder, false)?; - // Register indexes. - let rs1_id = circuit_builder.create_witin(|| "rs1_id")?; - let rd_id = circuit_builder.create_witin(|| "rd_id")?; + // Registers + let rs1 = ReadRS1::construct_circuit(circuit_builder, rs1_read, vm_state.ts)?; + let rd = WriteRD::construct_circuit(circuit_builder, rd_written, vm_state.ts)?; + + // TODO make imm representation consistent between instruction types // Fetch the instruction. circuit_builder.lk_fetch(&InsnRecord::new( - pc.expr(), + vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - rd_id.expr(), + rd.id.expr(), (insn_kind.codes().func3 as usize).into(), - rs1_id.expr(), + rs1.id.expr(), 0.into(), imm.clone(), ))?; - // Register state. - let prev_rs1_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; - let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; - let prev_rd_value = UInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; - - // Register read and write. - let (next_ts, lt_rs1_cfg) = circuit_builder.register_read( - || "read_rs1", - &rs1_id, - prev_rs1_ts.expr(), - cur_ts.expr(), - rs1_read, - )?; - let (next_ts, lt_rd_cfg) = circuit_builder.register_write( - || "write_rd", - &rd_id, - prev_rd_ts.expr(), - next_ts, - prev_rd_value.register_expr(), - rd_written, - )?; - - // State out. - let next_pc = pc.expr() + PC_STEP_SIZE.into(); - circuit_builder.state_out(next_pc, next_ts)?; - - Ok(IInstructionConfig { - pc, - ts: cur_ts, - rs1_id, - rd_id, - prev_rd_value, - prev_rs1_ts, - prev_rd_ts, - lt_rs1_cfg, - lt_rd_cfg, - }) + Ok(IInstructionConfig { vm_state, rs1, rd }) } pub fn assign_instance( @@ -108,43 +61,13 @@ impl IInstructionConfig { 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()); + self.vm_state.assign_instance(instance, step)?; + self.rs1.assign_instance(instance, lk_multiplicity, step)?; + self.rd.assign_instance(instance, lk_multiplicity, step)?; - // Register indexes. - set_val!(instance, self.rs1_id, step.insn().rs1() as u64); - set_val!(instance, self.rd_id, step.insn().rd() as u64); - - // Fetch the instruction. + // Fetch 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_rd_ts, step.rd().unwrap().previous_cycle); - self.prev_rd_value.assign_limbs( - instance, - Value::new_unchecked(step.rd().unwrap().value.before).as_u16_limbs(), - ); - - // Register read and write. - self.lt_rs1_cfg.assign_instance( - instance, - lk_multiplicity, - step.rs1().unwrap().previous_cycle, - step.cycle(), - )?; - self.lt_rd_cfg.assign_instance( - instance, - lk_multiplicity, - step.rd().unwrap().previous_cycle, - step.cycle() + 1, - )?; - Ok(()) } } diff --git a/ceno_zkvm/src/instructions/riscv/insn_base.rs b/ceno_zkvm/src/instructions/riscv/insn_base.rs new file mode 100644 index 000000000..9f3d7f869 --- /dev/null +++ b/ceno_zkvm/src/instructions/riscv/insn_base.rs @@ -0,0 +1,242 @@ +use ceno_emul::StepRecord; +use ff_ext::ExtensionField; + +use super::constants::{UInt, PC_STEP_SIZE}; +use crate::{ + chip_handler::{ + GlobalStateRegisterMachineChipOperations, RegisterChipOperations, RegisterExpr, + }, + circuit_builder::CircuitBuilder, + error::ZKVMError, + expression::{ToExpr, WitIn}, + gadgets::IsLtConfig, + set_val, + uint::Value, + witness::LkMultiplicity, +}; +use ceno_emul::Tracer; +use core::mem::MaybeUninit; +use std::marker::PhantomData; + +#[derive(Debug)] +pub struct StateInOut { + pub pc: WitIn, + pub next_pc: Option, + pub ts: WitIn, + _field_type: PhantomData, +} + +impl StateInOut { + /// If circuit is branching, leave witness for next_pc free and return in + /// configuration so that calling circuit can constrain its value. + /// Otherwise, internally increment by PC_STEP_SIZE + pub fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + branching: bool, + ) -> Result { + let pc = circuit_builder.create_witin(|| "pc")?; + let (next_pc_opt, next_pc_expr) = if branching { + let next_pc = circuit_builder.create_witin(|| "next_pc")?; + (Some(next_pc), next_pc.expr()) + } else { + (None, pc.expr() + PC_STEP_SIZE.into()) + }; + let ts = circuit_builder.create_witin(|| "ts")?; + let next_ts = ts.expr() + (Tracer::SUBCYCLES_PER_INSN as usize).into(); + circuit_builder.state_in(pc.expr(), ts.expr())?; + circuit_builder.state_out(next_pc_expr, next_ts)?; + + Ok(StateInOut { + pc, + next_pc: next_pc_opt, + ts, + _field_type: PhantomData, + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit<::BaseField>], + // lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + ) -> Result<(), ZKVMError> { + set_val!(instance, self.pc, step.pc().before.0 as u64); + if let Some(n_pc) = self.next_pc { + set_val!(instance, n_pc, step.pc().after.0 as u64); + } + set_val!(instance, self.ts, step.cycle()); + + Ok(()) + } +} + +#[derive(Debug)] +pub struct ReadRS1 { + pub id: WitIn, + pub prev_ts: WitIn, + pub lt_cfg: IsLtConfig, + _field_type: PhantomData, +} + +impl ReadRS1 { + pub fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + rs1_read: RegisterExpr, + cur_ts: WitIn, + ) -> Result { + let id = circuit_builder.create_witin(|| "rs1_id")?; + let prev_ts = circuit_builder.create_witin(|| "prev_rs1_ts")?; + let (_, lt_cfg) = circuit_builder.register_read( + || "read_rs1", + &id, + prev_ts.expr(), + cur_ts.expr() + (Tracer::SUBCYCLE_RS1 as usize).into(), + rs1_read, + )?; + + Ok(ReadRS1 { + id, + prev_ts, + lt_cfg, + _field_type: PhantomData, + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit<::BaseField>], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + ) -> Result<(), ZKVMError> { + set_val!(instance, self.id, step.insn().rs1() as u64); + + // Register state + set_val!(instance, self.prev_ts, step.rs1().unwrap().previous_cycle); + + // Register read + self.lt_cfg.assign_instance( + instance, + lk_multiplicity, + step.rs1().unwrap().previous_cycle, + step.cycle() + Tracer::SUBCYCLE_RS1, + )?; + + Ok(()) + } +} + +#[derive(Debug)] +pub struct ReadRS2 { + pub id: WitIn, + pub prev_ts: WitIn, + pub lt_cfg: IsLtConfig, + _field_type: PhantomData, +} + +impl ReadRS2 { + pub fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + rs2_read: RegisterExpr, + cur_ts: WitIn, + ) -> Result { + let id = circuit_builder.create_witin(|| "rs2_id")?; + let prev_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?; + let (_, lt_cfg) = circuit_builder.register_read( + || "read_rs2", + &id, + prev_ts.expr(), + cur_ts.expr() + (Tracer::SUBCYCLE_RS2 as usize).into(), + rs2_read, + )?; + + Ok(ReadRS2 { + id, + prev_ts, + lt_cfg, + _field_type: PhantomData, + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit<::BaseField>], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + ) -> Result<(), ZKVMError> { + set_val!(instance, self.id, step.insn().rs2() as u64); + + // Register state + set_val!(instance, self.prev_ts, step.rs2().unwrap().previous_cycle); + + // Register read + self.lt_cfg.assign_instance( + instance, + lk_multiplicity, + step.rs2().unwrap().previous_cycle, + step.cycle() + Tracer::SUBCYCLE_RS2, + )?; + + Ok(()) + } +} + +#[derive(Debug)] +pub struct WriteRD { + pub id: WitIn, + pub prev_ts: WitIn, + pub prev_value: UInt, + pub lt_cfg: IsLtConfig, +} + +impl WriteRD { + pub fn construct_circuit( + circuit_builder: &mut CircuitBuilder, + rd_written: RegisterExpr, + cur_ts: WitIn, + ) -> Result { + let id = circuit_builder.create_witin(|| "rd_id")?; + let prev_ts = circuit_builder.create_witin(|| "prev_rd_ts")?; + let prev_value = UInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; + let (_, lt_cfg) = circuit_builder.register_write( + || "write_rd", + &id, + prev_ts.expr(), + cur_ts.expr() + (Tracer::SUBCYCLE_RD as usize).into(), + prev_value.register_expr(), + rd_written, + )?; + + Ok(WriteRD { + id, + prev_ts, + prev_value, + lt_cfg, + }) + } + + pub fn assign_instance( + &self, + instance: &mut [MaybeUninit<::BaseField>], + lk_multiplicity: &mut LkMultiplicity, + step: &StepRecord, + ) -> Result<(), ZKVMError> { + set_val!(instance, self.id, step.insn().rd() as u64); + set_val!(instance, self.prev_ts, step.rd().unwrap().previous_cycle); + + // Register state + self.prev_value.assign_limbs( + instance, + Value::new_unchecked(step.rd().unwrap().value.before).as_u16_limbs(), + ); + + // Register write + self.lt_cfg.assign_instance( + instance, + lk_multiplicity, + step.rd().unwrap().previous_cycle, + step.cycle() + Tracer::SUBCYCLE_RD, + )?; + + Ok(()) + } +} diff --git a/ceno_zkvm/src/instructions/riscv/r_insn.rs b/ceno_zkvm/src/instructions/riscv/r_insn.rs index 0bc8034af..dfa38414c 100644 --- a/ceno_zkvm/src/instructions/riscv/r_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/r_insn.rs @@ -1,18 +1,13 @@ use ceno_emul::{InsnKind, StepRecord}; use ff_ext::ExtensionField; -use super::constants::{UInt, PC_STEP_SIZE}; use crate::{ - chip_handler::{ - GlobalStateRegisterMachineChipOperations, RegisterChipOperations, RegisterExpr, - }, + chip_handler::RegisterExpr, circuit_builder::CircuitBuilder, error::ZKVMError, - expression::{ToExpr, WitIn}, - gadgets::IsLtConfig, - set_val, + expression::ToExpr, + instructions::riscv::insn_base::{ReadRS1, ReadRS2, StateInOut, WriteRD}, tables::InsnRecord, - uint::Value, witness::LkMultiplicity, }; use core::mem::MaybeUninit; @@ -24,18 +19,10 @@ use core::mem::MaybeUninit; /// 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: UInt, - prev_rs1_ts: WitIn, - prev_rs2_ts: WitIn, - prev_rd_ts: WitIn, - lt_rs1_cfg: IsLtConfig, - lt_rs2_cfg: IsLtConfig, - lt_prev_ts_cfg: IsLtConfig, + pub vm_state: StateInOut, + pub rs1: ReadRS1, + pub rs2: ReadRS2, + pub rd: WriteRD, } impl RInstructionConfig { @@ -46,74 +33,30 @@ impl RInstructionConfig { rs2_read: RegisterExpr, rd_written: RegisterExpr, ) -> 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())?; + // State in and out + let vm_state = StateInOut::construct_circuit(circuit_builder, false)?; - // 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")?; + // Registers + let rs1 = ReadRS1::construct_circuit(circuit_builder, rs1_read, vm_state.ts)?; + let rs2 = ReadRS2::construct_circuit(circuit_builder, rs2_read, vm_state.ts)?; + let rd = WriteRD::construct_circuit(circuit_builder, rd_written, vm_state.ts)?; - // Fetch the instruction. + // Fetch instruction circuit_builder.lk_fetch(&InsnRecord::new( - pc.expr(), + vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - rd_id.expr(), + rd.id.expr(), (insn_kind.codes().func3 as usize).into(), - rs1_id.expr(), - rs2_id.expr(), + 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 = UInt::new_unchecked(|| "prev_rd_value", circuit_builder)?; - - // Register read and write. - let (next_ts, lt_rs1_cfg) = circuit_builder.register_read( - || "read_rs1", - &rs1_id, - prev_rs1_ts.expr(), - cur_ts.expr(), - rs1_read, - )?; - let (next_ts, lt_rs2_cfg) = circuit_builder.register_read( - || "read_rs2", - &rs2_id, - prev_rs2_ts.expr(), - next_ts, - rs2_read, - )?; - let (next_ts, lt_prev_ts_cfg) = circuit_builder.register_write( - || "write_rd", - &rd_id, - prev_rd_ts.expr(), - next_ts, - prev_rd_value.register_expr(), - rd_written, - )?; - - // State out. - let next_pc = pc.expr() + PC_STEP_SIZE.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, + vm_state, + rs1, + rs2, + rd, }) } @@ -123,55 +66,14 @@ impl RInstructionConfig { 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()); + self.vm_state.assign_instance(instance, step)?; + self.rs1.assign_instance(instance, lk_multiplicity, step)?; + self.rs2.assign_instance(instance, lk_multiplicity, step)?; + self.rd.assign_instance(instance, lk_multiplicity, step)?; - // 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. + // Fetch 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, - Value::new_unchecked(step.rd().unwrap().value.before).as_u16_limbs(), - ); - - // Register read and write. - self.lt_rs1_cfg.assign_instance( - instance, - lk_multiplicity, - step.rs1().unwrap().previous_cycle, - step.cycle(), - )?; - self.lt_rs2_cfg.assign_instance( - instance, - lk_multiplicity, - step.rs2().unwrap().previous_cycle, - step.cycle() + 1, - )?; - self.lt_prev_ts_cfg.assign_instance( - instance, - lk_multiplicity, - step.rd().unwrap().previous_cycle, - step.cycle() + 2, - )?; - Ok(()) } }