# Incremental Inclusion Verification

## The problem

As of now the protocol works like this:


> The commitment phase can be updated between different rounds

The element worth noting is that for each round of Proof of Solvency, the CEX needs to generate a different π of Inclusion for Alice. This proof, if verified by Alice, would tell that she has been accounted for correctly in the liabilities tree **at that specific round**. Considering the case in which a CEX performs a proof of solvency on a daily basis (we can push it up to every few minutes given the performance of our tech) the effort required by Alice to verify if the exchange is solvent is significant: she doesn't only needs to locally perform this type of verification, but this has to be performed at every round! Potentially every few minutes.

Each round is completely independent from the other ones and so is the π of Inclusion.

The protocol modification proposed here solved this problem using IVC (Incrementally Verifiable Computation) proof. In short, at round $n$, Alice will receive a π of Inclusion that that verifies that she has been accounted for correctly in the liabilities tree at that specific round **and** that she has been accounted for correctly in the liabilities tree **in every round up to latest one**.


In this updated implementation, Alice might be too lazy to check the π of Inclusion at every round. But that's ok, since she only needs to very it at a certain round to check her correct **incremental inclusion** within the Liabilities Tree.

Beyond the user experience benefit, this implementation brings a massive improvement in the security of the whole protocol.

In the existing implementation, the failure probability, defined as the likelihood that malicious CEX that manipulates their liabilities is able to go undetected is a function of the number of users that verifies their π of Inclusion **only within that round**.

In this updated implementation, the failure probability is a function of the number of users that verifies their π of Inclusion **at any (even future) point in time**.

## Core Idea

The desired properties of such proof are:

- The size of such proof should be such that the verification doesn't grow linearly with the number of rounds.
- Should be ZK, so namely hide data related to the rest of the merkle sum tree.
- Should be able to encapsulate the whole **history** of user data within the liabilities merkle sum tree generated by the CEX and committed to on-chain at every round (here's where the IVC component comes into place).
- Proving time should not add overhead to the CEX.

The core concept that to design this is [IVC](https://iacr.org/archive/tcc2008/49480001/49480001.pdf).

There are different tools that would allow to do that.

One could use Proof Aggregation ([Snark Verifier](https://github.com/privacy-scaling-explorations/snark-verifier)). With a naive approach, a CEX, at round $n$, could aggregate all the n-s π of Inclusion for a specific user up to that point and pass to the user only the aggregated proof. This would create a massive overhead on the CEX prover as the size of the aggregated proof (even if significantly smaller than the sum of the input proofs) would increase linearly at every round. The aggregated proof at round 2 would be way smaller than the aggregated proof at round 50.

A more efficient implemenation would be aggregating 2 proofs at each round:
- π of inclusion for the current round i
- aggregated π generated at round i - 1

In this scenario, the size of the proof to be generated by CEX would be the same at each round. Still, the proof aggregation in Halo2 adds huge overhead to the CEX.

In particular, in the current scenario generating a π of Solvency for a user takes around 400s ms. In this upgraded scenario, generating an aggregated π for each would take minutes. This is not feasible considering that this has to be reproduced at every round for the whole CEX's userbase (or, at least, on the fly to the users that actively query it).

To achieve faster prover time (and conserve the first 3 properties) we leverage Nova Folding Scheme.

Here's a detailed breakdown of what Nova is => https://hackmd.io/kPecllhZQi6AMy7EKMTPHg.

## How To

### `MerkleSumTree`

First of all a modification to the design of the core data structure of Summa, namely the Merkle Sum Tree needs to be performed.

Right now the commitment to the state of the users' liabiltiies is represented by the root of the Merkle Sum Tree. In order to create a chain of commitments between two subsequent rounds we need to link together the state of the trees. We do that by encapsulating the state of the previous round to the commitment of the current round.


The only difference is that we perform a further hashing between the `root_hash` and the `liabiltiies_state_prev` to get to the `liabilities_state_cur`. The CEX will commit this `liabilities_state_cur` to the Summa contract on-chain.

`liabilities_state_cur` is a commitment to the current state of the liabilities tree that also includes a reference to the previous committed state.

The act of publishing a new `liabilities_state_cur` to the Summa Smart Contract is very similar in terms of design to publishing a new block by propagating its block header.

### `Solvency` Circuit

The `Solvency` Circuit works the same way as today. The only difference is that the Smart Contract will also perform a further hashing on `mst_root_hash` together with the `liabilities_state_prev` to get `liabilities_state_cur`.

### `MstInclusion` Circuit

The `MstInclusion` circuit needs to change accordingly to express this concept of link between a round and the previous state up to that round. In particular, we introduce a concept of `user_state`.


The key takeaway here is that at `t=n` starting from the her historical balance log, Alice should be able to reconstruct the the latest `user_state_cur` by:
- reconstructing the `leaf_hash` for each round where leaf_hash at round `i` is equal `leaf_hash_i = H(username, balance_i)`
- recursively hashing the leaf hashes n times starting from the one at round 0 to the one at round i

The statement that the CEX, the prover, is proving here is "a user with latest state `user_state_cur` has been correctly included in the liabilities tree with state `liabilities_state_cur`.


### IVC with Nova

This new logic can be compacted into a Nova IVC Prover.


- At step 0 `liabilities_state_prev` and `user_state_prev` are 0
- Each step corresponds to execting a `MstInclusionCircuit`
- At every step the Nova prover generates a π for user verification.
- This proof would tell the user that all the steps up to that one very performed correctly
- The user has to check that `user_state_cur` matches the recursive hashing of its history logs.
- The user has to check that the `liabilities_state_cur` matches the latests one committed on-chain.

### Practical Issues

Such solution add some extra work on the user side:

- In order to verify the proof, the user would need to perform the recursive hashing for each `user_state` up to that round. An idea here would be to have a third-party server (which is independent from the CEX) that stores the log of users balances at each round and keep track of the latest user state on behalf of the user.

### Application

An example of this whole flow has been added to `summa-solvency` => https://github.com/summa-dev/summa-solvency/pull/153