Skip to content

Commit

Permalink
merge with master
Browse files Browse the repository at this point in the history
  • Loading branch information
@hero78119
hero78119 committed Sep 5, 2024
2 parents d4eb57e + 41ceaaa commit 5d2825e
Show file tree
Hide file tree
Showing 4 changed files with 60 additions and 86 deletions.
62 changes: 25 additions & 37 deletions ceno_zkvm/src/instructions/riscv/blt.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
use goldilocks::SmallField;
use std::mem::MaybeUninit;

use ff_ext::ExtensionField;
Expand All @@ -12,8 +13,8 @@ use crate::{
riscv::config::{LtConfig, LtInput},
Instruction,
},
set_field_val,
utils::{i64_to_base_field, limb_u8_to_u16},
set_val,
utils::{i64_to_base, limb_u8_to_u16},
};

use super::{
Expand Down Expand Up @@ -53,70 +54,64 @@ pub struct BltInput {

impl BltInput {
/// TODO: refactor after formalize the interface of opcode inputs
pub fn assign<E: ExtensionField>(
pub fn assign<F: SmallField, E: ExtensionField<BaseField = F>>(
&self,
config: &InstructionConfig<E>,
instance: &mut [MaybeUninit<E::BaseField>],
instance: &mut [MaybeUninit<F>],
) {
assert!(!self.lhs_limb8.is_empty() && (self.lhs_limb8.len() == self.rhs_limb8.len()));
// TODO: add boundary check for witin
let lt_input = LtInput {
lhs_limbs: &self.lhs_limb8,
rhs_limbs: &self.rhs_limb8,
};
let is_lt = lt_input.assign::<E>(instance, &config.is_lt);
let is_lt = lt_input.assign(instance, &config.is_lt);

set_field_val!(instance, config.pc, {
i64_to_base_field::<E>(self.pc as i64)
});
set_field_val!(instance, config.next_pc, {
set_val!(instance, config.pc, { i64_to_base::<F>(self.pc as i64) });
set_val!(instance, config.next_pc, {
if is_lt {
i64_to_base_field::<E>(self.pc as i64 + self.imm as i64)
i64_to_base::<F>(self.pc as i64 + self.imm as i64)
} else {
i64_to_base_field::<E>(self.pc as i64 + PC_STEP_SIZE as i64)
i64_to_base::<F>(self.pc as i64 + PC_STEP_SIZE as i64)
}
});
set_field_val!(instance, config.ts, {
i64_to_base_field::<E>(self.ts as i64)
});
set_field_val!(instance, config.imm, {
i64_to_base_field::<E>(self.imm as i64)
set_val!(instance, config.ts, { i64_to_base::<F>(self.ts as i64) });
set_val!(instance, config.imm, { i64_to_base::<F>(self.imm as i64) });
set_val!(instance, config.rs1_id, {
i64_to_base::<F>(self.rs1_id as i64)
});
set_field_val!(instance, config.rs1_id, {
i64_to_base_field::<E>(self.rs1_id as i64)
set_val!(instance, config.rs2_id, {
i64_to_base::<F>(self.rs2_id as i64)
});
set_field_val!(instance, config.rs2_id, {
i64_to_base_field::<E>(self.rs2_id as i64)
set_val!(instance, config.prev_rs1_ts, {
i64_to_base::<F>(self.prev_rs1_ts as i64)
});
set_field_val!(instance, config.prev_rs1_ts, {
i64_to_base_field::<E>(self.prev_rs1_ts as i64)
});
set_field_val!(instance, config.prev_rs2_ts, {
i64_to_base_field::<E>(self.prev_rs2_ts as i64)
set_val!(instance, config.prev_rs2_ts, {
i64_to_base::<F>(self.prev_rs2_ts as i64)
});

config.lhs_limb8.assign_limbs(instance, {
self.lhs_limb8
.iter()
.map(|&limb| i64_to_base_field::<E>(limb as i64))
.map(|&limb| i64_to_base::<F>(limb as i64))
.collect()
});
config.rhs_limb8.assign_limbs(instance, {
self.rhs_limb8
.iter()
.map(|&limb| i64_to_base_field::<E>(limb as i64))
.map(|&limb| i64_to_base::<F>(limb as i64))
.collect()
});
let lhs = limb_u8_to_u16(&self.lhs_limb8);
let rhs = limb_u8_to_u16(&self.rhs_limb8);
config.lhs.assign_limbs(instance, {
lhs.iter()
.map(|&limb| i64_to_base_field::<E>(limb as i64))
.map(|&limb| i64_to_base::<F>(limb as i64))
.collect()
});
config.rhs.assign_limbs(instance, {
rhs.iter()
.map(|&limb| i64_to_base_field::<E>(limb as i64))
.map(|&limb| i64_to_base::<F>(limb as i64))
.collect()
});
}
Expand Down Expand Up @@ -240,18 +235,11 @@ impl<E: ExtensionField> Instruction<E> for BltInstruction {
mod test {
use super::*;
use ceno_emul::StepRecord;
use ff_ext::ExtensionField;
use goldilocks::GoldilocksExt2;
use itertools::Itertools;
use multilinear_extensions::mle::IntoMLEs;

use crate::{
circuit_builder::{CircuitBuilder, ConstraintSystem},
instructions::Instruction,
scheme::mock_prover::MockProver,
};

use super::BltInstruction;
use crate::{circuit_builder::ConstraintSystem, scheme::mock_prover::MockProver};

#[test]
fn test_blt_circuit() -> Result<(), ZKVMError> {
Expand Down
65 changes: 30 additions & 35 deletions ceno_zkvm/src/instructions/riscv/config.rs
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
use std::mem::MaybeUninit;

use crate::{expression::WitIn, set_field_val, utils::i64_to_base_field};
use ff::Field;
use ff_ext::ExtensionField;
use crate::{expression::WitIn, set_val, utils::i64_to_base};
use goldilocks::SmallField;
use itertools::Itertools;

#[derive(Clone)]
Expand All @@ -24,19 +23,19 @@ pub struct MsbInput<'a> {
}

impl MsbInput<'_> {
pub fn assign<E: ExtensionField>(
pub fn assign<F: SmallField>(
&self,
instance: &mut [MaybeUninit<E::BaseField>],
instance: &mut [MaybeUninit<F>],
config: &MsbConfig,
) -> (u8, u8) {
let n_limbs = self.limbs.len();
assert!(n_limbs > 0);
let mut high_limb = self.limbs[n_limbs - 1];
let msb = (high_limb >> 7) & 1;
set_field_val!(instance, config.msb, i64_to_base_field::<E>(msb as i64));
set_val!(instance, config.msb, { i64_to_base::<F>(msb as i64) });
high_limb &= 0b0111_1111;
set_field_val!(instance, config.high_limb_no_msb, {
i64_to_base_field::<E>(high_limb as i64)
set_val!(instance, config.high_limb_no_msb, {
i64_to_base::<F>(high_limb as i64)
});
(msb, high_limb)
}
Expand All @@ -58,9 +57,9 @@ pub struct LtuInput<'a> {
}

impl LtuInput<'_> {
pub fn assign<E: ExtensionField>(
pub fn assign<F: SmallField>(
&self,
instance: &mut [MaybeUninit<E::BaseField>],
instance: &mut [MaybeUninit<F>],
config: &LtuConfig,
) -> bool {
let mut idx = 0;
Expand All @@ -78,31 +77,29 @@ impl LtuInput<'_> {
break;
}
}
set_field_val!(instance, config.indexes[idx], {
i64_to_base_field::<E>(flag as i64)
set_val!(instance, config.indexes[idx], {
i64_to_base::<F>(flag as i64)
});
config.acc_indexes.iter().enumerate().for_each(|(id, wit)| {
if id <= idx {
set_field_val!(instance, wit, i64_to_base_field::<E>(flag as i64));
set_val!(instance, wit, { i64_to_base::<F>(flag as i64) });
} else {
set_field_val!(instance, wit, E::BaseField::ZERO);
set_val!(instance, wit, 0);
}
});
let lhs_ne_byte = i64_to_base_field::<E>(self.lhs_limbs[idx] as i64);
let rhs_ne_byte = i64_to_base_field::<E>(self.rhs_limbs[idx] as i64);
set_field_val!(instance, config.lhs_ne_byte, lhs_ne_byte);
set_field_val!(instance, config.rhs_ne_byte, rhs_ne_byte);
set_field_val!(instance, config.byte_diff_inv, {
let lhs_ne_byte = i64_to_base::<F>(self.lhs_limbs[idx] as i64);
let rhs_ne_byte = i64_to_base::<F>(self.rhs_limbs[idx] as i64);
set_val!(instance, config.lhs_ne_byte, lhs_ne_byte);
set_val!(instance, config.rhs_ne_byte, rhs_ne_byte);
set_val!(instance, config.byte_diff_inv, {
if flag {
(lhs_ne_byte - rhs_ne_byte).invert().unwrap()
} else {
E::BaseField::ONE
F::ONE
}
});
let is_ltu = self.lhs_limbs[idx] < self.rhs_limbs[idx];
set_field_val!(instance, config.is_ltu, {
i64_to_base_field::<E>(is_ltu as i64)
});
set_val!(instance, config.is_ltu, { i64_to_base::<F>(is_ltu as i64) });
is_ltu
}
}
Expand All @@ -123,20 +120,20 @@ pub struct LtInput<'a> {
}

impl LtInput<'_> {
pub fn assign<E: ExtensionField>(
pub fn assign<F: SmallField>(
&self,
instance: &mut [MaybeUninit<E::BaseField>],
instance: &mut [MaybeUninit<F>],
config: &LtConfig,
) -> bool {
let n_limbs = self.lhs_limbs.len();
let lhs_msb_input = MsbInput {
limbs: self.lhs_limbs,
};
let (lhs_msb, lhs_high_limb_no_msb) = lhs_msb_input.assign::<E>(instance, &config.lhs_msb);
let (lhs_msb, lhs_high_limb_no_msb) = lhs_msb_input.assign(instance, &config.lhs_msb);
let rhs_msb_input = MsbInput {
limbs: self.rhs_limbs,
};
let (rhs_msb, rhs_high_limb_no_msb) = rhs_msb_input.assign::<E>(instance, &config.rhs_msb);
let (rhs_msb, rhs_high_limb_no_msb) = rhs_msb_input.assign(instance, &config.rhs_msb);

let mut lhs_limbs_no_msb = self.lhs_limbs.iter().copied().collect_vec();
lhs_limbs_no_msb[n_limbs - 1] = lhs_high_limb_no_msb;
Expand All @@ -148,26 +145,24 @@ impl LtInput<'_> {
lhs_limbs: &lhs_limbs_no_msb,
rhs_limbs: &rhs_limbs_no_msb,
};
let is_ltu = ltu_input.assign::<E>(instance, &config.is_ltu);
let is_ltu = ltu_input.assign::<F>(instance, &config.is_ltu);

let msb_is_equal = lhs_msb == rhs_msb;
let msb_diff_inv = if msb_is_equal {
0
} else {
lhs_msb as i64 - rhs_msb as i64
};
set_field_val!(instance, config.msb_is_equal, {
i64_to_base_field::<E>(msb_is_equal as i64)
set_val!(instance, config.msb_is_equal, {
i64_to_base::<F>(msb_is_equal as i64)
});
set_field_val!(instance, config.msb_diff_inv, {
i64_to_base_field::<E>(msb_diff_inv)
set_val!(instance, config.msb_diff_inv, {
i64_to_base::<F>(msb_diff_inv)
});

// is_lt = a_s\cdot (1-b_s)+eq(a_s,b_s)\cdot ltu(a_{<s},b_{<s})$
let is_lt = lhs_msb * (1 - rhs_msb) + msb_is_equal as u8 * is_ltu as u8;
set_field_val!(instance, config.is_lt, {
i64_to_base_field::<E>(is_lt as i64)
});
set_val!(instance, config.is_lt, { i64_to_base::<F>(is_lt as i64) });

assert!(is_lt == 0 || is_lt == 1);
is_lt > 0
Expand Down
12 changes: 5 additions & 7 deletions ceno_zkvm/src/utils.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,14 +11,12 @@ pub fn ext_to_u64<E: ExtensionField>(x: &E) -> u64 {
bases[0].to_canonical_u64()
}

#[allow(dead_code)]
pub fn i64_to_ext<E: ExtensionField>(x: i64) -> E {
let x0 = if x >= 0 {
E::BaseField::from(x as u64)
pub fn i64_to_base<F: SmallField>(x: i64) -> F {
if x >= 0 {
F::from(x as u64)
} else {
-E::BaseField::from((-x) as u64)
};
E::from_bases(&[x0, E::BaseField::ZERO])
-F::from((-x) as u64)
}
}

/// This is helper function to convert witness of u8 limb into u16 limb
Expand Down
7 changes: 0 additions & 7 deletions ceno_zkvm/src/witness.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,6 @@ macro_rules! set_val {
};
}

#[macro_export]
macro_rules! set_field_val {
($ins:ident, $field:expr, $val:expr) => {
$ins[$field.id as usize] = MaybeUninit::new($val);
};
}

pub struct RowMajorMatrix<T: Sized + Sync + Clone + Send> {
// represent 2D in 1D linear memory and avoid double indirection by Vec<Vec<T>> to improve performance
values: Vec<MaybeUninit<T>>,
Expand Down

0 comments on commit 5d2825e

Please sign in to comment.