# Halo2 Frontend: Expression, Calculation And Its Evaluation

>The limits of my language mean the limits of my world.

--Ludwig Wittgenstein, Tractatus logigo-philosphicus, 1922

Language model shapes our mind. A language design carves us how to think a problem, how to present the idea to others and how to deconstruct a statement to understand its ingredients. Will you think in same way when speaking Chinese and English? Are you able to write same style of codes in Lisp and C? From Wittgenstein, the surface of meaning of language, and its underlying 'unspoken' implication are bounded by boundary of language itself.

Our journey of Halo2 starts here. Undoubtly Halo2 converts what programmers would like to state, to a probablity check of a Boolean satisfiability problem(SAT). But what can we actually do, within the scope of Halo2, while what we can't? And what's the transition between the inital state and the end? This article tries to present our readers a clue what enables the expression of statement.

## A simple example
Let's examine an examle. Here, a multiplication gate is given.

meta.create_gate("mul", |meta| {
  // To implement multiplication, we need three advice cells and a selector
  // cell. We arrange them like so:
  //
  // | a0  | a1  | s_mul |
  // |-----|-----|-------|
  // | lhs | rhs | s_mul |
  // | out |     |       |
  //
  // Gates may refer to any relative offsets we want, but each distinct
  // offset adds a cost to the proof. The most common offsets are 0 (the
  // current row), 1 (the next row), and -1 (the previous row), for which
  // `Rotation` has specific constructors.
  let lhs = meta.query_advice(advice[0], Rotation::cur());
  let rhs = meta.query_advice(advice[1], Rotation::cur());
  let out = meta.query_advice(advice[0], Rotation::next());
  let s_mul = meta.query_selector(s_mul);

  // Finally, we return the polynomial expressions that constrain this gate.
  // For our multiplication gate, we only need a single polynomial constraint.
  //
  // The polynomial expressions returned from `create_gate` will be
  // constrained by the proving system to equal zero. Our expression
  // has the following properties:
  // - When s_mul = 0, any value is allowed in lhs, rhs, and out.
  // - When s_mul != 0, this constrains lhs * rhs = out.
  vec![s_mul * (lhs * rhs - out)]
});

Referrence [here](https://github.com/zcash/halo2/blob/main/halo2_proofs/examples/simple-example.rs).

In config gate, we define a customized constraint -- we constrain that the left hand side at the current row multiply right hand side of current row shall be equal to the next row of left hand side column, whenever `s_mul` is on. This is the gate both prover and verifier have consensus before any proof has been given. Once the witness being populated, this gate will convert to SAT problem and an assetion `lhs * rhs - out == 0` on table must be checked wherever selector indicates that the constraint shall be honored.

Later, in the main function, we have to build the "full stack" to convert the constraint, along with witness, to a succinct proof that verifier can verify with minimal effor. That includes:

// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
    constant,
    a: Value::known(a),
    b: Value::known(b),
};

// How many spaces shall we take?
// Equivalently, how many rows are needed? 2^k 
let params = ParamsKZG::<Bn256>::setup(k, OsRng);

// Prepare verifier key
let vk = keygen_vk(&params, &circuit).expect("vk should not fail");

// Prepare prover key
let pk = keygen_pk(&params, vk, &circuit).expect("pk should not fail");

// Prepare instance
let instances: &[&[Fr]] = &[&[c]];

// Init a transcript for proof generation
let mut transcript = Blake2bWrite::<_, _, Challenge255<_>>::init(vec![]);

// Generate proof
create_proof::<
  KZGCommitmentScheme<Bn256>,
  ProverGWC<'_, Bn256>,
  Challenge255<G1Affine>,
  _,
  Blake2bWrite<Vec<u8>, G1Affine, Challenge255<_>>,
  _,
>(
  &params,
  &pk,
  &[circuit],
  &[instances],
  OsRng,
  &mut transcript,
)
.expect("prover should not fail");

