Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

MSM/Serialization: start lookup #1944

Merged
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
127 changes: 121 additions & 6 deletions msm/src/serialization/mod.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
use crate::{mvlookup::LookupTableID, MVLookup};
use ark_ff::Field;

use crate::mvlookup::LookupTableID;

/// The number of intermediate limbs of 4 bits required for the circuit
pub const N_INTERMEDIATE_LIMBS: usize = 20;

Expand All @@ -10,6 +9,7 @@ pub mod constraints;
pub mod interpreter;
pub mod witness;

#[derive(Clone, Copy, Debug)]
pub enum LookupTable {
RangeCheck15,
RangeCheck4,
Expand All @@ -24,15 +24,19 @@ impl LookupTableID for LookupTable {
}
}

pub type Lookup<F> = MVLookup<F, LookupTable>;

#[cfg(test)]
mod tests {
use kimchi::circuits::domains::EvaluationDomains;
use poly_commitment::pairing_proof::PairingSRS;
use rand::Rng as _;

use super::{Lookup, LookupTable};

use crate::{
columns::Column,
lookups::LookupTableIDs,
mvlookup::MVLookupWitness,
precomputed_srs::get_bn254_srs,
proof::ProofInputs,
prover::prove,
Expand All @@ -44,6 +48,40 @@ mod tests {
BaseSponge, Fp, OpeningProof, ScalarSponge, BN254, N_LIMBS,
};

use ark_ff::{FftField, Field, PrimeField};

impl LookupTable {
fn into_lookup_vector<F: FftField + PrimeField + Field>(
self,
domain: EvaluationDomains<F>,
) -> Vec<Lookup<F>> {
assert!(domain.d1.size >= (1 << 15));
match self {
Self::RangeCheck15 => (0..(1 << 15))
.map(|i| Lookup {
table_id: LookupTable::RangeCheck15,
numerator: -F::one(),
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are these -1 by default? I'd assume that by default we are not using any of the elements, so they should have 0?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, ok, I think I misunderstood what this function does. Please tell me if I'm right: what you're doing is given a fixed table you're building a set of queries for that table covering every element of this table?

value: vec![F::from(i as u64)],
})
.collect::<Vec<Lookup<F>>>(),
Self::RangeCheck4 => (0..(1 << 15))
.map(|i| {
if i < (1 << 4) {
F::from(i as u64)
} else {
F::zero()
}
})
.map(|x| Lookup {
table_id: LookupTable::RangeCheck4,
numerator: -F::one(),
value: vec![x],
})
.collect::<Vec<Lookup<F>>>(),
}
}
}

#[test]
fn test_completeness() {
let mut rng = o1_utils::tests::make_test_rng();
Expand Down Expand Up @@ -77,7 +115,12 @@ mod tests {
}

let mut constraints = vec![];
for limbs in field_elements {

let mut rangecheck15: [Vec<Lookup<Fp>>; N_LIMBS] = std::array::from_fn(|_| vec![]);
let mut rangecheck4: [Vec<Lookup<Fp>>; N_INTERMEDIATE_LIMBS] =
std::array::from_fn(|_| vec![]);

for (i, limbs) in field_elements.into_iter().enumerate() {
let mut constraint_env = constraints::Env::<Fp>::create();
// Witness
deserialize_field_element(&mut witness_env, limbs);
Expand All @@ -102,11 +145,83 @@ mod tests {
constraints.push(cst.clone())
}
}

for (j, lookup) in witness_env.rangecheck4_lookups.iter().enumerate() {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably next step, but this code that collects something from witness and passes to MVLookup can be arguably moved to witness.rs so that witness_env.get_inputs would give you the inputs directly

rangecheck4[j].push(lookup.clone())
}

for (j, lookup) in witness_env.rangecheck15_lookups.iter().enumerate() {
rangecheck15[j].push(lookup.clone())
}

witness_env.add_rangecheck4_table_value(i);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like this needs to be called somewhere from range_check4() function on the witness impl InterpreterEnv side, no?

Copy link
Member Author

@dannywillems dannywillems Mar 12, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would like to move it somewhere else, yes. The table should be built outside the interpreter as it is a fixed table. We should have a way to handle multiple domain sizes.


witness_env.reset()
}

let rangecheck15_m = witness_env.get_rangecheck15_normalized_multipliticies(domain);
let rangecheck15_t = LookupTable::RangeCheck15
.into_lookup_vector(domain)
.into_iter()
.enumerate()
.map(
|(
i,
Lookup {
table_id,
numerator,
value,
},
)| {
Lookup {
table_id,
numerator: numerator * rangecheck15_m[i],
value,
}
},
);

let rangecheck4_m = witness_env.get_rangecheck4_normalized_multipliticies(domain);
let rangecheck4_t = LookupTable::RangeCheck4
.into_lookup_vector(domain)
.into_iter()
.enumerate()
.map(
|(
i,
Lookup {
table_id,
numerator,
value,
},
)| {
Lookup {
table_id,
numerator: numerator * rangecheck4_m[i],
value,
}
},
);

let lookup_witness_rangecheck4: MVLookupWitness<Fp, LookupTable> = {
MVLookupWitness {
f: rangecheck4.to_vec(),
t: rangecheck4_t.collect(),
m: rangecheck4_m,
}
};

let lookup_witness_rangecheck15: MVLookupWitness<Fp, LookupTable> = {
MVLookupWitness {
f: rangecheck15.to_vec(),
t: rangecheck15_t.collect(),
m: rangecheck15_m,
}
};

let proof_inputs = ProofInputs {
evaluations: *witness,
mvlookups: vec![],
mvlookups: vec![lookup_witness_rangecheck15, lookup_witness_rangecheck4],
public_input_size: 0,
};

Expand All @@ -118,7 +233,7 @@ mod tests {
Column,
_,
SERIALIZATION_N_COLUMNS,
LookupTableIDs,
LookupTable,
>(domain, &srs, &constraints, proof_inputs, &mut rng)
.unwrap();

Expand Down
79 changes: 77 additions & 2 deletions msm/src/serialization/witness.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,10 @@ use o1_utils::FieldHelpers;

use crate::columns::Column;
use crate::serialization::interpreter::InterpreterEnv;
use crate::serialization::{Lookup, LookupTable};
use crate::N_LIMBS;
use kimchi::circuits::domains::EvaluationDomains;
use std::iter;

use super::N_INTERMEDIATE_LIMBS;

Expand All @@ -17,9 +20,26 @@ pub struct Env<Fp> {
/// field Kimchi gate
pub intermediate_limbs: [Fp; N_INTERMEDIATE_LIMBS],

/// Keep track of the RangeCheck4 lookup multiplicities
// Boxing to avoid stack overflow
pub lookup_multiplicities_rangecheck4: Box<[Fp; 1 << 4]>,

/// Keep track of the RangeCheck4 table multiplicities.
/// The value `0` is used as a (repeated) dummy value.
// Boxing to avoid stack overflow
pub lookup_t_multiplicities_rangecheck4: Box<[Fp; 1 << 4]>,

/// Keep track of the RangeCheck15 lookup multiplicities
/// No t multiplicities as we do suppose we have a domain of
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

How does this work? You still need to construct the multiplicities for t, I guess you wanted to say that it's easier in the case of 2^15 domain size, but why? 🤔

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Copy link
Member

@volhovm volhovm Mar 12, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I thought (14) does not apply to our case because our t(x) is fully injective, since every element in the range table is unique? Why do we need normalised multiplicities?

/// size `1 << 15`
// Boxing to avoid stack overflow
pub lookup_multiplicities_rangecheck15: Box<[Fp; 1 << 15]>,

/// Keep track of the rangecheck 4 lookups for each row.
pub rangecheck4_lookups: Vec<Lookup<Fp>>,

/// Keep track of the rangecheck 15 lookups for each row.
pub rangecheck15_lookups: Vec<Lookup<Fp>>,
}

impl<Fp: PrimeField> InterpreterEnv<Fp> for Env<Fp> {
Expand Down Expand Up @@ -48,21 +68,29 @@ impl<Fp: PrimeField> InterpreterEnv<Fp> for Env<Fp> {
}

fn range_check15(&mut self, value: &Self::Variable) {
// FIXME: this is not the full intended implementation
let value_biguint = value.to_biguint();
assert!(value_biguint < BigUint::from(2u128.pow(15)));
// Adding multiplicities
let value_usize: usize = value_biguint.clone().try_into().unwrap();
self.lookup_multiplicities_rangecheck15[value_usize] += Fp::one();
self.rangecheck15_lookups.push(Lookup {
table_id: LookupTable::RangeCheck15,
numerator: Fp::one(),
value: vec![*value],
})
}

fn range_check4(&mut self, value: &Self::Variable) {
// FIXME: this is not the full intended implementation
let value_biguint = value.to_biguint();
assert!(value_biguint < BigUint::from(2u128.pow(4)));
// Adding multiplicities
let value_usize: usize = value_biguint.clone().try_into().unwrap();
self.lookup_multiplicities_rangecheck4[value_usize] += Fp::one();
self.rangecheck4_lookups.push(Lookup {
table_id: LookupTable::RangeCheck4,
numerator: Fp::one(),
value: vec![*value],
})
}

fn copy(&mut self, x: &Self::Variable, position: Self::Position) -> Self::Variable {
Expand Down Expand Up @@ -112,6 +140,48 @@ impl<Fp: PrimeField> Env<Fp> {
}
}
}

pub fn add_rangecheck4_table_value(&mut self, i: usize) {
if i < (1 << 4) {
self.lookup_t_multiplicities_rangecheck4[i] += Fp::one();
} else {
self.lookup_t_multiplicities_rangecheck4[0] += Fp::one();
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this dummy value handling? Wondering if it's not bringing any soundness issues, since in the first if case you also add to the [0] element, right?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

}
}

pub fn reset(&mut self) {
self.rangecheck15_lookups = vec![];
self.rangecheck4_lookups = vec![];
}

/// Return the normalized multiplicity vector of RangeCheck4 in case the
/// table is not injective. Note that it is the case for `RangeCheck4`.
pub fn get_rangecheck4_normalized_multipliticies(
&self,
domain: EvaluationDomains<Fp>,
) -> Vec<Fp> {
let mut m = vec![Fp::zero(); 1 << 4];
self.lookup_multiplicities_rangecheck4
.into_iter()
.zip(self.lookup_t_multiplicities_rangecheck4.iter())
.enumerate()
.for_each(|(i, (m_f, m_t))| m[i] = m_f / m_t);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why do we need to do this (field? or is it integer?) division here? Is it related to the dummy values?..

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

let repeated_dummy_value: Vec<Fp> = iter::repeat(m[0])
.take((domain.d1.size - (1 << 4)) as usize)
.collect();
m.extend(repeated_dummy_value);
m
}
/// Return the normalized multiplicity vector of RangeCheck4 in case the
/// table is not injective. Note that it is not the case for `RangeCheck15` as
/// we assume the domain size is `1 << 15`.
pub fn get_rangecheck15_normalized_multipliticies(
&self,
domain: EvaluationDomains<Fp>,
) -> Vec<Fp> {
assert_eq!(domain.d1.size, 1 << 15);
self.lookup_multiplicities_rangecheck15.to_vec()
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah OK, answered my own question about why 15bit case does not have t. The multiplicities are /exactly/ equal to the "called" vector that we build in the witness, so they are much easier to compute.

}
}

impl<Fp: PrimeField> Env<Fp> {
Expand All @@ -120,8 +190,13 @@ impl<Fp: PrimeField> Env<Fp> {
current_kimchi_limbs: [Fp::zero(); 3],
msm_limbs: [Fp::zero(); N_LIMBS],
intermediate_limbs: [Fp::zero(); N_INTERMEDIATE_LIMBS],

lookup_multiplicities_rangecheck4: Box::new([Fp::zero(); 1 << 4]),
lookup_t_multiplicities_rangecheck4: Box::new([Fp::zero(); 1 << 4]),

lookup_multiplicities_rangecheck15: Box::new([Fp::zero(); 1 << 15]),
rangecheck4_lookups: vec![],
rangecheck15_lookups: vec![],
}
}
}
Expand Down