Skip to content

Commit

Permalink
unittest assertion on register value
Browse files Browse the repository at this point in the history
  • Loading branch information
@hero78119
hero78119 committed Oct 3, 2024
1 parent 367c6f3 commit 5bb5c04
Show file tree
Hide file tree
Showing 11 changed files with 201 additions and 48 deletions.
75 changes: 70 additions & 5 deletions ceno_zkvm/src/instructions/riscv/arith.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,6 @@ mod test {
};

#[test]
#[allow(clippy::option_map_unit_fn)]
fn test_opcode_add() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
let mut cb = CircuitBuilder::new(&mut cs);
Expand Down Expand Up @@ -212,6 +211,17 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(
Value::new_unchecked(11_u32.wrapping_add(0xfffffffe))
.as_u16_limbs()
.to_vec(),
);

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand All @@ -225,7 +235,6 @@ mod test {
}

#[test]
#[allow(clippy::option_map_unit_fn)]
fn test_opcode_add_overflow() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
let mut cb = CircuitBuilder::new(&mut cs);
Expand Down Expand Up @@ -255,6 +264,17 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(
Value::new_unchecked((u32::MAX - 1).wrapping_add(u32::MAX - 1))
.as_u16_limbs()
.to_vec(),
);

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand All @@ -268,7 +288,6 @@ mod test {
}

#[test]
#[allow(clippy::option_map_unit_fn)]
fn test_opcode_sub() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
let mut cb = CircuitBuilder::new(&mut cs);
Expand Down Expand Up @@ -298,6 +317,17 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(
Value::new_unchecked(11_u32.wrapping_sub(2))
.as_u16_limbs()
.to_vec(),
);

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand All @@ -311,7 +341,6 @@ mod test {
}

