<aside> 💡 TLDR; Seems to me decision functions come in different types, and each type offers advantages when you pair it with proving system. (why suitable for pairing based zk proof systems)
R1CS is a different way to represent a statement representation.
Algebraic circuit is a class of decision functions, and defines an R1CS and helps compute R1CS solutions (so its a witness generator function).
</aside>
| Algebraic Circuits | R1CS | QAP | |
|---|---|---|---|
| Statement (both are membership claims) | There is a word (I;W) in L_R1CS | There is a word (I;W) in L_{QAP} | |
| Decision function | |||
| Proof | A valid assignment of field elements to the edges of the circuit | Check if elements of proof satisfy the R1CS constraints/equations | Polynomial P such that its divisible by T |
| Pros | Efficiently compute R1CS. Important for prover. |
circuit satisfiability is important,
helpful for zk proof systems since executing circuits can do witness generation. More practical usage | R1CS is a different way to represent a statement representation. Upgrade from formal languages as you separate into digestable, quadratic, discrete binary operations.
Preferred for specific proving systems | Efficiently proving R1CS statements, thus circuit statements, by just proving some polynomial divides by another. SUPER easy for verifier. | | Cons | | | Incurs high prover cost, lagrange is intense operation. |
How to represent statements and decision functions for proving systems.
Formal languages is not the best way to represent decisions for zero knowledge proving systems.
One type of constraint system is R1CS, which is a standard in zk proof systems.
Quadratic equations over a finite field, best for pairing based proving systems, since you can separate witness from instances and check the solution to equations in the exponent of pairing friendly cryptographic groups
R1CS
Each row or equation is called a constraint! Represents at a particular step in the execution of computation, what variables are being used at that step and how it should be constrained. Such that the relationship among all those variables on that row are constrained.
This means program execution is enforced to be computed in the exact way.
Very similar to a proof since it shows the exact sequence of steps by each equation to how the program should execute.
<aside> 💡 why cant formal language statements be used for proving program execution instead of R1CS?
My understanding is that formal language decision functions are used for formally rigorous purposes. BUT depends on proof system that makes R1CS more desirable.
</aside>
Flatten the equations into only multiplying two variables at a time