R1CS and zkSNARK

so recently I've been exploring zk-SNARKs algorithm, and I have a maybe stupid question. For example, let's take $x^2+x+1$ and make an algebraic circuit from it:

1. $y=x*x$
2. $sum=x+1$
3. $out=sum+y$

(First question: are finite fields needed here?)

Now we need to construct a R1CS to each gate. Our variables and one: ${1, x, y, sum, out}$

So we have:

1. $A_1 = [0, 1, 0, 0, 0]$, $B_1 = [0, 1, 0, 0, 0]$, and $C_1 = [0, 0, 1, 0, 0]$.
2. $A_2 = [1, 1, 0, 0, 0]$, $B_2 = [1, 0, 0, 0, 0]$, and $C_2 = [0, 0, 0, 1, 0]$.
3. $A_3 = [0, 0, 1, 1, 0]$, $B_3 = [1, 0, 0, 0, 0]$, and $C_3 = [0, 0, 0, 0, 1]$

After that, how finite fields are used exactly? Are computations between solution vector and all these nine made in a some $\mathbb{F_q}$? How is $q$ then defined? And why a solution vector is actually proving that our computations are true?

All computations in the proof are done in the finite field. The advantage of using Finite fields is that it keeps the operations closed - i.e. the output of an operation will also be in the same field - it won't be unbounded. Also using a field means that you will not end up with fractions or floating point numbers - so using a field makes it easy & also accurate. For e.g. take Vitalik Buterin's example of R1CS/QAP - https://medium.com/@VitalikButerin/quadratic-arithmetic-programs-from-zero-to-hero-f6d558cea649. Here he ends up with Polynomials which look like $[-5.0, 9.166, -5.0, 0.833]$ i.e. $0.833x^3 - 5x^2 + 9.166x -5$ - with Polynomails like these, when you divide $t(x)$ by $Z(x)$ like he does in the writeup, you will end up with a remainder - a very small remainder because floating point arithmetic is not exact though he says there is no remainder. On the other hand, if you had perform $t/Z$ in a finite field, you will actually end up with no remainder because there are no floating point numbers.

Also, in Groth16 (which uses R1CS/QAP), homomorphic hiding is used for the proof so that you are not exposing the polynomial to the verifier. The verifier verifies the proof using Elliptic Curve Bilinear pairings - How exactly bilinear pairing multiplication in the exponent of g is used in zk-SNARK polynomial verification step?. Pairings require a base finite field & an extension field. Pairings require 2 Elliptic Curve group generators operating on the fields - How to find second subgroup for ECC Pairing?. This is also another reason why finite fields are used.

There are also SNARKs like PLONK, where the Schwartz Zippel lemma is used for several proofs (PLONK doesn't use R1CS/QAP - it uses a different proving mechanism). If you have 2 polynomials $A(X)$ & $B(X)$ & the prover has to prove that they are the same polynomial. So you create a 3rd polynomial $P(X) = A(X) - B(X)$ - if the degree of the polynomial $P$ is $\le d$ & let's say $d = 2^{40}$. Now if you operate in a finite field $\mathbb F_p$ such that $p$ is very, very large as compared to $d$, say $p = 2^{256}$, then the verifier selects a random point $r \in \mathbb F_p$ & if you prover can prove that at $r$, $F(r)$ is $0$, then as per the Schwartz Zippel lemma, $F$ is the zero polynomial - i.e. it's $0$ at all points. Since $F$ is the zero polynomial it means $A(X) = B(X)$ which is what the prover set out to prove.

The solution vector takes care of 2 things

1. It helps the Prover prove that each Gate circuit is satisfied.
2. It also helps the Prover prove consistency across Gates i.e. since the same solution vector is used for all Gates, ensures stuff like the output of the first gate is the left input to the 2nd gate, the same public input is used as the right term of both the 4th & 5th gate & other such things.