Circle STARK: Understanding Circle Group’s Operation as Rotation

The goal of this blog is to explain circle group without complex mathematical definitions. However, this approach is not rigorous, it serves more like a intuition of understanding the geometry of a circle group. Before diving into the blog, may you need some pre-readings like Exploring circle STARKs or Yet

Constraint system in STWO

About the repetition in GKR

There are different ways to describe the GKR algorithm

from Libra paper:

\(\tilde{V}_i(g) = \sum\limits_{x,y \in \{0,1\}^{s_{i+1}}} f_i(x,y)\)

\(= \sum\limits_{x,y \in \{0,1\}^{s_{i+1}}} \left( \widetilde{add}_{i+1}(g,x,y)(\tilde{V}_{i+1}(x) + \tilde{V}_{i+1}(y))\right.\)

\(\left. + \tilde{mult}_{i+1}(g,x,y)(\tilde{V}_{i+1}(x)\tilde{V}_{i+1}(y)) \right)\)

from hyrax paper:

$$\widetilde{V_0}(q’,q)=\sum\limits_{h’\in \{0,1\}^{b_N}}\sum\limits_{h_L\in \{0,1\}^{b_G}}\sum\limits_{h_R\in \{0,1\}^{b_G}}P_{q’,q,1}(h’,h_L,h_R)$$

$$=\sum\limits_{h’\in \{0,1\}^{b_N}}\sum\limits_{h_L\in \{0,1\}^{b_G}}\sum\limits_{h_R\in \{0,1\}^{b_G}}\widetilde{eq_1}(q’,h’)$$

$$\cdot [\widetilde{mul_1}(q,h_L,h_R)(\widetilde{V_1}(h’,h_L)\times \widetilde{V_1}(h’,h_R) )$$

$$+\widetilde{add_1}(q,h_L,h_R)(\widetilde{V_1}(h’,h_L)+ \widetilde{V_1}(h’,h_R) )]$$…

Libra GKR Prover

performance:

Prover is \(\mathcal{O}(C)\)

Verifier is \(\mathcal{O}(d\log C)\) for d-depth log-space uniform circuit.

note: in sumcheck/GKR context, the size of the circuit usually is described as \(2^l\), namely, the inputs of the circuit is \(2^l\), for a linear prover in this setting, has complexity \(\mathcal{O}(2^l)\), a logarithmic verifier has \(\mathcal{O}(l)\) …

Spartan- part 1

Table of Contents

R1CS encoding

R1CS instance \(x=(\mathbb{F},A,B,C,io,m,n)\)

let \(Z=(io,1,w)\), then we have for example

\(\underbrace{\begin{bmatrix}0&1&1&0\\0&0&1&0\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{A}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\circ \underbrace{\begin{bmatrix}0&1&0&0\\0&0&1&0\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{B}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\)

\(=\underbrace{\begin{bmatrix}1&0&0&0\\0&0&0&1\\…&…&…&..\\…&…&…&..\end{bmatrix}}_{C}\begin{pmatrix}w_1\\1\\w_2\\w_3\end{pmatrix}\)

This express the constraints:

$$(1+w_2) \cdot 1=w_1$$

$$w_2 \cdot w_2=w_3$$

In order to use the sum-check protocol, we need to encode R1CS in a different way, as sum-check is about …