Skip to content

Commit

Permalink
add: RangeCheckCircuit with lookup
Browse files Browse the repository at this point in the history
  • Loading branch information
gnosed committed Sep 26, 2023
1 parent 0eb08f8 commit 7b166c6
Show file tree
Hide file tree
Showing 3 changed files with 272 additions and 5 deletions.
12 changes: 12 additions & 0 deletions halo2_proofs/src/poly/ipa/commitment.rs
Original file line number Diff line number Diff line change
Expand Up @@ -94,14 +94,26 @@ impl<'params, C: CurveAffine> Params<'params, C> for ParamsIPA<C> {
poly: &Polynomial<C::Scalar, LagrangeCoeff>,
r: Blind<C::Scalar>,
) -> C::Curve {
println!("DEBUG :: poly.len: {:?}", poly.len());
let mut tmp_scalars = Vec::with_capacity(poly.len() + 1);
let mut tmp_bases = Vec::with_capacity(poly.len() + 1);

tmp_scalars.extend(poly.iter());
tmp_scalars.push(r.0);

println!("DEBUG :: g_lagrange.len: {:?}", self.g_lagrange.len());
// for item in self.g_lagrange.iter() {
// if tmp_bases.len() < poly.len() {
// tmp_bases.push(*item);
// } else {
// break; // Stop adding when capacity is reached
// }
// }
tmp_bases.extend(self.g_lagrange.iter());
tmp_bases.push(self.w);
println!("DEBUG :: tmp_bases.len: {:?}", tmp_bases.len());

println!("DEBUG :: tmp_scalars.len: {:?}", tmp_scalars.len());

best_multiexp::<C>(&tmp_scalars, &tmp_bases)
}
Expand Down
7 changes: 7 additions & 0 deletions halo2_proofs/src/protostar/transcript/lookup.rs
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,9 @@ pub(crate) fn create_lookup_transcript<
singles_transcript: vec![],
};
}
println!("DEBUG :: num_lookups: {:?}", num_lookups);
let num_rows = params.n() as usize - pk.cs().blinding_factors() - 1 as usize;
println!("DEBUG :: num_rows: {:?}", num_rows);

let table_values_map: Vec<_> = lookups
.iter()
Expand All @@ -88,6 +90,9 @@ pub(crate) fn create_lookup_transcript<
})
.collect();

println!("DEBUG :: table_values_map.len: {:?}", table_values_map.len());
println!("DEBUG :: table_values_map[0].len: {:?}", table_values_map[0].len());

let m_polys: Vec<_> = lookups
.iter()
.zip(table_values_map.iter())
Expand All @@ -105,6 +110,8 @@ pub(crate) fn create_lookup_transcript<
.unwrap()
})
.collect();
println!("DEBUG :: m_polys.len: {:?}", m_polys.len());
println!("DEBUG :: m_polys[0].len: {:?}", m_polys[0].len());

