Add circuit audit comments

[alxkzmn]

There are two circuit audit comments starting with // Audit:

There are also minor typo fixes as well as some changes suggested by clippy.

[sifnoc]

Would you be able to split two lines?

[sifnoc]

I understand the issue you've pointed out. A malicious prover could potentially exploit the switch in values at this point:

summa-solvency/zk_prover/src/chips/merkle_sum_tree.rs

Lines 223 to 235 in 7489c53

	// Extract the value from the cell
	let mut l1_val = l1.value().copied();
	let mut r1_val = r1.value().copied();
	// perform the swap according to the swap bit
	// if swap_bit is 0 return (l1, r1) else return (r1, l1)
	swap_bit.value().copied().map(|x| {
	(l1_val, r1_val) = if x == Fp::zero() {
	(l1_val, r1_val)
	} else {
	(r1_val, l1_val)
	};
	});

However, considering the example provided, it seems that the constraint would not be satisfied.

$$ 1 * 2 * ( 3 - 2 ) - ( 1 - 3) - ( 2 - 4) = 2 \neq 0 $$

Please correct me if I'm missing something or if I'm wrong.

[alxkzmn]

The example is for the case when the swap bit is zero: swap_bit * 2 * (element_r_cur - element_l_cur) - (element_l_next - element_l_cur) - (element_r_cur - element_r_next) = - (element_l_next - element_l_cur) - (element_r_cur - element_r_next) = element_l_cur - element_l_next + element_r_next - element_r_cur

[alxkzmn]

For example, 3 - 4 + 2 - 1 = 0.

[sifnoc]

I see. For better understanding in the example, perhaps assigning 5 to element_l_next instead of 1 would make it clearer.

[enricobottazzi]

Thanks for the comment. I think this is a security issue. For example setting:

• element_l_cur = 3
• element_r_cur = 1
• element_l_next = 4
• element_r_next = 2

In the case in which swap_bit = 0 would satisfy this constraint

summa-solvency/zk_prover/src/chips/merkle_sum_tree.rs

Lines 62 to 67 in 7489c53

	let swap_constraint = s
	* ((swap_bit
	* Expression::Constant(Fp::from(2))
	* (element_r_cur.clone() - element_l_cur.clone())
	- (element_l_next - element_l_cur))
	- (element_r_cur - element_r_next));

as (0 * 2 * (1 - 3)) - (4 - 3) - ( 1 - 2) = 0

Which should not happen.

I had a look into how semaphore enforces the swapping constraint => https://github.com/semaphore-protocol/semaphore/blob/main/packages/circuits/tree.circom#L19-L34

In particular, they wire the two possible combinations (c[0] = [hash, sibling] and c[1] = sibling, hash) together with the path_index into the MultiMux1(2) template, which enforces the following constraints:

out[0] <== (c[0][1] - c[0][0])*s + c[0][0]
out[1] <== (c[1][1] - c[1][0])*s + c[1][0]

Applying this to summa, the two possible combinations are (element_l_cur, element_r_cur and element_r_cur, element_l_cur). Therefore we can set the following constraints:

element_l_next = (element_r_cur - element_l_cur)*s + element_l_cur
element_r_next = (element_l_cur - element_r_cur)*s + element_r_cur

Let's consider the case

• element_l_cur = 3
• element_r_cur = 4
• element_l_next = 4
• element_r_next = 3
• swap_bit = 1

4 = (4 - 3) * 1 + 3
3 = (3 - 4) * 1 + 4

Now let's consider the malicious case

• element_l_cur = 3
• element_r_cur = 1
• element_l_next = 4
• element_r_next = 2
• swap_bit = 0

4 != (1- 3) * 0 + 3
3 != (3 - 1) * 0 + 1

Would it be enough to fix the issue? What do you guys think?

[alxkzmn]

Yes, I think this is the solution.

[sifnoc]

Agreed

[enricobottazzi]

I replied to the two audit issues. Let's keep the PR open until we reach an agreement especially for the swapping constraint issue. When we are good, I'm gonna apply the solution for the two issues (together with the clippy fixes) in a separated PR

[enricobottazzi]

Yes, I agree that the lookup table should be build at a higher level and then passed downwards to the range_check chip.