Support R1CS asm

[katat]

This PR is to support asm (a debug feature) for R1CS backends.

Currently here is a draft example for equals.no:

v_0 + v_3 = 0
v_1 + v_3 = v_4
v_2 + v_5 = 0
v_5 + 1 = v_6
(v_2) * (v_4) = v_7
v_7 = 0
(v_8) * (v_4) = v_9
v_9 = v_6
v_2 = 1
v_10 = 3
v_0 + v_12 = 0
v_12 + v_10 = v_13
v_11 + v_14 = 0
v_14 + 1 = v_15
(v_11) * (v_13) = v_16
v_16 = 0
(v_17) * (v_13) = v_18
v_18 = v_15
v_11 = 1

v_* are the witness variables.

Each line represents a constraint (a*b = c) that contains the linear combinations of terms made up of factor and witness variables. If the value is 1 for either a or b, the linear combination will be ignored for reducing the unnecessary info.

• [x] review the format
• [x] wire up with span of debug info
• [ ] move generate_asm out of backend trait

[mimoo]

Quick comment: this format is not bijective. There are several r1cs constraints system that correspond to this one (for example, each line that doesn't involve a multiplication could have the constraint be encoded in A, B or C)

[katat]

Updated the format. Here is the example for public_output.no.

v_3 == (v_0 + v_1) * (1)
2 == (v_3) * (1)
v_4 == (v_3 + 6) * (1)
v_4 == (v_2) * (1)

The format assumes: C = A * B

[mimoo]

BTW another problem with this format is that we don't know what is part of the public input :D (I think the kimchi format has the same issue, created https://github.com/zksecurity/noname/issues/65).

I'm also not sure I understand it from your example, is it C == A B? If so, why not place A B first and then C? (so A * B == C) which is the "convention" when I see R1CS

[katat]

I'm also not sure I understand it from your example, is it C == A B? If so, why not place A B first and then C? (so A * B == C) which is the "convention" when I see R1CS

It was intended to align with the noname code in debug mode :D

Yeah, let's use A * B == C instead.

[mimoo]

also let's write 1 instead of v_0? (if the intention is to have v_0 be 1?)

[katat]

also let's write 1 instead of v_0? (if the intention is to have v_0 be 1?)

v_0 represents the 0 indexed variable.

do you mean substituting the witness variable with its value? but will this lost the trace of the variables?