Full example could be seen [here](https://github.com/LiuJiazheng/halo2/blob/example/halo2_proofs/examples/example_real_commit.rs).

"Well there is no check enforced" one may argue. Simply from the process of proof generation, no, we cannot see any. However, as mentioned just few lines before, as a consensus that both prover and verifier know, this kind of infomation has been embedded into the whole process of proof generation. Next, we will go into the compiling stack and show that the constraint, indeed, takes effects.

## Formation of `Expression`, as abstract syntax tree
In `keygen_vk`, a call stack is going as follow:

example_real_commit::FieldChip<F>::configure(meta=0x000000016fdfab60, advice=[halo2_proofs::plonk::circuit::Column<halo2_proofs::plonk::circuit::Advice>; 2] @ 0x000000016fdfaac0, instance=(index = 0, column_type = halo2_proofs::plonk::circuit::Instance @ 0x000000016fdfaa38), constant=(index = 0, column_type = halo2_proofs::plonk::circuit::Fixed @ 0x000000016fdfaa40)) at example_real_commit.rs:90:9
<example_real_commit::MyCircuit<F> as halo2_proofs::plonk::circuit::Circuit<F>>::configure(meta=0x000000016fdfab60) at example_real_commit.rs:268:9
halo2_proofs::plonk::keygen::create_domain(k=4) at keygen.rs:42:18
halo2_proofs::plonk::keygen::keygen_vk(params=0x000000016fdfcba8, circuit=0x000000016fdfca70) at keygen.rs:216:32

`keygen_vk` is the first step of this process. Recall the topic we are presenting --- if we regard Halo2 as a compiler, that would be first pass of compilation --- we will parse the "syntax", i.e., constraints, to another data structure that is easy for further operation. `keygen_vk` does not need concrete value of witness(neither does `keygen_pk`), instead, it sets placeholders for those values. Creating domain, parsing all gates and lookup table, reserving spaces, leaving a framework for further operation, that's basicly covering all elements inside the function.

Now, after a closer examination, one might find `create_domain` is the first step of `keygen_vk`, where `configure` is called, and a closure of user-defined constraits function has been feed in.

Back to the gate we gave in last section.
`let lhs = meta.query_advice(advice[0], Rotation::cur());`
Here lhs is an `Expression`. Again, in this step, no actual data is given. All this gate needs is relative location in such a 2-dimentional table: which column is quried? `Advice[0]`. Which row is involved in a row-wise constraint? `Current row and next row`.

Just like a symbol in other programming language, a query on (column, row) of table(or say, constraint system) does not necessarily birng a value associated with it. It provides a query pattern about how to load data onto it: if witness given and selector is on, column x and row y shall be queried and data loaded based on that, then doing arithmetics and check wheter the expression turns to zero.

`lhs`, `rhs` and `out` are all `Expression` and here goes the defination of `Expression`:

pub enum Expression<F> {
    /// This is a constant polynomial
    Constant(F),
    /// This is a virtual selector
    Selector(Selector),
    /// This is a fixed column queried at a certain relative location
    Fixed(FixedQuery),
    /// This is an advice (witness) column queried at a certain relative location
    Advice(AdviceQuery),
    /// This is an instance (external) column queried at a certain relative location
    Instance(InstanceQuery),
    /// This is a challenge
    Challenge(Challenge),
    /// This is a negated polynomial
    Negated(Box<Expression<F>>),
    /// This is the sum of two polynomials
    Sum(Box<Expression<F>>, Box<Expression<F>>),
    /// This is the product of two polynomials
    Product(Box<Expression<F>>, Box<Expression<F>>),
    /// This is a scaled polynomial
    Scaled(Box<Expression<F>>, F),
}

Let's only focus on an arithematic:
`Sum(Box<Expression<F>>, Box<Expression<F>>)`. It is simply a recursive expression of itself. Does this remind you something? Right, this is an **abstract syntax tree**(AST), essentially.

And the final constraint expression:
`s_mul * (lhs * rhs - out)` is not a numerical expression, but a symbolic one:

In `curcit.rs`, an multipilcation of `Expression` is defined as follow:

impl<F: Field> Mul for Expression<F> {
    type Output = Expression<F>;
    fn mul(self, rhs: Expression<F>) -> Expression<F> {
        if self.contains_simple_selector() && rhs.contains_simple_selector() {
            panic!("attempted to multiply two expressions containing simple selectors");
        }
        Expression::Product(Box::new(self), Box::new(rhs))
    }
}

As it shows, two `Expression` get involves and returns a new `Expression`. Knowing this, we can manually parse expression `s_mul * (lhs * rhs - out)` to a AST:

        Product
  /                \
Selector         Sum
  |            /          \
Selector     Product    Negated
              /   \         |
           Advice Advice   Advice

Here we omit the attribute of each advice and selector.
You can see each the actual non-recurisve element is `Advice`/`Fix`/`Selector` etc. They represents a real "read" operation in system. Others are more like a operation which needs basic bricks. Each constraints would have such `Expression` and a gate could possess multiple contraints, and a constraint system is able to hold multiple gates. As a result, there would be multiple contraints stored `ConstraintSystem`.

pub struct ConstraintSystem<F: Field> {
    ...
    pub(crate) gates: Vec<Gate<F>>,
    ...
}

pub struct Gate<F: Field> {
    name: String,
    constraint_names: Vec<String>,
    polys: Vec<Expression<F>>,
    ...
}

## Parsing `Expression`, caching in `Calculation` SSA
In last section, we reveal how a contraint written by user parsed as an `Expression` stored in `ConstraintSystem`. However as we all know, AST is an intermediate representation and cannot be used directly. The journey must go on.

In this section, we will study logics related with AST `Expression` in function `keygen_pk`, to track down what's going to be for an `Expression` as IR.

`keygen_pk` follows `keygen_vk`. As name suggests, it is for generating all related data associated with prover in order to get a proof. It has similar logic of `keygen_vk`. One of reasons for designing duplicate functionalities might be Halo2 cannot assume proof key and verifier key can be generated within same machine and same program. So to safely get key for prover, it'd better do similar things again: create domain, configure gates(get `Expression`), prepare some auxilary data and so on.

Nothing new up to now. However in the last procedure in `keygen_pk`, things change. A new object is created and added into `ProvingKey` later:

let ev = Evaluator::new(&vk.cs);

Follow the backtrace. In `Evaluator::new` we have

let mut parts = Vec::new();
for gate in cs.gates.iter() {
    parts.extend(
        gate.polynomials()
            .iter()
            .map(|poly| ev.custom_gates.add_expression(poly)),
    );
}

At first glance, this evaluator processes all constraints cached in constraint system.

fn add_expression(&mut self, expr: &Expression<C::ScalarExt>) -> ValueSource {
...
Expression::Product(a, b) => {
    let result_a = self.add_expression(a);
    let result_b = self.add_expression(b);
    ...
    else if result_a <= result_b {
       self.add_calculation(Calculation::Mul(result_a, result_b))
    } else {
       self.add_calculation(Calculation::Mul(result_b, result_a))
    }
}
...

We extract the core logic here. The function `add_expression` parse left and right operand, **recursively**, calls `add_calculation` and returns a `ValueSource`. It is clear: `add_expression` is doing a **postorder traverse** on each `Expression` AST, and returns another intermediate representative.

Now questions become, what is the `ValueSource` and what is `Calculation`?

pub enum Calculation {
    /// This is an addition
    Add(ValueSource, ValueSource),
    /// This is a subtraction
    Sub(ValueSource, ValueSource),
    /// This is a product
    Mul(ValueSource, ValueSource),
    /// This is a square
    Square(ValueSource),
    /// This is a double
    Double(ValueSource),
    /// This is a negation
    Negate(ValueSource),
    /// This is Horner's rule: `val = a; val = val * c + b[]`
    Horner(ValueSource, Vec<ValueSource>, ValueSource),
    /// This is a simple assignment
    Store(ValueSource),
}

/// Value used in a calculation
pub enum ValueSource {
    /// This is a constant value
    Constant(usize),
    /// This is an intermediate value
    Intermediate(usize),
    /// This is a fixed column
    Fixed(usize, usize),
    /// This is an advice (witness) column
    Advice(usize, usize),
    ...
}

    /// Adds a calculation.
    /// Currently does the simplest thing possible: just stores the
    /// resulting value so the result can be reused  when that calculation
    /// is done multiple times.
    fn add_calculation(&mut self, calculation: Calculation) -> ValueSource {
        let existing_calculation = self
            .calculations
            .iter()
            .find(|c| c.calculation == calculation);
        match existing_calculation {
            Some(existing_calculation) => ValueSource::Intermediate(existing_calculation.target),
            None => {
                let target = self.num_intermediates;
                self.calculations.push(CalculationInfo {
                    calculation,
                    target,
                });
                self.num_intermediates += 1;
                ValueSource::Intermediate(target)
            }
        }
    }

This one gives more hints. It finds whether a particualr calculation pattern is available, if found, return that object, if not, make a new pattern and push it inside as a side effect.

`ValueSource` is an abstract telling you where to find a value in a table. For example `Advice (0,1)` tells Halo2 to fetch frist column of advice table, with offset 1, which means 'the next line' of current cursor. And `Calculation` is a legit abstract of real calculation, you cannot do calculation on AST, it is way far complicated, but you can do calcualation on simple arithematic like add or mul. How can we achieve this? By postorder traverse on a tree, cache every piece that needs calculation and when the traverse ends, the actual excution plan of such AST has been generated as well.

By parsing our example, you might get an exculation plan like:

0 CalculationInfo { calculation: Store(Fixed(1, 0)), target: 0 }
1 CalculationInfo { calculation: Store(Advice(0, 0)), target: 1 }
2 CalculationInfo { calculation: Store(Advice(1, 0)), target: 2 }
3 CalculationInfo { calculation: Mul(Intermediate(1), Intermediate(2)), target: 3 }
4 CalculationInfo { calculation: Store(Advice(0, 1)), target: 4 }
5 CalculationInfo { calculation: Sub(Intermediate(3), Intermediate(4)), target: 5 }
6 CalculationInfo { calculation: Mul(Intermediate(0), Intermediate(5)), target: 6 }
7 CalculationInfo { calculation: Horner(PreviousValue, [Intermediate(6)], Y), target: 7 }

Note that index 3, the mul is dependent on itermediate result 1 and 2. This order cannot mutate. And index 7 is using Horner rule to do a single point evaluation.

Does above calculation list reminds you someting? Yes, it is quite similar to **single static assignment** form (SSA). Here, an AST is reduced to a sequence of execution plan, yet, no single data is calculated. It is just provides a calculation pattern so that no matter what kind of data feed in, evaluator would give the final numerical answer based on the pattern it knows. In this level, all operations are reduced to either a store instruction on a particular table, or, a arithematic operation based on previous cached result.

Thus, prover key knows more than verifier key by processing AST and stores the SSA excution plan in its own cacheline. This is pretty intuitive --- prover definitely needs to know "what to compute on domain" while verifier only needs where to open (the commitment) and verify.

## Evaluation, where SSA terminates
Up to now, we have mentioned `keygen_vk` and `keygen_pk`, yet no actual calculation on elliptic curve fields at all. And finally we will go inside `create_proof`. Again, the full interpretation is out of scope of this article --- we only track down how those `Calculation` lists being used in proof generation.

Recall the PLONK protocol, one critical step is quotient polynomial evaluation. In function, this is at `Evaluator::evaluate_h`, where all customized gates, lookups and permutations would be evaluated, of which become a portion of final evulation of h polynomial on domain.

For all gates:

for (i, value) in values.iter_mut().enumerate() {
  let idx = start + i;
  *value = self.custom_gates.evaluate(
  &mut eval_data,
  fixed,
  advice,
  instance,
  ...
  );
}

gets evaluated and detailedly,

    pub fn evaluate<F: Field, B: Basis>(
        &self,
        rotations: &[usize],
        constants: &[F],
        intermediates: &[F],
        fixed_values: &[Polynomial<F, B>],
        advice_values: &[Polynomial<F, B>],
        instance_values: &[Polynomial<F, B>],
        challenges: &[F],
        beta: &F,
        gamma: &F,
        theta: &F,
        y: &F,
        previous_value: &F,
    ) -> F {
        let get_value = |value: &ValueSource| {
            value.get(
                rotations,
                constants,
                intermediates,
                fixed_values,
                advice_values,
                instance_values,
                challenges,
                beta,
                gamma,
                theta,
                y,
                previous_value,
            )
        };
        match self {
            Calculation::Add(a, b) => get_value(a) + get_value(b),
            Calculation::Sub(a, b) => get_value(a) - get_value(b),
            Calculation::Mul(a, b) => get_value(a) * get_value(b),
            Calculation::Square(v) => get_value(v).square(),
            Calculation::Double(v) => get_value(v).double(),
            Calculation::Negate(v) => -get_value(v),
            Calculation::Horner(start_value, parts, factor) => {
                let factor = get_value(factor);
                let mut value = get_value(start_value);
                for part in parts.iter() {
                    value = value * factor + get_value(part);
                }
                value
            }
            Calculation::Store(v) => get_value(v),
        }
    }

In this function, all values are given as referrence. Then based on the calculation cached processed by `keygen_pk`, value gets calculated step by step and gets the final evaluation of polynomial. And this, is a real value representive of points on scalar field of elliptic curve.

The quotient poly evalutes on each points of domain. In the end, you will get a buffer with domain size. After an inverse FFT, `Polynomial<C::ScalarExt, ExtendedLagrangeCoeff>` will be returned. And that's the full cycle from a constraint to a quotient poly, which would be used to generate real proof.

## Reflect: Why has to be AST?
The most direct answer is, because Halo2 is in PLONKish style, not a standard plonk. As a comparison, ZkGarage's [PLONK](https://github.com/ZK-Garage/plonk) is a standard plonk and you can see user can only configure it with bricks like add, mul and so on. There is no need for complex syntax structure parser.

On the contrary, Halo2 supports "customized gate", which allows user to define nearly any kind of polynomial constraints (In fact, there is guildline that you should not compose higher order poly because that would be expensive when doing FFT --- break that down to several low degree constraints). Parsing such constraints inevitably requires AST. So the question essentially is: if not this, then what alternative?

## Ending
I hope you've enjoyed this journey with us. We began with an example, delved into the keygen for the verifier, moved on to the prover, and finally arrived at proof generation. Drawing parallels with a compiler syntax parser, we aimed to help readers understand the transition from a 'customized constraint' to its proof. In our next episode, we'll explore the 'backend' of the Halo2 compiler, focusing on IOP and the Commit Scheme. Until then.