Skip to content

Commit

Permalink
[#2427] Add a test for runtime tables
Browse files Browse the repository at this point in the history
  • Loading branch information
volhovm committed Aug 1, 2024
1 parent 19837e4 commit 7dfac05
Show file tree
Hide file tree
Showing 3 changed files with 142 additions and 6 deletions.
82 changes: 80 additions & 2 deletions msm/src/test/test_circuit/interpreter.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
use crate::{
circuit_design::{ColAccessCap, ColWriteCap, DirectWitnessCap},
circuit_design::{ColAccessCap, ColWriteCap, DirectWitnessCap, LookupCap},
serialization::interpreter::limb_decompose_ff,
test::test_circuit::columns::{TestColumn, N_FSEL_TEST},
test::test_circuit::{
columns::{TestColumn, N_FSEL_TEST},
lookups::LookupTable,
},
LIMB_BITSIZE, N_LIMBS,
};
use ark_ff::{Field, PrimeField, SquareRootField, Zero};
Expand Down Expand Up @@ -271,6 +274,81 @@ pub fn test_fixed_sel_degree_7_mul_witness<
constrain_test_fixed_sel_degree_7_mul_witness(env);
}

pub fn constrain_lookups<
F: PrimeField,
Env: ColAccessCap<F, TestColumn> + LookupCap<F, TestColumn, LookupTable>,
>(
env: &mut Env,
) {
let a0 = Env::read_column(env, TestColumn::A(0));
let a1 = Env::read_column(env, TestColumn::A(1));

env.lookup(LookupTable::RangeCheck15, vec![a0.clone()]);
env.lookup(LookupTable::RangeCheck15, vec![a1.clone()]);

let cur_index = Env::read_column(env, TestColumn::FixedSel1);
let prev_index = Env::read_column(env, TestColumn::FixedSel2);
let next_index = Env::read_column(env, TestColumn::FixedSel3);

env.lookup(
LookupTable::RuntimeTable1,
vec![
cur_index.clone(),
prev_index.clone(),
next_index.clone(),
Env::constant(F::from(4u64)),
],
);

// For now we only allow one read per runtime table with runtime_create_column = true.
//env.lookup(LookupTable::RuntimeTable1, vec![a0.clone(), a1.clone()]);

env.lookup_runtime_write(
LookupTable::RuntimeTable2,
vec![
Env::constant(F::from(1u64 << 26)),
Env::constant(F::from(5u64)),
],
);
env.lookup_runtime_write(
LookupTable::RuntimeTable2,
vec![cur_index, Env::constant(F::from(5u64))],
);
env.lookup(
LookupTable::RuntimeTable2,
vec![
Env::constant(F::from(1u64 << 26)),
Env::constant(F::from(5u64)),
],
);
env.lookup(
LookupTable::RuntimeTable2,
vec![prev_index, Env::constant(F::from(5u64))],
);
}

pub fn lookups_circuit<
F: SquareRootField + PrimeField,
Env: ColAccessCap<F, TestColumn>
+ ColWriteCap<F, TestColumn>
+ DirectWitnessCap<F, TestColumn>
+ LookupCap<F, TestColumn, LookupTable>,
>(
env: &mut Env,
domain_size: usize,
) {
for row_i in 0..domain_size {
env.write_column(TestColumn::A(0), &Env::constant(F::from(11u64)));
env.write_column(TestColumn::A(1), &Env::constant(F::from(17u64)));

constrain_lookups(env);

if row_i < domain_size - 1 {
env.next_row();
}
}
}

/// Fixed selectors for the test circuit.
pub fn build_fixed_selectors<F: Field>(domain_size: usize) -> Box<[Vec<F>; N_FSEL_TEST]> {
// 0 1 2 3 4 ...
Expand Down
9 changes: 5 additions & 4 deletions msm/src/test/test_circuit/lookups.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@ use strum_macros::EnumIter;

#[derive(Clone, Copy, Debug, Hash, Eq, PartialEq, Ord, PartialOrd, EnumIter)]
pub enum LookupTable {
/// x ∈ [0, 2^15]
/// Fixed table, x ∈ [0, 2^15].
RangeCheck15,
/// A runtime table.
/// A runtime table, with no explicit writes.
RuntimeTable1,
/// A runtime table.
/// A runtime table, with explicit writes.
RuntimeTable2,
}

Expand Down Expand Up @@ -42,7 +42,8 @@ impl LookupTableID for LookupTable {

fn runtime_create_column(&self) -> bool {
match self {
Self::RuntimeTable1 => false,
Self::RuntimeTable1 => true,
Self::RuntimeTable2 => false,
_ => panic!("runtime_create_column was called on a non-runtime table"),
}
}
Expand Down
57 changes: 57 additions & 0 deletions msm/src/test/test_circuit/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ mod tests {
test::test_circuit::{
columns::{TestColumn, N_COL_TEST, N_FSEL_TEST},
interpreter as test_interpreter,
lookups::LookupTable as TestLookupTable,
},
Ff1, Fp,
};
Expand Down Expand Up @@ -426,6 +427,62 @@ mod tests {
build_test_mul_circuit::<_, DummyLookupTable>(&mut rng, 1 << 4);
}

#[test]
fn test_completeness_lookups() {
let mut rng = o1_utils::tests::make_test_rng(None);

// Include tests for completeness for Logup as the random witness
// includes all arguments
let domain_size = 1 << 15;

let fixed_selectors = test_interpreter::build_fixed_selectors(domain_size);

let mut constraint_env = ConstraintBuilderEnv::<Fp, TestLookupTable>::create();
test_interpreter::constrain_lookups::<Fp, _>(&mut constraint_env);
let constraints = constraint_env.get_relation_constraints();

let mut witness_env: TestWitnessBuilderEnv<TestLookupTable> = WitnessBuilderEnv::create();
witness_env.set_fixed_selectors(fixed_selectors.to_vec());
test_interpreter::lookups_circuit(&mut witness_env, domain_size);
let runtime_tables: BTreeMap<_, Vec<Vec<Vec<_>>>> =
witness_env.get_runtime_tables(domain_size);

let mut lookup_tables_data: BTreeMap<TestLookupTable, Vec<Vec<Vec<Fp>>>> = BTreeMap::new();
for table_id in TestLookupTable::all_variants().into_iter() {
if table_id.is_fixed() {
lookup_tables_data.insert(
table_id,
vec![table_id
.entries(domain_size as u64)
.unwrap()
.into_iter()
.map(|x| vec![x])
.collect()],
);
}
}
for (table_id, runtime_table) in runtime_tables.into_iter() {
lookup_tables_data.insert(table_id, runtime_table);
}

let proof_inputs = witness_env.get_proof_inputs(domain_size, lookup_tables_data);

crate::test::test_completeness_generic::<
{ N_COL_TEST - N_FSEL_TEST },
{ N_COL_TEST - N_FSEL_TEST },
0,
N_FSEL_TEST,
TestLookupTable,
_,
>(
constraints,
fixed_selectors,
proof_inputs,
domain_size,
&mut rng,
);
}

#[test]
fn test_completeness() {
let mut rng = o1_utils::tests::make_test_rng(None);
Expand Down

0 comments on commit 7dfac05

Please sign in to comment.