Merge pull request #224 from dalek-cryptography/oleg/two-phase

Two-phase low-level variable commitments in R1CS protocol

Author: hdevalence

docs/cs-proof.md

@@ -17,54 +17,74 @@ The protocol begins with the prover computing commitments to the secret values \
 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](#building-constraints), allocating necessary multiplication gates on the fly,
-generating challenge values bound to the commitments \\(V_i\\), filling in weights \\(\mathbf{W}\_L,\mathbf{W}\_R,\mathbf{W}\_O,\mathbf{W}\_V\\), and assigning values to the left, right and output wires
-of the multiplication gates (\\(\mathbf{a}\_{L}, \mathbf{a}\_{R}, \mathbf{a}\_{O}\\)).
+The prover then [builds constraints](#building-constraints) in two phases.
 
-Once all multiplication wires are assigned, the prover commits to them via vector Pedersen commitments:
+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 \\\\
+\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\\)
+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
+\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
+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}\_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,
+\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\\) and \\(\mathbf{w}\_V\\) has length \\(m\\).
+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 \cdot x + \mathbf{s}\_L \cdot x^3 + \mathbf{y}^{-n} \circ \mathbf{w}\_R \cdot x + \mathbf{a}\_O \cdot x^2 \\\\
-  {\mathbf{r}}(x)  &\gets \mathbf{y}^n \circ \mathbf{a}\_R \cdot x + \mathbf{y}^n \circ \mathbf{s}\_R \cdot x^3 + \mathbf{w}\_L \cdot x - \mathbf{y}^n + \mathbf{w}\_O \\\\
+  {\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}
 \\]
@@ -80,16 +100,16 @@ The prover generates blinding factors for terms \\(t\_1, t\_3, t\_4, t\_5, t\_6\
 \\]
 
 The prover adds \\(T_1, T_3, T_4, T_5, T_6\\) to the protocol transcript
-and obtains a challenge scalar \\(x \in {\mathbb Z\_p}\\) from the transcript.
+and obtains the challenge scalars \\(u,x \in {\mathbb Z\_p}\\) from the transcript.
 
-Using the concrete value \\(x\\), the prover computes
+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} \cdot x + \tilde{o} \cdot x^2 + \tilde{s} \cdot x^3 \\\\
+  {\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}
 \\]
 
