Apply sumcheck to nonzero constraints directly

.vscode/settings.json

@@ -4,4 +4,5 @@
     "editor.formatOnSave": true,
     "editor.formatOnSaveMode": "file"
   },
+  "cSpell.words": ["hyperplonk", "plonkish", "layouter", "sumcheck"]
 }

prover/Cargo.toml

@@ -13,7 +13,7 @@ parallel = ["dep:rayon"]
 frontend-halo2 = ["dep:halo2_proofs"]
 
 [dependencies]
-plonkish_backend = { git = "https://github.com/summa-dev/plonkish", branch="summa-changes", package = "plonkish_backend", features= ["frontend-halo2", "benchmark"] }
+plonkish_backend = { git = "https://github.com/summa-dev/plonkish", branch="nonzero-constraints", package = "plonkish_backend", features= ["frontend-halo2", "benchmark"] }
 plotters = { version = "0.3.4", optional = true }
 rand = "0.8"
 csv = "1.1"

prover/benches/proof_of_liabilities.rs

@@ -14,7 +14,7 @@ use rand::{
     CryptoRng, Rng, RngCore, SeedableRng,
 };
 use summa_hyperplonk::{
-    circuits::summa_circuit::summa_hyperplonk::SummaHyperplonk,
+    circuits::{config::range_check_config::RangeCheckConfig, summa_circuit::SummaHyperplonk},
     utils::{big_uint_to_fp, generate_dummy_entries, uni_to_multivar_binary_index},
 };
 
@@ -30,12 +30,15 @@ fn bench_summa<const K: u32, const N_USERS: usize, const N_CURRENCIES: usize>()
 
     type ProvingBackend = HyperPlonk<MultilinearKzg<Bn256>>;
     let entries = generate_dummy_entries::<N_USERS, N_CURRENCIES>().unwrap();
-    let halo2_circuit = SummaHyperplonk::<N_USERS, N_CURRENCIES>::init(entries.to_vec());
+    let halo2_circuit =
+        SummaHyperplonk::<N_USERS, N_CURRENCIES, RangeCheckConfig<N_CURRENCIES, N_USERS>>::init(
+            entries.to_vec(),
+        );
 
-    let circuit = Halo2Circuit::<Fp, SummaHyperplonk<N_USERS, N_CURRENCIES>>::new::<ProvingBackend>(
-        K as usize,
-        halo2_circuit.clone(),
-    );
+    let circuit = Halo2Circuit::<
+        Fp,
+        SummaHyperplonk<N_USERS, N_CURRENCIES, RangeCheckConfig<N_CURRENCIES, N_USERS>>,
+    >::new::<ProvingBackend>(K as usize, halo2_circuit.clone());
 
     let circuit_info: PlonkishCircuitInfo<_> = circuit.circuit_info().unwrap();
     let instances = circuit.instances();
