Crate hacspec_halo2

Protocol

Let $\omega \in \field$ be a $n = 2^k$ primitive root of unity forming the domain $D = (\omega^0, \omega^1, …, \omega^{n - 1})$ with $t(X) = X^n - 1$ the vanishing polynomial over this domain. Let $n_g, n_a, n_e$ be positive integers with $n_a, n_e \lt n$ and $n_g \geq 4$. We present an interactive argument $\halo = (\setup, \prover, \verifier)$ for the relation

$\relation = \left\{ \begin{array}{ll} &\left( \begin{array}{ll} \left( g(X, C_0, …, C_{n_a - 1}, a_0(X), …, a_{n_a - 1}\left(X, C_0, …, C_{n_a - 1}, a_0(X), …, a_{n_a - 2}(X) \right)) \right); \ \left( a_0(X), a_1(X, C_0, a_0(X)), …, a_{n_a - 1}\left(X, C_0, …, C_{n_a - 1}, a_0(X), …, a_{n_a - 2}(X) \right) \right) \end{array} \right) : \ \ & g(\omega^i, \cdots) = 0 , , , , \forall i \in [0, 2^k) \end{array} \right\}$

where $a_0, a_1, …, a_{n_a - 1}$ are (multivariate) polynomials with degree $n - 1$ in $X$ and $g$ has degree $n_g(n - 1)$ at most in any indeterminates $X, C_0, C_1, …$.

$\setup(\sec)$ returns $\pp = (\group, \field, \mathbf{G} \in \group^n, U, W \in \group)$.

For all $i \in [0, n_a)$:

• Let $\mathbf{p_i}$ be the exhaustive set of integers $j$ (modulo $n$) such that $a_i(\omega^j X, \cdots)$ appears as a term in $g(X, \cdots)$.
• Let $\mathbf{q}$ be a list of distinct sets of integers containing $\mathbf{p_i}$ and the set $\mathbf{q_0} = {0}$.
• Let $\sigma(i) = \mathbf{q}_j$ when $\mathbf{q}_j = \mathbf{p_i}$.

Let $n_q \leq n_a$ denote the size of $\mathbf{q}$, and let $n_e$ denote the size of every $\mathbf{p_i}$ without loss of generality.

In the following protocol, we take it for granted that each polynomial $a_i(X, \cdots)$ is defined such that $n_e + 1$ blinding factors are freshly sampled by the prover and are each present as an evaluation of $a_i(X, \cdots)$ over the domain $D$. In all of the following, the verifier’s challenges cannot be zero or an element in $D$, and some additional limitations are placed on specific challenges as well.

