Merge pull request #48 from summa-dev/feat-recursive-verifier

Feat recursive verifier

zk_prover/Cargo.toml

@@ -13,6 +13,7 @@ halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2",
 halo2_gadgets = { git = "https://github.com/privacy-scaling-explorations/halo2", tag = "v2023_04_20"}
 ecdsa = { git = "https://github.com/privacy-scaling-explorations/halo2wrong"}
 ecc = { git = "https://github.com/privacy-scaling-explorations/halo2wrong"}
+maingate =  { git = "https://github.com/privacy-scaling-explorations/halo2wrong", tag = "v2023_04_20" }
 gadgets = { git = "https://github.com/privacy-scaling-explorations/zkevm-circuits"}
 plotters = { version = "0.3.4", optional = true }
 rand = "0.8"
@@ -23,6 +24,8 @@ serde = { version = "1.0", features = ["derive"] }
 hex = "0.4.3"
 num-bigint = "0.4"
 num_cpus = "1.15"
+snark-verifier-sdk = { git = "https://github.com/privacy-scaling-explorations/snark-verifier"}
+itertools = "0.10.3"
 
 [dev-dependencies]
 criterion= "0.3"

zk_prover/README.md

@@ -28,6 +28,11 @@ cargo build
 cargo test --features dev-graph -- --nocapture
 ```
 
+To run the on-chain verifer test run
+```
+cargo test --release  -- --ignored --nocapture test_valid_merkle_sum_tree_with_full_recursive_prover
+```
+
 ## Chips
 
 - [Poseidon](#Poseidon)

zk_prover/benches/full_solvency_flow.rs

@@ -29,7 +29,7 @@ fn build_mstree_benchmark(_c: &mut Criterion) {
 fn verification_key_gen_benchmark(_c: &mut Criterion) {
     let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);
 
-    let params: ParamsKZG<Bn256> = generate_setup_params(LEVELS);
+    let params: ParamsKZG<Bn256> = generate_setup_params(11);
 
     let empty_circuit = MerkleSumTreeCircuit::<LEVELS, MST_WIDTH, N_ASSETS>::init_empty();
 
@@ -44,7 +44,7 @@ fn verification_key_gen_benchmark(_c: &mut Criterion) {
 fn proving_key_gen_benchmark(_c: &mut Criterion) {
     let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);
 
-    let params: ParamsKZG<Bn256> = generate_setup_params(LEVELS);
+    let params: ParamsKZG<Bn256> = generate_setup_params(11);
 
     let empty_circuit = MerkleSumTreeCircuit::<LEVELS, MST_WIDTH, N_ASSETS>::init_empty();
 
@@ -60,7 +60,7 @@ fn proving_key_gen_benchmark(_c: &mut Criterion) {
 fn generate_zk_proof_benchmark(_c: &mut Criterion) {
     let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);
 
-    let params: ParamsKZG<Bn256> = generate_setup_params(LEVELS);
+    let params: ParamsKZG<Bn256> = generate_setup_params(11);
 
     let empty_circuit = MerkleSumTreeCircuit::<LEVELS, MST_WIDTH, N_ASSETS>::init_empty();
 
@@ -92,7 +92,7 @@ fn generate_zk_proof_benchmark(_c: &mut Criterion) {
 fn verify_zk_proof_benchmark(_c: &mut Criterion) {
     let mut criterion = Criterion::default().sample_size(SAMPLE_SIZE);
 
-    let params: ParamsKZG<Bn256> = generate_setup_params(LEVELS);
+    let params: ParamsKZG<Bn256> = generate_setup_params(11);
 
     let empty_circuit = MerkleSumTreeCircuit::<LEVELS, MST_WIDTH, N_ASSETS>::init_empty();
 

zk_prover/src/chips/aggregation.rs

@@ -0,0 +1,47 @@
+use halo2_proofs::{
+    circuit::{AssignedCell, Layouter},
+    halo2curves::bn256::Fr as Fp,
+    plonk::{Column, ConstraintSystem, Error, Instance},
+};
+use snark_verifier_sdk::halo2::aggregation::AggregationConfig;
+
+/// Wrapper around AggregationConfig that adds a vector of instance columns. Specifically an instance column for each input SNARK of the aggregation circuit.
+#[derive(Clone)]
+pub struct WrappedAggregationConfig<const N_SNARK: usize> {
+    pub aggregation_config: AggregationConfig,
+    pub instances: [Column<Instance>; N_SNARK],
+}
+
+impl<const N_SNARK: usize> WrappedAggregationConfig<N_SNARK> {
+    pub fn configure(
+        meta: &mut ConstraintSystem<Fp>,
+        composition_bits: Vec<usize>,
+        overflow_bits: Vec<usize>,
+    ) -> Self {
+        let instances = [(); N_SNARK].map(|_| meta.instance_column());
+
+        for instance in instances.iter() {
+            meta.enable_equality(*instance);
+        }
+
+        // Note that the aggregation config is configured after having configured the instances. Therefore, the instance column of the aggregation circuit is the last one
+        let aggregation_config =
+            AggregationConfig::configure(meta, composition_bits, overflow_bits);
+
+        Self {
+            aggregation_config,
+            instances,
+        }
+    }
+
+    // Enforce copy constraint check between input cell and instance column at row passed as input
+    pub fn expose_public(
+        &self,
+        mut layouter: impl Layouter<Fp>,
+        cell: &AssignedCell<Fp, Fp>,
+        instance: Column<Instance>,
+        row: usize,
+    ) -> Result<(), Error> {
+        layouter.constrain_instance(cell.cell(), instance, row)
+    }
+}

zk_prover/src/chips/mod.rs

@@ -1,3 +1,4 @@
+pub mod aggregation;
 pub mod merkle_sum_tree;
 pub mod overflow;
 pub mod poseidon;

zk_prover/src/circuits/aggregation.rs

@@ -0,0 +1,113 @@
+use crate::chips::aggregation::WrappedAggregationConfig;
+use ecc::integer::rns::Rns;
+use halo2_proofs::{
+    circuit::{Layouter, SimpleFloorPlanner},
+    halo2curves::bn256::{Bn256, Fq, Fr as Fp},
+    plonk::{Circuit, ConstraintSystem, Error},
+    poly::kzg::commitment::ParamsKZG,
+};
+use itertools::Itertools;
+use maingate::{MainGateInstructions, RangeInstructions};
+use snark_verifier_sdk::{
+    halo2::aggregation::AggregationCircuit, CircuitExt, Snark, BITS, LIMBS, SHPLONK,
+};
+
+/// Wrapper around Aggregation Circuit. It contains a vector of vectors `prev_instances`. Each inner vector represent the instance of an input snark.
+/// For example, if the input snarks are 2 and the instances are [0x11, 0xbb, ...] and [0x22, 0xcc, ...], then prev_instances is [[0x11, 0xbb, ...], [0x22, 0xcc, ...]]
+#[derive(Clone)]
+pub struct WrappedAggregationCircuit<const N_SNARK: usize> {
+    aggregation_circuit: AggregationCircuit<SHPLONK>,
+    prev_instances: Vec<Vec<Fp>>,
+}
+
+impl<const N_SNARK: usize> WrappedAggregationCircuit<N_SNARK> {
+    pub fn new(params: &ParamsKZG<Bn256>, snarks: impl IntoIterator<Item = Snark>) -> Self {
+        let snarks = snarks.into_iter().collect_vec();
+
+        let prev_instances: Vec<Vec<Fp>> = snarks
+            .iter()
+            .flat_map(|snark| snark.instances.iter())
+            .cloned() // need to clone it because otherwise I would be collecting references to the instances
+            .collect_vec();
+
+        let aggregation_circuit = AggregationCircuit::new(params, snarks);
+
+        Self {
+            aggregation_circuit,
+            prev_instances,
+        }
+    }
+}
+
+impl<const N_SNARK: usize> Circuit<Fp> for WrappedAggregationCircuit<N_SNARK> {
+    type Config = WrappedAggregationConfig<N_SNARK>;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn without_witnesses(&self) -> Self {
+        let aggregation_circuit = AggregationCircuit::without_witnesses(&self.aggregation_circuit);
+
+        let prev_instances: Vec<Vec<Fp>> = vec![Vec::new(); N_SNARK];
+
+        Self {
+            aggregation_circuit,
+            prev_instances,
+        }
+    }
+
+    fn configure(meta: &mut ConstraintSystem<Fp>) -> Self::Config {
+        WrappedAggregationConfig::configure(
+            meta,
+            vec![BITS / LIMBS],
+            Rns::<Fq, Fp, LIMBS, BITS>::construct().overflow_lengths(),
+        )
+    }
+
+    fn synthesize(
+        &self,
+        config: Self::Config,
+        mut layouter: impl Layouter<Fp>,
+    ) -> Result<(), Error> {
+        let main_gate = config.aggregation_config.main_gate();
+        let range_chip = config.aggregation_config.range_chip();
+        range_chip.load_table(&mut layouter)?;
+
+        let (accumulator_limbs, prev_instances) = self
+            .aggregation_circuit
+            .aggregation_region(config.clone().aggregation_config, &mut layouter)?;
+
+        for (row, limb) in accumulator_limbs.into_iter().enumerate() {
+            main_gate.expose_public(layouter.namespace(|| ""), limb, row)?;
+        }
+
+        // expose the instances from the input snarks to the public
+        for (prev_instance, instance) in prev_instances.iter().zip(config.instances.iter()) {
+            for (row, cell) in prev_instance.iter().enumerate() {
+                config.expose_public(layouter.namespace(|| ""), cell, *instance, row)?;
+            }
+        }
+
+        Ok(())
+    }
+}
+
+impl<const N_SNARK: usize> CircuitExt<Fp> for WrappedAggregationCircuit<N_SNARK> {
+    // for a case of 2 snarks input with 1 instance column each with 4 rows, it should be [4, 4, 16]. Where 16 are `num_instance` from the aggregation circuit
+    fn num_instance(&self) -> Vec<usize> {
+        let mut num_instance = self
+            .prev_instances
+            .iter()
+            .map(|instance| instance.len())
+            .collect_vec();
+
+        num_instance.push(self.aggregation_circuit.num_instance()[0]);
+
+        num_instance
+    }
+
+    // following the previous example, it should be like [[0x001, 0x111, 0xaaa, 0xbbb], [0xaaa, 0xfff, 0xeee, 0x111], [0x11, 0xbb, ...]]. Note that the last vector is the instance of the aggregation circuit
+    fn instances(&self) -> Vec<Vec<Fp>> {
+        let mut instances = self.prev_instances.clone();
+        instances.push(self.aggregation_circuit.instances()[0].clone());
+        instances
+    }
+}

zk_prover/src/circuits/merkle_sum_tree.rs

@@ -2,6 +2,7 @@ use crate::chips::merkle_sum_tree::{MerkleSumTreeChip, MerkleSumTreeConfig};
 use crate::merkle_sum_tree::{big_int_to_fp, MerkleProof, MerkleSumTree};
 use halo2_proofs::halo2curves::bn256::Fr as Fp;
 use halo2_proofs::{circuit::*, plonk::*};
+use snark_verifier_sdk::CircuitExt;
 
 #[derive(Clone)]
 pub struct MerkleSumTreeCircuit<const LEVELS: usize, const MST_WIDTH: usize, const N_ASSETS: usize>
@@ -15,6 +16,22 @@ pub struct MerkleSumTreeCircuit<const LEVELS: usize, const MST_WIDTH: usize, con
     pub root_hash: Fp,
 }
 
+impl<const LEVELS: usize, const MST_WIDTH: usize, const N_ASSETS: usize> CircuitExt<Fp>
+    for MerkleSumTreeCircuit<LEVELS, MST_WIDTH, N_ASSETS>
+{
+    fn num_instance(&self) -> Vec<usize> {
+        vec![2 * (1 + N_ASSETS)]
+    }
+
+    fn instances(&self) -> Vec<Vec<Fp>> {
+        let mut instances = vec![self.leaf_hash];
+        instances.extend(&self.leaf_balances);
+        instances.push(self.root_hash);
+        instances.extend(&self.assets_sum);
+        vec![instances]
+    }
+}
+
 impl<const LEVELS: usize, const MST_WIDTH: usize, const N_ASSETS: usize>
     MerkleSumTreeCircuit<LEVELS, MST_WIDTH, N_ASSETS>
 {

zk_prover/src/circuits/mod.rs

@@ -1,3 +1,4 @@
+pub mod aggregation;
 pub mod ecdsa;
 pub mod merkle_sum_tree;
 pub mod tests;