Optimize constraints for r1cs

[katat]

The whole idea is to have CellVar to accumulate the binary operations until it is necessary to enforce a constraint.

In order to do so, here are the todos:

• [x] refactor the CellVar to be an associated type for backend trait
• [x] Use CellVar to hold the internal var and linear combination
• [ ] Replace the backend constraint interfaces with CellVar

[katat]

Here is a draft to have a quick review to see if this is right direction.

R1csCellVar

https://github.com/zksecurity/noname/blob/289b13c3ed2b23552d5e09560d092594e3bfc8d9/src/backends/r1cs/mod.rs#L35-L38 The current implementation allows the CellVar to be an enum as either a WitnessVar or a LinearCombination

Recursive linear combination

https://github.com/zksecurity/noname/blob/289b13c3ed2b23552d5e09560d092594e3bfc8d9/src/backends/r1cs/mod.rs#L144-L150

The variables inside a LinearCombination is of R1csCellVar type. This means a linear combination can either recursively contain another linear combinations or witness vars:

ExpandedLinearCombination

https://github.com/zksecurity/noname/blob/289b13c3ed2b23552d5e09560d092594e3bfc8d9/src/backends/r1cs/mod.rs#L217-L251

When adding the linear combinations as a constraint, they will be converted to ExpandedLinearCombination, which is a expanded version of the symbolic linear combination. I think the benefit of this approach is to simply the logic during accumulating the linear combinations, and handle them all in one place (within the expand function).

For example, the following logic doesn't have to deal with specific cell var type, as they are wrapped as linear combinations which can be expanded at the end. https://github.com/zksecurity/noname/blob/4f6239b8c1146b7de49bae02e67f5fee8c0fc7e3/src/backends/r1cs/mod.rs#L75-L108

Linear combination calculation

This optimized R1cs constraint version uses the CellVar::LinearCombination for calculating the value for linear combination, instead of relying on the Value::LinearCombination, which is assumed to be for a corresponding witness var.

https://github.com/zksecurity/noname/blob/4f6239b8c1146b7de49bae02e67f5fee8c0fc7e3/src/backends/r1cs/mod.rs#L646-L664

Debug info

After the constraint is optimized, it might be helpful to keep the trace of how it comes up with the constraint and reduce the repeated info.

For example:

Refine the following(this is what it current shows):

v_4 == (v_3) * (-1 * v_1 + v_2)
v_6 == (v_5) * (-1 * v_1 + v_2)

To:

lc = -1 * v_1 + v_2
v_4 == (v_3) * (lc_1)
v_6 == (v_5) * (lc_1)

So while it can still trace where the lc is from, it avoids repeated string behind lc.

[katat]

The LinearCombination is reverted to non-recursive version.

The debug spans in the backend arithmetic methods are left unused until we decide if it is necessary to refactor the way we store and track the LinearCombination. The current implementation of LinearCombination doesn't track itself (it just updates its own terms after add or mul operations, then return the new LinearCombination). One way to track the LinearCombination, we might need r1cs backend to have a vector for the intermediate linear combinations(the intermediate states of a LinearCombination before being reduced by a constraint).

We could just display these linear combinations for now, although displayed asm info can be redundant (as I tried to explain above ^) for some lines of code since it doesn't track the intermediate linear combinations.

The other issue is that the refactor of R1csCellVar lead to the use of clone() whenever the R1csCellVar is presented. That is due to the fact the R1csCellVar can contains linear combination that holds hash map for terms. This could be avoid if the backend track the linear combination vector ^, then the R1csCellVar only needs to have a couple enum primitive types while the data can be retrieved from the vector managed by the R1CS backend.

[katat]

not sure I see how debugging is affected, could be nice to dump an example to see what it looks like :)

The intermediate calculations from the linear combinations are skipped. Take https://github.com/zksecurity/noname/blob/0c887067ba9387e76fa5ef28168c067c13cbf79b/examples/arithmetic.no#L2 for example, it only displays the span for the constraints.

I have updated the linear combination struct to also include the span. So we would just update the debug formatting to also display the intermediate linear combinations along with source code spans: https://github.com/zksecurity/noname/issues/75

[katat]

That will be tackled in another PR: https://github.com/zksecurity/noname/issues/70