Skip to content

Commit

Permalink
Merge branch 'master' into matthias/dead-code-2
Browse files Browse the repository at this point in the history
  • Loading branch information
@matthiasgoergens
matthiasgoergens authored Oct 27, 2024
2 parents 98ceb67 + 7a96556 commit 115faaf
Showing 1 changed file with 122 additions and 50 deletions.
172 changes: 122 additions & 50 deletions ceno_zkvm/src/instructions/riscv/shift_imm.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,28 +10,36 @@ use crate::{
},
witness::LkMultiplicity,
};
use ceno_emul::StepRecord;
use ceno_emul::{InsnKind, StepRecord};
use ff_ext::ExtensionField;
use std::{marker::PhantomData, mem::MaybeUninit};

pub struct InstructionConfig<E: ExtensionField> {
pub struct ShiftImmConfig<E: ExtensionField> {
i_insn: IInstructionConfig<E>,

rs1_read: UInt<E>,
imm: UInt<E>,
rd_written: UInt<E>,
remainder: UInt<E>,
div_config: DivConfig<E>,

// for SRLI division arithmetics
remainder: Option<UInt<E>>,
div_config: Option<DivConfig<E>>,
}

pub struct ShiftImmInstruction<E, I>(PhantomData<(E, I)>);

pub struct SlliOp;
impl RIVInstruction for SlliOp {
const INST_KIND: ceno_emul::InsnKind = ceno_emul::InsnKind::SLLI;
}

pub struct SrliOp;
impl RIVInstruction for SrliOp {
const INST_KIND: ceno_emul::InsnKind = ceno_emul::InsnKind::SRLI;
}

impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ShiftImmInstruction<E, I> {
type InstructionConfig = InstructionConfig<E>;
type InstructionConfig = ShiftImmConfig<E>;

fn name() -> String {
format!("{:?}", I::INST_KIND)
Expand All @@ -41,33 +49,56 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ShiftImmInstructio
circuit_builder: &mut CircuitBuilder<E>,
) -> Result<Self::InstructionConfig, ZKVMError> {
let mut imm = UInt::new(|| "imm", circuit_builder)?;
let mut rd_written = UInt::new(|| "rd_written", circuit_builder)?;

// Note: `imm` is set to 2**imm (upto 32 bit) just for SRLI for efficient verification
// Note: `imm` is set to 2**imm (upto 32 bit) just for efficient verification
// Goal is to constrain:
// rs1 == rd_written * imm + remainder
let remainder = UInt::new(|| "remainder", circuit_builder)?;
let div_config = DivConfig::construct_circuit(
circuit_builder,
|| "srli_div",
&mut imm,
&mut rd_written,
&remainder,
)?;
let (rs1_read, rd_written, remainder, div_config) = match I::INST_KIND {
InsnKind::SLLI => {
let mut rs1_read = UInt::new_unchecked(|| "rs1_read", circuit_builder)?;
let rd_written = rs1_read.mul(
|| "rd_written = rs1_read * imm",
circuit_builder,
&mut imm,
true,
)?;

(rs1_read, rd_written, None, None)
}
InsnKind::SRLI => {
let mut rd_written = UInt::new(|| "rd_written", circuit_builder)?;
let remainder = UInt::new(|| "remainder", circuit_builder)?;
let div_config = DivConfig::construct_circuit(
circuit_builder,
|| "srli_div",
&mut imm,
&mut rd_written,
&remainder,
)?;
(
div_config.dividend.clone(),
rd_written,
Some(remainder),
Some(div_config),
)
}
_ => unreachable!(),
};

let i_insn = IInstructionConfig::<E>::construct_circuit(
circuit_builder,
I::INST_KIND,
&imm.value(),
div_config.dividend.register_expr(),
rs1_read.register_expr(),
rd_written.register_expr(),
false,
)?;

Ok(InstructionConfig {
Ok(ShiftImmConfig {
i_insn,
imm,
rd_written,
rs1_read,
remainder,
div_config,
})
Expand All @@ -79,26 +110,38 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for ShiftImmInstructio
lk_multiplicity: &mut LkMultiplicity,
step: &StepRecord,
) -> Result<(), ZKVMError> {
let rd_written = Value::new(step.rd().unwrap().value.after, lk_multiplicity);

let (remainder, imm) = {
let rs1_read = step.rs1().unwrap().value;
let imm = step.insn().imm_or_funct7();
(
Value::new(rs1_read % imm, lk_multiplicity),
Value::new(imm, lk_multiplicity),
)
let imm = Value::new(step.insn().imm_or_funct7(), lk_multiplicity);
match I::INST_KIND {
InsnKind::SLLI => {
let rs1_read = Value::new_unchecked(step.rs1().unwrap().value);
let rd_written = rs1_read.mul(&imm, lk_multiplicity, true);
config.rs1_read.assign_value(instance, rs1_read);
config
.rd_written
.assign_mul_outcome(instance, lk_multiplicity, &rd_written)?;
}
InsnKind::SRLI => {
let rd_written = Value::new(step.rd().unwrap().value.after, lk_multiplicity);
let rs1_read = step.rs1().unwrap().value;
let remainder = Value::new(rs1_read % imm.as_u32(), lk_multiplicity);
config.div_config.as_ref().unwrap().assign_instance(
instance,
lk_multiplicity,
&imm,
&rd_written,
&remainder,
)?;
config
.remainder
.as_ref()
.unwrap()
.assign_value(instance, remainder);
config.rd_written.assign_value(instance, rd_written);
}
_ => unreachable!(),
};
config.div_config.assign_instance(
instance,
lk_multiplicity,
&imm,
&rd_written,
&remainder,
)?;

config.imm.assign_value(instance, imm);
config.rd_written.assign_value(instance, rd_written);
config.remainder.assign_value(instance, remainder);

config
.i_insn
Expand All @@ -118,31 +161,61 @@ mod test {
use crate::{
Value,
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::{Instruction, riscv::constants::UInt},
instructions::{
Instruction,
riscv::{RIVInstruction, constants::UInt},
},
scheme::mock_prover::{MOCK_PC_START, MockProver},
};

use super::{ShiftImmInstruction, SrliOp};
use super::{ShiftImmInstruction, SlliOp, SrliOp};

#[test]
fn test_opcode_slli() {
verify::<SlliOp>("imm = 3, rs1 = 32", 3, 32, 32 << 3);
verify::<SlliOp>("imm = 3, rs1 = 33", 3, 33, 33 << 3);

verify::<SlliOp>("imm = 31, rs1 = 32", 31, 32, 32 << 31);
verify::<SlliOp>("imm = 31, rs1 = 33", 31, 33, 33 << 31);
}

#[test]
fn test_opcode_srli() {
// imm = 3
verify_srli(3, 32, 32 >> 3);
verify_srli(3, 33, 33 >> 3);
// imm = 31
verify_srli(31, 32, 32 >> 31);
verify_srli(31, 33, 33 >> 31);
verify::<SrliOp>("imm = 3, rs1 = 32", 3, 32, 32 >> 3);
verify::<SrliOp>("imm = 3, rs1 = 33", 3, 33, 33 >> 3);

verify::<SrliOp>("imm = 31, rs1 = 32", 31, 32, 32 >> 31);
verify::<SrliOp>("imm = 31, rs1 = 33", 31, 33, 33 >> 31);
}

fn verify_srli(imm: u32, rs1_read: u32, expected_rd_written: u32) {
fn verify<I: RIVInstruction>(
name: &'static str,
imm: u32,
rs1_read: u32,
expected_rd_written: u32,
) {
let mut cs = ConstraintSystem::<GoldilocksExt2>::new(|| "riscv");
let mut cb = CircuitBuilder::new(&mut cs);

let (prefix, insn_code, rd_written) = match I::INST_KIND {
InsnKind::SLLI => (
"SLLI",
encode_rv32(InsnKind::SLLI, 2, 0, 4, imm),
rs1_read << imm,
),
InsnKind::SRLI => (
"SRLI",
encode_rv32(InsnKind::SRLI, 2, 0, 4, imm),
rs1_read >> imm,
),
_ => unreachable!(),
};

let config = cb
.namespace(
|| "srli",
|| format!("{prefix}_({name})"),
|cb| {
let config =
ShiftImmInstruction::<GoldilocksExt2, SrliOp>::construct_circuit(cb);
let config = ShiftImmInstruction::<GoldilocksExt2, I>::construct_circuit(cb);
Ok(config)
},
)
Expand All @@ -162,16 +235,15 @@ mod test {
)
.unwrap();

let insn_code = encode_rv32(InsnKind::SRLI, 2, 0, 4, imm);
let (raw_witin, lkm) = ShiftImmInstruction::<GoldilocksExt2, SrliOp>::assign_instances(
let (raw_witin, lkm) = ShiftImmInstruction::<GoldilocksExt2, I>::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, rs1_read >> imm),
Change::new(0, rd_written),
0,
)],
)
Expand Down

0 comments on commit 115faaf

Please sign in to comment.