Skip to content

Commit

Permalink
feat: FpChip::range_check now works with max_bits < n * (k-1) (#91)
Browse files Browse the repository at this point in the history
* feat(base): range_check 0 bits by asserting is zero

* chore: add range_check 0 bits test

* feat(ecc): `FpChip::range_check` now works with `max_bits < n * (k-1)`
  • Loading branch information
jonathanpwang authored Jul 7, 2023
1 parent de43c6f commit 57fe926
Show file tree
Hide file tree
Showing 4 changed files with 52 additions and 26 deletions.
4 changes: 4 additions & 0 deletions halo2-base/src/gates/range.rs
Original file line number Diff line number Diff line change
Expand Up @@ -505,6 +505,10 @@ impl<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
/// # Assumptions
/// * `ceil(range_bits / lookup_bits) * lookup_bits <= F::CAPACITY`
fn range_check(&self, ctx: &mut Context<F>, a: AssignedValue<F>, range_bits: usize) {
if range_bits == 0 {
self.gate.assert_is_const(ctx, &a, &F::zero());
return;
}
// the number of limbs
let k = (range_bits + self.lookup_bits - 1) / self.lookup_bits;
// println!("range check {} bits {} len", range_bits, k);
Expand Down
1 change: 1 addition & 0 deletions halo2-base/src/gates/tests/range_gate.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ use crate::{
use num_bigint::BigUint;
use test_case::test_case;

#[test_case(16, 10, Fr::zero(), 0; "range_check() 0 bits")]
#[test_case(16, 10, Fr::from(100), 8; "range_check() pos")]
pub fn test_range_check<F: ScalarField>(k: usize, lookup_bits: usize, a_val: F, range_bits: usize) {
set_var("LOOKUP_BITS", lookup_bits.to_string());
Expand Down
13 changes: 7 additions & 6 deletions halo2-ecc/src/fields/fp.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ use halo2_base::{
};
use num_bigint::{BigInt, BigUint};
use num_traits::One;
use std::cmp;
use std::{cmp::max, marker::PhantomData};

pub type BaseFieldChip<'range, C> =
Expand Down Expand Up @@ -298,7 +299,8 @@ impl<'range, F: PrimeField, Fp: PrimeField> FieldChip<F> for FpChip<'range, F, F
}

/// # Assumptions
/// * `max_bits` in `(n * (k - 1), n * k]`
/// * `max_bits <= n * k` where `n = self.limb_bits` and `k = self.num_limbs`
/// * `a.truncation.limbs.len() = self.num_limbs`
fn range_check(
&self,
ctx: &mut Context<F>,
Expand All @@ -307,15 +309,14 @@ impl<'range, F: PrimeField, Fp: PrimeField> FieldChip<F> for FpChip<'range, F, F
) {
let n = self.limb_bits;
let a = a.into();
let k = a.truncation.limbs.len();
debug_assert!(max_bits > n * (k - 1) && max_bits <= n * k);
let last_limb_bits = max_bits - n * (k - 1);
let mut remaining_bits = max_bits;

debug_assert!(a.value.bits() as usize <= max_bits);

// range check limbs of `a` are in [0, 2^n) except last limb should be in [0, 2^last_limb_bits)
for (i, cell) in a.truncation.limbs.into_iter().enumerate() {
let limb_bits = if i == k - 1 { last_limb_bits } else { n };
for cell in a.truncation.limbs {
let limb_bits = cmp::min(n, remaining_bits);
remaining_bits -= limb_bits;
self.range.range_check(ctx, cell, limb_bits);
}
}
Expand Down
60 changes: 40 additions & 20 deletions halo2-ecc/src/fields/tests/fp/mod.rs
Original file line number Diff line number Diff line change
@@ -1,9 +1,12 @@
use std::env::set_var;

use crate::fields::fp::FpChip;
use crate::fields::{FieldChip, PrimeField};
use crate::halo2_proofs::{
dev::MockProver,
halo2curves::bn256::{Fq, Fr},
};

use halo2_base::gates::builder::{GateThreadBuilder, RangeCircuitBuilder};
use halo2_base::gates::RangeChip;
use halo2_base::utils::biguint_to_fe;
Expand All @@ -15,39 +18,56 @@ pub mod assert_eq;

const K: usize = 10;

fn fp_mul_test<F: PrimeField>(
ctx: &mut Context<F>,
fn fp_chip_test(
k: usize,
lookup_bits: usize,
limb_bits: usize,
num_limbs: usize,
_a: Fq,
_b: Fq,
f: impl Fn(&mut Context<Fr>, &FpChip<Fr, Fq>),
) {
std::env::set_var("LOOKUP_BITS", lookup_bits.to_string());
let range = RangeChip::<F>::default(lookup_bits);
let chip = FpChip::<F, Fq>::new(&range, limb_bits, num_limbs);
set_var("LOOKUP_BITS", lookup_bits.to_string());
let range = RangeChip::<Fr>::default(lookup_bits);
let chip = FpChip::<Fr, Fq>::new(&range, limb_bits, num_limbs);

let [a, b] = [_a, _b].map(|x| chip.load_private(ctx, x));
let c = chip.mul(ctx, a, b);
let mut builder = GateThreadBuilder::mock();
f(builder.main(0), &chip);

assert_eq!(c.0.truncation.to_bigint(limb_bits), c.0.value);
assert_eq!(c.native().value(), &biguint_to_fe(&(c.value() % modulus::<F>())));
assert_eq!(c.0.value, fe_to_biguint(&(_a * _b)).into())
builder.config(k, Some(10));
let circuit = RangeCircuitBuilder::mock(builder);
MockProver::run(k as u32, &circuit, vec![]).unwrap().assert_satisfied();
}

#[test]
fn test_fp() {
let k = K;
let a = Fq::random(OsRng);
let b = Fq::random(OsRng);
let limb_bits = 88;
let num_limbs = 3;
fp_chip_test(K, K - 1, limb_bits, num_limbs, |ctx, chip| {
let _a = Fq::random(OsRng);
let _b = Fq::random(OsRng);

let mut builder = GateThreadBuilder::<Fr>::mock();
fp_mul_test(builder.main(0), k - 1, 88, 3, a, b);
let [a, b] = [_a, _b].map(|x| chip.load_private(ctx, x));
let c = chip.mul(ctx, a, b);

builder.config(k, Some(10));
let circuit = RangeCircuitBuilder::mock(builder);
assert_eq!(c.0.truncation.to_bigint(limb_bits), c.0.value);
assert_eq!(c.native().value(), &biguint_to_fe(&(c.value() % modulus::<Fr>())));
assert_eq!(c.0.value, fe_to_biguint(&(_a * _b)).into());
});
}

MockProver::run(k as u32, &circuit, vec![]).unwrap().assert_satisfied();
#[test]
fn test_range_check() {
fp_chip_test(K, K - 1, 88, 3, |ctx, chip| {
let mut range_test = |x, bits| {
let x = chip.load_private(ctx, x);
chip.range_check(ctx, x, bits);
};
let a = -Fq::one();
range_test(a, Fq::NUM_BITS as usize);
range_test(Fq::one(), 1);
range_test(Fq::from(u64::MAX), 64);
range_test(Fq::zero(), 1);
range_test(Fq::zero(), 0);
});
}

#[cfg(feature = "dev-graph")]
Expand Down

0 comments on commit 57fe926

Please sign in to comment.