From 948b16361b8dcc13417edfbf26801465af5721a5 Mon Sep 17 00:00:00 2001 From: KimiWu Date: Wed, 16 Oct 2024 14:09:49 +0800 Subject: [PATCH] apply to r instruction --- ceno_emul/src/tracer.rs | 23 +------ ceno_zkvm/src/instructions/riscv/arith.rs | 60 ++++++++++++------- ceno_zkvm/src/instructions/riscv/divu.rs | 11 ++-- .../src/instructions/riscv/logic/test.rs | 28 +++++---- ceno_zkvm/src/instructions/riscv/mulh.rs | 12 ++-- ceno_zkvm/src/instructions/riscv/shift.rs | 25 +++++--- ceno_zkvm/src/instructions/riscv/sltu.rs | 13 ++-- ceno_zkvm/src/scheme/mock_prover.rs | 2 + 8 files changed, 92 insertions(+), 82 deletions(-) diff --git a/ceno_emul/src/tracer.rs b/ceno_emul/src/tracer.rs index ee5c6f3f9..1350479c6 100644 --- a/ceno_emul/src/tracer.rs +++ b/ceno_emul/src/tracer.rs @@ -3,7 +3,7 @@ use std::{collections::HashMap, fmt, mem}; use crate::{ addr::{ByteAddr, Cycle, RegIdx, Word, WordAddr}, rv32im::DecodedInstruction, - InsnKind, CENO_PLATFORM, PC_STEP_SIZE, + CENO_PLATFORM, PC_STEP_SIZE, }; /// An instruction and its context in an execution trace. That is concrete values of registers and memory. @@ -54,27 +54,6 @@ pub type WriteOp = MemOp>; impl StepRecord { pub fn new_r_instruction( - cycle: Cycle, - pc: ByteAddr, - insn_code: Word, - rs1_read: Word, - rs2_read: Word, - rd: Change, - prev_cycle: Cycle, - ) -> StepRecord { - let pc = Change::new(pc, pc + PC_STEP_SIZE); - StepRecord::new_insn( - cycle, - pc, - insn_code, - Some(rs1_read), - Some(rs2_read), - Some(rd), - prev_cycle, - ) - } - - pub fn new_r_instruction2( cycle: Cycle, pc: ByteAddr, insn_code: u32, diff --git a/ceno_zkvm/src/instructions/riscv/arith.rs b/ceno_zkvm/src/instructions/riscv/arith.rs index b5be382e7..1ab507dd0 100644 --- a/ceno_zkvm/src/instructions/riscv/arith.rs +++ b/ceno_zkvm/src/instructions/riscv/arith.rs @@ -171,7 +171,7 @@ impl Instruction for ArithInstruction Instruction for MulhInstruction().as_u32()), @@ -175,7 +176,7 @@ mod test { ) .unwrap(); - MockProver::assert_satisfied( + MockProver::assert_satisfied_with_program( &cb, &raw_witin .de_interleaving() @@ -183,6 +184,7 @@ mod test { .into_iter() .map(|v| v.into()) .collect_vec(), + &[insn_code], None, ); } diff --git a/ceno_zkvm/src/instructions/riscv/shift.rs b/ceno_zkvm/src/instructions/riscv/shift.rs index 3b9692411..488159e49 100644 --- a/ceno_zkvm/src/instructions/riscv/shift.rs +++ b/ceno_zkvm/src/instructions/riscv/shift.rs @@ -183,7 +183,7 @@ impl Instruction for ShiftLogicalInstru #[cfg(test)] mod tests { - use ceno_emul::{Change, InsnKind, StepRecord}; + use ceno_emul::{Change, EncodedInstruction, InsnKind, StepRecord}; use goldilocks::GoldilocksExt2; use itertools::Itertools; use multilinear_extensions::mle::IntoMLEs; @@ -194,7 +194,7 @@ mod tests { riscv::{constants::UInt, RIVInstruction}, Instruction, }, - scheme::mock_prover::{MockProver, MOCK_PC_SLL, MOCK_PC_SRL, MOCK_PROGRAM}, + scheme::mock_prover::{MockProver, MOCK_PC_START}, Value, }; @@ -232,9 +232,17 @@ mod tests { let mut cb = CircuitBuilder::new(&mut cs); let shift = rs2_read & 0b11111; - let (prefix, mock_pc, mock_program_op, rd_written) = match I::INST_KIND { - InsnKind::SLL => ("SLL", MOCK_PC_SLL, MOCK_PROGRAM[19], rs1_read << shift), - InsnKind::SRL => ("SRL", MOCK_PC_SRL, MOCK_PROGRAM[20], rs1_read >> shift), + let (prefix, insn_code, rd_written) = match I::INST_KIND { + InsnKind::SLL => ( + "SLL", + EncodedInstruction::encode(InsnKind::SLL, 2, 3, 4, 0), + rs1_read << shift, + ), + InsnKind::SRL => ( + "SRL", + EncodedInstruction::encode(InsnKind::SRL, 2, 3, 4, 0), + rs1_read >> shift, + ), _ => unreachable!(), }; @@ -268,8 +276,8 @@ mod tests { cb.cs.num_witin as usize, vec![StepRecord::new_r_instruction( 3, - mock_pc, - mock_program_op, + MOCK_PC_START, + insn_code, rs1_read, rs2_read, Change::new(0, rd_written), @@ -278,7 +286,7 @@ mod tests { ) .unwrap(); - MockProver::assert_satisfied( + MockProver::assert_satisfied_with_program( &cb, &raw_witin .de_interleaving() @@ -286,6 +294,7 @@ mod tests { .into_iter() .map(|v| v.into()) .collect_vec(), + &[insn_code], None, ); } diff --git a/ceno_zkvm/src/instructions/riscv/sltu.rs b/ceno_zkvm/src/instructions/riscv/sltu.rs index 7919733c1..605ea7b63 100644 --- a/ceno_zkvm/src/instructions/riscv/sltu.rs +++ b/ceno_zkvm/src/instructions/riscv/sltu.rs @@ -105,7 +105,7 @@ impl Instruction for ArithInstruction