šŸŸLab: Chips

Time to write some code relating to the previous theory

Create a new file where you want to build your circuit, let's call ours TutorialCircuit.rs.

You may want to preemptively import the following items:

use std::marker::PhantomData;
use halo2_proofs::circuit::Value;
use halo2_proofs::{
    arithmetic::FieldExt,
    circuit::{Cell, Chip, Layouter, SimpleFloorPlanner},
    plonk::{Advice, Assigned, Circuit, Column, ConstraintSystem, Error, Fixed, Instance},
    poly::Rotation,
};

To recap, the steps were:

  1. Decide what functionality you want in the chip, and thus pick an equation that allows you to provide that functionality (for now we are just using the original plonk equation).

  2. Create a struct _Config that will wrap up all the columns you will need in your chip, and define their types.

  3. Wrap the previous struct up with _marker: PhantomData in something generically named _Chip.

  4. Create a trait to be implemented on your chip (can simply be called _Composer), putting all the gate types you will want to see as functions. Include any other functionality you will want on your chip that are algebraically possible (based on the equation you chose).

Let us go through them one by one. The first step is actually very theoretical and very hard; we should dig into how to do this ourselves later. For now we want to focus on building chips, so let's just assume we are trying to implement the basic plonk scheme - the equation was provided in the last section, and functionality-wise we will have addition, multiplication, copy constraints and public input gates.

Task 1

Implement your config as a struct. Remember, this is where we will define all the columns that we will need. The equation we had was

lā‹…sl+rā‹…sr+(lā‹…r)ā‹…smāˆ’oā‹…so+sc+PI=0.l\cdot s_l + r\cdot s_r + (l\cdot r)\cdot s_m - o\cdot s_o + s_c + PI = 0.

How many columns do we need? What type should each column be?

Task 2

We now need to wrap the config up into the chip struct along with marker.

Task 3

Implement the function new on the chip struct - this function should take in a config and produce a chip.

Task 4

Finally we want to create a trait that will contain all the functions we need to represent the gates. You can call this trait something like TutorialComposer. We haven't covered everything we need to fill in this trait very well yet (there is a lot to cover if you want to use this repo, we appreciate your patience with us).

We will define

trait TutorialComposer<F: FieldExt> {
fn raw_add<FM>()
fn raw_multiply<FM>()
fn copy()
fn expose_public()
}

To define a gate functions inputs and outputs, we will usually have something as so:

fn raw_add<FM>(
    &self,
    layouter: &mut impl Layouter<F>,
    f: F,
) -> Result<(Cell, Cell, Cell), Error>
where
    FM: FnMut() -> Value<(Assigned<F>, Assigned<F>, Assigned<F>)>;

Briefly, a Cell refers to a single location in the table of values we are building, such as one of the entries of r or one of the entries of s_o. Specifically it doesn't hold the value of that entry, but it holds a pointer that indicates which row of which column to refer to. The Layouter is a tool within the repo that helps us build the gates properly; we will cover it in due time.

The example given to you above is how we would define the addition gate.

  • Can you do something similar to define the multiplication gate?

  • Can you change some pieces to create the copy gate?

  • Can you do something similar for the expose public gate?

Recap

Well done! Thank you for making it through those. Let's be honest here - mostly what you will have done in this lab is one of copy&paste, or be frustrated. There is still a lot going on that we need to cover. I mean in order to define the trait we had to give you things without being able to tell you much about them at all. That is okay for now. We appreciate your patience; and remember, frustration is the essence of learning.

What we do want you to recall from this lab is the steps:

  1. Define your config

  2. Wrap your config with some marker in a struct (and build a new() for it)

  3. Define a trait that will contain the functionality you want in your chip, thinking carefully about what each function (each function will usually represent a gate, except for example copy) should have as input or output

  4. Implement those composer functions on your chip

Last updated