Step	Spec	Impl.	Protocol	Notes
1	NA	?	$\prover$ and $\verifier$ proceed in the following $n_a$ rounds of interaction, where in round $j$ (starting at $0$)
			* $\prover$ sets $a^\prime_j(X) = a_j(X, c_0, c_1, …, c_{j - 1}, a_0(X, \cdots), …, a_{j - 1}(X, \cdots, c_{j - 1}))$
			* $\prover$ sends a hiding commitment $A_j = \innerprod{\mathbf{a^\prime}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{a^\prime}$ are the coefficients of the univariate polynomial $a^\prime_j(X)$ and $\cdot$ is some random, independently sampled blinding factor elided for exposition. (This elision notation is used throughout this protocol description to simplify exposition.)	We denote the blinding $\cdot$ used in round $j$ as $a^* _j$
			* $\verifier$ responds with a challenge $c_j$.
2	NA	?	$\prover$ sets $g^\prime(X) = g(X, c_0, c_1, …, c_{n_a - 1}, \cdots)$.
3	NA	link	$\prover$ sends a commitment $R = \innerprod{\mathbf{r}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{r} \in \field^n$ are the coefficients of a randomly sampled univariate polynomial $r(X)$ of degree $n - 1$.	We denote the blinding $\cdot$ used as $r^*$
4	step_4	link	$\prover$ computes univariate polynomial $h(X) = \frac{g^\prime(X)}{t(X)}$ of degree $n_g(n - 1) - n$.
5	step_5	link	$\prover$ computes at most $n - 1$ degree polynomials $h_0(X), h_1(X), …, h_{n_g - 2}(X)$ such that $h(X) = \sum\limits_{i=0}^{n_g - 2} X^{ni} h_i(X)$.
6	step_6	link	$\prover$ sends commitments $H_i = \innerprod{\mathbf{h_i}}{\mathbf{G}} + [\cdot] W$ for all $i$ where $\mathbf{h_i}$ denotes the vector of coefficients for $h_i(X)$.	We denote the blinding $\cdot$ used in round $j$ as $h^* _j$
7	step_7	link(?)	$\verifier$ responds with challenge $x$ and computes $H^\prime = \sum\limits_{i=0}^{n_g - 2} [x^{ni}] H_i$.
8	step_8	link	$\prover$ sets $h^\prime(X) = \sum\limits_{i=0}^{n_g - 2} x^{ni} h_i(X)$.	$\prover$ sets $h^{\prime *} = \sum\limits_{i=0}^{n_g - 2} x^{ni} h_i^*$.
9	step_9	link	$\prover$ sends $r = r(x)$ and for all $i \in [0, n_a)$ sends $\mathbf{a_i}$ such that $(\mathbf{a_i})_j = a^\prime_i(\omega^{(\mathbf{p_i})_j} x)$ for all $j \in [0, n_e - 1]$.
10	step_10	link(?)	For all $i \in [0, n_a)$ $\prover$ and $\verifier$ set $s_i(X)$ to be the lowest degree univariate polynomial defined such that $s_i(\omega^{(\mathbf{p_i})_j} x) = (\mathbf{a_i})_j$ for all $j \in [0, n_e - 1)$.
11	step_11	link	$\verifier$ responds with challenges $x_1, x_2$ and initializes $Q_0, Q_1, …, Q_{n_q - 1} = \zero$.
			* Starting at $i=0$ and ending at $n_a - 1$ $\verifier$ sets $Q_{\sigma(i)} := [x_1] Q_{\sigma(i)} + A_i$.
			* $\verifier$ finally sets $Q_0 := [x_1^2] Q_0 + [x_1] H^\prime + R$.
12	step_12	link	$\prover$ initializes $q_0(X), q_1(X), …, q_{n_q - 1}(X) = 0$.	$\prover$ initializes $q^*_0, q^*_1, …, q^* _{n_q-1} = 0$.
			* Starting at $i=0$ and ending at $n_a - 1$ $\prover$ sets $q_{\sigma(i)} := x_1 q_{\sigma(i)} + a^\prime(X)$.	Starting at $i=0$ and ending at $n_a - 1$ $\prover$ sets $q^* _{\sigma(i)} := x_1 q^* _{\sigma(i)} + a^*_i$.
			* $\prover$ finally sets $q_0(X) := x_1^2 q_0(X) + x_1 h^\prime(X) + r(X)$.	$\prover$ finally sets $q^* _{0} := x_1^2 q^* _{0} + x_1 h^{\prime *} + r^*$
13	step_13	?	$\prover$ and $\verifier$ initialize $r_0(X), r_1(X), …, r_{n_q - 1}(X) = 0$.
			* Starting at $i = 0$ and ending at $n_a - 1$ $\prover$ and $\verifier$ set $r_{\sigma(i)}(X) := x_1 r_{\sigma(i)}(X) + s_i(X)$.
			* Finally $\prover$ and $\verifier$ set $r_0 := x_1^2 r_0 + x_1 h + r$ and where $h$ is computed by $\verifier$ as $\frac{g^\prime(x)}{t(x)}$ using the values $r, \mathbf{a}$ provided by $\prover$.
14	step_14	link	$\prover$ sends $Q^\prime = \innerprod{\mathbf{q^\prime}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{q^\prime}$ defines the coefficients of the polynomial $q^\prime(X) = \sum\limits_{i=0}^{n_q - 1} x_2^{n_q-1-i} \left( \frac {q_i(X) - r_i(X)} {\prod\limits_{j=0}^{n_e - 1} \left( X - \omega^{\left( \mathbf{q_i} \right)_j} x \right) } \right)$	The blinding $\cdot$ used here is denoted as $q^{\prime *}$.
15	step_15	link	$\verifier$ responds with challenge $x_3$.
16	step_16	link	$\prover$ sends $\mathbf{u} \in \field^{n_q}$ such that $\mathbf{u}_i = q_i(x_3)$ for all $i \in [0, n_q)$.
17	step_17	link	$\verifier$ responds with challenge $x_4$.
18	step_18	link	$\verifier$ sets $P = [x_4^{n_q}]Q’ + \sum\limits_{i=0}^{n_q - 1} [x_4^{n_q - 1 - i}] Q_i$ and $v = x_4^{n_q} \cdot \sum_{i=0}^{n_q - 1} \left(x_2^{n_q - 1 - i} \left(\frac{\mathbf{u}_i - r_i(x_3)}{\prod\ _{j=0}^{n_e - 1}(x_3 - \omega^{(\mathbf{q}_i)_j}x)}\right)\right) + \sum\ _{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \mathbf{u}_i$
19	step_19	link	$\prover$ sets $p(X) = x_4^{n_q} \cdot q’(X) + \sum\limits_{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \cdot q_i(X)$.	$\prover$ sets $p^* = x_4^{n_q} \cdot q’^* + \sum\limits_{i=0}^{n_q - 1} x_4^{n_q - 1 - i} \cdot q^*_i$.
20	step_20	link	$\prover$ samples a random polynomial $s(X)$ of degree $n - 1$ with a root at $x_3$ and sends a commitment $S = \innerprod{\mathbf{s}}{\mathbf{G}} + [\cdot] W$ where $\mathbf{s}$ defines the coefficients of $s(X)$.	The blinding $\cdot$ used here is denoted as $s^{*}$.
21	step_21	link	$\verifier$ responds with challenges $\xi, z$.
22	step_22	link	$\verifier$ sets $P^\prime = P - [v] \mathbf{G}_0 + [\xi] S$.
23	step_23	link	$\prover$ sets $p^\prime(X) = p(X) - p(x_3) + \xi s(X)$ (where $p(x_3)$ should correspond with the verifier’s computed value $v$).	$\prover$ sets $p^{\prime *} = s^* \cdot \xi + p^*$
24	step_24	link	Initialize $\mathbf{p^\prime}$ as the coefficients of $p^\prime(X)$ and $\mathbf{G^\prime} = \mathbf{G}$ and $\mathbf{b} = (x_3^0, x_3^1, …, x_3^{n - 1})$. $\prover$ and $\verifier$ will interact in the following $k$ rounds, where in the $j$th round starting in round $j=0$ and ending in round $j=k-1$ :
			* $\prover$ sends $L_j = \innerprod{\mathbf{p^\prime}\hi}{\mathbf{G^\prime}\lo} + [z \innerprod{\mathbf{p^\prime}\hi}{\mathbf{b}\lo}] U + [\cdot] W$ and $R_j = \innerprod{\mathbf{p^\prime}\lo}{\mathbf{G^\prime}\hi} + [z \innerprod{\mathbf{p^\prime}\lo}{\mathbf{b}\hi}] U + [\cdot] W$.	The blinding $\cdot$ used for $L_j$ is denoted $L_j^*$ and the blinding used for $R_j$ is denoted $R_j^*$
			* $\verifier$ responds with challenge $u_j$ chosen such that $1 + u_{k-1-j} x_3^{2^j}$ is nonzero.
			* $\prover$ and $\verifier$ set $\mathbf{G^\prime} := \mathbf{G^\prime}\lo + u_j \mathbf{G^\prime}\hi$ and $\mathbf{b} := \mathbf{b}\lo + u_j \mathbf{b}\hi$.
			* $\prover$ sets $\mathbf{p^\prime} := \mathbf{p^\prime}\lo + u_j^{-1} \mathbf{p^\prime}\hi$.
25	step_25	link	$\prover$ sends $c = \mathbf{p^\prime}_0$ and synthetic blinding factor $f$ computed from the elided blinding factors.	$\prover$ sets $f = p^{\prime *} + \sum_{j=0}^{k - 1}L_j^* \cdot u_j^{-1}+r_j^* \cdot u_j$
26	step_26	link	$\verifier$ accepts only if $\sum_{j=0}^{k - 1} [u_j^{-1}] L_j + P^\prime + \sum_{j=0}^{k - 1} [u_j] R_j = [c] \mathbf{G^\prime}_0 + [c \mathbf{b}_0 z] U + [f] W$.

Functions

add_polyx

Add two polynomials, return resulting polynomial

add_scalar_polyx

Add a scalar (constant) from a polynomial, return resulting polynomial

calculate_L_or_R 🔒

Auxilary function for computing L_j or R_j in step 24

check_equal_polyx 🔒

check_not_zero_polyx

Checks if all entries in a polynomial is 0

commit_polyx 🔒

Pedersen vector commitment

compute_vanishing_polynomial 🔒

Compute vanishing polynomial over n-order multiplicative subgroup H with root of unity omega

degree_polyx

Get the degree of a polynomial

divide_leading_terms

divide the leading terms of two polynomials, returning a single term (e.g. 5x^3) represented as a polynomial (helper function for divide_poly)

divide_polyx

Perform polynomial long division, returning the quotient and the remainder. The algorithm is from https://en.wikipedia.org/wiki/Polynomial_long_division.

eval_polyx

Evaluate a polynomial at point, return the evaluation

gen_one_polyx 🔒

gen_zero_polyx 🔒

inner_product 🔒

Inner product, between to equal length vectors of field elements

lagrange_basis

Finds the Lagrange basis for a set of points and a single evaluation point x This will produce a polynomial that evaluates to 1 at xand to 0 at all other x-values in the set points No other guarentees are given about the resulting polynomial

lagrange_polyx

Find lowest degree polynomial passing through a set points using legrange interpolation

msm 🔒

Multiscalar multiplicatoin, auxiliary function for Pedersen vector commitment

mul_polyx

Polynomial multiplication using sparse multiplication. This can be more efficient than operand scanning but also prone to side-channel attacks. Mostly copied from hacspec’s poly_mul

mul_scalar_polyx

Multiply a polynomial by a scalar, return resulting polynomial

multi_poly_with_x

Wrapper function for multiplying a polynomial with the indeterminate

multi_poly_with_x_pow

Wrapper function for multiplying a polynomial with the indeterminate multiple times

rotate_polyx 🔒

Rotate a polynomial

sigma 🔒

Implementation of the σ mapping from the protocol

step_4 🔒

Step 4 Beginning of the vanishing argument

step_5 🔒

Step 5 split polynomial of degree n_g(n-1)-n up into n_(g-2) polynomials of degree at most n-1

step_6 🔒

Step 6 commit to each h_i polynomial keeping them in the seq to peserve the power (i)

step_7 🔒

Step 7 Computes the sum from step 7 in the protocol description

step_8 🔒

Step 8 This functions calculates h’(X) from the h_i parts created in step 5 and the challenge x

step_9 🔒

Step 9 This functions returns r(x) and creates a seq filled with a_i from the second part of step 9

step_10 🔒

Step 10 This function initializes the s sequence of length n_a and fills it with polynomials of degree n_e-1 made with legrange interpolation

step_11 🔒

Step 11 Get the list of Q’s (Q_0, …, Q_{n_q - 1})

step_12 🔒

Step 12 Get the list of q’s (q_0, …, q_{n_q - 1}) and q_blinds (accumulated blindness)

step_13 🔒

Step 13 Get the list of r’s (r_0, …, r_{n_q - 1})

step_14 🔒

Step 14 Get the commitment Q’, poly q’ and the blindness used

step_15 🔒

Step 15 This function emulates sending a challenge.

step_16 🔒

Step 16 Get the u ∈ F^{n_q} vector

step_17 🔒

Step 17 This function emulates sending a challenge.

step_18 🔒

Step 18 Get P and the v

step_19 🔒

Step 19 Get the p(X) polynomial

step_20 🔒

Step 20 Get the commitment S and the blindness used

step_21 🔒

Step 21 Get the xi and z challenges. They have to be fed into hacspec, since there is no randomness.

step_22 🔒

Step 22 Get the P’ curve-point/group-element

step_23 🔒

Step 23 Get the p’(X) polynomial and p’ blindness

step_24 🔒

Step 24 Get G‘, p’, b, L, R, and {L,R} blinds

step_25 🔒

Step 25 Get the zeroth entry in p and synthetic blinding factor f

step_26 🔒

Step 26 Verifiers final check of the protocol

sub_polyx

Subtract two polynomials, return resulting polynomial

sub_scalar_polyx

Subtract a scalar (constant) from a polynomial, return resulting polynomial

trim_polyx

Trim a polynomial of trailing zeros (zero-terms) and return it

Type Definitions

CRS 🔒

Common Reference Struct

Polyx

A polynomial represented by its coefficient form, such that index i is the i’th term