Skip to content

Commit

Permalink
refac-r-type: leave register values outside
Browse files Browse the repository at this point in the history
  • Loading branch information
Aurélien Nicolas committed Sep 16, 2024
1 parent 922c6b3 commit c9dba79
Show file tree
Hide file tree
Showing 4 changed files with 51 additions and 37 deletions.
10 changes: 5 additions & 5 deletions ceno_zkvm/src/chip_handler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,23 +18,23 @@ pub trait GlobalStateRegisterMachineChipOperations<E: ExtensionField> {
}

pub trait RegisterChipOperations<E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> {
fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_read(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;

#[allow(clippy::too_many_arguments)]
fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_write(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;
}
10 changes: 5 additions & 5 deletions ceno_zkvm/src/chip_handler/register.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,13 @@ use super::RegisterChipOperations;
impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOperations<E, NR, N>
for CircuitBuilder<'a, E>
{
fn register_read<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_read(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
Expand Down Expand Up @@ -58,14 +58,14 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
})
}

fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
fn register_write(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
prev_values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
values: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
Expand Down
44 changes: 32 additions & 12 deletions ceno_zkvm/src/instructions/riscv/addsub.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,15 @@ use crate::{
};
use core::mem::MaybeUninit;

#[derive(Debug)]
pub struct AddSubConfig<E: ExtensionField> {
r_insn: RInstructionConfig<E>,

addend_0: RegUInt<E>,
addend_1: RegUInt<E>,
outcome: RegUInt<E>,
}

pub struct AddInstruction<E>(PhantomData<E>);
pub struct SubInstruction<E>(PhantomData<E>);

Expand All @@ -32,7 +41,7 @@ impl<E: ExtensionField> RIVInstruction<E> for SubInstruction<E> {

fn add_sub_gadget<E: ExtensionField, const IS_ADD: bool>(
circuit_builder: &mut CircuitBuilder<E>,
) -> Result<RInstructionConfig<E>, ZKVMError> {
) -> Result<AddSubConfig<E>, ZKVMError> {
// Execution result = addend0 + addend1, with carry.
let (addend_0, addend_1, outcome) = if IS_ADD {
// outcome = addend_0 + addend_1
Expand All @@ -59,22 +68,31 @@ fn add_sub_gadget<E: ExtensionField, const IS_ADD: bool>(

let funct7 = if IS_ADD { FUNCT7_ADD } else { FUNCT7_SUB };

RInstructionConfig::<E>::construct_circuit(
let r_insn = RInstructionConfig::<E>::construct_circuit(
circuit_builder,
(OPCODE_OP, FUNCT3_ADD_SUB, funct7),
addend_0.clone(),
addend_1.clone(),
outcome.clone(),
)
&addend_0,
&addend_1,
&outcome,
)?;

Ok(AddSubConfig {
r_insn,
addend_0,
addend_1,
outcome,
})
}

fn add_sub_assignment<E: ExtensionField, const IS_ADD: bool>(
config: &RInstructionConfig<E>,
config: &AddSubConfig<E>,
instance: &mut [MaybeUninit<E::BaseField>],
lk_multiplicity: &mut LkMultiplicity,
step: &StepRecord,
) -> Result<(), ZKVMError> {
config.assign_instance(instance, lk_multiplicity, step)?;
config
.r_insn
.assign_instance(instance, lk_multiplicity, step)?;

let addend_1 = UIntValue::new_unchecked(step.rs2().unwrap().value);
config
Expand Down Expand Up @@ -117,10 +135,11 @@ impl<E: ExtensionField> Instruction<E> for AddInstruction<E> {
fn name() -> String {
"ADD".into()
}
type InstructionConfig = RInstructionConfig<E>;
type InstructionConfig = AddSubConfig<E>;

fn construct_circuit(
circuit_builder: &mut CircuitBuilder<E>,
) -> Result<RInstructionConfig<E>, ZKVMError> {
) -> Result<Self::InstructionConfig, ZKVMError> {
add_sub_gadget::<E, true>(circuit_builder)
}

Expand All @@ -140,10 +159,11 @@ impl<E: ExtensionField> Instruction<E> for SubInstruction<E> {
fn name() -> String {
"SUB".into()
}
type InstructionConfig = RInstructionConfig<E>;
type InstructionConfig = AddSubConfig<E>;

fn construct_circuit(
circuit_builder: &mut CircuitBuilder<E>,
) -> Result<RInstructionConfig<E>, ZKVMError> {
) -> Result<Self::InstructionConfig, ZKVMError> {
add_sub_gadget::<E, false>(circuit_builder)
}

Expand Down
24 changes: 9 additions & 15 deletions ceno_zkvm/src/instructions/riscv/r_insn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ use crate::{
chip_handler::{GlobalStateRegisterMachineChipOperations, RegisterChipOperations},
circuit_builder::CircuitBuilder,
error::ZKVMError,
expression::{ToExpr, WitIn},
expression::{Expression, ToExpr, WitIn},
instructions::{riscv::config::ExprLtInput, Instruction},

Check warning on line 20 in ceno_zkvm/src/instructions/riscv/r_insn.rs

View workflow job for this annotation

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

unused import: `Instruction`
set_val,
tables::InsnRecord,
Expand All @@ -29,13 +29,10 @@ use core::mem::MaybeUninit;
pub struct RInstructionConfig<E: ExtensionField> {
pub pc: WitIn,
pub ts: WitIn,
pub prev_rd_value: RegUInt<E>,
pub addend_0: RegUInt<E>,
pub addend_1: RegUInt<E>,
pub outcome: RegUInt<E>,
pub rs1_id: WitIn,
pub rs2_id: WitIn,
pub rd_id: WitIn,
pub prev_rd_value: RegUInt<E>,
pub prev_rs1_ts: WitIn,
pub prev_rs2_ts: WitIn,
pub prev_rd_ts: WitIn,
Expand All @@ -48,9 +45,9 @@ impl<E: ExtensionField> RInstructionConfig<E> {
pub fn construct_circuit(
circuit_builder: &mut CircuitBuilder<E>,
opcode_funct_3_7: (usize, usize, usize),
addend_0: RegUInt<E>,
addend_1: RegUInt<E>,
outcome: RegUInt<E>,
addend_0: &impl ToExpr<E, Output = Vec<Expression<E>>>,
addend_1: &impl ToExpr<E, Output = Vec<Expression<E>>>,
outcome: &impl ToExpr<E, Output = Vec<Expression<E>>>,
) -> Result<Self, ZKVMError> {
// State in.
let pc = circuit_builder.create_witin(|| "pc")?;
Expand Down Expand Up @@ -86,22 +83,22 @@ impl<E: ExtensionField> RInstructionConfig<E> {
&rs1_id,
prev_rs1_ts.expr(),
cur_ts.expr(),
&addend_0,
addend_0,
)?;
let (ts, lt_rs2_cfg) = circuit_builder.register_read(
|| "read_rs2",
&rs2_id,
prev_rs2_ts.expr(),
ts,
&addend_1,
addend_1,
)?;
let (ts, lt_prev_ts_cfg) = circuit_builder.register_write(
|| "write_rd",
&rd_id,
prev_rd_ts.expr(),
ts,
&prev_rd_value,
&outcome,
outcome,
)?;

// State out.
Expand All @@ -112,13 +109,10 @@ impl<E: ExtensionField> RInstructionConfig<E> {
Ok(RInstructionConfig {
pc,
ts: cur_ts,
prev_rd_value,
addend_0,
addend_1,
outcome,
rs1_id,
rs2_id,
rd_id,
prev_rd_value,
prev_rs1_ts,
prev_rs2_ts,
prev_rd_ts,
Expand Down

0 comments on commit c9dba79

Please sign in to comment.