Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor/ remove MOCK_PROGRAM in MockProver #395

Merged
merged 18 commits into from
Oct 18, 2024
Merged

refactor/ remove MOCK_PROGRAM in MockProver #395

Show file tree
Hide file tree
Changes from 16 commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
b5d81f2
draft version
KimiWu123 Oct 14, 2024
c118cda
first version
KimiWu123 Oct 16, 2024
7ec1b86
apply to r instruction
KimiWu123 Oct 16, 2024
31a1540
apply to b instruction
KimiWu123 Oct 17, 2024
7c6a538
apply to I instruction
KimiWu123 Oct 17, 2024
e04c781
adopt fixed program table size
KimiWu123 Oct 17, 2024
d5e1943
apply to U instrunction
KimiWu123 Oct 17, 2024
ffaece6
apply to J instruction
KimiWu123 Oct 17, 2024
264feab
cleanup
KimiWu123 Oct 17, 2024
49a2c80
move EncodeInstruction to a module
KimiWu123 Oct 17, 2024
7df8f99
&mut cb -> &cb
KimiWu123 Oct 17, 2024
717a97f
refine run_maybe_challenge
KimiWu123 Oct 17, 2024
2531ddf
add comment
KimiWu123 Oct 17, 2024
228d8c8
fixing lint
KimiWu123 Oct 17, 2024
5690748
Merge branch 'master' into refactor/mock_program
naure Oct 17, 2024
ca0912d
Merge branch 'master' into refactor/mock_program
naure Oct 17, 2024
d1c6408
Merge remote-tracking branch 'upstream/master' into refactor/mock_pro…
KimiWu123 Oct 18, 2024
3ab4d6a
fix errors due to merge
KimiWu123 Oct 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions ceno_emul/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,3 +15,6 @@ pub use rv32im::{DecodedInstruction, EmuContext, InsnCategory, InsnCodes, InsnKi

mod elf;
pub use elf::Program;

mod rv32im_encode;
pub use rv32im_encode::encode_rv32;
107 changes: 107 additions & 0 deletions ceno_emul/src/rv32im_encode.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,107 @@
use crate::{InsnKind, rv32im::InsnFormat};

const MASK_4_BITS: u32 = 0xF;
const MASK_5_BITS: u32 = 0x1F;
const MASK_6_BITS: u32 = 0x3F;
const MASK_7_BITS: u32 = 0x7F;
const MASK_8_BITS: u32 = 0xFF;
const MASK_10_BITS: u32 = 0x3FF;
const MASK_12_BITS: u32 = 0xFFF;

pub fn encode_rv32(kind: InsnKind, rs1: u32, rs2: u32, rd: u32, imm: u32) -> u32 {
match kind.codes().format {
InsnFormat::R => encode_r(kind, rs1, rs2, rd),
InsnFormat::I => encode_i(kind, rs1, rd, imm),
InsnFormat::S => encode_s(kind, rs1, rs2, imm),
InsnFormat::B => encode_b(kind, rs1, rs2, imm),
InsnFormat::U => encode_u(kind, rd, imm),
InsnFormat::J => encode_j(kind, rd, imm),
}
}

// R-Type
// 25 20 15 12 7 0
// +------+-----+-----+--------+----+-------+
// funct7 | rs2 | rs1 | funct3 | rd | opcode
fn encode_r(kind: InsnKind, rs1: u32, rs2: u32, rd: u32) -> u32 {
let rs2 = rs2 & MASK_5_BITS; // 5-bits mask
let rs1 = rs1 & MASK_5_BITS;
let rd = rd & MASK_5_BITS;
let func7 = kind.codes().func7;
let func3 = kind.codes().func3;
let opcode = kind.codes().opcode;
func7 << 25 | rs2 << 20 | rs1 << 15 | func3 << 12 | rd << 7 | opcode
}

// I-Type
// 20 15 12 7 0
// +---------+-----+--------+----+-------+
// imm[0:11] | rs1 | funct3 | rd | opcode
fn encode_i(kind: InsnKind, rs1: u32, rd: u32, imm: u32) -> u32 {
let rs1 = rs1 & MASK_5_BITS;
let rd = rd & MASK_5_BITS;
let func3 = kind.codes().func3;
let opcode = kind.codes().opcode;
let imm = imm & MASK_12_BITS;
imm << 20 | rs1 << 15 | func3 << 12 | rd << 7 | opcode
}

// S-Type
// 25 20 15 12 7 0
// +---------+-----+-----+--------+----------+-------+
// imm[5:11] | rs2 | rs1 | funct3 | imm[0:4] | opcode
fn encode_s(kind: InsnKind, rs1: u32, rs2: u32, imm: u32) -> u32 {
let rs2 = rs2 & MASK_5_BITS;
let rs1 = rs1 & MASK_5_BITS;
let func3 = kind.codes().func3;
let opcode = kind.codes().opcode;
let imm_lo = imm & MASK_5_BITS;
let imm_hi = (imm >> 5) & MASK_7_BITS; // 7-bits mask
imm_hi << 25 | rs2 << 20 | rs1 << 15 | func3 << 12 | imm_lo << 7 | opcode
}

// B-Type
// 31 25 20 15 12 8 7 0
// +-------+-----------+-----+-----+--------+----------+---------+-------+
// imm[12] | imm[5:10] | rs2 | rs1 | funct3 | imm[1:4] | imm[11] | opcode
fn encode_b(kind: InsnKind, rs1: u32, rs2: u32, imm: u32) -> u32 {
let rs2 = rs2 & MASK_5_BITS;
let rs1 = rs1 & MASK_5_BITS;
let func3 = kind.codes().func3;
let opcode = kind.codes().opcode;
let imm_1_4 = (imm >> 1) & MASK_4_BITS; // skip imm[0]
let imm_5_10 = (imm >> 5) & MASK_6_BITS;
((imm >> 12) & 1) << 31
| imm_5_10 << 25
| rs2 << 20
| rs1 << 15
| func3 << 12
| imm_1_4 << 8
| ((imm >> 11) & 1) << 7
| opcode
}

// J-Type
// 31 21 20 12 7 0
// +-------+-----------+---------+------------+----+-------+
// imm[20] | imm[1:10] | imm[11] | imm[12:19] | rd | opcode
fn encode_j(kind: InsnKind, rd: u32, imm: u32) -> u32 {
let rd = rd & MASK_5_BITS;
let opcode = kind.codes().opcode;
let imm_1_10 = (imm >> 1) & MASK_10_BITS; // skip imm[0]
let imm_12_19 = (imm >> 12) & MASK_8_BITS;
((imm >> 20) & 1) << 31
| imm_1_10 << 21
| ((imm >> 11) & 1) << 20
| imm_12_19 << 12
| rd << 7
| opcode
}

// U-Type
// 12 7 0
// +----------+----+--------+
// imm[12:31] | rd | opcode
fn encode_u(kind: InsnKind, rd: u32, imm: u32) -> u32 {
(imm >> 12) << 12 | (rd & MASK_5_BITS) << 7 | kind.codes().opcode
}
12 changes: 6 additions & 6 deletions ceno_emul/src/tracer.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ impl StepRecord {
pub fn new_r_instruction(
cycle: Cycle,
pc: ByteAddr,
insn_code: Word,
insn_code: u32,
naure marked this conversation as resolved.
Show resolved Hide resolved
rs1_read: Word,
rs2_read: Word,
rd: Change<Word>,
Expand All @@ -77,7 +77,7 @@ impl StepRecord {
pub fn new_b_instruction(
cycle: Cycle,
pc: Change<ByteAddr>,
insn_code: Word,
insn_code: u32,
rs1_read: Word,
rs2_read: Word,
prev_cycle: Cycle,
Expand All @@ -96,7 +96,7 @@ impl StepRecord {
pub fn new_i_instruction(
cycle: Cycle,
pc: ByteAddr,
insn_code: Word,
insn_code: u32,
rs1_read: Word,
rd: Change<Word>,
prev_cycle: Cycle,
Expand All @@ -116,7 +116,7 @@ impl StepRecord {
pub fn new_u_instruction(
cycle: Cycle,
pc: ByteAddr,
insn_code: Word,
insn_code: u32,
rd: Change<Word>,
prev_cycle: Cycle,
) -> StepRecord {
Expand All @@ -127,7 +127,7 @@ impl StepRecord {
pub fn new_j_instruction(
cycle: Cycle,
pc: Change<ByteAddr>,
insn_code: Word,
insn_code: u32,
rd: Change<Word>,
prev_cycle: Cycle,
) -> StepRecord {
Expand All @@ -137,7 +137,7 @@ impl StepRecord {
fn new_insn(
cycle: Cycle,
pc: Change<ByteAddr>,
insn_code: Word,
insn_code: u32,
rs1_read: Option<Word>,
rs2_read: Option<Word>,
rd: Option<Change<Word>>,
Expand Down
46 changes: 30 additions & 16 deletions ceno_zkvm/src/instructions/riscv/arith.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,7 +169,7 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ArithInstruction<E

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

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

let insn_code = encode_rv32(InsnKind::ADD, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 Down Expand Up @@ -229,6 +230,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand All @@ -249,12 +251,13 @@ mod test {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::ADD, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 Down Expand Up @@ -282,6 +285,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand All @@ -302,12 +306,13 @@ mod test {
.unwrap()
.unwrap();

let insn_code = encode_rv32(InsnKind::SUB, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 Down Expand Up @@ -335,6 +340,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand All @@ -355,12 +361,13 @@ mod test {
.unwrap()
.unwrap();

let insn_code = encode_rv32(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 Down Expand Up @@ -388,6 +395,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
None,
);
Expand All @@ -403,12 +411,13 @@ mod test {
.unwrap();

// values assignment
let insn_code = encode_rv32(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 @@ -433,6 +442,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand All @@ -448,12 +458,13 @@ mod test {
.unwrap();

// values assignment
let insn_code = encode_rv32(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 @@ -477,6 +488,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand All @@ -497,12 +509,13 @@ mod test {
let c_limb = ret.limbs;

// values assignment
let insn_code = encode_rv32(InsnKind::MUL, 2, 3, 4, 0);
let (raw_witin, lkm) =
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 @@ -529,6 +542,7 @@ mod test {
.into_iter()
.map(|v| v.into())
.collect_vec(),
&[insn_code],
None,
Some(lkm),
);
Expand Down
Loading
Loading