## Notes on SNARK's/Plonk and Halo2

### Requirements of proof system:

$V$ --> verifier.
$P$ --> prover.
$C$ --> the circuit.

- Completeness: If i run a computation, I can compute a proof that the output is correct.

$\forall\, x, w; C(x,w) = 0$
that is:
$\textrm{Proof}[V(\textrm{vkey}, x, P[\textrm{pkey}, x, w]) = accept] = 1$

where:
$x$ is the public statement in $\mathbb{F}^n$
$w$ is the secret witness in $\mathbb{F}^m$

- Soundness: I cannot convince you that the results is correct if it's not.
i.e., Adaptively knowledge sound:
$V$ accepts that $P$ "knows" $w$ such that $C(x,w) = 0$, and that an extractor $E
can extract a valid $w$ from the prover.

- Zero-Knowledge: If I want to, I can hide some or all of the inputs to the computation.
$(C, \textrm{pkey}, \textrm{vkey}, x, Proof)$ reveal nothing new about $w$. A witness exists that can simulate the proof.

### Components of:

(1) Arithmetic Circuit $C$:
- Need to fix some finite filed $\mathbb{F} = \{0,...,p-1 \}$ for some $p>2$, where you can do addition and multpication $\textrm{mod } p$.
- Construct a arithmetic circuit $C$, where $C: \mathbb{F}^n \rightarrow \mathbb{F}$.
Which is a DAG with the nodes labeled $+, - \textrm{ or } \times$, i.e. these are the "Gates".
The circuit $C$ then defines a $n$-variant polynomial with an evaluation recipe.

(2) has an Argument System:
a public arithmetic circuit $C(x,w) \rightarrow \mathbb{F}$, takes a public statement $x$ in $\mathbb{F}$, and a secret witness $w$ in $\mathbb{F}^m$ and outputs a finite field element $\mathbb{F}$.
Goal:
$P$ is to convince $V$ that $\exists\,w$ such taht $C(x,w) = 0$.

### Preprocessing/Setup of a NARK / SNARK:

As above the public arithmetic circuit: $C(x,w) \rightarrow \mathbb{F}$

A preprocessing circuit ("Setup") will take a public circuit (a Synthesized circuit) through a setup algorithm $S(c)$ which will output parameters for the prover and verifier, $\textrm{vkey}, \textrm{pkey}$.

In preprocessing/ssetup we fix the arithmetic circuit $C$ by taking $x$ a public statement in $\mathbb{F}^{n}$, and a secret witness $w$ in $\mathbb{F}^{m}$, and outputting the finite field element $\mathbb{F}$.

Preprocessing (Setup): $S(C) \rightarrow \textrm{public paramaters}(\textrm{pkey}, \textrm{vkey})$

where $\textrm{pkey}$ is the proving key, and $\textrm{vkey}$ is the verification key. i.e., the `.params` files.

The Prover $P$, takes $\textrm{pkey}, x,w$ and produces a Proof. The Prover proves that the circuit evaluates to zero at the point $(x,w)$. $\textrm{Proof that } C(x,w) = 0$. The Verifier either accepts or rejects the proof.

In the a (preprocessing/setup based) NARK/SNARK is three algorithms:
- $S(C) \rightarrow$ public parameters $(\textrm{vkey}, \textrm{pkey})$ for provers and verifier.
- $P(\textrm{pkey}, x,w) \rightarrow$ produces a proof
- $V(\textrm{vkey}, x) \rightarrow$ accepts or rejects the proof.

a SNARK is just a NARK, retians all the same properties of completeness, soundness, but prodcues succinct public parameters $S\textrm{vkey}, S\textrm{pkey}$.

### Concepts:
In general building SNARKs can be done in two steps:
(1) a function commitment scheme.
(2) a suitable interactive oracle proof (IOP).

Within halo2 (an others) we use for:
(1) a polynomial commitment scheme (PCS) as the commitment scheme.
(2) a polynomial interactive oracle proof (poly-IOP) for the IOP.

Plonk + PCS $\rightarrow$ SNARK.

## Halo2 notes and deconstruction of codebase:

There are 3 phases for proof system: circuit construction, proof generation, proof verification. $S(C), P(\textrm{pkey}, x,w), V(\textrm{vkey}, x)$ respectively.

Phase 1:
Phase1 (1st), Configure to get the constraint system.
Phase1 (2nd) Synthesize to get the fixed $x$ --> then you can generate a $\textrm{vkey}$.

Phase 2:
Phase2 (3rd) Synthesize fills in the witness $w$ --> then you can generate a proof.

