### Halo2 On-chain Verification Cost Model 2 Dimensions: - `proof generation time` - `gas cost for verification, which relates to proof size` Using the type of operations computed inside the circuit, the goal is to optimize to the least amount of columns, in order to generate a proof that is feasible to verify on-chain. An important factor to take into account is `n` Tho n is not exactly number of columns but closed to, to be more precise it's: ``` n = #columns + #internal_columns + #quotient_commitments + #pc_opening_commitments + 2*#old_accumulators ``` where - #columns are allocated by user e.g. meta.xxx_column() or meta.selector() - #internal_columns are used by lookup argument and permutation argument - #pc_opening_commitment depends on which kind of polynomial commitment scheme we are using ### Direct on-chain verification The gas cost to verify a proof on chain is equal to `181k + 6.35k*n`. Goal is to try to reduce **n** as much as possible. # Proof Of Solvency Efficiency Improvement This type of prover performance improvement becomes necessary when adding multi-asset support #18. In particular the idea is to modify the core structure of the merkle sum tree to support multiple assets ![](https://hackmd.io/_uploads/B1N-WGKBn.png) If we keep the design logic as [it is right now](https://github.com/summa-dev/summa-solvency/tree/mst-optimization#merkle-sum-tree), each new currency supported will result in 2 more advice columns in our circuit design. Adding more columns will significantly impact the proof size (other than the proof generation time) and, therefore, the cost of verifying it on-chain. Even when using an Aggregation Circuit to output a smaller proof, the number of columns of the input circuit will have an impact on on that. Specifically more columns -> larger aggregation circuit -> longer aggregation time. The goal of the efficiency improvment efforts will be thefore aimed to reduce the number of advice columns used by the circuit. Here are some ideas in order to achieve that: ### 1. Reduce the number of advice columns needed for hashing This can be performed by using recursive hashing as mentioned here => https://github.com/summa-dev/summa-solvency/issues/37 ### 2. Reuse advice columns across different chips Further optimization involves reusing the same advice columns across different chips. We should start by realizing what's the maximum amount of advise column that we need at the same time. Basically this is determined by most number of advice columns needed by an individual region. This can be checked from the printing of the circuit. Once you see that, you can realize that the same region can be stacked one upon the other, sharing the same advice columns. There's no need to put them side by side. We can call this time of optimization **advice columns optimization** As of now, we are not saving of advice columns across different chips. For example, the poseidon hash chip is creating new advice columns, when it could reuse the same advice columns that are initiated in the `MerkleSumTreeChips`. In order to reduce the number of advice columns used in the Merkle Sum Tree Circuit we are gonna share advice columns between the Poseidon Chip and the Merkle Sum Tree Chip. - The Merkle Sum Tree Chip requires 5 advice columns - The Poseidon Chip (with WIDTH 5) requires 5 `hash_inputs` plus 1 `partial_sbox` The current implementation works with 11 advice columns. Ideally we can get to 6 advice columns. => [Circuit Print before optimization](https://github.com/summa-dev/summa-solvency/blob/poseidon-efficiency-test/prints/merkle-sum-tree-layout.png) => [Circuit Print after optimization](https://github.com/summa-dev/summa-solvency/blob/poseidon-efficiency-test/prints/merkle-sum-tree-layout-2.png) Of course it comes at the cost of increasing the number of rows needed and, therefore, the proving time ### 3. Tweak Overflow chip using different N_BITS and NUM_COLS to find the best optimization As of now the Overflow chip works with `31` accumulator columns. This number can be reduced at the cost of increasing the number of rows. ### 4. Replace multi-assets support with a structure based on multiple merkle trees We move to a design that involves creating a mst for each currency and, eventually, generating a merkle tree (not sum tree) commitment to the state of each tree. ![](https://hackmd.io/_uploads/r1ti9LjH3.png) ### 5. Add batching to MerkleSumTreeInclusion Circuit Basically it means proving a lot of membership at once in the same circuit. ### 6. Reduce row requirement for the OverFlow Chip As mentioned here => https://github.com/summa-dev/summa-solvency/issues/56 # Optimization efforts ### 1. Starting Point - [commit `19187c9`](https://github.com/summa-dev/summa-solvency/commit/19187c9ea9b401b677dbb4fcbe8fa1151b57ed3b) - [print](https://github.com/summa-dev/summa-solvency/blob/19187c9ea9b401b677dbb4fcbe8fa1151b57ed3b/zk_prover/prints/merkle-sum-tree-layout.png) #### Configuration ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, pub lt_selector: Selector, // 4 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // WIDTH + 1 advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // 1 + ACC_COLS advice columns // 1 fixed column // 1 selector pub lt_config: LtConfig<Fp, 8>, // 9 (8+1) advice columns // 1 Fixed } ``` ``` const MST_WIDTH: usize =9 const ACC_COLS: usize = 31; const MAX_BITS: u8 = 8; const WIDTH: usize = 7; const RATE: usize = 6; ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9+7+1+31+9 (57) | 8 | 14+1+1 (16) | 1 | #### Outcome of `test_standard_on_chain_verifier` ``` thread 'circuits::tests::test::test_standard_on_chain_verifier' panicked at 'called `Result::unwrap()` on an `Err` value: Transaction(CreateInitcodeSizeLimit)', /Users/enricobottazzi/.cargo/git/checkouts/snark-verifier-972b60abf3a1213b/5ea3619/snark-verifier/src/loader/evm/util/executor.rs:21:40 ``` ### 2. Separating logic of MstInclusion Circuit from ProofOfSolvency Circuit As described here => https://github.com/summa-dev/summa-solvency/issues/53 Separating it into two circuit would make the `MstInclusionCircuit` more lean as: a) It would no longer need to perform the LessThan check b) It would no longer need to store the 8 advice columns that are required in the configuration of the `LTChip` - [commit `bffa1f0`](https://github.com/summa-dev/summa-solvency/commit/bffa1f04665b038a99f6d9a2fdadbb327607f85a) - [print](https://github.com/summa-dev/summa-solvency/blob/bffa1f04665b038a99f6d9a2fdadbb327607f85a/zk_prover/prints/merkle-sum-tree-layout.png) #### Configuration ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, pub lt_selector: Selector, // 4 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // WIDTH + 1 advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // 1 + ACC_COLS advice columns // 1 fixed column // 1 selector } ``` ``` const MST_WIDTH: usize =9 const ACC_COLS: usize = 31; const MAX_BITS: u8 = 8; const WIDTH: usize = 7; const RATE: usize = 6; ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9+7+1+31 (48) | 8 | 14+1 (15) | 1 | #### Outcome of `test_standard_on_chain_verifier` ``` thread 'circuits::tests::test::test_standard_on_chain_verifier' panicked at 'called `Result::unwrap()` on an `Err` value: Transaction(CreateInitcodeSizeLimit)', /Users/enricobottazzi/.cargo/git/checkouts/snark-verifier-972b60abf3a1213b/5ea3619/snark-verifier/src/loader/evm/util/executor.rs:21:40 ``` ### 3. Reuse advice columns between Poseidon hasher and `advice` of Merkle Sum Tree ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, pub lt_selector: Selector, // 4 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // WIDTH + 1 advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // 1 + ACC_COLS advice columns // 1 fixed column // 1 selector } ``` Considering MST_WIDTH here of 9, there are is an array `advice` that contains 9 advice columns. While the `PoseidonConfig` requires `WIDTH + 1` advice columns. Considering the case of 2 assets, `MST_WIDTH = 3 * (1 + N_ASSETS) = 9`. WIDTH=7, namely the length of 1 + 6, where 6 is the length of the input array. It is still not clear if width can be constant or varies according to N_ASSETS. For now let's just consider WIDTH=7. The PoseidonConfig requires `WIDTH + 1 = 8` advice columns. The Poseidon Config can easily reuse the 8 of the 9 advice column contained in the `advice` array. - [commit `8dae130`](https://github.com/summa-dev/summa-solvency/commit/8dae130ea9ee309dd86b247845994b3d03b81f15) - [print](https://github.com/summa-dev/summa-solvency/blob/8dae130ea9ee309dd86b247845994b3d03b81f15/zk_prover/prints/merkle-sum-tree-layout.png). The circuit is getting thinner! #### Configuration ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, pub lt_selector: Selector, // 4 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // no additional advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // 1 + ACC_COLS advice columns // 1 fixed column // 1 selector } ``` ``` const MST_WIDTH: usize = 9 const ACC_COLS: usize = 31; const MAX_BITS: u8 = 8; const WIDTH: usize = 7; const RATE: usize = 6; ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9+1+31 (41) | 8 | 14+1 (15) | 1 | **we saved 7 advice columns!** #### Outcome of `test_standard_on_chain_verifier` ``` thread 'circuits::tests::test::test_standard_on_chain_verifier' panicked at 'called `Result::unwrap()` on an `Err` value: Transaction(CreateInitcodeSizeLimit)', /Users/enricobottazzi/.cargo/git/checkouts/snark-verifier-972b60abf3a1213b/5ea3619/snark-verifier/src/loader/evm/util/executor.rs:21:40 ``` ### 4. Reduce the amount of columns needed for the OverFlow Chip and share columns from `advice` Our `MST_WIDTH` is equal to 9. Let's reuse these columns for the `Overflow` Chip. In order to so we have to modify `ACC_COLS` to 8. For now let's keep `MAX_BITS = 8`. This means that we are performing a check that the value is in 8*8 = 64 bits range. This is of course not enough, but we'll think about this problem later. - [commit `8e8b9fd`](https://github.com/summa-dev/summa-solvency/commit/8dae130ea9ee309dd86b247845994b3d03b81f15) - [print](https://github.com/summa-dev/summa-solvency/blob/8e8b9fd253546b7abede41f821ea853e8c949e10/zk_prover/prints/merkle-sum-tree-layout.png). #### Configuration ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, pub lt_selector: Selector, // 4 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // no additional advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // no additional advice columns // 1 fixed column // 1 selector } ``` ``` const MST_WIDTH: usize = 9 const ACC_COLS: usize = 8; const MAX_BITS: u8 = 8; const WIDTH: usize = 7; const RATE: usize = 6; ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9 | 8 | 14+1 (15) | 1 | **we saved 32 advice columns!** #### Outcome of `test_standard_on_chain_verifier` ``` thread 'circuits::tests::test::test_standard_on_chain_verifier' panicked at 'called `Result::unwrap()` on an `Err` value: "Contract deployment transaction halts unexpectedly with gas_used 18446744073709551615 and reason CreateContractSizeLimit"', /Users/enricobottazzi/.cargo/git/checkouts/snark-verifier-972b60abf3a1213b/5ea3619/snark-verifier-sdk/src/evm.rs:182:63 ``` The error message changed a bit... I think we are getting closer ### 5. Reduce the number of selectors The latest configuration had 8 selectors. Removing a selector is very delicate. A selector should be shared only when all the constraints toggled by two selectors should always apply at the same time. Not really easy task... But we can see that there's an unused `LTSelector` that we can safely remove - [commit `2ece580`](https://github.com/summa-dev/summa-solvency/commit/2ece580b25c4f306378076becaf81edc52da0486) - [print](https://github.com/summa-dev/summa-solvency/blob/2ece580b25c4f306378076becaf81edc52da0486/zk_prover/prints/merkle-sum-tree-layout.png). #### Configuration ```rust pub struct MerkleSumTreeConfig<const MST_WIDTH: usize> { pub advice: [Column<Advice>; MST_WIDTH], // #MST_WIDTH advice columns pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, // 3 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // no additional advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // no additional advice columns // 1 fixed column // 1 selector } ``` ``` const MST_WIDTH: usize = 9 const ACC_COLS: usize = 8; const MAX_BITS: u8 = 8; const WIDTH: usize = 7; const RATE: usize = 6; ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9 | 7 | 14+1 (15) | 1 | **we only saved 1 selector!** #### Outcome of `test_standard_on_chain_verifier` Same as before... ### 6. Fix poseidon WIDTH to 5 As mentioned by Alex, the Poseidon Paper advice to use rate = 4 and width = 5. We can keep this parameters fixed regardless the length of the input array. Remember that the Poseidon Config requires a further `partial_sbox` advice column In this scenario, the number of advice columns used for the Poseidon Config will shrink to 6 (WIDTH + 1) and the number of the fixed columns will shrink to 10. Unfortunately, a current bug in the padding of the poseidon hasher, doesn't allow us to do so => https://discord.com/channels/995022112811135148/1005560452446683186/1120647178994581504 In particular, if we are using an input of 6 elements to the hasher, it won't work because the input `L` should be a multiple of Rate, and 6 is not a multiple of 4. Once the bug in halo2 is fixed, we will be able to use the poseidon parameters of rate = 4 and width = 5 Even if not implemented yet, we'll consider a virtual design of our MerkleSumTreeConfig as follows: ```rust pub struct MerkleSumTreeConfig { pub advice: [Column<Advice>; 6], // #5 + 1 pub bool_selector: Selector, pub swap_selector: Selector, pub sum_selector: Selector, // 3 selectors pub instance: Column<Instance>, // 1 instance pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // no additional advice columns // 2*WIDTH Fixed columns // 3 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // no additional advice columns // 1 fixed column // 1 selector } ``` ``` const ACC_COLS: usize = 5; const MAX_BITS: u8 = 8; const WIDTH: usize = 5; const RATE: usize = 4; ``` Note that the number of acc_cols also has been reduced in order to comply with the maximum amount of advice columns taken into account in the circuit. Namelyy 5! | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 9 | 7 | 10+1 (11) | 1 | ### 7. Implement a more verticial merkle tree layer circuit design Consider the limits imposed by the previous proposal, we have to virtually consider a maximum number of `5` advice columns. Let's consider the situation in which we have `N_ASSETS=2`. The circuit as of designed now would take `MST_WIDTH` advice columns, where `pub const MST_WIDTH: usize = 3 * (1 + N_ASSETS)` so, in this case, it would be 9. The current layout would look like this: | a | b | c | d | e | f | g | h | i | | --- | --- | --- | --- | --- | --- | ---- | ---- | ---- | | `bal_0_left` | `bal_1_left` | `bal_0_right` | `bal_1_right` | - | - | `hash_left` | `hash_right` | `-` | At the row = 0, `bool selector` would be applied to check that `swap_bit` is either 0 or 1. At the row = 0, `swap selector` would be applied to check that according to the `swap_bit` selector, the values are swapped correctly in the next row. For example, considering the case in which the `swap_bit` is 0, this would mean that no swap needs to be performed as follow in row=1 | a | b | c | d | e | f | g | h | i | | --- | --- | --- | --- | --- | --- | ---- | ---- | ---- | | `bal_0_left` | `bal_1_left` | `bal_0_right` | `bal_1_right` | `sum_0` | `sum_1` | `hash_left` | `hash_right` | `swap_bit` | At the row = 1 `sum_selector` would be applied to check that `sum_i = bal_i_left + bal_i_right`. Furthermore, after row=1 is computed, other 2 operations are performed on the assigned cells of row 1: - poseidon_chip is used to hash `H(hash_left, bal_0_left, bal_1_left, hash_right bal_0_right, bal_1_right, hash_leaf)` - overflow check is performed on `bal_0_left, bal_1_left, bal_0_right, bal_1_right`. This structure grows in size linearly according to `N_ASSETS`, in particular the relation between the number of assets and the number of advice columns is defined by `MST_WIDTH`. 3 assets would mean 12 columns. This won't fit in the limit of the `5` advice columns. Therefore we can try to redisign it as follow, considering `N_ASSETS = 2` and again considering `swap_bit = 0` | a | b | c | | ------------ | ------------- | ---------- | | `hash_left` | `hash_right` | `swap_bit` | | `hash_left` | `hash_right` | | | `bal_0_left` | `bal_0_right` | `swap_bit` | | `bal_0_left` | `bal_0_right` | `sum_0` | | `bal_1_left` | `bal_1_right` | `swap_bit` | | `bal_1_left` | `bal_1_right` | `sum_1` | At row 0, 2 and 4 `bool_constraint` and `swap_selectors` need to be toogled. At row 1 and 3 `sum_selector` needs to be toogled After row 5 is computed, the same `poseidon` and `overflow` check can be performed following the same structure as before. An additional check that need to be performed here is that the `swap_bit` remains consistent for an hasher round! Note that this structure grows vertically according to `N_ASSETS`, since every new asset will contribute with a two more rows, while it doesn't add any advice column! Which is exactly what we are looking for. - [commit `1530db2`](https://github.com/summa-dev/summa-solvency/commit/1530db28d3fc2e53fed2cdbab601fa037aeb316a) - [print](https://github.com/summa-dev/summa-solvency/blob/d835cb84783b4600c60b80c530351f774213660b/zk_prover/prints/merkle-sum-tree-layout.png). #### Configuration Note that in this experiment are still using the version with the Poseidon Hasher with `WIDTH=7` ```rust pub struct MstInclusionConfig<const L: usize, const N_ASSETS: usize> { pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // WIDTH + 1 Advice columns // 2*WIDTH Fixed columns // 3 selectors pub merkle_sum_tree_config: MerkleSumTreeConfig, // no additional advice columns // 2 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // no additional advice columns // 1 selector // 1 fixed pub instance: Column<Instance>, } ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 8 | 6 | 14+1 (15) | 1 | We also reduced a further selector by merging together the `bool_selector` and the `swap_selector`. Therefore we saved a further selector, and an advice column! #### Outcome of `test_standard_on_chain_verifier` Same as before... The cost of deploying such verifier is still too big... Actually, I tried to test it with only 1 asset, using a poseidon configuration with WIDTH=5. Here's the fork where I made the experiment, but unfortunately, got the same negative result.. => https://github.com/summa-dev/summa-solvency/tree/test-1-asset ### 8. Further column reductions Right now the numbers of advice columns and fixed columns that we are using is mainly due to the nature of the Poseidon Chip. The next step that I tried is to reduce the parameters of the `PoseidonConfig` to RATE = 1 and WIDTH = 2. In this scenario the whole config would look like this ```rust pub struct MstInclusionConfig<const L: usize, const N_ASSETS: usize> { pub poseidon_config: PoseidonConfig<WIDTH, RATE, L>, // 2 + 1 Advice columns // 2*2 Fixed columns // 3 selectors pub merkle_sum_tree_config: MerkleSumTreeConfig, // no additional advice columns // 2 selectors pub overflow_check_config: OverflowCheckConfig<MAX_BITS, ACC_COLS>, // no additional advice columns // 1 selector // 1 fixed pub instance: Column<Instance>, } ``` | Advice Cols | Selectors | Fixed | Instance | | ---------------- | --------- | ----- | -------- | | 3 | 6 | 4+1 (5) | 1 | This worked! ``` [/Users/enricobottazzi/.cargo/git/checkouts/snark-verifier-972b60abf3a1213b/5ea3619/snark-verifier-sdk/src/evm.rs:183] gas_cost = 474019 ``` It would be important to assess the security of this decision of reducing the width. what's important is that we now have a clearer heuristic of the target that we need to reach in order to achieve on-chain verification without recursion. ### NEXT STEPS - [ ] Jin to add vertical design of Overflow config - [ ] Assess security of Poseidon Chip with WIDTH 1 - [ ] Benchmark the performance with the new circuit with the one before the efficiency improvements - [ ] Add batching for multiple proof of inclusions and see how far we can get!