modern snark system is modularized: functional commitment + interactive oracle proof
**funtional commitment**: commit and eval function value efficiently (faster than O(d)). includes vector commitment, multilinear commitment, poly commitment, inner product commitment, etc.
**interactive oracle proof**: a proof system where verifier sends prover public coin(public randomness) and verifier sends proof oracle of a function. **Oracle** here stands for a trusted third party for the verifier to query value of the function. Oracle guarantees the function it serves meets the requirement(e.g. polynomial with degree < d) and the query result is computed correctly.

**Functional commitment is a SNARK on function evaluation and proves f(x) = y. IOP extends functional commitment to a SNARK on any arithmetic circuit C and proves C(x, w) = 0.**

[zk application landscape](https://archive.devcon.org/resources/6/zk-application-design-patterns.pdf)
**privacy requires prover to run in an environment trusted by the user, which means we can't leverage large computation power provided by the cloud or customized hardware.**

succint requires efficient, blockchain compatible verifier. for example, ethereum only supports BN254.
**recursion and aggregation is used to generate bigger proof on multiple circuits and balance the cost of verifier / prover.**

[recursive SNARKs](https://zk-learning.org/assets/lecture10.pdf):
Snarks can be combined to prove knowledge of a proof, to combine strengths of different proving system.
applications:
1. proof compression
2. streaming proof generation
3. zk-rollup
4. incrementally verifiable computation(IVC)
5. a market for zk provers

since prover runs verifier circuit, curves need to be carfully chosen to make proving systems compatible.

**folding, used by Nova, is used to compress two instances(statement to be proved) into one.**

folding scheme is a cryptographic primitive that reduces the task of checking two NP statements into the task of checking a single NP statement.

Nova uses relaxed R1CS + homomorphic function commitment scheme that supports addition.
folding is applied to IVC
folding is much faster than proving SNARK verification
SuperNova extends Nova to different functions at each step, Sangira extends Nova to any quadratic constraint system.

**Halo is the first practical example of recursive proof composition without a trusted setup, using the discrete log assumption over normal cycles of elliptic curves.**

The choice of an arithmetization and a front-end for writing in that arithmetization is the closest thing to choosing a programming language in ZK.

In the real world, after you have designed your [hardware] circuit its performance is governed by the laws of physics. In ZK, circuit performance is governed by the laws of math, and polynomial commitment schemes specify which laws apply.

KZG commitment scheme:
KZG eval:
KZG uses property of bilinear pairing to verify relationship between commited polynomials.

KZG support batch proofs, linear time commitment and multi-point proof generation.
proof gadgets:
trick for product check: **note that unlike product check and zero check, prover needs randomness from verifier to construct commitment to a polynomial**
trick for permutation check:
Plonk encodes the permutation trace as polynomial:
S is selector polynomial to encode gate type.
Hyperplonk works on cube space and multilinear polynomial, prover time reduce from O(dlogd) to O(d).
plonkish arithmetization supports custom gates:
Plonkup supports set check for values encoded.

Copy constraints enable a designer to abstract away explicitly thinking about the execution trace and PAIR, and rather design a program like this: We have a set of witness variables, whose value can only be set once in the program.
We choose at each step what gate to apply on which variables.

## Notes on axiom-lib
`Context` can roughly be thought of as a single-threaded execution trace of a program we want ZK to prove.
A `QuantumCell` is a convenience enum we have introduced because there are several slightly different scenarios under which you want to add a value into the advice column.

The `ctx.assign_region` function can be thought of as a low-level function to write assembly-level code.

GateChip and RangeChip, range check uses look up table.

For a big computation, the number of rows in this table will get very large. For the Prover, this means they need to perform certain operations on a very large vector (column). These operations include Fast Fourier Transform and certain elliptic curve operations (multi-scalar multiplication). For performance, it is generally faster to parallelize such operations across multiple vectors of shorter length instead of a single large vector.

more columns --> more polynomial with lower degree --> faster prover --> slower verifier

**halo-lib implements an arithemtization model with simplier constraints, which is easier to use and improves developer velocities.**

halo2-base crate provides an additional API for writing circuits in Halo 2 using our simple vertical gate.

what's the difference between base field and scalar field for an elliptical curve?

While circuit design involves just filling out a table using some front end, to actually create a proof there is a backend that takes the PLONK table above and does a bunch of computations involving polynomial commitment schemes. This part is largely independent of the circuit design, but different backends lead to different performance characteristics, which become important to understand for production use cases.

**plonkish circuit design mental model**:
1. assert values at certain cells(for public input and output match verification)
2. define copy constraints / permutation / wire
3. fill in witness value for each cell

lookup tables:
In normal programs, you can trade memory for CPU to improve performance, by pre-computing and storing lookup tables for some part of the computation. We can do the same thing in halo2 circuits! A lookup table can be thought of as enforcing a relation between variables, where the relation is expressed as a table. Assuming we have only one lookup argument in our constraint system, the total size of tables is constrained by the size of the circuit: each table entry costs one row, and it also costs one row to do each lookup.

plonkish arithmetization:
Table columns are used for lookup tables: this is a powerful feature (and our primary reason for using Halo2). can also perform lookup arguments on tuples of advice values.

There are different ways to represent the execution trace as vectors + constraints, these are called arithmetizations. Nowadays there are “front-ends” with different levels of abstraction and customizability for translating a ZK circuit into an arithmetization.

prover, verifier dynamic:

**AIRs** - Algebraic Intermediate Representations:
**PAIRs** - AIRs with preprocessed columns:
predefined columns are often refereed to as selectors.

**RAPs** - PAIRs with interjected verifier randomness.
Our final model allows rounds of interaction, where the verifier sends random field elements, and the prover can subsequently add more columns after seeing these field elements. The constraint polynomials will now be able to use the verifier randomness as additional variable to prove, for example, permutation check.

A turbo-plonk program is a PAIR with the extra ability to define copy constraints between any two elements of the execution trace.

program in turbo-plonk:

**limitation on R1CS**:
As we currently have at our disposal cryptographic k-linear maps only for k = 2 via elliptic curve pairings), R1CS is truly the most general form of constraints these protocols can work with.

However the polynomial IOP approach to constructing SNARKs, that perhaps explicitly started with Sonic, enables a more flexible constraint format. In particular, it is possible to use constraints of degree larger than two.

On proving systems:

**Challenge**: to keep gates linearly independent
Groth16 bakes permutation check into trusted setup

random challenges are for Fiat-Shamir transformation:

### axiom halo2 implementation
bits_to_indicator is built through recursion, build b1..bn first, then add bo and build representation for b0b1..bn.

**why we need const generics for gate functions?**

**Copy of the assigned value should only be used when you are about to assign the value again elsewhere.**
Why? How Rust Clone / Copy works, how AssignedValue works, how Rust iterator works. What happens if we make extra copy of AssignedValue, does it affect performance?

Using RangeChip is tricky, need to make sure environment variables LOOKUP_BITS and DEGREE are set up correctly.

relationship of the xxBuilder in builder.rs of halo2-base:
**GateThreadBuilder** stores contexts(execution traces), and has functions like assign_all and assign_threads_in to assign values to contexts.

**GateCircuitBuilder** contains GateThreadBuilder.

**GateCircuitBuilder** implements trait Circuit.

Random linear combinations (RLCs) can be used to improve circuit efficiency.

breakpoint breaks one column into multiple column to reduce number of rows.

In this case we sometimes refer to a set of constraints controlled by a set of selector columns that are designed to be used together, as a gate.

Gates --> Region --> Chips --> Gadgets / Circuits
# references
on plonk arithmization:
https://hackmd.io/@aztec-network/plonk-arithmetiization-air#fn1
https://zcash.github.io/halo2/index.html
https://docs.axiom.xyz/zero-knowledge-proofs/getting-started-with-halo2
https://github.com/fluidex/awesome-plonk
https://o1-labs.github.io/proof-systems/plonk/overview.html
https://hackmd.io/RtzxBTTgTaur0YIUoOiULw (linked to lots of good resources)
https://research.metastate.dev/plonk-by-hand-part-1/

on Halo2:
https://learn.0xparc.org/halo2/
https://hackmd.io/@axiom/HyoXzD7Zh (halo2 cheatsheet)
https://hackmd.io/@axiom/SJw3p-qX3 (halo2 challenge API and RLC)
https://hackmd.io/@arielg/ByFgSDA7D (multiset check used for lookup table)
https://docs.google.com/presentation/d/1UpMo2Ze5iwzpwICPoKkeT04-xGFRp7ZzVPhgnidr-vs/edit#slide=id.p(slides about halo2, plonkish arithmetization, IPA, accumulation(recursive zk))
https://learn.0xparc.org/materials/halo2/learning-group-1/halo2-api (live coding session on Halo2)

on plonk lookup:
https://hackmd.io/@arielg/ByFgSDA7D

on proving systems:
https://hackmd.io/@jpw/BJAf6spB9 (zk proving system)
https://twitter.com/SrikarVaradaraj/status/1521188996147290117
https://www.youtube.com/watch?v=tGaD8qpQi6c&ab_channel=0xPARCFoundation(Ye Zhang's talk on proving system)