@@ -46,10 +49,10 @@ fn bench_summa<const K: u32, const N_USERS: usize, const N_CURRENCIES: usize>()
     c.bench_function(&grand_sum_proof_bench_name, |b| {
         b.iter_batched(
             || {
-                Halo2Circuit::<Fp, SummaHyperplonk<N_USERS, N_CURRENCIES>>::new::<ProvingBackend>(
-                    K as usize,
-                    halo2_circuit.clone(),
-                )
+                Halo2Circuit::<
+                    Fp,
+                    SummaHyperplonk<N_USERS, N_CURRENCIES, RangeCheckConfig<N_CURRENCIES, N_USERS>>,
+                >::new::<ProvingBackend>(K as usize, halo2_circuit.clone())
             },
             |circuit| {
                 let mut transcript = Keccak256Transcript::default();
@@ -189,7 +192,7 @@ fn bench_summa<const K: u32, const N_USERS: usize, const N_CURRENCIES: usize>()
 }
 
 fn criterion_benchmark(_c: &mut Criterion) {
-    const N_CURRENCIES: usize = 1;
+    const N_CURRENCIES: usize = 100;
 
     {
         const K: u32 = 17;

prover/src/chips/range/range_check.rs

@@ -2,7 +2,7 @@ use crate::chips::range::utils::decompose_fp_to_byte_pairs;
 use halo2_proofs::arithmetic::Field;
 use halo2_proofs::circuit::{AssignedCell, Region, Value};
 use halo2_proofs::halo2curves::bn256::Fr as Fp;
-use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed};
+use halo2_proofs::plonk::{Advice, Column, ConstraintSystem, Error, Expression, Fixed, Selector};
 use halo2_proofs::poly::Rotation;
 use std::fmt::Debug;
 
@@ -27,17 +27,17 @@ use std::fmt::Debug;
 /// # Fields
 ///
 /// * `zs`: Four advice columns - contain the truncated right-shifted values of the element to be checked
-/// * `z0`: An advice column - for storing the zero value from the instance column
-/// * `instance`: An instance column - zero value provided to the circuit
+/// * `selector`: Selector used to enable the range check
 ///
 /// # Assumptions
 ///
 /// * The lookup table `range_u16` is by default loaded with values from 0 to 2^16 - 1.
 ///
 /// Patterned after [halo2_gadgets](https://github.com/privacy-scaling-explorations/halo2/blob/main/halo2_gadgets/src/utilities/decompose_running_sum.rs)
 #[derive(Debug, Copy, Clone)]
-pub struct RangeCheckU64Config {
+pub struct RangeCheckChipConfig {
     zs: [Column<Advice>; 4],
+    selector: Selector,
 }
 
 /// Helper chip that verifies that the element witnessed in a given cell lies within the u64 range.
@@ -72,22 +72,23 @@ pub struct RangeCheckU64Config {
 /// zs[3] == z0
 #[derive(Debug, Clone)]
 pub struct RangeCheckU64Chip {
-    config: RangeCheckU64Config,
+    config: RangeCheckChipConfig,
 }
 
 impl RangeCheckU64Chip {
-    pub fn construct(config: RangeCheckU64Config) -> Self {
+    pub fn construct(config: RangeCheckChipConfig) -> Self {
         Self { config }
     }
 
     /// Configures the Range Chip
-    /// Note: the lookup table should be loaded with values from `0` to `2^16 - 1` otherwise the range check will fail.
+    /// Note: the lookup table should be loaded with values from `0` to `2^16 - 1`, otherwise the range check will fail.
     pub fn configure(
         meta: &mut ConstraintSystem<Fp>,
         z: Column<Advice>,
         zs: [Column<Advice>; 4],
         range_u16: Column<Fixed>,
-    ) -> RangeCheckU64Config {
+        range_check_enabled: Selector,
+    ) -> RangeCheckChipConfig {
         // Constraint that the difference between the element to be checked and the 0-th truncated right-shifted value of the element to be within the range.
         // z - 2^16⋅zs[0] = ks[0] ∈ range_u16
         meta.lookup_any(
@@ -99,7 +100,9 @@ impl RangeCheckU64Chip {
 
                 let range_u16 = meta.query_fixed(range_u16, Rotation::cur());
 
-                let diff = element - zero_truncation * Expression::Constant(Fp::from(1 << 16));
+                let s = meta.query_selector(range_check_enabled);
+
+                let diff = s * (element - zero_truncation * Expression::Constant(Fp::from(1 << 16)));
 
                 vec![(diff, range_u16)]
             },
@@ -123,7 +126,10 @@ impl RangeCheckU64Chip {
             );
         }
 
-        RangeCheckU64Config { zs }
+        RangeCheckChipConfig {
+            zs,
+            selector: range_check_enabled,
+        }
     }
 
     /// Assign the truncated right-shifted values of the element to be checked to the corresponding columns zs at offset 0 starting from the element to be checked.
@@ -163,6 +169,8 @@ impl RangeCheckU64Chip {
             zs.push(z.clone());
         }
 
+        self.config.selector.enable(region, 0)?;
+
         Ok(())
     }
 }

prover/src/chips/range/tests.rs

@@ -1,4 +1,4 @@
-use crate::chips::range::range_check::{RangeCheckU64Chip, RangeCheckU64Config};
+use crate::chips::range::range_check::{RangeCheckChipConfig, RangeCheckU64Chip};
 use halo2_proofs::{
     circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value},
     halo2curves::bn256::Fr as Fp,
@@ -87,7 +87,7 @@ impl AddChip {
 #[derive(Debug, Clone)]
 pub struct TestConfig {
     pub addchip_config: AddConfig,
-    pub range_check_config: RangeCheckU64Config,
+    pub range_check_config: RangeCheckChipConfig,
     pub range_u16: Column<Fixed>,
     pub instance: Column<Instance>,
 }
@@ -134,7 +134,10 @@ impl Circuit<Fp> for TestCircuit {
         let instance = meta.instance_column();
         meta.enable_equality(instance);
 
-        let range_check_config = RangeCheckU64Chip::configure(meta, c, zs, range_u16);
+        let range_check_selector = meta.complex_selector();
+
+        let range_check_config =
+            RangeCheckU64Chip::configure(meta, c, zs, range_u16, range_check_selector);
 
         let addchip_config = AddChip::configure(meta, a, b, c, add_selector);
 

prover/src/circuits/config/circuit_config.rs

@@ -0,0 +1,119 @@
+use halo2_proofs::{
+    circuit::{Layouter, Value},
+    plonk::{Advice, Column, ConstraintSystem, Error, Instance},
+};
+
+use crate::{entry::Entry, utils::big_uint_to_fp};
+
+use crate::chips::range::range_check::RangeCheckU64Chip;
+use halo2_proofs::halo2curves::bn256::Fr as Fp;
+
+/// The abstract configuration of the circuit.
+/// The default implementation assigns the entries and grand total to the circuit, and constrains
+/// grand total to the instance values.
+///
+/// The specific implementations have to provide the range check logic.
+pub trait CircuitConfig<const N_CURRENCIES: usize, const N_USERS: usize>: Clone {
+    /// Configures the circuit
+    fn configure(
+        meta: &mut ConstraintSystem<Fp>,
+        username: Column<Advice>,
+        balances: [Column<Advice>; N_CURRENCIES],
+        instance: Column<Instance>,
+    ) -> Self;
+
+    fn get_username(&self) -> Column<Advice>;
+
+    fn get_balances(&self) -> [Column<Advice>; N_CURRENCIES];
+
+    fn get_instance(&self) -> Column<Instance>;
+
+    /// Assigns the entries to the circuit, constrains the grand total to the instance values.
+    fn synthesize(
+        &self,
+        mut layouter: impl Layouter<Fp>,
+        entries: &[Entry<N_CURRENCIES>],
+        grand_total: &[Fp],
+    ) -> Result<(), Error> {
+        // Initiate the range check chips
+        let range_check_chips = self.initialize_range_check_chips();
+
+        for (i, entry) in entries.iter().enumerate() {
+            let last_decompositions = layouter.assign_region(
+                || format!("assign entry {} to the table", i),
+                |mut region| {
+                    region.assign_advice(
+                        || "username",
+                        self.get_username(),
+                        0,
+                        || Value::known(big_uint_to_fp::<Fp>(entry.username_as_big_uint())),
+                    )?;
+
+                    let mut last_decompositions = vec![];
+
+                    for (j, balance) in entry.balances().iter().enumerate() {
+                        let assigned_balance = region.assign_advice(
+                            || format!("balance {}", j),
+                            self.get_balances()[j],
+                            0,
+                            || Value::known(big_uint_to_fp(balance)),
+                        )?;
+
+                        let mut zs = Vec::with_capacity(4);
+
+                        if !range_check_chips.is_empty() {
+                            range_check_chips[j].assign(&mut region, &mut zs, &assigned_balance)?;
+
+                            last_decompositions.push(zs[3].clone());
+                        }
+                    }
+
+                    Ok(last_decompositions)
+                },
+            )?;
+
+            self.constrain_decompositions(last_decompositions, &mut layouter)?;
+        }
+
+        let assigned_total = layouter.assign_region(
+            || "assign total".to_string(),
+            |mut region| {
+                let mut assigned_total = vec![];
+
+                for (j, total) in grand_total.iter().enumerate() {
+                    let balance_total = region.assign_advice(
+                        || format!("total {}", j),
+                        self.get_balances()[j],
+                        0,
+                        || Value::known(total.neg()),
+                    )?;
+
+                    assigned_total.push(balance_total);
+                }
+
+                Ok(assigned_total)
+            },
+        )?;
+
+        for (j, total) in assigned_total.iter().enumerate() {
+            layouter.constrain_instance(total.cell(), self.get_instance(), 1 + j)?;
+        }
+
+        self.load_lookup_table(layouter)?;
+
+        Ok(())
+    }
+
+    /// Initializes the range check chips
+    fn initialize_range_check_chips(&self) -> Vec<RangeCheckU64Chip>;
+
+    /// Loads the lookup table
+    fn load_lookup_table(&self, layouter: impl Layouter<Fp>) -> Result<(), Error>;
+
+    /// Constrains the last decompositions of the balances to be zero
+    fn constrain_decompositions(
+        &self,
+        last_decompositions: Vec<halo2_proofs::circuit::AssignedCell<Fp, Fp>>,
+        layouter: &mut impl Layouter<Fp>,
+    ) -> Result<(), Error>;
+}

prover/src/circuits/config/mod.rs

@@ -0,0 +1,3 @@
+pub mod circuit_config;
+pub mod no_range_check_config;
+pub mod range_check_config;