## Weekly report:

2023 Week 33.

**Uderstanding:** Working mostly this week on understanding the 5 phases of halo2 proving algorithm (see notes below).

**Documentation:** Delphinus-Lab-Book documentation PR:
https://github.com/DelphinusLab/Delphinus-Lab-Book/pull/3

**Productivity:** goal: to understand halo2 proving algo (as cs from last week) in order to write helper functions & actually understand circuit construction and proof generation.

## Notes Proving algorithm. (notes rough)

Working on understanding:

(1) Constraint system construction.
(2) proving algorith in halo2

## CS

halo to routine algo.

run fn copy () in `Assembily` halo2_proofs/src/plonk/permutation/keygen.rs
runs polynomial() in circuit.rs
verify_at_rows()

## Copy constraints:

encode permutation from copy constraint as polynomial

The copy constraints involving left, right and output values are encoded as polynomials $S\sigma_1$, $S\sigma_2$ and $S\sigma_3$ using the cosets.

## Prover Protocol:

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

# Proving system
below if from [here](https://github.com/DelphinusLab/halo2-gpu-specific/blob/main/book/src/design/proving-system.md)
The Halo 2 proving system can be broken down into five stages:

1. Commit to polynomials encoding the main components of the circuit:
- Cell assignments.
- Permuted values and products for each lookup argument.
- Equality constraint permutations.
2. Construct the vanishing argument to constrain all circuit relations to zero:
- Standard and custom gates.
- Lookup argument rules.
- Equality constraint permutation rules.
3. Evaluate the above polynomials at all necessary points:
- All relative rotations used by custom gates across all columns.
- Vanishing argument pieces.
4. Construct the multipoint opening argument to check that all evaluations are consistent
with their respective commitments.
5. Run the inner product argument to create a polynomial commitment opening proof for the
multipoint opening argument polynomial.

------

Compute elliptic curve points which represent these polynomials evaluated at the "secret" number $s$.
Do this by using the SRS from the setup phase. Prover to use the algorithms for adding and scaling elliptic curve points from the SRS in order to compute these points.

These points are commitments to polynomials representing our chosen assignments to the circuit.

### Round 2:

Round 2 is about committing to a single polynomial $z$ that encodes all of the copy constraints.

generate randonm $b_7, b_8, b_9 \in \mathbb{F}_p$

In Round 2 we see the first use of "challenge" values, in this case $\beta$ and $\gamma$. The nature of these challenge values depends on whether the protocol is interactive. In an interactive protocol, the Verifier chooses these challenge values and sends them to the Prover, who uses them to construct the proof. In a non-interactive protocol, these values are derived from a cryptographic hash of a transcript of the Prover's process. These values would be unpredictable by the either the Prover or Verifier, but each party is be able to compute the same challenge values using the same hash function on the transcript. This is known as the Fiat-Shamir transform which can turn an interactive protocol non-interactive.

### Round 3:

Compute quotient challenge $\alpha = \textrm{some random number} \in \mathbb{F}_p$, then compute quotient polynomial $t(x)$:

### Round 4:

In Round 4, we create a polynomial $r$ that is a kind of partner to $t$, where many of the polynomials that were included in $t$ are replaced by field elements that are evaluations of those polynomials at a challenge value $\zeta$

Linearization. Compute evaluation challenge $\zeta = 5 \in \mathbb{F}_p$

### Round 5:

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

Compute opening proof polynomial $W_{\zeta}(x)$ and compute opening proof polynomial $W_{\zeta \omega}(x)$

### The Proof:

the proof is then:

$$\pi_{\textrm{SNARK}} = ([a],[b],[c],[z],[t_{lo}],[t_{mid}],[t_{hi}],[W_{\zeta}],[W_{\zeta\omega}]\\
\bar{a},\bar{b},\bar{c},\bar{S_{\sigma_1}},\bar{S_{\sigma_2}},\bar{z_{\omega}},\bar{r})$$

## The Verifier algorithm
The Verifier arithmetically combines the proof and any public information and checks that a single equation holds. If using Kate polynomial commitments this equation will involve evaluating an elliptic curve pairing.

1. Validate that $[a],[b],[c],[z],[t_{lo}],[t_{mid}],[t_{hi}],[W_{\zeta}],[W_{\zeta\omega}]\in G_1$
1. Validate $\bar{a},\bar{b},\bar{c},\bar{S_{\sigma_1}},\bar{S_{\sigma_2}},\bar{z_{\omega}},\bar{r}\in\mathbb{F}_{17}$.
1. Validate $w_{i\in[l]}\in \mathbb{F}_{17}$ (public inputs)
1. Compute zero polynomial evaluation: $Z_H(\zeta)=\zeta^n-1$.
1. Compute $L_1(\zeta)=\frac{\zeta^n-1}{n(\zeta-1)}$
1. Compute public input polynomial evaluation: $PI(\zeta)=\sum_{i\in[l]}w_iL_i(\zeta)$
1. Compute quotient polynomial evaluation:
$$\bar{t}=\frac{\bar{r}+PI(\zeta)-(\bar{a}+\beta\bar{S_{\sigma_1}}+\gamma)(\bar{b}+\beta\bar{S_{\sigma_2}}+\gamma)(\bar{c}+\gamma)\alpha-L_1(\zeta)\alpha^2}{Z_H(\zeta)}$$
1. Compute first part of batched polynomial commitment. Define $[D]=v[r(x)]+u[z]$:
$$[D]=\bar{a}\bar{b}v[q_M]+\bar{a}v[q_L]+\bar{b}v[q_R]+\bar{c}v[q_O]+v[q_C]\\
+((\bar{a}+\beta\zeta+\gamma)(\bar{b}+\beta k_1\zeta+\gamma)(\bar{c}+\beta k_2\zeta+\gamma)\alpha v+L_1(\zeta)\alpha^2 v+u)[z]\\
-(\bar{a}+\beta\bar{S_{\sigma_1}}+\gamma)(\bar{b}+\beta{S_{\sigma_2}}+\gamma)\alpha v\beta\bar{z_{\omega}}[S_{\sigma_3}]$$
1. Compute full batched polynomial commitment
$$[F]=[t_{lo}]+\zeta^{n+2}[t_{mid}]+\zeta^{2n+4}[t_{hi}]+[D]+v^2[a]+v^3[b]+v^4[c]+v^5[S_{\sigma_1}]+v^6[S_{\sigma_2}]$$
1. Compute group encoded batch evaluation $[E]$:
$$[E]=(\bar{t}+v\bar{r}+v^2\bar{a}+v^3\bar{b}+v^4\bar{c}+v^5\bar{S_{\sigma_1}}+v^6\bar{S_{\sigma_2}}+u\bar{z_{\omega}})\cdot[1]$$
1. Batch validate all evaluations:
$$e([W_{\zeta}]+u[W_{\zeta\omega}],[s]_2)=e(\zeta[W_{\zeta}]+u\zeta\omega[W_{\zeta\omega}]+[F]-[E],[1]_2)
$$

## Proof Generation (halo2):
In the proving system .halo2_proofs/src/plonk/prover.rs . Walking through the code a bit:

/// This creates a proof for the provided `circuit` when given the public
/// parameters `params` and the proving key [`ProvingKey`] that was
/// generated previously for the same circuit. The provided `instances`
/// are zero-padded internally.
pub fn create_proof<
    C: CurveAffine,
    E: EncodedChallenge<C>,
    R: RngCore,
    T: TranscriptWrite<C, E>,
    ConcreteCircuit: Circuit<C::Scalar>,
>(
    params: &Params<C>,
    pk: &ProvingKey<C>,
    circuits: &[ConcreteCircuit],
    instances: &[&[&[C::Scalar]]],
    mut rng: R,
    transcript: &mut T,
) -> Result<(), Error> {
...
}

In create_proof() we construct an instance (line 81 in prover.rs), We create an advice (line 141),

Note: When (in the first round) you do Synthesize, you only calculate the fixed stuff, In the second round, Synthesize happens again, but it is based on the instance, and we get the the advice(s). line 289 in prover.rs

            // Synthesize the circuit to obtain the witness and other information.
            ConcreteCircuit::FloorPlanner::synthesize(
                &mut witness,
                circuit,
                config.clone(),
                meta.constants.clone(),
            )?;

These (the advice(s)) are used for the proof, in Phase 2.

Phase 1 - Synthesize runs, get fixed , generates the vkey.
Phase 2 - Synthesize runs based on the instance, to generate the advice.

Note: lookups are part in the proving key part

After phase 2, lets see how the constraint system permutation is applied. Permutation pert in prover.rs:

pk.vk.cs.permutation.commit(
i.e., commitment of the cs permutaton. in other words is it apply cs.permutation on the vk ?

    // Commit to permutations.
    let permutations: Vec<permutation::prover::Committed<C>> = instance
        .iter()
        .zip(advice.iter())
        .map(|(instance, advice)| {
            pk.vk.cs.permutation.commit(
                params,
                pk,
                &pk.permutation,
                advice.advice_values.as_ref().unwrap(),
                &pk.fixed_values,
                &instance.instance_values,
                beta,
                gamma,
                &mut rng,
                transcript,
            )
        })
        .collect::<Result<Vec<_>, _>>()?;

line 500 up to 486. .advice_evals , these are commitments. .advice_queries ?? commitments minus the evaluations.

line 551 IS the ? ILC part? Sum chain the query together with a random coefficient.

From line 551 in prover.rs

    let instances = instance
        .iter()
        .zip(advice.iter())
        .zip(permutations.iter())
        .zip(lookups.iter())
        .flat_map(|(((instance, advice), permutation), lookups)| {
            iter::empty()
                .chain(
                    pk.vk
                        .cs
                        .instance_queries
                        .iter()
                        .map(move |&(column, at)| ProverQuery {
                            point: domain.rotate_omega(*x, at),
                            rotation: at,
                            poly: &instance.instance_polys[column.index()],
                        }),
                )
                .chain(pk.vk.cs.advice_queries.iter().map(move |&(column, at)| {
                    ProverQuery {
                        point: domain.rotate_omega(*x, at),
                        rotation: at,
                        poly: advice
                            .advice_polys
                            .as_ref()
                            .unwrap()
                            .get(column.index())
                            .unwrap(),
                    }
                }))
                .chain(permutation.open(pk, x))
                .chain(lookups.iter().flat_map(move |p| p.open(pk, x)).into_iter())
        })
        .chain(
            pk.vk
                .cs
                .fixed_queries
                .iter()
                .map(|&(column, at)| ProverQuery {
                    point: domain.rotate_omega(*x, at),
                    rotation: at,
                    poly: &pk.fixed_polys[column.index()],
                }),
        )
        .chain(pk.permutation.open(x))
        // We query the h(X) polynomial at x
        .chain(vanishing.open(x));