@@ -104,34 +124,43 @@ The prover evaluates polynomials \\(\mathbf{l}(x), \mathbf{r}(x)\\) and
 
 \\[
 \begin{aligned}
-             n^{+} &= 2^{\lceil \log_2 n \rceil} \\\\
-\mathbf{l}^{+}     &= \mathbf{l}(x) \hspace{0.1cm} || \hspace{0.1cm} \mathbf{0} \\\\
-\mathbf{r}^{+}     &= \mathbf{r}(x) \hspace{0.1cm} || \hspace{0.1cm} [-y^n,...,-y^{n^{+}-1}]
+             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}
-\mathbf{G}^{+}     &= \mathbf{G}    \hspace{0.1cm} || \hspace{0.1cm} [G_n,...,G_{n^{+}-1}] \\\\
-{\mathbf{H}'}^{+}  &= \mathbf{H}'   \hspace{0.1cm} || \hspace{0.1cm} \Big( [y^n,...,y^{n^{+}-1}] \circ [H_n,...,H_{n^{+}-1}] \Big) \\\\
+\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](../inner_product_proof/index.html) to prove the relation:
 \\[
 \operatorname{PK}\left\\{
-  (\mathbf{G}^{+}, {\mathbf{H}'}^{+} \in {\mathbb G}^{n^{+}}, P', Q \in {\mathbb G}; \mathbf{l}^{+}, \mathbf{r}^{+} \in {\mathbb Z\_p}^{n^{+}})
-  : P' = {\langle \mathbf{l}^{+}, \mathbf{G}^{+} \rangle} + {\langle \mathbf{r}^{+}, {\mathbf{H}'}^{+} \rangle} + {\langle \mathbf{l}^{+}, \mathbf{r}^{+} \rangle} Q
+  (\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\\}
-\\] where \\({\mathbf{H}'}^{+} = {\mathbf{y}}^{-n^{+}} \circ \mathbf{H}^{+}\\).
+\\]
 
 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 \\(13+2k\\) 32-byte elements:
+The complete proof consists of \\(16+2k\\) 32-byte elements:
 \\[
-  \\{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\\}
+  \\{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\\}
 \\]
 
 
@@ -140,21 +169,28 @@ Verifier’s algorithm
 --------------------
 
 The input to the verifier is the aggregated proof, which contains the \\(m\\) value commitments \\(V_{(j)}\\),
-and \\(32 \cdot (13 + 2 k)\\) bytes of the proof data where \\(k = \lceil \log_2(n) \rceil\\) and \\(n\\) is a number of [multiplication gates](#multiplication-gates):
+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](#multiplication-gates):
 
 \\[
-  \\{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\\}
+  \\{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](#building-constraints), allocating necessary multiplication gates on the fly and
-generating challenge values bound to the commitments \\(V_i\\).
+The verifier then [builds constraints](#building-constraints) in two phases.
 
-The verifier uses the Fiat-Shamir transform to obtain challenges by adding the appropriate data sequentially to the protocol transcript:
+In the first phase, the verifier allocates \\(n'\\) multiplication gates and the first set of constraints without using challenges.
 
-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 \\(x \in {\mathbb Z\_p}\\),
+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:
@@ -175,10 +211,10 @@ by taking a larger slice of the generators \\(\mathbf{G},\mathbf{H}\\) and more
 
 \\[
 \begin{aligned}
-             n^{+} &= 2^{\lceil \log_2 n \rceil} \\\\
-\mathbf{G}^{+}     &= \mathbf{G}   \hspace{0.1cm} || \hspace{0.1cm} [G_n,...,G_{n^{+}-1}] \\\\
-\mathbf{H}^{+}     &= \mathbf{H}   \hspace{0.1cm} || \hspace{0.1cm} [H_n,...,H_{n^{+}-1}] \\\\
-\mathbf{y}^{n^{+}} &= \mathbf{y}^n \hspace{0.1cm} || \hspace{0.1cm} [y^n,...,y^{n^{+}-1}] \\\\
+              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}
 \\]
 
@@ -209,26 +245,29 @@ If we rewrite the check as a comparison with the identity point, we get:
 **Second**, verify the inner product argument for the vectors \\(\mathbf{l}(x), \mathbf{r}(x)\\) that form the \\(t(x)\\) (see [inner-product protocol](../inner_product_proof/index.html#verification-equation))
 
 \\[
-P' \overset ? = {\langle a \cdot \mathbf{s}, \mathbf{G}^{+} \rangle} + {\langle {\mathbf{y}^{-n^{+}}} \circ (b /{\mathbf{s}}), \mathbf{H}^{+} \rangle} + abQ - \sum\_{j=1}^{k} \left( L\_{j} u\_{j}^{2} + u\_{j}^{-2} R\_{j} \right).
+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](../notes/index.html#inner-product-proof):
 
 \\[
-0 \overset ? = P^{+} + t(x) wB - {\langle a \cdot \mathbf{s}, \mathbf{G}^{+} \rangle} - {\langle \mathbf{y}^{-n^{+}} \circ (b /\mathbf{s}), \mathbf{H}^{+} \rangle} - abwB + \sum\_{j=1}^{k} \left( L\_{j} u\_{j}^{2} + u\_{j}^{-2} R\_{j} \right),
+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](#proving-that-mathbflx-mathbfrx-are-correct) of \\(P^{+}\\) is:
 
 \\[
 \begin{aligned}
-  P^{+}   = -{\widetilde{e}} {\widetilde{B}} + x \cdot A_I + x^2 \cdot A_O - \langle \mathbf{1}, \mathbf{H}^{+} \rangle + W_L \cdot x + W_R \cdot x + W_O + x^3 \cdot S
-\end{aligned}
-\\]
-\\[
-\begin{aligned}
-  W_L &= \langle \mathbf{y}^{-n} \circ \mathbf{w}\_L, \mathbf{H} \rangle \\\\
-  W_R &= \langle \mathbf{y}^{-n} \circ \mathbf{w}\_R, \mathbf{G} \rangle \\\\
-  W_O &= \langle \mathbf{y}^{-n} \circ \mathbf{w}\_O, \mathbf{H} \rangle \\\\
+  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}
 \\]
 
@@ -239,15 +278,22 @@ Finally, verifier groups all scalars by each point and performs a single multisc
 
 \\[
 \begin{aligned}
-0 \quad \stackrel{?}{=} & \quad x       \cdot A\_I \\\\
-                      + & \quad x^2     \cdot A\_O \\\\
-                      + & \quad x^3     \cdot S \\\\
-                      + & \quad \langle r x^2 \mathbf{w}\_V, \mathbf{V} \rangle \\\\
-                      + & \quad \sum\_{i = 1,3,4,5,6} r x^i T\_{i} \\\\
-                      + & \quad \Big(w \big(t(x) - ab\big) + r \big(x^2 (w\_c + \delta(y,z)) - t(x)\big) \Big) \cdot B \\\\
-                      + & \quad (-{\widetilde{e}} - r{\tilde{t}}(x)) \cdot \widetilde{B} \\\\
-                      + & \quad {\langle \big( x \mathbf{y}^{-n} \circ \mathbf{w}\_R \big) || \mathbf{0} - a\mathbf{s}, \mathbf{G}^{+} \rangle}\\\\
-                      + & \quad {\langle -\mathbf{1} + \mathbf{y}^{-n^{+}} \circ \big( (x \mathbf{w}\_L + \mathbf{w}\_O) || \mathbf{0} - (b /{\mathbf{s}}) \big), \mathbf{H}^{+} \rangle}\\\\
+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}