diff --git a/Makefile.toml b/Makefile.toml index 027f51d2c..2a4a079a2 100644 --- a/Makefile.toml +++ b/Makefile.toml @@ -11,6 +11,10 @@ CUR_TARGET = { script = [''' '''] } RAYON_NUM_THREADS = "${CORE}" +[tasks.build] +# Override the default `--all-features`, that's broken, because some of our features are mutually exclusive. +args = ["build"] + [tasks.tests] args = [ "test", diff --git a/README.md b/README.md index 7f3e6b106..70f435371 100644 --- a/README.md +++ b/README.md @@ -1,47 +1,38 @@ -# Ceno: Non-uniform, Segment and Parallel Zero-knowledge Virtual Machine - -Please see [the paper](https://eprint.iacr.org/2024/387) for an introduction to Ceno. - -# MVP -step 1 -- non-uniform prover end to end - - no recursion - - no PCS - - with IOP - - with lookup - - with Frontend + VM - -step 2 -- introduce PCS - -step 3 -- recursion and achieve uniformality - -# Building blocks -- hash function - - - [ ] decision: start with 8-4 first - -- IOP - - lookup - - [ ] logup: spec @wenqing - - [ ] implement as an IOP module along with high degree gate - - high degree gates - - [ ] paper/spec @tianyi - - one on one tianyi/zhenfei - -- PCS - -- gates/subcircuits - - spec - - example by tianyi - - -option 1 -- repeat sumcheck twice/three times -option 2 -- use F_q^2/3 extension field, do not repeat -- rule of thumb: n rounds, soundness ~ (64-n) bits +# Ceno: Non-uniform, Segment and Parallel Risc-V Zero-knowledge Virtual Machine + +Please see [the slightly outdated paper](https://eprint.iacr.org/2024/387) for an introduction to Ceno. + +🚧 This project is currently under construction and not suitable for use in production. 🚧 + +If you are unfamiliar with the RISC-V instruction set, please have a look at the [RISC-V instruction set reference](https://github.com/jameslzhu/riscv-card/blob/master/riscv-card.pdf). + +## Local build requirements + +Ceno is built in Rust, so [installing the Rust toolchain](https://www.rust-lang.org/tools/install) is a pre-requisite, if you want to develop on your local machine. We also use [cargo-make](https://sagiegurari.github.io/cargo-make/) to build Ceno. You can install cargo-make with the following command: + +```sh +cargo install cargo-make +``` + +You will also need to install the Risc-V target for Rust. You can do this with the following command: + +```sh +rustup target add riscv32im-unknown-none-elf +``` + +## Building Ceno and running tests + +To run the tests, you can use the following command: + +```sh +cargo make tests +``` + +Clippy and check work as usual: + +```sh +cargo check +cargo clippy +``` + +Alas, `cargo build` doesn't work. That's a known problem and we're working on it. Please use `cargo make build` instead for now. diff --git a/ceno_emul/src/lib.rs b/ceno_emul/src/lib.rs index f32e462f1..628c75b7c 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, InsnCodes, InsnKind}; +pub use rv32im::{DecodedInstruction, EmuContext, InsnCodes, InsnKind}; mod elf; pub use elf::Program; diff --git a/ceno_emul/src/platform.rs b/ceno_emul/src/platform.rs index e58dd2687..511981ba0 100644 --- a/ceno_emul/src/platform.rs +++ b/ceno_emul/src/platform.rs @@ -98,11 +98,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 { @@ -154,6 +149,7 @@ impl Platform { #[cfg(test)] mod tests { use super::*; + use crate::VMState; #[test] fn test_no_overlap() { @@ -165,7 +161,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..17749e03a 100644 --- a/ceno_emul/src/rv32im.rs +++ b/ceno_emul/src/rv32im.rs @@ -24,9 +24,6 @@ pub trait EmuContext { // Handle environment call fn ecall(&mut self) -> Result; - // Handle a machine return - fn mret(&self) -> Result; - // Handle a trap fn trap(&self, cause: TrapCause) -> Result; @@ -104,6 +101,7 @@ pub enum TrapCause { pub struct DecodedInstruction { insn: u32, top_bit: u32, + // The bit fields of the instruction encoding, regardless of the instruction format. func7: u32, rs2: u32, rs1: u32, @@ -113,8 +111,9 @@ pub struct DecodedInstruction { } #[derive(Clone, Copy, Debug)] -pub enum InsnCategory { +enum InsnCategory { Compute, + Branch, Load, Store, System, @@ -182,8 +181,8 @@ pub enum InsnKind { SB, SH, SW, + /// ECALL and EBREAK etc. EANY, - MRET, } use InsnKind::*; @@ -204,6 +203,9 @@ pub struct InsnCodes { } impl DecodedInstruction { + /// A virtual register which absorbs the writes to x0. + pub const RD_NULL: u32 = 32; + pub fn new(insn: u32) -> Self { Self { insn, @@ -225,24 +227,15 @@ 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 { + /// The internal register destination. It is either the regular rd, or an internal RD_NULL if + /// the instruction does not write to a register or writes to x0. + pub fn rd_internal(&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, } } - /// Get the funct3 field, regardless of the instruction format. - pub fn funct3(&self) -> u32 { - self.func3 - } - /// Get the funct3 field, or zero if the instruction does not use funct3. pub fn funct3_or_zero(&self) -> u32 { match self.codes().format { @@ -277,68 +270,64 @@ impl DecodedInstruction { } } - /// Get the funct7 field, regardless of the instruction format. - pub fn funct7(&self) -> u32 { - self.func7 - } - /// Get the decoded immediate, or 2^shift, or the funct7 field, depending on the instruction format. pub fn imm_or_funct7(&self) -> u32 { - match self.codes() { - InsnCodes { format: R, .. } => self.func7, - InsnCodes { - kind: SLLI | SRLI | SRAI, - .. - } => 1 << self.rs2(), // decode the shift as a multiplication by 2.pow(rs2) - InsnCodes { format: I, .. } => self.imm_i(), - InsnCodes { format: S, .. } => self.imm_s(), - InsnCodes { format: B, .. } => self.imm_b(), - InsnCodes { format: U, .. } => self.imm_u(), - InsnCodes { format: J, .. } => self.imm_j(), + match self.codes().format { + R => self.func7, + I => match self.codes().kind { + // decode the shift as a multiplication/division by 1 << immediate + SLLI | SRLI | SRAI => 1 << self.imm_shamt(), + _ => self.imm_i(), + }, + S => self.imm_s(), + B => self.imm_b(), + U => self.imm_u(), + J => self.imm_j(), } } - /// Indicate whether the immediate is interpreted as a signed integer, and it is negative. - pub fn imm_is_negative(&self) -> bool { + /// Indicates if the immediate value, when signed, needs to be encoded as field negative. + /// example: + /// imm = ux::MAX - 1 implies + /// imm_field = FIELD_MODULUS - 1 if imm_field_is_negative + /// imm_field = ux::MAX - 1 otherwise + /// see InsnRecord::imm_or_funct7_field + pub fn imm_field_is_negative(&self) -> bool { match self.codes() { InsnCodes { format: R | U, .. } => false, InsnCodes { - kind: SLLI | SRLI | SRAI | ADDI, + kind: SLLI | SRLI | SRAI | ADDI | SLTIU, .. } => false, _ => self.top_bit != 0, } } - pub fn sign_bit(&self) -> u32 { - self.top_bit - } - pub fn codes(&self) -> InsnCodes { FastDecodeTable::get().lookup(self) } - pub fn kind(&self) -> (InsnCategory, InsnKind) { - let i = FastDecodeTable::get().lookup(self); - (i.category, i.kind) - } - - pub fn imm_b(&self) -> u32 { + fn imm_b(&self) -> u32 { (self.top_bit * 0xfffff000) | ((self.rd & 1) << 11) | ((self.func7 & 0x3f) << 5) | (self.rd & 0x1e) } - pub fn imm_i(&self) -> u32 { - (self.top_bit * 0xfffff000) | (self.func7 << 5) | self.rs2 + fn imm_i(&self) -> u32 { + (self.top_bit * 0xffff_f000) | (self.func7 << 5) | self.rs2 } - pub fn imm_s(&self) -> u32 { + /// Shift amount field of SLLI, SRLI, SRAI. + fn imm_shamt(&self) -> u32 { + self.rs2 + } + + fn imm_s(&self) -> u32 { (self.top_bit * 0xfffff000) | (self.func7 << 5) | self.rd } - pub fn imm_j(&self) -> u32 { + fn imm_j(&self) -> u32 { (self.top_bit * 0xfff00000) | (self.rs1 << 15) | (self.func3 << 12) @@ -347,7 +336,7 @@ impl DecodedInstruction { | (self.rs2 & 0x1e) } - pub fn imm_u(&self) -> u32 { + fn imm_u(&self) -> u32 { self.insn & 0xfffff000 } } @@ -397,7 +386,7 @@ const fn insn( } } -type InstructionTable = [InsnCodes; 48]; +type InstructionTable = [InsnCodes; 47]; type FastInstructionTable = [u8; 1 << 10]; const RV32IM_ISA: InstructionTable = [ @@ -421,12 +410,12 @@ const RV32IM_ISA: InstructionTable = [ insn(I, SRAI, Compute, 0x13, 0x5, 0x20), insn(I, SLTI, Compute, 0x13, 0x2, -1), insn(I, SLTIU, Compute, 0x13, 0x3, -1), - insn(B, BEQ, Compute, 0x63, 0x0, -1), - insn(B, BNE, Compute, 0x63, 0x1, -1), - insn(B, BLT, Compute, 0x63, 0x4, -1), - insn(B, BGE, Compute, 0x63, 0x5, -1), - insn(B, BLTU, Compute, 0x63, 0x6, -1), - insn(B, BGEU, Compute, 0x63, 0x7, -1), + insn(B, BEQ, Branch, 0x63, 0x0, -1), + insn(B, BNE, Branch, 0x63, 0x1, -1), + insn(B, BLT, Branch, 0x63, 0x4, -1), + insn(B, BGE, Branch, 0x63, 0x5, -1), + insn(B, BLTU, Branch, 0x63, 0x6, -1), + insn(B, BGEU, Branch, 0x63, 0x7, -1), insn(J, JAL, Compute, 0x6f, -1, -1), insn(I, JALR, Compute, 0x67, 0x0, -1), insn(U, LUI, Compute, 0x37, -1, -1), @@ -448,7 +437,6 @@ const RV32IM_ISA: InstructionTable = [ insn(S, SH, Store, 0x23, 0x1, -1), insn(S, SW, Store, 0x23, 0x2, -1), insn(I, EANY, System, 0x73, 0x0, 0x00), - insn(I, MRET, System, 0x73, 0x0, 0x18), ]; #[cfg(test)] @@ -560,6 +548,7 @@ impl Emulator { if match insn.category { InsnCategory::Compute => self.step_compute(ctx, insn.kind, &decoded)?, + InsnCategory::Branch => self.step_branch(ctx, insn.kind, &decoded)?, InsnCategory::Load => self.step_load(ctx, insn.kind, &decoded)?, InsnCategory::Store => self.step_store(ctx, insn.kind, &decoded)?, InsnCategory::System => self.step_system(ctx, insn.kind, &decoded)?, @@ -581,15 +570,7 @@ 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()); - } - 0 - }; let out = match kind { // Instructions that do not read rs1 nor rs2. JAL => { @@ -657,12 +638,6 @@ impl Emulator { 0 } } - BEQ => br_cond(rs1 == rs2), - BNE => br_cond(rs1 != rs2), - BLT => br_cond((rs1 as i32) < (rs2 as i32)), - BGE => br_cond((rs1 as i32) >= (rs2 as i32)), - BLTU => br_cond(rs1 < rs2), - BGEU => br_cond(rs1 >= rs2), MUL => rs1.wrapping_mul(rs2), MULH => { (sign_extend_u32(rs1).wrapping_mul(sign_extend_u32(rs2)) >> 32) @@ -708,7 +683,42 @@ impl Emulator { if !new_pc.is_aligned() { return ctx.trap(TrapCause::InstructionAddressMisaligned); } - ctx.store_register(rd as usize, out)?; + ctx.store_register(decoded.rd_internal() as usize, out)?; + ctx.set_pc(new_pc); + Ok(true) + } + + fn step_branch( + &self, + ctx: &mut M, + kind: InsnKind, + decoded: &DecodedInstruction, + ) -> Result { + use InsnKind::*; + + let pc = ctx.get_pc(); + let rs1 = ctx.load_register(decoded.rs1 as RegIdx)?; + let rs2 = ctx.load_register(decoded.rs2 as RegIdx)?; + + let taken = match kind { + BEQ => rs1 == rs2, + BNE => rs1 != rs2, + BLT => (rs1 as i32) < (rs2 as i32), + BGE => (rs1 as i32) >= (rs2 as i32), + BLTU => rs1 < rs2, + BGEU => rs1 >= rs2, + _ => unreachable!("Illegal branch instruction: {:?}", kind), + }; + + let new_pc = if taken { + pc.wrapping_add(decoded.imm_b()) + } else { + pc + WORD_SIZE + }; + + if !new_pc.is_aligned() { + return ctx.trap(TrapCause::InstructionAddressMisaligned); + } ctx.set_pc(new_pc); Ok(true) } @@ -760,7 +770,7 @@ impl Emulator { } _ => unreachable!(), }; - ctx.store_register(decoded.rd as usize, out)?; + ctx.store_register(decoded.rd_internal() as usize, out)?; ctx.set_pc(ctx.get_pc() + WORD_SIZE); Ok(true) } @@ -819,7 +829,6 @@ impl Emulator { 1 => ctx.trap(TrapCause::Breakpoint), _ => ctx.trap(TrapCause::IllegalInstruction(decoded.insn)), }, - InsnKind::MRET => ctx.mret(), _ => unreachable!(), } } diff --git a/ceno_emul/src/tracer.rs b/ceno_emul/src/tracer.rs index b9423f418..d17e410a5 100644 --- a/ceno_emul/src/tracer.rs +++ b/ceno_emul/src/tracer.rs @@ -214,7 +214,9 @@ 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_internal() 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..5ae155fc8 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(), }; @@ -124,13 +128,6 @@ impl EmuContext for VMState { } } - // No traps are implemented so MRET is not legal. - fn mret(&self) -> Result { - #[allow(clippy::unusual_byte_groupings)] - let mret = 0b001100000010_00000_000_00000_1110011; - self.trap(TrapCause::IllegalInstruction(mret)) - } - fn trap(&self, cause: TrapCause) -> Result { Err(anyhow!("Trap {:?}", cause)) // Crash. } diff --git a/ceno_emul/tests/test_vm_trace.rs b/ceno_emul/tests/test_vm_trace.rs index c01977823..3f6b00cd6 100644 --- a/ceno_emul/tests/test_vm_trace.rs +++ b/ceno_emul/tests/test_vm_trace.rs @@ -33,7 +33,7 @@ fn test_vm_trace() -> Result<()> { assert_eq!(ctx.peek_register(2), x2); assert_eq!(ctx.peek_register(3), x3); - let ops: Vec = steps.iter().map(|step| step.insn().kind().1).collect(); + let ops: Vec = steps.iter().map(|step| step.insn().codes().kind).collect(); assert_eq!(ops, expected_ops_fibonacci_20()); assert_eq!( diff --git a/ceno_zkvm/.gitignore b/ceno_zkvm/.gitignore index 8db038a03..b38ddc923 100644 --- a/ceno_zkvm/.gitignore +++ b/ceno_zkvm/.gitignore @@ -1 +1,2 @@ tracing.folded +.tmp* diff --git a/ceno_zkvm/examples/riscv_opcodes.rs b/ceno_zkvm/examples/riscv_opcodes.rs index 438c3cfb8..a274134ce 100644 --- a/ceno_zkvm/examples/riscv_opcodes.rs +++ b/ceno_zkvm/examples/riscv_opcodes.rs @@ -30,7 +30,7 @@ use tracing_flame::FlameLayer; use tracing_subscriber::{EnvFilter, Registry, fmt, layer::SubscriberExt}; use transcript::Transcript; -const PROGRAM_SIZE: usize = 512; +const PROGRAM_SIZE: usize = 16; // For now, we assume registers // - x0 is not touched, // - x1 is initialized to 1, @@ -118,7 +118,7 @@ fn main() { zkvm_fixed_traces.register_table_circuit::>( &zkvm_cs, - prog_config.clone(), + &prog_config, &program, ); @@ -196,11 +196,20 @@ fn main() { .iter() .map(|rec| { let index = rec.addr as usize; - let vma: WordAddr = CENO_PLATFORM.register_vma(index).into(); - MemFinalRecord { - addr: rec.addr, - value: vm.peek_register(index), - cycle: *final_access.get(&vma).unwrap_or(&0), + if index < VMState::REG_COUNT { + let vma: WordAddr = CENO_PLATFORM.register_vma(index).into(); + MemFinalRecord { + addr: rec.addr, + value: vm.peek_register(index), + cycle: *final_access.get(&vma).unwrap_or(&0), + } + } else { + // The table is padded beyond the number of registers. + MemFinalRecord { + addr: rec.addr, + value: 0, + cycle: 0, + } } }) .collect_vec(); diff --git a/ceno_zkvm/src/circuit_builder.rs b/ceno_zkvm/src/circuit_builder.rs index cb326d345..acacc6024 100644 --- a/ceno_zkvm/src/circuit_builder.rs +++ b/ceno_zkvm/src/circuit_builder.rs @@ -73,7 +73,7 @@ pub struct LogupTableExpression { pub table_len: usize, } -// TODO encaptulate few information of table spec to SetTableAddrType value +// TODO encapsulate few information of table spec to SetTableAddrType value // once confirm syntax is friendly and parsed by recursive verifier #[derive(Clone, Debug)] pub enum SetTableAddrType { 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..64ac91b12 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_internal() 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/jump/jalr.rs b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs index a80e11c4a..39ee50458 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/jalr.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/jalr.rs @@ -7,7 +7,7 @@ use crate::{ Value, circuit_builder::CircuitBuilder, error::ZKVMError, - expression::{ToExpr, WitIn}, + expression::{Expression, ToExpr, WitIn}, instructions::{ Instruction, riscv::{constants::UInt, i_insn::IInstructionConfig, insn_base::MemAddr}, @@ -23,7 +23,7 @@ pub struct JalrConfig { pub rs1_read: UInt, pub imm: WitIn, pub next_pc_addr: MemAddr, - pub overflow: WitIn, + pub overflow: Option<(WitIn, WitIn)>, pub rd_written: UInt, } @@ -63,17 +63,25 @@ impl Instruction for JalrInstruction { // 3. next_pc = next_pc_addr aligned to even value (round down) let next_pc_addr = MemAddr::::construct_unaligned(circuit_builder)?; - let overflow = circuit_builder.create_witin(|| "overflow"); + + let (overflow_expr, overflow) = if cfg!(feature = "forbid_overflow") { + (Expression::ZERO, None) + } else { + let overflow = circuit_builder.create_witin(|| "overflow"); + let tmp = circuit_builder.create_witin(|| "overflow1"); + circuit_builder.require_zero(|| "overflow_0_or_pm1", overflow.expr() * tmp.expr())?; + circuit_builder.require_equal( + || "overflow_tmp", + tmp.expr(), + (1 - overflow.expr()) * (1 + overflow.expr()), + )?; + (overflow.expr(), Some((overflow, tmp))) + }; circuit_builder.require_equal( || "rs1+imm = next_pc_unrounded + overflow*2^32", rs1_read.value() + imm.expr(), - next_pc_addr.expr_unaligned() + overflow.expr() * (1u64 << 32), - )?; - - circuit_builder.require_zero( - || "overflow_0_or_pm1", - overflow.expr() * (overflow.expr() - 1) * (overflow.expr() + 1), + next_pc_addr.expr_unaligned() + overflow_expr * (1u64 << 32), )?; circuit_builder.require_equal( @@ -126,12 +134,18 @@ impl Instruction for JalrInstruction { config .next_pc_addr .assign_instance(instance, lk_multiplicity, sum)?; - let overflow: E::BaseField = match (overflowing, imm < 0) { - (false, _) => E::BaseField::ZERO, - (true, false) => E::BaseField::ONE, - (true, true) => -E::BaseField::ONE, - }; - set_val!(instance, config.overflow, overflow); + + if let Some((overflow_cfg, tmp_cfg)) = &config.overflow { + let (overflow, tmp) = match (overflowing, imm < 0) { + (false, _) => (E::BaseField::ZERO, E::BaseField::ONE), + (true, false) => (E::BaseField::ONE, E::BaseField::ZERO), + (true, true) => (-E::BaseField::ONE, E::BaseField::ZERO), + }; + set_val!(instance, overflow_cfg, overflow); + set_val!(instance, tmp_cfg, tmp); + } else { + assert!(!overflowing, "overflow not allowed in JALR"); + } config .i_insn diff --git a/ceno_zkvm/src/instructions/riscv/jump/test.rs b/ceno_zkvm/src/instructions/riscv/jump/test.rs index 887db8da3..4453f4c3a 100644 --- a/ceno_zkvm/src/instructions/riscv/jump/test.rs +++ b/ceno_zkvm/src/instructions/riscv/jump/test.rs @@ -62,7 +62,7 @@ fn test_opcode_jalr() { .unwrap(); let imm = -15i32; - let rs1_read: Word = 10u32; + let rs1_read: Word = 100u32; let new_pc: ByteAddr = ByteAddr(rs1_read.wrapping_add_signed(imm) & (!1)); let insn_code = encode_rv32(InsnKind::JALR, 2, 0, 4, imm as u32); 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/rv32im.rs b/ceno_zkvm/src/instructions/riscv/rv32im.rs index f318a3ec6..54d3d09f5 100644 --- a/ceno_zkvm/src/instructions/riscv/rv32im.rs +++ b/ceno_zkvm/src/instructions/riscv/rv32im.rs @@ -98,18 +98,18 @@ impl Rv32imConfig { fixed.register_opcode_circuit::>(cs); fixed.register_opcode_circuit::>(cs); - fixed.register_table_circuit::>(cs, self.u16_range_config.clone(), &()); - fixed.register_table_circuit::>(cs, self.u14_range_config.clone(), &()); - fixed.register_table_circuit::>(cs, self.and_config.clone(), &()); - fixed.register_table_circuit::>(cs, self.ltu_config.clone(), &()); + fixed.register_table_circuit::>(cs, &self.u16_range_config, &()); + fixed.register_table_circuit::>(cs, &self.u14_range_config, &()); + fixed.register_table_circuit::>(cs, &self.and_config, &()); + fixed.register_table_circuit::>(cs, &self.ltu_config, &()); - fixed.register_table_circuit::>(cs, self.reg_config.clone(), reg_init); + fixed.register_table_circuit::>(cs, &self.reg_config, reg_init); fixed.register_table_circuit::>( cs, - self.program_data_config.clone(), + &self.program_data_config, program_data_init, ); - fixed.register_table_circuit::>(cs, self.public_io_config.clone(), &()); + fixed.register_table_circuit::>(cs, &self.public_io_config, &()); } pub fn assign_opcode_circuit( 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/slti.rs b/ceno_zkvm/src/instructions/riscv/slti.rs index 71d0bb26f..cc80d629b 100644 --- a/ceno_zkvm/src/instructions/riscv/slti.rs +++ b/ceno_zkvm/src/instructions/riscv/slti.rs @@ -4,6 +4,7 @@ use ceno_emul::{InsnKind, SWord, StepRecord, Word}; use ff_ext::ExtensionField; use super::{ + RIVInstruction, constants::{UINT_LIMBS, UInt}, i_insn::IInstructionConfig, }; @@ -21,25 +22,36 @@ use crate::{ use core::mem::MaybeUninit; #[derive(Debug)] -pub struct InstructionConfig { +pub struct SetLessThanImmConfig { i_insn: IInstructionConfig, rs1_read: UInt, imm: WitIn, #[allow(dead_code)] rd_written: UInt, - - is_rs1_neg: IsLtConfig, lt: IsLtConfig, + + // SLTI + is_rs1_neg: Option, } -pub struct SltiInstruction(PhantomData); +pub struct SetLessThanImmInstruction(PhantomData<(E, I)>); -impl Instruction for SltiInstruction { - type InstructionConfig = InstructionConfig; +pub struct SltiOp; +impl RIVInstruction for SltiOp { + const INST_KIND: ceno_emul::InsnKind = ceno_emul::InsnKind::SLTI; +} + +pub struct SltiuOp; +impl RIVInstruction for SltiuOp { + const INST_KIND: ceno_emul::InsnKind = ceno_emul::InsnKind::SLTIU; +} + +impl Instruction for SetLessThanImmInstruction { + type InstructionConfig = SetLessThanImmConfig; fn name() -> String { - format!("{:?}", InsnKind::SLTI) + format!("{:?}", I::INST_KIND) } fn construct_circuit(cb: &mut CircuitBuilder) -> Result { @@ -47,34 +59,37 @@ impl Instruction for SltiInstruction { let rs1_read = UInt::new_unchecked(|| "rs1_read", cb)?; let imm = cb.create_witin(|| "imm"); - let max_signed_limb_expr: Expression<_> = ((1 << (UInt::::LIMB_BITS - 1)) - 1).into(); - let is_rs1_neg = IsLtConfig::construct_circuit( - cb, - || "lhs_msb", - max_signed_limb_expr, - rs1_read.limbs.iter().last().unwrap().expr(), // msb limb - 1, - )?; + let (value_expr, is_rs1_neg) = match I::INST_KIND { + InsnKind::SLTIU => (rs1_read.value(), None), + InsnKind::SLTI => { + let max_signed_limb_expr: Expression<_> = + ((1 << (UInt::::LIMB_BITS - 1)) - 1).into(); + let is_rs1_neg = IsLtConfig::construct_circuit( + cb, + || "lhs_msb", + max_signed_limb_expr, + rs1_read.limbs.iter().last().unwrap().expr(), // msb limb + 1, + )?; + (rs1_read.to_field_expr(is_rs1_neg.expr()), Some(is_rs1_neg)) + } + _ => unreachable!("Unsupported instruction kind {:?}", I::INST_KIND), + }; - let lt = IsLtConfig::construct_circuit( - cb, - || "rs1 < imm", - rs1_read.to_field_expr(is_rs1_neg.expr()), - imm.expr(), - UINT_LIMBS, - )?; + let lt = + IsLtConfig::construct_circuit(cb, || "rs1 < imm", value_expr, imm.expr(), UINT_LIMBS)?; let rd_written = UInt::from_exprs_unchecked(vec![lt.expr()]); let i_insn = IInstructionConfig::::construct_circuit( cb, - InsnKind::SLTI, + I::INST_KIND, &imm.expr(), rs1_read.register_expr(), rd_written.register_expr(), false, )?; - Ok(InstructionConfig { + Ok(SetLessThanImmConfig { i_insn, rs1_read, imm, @@ -98,20 +113,30 @@ impl Instruction for SltiInstruction { config .rs1_read .assign_value(instance, Value::new_unchecked(rs1)); - config.is_rs1_neg.assign_instance( - instance, - lkm, - max_signed_limb, - *rs1_value.limbs.last().unwrap() as u64, - )?; let imm = step.insn().imm_or_funct7(); let imm_field = InsnRecord::imm_or_funct7_field::(&step.insn()); set_val!(instance, config.imm, imm_field); - config - .lt - .assign_instance_signed(instance, lkm, rs1 as SWord, imm as SWord)?; + match I::INST_KIND { + InsnKind::SLTIU => { + config + .lt + .assign_instance(instance, lkm, rs1 as u64, imm as u64)?; + } + InsnKind::SLTI => { + config.is_rs1_neg.as_ref().unwrap().assign_instance( + instance, + lkm, + max_signed_limb, + *rs1_value.limbs.last().unwrap() as u64, + )?; + config + .lt + .assign_instance_signed(instance, lkm, rs1 as SWord, imm as SWord)?; + } + _ => unreachable!("Unsupported instruction kind {:?}", I::INST_KIND), + } Ok(()) } @@ -119,7 +144,7 @@ impl Instruction for SltiInstruction { #[cfg(test)] mod test { - use ceno_emul::{Change, PC_STEP_SIZE, StepRecord, Word, encode_rv32}; + use ceno_emul::{Change, PC_STEP_SIZE, StepRecord, encode_rv32}; use goldilocks::GoldilocksExt2; use rand::Rng; @@ -127,81 +152,120 @@ mod test { use super::*; use crate::{ circuit_builder::{CircuitBuilder, ConstraintSystem}, - instructions::{Instruction, riscv::test_utils::imm_i}, + instructions::Instruction, scheme::mock_prover::{MOCK_PC_START, MockProver}, }; - fn verify(name: &'static str, rs1: i32, imm: i32, rd: Word) { - let mut cs = ConstraintSystem::::new(|| "riscv"); - let mut cb = CircuitBuilder::new(&mut cs); - let config = cb - .namespace( - || format!("SLTI/{name}"), - |cb| { - let config = SltiInstruction::construct_circuit(cb); - Ok(config) - }, - ) - .unwrap() - .unwrap(); - - let insn_code = encode_rv32(InsnKind::SLTI, 2, 0, 4, imm_i(imm)); - let (raw_witin, lkm) = - SltiInstruction::assign_instances(&config, cb.cs.num_witin as usize, vec![ - StepRecord::new_i_instruction( - 3, - Change::new(MOCK_PC_START, MOCK_PC_START + PC_STEP_SIZE), - insn_code, - rs1 as Word, - Change::new(0, rd), - 0, - ), - ]) - .unwrap(); + #[test] + fn test_sltiu_true() { + verify::("lt = true, 0 < 1", 0, 1, 1); + verify::("lt = true, 1 < 2", 1, 2, 1); + verify::("lt = true, 10 < 20", 10, 20, 1); + verify::("lt = true, 0 < imm upper boundary", 0, 2047, 1); + // negative imm is treated as positive + verify::("lt = true, 0 < u32::MAX-1", 0, -1, 1); + verify::("lt = true, 1 < u32::MAX-1", 1, -1, 1); + verify::("lt = true, 0 < imm lower bondary", 0, -2048, 1); + } - let expected_rd_written = - UInt::from_const_unchecked(Value::new_unchecked(rd).as_u16_limbs().to_vec()); - config - .rd_written - .require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written) - .unwrap(); + #[test] + fn test_sltiu_false() { + verify::("lt = false, 1 < 0", 1, 0, 0); + verify::("lt = false, 2 < 1", 2, 1, 0); + verify::("lt = false, 100 < 50", 100, 50, 0); + verify::("lt = false, 500 < 100", 500, 100, 0); + verify::("lt = false, 100000 < 2047", 100000, 2047, 0); + verify::("lt = false, 100000 < 0", 100000, 0, 0); + verify::("lt = false, 0 == 0", 0, 0, 0); + verify::("lt = false, 1 == 1", 1, 1, 0); + verify::("lt = false, imm upper bondary", u32::MAX, 2047, 0); + // negative imm is treated as positive + verify::("lt = false, imm lower bondary", u32::MAX, -2048, 0); + } - MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm)); + #[test] + fn test_sltiu_random() { + let mut rng = rand::thread_rng(); + let a: u32 = rng.gen::(); + let b: i32 = rng.gen_range(-2048..2048); + println!("random: {} ("random unsigned comparison", a, b, (a < (b as u32)) as u32); } #[test] fn test_slti_true() { - verify("lt = true, 0 < 1", 0, 1, 1); - verify("lt = true, 1 < 2", 1, 2, 1); - verify("lt = true, -1 < 0", -1, 0, 1); - verify("lt = true, -1 < 1", -1, 1, 1); - verify("lt = true, -2 < -1", -2, -1, 1); + verify::("lt = true, 0 < 1", 0, 1, 1); + verify::("lt = true, 1 < 2", 1, 2, 1); + verify::("lt = true, -1 < 0", -1i32 as u32, 0, 1); + verify::("lt = true, -1 < 1", -1i32 as u32, 1, 1); + verify::("lt = true, -2 < -1", -2i32 as u32, -1, 1); // -2048 <= imm <= 2047 - verify("lt = true, imm upper bondary", i32::MIN, 2047, 1); - verify("lt = true, imm lower bondary", i32::MIN, -2048, 1); + verify::("lt = true, imm upper bondary", i32::MIN as u32, 2047, 1); + verify::("lt = true, imm lower bondary", i32::MIN as u32, -2048, 1); } #[test] fn test_slti_false() { - verify("lt = false, 1 < 0", 1, 0, 0); - verify("lt = false, 2 < 1", 2, 1, 0); - verify("lt = false, 0 < -1", 0, -1, 0); - verify("lt = false, 1 < -1", 1, -1, 0); - verify("lt = false, -1 < -2", -1, -2, 0); - verify("lt = false, 0 == 0", 0, 0, 0); - verify("lt = false, 1 == 1", 1, 1, 0); - verify("lt = false, -1 == -1", -1, -1, 0); + verify::("lt = false, 1 < 0", 1, 0, 0); + verify::("lt = false, 2 < 1", 2, 1, 0); + verify::("lt = false, 0 < -1", 0, -1, 0); + verify::("lt = false, 1 < -1", 1, -1, 0); + verify::("lt = false, -1 < -2", -1i32 as u32, -2, 0); + verify::("lt = false, 0 == 0", 0, 0, 0); + verify::("lt = false, 1 == 1", 1, 1, 0); + verify::("lt = false, -1 == -1", -1i32 as u32, -1, 0); // -2048 <= imm <= 2047 - verify("lt = false, imm upper bondary", i32::MAX, 2047, 0); - verify("lt = false, imm lower bondary", i32::MAX, -2048, 0); + verify::("lt = false, imm upper bondary", i32::MAX as u32, 2047, 0); + verify::("lt = false, imm lower bondary", i32::MAX as u32, -2048, 0); } #[test] fn test_slti_random() { let mut rng = rand::thread_rng(); let a: i32 = rng.gen(); - let b: i32 = rng.gen::() % 2048; + let b: i32 = rng.gen_range(-2048..2048); println!("random: {} ("random 1", a as u32, b, (a < b) as u32); + } + + fn verify(name: &'static str, rs1_read: u32, imm: i32, expected_rd: u32) { + let mut cs = ConstraintSystem::::new(|| "riscv"); + let mut cb = CircuitBuilder::new(&mut cs); + + let insn_code = encode_rv32(I::INST_KIND, 2, 0, 4, imm as u32); + + let config = cb + .namespace( + || format!("{:?}_({name})", I::INST_KIND), + SetLessThanImmInstruction::::construct_circuit, + ) + .unwrap(); + + let (raw_witin, lkm) = SetLessThanImmInstruction::::assign_instances( + &config, + cb.cs.num_witin as usize, + vec![StepRecord::new_i_instruction( + 3, + Change::new(MOCK_PC_START, MOCK_PC_START + PC_STEP_SIZE), + insn_code, + rs1_read, + Change::new(0, expected_rd), + 0, + )], + ) + .unwrap(); + + let expected_rd = + UInt::from_const_unchecked(Value::new_unchecked(expected_rd).as_u16_limbs().to_vec()); + config + .rd_written + .require_equal( + || format!("{:?}_({name})_assert_rd_written", I::INST_KIND), + &mut cb, + &expected_rd, + ) + .unwrap(); + + MockProver::assert_satisfied_raw(&cb, raw_witin, &[insn_code], None, Some(lkm)); } } 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/scheme/mock_prover.rs b/ceno_zkvm/src/scheme/mock_prover.rs index 74fe11006..92a43aa4e 100644 --- a/ceno_zkvm/src/scheme/mock_prover.rs +++ b/ceno_zkvm/src/scheme/mock_prover.rs @@ -30,6 +30,7 @@ use std::{ }; use strum::IntoEnumIterator; +const MAX_CONSTRAINT_DEGREE: usize = 2; const MOCK_PROGRAM_SIZE: usize = 32; pub const MOCK_PC_START: ByteAddr = ByteAddr(CENO_PLATFORM.pc_base()); @@ -50,6 +51,11 @@ pub(crate) enum MockProverError { name: String, inst_id: usize, }, + DegreeTooHigh { + expression: Expression, + degree: usize, + name: String, + }, LookupError { expression: Expression, evaluated: E, @@ -178,6 +184,18 @@ impl MockProverError { Inst[{inst_id}]:\n{wtns_fmt}\n", ); } + Self::DegreeTooHigh { + expression, + degree, + name, + } => { + let expression_fmt = fmt::expr(expression, &mut wtns, false); + println!( + "\nDegreeTooHigh {name:?}: Expression degree is too high\n\ + Expression: {expression_fmt}\n\ + Degree: {degree} > {MAX_CONSTRAINT_DEGREE}\n", + ); + } Self::LookupError { expression, evaluated, @@ -251,6 +269,7 @@ impl MockProverError { | Self::AssertEqualError { inst_id, .. } | Self::LookupError { inst_id, .. } | Self::LkMultiplicityError { inst_id, .. } => *inst_id, + Self::DegreeTooHigh { .. } => unreachable!(), } } @@ -438,6 +457,14 @@ impl<'a, E: ExtensionField + Hash> MockProver { .chain(&cb.cs.assert_zero_sumcheck_expressions_namespace_map), ) { + if expr.degree() > MAX_CONSTRAINT_DEGREE { + errors.push(MockProverError::DegreeTooHigh { + expression: expr.clone(), + degree: expr.degree(), + name: name.clone(), + }); + } + // require_equal does not always have the form of Expr::Sum as // the sum of witness and constant is expressed as scaled sum if name.contains("require_equal") && expr.unpack_sum().is_some() { @@ -701,6 +728,7 @@ Hints: .collect_vec(); Self::assert_satisfied(cb, &wits_in, programs, challenge, lkm); } + pub fn assert_satisfied( cb: &CircuitBuilder, wits_in: &[ArcMultilinearExtension<'a, E>], diff --git a/ceno_zkvm/src/scheme/tests.rs b/ceno_zkvm/src/scheme/tests.rs index 825f93724..39cf279f3 100644 --- a/ceno_zkvm/src/scheme/tests.rs +++ b/ceno_zkvm/src/scheme/tests.rs @@ -235,13 +235,13 @@ fn test_single_add_instance_e2e() { zkvm_fixed_traces.register_table_circuit::>( &zkvm_cs, - u16_range_config.clone(), + &u16_range_config, &(), ); zkvm_fixed_traces.register_table_circuit::>( &zkvm_cs, - prog_config.clone(), + &prog_config, &program, ); @@ -262,7 +262,7 @@ fn test_single_add_instance_e2e() { let mut add_records = vec![]; let mut halt_records = vec![]; all_records.into_iter().for_each(|record| { - let kind = record.insn().kind().1; + let kind = record.insn().codes().kind; match kind { ADD => add_records.push(record), EANY => { diff --git a/ceno_zkvm/src/structs.rs b/ceno_zkvm/src/structs.rs index a9b78f416..e00656c19 100644 --- a/ceno_zkvm/src/structs.rs +++ b/ceno_zkvm/src/structs.rs @@ -188,7 +188,7 @@ impl ZKVMFixedTraces { pub fn register_table_circuit>( &mut self, cs: &ZKVMConstraintSystem, - config: TC::TableConfig, + config: &TC::TableConfig, input: &TC::FixedInput, ) { let cs = cs.get_cs(&TC::name()).expect("cs not found"); @@ -196,7 +196,7 @@ impl ZKVMFixedTraces { self.circuit_fixed_traces .insert( TC::name(), - Some(TC::generate_fixed_traces(&config, cs.num_fixed, input)), + Some(TC::generate_fixed_traces(config, cs.num_fixed, input)), ) .is_none() ); diff --git a/ceno_zkvm/src/tables/program.rs b/ceno_zkvm/src/tables/program.rs index d5b629957..0b4ed5e98 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,21 +84,21 @@ impl InsnRecord { impl InsnRecord { fn from_decoded(pc: u32, insn: &DecodedInstruction) -> Self { - InsnRecord::new( + InsnRecord([ pc, insn.opcode(), - insn.rd_or_zero(), + insn.rd_internal(), 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. /// Convert negative values from two's complement to field. pub fn imm_or_funct7_field(insn: &DecodedInstruction) -> F { - if insn.imm_is_negative() { + if insn.imm_field_is_negative() { -F::from(-(insn.imm_or_funct7() as i32) as u64) } else { F::from(insn.imm_or_funct7() as u64) @@ -184,6 +188,7 @@ impl TableCircuit ); }); + Self::padding_zero(&mut fixed, num_fixed).expect("padding error"); fixed } diff --git a/ceno_zkvm/src/tables/ram.rs b/ceno_zkvm/src/tables/ram.rs index 3b4f8233d..03993557a 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::{ DynVolatileRamCircuit, NonVolatileRamCircuit, NonVolatileTable, PubIORamCircuit, }; @@ -46,7 +46,7 @@ impl NonVolatileTable for RegTable { } fn len() -> usize { - 32 // register size 32 + VMState::REG_COUNT.next_power_of_two() } fn addr(entry_index: usize) -> Addr {