Range check tests are unreliable regarding the number of overflows.

[qpzm]

participants: qpzm, pia

Description

This test data has two entries which exceed 2^64 -1.

1. user0 balance0
2. user1 balance1

https://github.com/summa-dev/summa-solvency/blob/fec83a747ead213261aecfaf4a01b43fff9731ee/csv/entry_16_overflow.csv

The test result, however, shows 4 balances break the range check. For example, user2 balance0 is zero, but the test error contains "Perform range check on balance 0 of user 2".
https://github.com/summa-dev/summa-solvency/blob/fec83a747ead213261aecfaf4a01b43fff9731ee/prover/src/circuits/tests.rs#L453-L484

Cause

The range check chip has 3 constraints.
https://github.com/summa-dev/summa-solvency/blob/v2/fec83a747ead213261aecfaf4a01b43fff9731ee/src/chips/range/range_check.rs#L63-L72

The third one constrains that zs[3] must be equal to the public instance column.
https://github.com/summa-dev/summa-solvency/blob/v2/fec83a747ead213261aecfaf4a01b43fff9731ee/src/circuits/univariate_grand_sum.rs#L165

In tests, it is 0.
https://github.com/summa-dev/summa-solvency/blob/fec83a747ead213261aecfaf4a01b43fff9731ee/prover/src/circuits/tests.rs#L451

In Summa.sol, it is also 0.
https://github.com/summa-dev/summa-solvency/blob/fec83a747ead213261aecfaf4a01b43fff9731ee/contracts/src/Summa.sol#L242

Therefore, all balances are constrained that zs[3] == 0 through this chained constraints.

public instance == zs[3] in user0, balance
user0 balance0 zs[3] == user0 balance1 zs[3]
user0 balance1 zs[3] == user1 balance0 zs[3]
...
user15 balance0 zs[3] == user15 balance1 zs[3]

If a balance in the middle is not equal to 0, it breaks the range check of its subsequent balance. For example, in the above test case, it breaks two equations that user1 balance1 zs[3] is 1.

user1 balance0 zs[3] != user1 balance1 zs[3] // 0 != 1
user1 balance1 zs[3] != user2 balance0 zs[3] // 1 != 0

Case1

Only one balance of user is out of range, but two error occurs. This is the case I mentioned before.

username,balance_ETH_ETH,balance_USDT_ETH
dxGaEAii,0,0
MBlfbBGI,0,18446744073709551616
lAhWlEWZ,0,0
...

https://github.com/rkdud007/summa-solvency/blob/permute-overflow-poc/prover/src/circuits/tests.rs#L438

These are two constraints that break.

user1 balance0 zs[3] != user1 balance1 zs[3] // 0 != 1
user1 balance1 zs[3] != user2 balance0 zs[3] // 1 != 0

https://github.com/rkdud007/summa-solvency/blob/permute-overflow-poc/prover/src/circuits/tests.rs#L454-L473

Case2

In this test, there are two overflows: balance0 and balance1 of user1.

username,balance_ETH_ETH,balance_USDT_ETH
dxGaEAii,0,0
MBlfbBGI,18446744073709551616,18446744073709551616
lAhWlEWZ,0,0
...

The test gives two errors: balance 0 of user 1, balance 0 of user 2 because these two constraints that break.

user1 balance0 zs[3] != user1 balance1 zs[3] // 0 != 1
user1 balance1 zs[3] != user2 balance0 zs[3] // 1 != 0

https://github.com/rkdud007/summa-solvency/blob/permute-overflow-poc/prover/src/circuits/tests.rs#L477

Case3

In this test, there are 4 overflows.

username,balance_ETH_ETH,balance_USDT_ETH
dxGaEAii,0,0
MBlfbBGI,0,18446744073709551616
lAhWlEWZ,18446744073709551616,18446744073709551616
nuZweYtO,18446744073709551616,0
gbdSwiuY,0,0

https://github.com/rkdud007/summa-solvency/blob/permute-overflow-poc/csv/entry_16_overflow_case_3.csv

However, only two overflow error comes.

• balance 0 of user 1
• balance 1 of user 3

user1 balance0 zs[3] != user1 balance1 zs[3] // 0 != 1
user1 balance1 zs[3] == user2 balance0 zs[3] // 1 == 1
user2 balance0 zs[3] == user2 balance1 zs[3] // 1 == 1
user2 balance1 zs[3] == user3 balance0 zs[3] // 1 == 1
user3 balance0 zs[3] == user3 balance1 zs[3] // 1 != 0

https://github.com/rkdud007/summa-solvency/blob/permute-overflow-poc/prover/src/circuits/tests.rs#L517

Expected behavior

A prover should not expect the test errors to include the whole overflow list. Certainly the real proof verification just shows pass or fail unlike MockProver in tests. However, the test gives so confusing a result that we clarify.

[rkdud007]

How did we print out values in logging?

1. https://github.com/summa-dev/halo2 clone
2. https://github.com/summa-dev/halo2-solidity-verifier clone
3. local halo2-solidity-verifier Cargo.toml dependency modify

[dependencies]
halo2_proofs = { path = "../halo2-fork/halo2_proofs" }

local halo2_proofs path switch
4. local summa-solvency Cargo.toml dependency modify

halo2_proofs = { path = "../../halo2-fork/halo2_proofs" }

local halo2_proofs path switch (note: backend / prover crate both require modify )

5. cargo clean / cargo update / cargo check
6. Now was able to modify & log out the exact cell when returning permutation error on over flow case :summa-dev/halo2@main...rkdud007:halo2:permute-overflow-poc

😇 permuted cell come from: column9, row0
original_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000001), permuted_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000000), column: Column { index: 6, column_type: Advice }, row: 1
😇 permuted cell come from: column9, row2
original_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000000), permuted_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000001), column: Column { index: 6, column_type: Advice }, row: 3
😇 permuted cell come from: column5, row1
original_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000000), permuted_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000001), column: Column { index: 10, column_type: Advice }, row: 1
😇 permuted cell come from: column5, row2
original_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000001), permuted_cell: Assigned(0x0000000000000000000000000000000000000000000000000000000000000000), column: Column { index: 10, column_type: Advice }, row: 2

All relevant revision pushed inpermute-everflow-poc branch among 3 repos ( default branch )

• halo2 : https://github.com/rkdud007/halo2
• solidity-verifier : https://github.com/rkdud007/halo2-solidity-verifier
• summa-solvency : https://github.com/rkdud007/summa-solvency