A circuit $C$ is synthesized in two steps.
step 1. call synthesise to fill in all the fixed columns, these columns will be commited and become the $\textrm{vkey}$.

Every time you define acircuit you have the fixed colums, and the fixed permutations, these two parts will become the $\textrm{vkey}$ that will be used to verify a proof.
Every time you have a fixed circuit, the copy constraint and the fixed columns are fixed. When you synthesize the circuit you can change the advice column.

./halo2/halo2_proofs/src/plonk/circuit.rs

./halo2/halo2_proofs/src/plonk/keygen.rs

/// Generate a `VerifyingKey` from an instance of `Circuit`.
pub fn keygen_vk<C, ConcreteCircuit>(
    params: &Params<C>,
    circuit: &ConcreteCircuit,
) -> Result<VerifyingKey<C>, Error>
where
    C: CurveAffine,
    ConcreteCircuit: Circuit<C::Scalar>,
{

`keygen_zk` calls `synthesize()` passing in the assembily object which implements several traits. It implements the traits that are a list of callbacks, i.e.,
When you assign asvice, it will call assembilies advice.
When you assign a copy constraint, it will call assembily.assign copy constraint of .. .
Assign fixed, will call assembily.assign_fixed.

Becuase this (syntehsize) is in the keygen_vk phase, it ignores all the witness assignments, it only proccesses the assignment of fixed and the copy constraints.

When we implment Assembily, we implement a trait with dummy functions when assign advice, and some meaningful functions when assign_fixed and copy constaints.

Looking at the implementation of Assembily (in the same file keygen.rs):

// Assembly to be used in circuit synthesis.
#[derive(Debug)]
struct Assembly<F: Field> {
    k: u32,
    fixed: Vec<Polynomial<Assigned<F>, LagrangeCoeff>>,
    permutation: permutation::keygen::Assembly,
    selectors: Vec<Vec<bool>>,
    // A range of available rows for assignment and copies.
    usable_rows: Range<usize>,
    _marker: std::marker::PhantomData<F>,
}

impl<F: Field> Assignment<F> for Assembly<F> {

    fn enter_region<NR, N>(&mut self, _: N) {...}
    fn exit_region(&mut self) {...}
    fn enable_selector<A, AR>(&mut self, _: A, selector: &Selector, row: usize) -> Result<(), Error> {...}
    
    fn query_instance(
        &self, 
        _: Column<Instance>, 
        row: usize
    ) -> Result<Option<F>, Error> {... DUMMY FUNCTION ...}
    
    fn assign_advice<V, VR, A, AR>(
        &mut self,
        _: A,
        _: Column<Advice>,
        _: usize,
        _: V,
    ) -> Result<(), Error> {... DUMMY FUNCTION ...}

    fn assign_fixed<V, VR, A, AR>(
        &mut self,
        _: A,
        column: Column<Fixed>,
        row: usize,
        to: V,
    ) -> Result<(), Error> {...}

    fn copy(
        &mut self,
        left_column: Column<Any>,
        left_row: usize,
        right_column: Column<Any>,
        right_row: usize,
    ) -> Result<(), Error> {...}

    fn fill_from_row(
        &mut self,
        column: Column<Fixed>,
        from_row: usize,
        to: Option<Assigned<F>>,
    ) -> Result<(), Error> {...}

    fn push_namespace<NR, N>(&mut self, _: N)
    where
        NR: Into<String>,
        N: FnOnce() -> NR,
    {
        // Do nothing; we don't care about namespaces in this context.
    }

    fn pop_namespace(&mut self, _: Option<String>) {
        // Do nothing; we don't care about namespaces in this context.
    }
}

`enable_selector()` does something because selectors are part of the fixed configuration of the circuit. If you have the selectors then you have a fixed circuit.

`query_instance()` gives you assign cell None. i.e., it does nothing when you create an instance."There is no instance in this context" ... DUMMY FUNCTION ...

`assign_advice()` is also a dummy function "We only care about fixed columns here". (see below) ... DUMMY FUNCTION ...

`assign_fixed()` does something, put in the column. This is the fixed part that we will use to generate the $\textrm{vkey}$.

When we then use `copy()` (copy constraint) its fixed and goes into the $\textrm{vkey}$.

`fill_from_row()` is fixed, does something, its a fixed column.

That means that after the $\textrm{vkey}$ generation, we get a commitment of the whole circuit. via a PCS.

domain is somehow fixed.
fixed_commitment --> is the commitment of the fixed columns.
permutation_vk --> is the fixed commitment of the permutation.

### CS:

So far we have fixed commitment, but we can not see anything about the constraint of every row (in keygen_vk()). So how is the constraint recoreded in the keygen_v or _pkk?

We have to create a domain, buy the circuit (ConcreteCircuit). The circuit only defines the constaint, and circuit Synthesize assigns the copy constraints. If you do not run Synthesize, you dont know if there is a copy of another cell. Constraints are applied on a circuit level, this is done in the Config part of the ConcreteCircuit.

**
That means the circuit does configure first, which gives you the constraint system, and then, the circuit runs Synthesize which is Phase 1, which gives you the fixed part to generate a vkey. Then in phase 2, of Synthesize, it fills in the fields in the witness part. Then you can generate a proof.
**

the "cs" that is returned from keygen_vk:

    Ok(VerifyingKey {
        domain,
        fixed_commitments,
        permutation: permutation_vk,
        cs,
    })

cs --> ConstraintSystem is a struct that is in ./halo2_proofs/src/plonk/circuit.rs line 985 (junyu0312), line 934 in (zcash).

/// This is a description of the circuit environment, such as the gate, column and
/// permutation arrangements.
#[derive(Debug, Clone)]
pub struct ConstraintSystem<F: Field> {
    pub(crate) num_fixed_columns: usize,
    pub num_advice_columns: usize,
    pub num_instance_columns: usize,
    pub(crate) num_selectors: usize,
    pub(crate) selector_map: Vec<Column<Fixed>>,
    pub gates: Vec<Gate<F>>,
    pub advice_queries: Vec<(Column<Advice>, Rotation)>,
    // Contains an integer for each advice column
    // identifying how many distinct queries it has
    // so far; should be same length as num_advice_columns.
    pub(crate) num_advice_queries: Vec<usize>,
    pub instance_queries: Vec<(Column<Instance>, Rotation)>,
    pub fixed_queries: Vec<(Column<Fixed>, Rotation)>,

    // Permutation argument for performing equality constraints
    pub permutation: permutation::Argument,

    // Vector of lookup arguments, where each corresponds to a sequence of
    // input expressions and a sequence of table expressions involved in the lookup.
    pub lookups: Vec<lookup::Argument<F>>,

    // Vector of fixed columns, which can be used to store constant values
    // that are copied into advice columns.
    pub(crate) constants: Vec<Column<Fixed>>,

    pub(crate) minimum_degree: Option<usize>,
}

The ConstraintSystem struct tells you about columns.
The Gate define the relationship between arrays of these columns

The gate means only the constraint system. So do not confuse the Gate with the copy constraint. Gate defines the constraint system.

Gate is a struct in .halo2_proofs/src/plonk/circuit.rs line 941.

pub struct Gate<F: Field> {
    name: &'static str,
    constraint_names: Vec<&'static str>,
    pub polys: Vec<Expression<F>>,
    /// We track queried selectors separately from other cells, so that we can use them to
    /// trigger debug checks on gates.
    queried_selectors: Vec<Selector>,
    pub queried_cells: Vec<VirtualCell>,
}

The constraint system is defined by a bunch of polynomials that are equal to zero.

## Prover Protocol:

The prover has five (5) rounds. In each round polynomials are created and evaluated at some point.

------

WIP more to be added

------
Phase 1:
1st, Configure to get the constraint system.
2nd Synthesize to get the fixed part --> then you can generate a vkey.
Phase 2:
3rd Synthesize fills in the witness part --> then you can generate a proof.

Tasks: write up notes on:

any SRS or PCS schemete relted info.
roots of unity.
Polynomial interpolation.
Copy Constraint.
Encode Permutation from Copy Constraint as polynomial.
Copy Constraints and Assignments

proof generation algo:
sigma --> mapping from the copy constraints to roots of unity

        // for all the components of the plonk circuit
        //
        //   (a,b,c)                  : assigments / values
        //   (o,m,l,r,c)              : gate constraints
        //   (sigma1, sigma2, sigma3) : copy constraints

round 1 - eval a(x), b(x), c(x) at s:
round 2 - eval "acummulator vector polynomial" at s:

        // create the accumulator vector
        //
        // we have to prove that the wires are the same that the permutation of the
        // copy constrains one.
        //
        // beta       blinding against prover addition manipulation
        // gamma      blinding against prover multiplication manipulation
        // k1,k2      coset independance between a,b,c

the accumulator vector is interpolated into a polynomial acc(x) and this is used to create the polynomial z.

we know that evaluating the accumulator polinimial at the last root of unity, the evaluation should be 1, check it.

round 3 - compute the quotient polynomial:
...

round 4 - compute linearization polynomial:
...

round 5:
create two large polynomials that combine all the polynomials we've been using so far and we output commitments to them.