Perf/gkr/solvable var

[Tabaie]

A "solvable" variable in a polynomial is one that only occurs in monomials of total degree 1, and with a non-zero coefficient. Its value can be uniquely determined from the polynomial's and those of the other variables. For example, in $\ f(x,y,z) = 2x + yz $, $\ x $ is a solvable variable because we can get $\ x = \frac {f(x,y,z) - yz} 2 $.

In GKR, at the end of the sumcheck subprotocol for wire $\ w $, we end up with a claim of the form $\ w(r_1, r_2, \dots, r_n) = y $, where the symbol $\ w$ represents the current wire, as well as the multilinear extension of its value across all instances, represented on an n-dimensional hypercube . More explicitly,
$$g\big( w_1(r_1, r_2, \dots, r_n), w_2(r_1, r_2, \dots, r_n), \dots, w_m(r_1, r_2, \dots, r_n)\big) = y$$
where $\ w_1, \dots, w_m$ are the input wires to $\ w$'s gate, $\ g$.

The prover sends explicit claimed values $\ y_i = w_i(r_1, r_2, \dots, r_n) $. The verifier checks if the consistency of these claims with the original claim about $\ w $, i.e. whether indeed $\ g(y_1, y_2, \dots, y_m) = y$ and records the new claims to be verified later. In a non-interactive settings, $\ y_1, y_2, \dots, y_m$ are hashed, as new prover messages.

This optimization is based on the observation that if, say, the first variable of $\ g$ is solvable according to the above definition, the claim $\ y_1$ will not need to be hashed.

For a circuit consisting of 56K Poseidon2 permutations (equivalent to the Linea blob decompression circuit) this saves about 25K constraints, only about 0.5% of total constraints.

[Copilot]

Copilot encountered an error and was unable to review this pull request. You can try again by re-requesting a review.