let (m_commitments_projective, m_blinds): (Vec<_>, Vec<_>) = m_polys
.iter()
Expand Down
258 changes: 253 additions & 5 deletions halo2_proofs/src/protostar/verifier.rs
Original file line number Diff line number Diff line change
Expand Up @@ -248,13 +248,14 @@ impl<C: CurveAffine> VerifierAccumulator<C> {

#[cfg(test)]
mod tests {
use ff::{BatchInvert, FromUniformBytes};
use ff::{BatchInvert, FromUniformBytes, PrimeField, PrimeFieldBits};

use crate::{
arithmetic::{CurveAffine, Field},
circuit::{floor_planner::V1, Layouter, Value},
circuit::{floor_planner::V1, AssignedCell, Layouter, Value},
dev::{metadata, FailureLocation, MockProver, VerifyFailure},
plonk::*,
poly::Rotation,
poly::{
self,
commitment::ParamsProver,
Expand All @@ -272,9 +273,12 @@ mod tests {
},
};

use halo2curves::pasta::pallas;
use halo2curves::pasta::{pallas, Fp, self};
use rand_core::{OsRng, RngCore};
use std::iter::{self, zip};
use std::{
iter::{self, zip},
marker::PhantomData,
};

fn rand_2d_array<F: Field, R: RngCore, const W: usize, const H: usize>(
rng: &mut R,
Expand Down Expand Up @@ -507,6 +511,179 @@ mod tests {
}
}

/// A lookup table of values from 0..RANGE.
#[derive(Debug, Clone)]
pub(super) struct RangeTableConfig<F: PrimeFieldBits, const RANGE: usize> {
pub(super) value: TableColumn,
_marker: PhantomData<F>,
}

impl<F: PrimeFieldBits, const RANGE: usize> RangeTableConfig<F, RANGE> {
pub(super) fn configure(meta: &mut ConstraintSystem<F>) -> Self {
let value = meta.lookup_table_column();

Self {
value,
_marker: PhantomData,
}
}

pub(super) fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
layouter.assign_table(
|| "load range-check table",
|mut table| {
let mut offset = 0;
for value in 0..RANGE {
table.assign_cell(
|| "num_bits",
self.value,
offset,
|| Value::known(F::from(value as u64)),
)?;
offset += 1;
}

Ok(())
},
)
}
}

#[derive(Debug, Clone)]
/// A range-constrained value in the circuit produced by the RangeCheckConfig.
struct RangeConstrained<F: PrimeFieldBits, const RANGE: usize>(AssignedCell<Assigned<F>, F>);

#[derive(Debug, Clone)]
struct RangeCheckConfig<F: PrimeFieldBits, const RANGE: usize, const LOOKUP_RANGE: usize> {
q_range_check: Selector,
q_lookup: Selector,
value: Column<Advice>,
table: RangeTableConfig<F, LOOKUP_RANGE>,
}

impl<F: PrimeFieldBits, const RANGE: usize, const LOOKUP_RANGE: usize>
RangeCheckConfig<F, RANGE, LOOKUP_RANGE>
{
pub fn configure(meta: &mut ConstraintSystem<F>, value: Column<Advice>) -> Self {
let q_range_check = meta.selector();
let q_lookup = meta.complex_selector();
let table = RangeTableConfig::configure(meta);

meta.create_gate("range check", |meta| {
// value | q_range_check
// ------------------------------
// v | 1

let q = meta.query_selector(q_range_check);
let value = meta.query_advice(value, Rotation::cur());

// Given a range R and a value v, returns the expression
// (v) * (1 - v) * (2 - v) * ... * (R - 1 - v)
let range_check = |range: usize, value: Expression<F>| {
assert!(range > 0);
(1..range).fold(value.clone(), |expr, i| {
expr * (Expression::Constant(F::from(i as u64)) - value.clone())
})
};

Constraints::with_selector(q, [("range check", range_check(RANGE, value))])
});

meta.lookup("lookup", |meta| {
let q_lookup = meta.query_selector(q_lookup);
let value = meta.query_advice(value, Rotation::cur());

vec![(q_lookup * value, table.value)]
});

Self {
q_range_check,
q_lookup,
value,
table,
}
}

pub fn assign_simple(
&self,
mut layouter: impl Layouter<F>,
value: Value<Assigned<F>>,
) -> Result<RangeConstrained<F, RANGE>, Error> {
layouter.assign_region(
|| "Assign value for simple range check",
|mut region| {
let offset = 0;

// Enable q_range_check
self.q_range_check.enable(&mut region, offset)?;

// Assign value
region
.assign_advice(|| "value", self.value, offset, || value)
.map(RangeConstrained)
},
)
}

pub fn assign_lookup(
&self,
mut layouter: impl Layouter<F>,
value: Value<Assigned<F>>,
) -> Result<RangeConstrained<F, LOOKUP_RANGE>, Error> {
layouter.assign_region(
|| "Assign value for lookup range check",
|mut region| {
let offset = 0;

// Enable q_lookup
self.q_lookup.enable(&mut region, offset)?;

// Assign value
region
.assign_advice(|| "value", self.value, offset, || value)
.map(RangeConstrained)
},
)
}
}
#[derive(Default)]
struct RangeCheckCircuit<F: PrimeFieldBits, const RANGE: usize, const LOOKUP_RANGE: usize> {
value: Value<Assigned<F>>,
lookup_value: Value<Assigned<F>>,
}

impl<F: PrimeFieldBits, const RANGE: usize, const LOOKUP_RANGE: usize> Circuit<F>

Check failure on line 655 in halo2_proofs/src/protostar/verifier.rs

View workflow job for this annotation

GitHub Actions / Test on macOS-latest

not all trait items implemented, missing: `Params`

Check failure on line 655 in halo2_proofs/src/protostar/verifier.rs

View workflow job for this annotation

GitHub Actions / Test on ubuntu-latest

not all trait items implemented, missing: `Params`
for RangeCheckCircuit<F, RANGE, LOOKUP_RANGE>

Check failure on line 656 in halo2_proofs/src/protostar/verifier.rs

View workflow job for this annotation

GitHub Actions / Clippy (beta)

not all trait items implemented, missing: `Params`

error[E0046]: not all trait items implemented, missing: `Params` --> halo2_proofs/src/protostar/verifier.rs:655:5 | 655 | / impl<F: PrimeFieldBits, const RANGE: usize, const LOOKUP_RANGE: usize> Circuit<F> 656 | | for RangeCheckCircuit<F, RANGE, LOOKUP_RANGE> | |_____________________________________________________^ missing `Params` in implementation | ::: halo2_proofs/src/plonk/circuit.rs:774:5 | 774 | type Params: Default; | -------------------- `Params` from trait
{
type Config = RangeCheckConfig<F, RANGE, LOOKUP_RANGE>;
type FloorPlanner = V1;

fn without_witnesses(&self) -> Self {
Self::default()
}

fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let value = meta.advice_column();
RangeCheckConfig::configure(meta, value)
}

fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
config.table.load(&mut layouter)?;

config.assign_simple(layouter.namespace(|| "Assign simple value"), self.value)?;
config.assign_lookup(
layouter.namespace(|| "Assign lookup value"),
self.lookup_value,
)?;

Ok(())
}
}

