From b34757cab916a2130ed3967c1bc28c4a9a4f9df4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aur=C3=A9lien=20Nicolas?= Date: Wed, 30 Oct 2024 12:14:38 +0100 Subject: [PATCH] feat/x0: support x0 by redirecting writes to RD_NULL --- ceno_emul/src/platform.rs | 8 ++----- ceno_emul/src/rv32im.rs | 21 +++++++------------ ceno_emul/src/tracer.rs | 2 +- ceno_emul/src/vm_state.rs | 8 +++++-- ceno_zkvm/src/instructions/riscv/b_insn.rs | 2 +- .../src/instructions/riscv/ecall_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/i_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/im_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/insn_base.rs | 2 +- ceno_zkvm/src/instructions/riscv/j_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/r_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/s_insn.rs | 2 +- ceno_zkvm/src/instructions/riscv/u_insn.rs | 2 +- ceno_zkvm/src/tables/program.rs | 14 ++++++++----- ceno_zkvm/src/tables/ram.rs | 4 ++-- 15 files changed, 37 insertions(+), 38 deletions(-) diff --git a/ceno_emul/src/platform.rs b/ceno_emul/src/platform.rs index 163757057..5b942932b 100644 --- a/ceno_emul/src/platform.rs +++ b/ceno_emul/src/platform.rs @@ -72,11 +72,6 @@ impl Platform { (vma >> 8) as RegIdx } - /// Virtual address of the program counter. - pub const fn pc_vma(&self) -> Addr { - self.register_vma(32) - } - // Startup. pub const fn pc_base(&self) -> Addr { @@ -128,6 +123,7 @@ impl Platform { #[cfg(test)] mod tests { use super::*; + use crate::VMState; #[test] fn test_no_overlap() { @@ -139,7 +135,7 @@ mod tests { assert!(!p.is_ram(p.rom_start())); assert!(!p.is_ram(p.rom_end())); // Registers do not overlap with ROM or RAM. - for reg in [p.pc_vma(), p.register_vma(0), p.register_vma(31)] { + for reg in [p.register_vma(0), p.register_vma(VMState::REG_COUNT - 1)] { assert!(!p.is_rom(reg)); assert!(!p.is_ram(reg)); } diff --git a/ceno_emul/src/rv32im.rs b/ceno_emul/src/rv32im.rs index 2deb4598a..df54f274d 100644 --- a/ceno_emul/src/rv32im.rs +++ b/ceno_emul/src/rv32im.rs @@ -204,6 +204,8 @@ pub struct InsnCodes { } impl DecodedInstruction { + pub const RD_NULL: u32 = 32; + pub fn new(insn: u32) -> Self { Self { insn, @@ -225,16 +227,11 @@ impl DecodedInstruction { self.opcode } - /// Get the rd field, regardless of the instruction format. - pub fn rd(&self) -> u32 { - self.rd - } - - /// Get the register destination, or zero if the instruction does not write to a register. - pub fn rd_or_zero(&self) -> u32 { + /// Get the register destination, or RD_NULL if the instruction does not write to a register or writes to x0. + pub fn rd_or_null(&self) -> u32 { match self.codes().format { - R | I | U | J => self.rd, - _ => 0, + R | I | U | J if self.rd != 0 => self.rd, + _ => Self::RD_NULL, } } @@ -581,10 +578,8 @@ impl Emulator { let pc = ctx.get_pc(); let mut new_pc = pc + WORD_SIZE; - let mut rd = decoded.rd; let imm_i = decoded.imm_i(); let mut br_cond = |cond| -> u32 { - rd = 0; if cond { new_pc = pc.wrapping_add(decoded.imm_b()); } @@ -708,7 +703,7 @@ impl Emulator { if !new_pc.is_aligned() { return ctx.trap(TrapCause::InstructionAddressMisaligned); } - ctx.store_register(rd as usize, out)?; + ctx.store_register(decoded.rd_or_null() as usize, out)?; ctx.set_pc(new_pc); Ok(true) } @@ -760,7 +755,7 @@ impl Emulator { } _ => unreachable!(), }; - ctx.store_register(decoded.rd as usize, out)?; + ctx.store_register(decoded.rd_or_null() as usize, out)?; ctx.set_pc(ctx.get_pc() + WORD_SIZE); Ok(true) } diff --git a/ceno_emul/src/tracer.rs b/ceno_emul/src/tracer.rs index b9423f418..0cb4a6532 100644 --- a/ceno_emul/src/tracer.rs +++ b/ceno_emul/src/tracer.rs @@ -214,7 +214,7 @@ impl StepRecord { previous_cycle, }), rd: rd.map(|rd| WriteOp { - addr: CENO_PLATFORM.register_vma(insn.rd() as RegIdx).into(), + addr: CENO_PLATFORM.register_vma(insn.rd_or_null() as RegIdx).into(), value: rd, previous_cycle, }), diff --git a/ceno_emul/src/vm_state.rs b/ceno_emul/src/vm_state.rs index bff16fe09..fbd8798a4 100644 --- a/ceno_emul/src/vm_state.rs +++ b/ceno_emul/src/vm_state.rs @@ -18,13 +18,17 @@ pub struct VMState { pc: Word, /// Map a word-address (addr/4) to a word. memory: HashMap, - registers: [Word; 32], + registers: [Word; VMState::REG_COUNT], // Termination. halted: bool, tracer: Tracer, } impl VMState { + /// The number of registers that the VM uses. + /// 32 architectural registers + 1 register RD_NULL for dark writes to x0. + pub const REG_COUNT: usize = 32 + 1; + pub fn new(platform: Platform, program: Program) -> Self { let pc = program.entry; let program = Arc::new(program); @@ -34,7 +38,7 @@ impl VMState { platform, program: program.clone(), memory: HashMap::new(), - registers: [0; 32], + registers: [0; VMState::REG_COUNT], halted: false, tracer: Tracer::new(), }; diff --git a/ceno_zkvm/src/instructions/riscv/b_insn.rs b/ceno_zkvm/src/instructions/riscv/b_insn.rs index 2edd1e5b6..18d847263 100644 --- a/ceno_zkvm/src/instructions/riscv/b_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/b_insn.rs @@ -61,7 +61,7 @@ impl BInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), insn_kind.codes().opcode.into(), - 0.into(), + None, insn_kind.codes().func3.into(), rs1.id.expr(), rs2.id.expr(), diff --git a/ceno_zkvm/src/instructions/riscv/ecall_insn.rs b/ceno_zkvm/src/instructions/riscv/ecall_insn.rs index d409b288a..9541c879f 100644 --- a/ceno_zkvm/src/instructions/riscv/ecall_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/ecall_insn.rs @@ -40,7 +40,7 @@ impl EcallInstructionConfig { cb.lk_fetch(&InsnRecord::new( pc.expr(), (EANY.codes().opcode as usize).into(), - 0.into(), + None, (EANY.codes().func3 as usize).into(), 0.into(), 0.into(), diff --git a/ceno_zkvm/src/instructions/riscv/i_insn.rs b/ceno_zkvm/src/instructions/riscv/i_insn.rs index 4a099477b..708bd189f 100644 --- a/ceno_zkvm/src/instructions/riscv/i_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/i_insn.rs @@ -46,7 +46,7 @@ impl IInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), insn_kind.codes().opcode.into(), - rd.id.expr(), + Some(rd.id.expr()), insn_kind.codes().func3.into(), rs1.id.expr(), 0.into(), diff --git a/ceno_zkvm/src/instructions/riscv/im_insn.rs b/ceno_zkvm/src/instructions/riscv/im_insn.rs index 0977dfa55..2a29df3e0 100644 --- a/ceno_zkvm/src/instructions/riscv/im_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/im_insn.rs @@ -46,7 +46,7 @@ impl IMInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - rd.id.expr(), + Some(rd.id.expr()), (insn_kind.codes().func3 as usize).into(), rs1.id.expr(), 0.into(), diff --git a/ceno_zkvm/src/instructions/riscv/insn_base.rs b/ceno_zkvm/src/instructions/riscv/insn_base.rs index cd799c29a..42d1b9cbd 100644 --- a/ceno_zkvm/src/instructions/riscv/insn_base.rs +++ b/ceno_zkvm/src/instructions/riscv/insn_base.rs @@ -223,7 +223,7 @@ impl WriteRD { lk_multiplicity: &mut LkMultiplicity, step: &StepRecord, ) -> Result<(), ZKVMError> { - set_val!(instance, self.id, step.insn().rd() as u64); + set_val!(instance, self.id, step.insn().rd_or_null() as u64); set_val!(instance, self.prev_ts, step.rd().unwrap().previous_cycle); // Register state diff --git a/ceno_zkvm/src/instructions/riscv/j_insn.rs b/ceno_zkvm/src/instructions/riscv/j_insn.rs index 1ffec5b99..38eca5b5d 100644 --- a/ceno_zkvm/src/instructions/riscv/j_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/j_insn.rs @@ -42,7 +42,7 @@ impl JInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - rd.id.expr(), + Some(rd.id.expr()), 0.into(), 0.into(), 0.into(), diff --git a/ceno_zkvm/src/instructions/riscv/r_insn.rs b/ceno_zkvm/src/instructions/riscv/r_insn.rs index c5a19cbac..b7e10418d 100644 --- a/ceno_zkvm/src/instructions/riscv/r_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/r_insn.rs @@ -45,7 +45,7 @@ impl RInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), insn_kind.codes().opcode.into(), - rd.id.expr(), + Some(rd.id.expr()), insn_kind.codes().func3.into(), rs1.id.expr(), rs2.id.expr(), diff --git a/ceno_zkvm/src/instructions/riscv/s_insn.rs b/ceno_zkvm/src/instructions/riscv/s_insn.rs index 702a3d5ea..8d27b4f88 100644 --- a/ceno_zkvm/src/instructions/riscv/s_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/s_insn.rs @@ -45,7 +45,7 @@ impl SInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - 0.into(), + None, (insn_kind.codes().func3 as usize).into(), rs1.id.expr(), rs2.id.expr(), diff --git a/ceno_zkvm/src/instructions/riscv/u_insn.rs b/ceno_zkvm/src/instructions/riscv/u_insn.rs index 1c6d7040e..098be43f1 100644 --- a/ceno_zkvm/src/instructions/riscv/u_insn.rs +++ b/ceno_zkvm/src/instructions/riscv/u_insn.rs @@ -40,7 +40,7 @@ impl UInstructionConfig { circuit_builder.lk_fetch(&InsnRecord::new( vm_state.pc.expr(), (insn_kind.codes().opcode as usize).into(), - rd.id.expr(), + Some(rd.id.expr()), 0.into(), 0.into(), 0.into(), diff --git a/ceno_zkvm/src/tables/program.rs b/ceno_zkvm/src/tables/program.rs index d5b629957..33c7ad16b 100644 --- a/ceno_zkvm/src/tables/program.rs +++ b/ceno_zkvm/src/tables/program.rs @@ -34,7 +34,11 @@ macro_rules! declare_program { pub struct InsnRecord([T; 7]); impl InsnRecord { - pub fn new(pc: T, opcode: T, rd: T, funct3: T, rs1: T, rs2: T, imm_or_funct7: T) -> Self { + pub fn new(pc: T, opcode: T, rd: Option, funct3: T, rs1: T, rs2: T, imm_or_funct7: T) -> Self + where + T: From, + { + let rd = rd.unwrap_or_else(|| T::from(DecodedInstruction::RD_NULL)); InsnRecord([pc, opcode, rd, funct3, rs1, rs2, imm_or_funct7]) } @@ -50,7 +54,7 @@ impl InsnRecord { &self.0[1] } - pub fn rd_or_zero(&self) -> &T { + pub fn rd_or_null(&self) -> &T { &self.0[2] } @@ -80,15 +84,15 @@ impl InsnRecord { impl InsnRecord { fn from_decoded(pc: u32, insn: &DecodedInstruction) -> Self { - InsnRecord::new( + InsnRecord([ pc, insn.opcode(), - insn.rd_or_zero(), + insn.rd_or_null(), insn.funct3_or_zero(), insn.rs1_or_zero(), insn.rs2_or_zero(), insn.imm_or_funct7(), - ) + ]) } /// Interpret the immediate or funct7 as unsigned or signed depending on the instruction. diff --git a/ceno_zkvm/src/tables/ram.rs b/ceno_zkvm/src/tables/ram.rs index decd52608..51c844363 100644 --- a/ceno_zkvm/src/tables/ram.rs +++ b/ceno_zkvm/src/tables/ram.rs @@ -1,4 +1,4 @@ -use ceno_emul::{Addr, CENO_PLATFORM, WORD_SIZE, Word}; +use ceno_emul::{Addr, CENO_PLATFORM, VMState, WORD_SIZE, Word}; use ram_circuit::RamTableCircuit; use crate::{instructions::riscv::constants::UINT_LIMBS, structs::RAMType}; @@ -34,7 +34,7 @@ impl RamTable for RegTable { const V_LIMBS: usize = UINT_LIMBS; // See `RegisterExpr`. fn len() -> usize { - 32 // register size 32 + VMState::REG_COUNT } fn addr(entry_index: usize) -> Addr {