#[test]
#[allow(clippy::option_map_unit_fn)]
fn test_opcode_sub_underflow() {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
let mut cb = CircuitBuilder::new(&mut cs);
Expand Down Expand Up @@ -341,6 +370,17 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(
Value::new_unchecked(3_u32.wrapping_sub(11))
.as_u16_limbs()
.to_vec(),
);

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down Expand Up @@ -378,6 +418,14 @@ mod test {
)
.unwrap();

let expected_rd_written =
UInt::from_witin_const_unchecked(Value::new_unchecked(22u32).as_u16_limbs().to_vec());

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down Expand Up @@ -415,6 +463,13 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(vec![0u64, 0]);

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down Expand Up @@ -450,12 +505,22 @@ mod test {
MOCK_PROGRAM[2],
a.as_u64() as u32,
b.as_u64() as u32,
Change::new(0, Value::<u32>::from_limb_unchecked(c_limb).as_u64() as u32),
Change::new(
0,
Value::<u32>::from_limb_unchecked(c_limb.clone()).as_u64() as u32,
),
0,
)],
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(c_limb.clone());

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down
17 changes: 15 additions & 2 deletions ceno_zkvm/src/instructions/riscv/divu.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ pub struct ArithConfig<E: ExtensionField> {

dividend: UInt<E>,
divisor: UInt<E>,
outcome: UInt<E>,
pub(crate) outcome: UInt<E>,

remainder: UInt<E>,
inter_mul_value: UInt<E>,
Expand Down Expand Up @@ -160,8 +160,12 @@ mod test {

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::{riscv::divu::DivUInstruction, Instruction},
instructions::{
riscv::{constants::UInt, divu::DivUInstruction},
Instruction,
},
scheme::mock_prover::{MockProver, MOCK_PC_DIVU, MOCK_PROGRAM},
Value,
};

fn verify(name: &'static str, dividend: Word, divisor: Word, outcome: Word) {
Expand Down Expand Up @@ -191,6 +195,15 @@ mod test {
)
.unwrap();

let expected_rd_written = UInt::from_witin_const_unchecked(
Value::new_unchecked(outcome).as_u16_limbs().to_vec(),
);

config
.outcome
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down
21 changes: 6 additions & 15 deletions ceno_zkvm/src/instructions/riscv/logic/logic_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,9 +12,10 @@ use crate::{
Instruction,
},
tables::OpsTable,
utils::split_to_u8,
witness::LkMultiplicity,
};
use ceno_emul::{InsnKind, StepRecord, Word, WORD_SIZE};
use ceno_emul::{InsnKind, StepRecord};

/// This trait defines a logic instruction, connecting an instruction type to a lookup table.
pub trait LogicOp {
Expand Down Expand Up @@ -71,7 +72,7 @@ pub struct LogicConfig<E: ExtensionField> {

rs1_read: UInt8<E>,
rs2_read: UInt8<E>,
rd_written: UInt8<E>,
pub(crate) rd_written: UInt8<E>,
}

impl<E: ExtensionField> LogicConfig<E> {
Expand Down Expand Up @@ -108,25 +109,15 @@ impl<E: ExtensionField> LogicConfig<E> {
self.r_insn
.assign_instance(instance, lk_multiplicity, step)?;

let rs1_read = Self::u8_limbs(step.rs1().unwrap().value);
let rs1_read = split_to_u8(step.rs1().unwrap().value);
self.rs1_read.assign_limbs(instance, &rs1_read);

let rs2_read = Self::u8_limbs(step.rs2().unwrap().value);
let rs2_read = split_to_u8(step.rs2().unwrap().value);
self.rs2_read.assign_limbs(instance, &rs2_read);

let rd_written = Self::u8_limbs(step.rd().unwrap().value.after);
let rd_written = split_to_u8(step.rd().unwrap().value.after);
self.rd_written.assign_limbs(instance, &rd_written);

Ok(())
}

/// Decompose a word into byte in little-endian order, each hold in u16
/// using u16 as placeholder
fn u8_limbs(v: Word) -> Vec<u16> {
let mut limbs = Vec::with_capacity(WORD_SIZE);
for i in 0..WORD_SIZE {
limbs.push((v >> (i * 8) & 0xff) as u16);
}
limbs
}
}
24 changes: 23 additions & 1 deletion ceno_zkvm/src/instructions/riscv/logic/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@ use multilinear_extensions::mle::IntoMLEs;

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
instructions::{riscv::constants::UInt8, Instruction},
scheme::mock_prover::{MockProver, MOCK_PC_AND, MOCK_PC_OR, MOCK_PC_XOR, MOCK_PROGRAM},
utils::split_to_u8,
ROMType,
};

Expand Down Expand Up @@ -50,6 +51,13 @@ fn test_opcode_and() {
let lkm = lkm.into_finalize_result()[ROMType::And as usize].clone();
assert_eq!(&lkm.into_iter().sorted().collect_vec(), LOOKUPS);

let expected_rd_written = UInt8::from_witin_const_unchecked(split_to_u8::<u64>((A & B) as u32));

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down Expand Up @@ -95,6 +103,13 @@ fn test_opcode_or() {
let lkm = lkm.into_finalize_result()[ROMType::Or as usize].clone();
assert_eq!(&lkm.into_iter().sorted().collect_vec(), LOOKUPS);

let expected_rd_written = UInt8::from_witin_const_unchecked(split_to_u8::<u64>((A | B) as u32));

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down Expand Up @@ -140,6 +155,13 @@ fn test_opcode_xor() {
let lkm = lkm.into_finalize_result()[ROMType::Xor as usize].clone();
assert_eq!(&lkm.into_iter().sorted().collect_vec(), LOOKUPS);

let expected_rd_written = UInt8::from_witin_const_unchecked(split_to_u8::<u64>((A ^ B) as u32));

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down
2 changes: 1 addition & 1 deletion ceno_zkvm/src/instructions/riscv/shift_imm/shift_imm_circuit.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ pub struct InstructionConfig<E: ExtensionField> {
i_insn: IInstructionConfig<E>,

imm: UInt<E>,
rd_written: UInt<E>,
pub(crate) rd_written: UInt<E>,
remainder: UInt<E>,
rd_imm_mul: UInt<E>,
rd_imm_rem_add: UInt<E>,
Expand Down
11 changes: 10 additions & 1 deletion ceno_zkvm/src/instructions/riscv/shift_imm/test.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,9 @@ use multilinear_extensions::mle::IntoMLEs;

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
instructions::{riscv::constants::UInt, Instruction},
scheme::mock_prover::{MockProver, MOCK_PC_SRLI, MOCK_PC_SRLI_31, MOCK_PROGRAM},
Value,
};

use super::{shift_imm_circuit::ShiftImmInstruction, SrliOp};
Expand Down Expand Up @@ -40,6 +41,14 @@ fn test_opcode_srli_1() {
)
.unwrap();

let expected_rd_written =
UInt::from_witin_const_unchecked(Value::new_unchecked(32u32 >> 3).as_u16_limbs().to_vec());

config
.rd_written
.require_equal(|| "assert_rd_written", &mut cb, &expected_rd_written)
.unwrap();

MockProver::assert_satisfied(
&cb,
&raw_witin
Expand Down
9 changes: 8 additions & 1 deletion ceno_zkvm/src/instructions/riscv/sltu.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ pub struct ArithConfig<E: ExtensionField> {

rs1_read: UInt<E>,
rs2_read: UInt<E>,
#[allow(dead_code)]
rd_written: UInt<E>,

Check warning on line 24 in ceno_zkvm/src/instructions/riscv/sltu.rs

View workflow job for this annotation

GitHub Actions / Various lints (x86_64-unknown-linux-gnu) 

field `rd_written` is never read

Check failure on line 24 in ceno_zkvm/src/instructions/riscv/sltu.rs

View workflow job for this annotation

GitHub Actions / Various lints (x86_64-unknown-linux-gnu) 

field `rd_written` is never read

is_lt: IsLtConfig,
Expand Down Expand Up @@ -150,6 +149,14 @@ mod test {
)
.unwrap();

let expected_rd_written =
UInt::from_witin_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();

MockProver::assert_satisfied(
&mut cb,
&raw_witin
Expand Down
Loading

0 comments on commit 5bb5c04

Please sign in to comment.