fn check_v_and_p_transcripts<C: CurveAffine>(
v_acc: VerifierAccumulator<C>,
p_acc: Accumulator<C>,
Expand Down Expand Up @@ -680,7 +857,78 @@ mod tests {
}

#[test]
fn test_scroll_zkevm_keccak_circuit(){
fn test_lookup() {
let mut rng: OsRng = OsRng;
const K: u32 = 9;
const RANGE: usize = 8; // 3-bit value
const LOOKUP_RANGE: usize = 256; // 8-bit value

let params = poly::ipa::commitment::ParamsIPA::<pallas::Affine>::new(K);

let circuit0 = RangeCheckCircuit::<pallas::Scalar, RANGE, LOOKUP_RANGE> {
value: Value::known(pallas::Scalar::from(4).into()),
lookup_value: Value::known(pallas::Scalar::from(12).into()),
};

let circuit1 = RangeCheckCircuit::<pallas::Scalar, RANGE, LOOKUP_RANGE> {
value: Value::known(pallas::Scalar::from(5).into()),
lookup_value: Value::known(pallas::Scalar::from(220).into()),
};

// let params = poly::kzg::commitment::ParamsKZG::<halo2curves::bn256::Bn256>::new(K);
// let circuit0 = RangeCheckCircuit::<pallas::Scalar, RANGE, LOOKUP_RANGE> {
// value: Value::known(halo2curves::bn256::Fq::from(4).into()),
// lookup_value: Value::known(pasta::Fq::from(12).into()),
// };

// let circuit1 = RangeCheckCircuit::<pallas::Scalar, RANGE, LOOKUP_RANGE> {
// value: Value::known(pasta::Fq::from(5).into()),
// lookup_value: Value::known(pasta::Fq::from(220).into()),
// };

let prover0 = MockProver::run(K, &circuit0, vec![]).unwrap();
let prover1 = MockProver::run(K, &circuit1, vec![]).unwrap();

prover0.assert_satisfied();
prover1.assert_satisfied();

let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]);
let pk = protostar::ProvingKey::new(&params, &circuit0).unwrap();

let mut acc0 = protostar::prover::create_accumulator(
&params,
&pk,
&circuit0,
&[],
&mut rng,
&mut transcript,
)
.unwrap();
// let acc1 = protostar::prover::create_accumulator(
// &params,
// &pk,
// &circuit1,
// &[],
// &mut rng,
// &mut transcript,
// )
// .unwrap();

// let acc0_old = acc0.clone();

// acc0.fold(&pk, acc1.clone(), &mut transcript);

// let proof: Vec<u8> = transcript.finalize();
// let mut v_transcript = Blake2bRead::<_, _, Challenge255<_>>::init(&proof[..]);

// let mut v_acc0 = VerifierAccumulator::new_from_prover(&mut v_transcript, &[], &pk).unwrap();
// let v_acc1 = VerifierAccumulator::new_from_prover(&mut v_transcript, &[], &pk).unwrap();
// let v_acc0_old = v_acc0.clone();

// v_acc0.fold(&v_acc1.clone(), &pk, &mut v_transcript);

// check_v_and_p_transcripts(v_acc0_old, acc0_old);
// check_v_and_p_transcripts(v_acc1, acc1);
// check_v_and_p_transcripts(v_acc0, acc0);
}
}

0 comments on commit 7b166c6

Please sign in to comment.