# Soundness of music

This week's puzzle is all about soundness - the requirement of a proof system that it should not be possible to prove false statements.

Here, we use a toy proof system based on BCTV14 which is unsound.

## The proof system

This proof system is intended to allow a prover to show that a certain set of arithmetic constraints is satisfiable. Each constraint is of the form:

$$[a_1, \ldots, a_m]*[v_1, \ldots, v_m]^T + [a_1, \ldots, a_m]*[v_1, \ldots, v_m]^T = [c_1, \ldots, c_m]*[v_1, \ldots, v_m]^T$$

If you're familiar with the concept of rank-1 constraint systems, the format of an R1CS constraint may look similar. However, our constraints are much more limited: our kind of constraint system can only describe a very specific kind of arithmetic relations. In particular, it is not universal, since multiplication of variables is not possible. However, we can still prove statements such as 1+1+1+1=4.

### Constraints to polynomials

Each variable can be represented by a pair of polynomials, one which encodes every time that variable is an input in a constraint, and one polynomial which encodes every time that variable is an output in a constraint.

First, let's fix a domain $\omega_1, \ldots, \omega_m \in \mathbb{F}$, one field element for each constraint. (In general, these will be roots of unity; for our purposes, they only need to be distinct from each other)

Then the input polynomial $A_i$ for $v_i$ is defined as a polynomial of degree $n+1$ such that for all $j \in \{1,\ldots,n\}$, if

$$ A_i(\omega_j) = a_i$$

where $a_i$ comes from constraint $C_j$.

We can think of this polynomial as encoding the coefficients of the variable in each constraint.

Similarly, the output polynomial $C_i$ for each variable is defined as a polynomial of degree $n+1$ such that for all $j \in \{1,\ldots,n\}$

$$ C_i(\omega_j) = c_i$$

where $c_i$ comes from constraint $C_j$.

Together with the vanishing polynomial $Z = (x-\omega_1)\cdots(x-\omega_n)$, defined so $Z(\omega_j) = 0$ for all $j$, the polynomials $A_1, C_1, \ldots, A_m, C_m,Z$ define what we will call the "circuit" for our proving system.

### Trusted setup

Our succinct proving system requires a trusted setup.

Suppose we have $n$ constraints over $m$ variables, with polynomials $A_1, C_1, \ldots, A_m, C_m,Z$. We use the pairing-friendly BLS12-381 elliptic curve, with groups $\mathbb{G}_1, \mathbb{G}_2$.

Using the notation $[x]_1 = [x] G$ and $[x]_2 = [x] H$, where $G$ is a generator in $\mathbb{G}_1$ and $H$ is a generator in $\mathbb{G}_2$ and $[x] G$ refers to scalar multiplication by $x$.

| Trusted setup elements | |
| -------- | ------ |
| Powers of tau | $[1]_1, [\tau]_1, [\tau^2]_1, \ldots, [\tau^m]_1$ |
| Input polynomial commitments | $[\rho A_1(\tau)]_1, \ldots, [\rho A_m(\tau)]_1$ |
| $\alpha$ Input polynomial commitments| $[\alpha_I \rho A_1(\tau)]_1, \ldots, [\alpha_I \rho A_m(\tau)]_1$ |
| Output polynomial commitments | $[\rho C_1(\tau)]_1,\ldots, [\rho C_m(\tau)]_1$ |
| $\alpha$ Output polynomial commitments| $[\alpha_O \rho C_j(\tau)]_1, \ldots, [\alpha_O \rho C_m(\tau)]_1$ |
| $K$ | $\beta \rho (A_1(\tau) + C_1(\tau))]_1, \ldots, [\beta \rho (A_m(\tau) + C_m(\tau))]_1$ |
| $\alpha_I$ | $[\alpha_I]_2$ |
| $\alpha_O$ | $[\alpha_O]_2$ |
| $\gamma$ | $[\gamma]_2$ |
| $\beta\gamma$ | $[\beta \gamma]_2$ |
| Vanishing polynomial | $[\rho Z(\tau)]_2$ |

This trusted setup mostly copies the BCTV14 trusted setup, with minor modifications to the constraint format. In theory, the elements of the trusted setup help the verifier check that a proof is properly constructed.

For the puzzle, there was no multi-party computation ceremony, or any other special measures taken; random values of $\tau, \rho, \alpha_I, \alpha_O, \beta, \gamma$ are taken and the trusted setup values computed directly and honestly.

### Creating a proof

Suppose an assignment of values $x_1, \ldots, x_m$ to the variables $v_1, \ldots, v_m$ satisfies all constraints. Then equality:

$$ (x_1 A_1(\omega_1) + \ldots + x_m A_m(\omega_1)) + (x_1 A_1(\omega_1) + \ldots + x_m A_m(\omega_1)) = x_1 C_1(\omega_1) + \ldots + x_m C_m(\omega_1)$$

must hold, because it simplifies to:

$$[a_1, \ldots, a_m]*[x_1, \ldots, x_m]^T + [a_1, \ldots, a_m]*[x_1, \ldots, x_m]^T = [c_1, \ldots, c_m]*[x_1, \ldots, x_m]^T$$

