R1CS

Introduction

The Rank 1 Constraint System (R1CS) is one of the common arithmetization techniques used today. In short, it uses 3 matrices to constrain two inputs to the gate and 1 output of the gate.

AzBz=?Cz\bm{Az}\cdot \bm{Bz}\stackrel{?}=\bm{Cz}

If the equation above is valid for a given A,B,C\bm{A},\bm{B},\bm{C} constraint matrices, we consider z\bm{z} a valid witness (also known as trace).

So how do we get these constraint matrices for a target computation? For the sake of simplicity, let's say we want to prove that we know a solution to x3+x+5=35x^3+x+5=35.

Flattening to gates

First we convert our x3+x+5x^3 + x + 5 program into simple statements which typically look like x=yx=y or x=yzx=y \oplus z. So x3+x+5x^3 + x + 5 can be flattened to:

sym_1 = x * x  
y = sym_1 * x  
sym_2 = y + x  
out = sym_2 + 5

Gates to R1CS

In this step we convert the equations above into an R1CS matrix representation. At each row of R1CS matrices, we have 3 row vectors a,b,c\bm{a},\bm{b},\bm{c} which we multiply with column vector z\bm{z}. This solution vector z\bm{z} should satisfy

za×zbzc=0za×zb=zc\bm{z}\cdot \bm{a} \times \bm{z} \cdot \bm{b} - \bm{z} \cdot \bm{c} = 0\\ \bm{z}\cdot \bm{a} \times \bm{z} \cdot \bm{b} = \bm{z}\cdot \bm{c}

Each vector's length is equal to the number of variables in our program plus 1 for constant 1. So in the case above, we have ~one,x,sym1,sym2,sym3,~out\char`\~one,x, sym_1, sym_2, sym_3, \char`\~ out so we need vectors of size 6. We need the extra constant 11 or identity multiplier to deal with situations involving addition in our scheme as well as to add constants. So in total for our case above we have:

index     0    1.   2     3.     4.   5.
varname ~one.  x. ~out  sym_1    y.  sym_2

The reason for having three vectors is due to the nature of the constraints R1CS is designed to represent. Remember, in circuit computation, we have conceptual gates. These gates have a left input, a right input, and one output. So, basically, the a\bm{a} vector represents the left input, the b\bm{b} vector represents the right input, and the c\bm{c} vector represents the output.

  1. To express sym1=xxsym_1 = x \cdot x, what we need to say is input 1 and input 2 is xx and result is sym1sym_1

a=(0,1,0,0,0,0)b=(0,1,0,0,0,0)c=(0,0,0,1,0,0)\bm{a} = (0, 1, 0, 0, 0, 0)\\ \bm{b} = (0, 1, 0, 0, 0, 0) \\ \bm{c} = (0, 0, 0, 1, 0, 0)
  1. Similarly, to express y=sym1xy = sym_1\cdot x:

a=(0,0,0,1,0,0)b=(0,1,0,0,0,0)c=(0,0,0,0,1,0)\bm{a} = (0, 0, 0, 1, 0, 0)\\ \bm{b} = (0, 1, 0, 0, 0, 0)\\ \bm{c} = (0, 0, 0, 0, 1, 0)
  1. For sym2=(x+y)1sym_2 = (x + y) \cdot 1, we have:

a=(0,1,0,0,1,0)b=(1,0,0,0,0,0)c=(0,0,0,0,0,1)\bm{a} = (0, 1, 0, 0, 1, 0)\\ \bm{b} = (1, 0, 0, 0, 0, 0)\\ \bm{c} = (0, 0, 0, 0, 0, 1)
  1. And for ~out=(sym2+5)1\char`~out = (sym_2 + 5) \cdot 1, we have:

a=(5,0,0,0,0,1)b=(1,0,0,0,0,0)c=(0,0,1,0,0,0)\bm{a} = (5, 0, 0, 0, 0, 1)\\ \bm{b} = (1, 0, 0, 0, 0, 0)\\ \bm{c} = (0, 0, 1, 0, 0, 0)

This gives us the R1CS matrix representation:

A  
[0, 1, 0, 0, 0, 0]  
[0, 0, 0, 1, 0, 0]  
[0, 1, 0, 0, 1, 0]  
[5, 0, 0, 0, 0, 1]
B  
[0, 1, 0, 0, 0, 0]  
[0, 1, 0, 0, 0, 0]  
[1, 0, 0, 0, 0, 0]  
[1, 0, 0, 0, 0, 0]
C  
[0, 0, 0, 1, 0, 0]  
[0, 0, 0, 0, 1, 0]  
[0, 0, 0, 0, 0, 1]  
[0, 0, 1, 0, 0, 0]

So by knowing z=[1,3,35,9,27,30]\bm{z} = [1, 3, 35, 9, 27, 30], you prove that you know the solution since it satisfies all the constraints.

References

Written by Batzorig Zorigoo from A41

Last updated