Skip to content

Commit

Permalink
fix logic
Browse files Browse the repository at this point in the history
  • Loading branch information
@zemse
zemse committed Sep 11, 2024
1 parent 76fcf23 commit 84f7fc4
Show file tree
Hide file tree
Showing 4 changed files with 26 additions and 33 deletions.
6 changes: 2 additions & 4 deletions ceno_zkvm/src/chip_handler.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,18 +24,16 @@ pub trait RegisterChipOperations<E: ExtensionField, NR: Into<String>, N: FnOnce(
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
) -> Result<Expression<E>, ZKVMError>;
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;

#[allow(clippy::too_many_arguments)]
fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_rs1_ts: Expression<E>,
prev_rs2_ts: Expression<E>,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
) -> Result<(Expression<E>, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError>;
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError>;
}
24 changes: 8 additions & 16 deletions ceno_zkvm/src/chip_handler/register.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
prev_ts: Expression<E>,
ts: Expression<E>,
values: &V,
) -> Result<Expression<E>, ZKVMError> {
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
let read_record = cb.rlc_chip_record(
Expand All @@ -30,7 +30,7 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
))],
vec![register_id.expr()],
values.expr(),
vec![prev_ts],
vec![prev_ts.clone()],
]
.concat(),
);
Expand All @@ -50,26 +50,23 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
cb.write_record(|| "write_record", write_record)?;

// assert prev_ts < current_ts
// TODO implement lt gadget
// let is_lt = prev_ts.lt(self, ts)?;
// self.require_one(is_lt)?;
let lt_cfg = cb.less_than(|| "prev_ts < ts", prev_ts, ts.clone(), Some(true))?;

let next_ts = ts + 1.into();

Ok(next_ts)
Ok((next_ts, lt_cfg))
})
}

fn register_write<V: ToExpr<E, Output = Vec<Expression<E>>>>(
&mut self,
name_fn: N,
register_id: &WitIn,
prev_rs1_ts: Expression<E>,
prev_rs2_ts: Expression<E>,
prev_ts: Expression<E>,
ts: Expression<E>,
prev_values: &V,
values: &V,
) -> Result<(Expression<E>, ExprLtConfig, ExprLtConfig, ExprLtConfig), ZKVMError> {
) -> Result<(Expression<E>, ExprLtConfig), ZKVMError> {
self.namespace(name_fn, |cb| {
// READ (a, v, t)
let read_record = cb.rlc_chip_record(
Expand Down Expand Up @@ -98,16 +95,11 @@ impl<'a, E: ExtensionField, NR: Into<String>, N: FnOnce() -> NR> RegisterChipOpe
cb.read_record(|| "read_record", read_record)?;
cb.write_record(|| "write_record", write_record)?;

let lt_rs1_cfg =
cb.less_than(|| "prev_rs1_ts < ts", prev_rs1_ts, ts.clone(), Some(true))?;
let lt_rs2_cfg =
cb.less_than(|| "prev_rs2_ts < ts", prev_rs2_ts, ts.clone(), Some(true))?;
let lt_prev_ts_cfg =
cb.less_than(|| "prev_rd_ts < ts", prev_ts, ts.clone(), Some(true))?;
let lt_cfg = cb.less_than(|| "prev_ts < ts", prev_ts, ts.clone(), Some(true))?;

let next_ts = ts + 1.into();

Ok((next_ts, lt_rs1_cfg, lt_rs2_cfg, lt_prev_ts_cfg))
Ok((next_ts, lt_cfg))
})
}
}
20 changes: 9 additions & 11 deletions ceno_zkvm/src/instructions/riscv/addsub.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -103,21 +103,19 @@ fn add_sub_gadget<E: ExtensionField, const IS_ADD: bool>(
let prev_rs2_ts = circuit_builder.create_witin(|| "prev_rs2_ts")?;
let prev_rd_ts = circuit_builder.create_witin(|| "prev_rd_ts")?;

let ts = circuit_builder.register_read(
let (ts, lt_rs1_cfg) = circuit_builder.register_read(
|| "read_rs1",
&rs1_id,
prev_rs1_ts.expr(),
cur_ts.expr(),
&addend_0,
)?;
let ts =
let (ts, lt_rs2_cfg) =
circuit_builder.register_read(|| "read_rs2", &rs2_id, prev_rs2_ts.expr(), ts, &addend_1)?;

let (ts, lt_rs1_cfg, lt_rs2_cfg, lt_prev_ts_cfg) = circuit_builder.register_write(
let (ts, lt_prev_ts_cfg) = circuit_builder.register_write(
|| "write_rd",
&rd_id,
prev_rs1_ts.expr(),
prev_rs2_ts.expr(),
prev_rd_ts.expr(),
ts,
&prev_rd_value,
Expand Down Expand Up @@ -193,18 +191,18 @@ impl<E: ExtensionField> Instruction<E> for AddInstruction {
set_val!(instance, config.prev_rd_ts, 2);

ExprLtInput {
lhs: 2, // rs1
rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1
lhs: 2, // rs1
rhs: 3, // cur_ts
}
.assign(instance, &config.lt_rs1_cfg);
ExprLtInput {
lhs: 2, // rs2
rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1
lhs: 2, // rs2
rhs: 4, // cur_ts
}
.assign(instance, &config.lt_rs2_cfg);
ExprLtInput {
lhs: 2, // rd
rhs: 3 + 1 + 1, // ts = cur_ts + 1 + 1
lhs: 2, // rd
rhs: 5, // cur_ts
}
.assign(instance, &config.lt_prev_ts_cfg);

Expand Down
9 changes: 7 additions & 2 deletions ceno_zkvm/src/instructions/riscv/blt.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,7 @@ use crate::{
};

use super::{
config::ExprLtConfig,
constants::{OPType, OpcodeType, RegUInt, RegUInt8, PC_STEP_SIZE},
RIVInstruction,
};
Expand All @@ -38,6 +39,8 @@ pub struct InstructionConfig<E: ExtensionField> {
pub prev_rs1_ts: WitIn,
pub prev_rs2_ts: WitIn,
pub is_lt: UIntLtConfig,
pub lt_rs1_cfg: ExprLtConfig,
pub lt_rs2_cfg: ExprLtConfig,
}

pub struct BltInput {
Expand Down Expand Up @@ -174,14 +177,14 @@ fn blt_gadget<E: ExtensionField>(
let lhs = RegUInt::from_u8_limbs(circuit_builder, &lhs_limb8);
let rhs = RegUInt::from_u8_limbs(circuit_builder, &rhs_limb8);

let ts = circuit_builder.register_read(
let (ts, lt_rs1_cfg) = circuit_builder.register_read(
|| "read ts for lhs",
&rs1_id,
prev_rs1_ts.expr(),
cur_ts.expr(),
&lhs,
)?;
let ts = circuit_builder.register_read(
let (ts, lt_rs2_cfg) = circuit_builder.register_read(
|| "read ts for rhs",
&rs2_id,
prev_rs2_ts.expr(),
Expand All @@ -207,6 +210,8 @@ fn blt_gadget<E: ExtensionField>(
prev_rs1_ts,
prev_rs2_ts,
is_lt,
lt_rs1_cfg,
lt_rs2_cfg,
})
}

Expand Down

0 comments on commit 84f7fc4

Please sign in to comment.