Constructing division gate in R1CS One thing I don't quite understand is how to naively handle division operation in rank-1 constraint systems (R1CS).
supposedly A.s * B.s - C.s = 0 allows you to perform any addition/subtraction/multiplication/division operations, but how do you actually perform division from multiplication gate in any of the SNARKs system? the only thing I can think of is to use multiplicative inverse of the value you want to divide as your input for B in the A*Bpart, so that A*B becomes A*B^-1 which is same as performing A/B
My question is how does the verifier know the input prover send to the division gate is the multiplicative inverse of B? it seems that the verifier would need to either trust the prover sending the correct input (there is no way to check that the prover is sending B^-1 or some other B'^-1 ), did I miss something here?
-edited
My question is about how to build R1CS constraint on division. for example, how do I build a constraint matrix for (a*b)/(c*d) where a,b,c,d are inputs to an arithmetic circuit.
Well this question depends on what you mean by $\textit{division}$. R1CS is usually defined over a finite field $\mathbb{F}_p$, so constraints about modular inverses are quite easy to represent. On the other hand, if you're asking about integer division, which is not natively supported by finite field arithmetic, then this becomes more tricky.
Let me expand on this. I'll try to follow the notation used in Vitalik's popular post. In order to represent a modular inverse operation such as $x \cdot y^{-1} = z$, we could define two constraints in our flattened arithmetic circuit:
$\text{one = y}\cdot \text{y_inv}$
$\text{z = x}\cdot \text{y_inv}$
As you can see, we've introduced the extra variable $\text{y_inv}$ and added the constraint that $y \cdot y^{-1} = 1$ (i.e., the definition of modular inverse).
Now, you might instead be asking the question of how we perform integer division i.e., $\lfloor\frac{x}{y}\rfloor = z$, using finite field arithmetic? Recall that this is much different than taking modular inverses in $\mathbb{F}_p$.
As example, let's try $7 / 2$ in $\mathbb{F}_{11}$:
$7 / 2 = 7 \cdot 2^{-1} = 7 \cdot 6 = 42 = 9 \mod 11$, since $6$ is the modular inverse of $2$ in $\mathbb{F}_{11}$.
However, $\lfloor\frac{7}{2}\rfloor = 3$ (obviously) if we're talking about integer arithmetic. This more complex operation can be represented in $O(\log(p))$ R1CS gates using non-determinsitic advice e.g., by enforcing that $x = z \cdot y + r$ and $r &lt; y$, where $r$ is provided by the prover.