---
# System prepended metadata

title: Nova and its Implementation：A Deep Dive
tags: [IVC, zkSNARK, Folding, Nova]

---

# Nova and its Implementation：A Deep Dive

> [TOC]

This article will analysis [Nova's code implementation](https://github.com/microsoft/Nova), and explain how  the code works based on the relevant papers.


 I will first deduce the formula according to the papers, until it corresponds to the code, and then explain the code, which will be clearer and easier to understand.

As of August 30, 2023, I refer to the code corresponding to the [latest commit](https://github.com/microsoft/Nova/tree/bd56514f3a5364553a31979aa1c1c480aa9e20cd), and considering that the code comments should be located near the code as much as possible, so I created the [Nova-Analysis](https://github.com/zkp-learning/Nova-Analysis) repo to save the code comments. When there are code comments, I will prompt in this article

## Code structure

```rs=
// private modules
mod bellpepper;
mod circuit;
mod constants;
mod nifs;
mod r1cs;

// public modules
pub mod errors;
pub mod gadgets;
pub mod provider;
pub mod spartan;
pub mod traits;
```

According to its [lib.rs](https://github.com/microsoft/Nova/blob/6a6308ebcaff3a7c6d1245bd3b4f10355afb588c/src/lib.rs), we know that Nova has these different mods. we explain these mods below.

## r1cs mod
Here is a example on how r1cs works.

### R1CS

#### a example
*the relation:*

private inputs $\{w_1, w_2, w_3, w_4\}$ and public output $x_1$ satisfy the following constraint relation:
$$(w_1 + w_2)*(w_3*w_4) = x_1$$

Let's try to represent this relation in terms of R1CS.

*the circuit:*

![](https://hackmd.io/_uploads/HJ8Ur5YT3.png)

*the R1CS struct:*

let $Z = \begin{bmatrix} w_1 \\ w_2 \\ w_3 \\ w_4 \\ w_5 \\ x_1 \\ 1 \end{bmatrix}$, According to the definition in Nova $Z = \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix}$, where $W$ represents **witness**, including `private input` and `intermediate values`, that is $w_i$ here. $\mathsf{x}$ represents `public inputs` and `outputs`, that is $x_1$ here. If there are constants in the relation, the `1` can be used to encode them.

Write the $A \ B \ C$ matrix according to the circuit:

for multiplication gate `#1`, the **left input** is $(w_1 + w_2) = \begin{bmatrix} 1 & 1 & 0 & 0 & 0 & 0 & 0 \end{bmatrix}\cdot \begin{bmatrix} w_1 \\ w_2 \\ w_3 \\ w_4 \\ w_5 \\ x_1 \\ 1 \end{bmatrix}$ 

for multiplication gate `#2`, the **left input** is $w_3 = \begin{bmatrix} 0 & 0 & 1 & 0 & 0 & 0 & 0 \end{bmatrix}\cdot \begin{bmatrix} w_1 \\ w_2 \\ w_3 \\ w_4 \\ w_5 \\ x_1 \\ 1 \end{bmatrix}$ 

So, we get the **left input** matrix:

$$A =\begin{bmatrix} 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 & 0 & 0 & 0 \end{bmatrix} $$ 

Matrix $A$ consists of the **left input** of the **all** multiplication gates, and its number of rows is equal to the number of multiplication gates, and its number of columns is equal to the length of vector $Z$.

Using the same approach, we can get the **right input** matrix:

$$B = \begin{bmatrix} 0 & 0 & 0 & 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 & 0 & 0 & 0 \end{bmatrix}$$ 

Matrix $B$ consists of the **right input** of the **all** multiplication gates. Its shape is the same with $A$.

$$C = \begin{bmatrix} 0 & 0 & 0 & 0 & 0 & 1 & 0\\ 0 & 0 & 0 & 0 & 1 & 0 & 0 \end{bmatrix}$$

Matrix $C$ consists of the **output** of the **all** multiplication gates. Its shape is the same with $A$.

Let's check:

$$\begin{align*} (A \cdot Z) \circ (B·Z) &= (\begin{bmatrix} 1 & 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 1 & 0 & 0 & 0 & 0 \end{bmatrix} \cdot  \begin{bmatrix} w_1 \\ w_2 \\ w_3 \\ w_4 \\ w_5 \\ x_1 \\ 1 \end{bmatrix} ) \circ (\begin{bmatrix} 0 & 0 & 0 & 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 1 & 0 & 0 & 0 \end{bmatrix} \cdot \begin{bmatrix} w_1 \\ w_2 \\ w_3 \\ w_4 \\ w_5 \\ x_1 \\ 1 \end{bmatrix}) \\ &= \begin{bmatrix} w_1 + w_2 \\ w_3 \end{bmatrix} \circ \begin{bmatrix} w_5 \\ w_4 \end{bmatrix} = \begin{bmatrix} (w_1 + w_2)w_5 \\ w_3w_4 \end{bmatrix} = \begin{bmatrix} x_1 \\ w_5 \end{bmatrix} = C\cdot Z \end{align*}$$


#### R1CS Definition

According to **Definition 10 (R1CS)** in [Nova paper](https://ia.cr/2021/370):
>Consider a finite field $\mathbb{F}$. Let the public parameters consist of size bounds $m, n, l \in \mathbb{N}$ where $m > l$. The R1CS structure consists of sparse matrices $A, B, C \in \mathbb{F}^{m\times m}$ with at most $n = \Omega{(m)}$ non-zero entries in each matrix. An instance $\mathsf{x} \in \mathbb{F}^l$ consists of public inputs and outputs and is satisfied by a witness $W \in \mathbb{F}^{m−l−1}$ if $(A \cdot Z) \circ (B \cdot Z)=C \cdot Z$, where $Z=(W,\mathsf{x},1)$.

#### R1CS's attempt:

There are different vector $Z_1$ and $Z_2$ for different instance witness pairs $(\mathsf{x_1}, W_1)$, $(\mathsf{x_2}, W_2)$ and so on, which need to be verified repeatedly $(A \cdot Z_i) \circ (B·Z_i)=C·Z_i$.

It can be seen that matrix $A, B, C$ representing constraints will not change. What Folding needs to solve is to reduce the number of verifications $(A \cdot Z_i) \circ (B·Z_i)=C·Z_i$ by merging different instances $Z_i$

So, $Z = \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix}$, choose a random value $r \in \mathbb{F}$, let 

$$\begin{align*} \mathsf{x} & \leftarrow \mathsf{x}_1 + r \cdot \mathsf{x}_2 \\ W & \leftarrow W_1 + r \cdot W_2 \end{align*}$$

failed because $Z \neq Z_1 + r\cdot Z_2$

### Relaxed R1CS
#### Relaxed R1CS Definition
According to **Definition 11 (Relaxed R1CS)** in [Nova paper](https://ia.cr/2021/370):

> Consider a finite field $\mathbb{F}$. Let the public parameters consist of size bounds $m, n, l \in \mathbb{N}$ where $m > l$. The relaxed R1CS structure consists of sparse matrices $A, B, C \in \mathbb{F}^{m \times m}$ with at most $n = \Omega{(m)}$ non-zero entries in each matrix. A relaxed R1CS instance consists of an error vector $E \in \mathbb{F}^m$, a scalar $u \in \mathbb{F}$, and public inputs and outputs $x \in \mathbb{F}^l$. An instance $(E,u,\mathsf{x})$ is satisfied by a witness $W \in \mathbb{F}^{m−l−1}$ if $(A \cdot Z) \circ (B \cdot Z) = u \cdot (C \cdot Z) + E$, where $Z = (W, \mathsf{x}, u)$.



#### Relaxed R1CS's attempt:

From the definition, we can get: $$\begin{align*} (A\cdot Z_i) \circ (B\cdot Z_i) & = u_i\cdot(C\cdot Z_i) + E_i \\ Z & = (W, \mathsf{x}, u) \end{align*}$$

Choose a random value $r \in \mathbb{F}$, if we perform a linear combination of two instances in the following way:

$$\begin{align*} \mathsf{x} & \leftarrow \mathsf{x_1} + r \cdot \mathsf{x_2} \\ W & \leftarrow W_1 + r \cdot W_2 \\ u & \leftarrow u_1 + r\cdot u_2 \\ E & \leftarrow E_1 + r\cdot(AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1 - u_1 CZ_2 - u_2 CZ_1) + r^2 \cdot E_2\end{align*}$$

We can deduce the following result: $Z = (W, \mathsf{x}, u) = \begin{bmatrix} W \\ \mathsf{x} \\ u \end{bmatrix} =  \begin{bmatrix} W_1 + rW_2 \\  \mathsf{x}_1 + r\mathsf{x}_2  \\ u_1 + r u_2 \end{bmatrix}  =  Z_1 + r\cdot Z_2$.
$$\begin{align*} AZ \circ BZ &= A(Z_1 + r\cdot Z_2) \circ B(Z_1 + r\cdot Z_2) \\ &= AZ_1 \circ BZ_1 + r \cdot(AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1) + r^2 \cdot AZ_2 \circ BZ_2 \\ &= u_1\cdot CZ_1 + E_1 + r \cdot (AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1) + r^2 \cdot (u_2 \cdot CZ_2 + E_2) \\ &= u_1\cdot CZ_1 + ru_2 \cdot CZ_1 - ru_2\cdot CZ_1 + E_1 + r \cdot (AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1) + r^2 \cdot (u_2 \cdot CZ_2 + E_2) + ru_1CZ_2 - ru_1CZ_2 \\ &= (u_1 + ru_2)CZ_1 + E_1 -ru_2CZ_1 + r(AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1) + (u_1+ ru_2)rCZ_2 + r^2E_2 - ru_1CZ_2 \\ &=(u_1 + ru_2)C(Z_1 + rZ_2) + r(AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1 - u_2CZ_1 -u_1CZ_2) + E_1 + r^2E_2 \\ &= uCZ + E  \end{align*}$$

Success! we only need to verify whether $Z$ satisfies the constraints $(A\cdot Z) \circ (B\cdot Z)  = u\cdot(C\cdot Z) + E$ to check whether both $Z_1$ and $Z_2$ satisfy the constraints.

### Committed Relaxed R1CS
#### Committed Relaxed R1CS Definition

According to **Definition 12 (Committed Relaxed R1CS)** in [Nova paper](https://ia.cr/2021/370):

> Consider a finite field $\mathbb{F}$ and a commitment scheme $\mathsf{Com}$ over $\mathbb{F}$. Let the public parameters consist of size bounds $m, n, l \in \mathbb{N}$ where $m > l$, and commitment parameters $\mathsf{pp}_E$ and $\mathsf{pp}_W$ for vectors of size $m$ and $m−l−1$ respectively. The committed relaxed R1CS structure consists of sparse matrices $A, B, C \in \mathbb{F}^{m×m}$ with at most $n = \Omega{(m)}$ non-zero entries in each matrix. A committed relaxed R1CS instance is a tuple $(\overline{E},u,\overline{W},\mathsf{x})$, where $\overline{E}$ and $\overline{W}$ are commitments, $u \in \mathbb{F}$, and $x \in \mathbb{F}^l$ are public inputs and outputs. An instance $(\overline{E},u,\overline{W},\mathsf{x})$ is satisfied by a witness $(E,r_E,W,r_W ) \in (\mathbb{F}^m,\mathbb{F},\mathbb{F}^{m−l−1},\mathbb{F})$ if $\overline{E} = \mathsf{Com}(\mathsf{pp}_E,E,r_E),\overline{W} =\mathsf{Com}(\mathsf{pp}_W,W,r_W)$, and $(A\cdot Z)\circ (B\cdot Z)=u\cdot(C\cdot Z)+E$, where $Z = (W, \mathsf{x}, u)$.

For more introduction to the commitment, please refer to the [wiki](https://en.wikipedia.org/wiki/Commitment_scheme).

### A Folding Scheme for Committed Relaxed R1CS
According to **Construction 1 (A Folding Scheme for Committed Relaxed R1CS)** in [Nova paper](https://ia.cr/2021/370):

> Consider a finite field $\mathbb{F}$ and a succinct, hiding, and homomorphic commitment scheme $\mathsf{Com}$ over $\mathbb{F}$. We define the generator and the encoder as follows.
– $\mathcal{G}(1^{\lambda}) \rightarrow \mathsf{pp}$: output size bounds $m,n,l \in \mathbb{N}$, and commitment parameters $\mathsf{pp}_E$ and $\mathsf{pp}_W$ for vectors of size $m$ and $m − l − 1$ respectively.
– $\mathcal{K}(\mathsf{pp},(A,B,C)) \rightarrow (\mathsf{pk,vk})$: output $\mathsf{pk} \leftarrow (\mathsf{pp},(A,B,C))$ and $\mathsf{vk} \leftarrow \bot$.
>
> The verifier $\mathcal{V}$ takes two committed relaxed R1CS instances $(\overline{E_1},u_1,\overline{W_1},\mathsf{x}_1)$ and $(\overline{E_2},u_2,\overline{W_2},\mathsf{x}_2)$. The prover $\mathcal{P}$, in addition to the two instances, takes witnesses to both instances, $(E_1, r_{E_1}, W_1, r_{W_1})$ and $(E_2, r_{E_2}, W_2, r_{W_2})$. Let $Z_1 = (W_1, \mathsf{x}_1, u_1)$ and $Z_2 = (W_2, \mathsf{x}_2, u_2)$. The prover and the verifier proceed as follows. 
>1. $\mathcal{P}:$ Send $\overline{T} := \mathsf{Com}(\mathsf{pp}_E,T,r_T)$, wherer $r_T \leftarrow _R\mathbb{F}$ and with cross term
$$T =AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1 − u_1 \cdot CZ_2 - u_2 \cdot CZ_1.$$
> 2. $\mathcal{V}:$ Sample and send challenge $r ← _r\mathbb{F}$.
> 3. $\mathcal{V, P}:$ Output the folded instance $(\overline{E}, u, \overline{W} , \mathsf{x})$ where
$$\begin{align*} \overline{E} & \leftarrow \overline{E_1} + r\cdot \overline{T} + r^2 \cdot \overline{E_2} \\  u & \leftarrow u_1 +r\cdot u_2 \\ \overline{W} & \leftarrow \overline{W_1} + r \cdot \overline{W_2} \\ \mathsf{x} & \leftarrow \mathsf{x}_1 + r \cdot \mathsf{x}_2 \end{align*}$$
> 4. $\mathcal{P}:$ Output the folded witness $(E, r_E, W, r_W)$, where
$$\begin{align*} E & \leftarrow E_1 +r\cdot T + r^2 \cdot E_2 \\ r_E & \leftarrow r_{E_1} +r\cdot r_T +r^2 \cdot r_{E_2} \\  W & \leftarrow W_1 + r\cdot W_2 \\
r_W & \leftarrow r_{W_1} +r\cdot r_{W_2} \end{align*}$$

### code

Next, we analyze the code of `r1cs mod` according to the above theory, located in `src/r1cs.rs`.

#### R1CS struct

```rs=
pub struct R1CS<G: Group> { 
  _p: PhantomData<G>,
}
```
This structure only retains a generic G, which needs to implement the methods in the Group trait, and has no valid data other than that.

There is a method for `R1CS`:
* `commitment_key`, for a given circuit(certain $A, B, C$), it will call Group's `CE` type's `setup` method to get a `CommitmentKey` and return it.

#### R1CSShape struct
```rs=
pub struct R1CSShape<G: Group> {
  pub(crate) num_cons: usize,
  pub(crate) num_vars: usize,
  pub(crate) num_io: usize,
  pub(crate) A: Vec<(usize, usize, G::Scalar)>,
  pub(crate) B: Vec<(usize, usize, G::Scalar)>,
  pub(crate) C: Vec<(usize, usize, G::Scalar)>,
}
```

`R1CSShape` means matrix $A, B, C,$ that is, circuit constraints. 

There are some [fields](https://en.wikipedia.org/wiki/Field_(computer_science)) in this structure:
* `num_cons`: Length of a column in the matrix, also the number of multiplication gates.
* `num_vars`: Length of witness $W$, and according to the previous, it equals $m-l-1$.
* `num_io`: Length of public input and output $x$, and according to the previous, it equals $l$. 
* `A, B, C`: Represent the position and value of the non-zero value in the sparse matrix.


We can get length of a column in the matrix by `num_vars + num_io + 1`, so the three matrices $A, B, C$ are completely determined by struct `R1CSShape`.

There are some methods for `R1CSShape`:
* `new()`: Receive `num_cons`, `num_vars`, `num_io`, `A`, `B`, `C` as parameters, then do some checks，and return `R1CSShape`. The [checks's comments](https://github.com/zkp-learning/Nova-Analysis).
* `check_regular_shape()`: Checks regularity conditions on the R1CSShape, required in Spartan-class SNARKs. The [checks's comments](https://github.com/zkp-learning/Nova-Analysis).
* `multiply_vec()`: Calculate and return them: $(A\cdot Z, B\cdot Z, C \cdot Z)$
* `is_sat_relaxed()`: Check $A\cdot Z \circ B \cdot Z = u\cdot C\cdot Z + E$, $\overline{W} = \mathsf{Com}(\mathsf{pp}_W, W, ck)$ and $\overline{E} = \mathsf{Com}(\mathsf{pp}_E, E, ck)$. $\overline{W}$ and $\overline{E}$ used the same commitment key.
* `is_sat()`: pass CommitmentKey, [R1CSInstance](#R1CSInstance-struct) and [R1CSWitness](#R1CSWitness-struct) as parameters, check $A \cdot \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix} \circ B \cdot \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix} = C \cdot \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix}$ and $\overline{W} = \mathsf{Com}(\mathsf{pp}_W, W, ck)$
* `commit_T()`: $\overline{T} := \mathsf{Com}(\mathsf{pp}_W, T,ck_T)$, wherer $r_T \leftarrow _R\mathbb{F}$ and with cross term
$T =AZ_1 \circ BZ_2 + AZ_2 \circ BZ_1 − u_1 \cdot CZ_2 - u_2 \cdot CZ_1$. first calculate $Z_1$ and $Z_2$ by $Z_i = (W_i, u_i, x_i)$
* `pad()`: make `witness.len() = M.colume.len() = 2^k`, required in Spartan-class SNARKs.


#### R1CSWitness struct
```rs=
pub struct R1CSWitness<G: Group> {
  W: Vec<G::Scalar>,
}
```

`R1CSWitness` means $W$, Witness of R1CS, which is a vector of length $m-l-1$, the $W$ in $Z = \begin{bmatrix} W \\ \mathsf{x} \\ 1 \end{bmatrix}$

There are some methods for `R1CSWitness`:
* `new()`: Pass in an `R1CSShape` example S and a vector W. Because creating a Witness needs to know which R1CS's witness it is, and it will check that the length of W is equal to S.num_vars.
* `commit()`: Calculate $\overline{W} = \mathsf{Com}(\mathsf{pp}_W,W,r_W)$. And the parameter `ck`, a `CommitmentKey`, means $r_W$.

#### R1CSInstance struct
```rs=
pub struct R1CSInstance<G: Group> {
  pub(crate) comm_W: Commitment<G>,
  pub(crate) X: Vec<G::Scalar>,
}
```

`R1CSInstance` means $(\overline{W}, \mathsf{x})$

There are a method for `R1CSInstance`:
* `new()`: $(\overline{W}, \mathsf{x}, 1)$ and `A.num_io should == x.len()`

#### RelaxedR1CSWitness struct
```rs=
pub struct RelaxedR1CSWitness<G: Group> {
  pub(crate) W: Vec<G::Scalar>,
  pub(crate) E: Vec<G::Scalar>,
}
```

`RelaxedR1CSWitness` means $(W, E)$.

There are some methods for `RelaxedR1CSWitness`:
* `default()`, use zero value to init the $W, E$.
* `from_r1cs_witness()`, use zero value to init the $E$, and get the $W$ from parameter.
* `commit()`, return $\overline{W}/ \overline{E} = \mathsf{Com}(\mathsf{pp}_{W/E}, W/E, ck)$, with the same comitment key `ck`.
* `fold()`, Calculate $W = W_1 + r\cdot W_2$ and $E = E_1 + r \cdot T$, used the same `r`. Why is not $E = E_1 + r\cdot T + r^2 \cdot E_2$ here? since $E_2$ of parameter's `R1CSWitness` is $\vec{0}$, $r^2 \cdot E_2$ can be omitted.
* `pad()`: Pads the provided witness to the correct length.


#### RelaxedR1CSInstance struct
```rs=
pub struct RelaxedR1CSInstance<G: Group> {
  pub(crate) comm_W: Commitment<G>,
  pub(crate) comm_E: Commitment<G>,
  pub(crate) X: Vec<G::Scalar>,
  pub(crate) u: G::Scalar,
}
```

`RelaxedR1CSInstance` means $(\overline{W}, \overline{E}, \mathsf{x}, u)$

There are some methods for `RelaxedR1CSInstance`:
* `default()`: Produces a default `RelaxedR1CSInstance` given `R1CSGens` and `R1CSShape`
* `from_r1cs_instance()`: Initializes a new `RelaxedR1CSInstance` from an `R1CSInstance`, the `u` use `one` value
* `from_r1cs_instance_unchecked()`: Initializes a new `RelaxedR1CSInstance` from an `R1CSInstance`, the `u` use `one` value
* `fold()`: Folds an incoming `R1CSInstance` into the current one, calculate $\mathsf{x} = \mathsf{x}_1 + r \cdot \mathsf{x_2}$ and $\overline{W} = \overline{W_1} + r\cdot \overline{W_2}$ and $\overline{E} = \overline{E_1} + r \cdot \overline{T}$ and $u = u_1 + r$ used the same `r`. Why is not $\overline{E} = \overline{E_1} + r\cdot \overline{T} + r^2 \cdot \overline{E_2}$ here? Since $\overline{E_2}$ of parameter's `R1CSInstance` is $\mathcal{O}$, $r^2 \cdot \overline{E_2}$ can be omitted. and why is it $u = u_1 + r \cdot u_2$? Since the $u_2$ from `R1CSInstance` is `1` in default.

## nifs mod

### A Non-Interactive Folding Scheme
According to **Construction 2 (A Non-Interactive Folding Scheme)** in Nova paper:

> We achieve non-interactivity in the random oracle model using the strong Fiat-Shamir transform. Let $\rho$ denote a random oracle sampled during parameter generation and provided to all parties. Let $(\mathsf{G, K, P, V})$ represent our interactive folding scheme (Construction 1). We construct a non-interactive folding scheme $\mathcal{(G, K, P, V)}$ as follows:
– $\mathcal{G}(1^{\lambda})$: output $\mathsf{pp} \leftarrow \mathsf{G}(1^{\lambda})$.
– $\mathcal{K}(\mathsf{pp}, (A, B, C))$: $\mathsf{vk} \leftarrow \rho (\mathsf{pp}, \mathsf{s})$ and $\mathsf{pk} \leftarrow (\mathsf{pp}, (A, B, C), \mathsf{vk})$; output $(\mathsf{vk}, \mathsf{pk})$.
– $\mathcal{P}(\mathsf{pk}, (u_1, w_1), (u_2, w_2))$: runs $\mathsf{P}((\mathsf{pk.pp}, \mathsf{pk.}(A, B, C))$ to retrieve its first message $\overline{T}$ , and sends $\overline{T}$ to $\mathcal{V}$; computes $r \leftarrow \rho(\mathsf{vk}, u_1, u_2, \overline{T})$, forwards this to $\mathsf{P}$, and outputs the resulting output.
– $\mathcal{V}(\mathsf{vk},u_1,u_2,\overline{T})$: runs $\mathsf{V}$ with $\overline{T}$ as the message from the prover and with randomness $r \leftarrow \rho(\mathsf{vk}, u_1, u_2, \overline{T})$, and outputs the resulting output.


**Assumption 1 (RO instantiation)**:
> Construction 2 is a non-interactive folding scheme that satisfies completeness, knowledge soundness, and zero-knowledge in the standard model when $\rho$ is instantiated with a cryptographic hash function.

### code
Next, we analyze the code of nifs mod, located in src/nifs.rs.

#### NIFS struct
```rs=
pub struct NIFS<G: Group> {
  pub(crate) comm_T: CompressedCommitment<G>,
}
```

This structure contains $\overline{T}$, where $$T = A \cdot Z_1 \circ B \cdot Z_2 + A \cdot Z_2 \circ B \cdot Z_1 - u_1 \cdot C \cdot Z_2 - u_2 \cdot C\cdot Z_1, \\ \overline{T} = \mathsf{Com}(\mathsf{pp}_E, T, r_E)$$ and there are two methods impl for `NISF`:

* `prove()`: Given `ck`, `ro_consts`, `pp_digest`, `S`$(A, B, C)$, `U1`$(\overline{W_1}, \overline{E_1}, \mathsf{x_1}, u_1)$, `W1`$(W_1, E_1)$, `U2`$(\overline{W_2}, \mathsf{x}_2)$, `W2`($W_2$), return `NIFS` , $(W, E)$ and $(\overline{W}, \overline{E}, \mathsf{x}, u)$, and the random `r = ρ(ro_consts, pp_digest, U1, U2, comm_T)`
* `verify()`: Given `ro_consts`, `pp_digest`, `U1`$(\overline{W_1}, \overline{E_1}, \mathsf{x_1}, u_1)$, `U2`$(\overline{W_2}, \mathsf{x_2})$, get $\overline{T}$ from `self.comm_T`, calculate random `r = ρ(ro_consts, pp_digest, U1, U2, comm_T)`, return the new `U = U1.fold(U2)`.

## constants mod
```rs=
pub(crate) const NUM_CHALLENGE_BITS: usize = 128;
pub(crate) const NUM_HASH_BITS: usize = 250;
pub(crate) const BN_LIMB_WIDTH: usize = 64;
pub(crate) const BN_N_LIMBS: usize = 4;
pub(crate) const NUM_FE_WITHOUT_IO_FOR_CRHF: usize = 17;
pub(crate) const NUM_FE_FOR_RO: usize = 24;
```

* `NUM_CHALLENGE_BITS`: Valid output bits when a random oracle is used to generate challenge value `r`.
* `NUM_HASH_BITS`: Valid output bits when a random oracle is used to generate **hash**
* `BN_LIMB_WIDTH` and `BN_N_LIMBS`: Use 4 * 64 bits to represent 256 bits.
* `NUM_FE_WITHOUT_IO_FOR_CRHF`
* `NUM_FE_FOR_RO`


## circuit mod

According to **Construction 3 (IVC)** in Nova paper:

> Let $\mathsf{NIFS} = (\mathsf{G}, \mathsf{K}, \mathsf{P}, \mathsf{V})$ be the non-interactive folding scheme for committed relaxed R1CS (Construction 2). Consider a polynomialtime function F that takes non-deterministic input, and a cryptographic hash function $\mathsf{hash}$. We define our augmented function $F^{\prime}$ as follows (all arguments to $F^{\prime}$ are taken as non-deterministic advice):
>
> $\underline{F^{\prime}(\mathsf{vk}, \mathsf{U}_i, \mathsf{u}_i, (i, z_0, z_i), w_i, \overline{T}) \rightarrow \mathsf{x}:}$
> 
> If $i$ is $0$, output $\mathsf{hash}(\mathsf{vk}, 1, z_0, F(z_0, w_i), \mathsf{u}_\bot)$;
>
> otherwise,
> $\quad(1)$ check that $\mathsf{u}_i.\mathsf{x} = \mathsf{hash}(\mathsf{vk}, i, z_0, z_i, \mathsf{U}_i)$, where $\mathsf{u}_i.\mathsf{x}$ is the public IO of $\mathsf{u}_i$,
> $\quad(2)$ check that $(\mathsf{u}_i.\overline{E}, \mathsf{u}_i.u) = (\mathsf{u}_\bot.\overline{E}, 1)$,
$\quad(3)$ compute $\mathsf{U}_{i+1} \leftarrow \mathsf{NIFS.V}(\mathsf{vk, U, u}, \overline{T})$, and
$\quad(4)$ output $\mathsf{hash}(\mathsf{vk}, i + 1, z_0, F (z_i, w_i), \mathsf{U}_{i+1})$.
> 
> $\quad$ Because $F^{\prime}$ can be computed in polynomial time, it can be represented as a committed relaxed R1CS structure $\mathsf{s}_{F^{\prime}}$. Let
$$(\mathsf{u}_{i+1}, \mathsf{w}_{i+1}) \leftarrow \mathsf{trace}(F^\prime, (\mathsf{vk}, \mathsf{U}_i, \mathsf{u}_i, (i, z_0, z_i), w_i, \overline{T}))$$
> denote the satisfying committed relaxed R1CS instance-witness pair $(\mathsf{u}_{i+1},\mathsf{w}_{i+1})$ for the execution of $F^\prime$ on non-deterministic advice $(\mathsf{vk},\mathsf{U}_i,\mathsf{u}_i,(i,z_0,z_i), w_i,\overline{T})$.
$\quad$ We define the IVC scheme $(\mathcal{G}, \mathcal{K}, \mathcal{P}, \mathcal{V})$ as follows.
> 
> $\underline{\mathcal{G}(1^\lambda) \rightarrow \mathsf{pp}}$: Output $\mathsf{NIFS.G}(1^\lambda)$.
> 
> $\underline{\mathcal{K}(\mathsf{pp}, F) \rightarrow (\mathsf{pk}, \mathsf{vk})}$:
>
> Compute $(\mathsf{pk_{fs}}, \mathsf{vk_{fs}}) \leftarrow \mathsf{NIFS.K}(\mathsf{pp}, \mathsf{s}_{F^\prime})$ and output $(\mathsf{pk, vk}) \leftarrow ((F, \mathsf{pk_{fs}}), (F, \mathsf{vk_{fs}}))$. 
> 
> $\underline{\mathcal{P}(\mathsf{pk}, (i, z_0, z_i), w_i, \Pi_i) \rightarrow \Pi_{i+1}}$: 
>
> Parse $\Pi_i$ as $((\mathsf{U}_i, \mathsf{W}_i), (\mathsf{u}_i, \mathsf{w}_i))$ and then
$\quad(1)$ if $i$ is $0$, compute $(\mathsf{U}_{i+1},\mathsf{W}_{i+1},\overline{T}) \leftarrow (\mathsf{u}_\bot,\mathsf{w}_\bot, \mathsf{u}_\bot.\overline{E})$;
$\qquad$ otherwise, compute $(\mathsf{U}_{i+1},\mathsf{W}_{i+1},\overline{T}) \leftarrow \mathsf{NIFS.P}(\mathsf{pk},(\mathsf{U}_i,\mathsf{W}_i),(\mathsf{u}_i,\mathsf{w}_i))$, 
$\quad(2)$ compute $(\mathsf{u}_{i+1}, \mathsf{w}_{i+1}) \leftarrow \mathsf{trace}(F^\prime, (\mathsf{vk}, \mathsf{U}_i, \mathsf{u}_i, (i, z_0, z_i), w_i, \overline{T}))$, and
$\quad(3)$ output $\Pi_{i+1} \leftarrow ((\mathsf{U}_{i+1}, \mathsf{W}_{i+1}),( \mathsf{u}_{i+1}, \mathsf{w}_{i+1}))$.
>
> $\underline{\mathcal{V}(\mathsf{vk}, (i, z_0, z_i), \Pi_i) \rightarrow \{0, 1\}}$:
> 
> If $i$ is $0$, check that $z_i = z_0$; 
otherwise,
$\quad(1)$ parse $\Pi_i$ as $((\mathsf{U}_i, \mathsf{W}_i), (\mathsf{u}_i, \mathsf{w}_i))$,
$\quad(2)$ check that $\mathsf{u}_i.\mathsf{x} = \mathsf{hash}(\mathsf{vk}, i, z_0, z_i, \mathsf{U}_i)$,
$\quad(3)$ check that $(\mathsf{u}_i.\overline{E}, \mathsf{u}.u) = (\mathsf{u}_\bot.\overline{E}, 1)$, and
$\quad(4)$ check that $\mathsf{W}_i$ and $\mathsf{w}_i$ are satisfying witnesses to $\mathsf{U}_i$ and $\mathsf{u}_i$ respectively.

### code

```rs=
pub struct NovaAugmentedCircuitParams {
  limb_width: usize, // word size
  n_limbs: usize, // how many words
  is_primary_circuit: bool, // A boolean indicating if this is the primary circuit
}
```

```rs=
pub struct NovaAugmentedCircuitInputs<G: Group> {
  params: G::Scalar, // Hash(Shape of u2, Gens for u2). Needed for computing the challenge.
  i: G::Base,
  z0: Vec<G::Base>,
  zi: Option<Vec<G::Base>>,
  U: Option<RelaxedR1CSInstance<G>>,
  u: Option<R1CSInstance<G>>,
  T: Option<Commitment<G>>,
}
```

`params`:


## `lib.rs`

### A zkSNARK of a Valid IVC Proof

> **Construction 4 (A zkSNARK of a Valid IVC Proof).** Let $\mathsf{IVC}$ denote the IVC scheme in Construction 3, let $\mathsf{NIFS}$ denote the non-interactive folding scheme in Construction 2, and let $\mathsf{hash}$ denote a randomized cryptographic hash function. Assume a zero-knowledge succinct non-interactive argument of knowledge (Definition 2), $\mathsf{zkSNARK}$, for committed relaxed R1CS. That is, given public parameters $\mathsf{pp}$, structure $\mathsf{s}$, and instance $\mathsf{u}$, $\mathsf{zkSNARK.P}$ can convince $\mathsf{zkSNARK.V}$ in zero-knowledge and with a succinct proof (e.g., $O_\lambda(\log N)$-sized proof) that it knows a corresponding witness $\mathsf{w}$ such that $(\mathsf{pp, s, u, w})$ is a satisfying committed relaxed R1CS tuple.
>
>$\quad$Consider a polynomial-time computable function $F$. Suppose $\mathsf{pp} \leftarrow \mathsf{IVC.G}(1^\lambda)$ and $(\mathsf{pk, vk}) \leftarrow \mathsf{IVC.K}(\mathsf{pp}, F)$. Suppose the prover $\mathcal{P}$ and verifier $\mathcal{V}$ are provided an instance $(i,z_0,z_i)$. We construct a zkSNARK that allows the prover to show that it knows an IVC proof $\Pi_i$ such that $\mathsf{IVC.V}(\mathsf{vk}, i, z_0, z_i, \Pi_i) = 1$.
>
>$\quad$In a nutshell, we leverage the fact that $\Pi$ is two committed relaxed R1CS instance-witness pairs. So, $\mathcal{P}$ first folds instance-witness pairs $(\mathsf{u, w})$ and $(\mathsf{U, W})$ to produce a folded instance-witness pair $(\mathsf{U^\prime,W^\prime})$, using $\mathsf{NIFS.P}$. Next, $\mathcal{P}$ runs $\mathsf{zkSNARK.P}$ to prove that it knows a valid witness for $\mathsf{U^\prime}$. In more detail, for polynomial-time computable function $F$ and corresponding function $F^\prime$ as defined in Construction 3 (and instantiated with $\mathsf{hash}$), we define $(\mathcal{G, K, P, V})$ as follows.
>
> $\underline{\mathcal{G}(1^\lambda) \rightarrow \mathsf{pp}}$:
$(1)$ Compute $\mathsf{pp_{NIFS}} \leftarrow \mathsf{NIFS.G}(1^\lambda)$
$(2)$ Compute $\mathsf{pp_{zkSNARK}} \leftarrow \mathsf{zkSNARK.G}(1^\lambda)$
$(3)$ Output ($\mathsf{pp_{NIFS}}, \mathsf{pp_{zkSNARK}})$
>
> $\underline{\mathcal{K}(\mathsf{pp}, F) \rightarrow (\mathsf{pk, vk})}$:
$(1)$ Compute $(\mathsf{pk_{NIFS}, vk_{NIFS}}) \leftarrow \mathsf{NIFS.K}(\mathsf{pp.pp_{NIFS}}, \mathsf{s}_{F^\prime})$.
$(2)$ Compute $(\mathsf{pk_{zkSNARK}, vk_{zkSNARK}}) \leftarrow \mathsf{zkSNARK.K}(\mathsf{pp.pp_{zkSNARK}}, \mathsf{s}_{F^\prime})$. 
$(3)$ Output $((\mathsf{pk_{NIFS}, pk_{zkSNARK}}), (\mathsf{vk_{NIFS}, vk_{zkSNARK}}))$.
> 
> $\underline{\mathcal{P}(\mathsf{pk}, (i, z_0, z_i), \Pi) \rightarrow \pi}$:
If $i$ is $0$, output $\bot$;
otherwise,
$\quad(1)$ parse $\Pi$ as $((\mathsf{U, W}), (\mathsf{u, w}))$
$\quad(2)$ compute $(\mathsf{U^\prime,W^\prime},\overline{T}) \leftarrow \mathsf{NIFS.P}(\mathsf{pk_{NIFS}},(\mathsf{U,W}),(\mathsf{u,w}))$ 
$\quad(3)$ compute $\pi_{\mathsf{U^\prime}} \leftarrow \mathsf{zkSNARK.P}(\mathsf{pk_{zkSNARK}, U^\prime, W^\prime})$
$\quad(4)$ output $(\mathsf{U, u}, \overline{T}, \pi_{\mathsf{U^\prime}})$.
>
>$\underline{\mathcal{V}(\mathsf{vk}, (i, z_0, z_i), \pi) \rightarrow \{0, 1\}}$:
If $i$ is $0$, check that $z_0 = z_i$; 
otherwise,
$\quad(1)$ parse $\pi$ as $(\mathsf{U,u},\overline{T},\pi_{\mathsf{U^\prime}})$,
$\quad(2)$ check that $\mathsf{u.x} = \mathsf{hash}(\mathsf{vk_{NIFS}}, i, z_0, z_i, \mathsf{U})$,
$\quad(3)$ check that $(\mathsf{u}.\overline{E}, \mathsf{u}.u) = (\mathsf{u}_{\bot}.\overline{E}, 1)$,
$\quad(4)$ compute $\mathsf{U}^\prime \leftarrow \mathsf{NIFS.V}(\mathsf{vk_{NIFS},U,u},\overline{T})$, and
$\quad(5)$ check that $\mathsf{zkSNARK.V}(\mathsf{vk_{zkSNARK}}, \mathsf{U^\prime}, \pi_\mathsf{U^\prime} ) = 1$.



**Polynomial Extension**(MLE) see [Notes for PAZK(MLE)](/EmflUXcZS9mE9wIkh8i-mQ?view#35-Low-Degree-and-Multilinear-Extensions)

**The Sum-Check Protocol** see [Notes for PAZK(Sum-Check)](/EmflUXcZS9mE9wIkh8i-mQ?view#41-The-Sum-Check-Protocol)

### Idealized Relaxed R1CS
> **Definition 14 (Idealized Relaxed R1CS).** Consider a finite field $\mathbb{F}$. Let the public parameters consist of size bounds $m, n, l \in \mathbb{N}$ where $m > l.$ The idealized relaxed R1CS structure consists of sparse matrices $A, B, C \in \mathbb{F}^{m \times m}$ with at most $n = \Omega(m)$ non-zero entries in each matrix. A idealized relaxed R1CS instance consists of an error vector $E \in \mathbb{F}^m$, a scalar $u \in \mathbb{F}$, witness vector $W \in \mathbb{F}^m$, and public inputs and outputs $\mathsf{x} \in \mathbb{F}^l$. An instance $(E,u,W,\mathsf{x})$ is satisfying if $(A \cdot Z) \circ (B \cdot Z) = u \cdot (C \cdot Z) + E$, where $Z = (W, \mathsf{x}, u)$.

### Polynomial IOP for Idealized Relaxed R1CS
> **Construction 5 (Polynomial IOP for Idealized Relaxed R1CS)**. Consider an idealized relaxed R1CS statement $\varphi$ consisting of public parameters $(m, n, l)$, structure $(A,B,C)$, and instance $(E,u,W,\mathsf{x})$, Without loss of generality, we assume that $m$ and $n$ are powers of $2$ and that $m = 2 \cdot (l + 1)$.
> $\quad$Let $s = \log m$. We interpret the matrices $A, B, C$ as functions with signature $\{0, 1\}^{\log m} \times \{0, 1\}^{\log m} \rightarrow \mathbb{F}$ in a natural manner. In particular, an input in $\{0, 1\}^{\log m} \times \{0, 1\}^{\log m}$ is interpreted as the binary representation of an index $(i, j) \in [m] \times [m]$, where $[m] := \{1, \dots, m\}$ and the function outputs $(i, j)$th entry of the matrix. As such, let $\widetilde{A}, \widetilde{B}$, and $\widetilde{C}$ denote multilinear extensions of $A, B,$ and $C$ interpreted as functions, so they are $2\log m$-variate sparse multilinear polynomials of size $n$. Similarly, we interpret $E$ and $W$ as functions with respective signatures $\{0, 1\}^{\log m} \rightarrow \mathbb{F}$ and $\{0, 1\}^{\log m−1} \rightarrow \mathbb{F}$. Furthermore, let $\widetilde{E}$ and $\widetilde{W}$ denote the multilinear extensions of $E$ and $W$ interpreted as functions, so they are multilinear polynomials in $\log m$ and $\log m − 1$ variables respectively.
> $\quad$As noted earlier, the verifier has an oracle access to the following polynomials: $\widetilde{A}, \widetilde{B}, \widetilde{C}, \widetilde{E}$, and $\widetilde{W}$. Additionally, the verifier reads $u$ and $\mathsf{x}$ in entirety.
> $\quad$Let $Z = (W,\mathsf{x},u)$. Similar to how we interpret matrices as functions, we interpret $Z$ and $(\mathsf{x},u)$ as functions with the following respective signatures: $\{0, 1\}^s \rightarrow \mathbb{F}$ and $\{0, 1\}^{s−1} \rightarrow \mathbb{F}$. Observe that the $\text{MLE}$ $\widetilde{Z}$ of $Z$ satisfies $$\widetilde{Z}(X_1,\dots,X_s) =(1−X_1)\cdot \widetilde{W}(X_2,\dots,X_s)+X_1\cdot \widetilde{(\mathsf{x},u)}(X_2,\dots,X_s) \quad (1)$$
> $\quad$Similar to [40, Theorem 4.1], checking if $\varphi$ is satisfiable is equivalent, except for a soundness error of $\log m/|\mathbb{F}|$ over the choice of $\tau \in \mathbb{F}^s$, to checking if the following identity holds: $$0 \stackrel{?}{=} \sum_{x \in \{0,1\}^s} \widetilde{\mathsf{eq}}(\tau, x) \cdot F (x), \quad (2)$$ where $$F(x)= \begin{pmatrix} \sum_{y\in \{0,1\}^s} \widetilde{A}(x,y) \cdot \widetilde{Z}(y) \end{pmatrix} \cdot \begin{pmatrix} \sum_{y \in \{0, 1\}^s} \widetilde{B}(x,y) \cdot \widetilde{Z}(y) \end{pmatrix} − \begin{pmatrix} u \cdot \sum_{y \in \{0,1\}^s} \widetilde{C}(x,y)  \cdot \widetilde{Z}(y)+ \widetilde{E}(x)\end{pmatrix},$$ and $\widetilde{\mathsf{eq}}$ is the multilinear extension of $\mathsf{eq}: \{0, 1\}^s \times \{0, 1\}^s \rightarrow \mathbb{F}$ where $\mathsf{eq}(x, e) = 1$ if $x = e$ and $0$ otherwise.
> $\quad$That is, if $\varphi$ is satisfiable, then Equation (2) holds with probability $1$ over the choice of $\tau$, and if not, then Equation (2) holds with probability at most $O(\log m/|\mathbb{F}|)$ over the random choice of $\tau$.
> $\quad$To compute the right-hand side in Equation (2), the prover and the verifier apply the sum-check protocol to the following polynomial: $g(x) := \widetilde{\mathsf{eq}}(\tau, x) \cdot F(x)$ From the verifier’s perspective, this reduces the task of computing the right-hand side of Equation (2) to the task of evaluating $g$ at a random input $r_x \in \mathbb{F}^s$. Note that the verifier can locally evaluate $\widetilde{\mathsf{eq}}(\tau,r_x)$ in $O(\log m)$ field operations via $\widetilde{\mathsf{eq}}(\tau, r_x) = \prod_{i=1}^s(\tau_ir_{x,i} + (1 − \tau_i)(1 − r_{x,i})).$ With $\widetilde{\mathsf{eq}}(\tau, r_x)$ in hand, $g(r_x)$ can be computed in $O(1)$ time given the four quantities: $\sum_{y\in \{0,1\}^s} \widetilde{A}(r_x, y) \cdot \widetilde{Z}(y),\ \sum_{y\in \{0,1\}^s} \widetilde{B}(r_x, y) \cdot \widetilde{Z}(y),\ \sum_{y\in \{0,1\}^s} \widetilde{C}(r_x, y) \cdot \widetilde{Z}(y)$, and $\widetilde{E}(r_x)$.
> $\quad$The last quantity can be computed with a single query to polynomial $\widetilde{E}$. Furthermore, the first three quantities can be computed by applying the sum-check protocol three more times in parallel, once to each of the following three polynomials (using the same random vector of field elements, $r_y \in \mathbb{F}^s$, in each of the three invocations): $\widetilde{A}(r_x, y) \cdot \widetilde{Z}(y), \widetilde{B}(r_x, y) \cdot \widetilde{Z}(y)$, and $\widetilde{C}(r_x, y) \cdot \widetilde{Z}(y)$.
> $\quad$To perform the verifier’s final check in each of these three invocations of the sum-check protocol, it suffices for the verifier to evaluate each of the above three polynomials at the random vector $r_y$, which means it suffices for the verifier to evaluate $\widetilde{A}(r_x,r_y), \widetilde{B}(r_x,r_y), \widetilde{C}(r_x,r_y)$, and $\widetilde{Z}(r_y)$. The first three evaluations can be obtained via the verifier’s assumed query access to $(\widetilde{A},\widetilde{B},\widetilde{C})$. $\widetilde{Z}(r_y)$ can be computed (via Equation (1)) from a query to $\widetilde{W}$ and from computing $\widetilde{(x, u)}$.
> $\quad$In summary, we have the following polynomial IOP.
> 1. $\mathcal{V} \rightarrow \mathcal{P}: \tau \in _R \mathbb{F}^s$
> 2. $\mathcal{V} \leftrightarrow \mathcal{P}$: run the sum-check protocol to reduce the check in Equation (2) to checking if the following hold, where $r_x,r_y$ are vectors in $\mathbb{F}^s$ chosen at random by the verifier over the course of the sum-check protocol:
>  – $\widetilde{A}(r_x,r_y) \stackrel{?}{=} v_A, \widetilde{B}(r_x,r_y) \stackrel{?}{=} v_B$, and $\widetilde{C}(r_x,r_y) \stackrel{?}{=} v_C$;
>  – $\widetilde{E}(r_x) \stackrel{?}{=} v_E;$ and
>  – $\widetilde{Z}(r_y) \stackrel{?}{=} v_Z$. 
> 3. $\mathcal{V}$:
>  – check if $\widetilde{A}(r_x,r_y) \stackrel{?}{=} v_A, \widetilde{B}(r_x,r_y) \stackrel{?}{=} v_B$, and $\widetilde{C}(r_x,r_y) \stackrel{?}{=} v_C$, with a query to $\widetilde{A}, \widetilde{B},\widetilde{C}$ at $(r_x,r_y)$;
>  – check if $\widetilde{E}(r_x) \stackrel{?}{=} v_E$ with an oracle query to $\widetilde{E}$; and
>  – check if $\widetilde{Z}(r_y) \stackrel{?}{=} v_Z$ by checking if: $v_Z = (1−r_y[1])\cdot v_W + r_y[1]\cdot \widetilde{(x,u)}(r_y[2..])$, where $r_y[2..]$ refers to a slice of $r_y$ without the first element of $r_y$, and $v_W \leftarrow \widetilde{W}(r_y[2..])$ via an oracle query (see Equation (1)).)



## bellpepper mod


## dependencies

### bellpepper
see 

https://hackmd.io/iR4lHIphQpeyZo1W3-VxQA?view