which is simply constraint 1. Therefore, the polynomial equation:

$$ (x_1 A_1(x) + \ldots + x_m A_m(x)) + (x_1 A_1(x) + \ldots + x_m A_m(x)) = x_1 C_1(x) + \ldots + x_m C_m(x)$$

must hold over the entire domain $\omega_1, \ldots, \omega_n$. Further, this polynomial equation holds over the domain if and only if the assignment $x_1, \ldots, x_m$ actually satisfies every constraint; therefore, we can simply prove that this polynomial equation holds over this domain, and then conclude the constraint system is satisfied.

Rearranging everything to the left and denoting it as $P(x)$:

$$ P(x) = (x_1 A_1(x) + \ldots + x_m A_m(x)) + (x_1 A_1(x) + \ldots + x_m A_m(x)) - (x_1 C_1(x) + \ldots + x_m C_m(x)) $$

We get that $P(x) = 0$ for all $x \in \{\omega_1, \ldots, \omega_n\}$. Therefore, $P(x)$ is divisible by the vanishing polynomial $Z(x)$; put another way, there exists a polynomial $H(x)$ such that $P(x) = H(x) * Z(x)$.

Therefore, if we compute a polynomial commitment $\pi_H = [P(\tau)/Z(\tau)]_1$, a verifier should be able to confirm that $P(x) = 0$ over the correct domain.

We also compute some additional proof elements, which encode the private inputs and also help the verifier verify this fact:

$$ \pi_I = \sum_{x_i \text{ is private}} x_i [\rho A_i(\tau)] $$
$$ \pi_I' = \sum_{x_i \text{ is private}} x_i [\alpha_I \rho A_i(\tau)] $$
$$ \pi_O = \sum_{x_i} x_i [\rho C_i(\tau)] $$
$$ \pi_O' = \sum_{x_i } x_i [\alpha_O \rho O_i(\tau)] $$
$$ \pi_K = \sum_{x_i} [\beta \rho (A_1(\tau) + C_1(\tau))]_1, \ldots, [\beta \rho (A_m(\tau) + C_m(\tau))]_1 $$

The final proof is $(\pi_I, \pi_I', \pi_O, \pi_O', \pi_K, \pi_H)$

### Verifier

The given verifier takes in the public inputs $x_1, \ldots, x_p$. The public inputs get encoded into:

$$ \pi_{PI} = \sum_{x_i \text{ is public}} x_i [\rho A_i(\tau)] $$

The verifier checks, where $e(\cdot, \cdot)$ is the pairing operation:

$$ e(\pi_I', H) = e(\pi_{I}, [\alpha_I]_2)$$
$$ e(\pi_O', H) = e(\pi_{O}, [\alpha_O]_2)$$
$$ e(\pi_K, [\gamma]_2) = e(\pi_{PI} + \pi_I + \pi_O, [\beta\gamma]_2) $$
$$ e(\pi_{PI} + \pi_{I} + \pi_{PI} + \pi_{I} - \pi_{O}) = e(\pi_H, [\rho Z(\tau)]_2)$$

The final pairing effectively checks the condition that $P(x) = H(x) Z(x)$ as required.

## Soundness Bugs

The proof system in this puzzle has two soundness bugs; the verifier accepts proofs even when the constraint system is unsatisfiable with given public inputs.

### Bug 1

The first bug is an implementation bug. Recall that for variable $v_i$, the polynomials $A_i$ and $C_i$ were defined as a polynomial of degree $n+1$ with certain values on a domain. In the puzzle, $A_i$ and $C_i$ were interpolated without regard to the resulting degree, which meant that $A_i$ sometimes was degenerate. When this happens for a public input variable, the verifier may ignore this public input.

The correct fix is to ensure that every polynomial is actually degree $n+1$. This can be achieved by taking the polynomial mod $Z(x)$ and adding $Z(x)$, since $Z(x)$ is known to be exactly degree $n+1$. Since zero-knowledge blinding wasn't necessary for this puzzle, this necessary step was omitted.

### Bug 2

The second bug is a conceptual bug, based on the one that occurs in BCTV14. The trusted setup includes terms:

$$[\alpha_I \rho A_1(\tau)]_1, \ldots, [\alpha_I \rho A_p(\tau)]_1$$

which are not used anywhere by the prover or verifier.

However, these elements can be used to alter any valid proof for public input $x_1, \ldots, x_p$ to work for an arbitrary public input:

$$\eta_I = \pi_I + \sum_{i=0}^p (x_i - x_i') [\rho A_i(\tau)]_1$$

$$\eta_I' = \pi_I' + \sum_{i=0}^p (x_i - x_i') [\alpha_I \rho A_i(\tau)]_1$$

The proof $(\eta_I, \eta_I', \pi_O, \pi_O', \pi_K, \pi_H)$ will verify against the arbitrarily-chosen public input $x_1', \ldots, x_p'$.

The fix for this bug is to remove the unnecessary elements of the trusted setup.