Skip to content

Commit

Permalink
apply to r instruction
Browse files Browse the repository at this point in the history
  • Loading branch information
KimiWu123 committed Oct 16, 2024
1 parent 2222e89 commit 948b163
Show file tree
Hide file tree
Showing 8 changed files with 92 additions and 82 deletions.
23 changes: 1 addition & 22 deletions ceno_emul/src/tracer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -54,27 +54,6 @@ pub type WriteOp = MemOp<Change<Word>>;

impl StepRecord {
pub fn new_r_instruction(
cycle: Cycle,
pc: ByteAddr,
insn_code: Word,
rs1_read: Word,
rs2_read: Word,
rd: Change<Word>,
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,
Expand Down
60 changes: 37 additions & 23 deletions ceno_zkvm/src/instructions/riscv/arith.rs
Original file line number Diff line number Diff line change
Expand Up @@ -171,7 +171,7 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E

#[cfg(test)]
mod test {
use ceno_emul::{Change, StepRecord};
use ceno_emul::{Change, EncodedInstruction, StepRecord};
use goldilocks::GoldilocksExt2;
use itertools::Itertools;
use multilinear_extensions::mle::IntoMLEs;
Expand All @@ -180,7 +180,7 @@ mod test {
use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
scheme::mock_prover::{MockProver, MOCK_PC_ADD, MOCK_PC_MUL, MOCK_PC_SUB, MOCK_PROGRAM},
scheme::mock_prover::{MockProver, MOCK_PC_START},
};

#[test]
Expand All @@ -198,13 +198,14 @@ mod test {
.unwrap()
.unwrap();

let insn_code = EncodedInstruction::encode(InsnKind::ADD, 2, 3, 4, 0);
let (raw_witin, _) = AddInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_ADD,
MOCK_PROGRAM[0],
MOCK_PC_START,
insn_code,
11,
0xfffffffe,
Change::new(0, 11_u32.wrapping_add(0xfffffffe)),
Expand All @@ -224,14 +225,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -251,13 +253,14 @@ mod test {
.unwrap()
.unwrap();

let insn_code = EncodedInstruction::encode(InsnKind::ADD, 2, 3, 4, 0);
let (raw_witin, _) = AddInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_ADD,
MOCK_PROGRAM[0],
MOCK_PC_START,
insn_code,
u32::MAX - 1,
u32::MAX - 1,
Change::new(0, (u32::MAX - 1).wrapping_add(u32::MAX - 1)),
Expand All @@ -277,14 +280,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -304,13 +308,14 @@ mod test {
.unwrap()
.unwrap();

let insn_code = EncodedInstruction::encode(InsnKind::SUB, 2, 3, 4, 0);
let (raw_witin, _) = SubInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_SUB,
MOCK_PROGRAM[1],
MOCK_PC_START,
insn_code,
11,
2,
Change::new(0, 11_u32.wrapping_sub(2)),
Expand All @@ -330,14 +335,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -357,13 +363,14 @@ mod test {
.unwrap()
.unwrap();

let insn_code = EncodedInstruction::encode(InsnKind::SUB, 2, 3, 4, 0);
let (raw_witin, _) = SubInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_SUB,
MOCK_PROGRAM[1],
MOCK_PC_START,
insn_code,
3,
11,
Change::new(0, 3_u32.wrapping_sub(11)),
Expand All @@ -383,14 +390,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -405,13 +413,14 @@ mod test {
.unwrap();

// values assignment
let insn_code = EncodedInstruction::encode(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, _) = MulInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_MUL,
MOCK_PROGRAM[2],
MOCK_PC_START,
insn_code,
11,
2,
Change::new(0, 22),
Expand All @@ -428,14 +437,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -450,13 +460,14 @@ mod test {
.unwrap();

// values assignment
let insn_code = EncodedInstruction::encode(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, _) = MulInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_MUL,
MOCK_PROGRAM[2],
MOCK_PC_START,
insn_code,
u32::MAX / 2 + 1,
2,
Change::new(0, 0),
Expand All @@ -472,14 +483,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand All @@ -499,13 +511,14 @@ mod test {
let c_limb = ret.limbs;

// values assignment
let insn_code = EncodedInstruction::encode(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, _) = MulInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction(
3,
MOCK_PC_MUL,
MOCK_PROGRAM[2],
MOCK_PC_START,
insn_code,
a.as_u64() as u32,
b.as_u64() as u32,
Change::new(
Expand All @@ -524,14 +537,15 @@ mod test {
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
MockProver::assert_satisfied_with_program(
&mut cb,
&raw_witin
.de_interleaving()
.into_mles()
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
);
}
Expand Down
11 changes: 4 additions & 7 deletions ceno_zkvm/src/instructions/riscv/divu.rs
Original file line number Diff line number Diff line change
Expand Up @@ -156,10 +156,7 @@ mod test {

mod divu {

use ceno_emul::{
ByteAddr, Change, DecodedInstruction, EncodedInstruction, InsnFormat, InsnKind,
StepRecord, Word, CENO_PLATFORM,
};
use ceno_emul::{Change, EncodedInstruction, InsnKind, StepRecord, Word};
use goldilocks::GoldilocksExt2;
use itertools::Itertools;
use multilinear_extensions::mle::IntoMLEs;
Expand All @@ -171,7 +168,7 @@ mod test {
riscv::{constants::UInt, divu::DivUInstruction},
Instruction,
},
scheme::mock_prover::MockProver,
scheme::mock_prover::{MockProver, MOCK_PC_START},
Value,
};

Expand All @@ -197,9 +194,9 @@ mod test {
let (raw_witin, _) = DivUInstruction::assign_instances(
&config,
cb.cs.num_witin as usize,
vec![StepRecord::new_r_instruction2(
vec![StepRecord::new_r_instruction(
3,
ByteAddr(CENO_PLATFORM.pc_start()),
MOCK_PC_START,
insn_code,
dividend,
divisor,
Expand Down
Loading

0 comments on commit 948b163

Please sign in to comment.