Sum balance overflow

[zeroqn]

Describe the bug

There is no range check in the circuit for the sum of balances, which poses a risk of overflow.

Furthermore, since N_BYTES is not exposed in the contract, users must run examples/gen_inclusion_verifier.rs to obtain a warning message about the risk of overflow.

To Reproduce
Steps to reproduce the behavior:

examples/gen_inclusion_proof.rs set N_BYTES to 32 and change one of MBlfbBGI's balance to 21888242871839275222246405745257275088548364400416034343698204186575808495617 in csv/entry_16.csv.

A valid proof is generated and pass verification.

Expected behavior
A clear and concise description of what you expected to happen.

Cannot generate valid proof

Additional context
Add any other context about the problem here.

Perhaps we could use a new lookup argument to achieve acceptable performance?

Lasso

privacy-scaling-explorations/halo2#194
DoHoonKim8/halo2-lasso#4

[enricobottazzi]

I think that this issue and #14 are basically the same thing and, in my opinion, do not reflect a bug.

We deliberately decided to design the range check inside the circuit such that the only way that it can lead to an overflow is for some combinations between N_BYTES and LEVELS (check the presentation I gave at the beginning at the cohort).

Following the principle that everything that can be verified outside of the circuit should be verified outside the circuit, the user has all the tools (https://summa.gitbook.io/summa/v/1/smart-contract/summa.sol#verifier-contract-validity) to assess if, given the compiled verifier contract, the combination poses a risk of balance overflow. If the combination is fine, we believe there's no any way that a prover can generate a valid proof. Only in that case, I would consider it as an high vulnerability.