Module bulletproofs::r1cs::notes

Constraint system proof protocol

The constraint_system module contains an API for producing a proof that a set of secret values satisfies a given constraint system.

For more background on the constraint system proofs, see these two sections in the notes module:

• Constraint system: description of the constraint system architecture.
• Constraint system proof: the math behind the constraint system proofs.

Prover’s algorithm

The protocol begins with the prover computing commitments to the secret values \(\mathbf{v}\) and adding all commitments to the protocol transcript.

\[ V_i \gets \operatorname{Com}(v_i, {\widetilde{v}_i}) = v_i \cdot B + {\widetilde{v}_i} \cdot {\widetilde{B}} \] where each \(\widetilde{v}_i\) is sampled randomly.

The prover then builds constraints in two phases.

In the first phase, the prover allocates necessary multiplication gates on the fly, fills in weights \(\mathbf{W}_L',\mathbf{W}_R',\mathbf{W}_O',\mathbf{W}_V'\), and assigns values to the left, right and output wires of the multiplication gates (\(\mathbf{a}_L', \mathbf{a}_R', \mathbf{a}_O'\)) without using the challenge values.

Once \(n'\) multiplication gates are assigned, the prover commits to them via vector Pedersen commitments:

\[ \begin{aligned} \tilde{a}' \;&{\xleftarrow{\$}}\; \mathbb Z_p \\ \tilde{o}' \;&{\xleftarrow{\$}}\; \mathbb Z_p \\ A_I' &\gets \widetilde{B} \cdot \tilde{a}' + \langle \mathbf{G}' , \mathbf{a}_L' \rangle + \langle \mathbf{H}', \mathbf{a}_R' \rangle \\ A_O' &\gets \widetilde{B} \cdot \tilde{o}' + \langle \mathbf{G}' , \mathbf{a}_O' \rangle \\ \end{aligned} \]

The prover also computes blinding factors \(\mathbf{s}_L', \mathbf{s}_R'\) for the left and right multiplication values and commits to them:

\[ \begin{aligned} \mathbf{s}_L' \; &{\xleftarrow{\$}}\; {\mathbb Z_p}^{n'} \\ \mathbf{s}_R' \; &{\xleftarrow{\$}}\; {\mathbb Z_p}^{n'} \\ \tilde{s}' \; &{\xleftarrow{\$}}\; \mathbb Z_p \\ S' &\gets \widetilde{B} \cdot \tilde{s}' + \langle \mathbf{G}', \mathbf{s}_L' \rangle + \langle \mathbf{H}', \mathbf{s}_R' \rangle \end{aligned} \]

The prover adds \(A_I'\), \(A_O'\) and \(S'\) to the protocol transcript.

In the second phase, the prover is allowed to use challenge values when allocating multiplication gates (\(\mathbf{a}_{L}'', \mathbf{a}_{R}'', \mathbf{a}_{O}''\)) and computing weights \(\mathbf{W}_L'',\mathbf{W}_R'',\mathbf{W}_O'',\mathbf{W}_V''\).

When additional \(n''\) multiplication gates are assigned, the prover commits to them via vector Pedersen commitments, along with the corresponding blinding factors \(\mathbf{s}_L'', \mathbf{s}_R''\):

\[ \begin{aligned} \tilde{a}'' \;&{\xleftarrow{\$}}\; \mathbb Z_p \\ \tilde{o}'' \;&{\xleftarrow{\$}}\; \mathbb Z_p \\ A_I'' &\gets \widetilde{B} \cdot \tilde{a}'' + \langle \mathbf{G}'' , \mathbf{a}_L'' \rangle + \langle \mathbf{H}'', \mathbf{a}_R'' \rangle \\ A_O'' &\gets \widetilde{B} \cdot \tilde{o}'' + \langle \mathbf{G}'' , \mathbf{a}_O'' \rangle \\ \mathbf{s}_L'' \; &{\xleftarrow{\$}}\; {\mathbb Z_p}^{n''} \\ \mathbf{s}_R'' \; &{\xleftarrow{\$}}\; {\mathbb Z_p}^{n''} \\ \tilde{s}'' \; &{\xleftarrow{\$}}\; \mathbb Z_p \\ S'' &\gets \widetilde{B} \cdot \tilde{s}'' + \langle \mathbf{G}'' , \mathbf{s}_L'' \rangle + \langle \mathbf{H}'', \mathbf{s}_R'' \rangle \end{aligned} \]

The prover adds \(A_I''\), \(A_O''\) and \(S''\) to the protocol transcript and obtains challenge scalars \(y,z \in {\mathbb Z_p}\) from the transcript.

The prover then flattens the constraints using \(q\) powers of challenge \(z\):

\[ \begin{aligned} \mathbf{w}_L &\gets z \mathbf{z}^q \cdot (\mathbf{W}_L' || \mathbf{W}_L''), \\ \mathbf{w}_R &\gets z \mathbf{z}^q \cdot (\mathbf{W}_R' || \mathbf{W}_R''), \\ \mathbf{w}_O &\gets z \mathbf{z}^q \cdot (\mathbf{W}_O' || \mathbf{W}_O''), \\ \mathbf{w}_V &\gets z \mathbf{z}^q \cdot (\mathbf{W}_V' || \mathbf{W}_V''), \end{aligned} \] where each of \(\mathbf{w}_L, \mathbf{w}_R, \mathbf{w}_O\) has length \(n = n' + n''\) and \(\mathbf{w}_V\) has length \(m\).

The prover then constructs the blinded polynomials and their inner product:

\[ \begin{aligned} {\mathbf{l}}(x) &\gets (\mathbf{a}_L' || \mathbf{a}_L'') \cdot x + (\mathbf{s}_L' || \mathbf{s}_L'') \cdot x^3 + \mathbf{y}^{-n} \circ \mathbf{w}_R \cdot x + (\mathbf{a}_O' || \mathbf{a}_O'') \cdot x^2 \\ {\mathbf{r}}(x) &\gets \mathbf{y}^n \circ (\mathbf{a}_R' || \mathbf{a}_R'') \cdot x + \mathbf{y}^n \circ (\mathbf{s}_R' || \mathbf{s}_R'') \cdot x^3 + \mathbf{w}_L \cdot x - \mathbf{y}^n + \mathbf{w}_O \\ t(x) &\gets {\langle {\mathbf{l}}(x), {\mathbf{r}}(x) \rangle} \end{aligned} \]

The prover generates blinding factors for terms \(t_1, t_3, t_4, t_5, t_6\) and creates Pedersen commitments to them (term \(t_0\) is known to be zero and term \(t_2\) is being proven):

\[ \begin{aligned} &\tilde{t}_1, \tilde{t}_3, \tilde{t}_4, \tilde{t}_5, \tilde{t}_6 \;{\xleftarrow{\$}}\; \mathbb Z_p \\ &T_i \gets \operatorname{Com}(t_i, {\tilde{t}_i}) = t_i \cdot B + {\tilde{t}_i} \cdot {\widetilde{B}} \\ \end{aligned} \]

The prover adds \(T_1, T_3, T_4, T_5, T_6\) to the protocol transcript and obtains the challenge scalars \(u,x \in {\mathbb Z_p}\) from the transcript.

Using the concrete values \(u, x\), the prover computes the synthetic blinding factors \({\tilde{t}}(x)\) and \(\tilde{e}\):

\[ \begin{aligned} \tilde{t}_2 &\gets \langle \mathbf{w}_V, \tilde{\mathbf{v}} \rangle \\ {\tilde{t}}(x) &\gets \sum_{i = 1}^{6} x^i \tilde{t}_{i} \\ {\tilde{e}} &\gets (\tilde{a}' + u \tilde{a}'') \cdot x + (\tilde{o}' + u \tilde{o}'') \cdot x^2 + (\tilde{s}' + u \tilde{s}'') \cdot x^3 \\ \end{aligned} \]

The prover adds \(t(x), {\tilde{t}}(x), {\tilde{e}}\) to the protocol transcript, obtains a challenge scalar \(w \in {\mathbb Z_p}\), and uses it to create a point \(Q\):

\[ Q \gets w \cdot B \]

The prover evaluates polynomials \(\mathbf{l}(x), \mathbf{r}(x)\) and pads them to the next power of two \(n \rightarrow n^{+}\):

\[ \begin{aligned} n^{+} &\gets 2^{\lceil \log_2 n \rceil} \\ \mathbf{l}^{+} &\gets \mathbf{l}(x) \hspace{0.1cm} || \hspace{0.1cm} \mathbf{0} \\ \mathbf{r}^{+} &\gets \mathbf{r}(x) \hspace{0.1cm} || \hspace{0.1cm} [-y^n,...,-y^{n^{+}-1}] \end{aligned} \]

The prover transmutes generators using challenges \(y\) and \(u\):

\[ \begin{aligned} \hat{\mathbf{G}} &\gets \mathbf{G}' || (u \cdot \mathbf{G}'') \\ \hat{\mathbf{H}} &\gets \mathbf{y}^{-n} \circ \big( \mathbf{H}' || (u \cdot \mathbf{H}'') \big) \\ \end{aligned} \]

The prover also takes a larger slice of the generators \(\mathbf{G}, \mathbf{H}\):

\[ \begin{aligned} \hat{\mathbf{G}}^{+} &\gets \hat{\mathbf{G}} \hspace{0.1cm} || \hspace{0.1cm} u \cdot [G_n,...,G_{n^{+}-1}] \\ \hat{\mathbf{H}}^{+} &\gets \hat{\mathbf{H}} \hspace{0.1cm} || \hspace{0.1cm} u \cdot [y^{-n} H_n,..., y^{-(n^{+}-1)} H_{n^{+}-1}] \\ \end{aligned} \]

Finally, the prover performs the inner product argument to prove the relation: \[ \operatorname{PK}\left\{ (\hat{\mathbf{G}}^{+}, \hat{\mathbf{H}}^{+} \in {\mathbb G}^{n^{+}}, P', Q \in {\mathbb G}; \mathbf{l}^{+}, \mathbf{r}^{+} \in {\mathbb Z_p}^{n^{+}}) : P' = {\langle \mathbf{l}^{+}, \hat{\mathbf{G}}^{+} \rangle} + {\langle \mathbf{r}^{+}, \hat{\mathbf{H}}^{+} \rangle} + {\langle \mathbf{l}^{+}, \mathbf{r}^{+} \rangle} Q \right\} \]

The result of the inner product proof is a list of \(2k\) points and \(2\) scalars, where \(k = \lceil \log_2(n) \rceil\): \(\{L_k, R_k, \dots, L_1, R_1, a, b\}\).

The complete proof consists of \(16+2k\) 32-byte elements: \[ \{A_I', A_O', S', A_I'', A_O'', S'', T_1, T_3, T_4, T_5, T_6, t(x), {\tilde{t}}(x), \tilde{e}, L_k, R_k, \dots, L_1, R_1, a, b\} \]

Verifier’s algorithm

The input to the verifier is the aggregated proof, which contains the \(m\) value commitments \(V_{(j)}\), and \(32 \cdot (16 + 2 k)\) bytes of the proof data where \(k = \lceil \log_2(n) \rceil\) and \(n\) is a number of multiplication gates:

\[ \{A_I', A_O', S', A_I'', A_O'', S'', T_1, T_3, T_4, T_5, T_6, t(x), {\tilde{t}}(x), \tilde{e}, L_k, R_k, \dots, L_1, R_1, a, b\} \]

The verifier starts by adding all value commitments \(V_i\) to the protocol transcript.

The verifier then builds constraints in two phases.

In the first phase, the verifier allocates \(n'\) multiplication gates and the first set of constraints without using challenges.

Then, the verifier uses the Fiat-Shamir transform to generate challenges required by the gadgets by adding the intermediate commitments \(A_I', A_O', S'\) to the protocol transcript.

In the second phase, the verifier allocates additional \(n''\) multiplication gates and the second set of constraints, providing necessary challenges to the gadgets that form the constraint system.

The verifier obtains more challenges by adding the appropriate data sequentially to the protocol transcript:

1. \(A_I'', A_O'', S''\) are added to obtain challenge scalars \(y,z \in {\mathbb Z_p}\),
2. \(T_1, T_3, T_4, T_5, T_6\) are added to obtain a challenge scalars \(u,x \in {\mathbb Z_p}\),
3. \(t(x), {\tilde{t}}(x), \tilde{e}\) are added to obtain a challenge \(w \in {\mathbb Z_p}\).

The verifier flattens constraints:

\[ \begin{aligned} \mathbf{w}_L &\gets z \mathbf{z}^q \cdot \mathbf{W}_L, \\ \mathbf{w}_R &\gets z \mathbf{z}^q \cdot \mathbf{W}_R, \\ \mathbf{w}_O &\gets z \mathbf{z}^q \cdot \mathbf{W}_O, \\ \mathbf{w}_V &\gets z \mathbf{z}^q \cdot \mathbf{W}_V, \\ w_c &\gets \langle z \mathbf{z}^q, \mathbf{c} \rangle, \end{aligned} \] where each of \(\mathbf{w}_L, \mathbf{w}_R, \mathbf{w}_O\) has length \(n\) and \(\mathbf{w}_V\) has length \(m\).

The verifier pads the proof data by taking a larger slice of the generators \(\mathbf{G},\mathbf{H}\) and more powers of challenges \(y\) up to \((n^{+}-1)\):

\[ \begin{aligned} n^{+} &\gets 2^{\lceil \log_2 n \rceil} \\ \mathbf{G}^{+} &\gets \mathbf{G} \hspace{0.1cm} || \hspace{0.1cm} [G_n,...,G_{n^{+}-1}] \\ \mathbf{H}^{+} &\gets \mathbf{H} \hspace{0.1cm} || \hspace{0.1cm} [H_n,...,H_{n^{+}-1}] \\ \mathbf{y}^{n^{+}} &\gets \mathbf{y}^n \hspace{0.1cm} || \hspace{0.1cm} [y^n,...,y^{n^{+}-1}] \\ \end{aligned} \]

The verifier computes the following scalars for the inner product argument:

\[ \{u_{1}^{2}, \dots, u_{k}^{2}, u_{1}^{-2}, \dots, u_{k}^{-2}, s_0, \dots, s_{n^{+}-1}\} \]

The goal of the verifier is to check two equations.

First, verify the second term of the polynomial \(t(x)\) (see notes):

\[ \begin{aligned} t(x) B + {\tilde{t}}(x) {\widetilde{B}} &\stackrel{?}{=} x^2 \langle \mathbf{w}_V, \mathbf{V} \rangle + x^2 \big(w_c + \delta(y,z)\big) B + \sum_{i = 1,3,4,5,6} x^i T_{i},\\ \delta(y, z) &= \langle \mathbf{y}^{-n} \circ \mathbf{w}_R, \mathbf{w}_L \rangle \\ \end{aligned} \]

If we rewrite the check as a comparison with the identity point, we get: \[ 0 \stackrel{?}{=} x^2 \langle \mathbf{w}_V, \mathbf{V} \rangle + x^2 \big(w_c + \delta(y,z)\big) B + \sum_{i = 1,3,4,5,6} x^i T_{i} - t(x) B - {\tilde{t}}(x) {\widetilde{B}} \]

Second, verify the inner product argument for the vectors \(\mathbf{l}(x), \mathbf{r}(x)\) that form the \(t(x)\) (see inner-product protocol)

\[ P' \overset ? = {\langle a \cdot \mathbf{s}, \hat{\mathbf{G}}^{+} \rangle} + {\langle b/\mathbf{s}, \hat{\mathbf{H}}^{+} \rangle} + abQ - \sum_{j=1}^{k} \left( L_{j} u_{j}^{2} + u_{j}^{-2} R_{j} \right), \] where \[ \begin{aligned} \hat{\mathbf{G}}^{+} &= \mathbf{G}' \hspace{0.1cm} || \hspace{0.1cm} u \cdot \mathbf{G}'' \hspace{0.1cm} || \hspace{0.1cm} u \cdot [G_n,...,G_{n^{+}-1}] \\ \hat{\mathbf{H}}^{+} &= \mathbf{y}^{-n^{+}} \circ \big( \mathbf{H}' \hspace{0.1cm} || \hspace{0.1cm} u \cdot \mathbf{H}'' \hspace{0.1cm} || \hspace{0.1cm} u \cdot [H_n,...,H_{n^{+}-1}]\big) \\ \end{aligned} \]

Rewriting as a comparison with the identity point and expanding \(Q = wB\) and \(P' = P^{+} + t(x) wB\) as needed for transition to the inner-product protocol:

\[ 0 \overset ? = P^{+} + t(x) wB - {\langle a \cdot \mathbf{s}, \hat{\mathbf{G}}^{+} \rangle} - {\langle b/\mathbf{s}, \hat{\mathbf{H}}^{+} \rangle} - abwB + \sum_{j=1}^{k} \left( L_{j} u_{j}^{2} + u_{j}^{-2} R_{j} \right), \] where the definition of \(P^{+}\) is:

\[ \begin{aligned} P^{+} = &-{\widetilde{e}} {\widetilde{B}} + x \cdot (A_I' + u \cdot A_I'') + x^2 \cdot (A_O' + u \cdot A_O'') \\ &-\langle \mathbf{1}, \mathbf{H}' \rangle - u \cdot \langle \mathbf{1}, {\mathbf{H}''} \rangle - u \cdot [H_n,...,H_{n^{+}-1}]\\ &+x \cdot \langle \mathbf{w}_L, \hat{\mathbf{H}} \rangle + x \cdot \langle \mathbf{w}_R, \hat{\mathbf{G}} \rangle + \langle \mathbf{w}_O, \hat{\mathbf{H}} \rangle + x^3 \cdot (S' + u \cdot S'') \end{aligned} \]

The verifier combines two equations in one by sampling a random factor \(r \; {\xleftarrow{\$}} \; {\mathbb Z_p}\), multiplying the first equation by \(r\), and adding it with the second equation.

Finally, verifier groups all scalars by each point and performs a single multiscalar multiplication:

\[ \begin{aligned} 0 \quad \stackrel{?}{=} & \quad x \cdot A_I' \\ + & \quad x^2 \cdot A_O' \\ + & \quad x^3 \cdot S' \\ + & \quad u \cdot x \cdot A_I'' \\ + & \quad u \cdot x^2 \cdot A_O'' \\ + & \quad u \cdot x^3 \cdot S'' \\ + & \quad \langle r \cdot x^2 \cdot \mathbf{w}_V, \mathbf{V} \rangle \\ + & \quad \sum_{i = 1,3,4,5,6} r \cdot x^i \cdot T_{i} \\ + & \quad \Big(w \cdot \big(t(x) - a \cdot b\big) + r \cdot \big(x^2 \cdot (w_c + \delta(y,z)) - t(x)\big) \Big) \cdot B \\ + & \quad (-{\widetilde{e}} - r \cdot {\tilde{t}}(x)) \cdot \widetilde{B} \\ + & \quad {\langle x \cdot \mathbf{y}^{-n^{+}}_{[0:n']} \circ \mathbf{w}_R' - a \cdot \mathbf{s}_{[0:n']}, \mathbf{G}^{+}_{[0:n']} \rangle}\\ + & \quad {\langle u \cdot \big( x \cdot \mathbf{y}^{-n^{+}}_{[n':n]} \circ \mathbf{w}_R'' - a \cdot \mathbf{s}_{[n':n]} \big), \mathbf{G}^{+}_{[n':n]} \rangle}\\ + & \quad {\langle -u \cdot a \cdot \mathbf{s}_{[n:n^{+}]}, \mathbf{G}^{+}_{[n:n^{+}]} \rangle}\\ + & \quad {\langle -\mathbf{1} + \mathbf{y}^{-n^{+}}_{[0:n']} \circ (x \mathbf{w}_L' + \mathbf{w}_O' - b /\mathbf{s}_{[0:n']} ), \mathbf{H}^{+}_{[0:n']} \rangle}\\ + & \quad {\langle u \cdot \big(-\mathbf{1} + \mathbf{y}^{-n^{+}}_{[n':n]} \circ (x \mathbf{w}_L'' + \mathbf{w}_O'' - b /\mathbf{s}_{[n':n]} ) \big), \mathbf{H}^{+}_{[n':n]} \rangle}\\ + & \quad {\langle u \cdot \big(-\mathbf{1} + \mathbf{y}^{-n^{+}}_{[n:n^{+}]} \circ ( -b /\mathbf{s}_{[n:n^{+}]} ) \big), \mathbf{H}^{+}_{[n:n^{+}]} \rangle}\\ + & \quad {\langle [u_{1}^2, \dots, u_{k}^2 ], [L_1, \dots, L_{k}] \rangle}\\ + & \quad {\langle [u_{1}^{-2}, \dots, u_{k}^{-2} ], [R_1, \dots, R_{k}] \rangle} \end{aligned} \] where \(1/{\mathbf{s}}\) are inverses of \(\mathbf{s}\), computed as a reversed list of \(\mathbf{s}\).