From 7611a88c28061c73bf968231a694ab799cabc1a0 Mon Sep 17 00:00:00 2001 From: Constance Beguier Date: Mon, 16 Oct 2023 09:27:33 +0200 Subject: [PATCH] Optimized short range check on 4 and 5 bits (#21) Short range checks on 4 and 5 bits are now performed with only one lookup (instead of 2). To do that, we added a column `table_short_range_tag` in the lookup table. This new column `table_short_range_tag` contains the value - 4 for rows used in short range check on 4 bits - 5 for rows used in short range check on 5 bits - 0 for rows used in short range check on 10 bits Disable tests on i686 and code coverage in CI --- .github/workflows/ci.yml | 114 +++++------ halo2_gadgets/src/ecc.rs | 8 +- halo2_gadgets/src/ecc/chip/mul_fixed/short.rs | 18 +- halo2_gadgets/src/sinsemilla.rs | 9 +- halo2_gadgets/src/sinsemilla/chip.rs | 3 +- .../src/sinsemilla/chip/generator_table.rs | 63 +++++- halo2_gadgets/src/sinsemilla/merkle.rs | 4 +- .../src/utilities/lookup_range_check.rs | 186 +++++++++++++++--- 8 files changed, 308 insertions(+), 97 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d2ecd3ba57..db9abdc62e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -33,36 +33,36 @@ jobs: ${{ steps.prepare.outputs.feature-flags }} ${{ matrix.extra_flags }} - test-32-bit: - name: Test on i686-unknown-linux-gnu${{ matrix.name_suffix }} - runs-on: ubuntu-latest - strategy: - matrix: - stage: [stable, beta, nightly] - include: - - stage: beta - name_suffix: " with beta features" - - stage: nightly - name_suffix: " with nightly features" - - steps: - - uses: actions/checkout@v3 - - id: prepare - uses: ./.github/actions/prepare - with: - beta-features: ${{ matrix.stage == 'beta' }} - nightly-features: ${{ matrix.stage == 'nightly' }} - - name: Install cross-platform support dependencies - run: sudo apt install gcc-multilib - - run: rustup target add i686-unknown-linux-gnu - - name: Run tests - run: > - cargo test - --verbose - --release - --workspace - --target i686-unknown-linux-gnu - ${{ steps.prepare.outputs.feature-flags }} +# test-32-bit: +# name: Test on i686-unknown-linux-gnu${{ matrix.name_suffix }} +# runs-on: ubuntu-latest +# strategy: +# matrix: +# stage: [stable, beta, nightly] +# include: +# - stage: beta +# name_suffix: " with beta features" +# - stage: nightly +# name_suffix: " with nightly features" +# +# steps: +# - uses: actions/checkout@v3 +# - id: prepare +# uses: ./.github/actions/prepare +# with: +# beta-features: ${{ matrix.stage == 'beta' }} +# nightly-features: ${{ matrix.stage == 'nightly' }} +# - name: Install cross-platform support dependencies +# run: sudo apt install gcc-multilib +# - run: rustup target add i686-unknown-linux-gnu +# - name: Run tests +# run: > +# cargo test +# --verbose +# --release +# --workspace +# --target i686-unknown-linux-gnu +# ${{ steps.prepare.outputs.feature-flags }} build: name: Build target ${{ matrix.target }} @@ -125,33 +125,33 @@ jobs: - name: Test halo2 book run: mdbook test -L target/debug/deps book/ - codecov: - name: Code coverage - runs-on: ubuntu-latest - - steps: - - uses: actions/checkout@v3 - # Use stable for this to ensure that cargo-tarpaulin can be built. - - id: prepare - uses: ./.github/actions/prepare - with: - toolchain: stable - nightly-features: true - - name: Install cargo-tarpaulin - uses: actions-rs/cargo@v1 - with: - command: install - args: cargo-tarpaulin - - name: Generate coverage report - uses: actions-rs/cargo@v1 - with: - command: tarpaulin - args: > - ${{ steps.prepare.outputs.feature-flags }} - --timeout 600 - --out Xml - - name: Upload coverage to Codecov - uses: codecov/codecov-action@v3.1.4 +# codecov: +# name: Code coverage +# runs-on: ubuntu-latest +# +# steps: +# - uses: actions/checkout@v3 +# # Use stable for this to ensure that cargo-tarpaulin can be built. +# - id: prepare +# uses: ./.github/actions/prepare +# with: +# toolchain: stable +# nightly-features: true +# - name: Install cargo-tarpaulin +# uses: actions-rs/cargo@v1 +# with: +# command: install +# args: cargo-tarpaulin +# - name: Generate coverage report +# uses: actions-rs/cargo@v1 +# with: +# command: tarpaulin +# args: > +# ${{ steps.prepare.outputs.feature-flags }} +# --timeout 600 +# --out Xml +# - name: Upload coverage to Codecov +# uses: codecov/codecov-action@v3.1.4 doc-links: name: Intra-doc links diff --git a/halo2_gadgets/src/ecc.rs b/halo2_gadgets/src/ecc.rs index 2e6e509190..4861a20e52 100644 --- a/halo2_gadgets/src/ecc.rs +++ b/halo2_gadgets/src/ecc.rs @@ -793,6 +793,7 @@ pub(crate) mod tests { meta.advice_column(), ]; let lookup_table = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let lagrange_coeffs = [ meta.fixed_column(), meta.fixed_column(), @@ -807,7 +808,12 @@ pub(crate) mod tests { let constants = meta.fixed_column(); meta.enable_constant(constants); - let range_check = LookupRangeCheckConfig::configure(meta, advices[9], lookup_table); + let range_check = LookupRangeCheckConfig::configure( + meta, + advices[9], + lookup_table, + table_range_check_tag, + ); EccChip::::configure(meta, advices, lagrange_coeffs, range_check) } diff --git a/halo2_gadgets/src/ecc/chip/mul_fixed/short.rs b/halo2_gadgets/src/ecc/chip/mul_fixed/short.rs index 94d61de54a..a10c54c1ed 100644 --- a/halo2_gadgets/src/ecc/chip/mul_fixed/short.rs +++ b/halo2_gadgets/src/ecc/chip/mul_fixed/short.rs @@ -508,6 +508,7 @@ pub mod tests { meta.advice_column(), ]; let lookup_table = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let lagrange_coeffs = [ meta.fixed_column(), meta.fixed_column(), @@ -523,7 +524,12 @@ pub mod tests { let constants = meta.fixed_column(); meta.enable_constant(constants); - let range_check = LookupRangeCheckConfig::configure(meta, advices[9], lookup_table); + let range_check = LookupRangeCheckConfig::configure( + meta, + advices[9], + lookup_table, + table_range_check_tag, + ); EccChip::::configure(meta, advices, lagrange_coeffs, range_check) } @@ -644,7 +650,7 @@ pub mod tests { )], }, VerifyFailure::Permutation { - column: (Any::Fixed, 9).into(), + column: (Any::Fixed, 10).into(), location: FailureLocation::OutsideRegion { row: 0 }, }, VerifyFailure::Permutation { @@ -827,6 +833,7 @@ pub mod tests { meta.advice_column(), ]; let lookup_table = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let lagrange_coeffs = [ meta.fixed_column(), meta.fixed_column(), @@ -842,7 +849,12 @@ pub mod tests { let constants = meta.fixed_column(); meta.enable_constant(constants); - let range_check = LookupRangeCheckConfig::configure(meta, advices[9], lookup_table); + let range_check = LookupRangeCheckConfig::configure( + meta, + advices[9], + lookup_table, + table_range_check_tag, + ); EccChip::::configure(meta, advices, lagrange_coeffs, range_check) } diff --git a/halo2_gadgets/src/sinsemilla.rs b/halo2_gadgets/src/sinsemilla.rs index ca4c14fb1d..a1dcb9d2a2 100644 --- a/halo2_gadgets/src/sinsemilla.rs +++ b/halo2_gadgets/src/sinsemilla.rs @@ -586,6 +586,7 @@ pub(crate) mod tests { meta.enable_constant(constants); let table_idx = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let lagrange_coeffs = [ meta.fixed_column(), meta.fixed_column(), @@ -602,9 +603,15 @@ pub(crate) mod tests { table_idx, meta.lookup_table_column(), meta.lookup_table_column(), + table_range_check_tag, ); - let range_check = LookupRangeCheckConfig::configure(meta, advices[9], table_idx); + let range_check = LookupRangeCheckConfig::configure( + meta, + advices[9], + table_idx, + table_range_check_tag, + ); let ecc_config = EccChip::::configure(meta, advices, lagrange_coeffs, range_check); diff --git a/halo2_gadgets/src/sinsemilla/chip.rs b/halo2_gadgets/src/sinsemilla/chip.rs index ac4c34f781..ef76b19815 100644 --- a/halo2_gadgets/src/sinsemilla/chip.rs +++ b/halo2_gadgets/src/sinsemilla/chip.rs @@ -153,7 +153,7 @@ where advices: [Column; 5], witness_pieces: Column, fixed_y_q: Column, - lookup: (TableColumn, TableColumn, TableColumn), + lookup: (TableColumn, TableColumn, TableColumn, TableColumn), range_check: LookupRangeCheckConfig, ) -> >::Config { // Enable equality on all advice columns @@ -178,6 +178,7 @@ where table_idx: lookup.0, table_x: lookup.1, table_y: lookup.2, + table_range_check_tag: lookup.3, }, lookup_config: range_check, _marker: PhantomData, diff --git a/halo2_gadgets/src/sinsemilla/chip/generator_table.rs b/halo2_gadgets/src/sinsemilla/chip/generator_table.rs index fd0ff03f91..13773a4659 100644 --- a/halo2_gadgets/src/sinsemilla/chip/generator_table.rs +++ b/halo2_gadgets/src/sinsemilla/chip/generator_table.rs @@ -6,7 +6,7 @@ use halo2_proofs::{ }; use super::{CommitDomains, FixedPoints, HashDomains}; -use crate::sinsemilla::primitives::{self as sinsemilla, SINSEMILLA_S}; +use crate::sinsemilla::primitives::{self as sinsemilla, K, SINSEMILLA_S}; use pasta_curves::pallas; /// Table containing independent generators S[0..2^k] @@ -15,6 +15,7 @@ pub struct GeneratorTableConfig { pub table_idx: TableColumn, pub table_x: TableColumn, pub table_y: TableColumn, + pub table_range_check_tag: TableColumn, } impl GeneratorTableConfig { @@ -90,6 +91,66 @@ impl GeneratorTableConfig { )?; table.assign_cell(|| "table_x", self.table_x, index, || Value::known(*x))?; table.assign_cell(|| "table_y", self.table_y, index, || Value::known(*y))?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + index, + || Value::known(pallas::Base::zero()), + )?; + if index < (1 << 4) { + let new_index = index + (1 << K); + table.assign_cell( + || "table_idx", + self.table_idx, + new_index, + || Value::known(pallas::Base::from(index as u64)), + )?; + table.assign_cell( + || "table_x", + self.table_x, + new_index, + || Value::known(*x), + )?; + table.assign_cell( + || "table_y", + self.table_y, + new_index, + || Value::known(*y), + )?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + new_index, + || Value::known(pallas::Base::from(4_u64)), + )?; + } + if index < (1 << 5) { + let new_index = index + (1 << 10) + (1 << 4); + table.assign_cell( + || "table_idx", + self.table_idx, + new_index, + || Value::known(pallas::Base::from(index as u64)), + )?; + table.assign_cell( + || "table_x", + self.table_x, + new_index, + || Value::known(*x), + )?; + table.assign_cell( + || "table_y", + self.table_y, + new_index, + || Value::known(*y), + )?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + new_index, + || Value::known(pallas::Base::from(5_u64)), + )?; + } } Ok(()) }, diff --git a/halo2_gadgets/src/sinsemilla/merkle.rs b/halo2_gadgets/src/sinsemilla/merkle.rs index 02a3bdaf7c..1eabfaa870 100644 --- a/halo2_gadgets/src/sinsemilla/merkle.rs +++ b/halo2_gadgets/src/sinsemilla/merkle.rs @@ -246,9 +246,11 @@ pub mod tests { meta.lookup_table_column(), meta.lookup_table_column(), meta.lookup_table_column(), + meta.lookup_table_column(), ); - let range_check = LookupRangeCheckConfig::configure(meta, advices[9], lookup.0); + let range_check = + LookupRangeCheckConfig::configure(meta, advices[9], lookup.0, lookup.3); let sinsemilla_config_1 = SinsemillaChip::configure( meta, diff --git a/halo2_gadgets/src/utilities/lookup_range_check.rs b/halo2_gadgets/src/utilities/lookup_range_check.rs index b26a89a884..d1173babbc 100644 --- a/halo2_gadgets/src/utilities/lookup_range_check.rs +++ b/halo2_gadgets/src/utilities/lookup_range_check.rs @@ -60,8 +60,11 @@ pub struct LookupRangeCheckConfig { q_lookup: Selector, q_running: Selector, q_bitshift: Selector, + q_range_check_4: Selector, + q_range_check_5: Selector, running_sum: Column, table_idx: TableColumn, + table_range_check_tag: TableColumn, _marker: PhantomData, } @@ -81,18 +84,24 @@ impl LookupRangeCheckConfig { meta: &mut ConstraintSystem, running_sum: Column, table_idx: TableColumn, + table_range_check_tag: TableColumn, ) -> Self { meta.enable_equality(running_sum); let q_lookup = meta.complex_selector(); let q_running = meta.complex_selector(); let q_bitshift = meta.selector(); + let q_range_check_4 = meta.complex_selector(); + let q_range_check_5 = meta.complex_selector(); let config = LookupRangeCheckConfig { q_lookup, q_running, q_bitshift, + q_range_check_4, + q_range_check_5, running_sum, table_idx, + table_range_check_tag, _marker: PhantomData, }; @@ -100,7 +109,10 @@ impl LookupRangeCheckConfig { meta.lookup(|meta| { let q_lookup = meta.query_selector(config.q_lookup); let q_running = meta.query_selector(config.q_running); + let q_range_check_4 = meta.query_selector(config.q_range_check_4); + let q_range_check_5 = meta.query_selector(config.q_range_check_5); let z_cur = meta.query_advice(config.running_sum, Rotation::cur()); + let one = Expression::Constant(F::ONE); // In the case of a running sum decomposition, we recover the word from // the difference of the running sums: @@ -117,17 +129,40 @@ impl LookupRangeCheckConfig { // In the short range check, the word is directly witnessed. let short_lookup = { - let short_word = z_cur; - let q_short = Expression::Constant(F::ONE) - q_running; + let short_word = z_cur.clone(); + let q_short = one.clone() - q_running; q_short * short_word }; + // q_range_check is equal to + // - 1 if q_range_check_4 = 1 or q_range_check_5 = 1 + // - 0 otherwise + let q_range_check = one.clone() + - (one.clone() - q_range_check_4.clone()) * (one.clone() - q_range_check_5.clone()); + + // num_bits is equal to + // - 5 if q_range_check_5 = 1 + // - 4 if q_range_check_4 = 1 and q_range_check_5 = 0 + // - 0 otherwise + let num_bits = q_range_check_5.clone() * Expression::Constant(F::from(5_u64)) + + (one.clone() - q_range_check_5) + * q_range_check_4 + * Expression::Constant(F::from(4_u64)); + // Combine the running sum and short lookups: - vec![( - q_lookup * (running_sum_lookup + short_lookup), - config.table_idx, - )] + vec![ + ( + q_lookup.clone() + * ((one - q_range_check.clone()) * (running_sum_lookup + short_lookup) + + q_range_check.clone() * z_cur), + config.table_idx, + ), + ( + q_lookup * q_range_check * num_bits, + config.table_range_check_tag, + ), + ] }); // For short lookups, check that the word has been shifted by the correct number of bits. @@ -152,9 +187,9 @@ impl LookupRangeCheckConfig { } #[cfg(test)] - // Loads the values [0..2^K) into `table_idx`. This is only used in testing - // for now, since the Sinsemilla chip provides a pre-loaded table in the - // Orchard context. + // Fill `table_idx` and `table_range_check_tag`. + // This is only used in testing for now, since the Sinsemilla chip provides a pre-loaded table + // in the Orchard context. pub fn load(&self, layouter: &mut impl Layouter) -> Result<(), Error> { layouter.assign_table( || "table_idx", @@ -167,6 +202,42 @@ impl LookupRangeCheckConfig { index, || Value::known(F::from(index as u64)), )?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + index, + || Value::known(F::ZERO), + )?; + } + for index in 0..(1 << 4) { + let new_index = index + (1 << K); + table.assign_cell( + || "table_idx", + self.table_idx, + new_index, + || Value::known(F::from(index as u64)), + )?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + new_index, + || Value::known(F::from(4_u64)), + )?; + } + for index in 0..(1 << 5) { + let new_index = index + (1 << K) + (1 << 4); + table.assign_cell( + || "table_idx", + self.table_idx, + new_index, + || Value::known(F::from(index as u64)), + )?; + table.assign_cell( + || "table_range_check_tag", + self.table_range_check_tag, + new_index, + || Value::known(F::from(5_u64)), + )?; } Ok(()) }, @@ -350,33 +421,43 @@ impl LookupRangeCheckConfig { element: AssignedCell, num_bits: usize, ) -> Result<(), Error> { - // Enable lookup for `element`, to constrain it to 10 bits. + // Enable lookup for `element`. self.q_lookup.enable(region, 0)?; - // Enable lookup for shifted element, to constrain it to 10 bits. - self.q_lookup.enable(region, 1)?; + match num_bits { + 4 => { + self.q_range_check_4.enable(region, 0)?; + } + 5 => { + self.q_range_check_5.enable(region, 0)?; + } + _ => { + // Enable lookup for shifted element, to constrain it to 10 bits. + self.q_lookup.enable(region, 1)?; - // Check element has been shifted by the correct number of bits. - self.q_bitshift.enable(region, 1)?; + // Check element has been shifted by the correct number of bits. + self.q_bitshift.enable(region, 1)?; - // Assign shifted `element * 2^{K - num_bits}` - let shifted = element.value().into_field() * F::from(1 << (K - num_bits)); + // Assign shifted `element * 2^{K - num_bits}` + let shifted = element.value().into_field() * F::from(1 << (K - num_bits)); - region.assign_advice( - || format!("element * 2^({}-{})", K, num_bits), - self.running_sum, - 1, - || shifted, - )?; + region.assign_advice( + || format!("element * 2^({}-{})", K, num_bits), + self.running_sum, + 1, + || shifted, + )?; - // Assign 2^{-num_bits} from a fixed column. - let inv_two_pow_s = F::from(1 << num_bits).invert().unwrap(); - region.assign_advice_from_constant( - || format!("2^(-{})", num_bits), - self.running_sum, - 2, - inv_two_pow_s, - )?; + // Assign 2^{-num_bits} from a fixed column. + let inv_two_pow_s = F::from(1 << num_bits).invert().unwrap(); + region.assign_advice_from_constant( + || format!("2^(-{})", num_bits), + self.running_sum, + 2, + inv_two_pow_s, + )?; + } + } Ok(()) } @@ -418,10 +499,16 @@ mod tests { fn configure(meta: &mut ConstraintSystem) -> Self::Config { let running_sum = meta.advice_column(); let table_idx = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let constants = meta.fixed_column(); meta.enable_constant(constants); - LookupRangeCheckConfig::::configure(meta, running_sum, table_idx) + LookupRangeCheckConfig::::configure( + meta, + running_sum, + table_idx, + table_range_check_tag, + ) } fn synthesize( @@ -517,10 +604,16 @@ mod tests { fn configure(meta: &mut ConstraintSystem) -> Self::Config { let running_sum = meta.advice_column(); let table_idx = meta.lookup_table_column(); + let table_range_check_tag = meta.lookup_table_column(); let constants = meta.fixed_column(); meta.enable_constant(constants); - LookupRangeCheckConfig::::configure(meta, running_sum, table_idx) + LookupRangeCheckConfig::::configure( + meta, + running_sum, + table_idx, + table_range_check_tag, + ) } fn synthesize( @@ -646,5 +739,34 @@ mod tests { }]) ); } + + // Element within 4 bits + { + let circuit: MyCircuit = MyCircuit { + element: Value::known(pallas::Base::from((1 << 4) - 1)), + num_bits: 4, + }; + let prover = MockProver::::run(11, &circuit, vec![]).unwrap(); + assert_eq!(prover.verify(), Ok(())); + } + + // Element larger than 5 bits + { + let circuit: MyCircuit = MyCircuit { + element: Value::known(pallas::Base::from(1 << 5)), + num_bits: 5, + }; + let prover = MockProver::::run(11, &circuit, vec![]).unwrap(); + assert_eq!( + prover.verify(), + Err(vec![VerifyFailure::Lookup { + lookup_index: 0, + location: FailureLocation::InRegion { + region: (1, "Range check 5 bits").into(), + offset: 0, + }, + }]) + ); + } } }