Crate hacspec_halo2

source ·
Expand description

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.

StepSpecImpl.ProtocolNotes
1NA?$\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$.
2NA?$\prover$ sets $g^\prime(X) = g(X, c_0, c_1, …, c_{n_a - 1}, \cdots)$.
3NAlink$\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^*$
4step_4link$\prover$ computes univariate polynomial $h(X) = \frac{g^\prime(X)}{t(X)}$ of degree $n_g(n - 1) - n$.
5step_5link$\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)$.
6step_6link$\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$
7step_7link(?)$\verifier$ responds with challenge $x$ and computes $H^\prime = \sum\limits_{i=0}^{n_g - 2} [x^{ni}] H_i$.
8step_8link$\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^*$.
9step_9link$\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]$.
10step_10link(?)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)$.
11step_11link$\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$.
12step_12link$\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^*$
13step_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$.
14step_14link$\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 *}$.
15step_15link$\verifier$ responds with challenge $x_3$.
16step_16link$\prover$ sends $\mathbf{u} \in \field^{n_q}$ such that $\mathbf{u}_i = q_i(x_3)$ for all $i \in [0, n_q)$.
17step_17link$\verifier$ responds with challenge $x_4$.
18step_18link$\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$$
19step_19link$\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$.
20step_20link$\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^{*}$.
21step_21link$\verifier$ responds with challenges $\xi, z$.
22step_22link$\verifier$ sets $P^\prime = P - [v] \mathbf{G}_0 + [\xi] S$.
23step_23link$\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^*$
24step_24linkInitialize $\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$.
25step_25link$\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$
26step_26link$\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