mirror of
https://github.com/privacy-scaling-explorations/chiquito.git
synced 2026-01-09 14:08:03 -05:00
Steve/issue 5 readme (#12)
see commit message :) Please read fibonacci example from files changed of this PR. The link in README refers to main which doesn't include changes yet API doc links are deployed from fork, and will be re-deployed from main once docs are approved and merged --------- Co-authored-by: Steve Wang <qwang97@wharton.upenn.edu> Co-authored-by: Chih Cheng Liang <chihchengliang@gmail.com>
This commit is contained in:
82
Appendix.md
Normal file
82
Appendix.md
Normal file
@@ -0,0 +1,82 @@
|
||||
# Appendix
|
||||
|
||||
## Design Principles
|
||||
|
||||
**Abstraction**. As circuit complexity increases, abstraction is inevitable. By abstracting constraint building and column placement, Chiquito improves the readability and learnability of Halo2 circuits, which can not only standardize and simplify the code base for complex projects such as the zkEVM, but also onboard more circuit developers.
|
||||
|
||||
**Composability**. Chiquito circuits are fully composable with Halo2 circuits, which allows developers to write any part or the entirety of a circuit in Chiquito and integrate with other Halo2 circuits.
|
||||
|
||||
**Modularity**. The AST and IR representations of a circuit allow Chiquito to integrate any frontend that can compile into the AST data structure and any backend that can compile from the IR data structure. For example, we can have a Python frontend that compiles to Chiquito AST/IR, which compiles to a Sangria backend. Modularity allows for future extensions.
|
||||
|
||||
**User Experience**. Chiquito simplifies and optimizes user experience. For example, annotations for constraints are automatically generated for debugging messages.
|
||||
|
||||
## Architecture
|
||||
|
||||
There are two major architectural differences between Chiquito and Halo2:
|
||||
|
||||
- Chiquito circuit is composed of “step” instances. Each step type defines the constraints among witnesses, fixed columns, and lookup tables. Step instances are also called “super rows”, each composed of one or multiple rows in a PLONKish table. We made this design choice to allow for more complex constraints, which sometimes require allocating multiple Halo2 rows.
|
||||
- Chiquito DSL is based on “signals” rather than columns in order to abstract away column placements. One signal can be placed in different columns across different steps, all handled by Chiquito’s compiler.
|
||||
|
||||
Chiquito circuit has the following architecture
|
||||
|
||||
- Circuit (with optional input from Halo2)
|
||||
- Forward signals (signals with constraints across different steps)
|
||||
- Fixed columns
|
||||
- Step types
|
||||
- Internal signals (signals with constraints only within one step)
|
||||
- Internal constraints (constraints for internal signals only)
|
||||
- Transition constraints (constraints involving forward signals)
|
||||
- Witness generation function for one step type instance
|
||||
- Trace (global circuit witness generation)
|
||||
- Adds instances of step types
|
||||
|
||||
## Overall Workflow
|
||||
|
||||
Chiquito is a DSL that compiles Chiquito AST to an IR which can be parsed by a Chiquito Halo2 backend and integrated into a Halo2 circuit. Therefore, to create a Halo2 circuit using Chiquito, we need to:
|
||||
|
||||
- Call `circuit` function in DSL, which returns an `ast::Circuit` object. The `circuit` function defines the `ast::Circuit` object by:
|
||||
- Importing Halo2 columns
|
||||
- Generating fixed columns
|
||||
- Adding forward signals
|
||||
- Defining and instantiating “steps”, which defines internal signals, constraints, lookups, and witness generation
|
||||
- Create a `Compiler` object that compiles the `ast::Circuit` object to an `ir::Circuit` object
|
||||
- Call `chiquito2Halo2` function in Halo2 backend to convert the `ir::Circuit` object to a `ChiquitoHalo2` object
|
||||
- Integrate `ChiquitoHalo2` object into a Halo2 circuit by including it in the Halo2 circuit config struct
|
||||
- Call `configure` and `synthesize` functions defined in the Halo2 backend on the `ChiquitoHalo2` object
|
||||
|
||||
## Exposed User Functions
|
||||
|
||||
The above section describes the high level process of building and integrating a Chiquito Halo2 backend object into a Halo2 circuit. However, when building a circuit using Chiquito, the developer mostly call DSL functions to manipulate the `ast::Circuit` object.
|
||||
|
||||
DSL functions are defined on five different levels, with nested relationships:
|
||||
|
||||
- Circuit level: define and manipulate circuit-level objects, such as forward signals, step types, fixed columns, and imported Halo2 columns
|
||||
- Step type level: define and manipulate step-specific objects, such as internal signals, constraints, witness generations
|
||||
- Witness generation level: allow user-defined Turing-complete function to manipulate witness generation inputs and assign witness values
|
||||
- Fixed column generation level: allow user-defined Turing-complete function to manipulate fixed column generation inputs and assign fixed column values
|
||||
- Trace level: create the main circuit by instantiating step types; allow user-defined Turing-complete function to manipulate external trace inputs and assign input values to step type instances
|
||||
|
||||
## Project Status (as of April 2023)
|
||||
|
||||
The current implementation includes:
|
||||
|
||||
- A DSL in Rust
|
||||
- A backend in Halo2
|
||||
- Composability with Halo2 circuits
|
||||
- A working prototype that passes zkEVM bytecode circuit tests
|
||||
- Hashing function circuit examples
|
||||
|
||||
## Vision and Next Steps
|
||||
|
||||
Modularity
|
||||
|
||||
- Expand frontend to other programming languages, e.g. Python
|
||||
- Integrate additional backends and proof systems
|
||||
|
||||
Library
|
||||
|
||||
- Add additional circuit examples
|
||||
|
||||
Infrastructure
|
||||
|
||||
- Cmd tool and npm package for developers
|
||||
56
README.md
56
README.md
@@ -1,2 +1,56 @@
|
||||
# Chiquito pecador plonkish
|
||||
# Chiquito
|
||||
|
||||
# Project Description
|
||||
|
||||
Chiquito is a high-level DSL that provides syntax sugar and abstraction for constraint building and column placement when writing Halo2 circuits. It allows the user to manipulate an AST that’s compiled to a Chiquito Halo2 backend, which can be integrated into any Halo2 circuit.
|
||||
|
||||
It's **HIGHLY RECOMMENDED** that you read the [design principles](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#design-principles), [architecture, and specific terms](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#architecture) of a Chiquito circuit before getting started.
|
||||
|
||||
You can also learn about the project's [current status](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#project-status-as-of-april-2023)) and its [next steps](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#vision-and-next-steps).
|
||||
|
||||
# Getting Started
|
||||
|
||||
## Setup
|
||||
Run the following in command line to add Chiquito as a dependency for your project:
|
||||
```
|
||||
cargo add --git https://github.com/privacy-scaling-explorations/chiquito
|
||||
```
|
||||
|
||||
Use the following examples to understand how Chiquito works or use them as starting templates for building your own Chiquito circuit.
|
||||
|
||||
Refer to the Appendix on the [exposed user functions](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#exposed-user-functions) and [overall workflow](https://github.com/privacy-scaling-explorations/chiquito/blob/main/Appendix.md/#overall-workflow) of a Chiquito circuit.
|
||||
|
||||
Refer to [Testing and Links](#testing-and-links) on detailed API documentations.
|
||||
|
||||
|
||||
## Example: Fibonacci Circuit
|
||||
Run the following in command line:
|
||||
```
|
||||
cargo run --example fibonacci
|
||||
```
|
||||
|
||||
This example demonstrates how to construct signals, step types, constraints, and witness generation in Chiquito. Best for first time Chiquito users.
|
||||
|
||||
## Example: MiMC7 Circuit
|
||||
TODO: annotate this code example
|
||||
|
||||
This example demonstrates how to construct a lookup table and use external inputs as trace arguments in Chiquito, besides covering concepts in the Fibonacci example. MiMC7 is a zk-friendly hashing function.
|
||||
|
||||
## Example: zkEVM Bytecode Circuit
|
||||
https://github.com/privacy-scaling-explorations/zkevm-circuits/pull/1348
|
||||
|
||||
This example rewrites the zkEVM bytecode circuit using Chiquito and passes all original tests. It demonstrates how Chiquito can standardize and simplify larger scale circuits on the production level.
|
||||
|
||||
# Testing and Links
|
||||
**API documentation**: `cargo doc --no-deps --package chiquito --open`
|
||||
|
||||
Currently API documentation is only written for exposed user functions, which are scattered across the DSL, constraint builder, compiler, and AST. **Refer to the following subdirectories for specific functions:**
|
||||
- Circuit building (DSL): https://qwang98.github.io/chiquito/chiquito/dsl/index.html
|
||||
- Constraint building (constraint builder): https://qwang98.github.io/chiquito/chiquito/dsl/cb/index.html
|
||||
- Witness generation (compiler): https://qwang98.github.io/chiquito/chiquito/compiler/trait.WitnessGenContext.html
|
||||
- Fixed column generation (compiler): https://qwang98.github.io/chiquito/chiquito/compiler/trait.FixedGenContext.html
|
||||
- Invoking the next instance of a forward signal (AST): https://qwang98.github.io/chiquito/chiquito/ast/expr/query/enum.Queriable.html#method.next
|
||||
|
||||
# Licenses
|
||||
|
||||
MIT OR Apache-2.0
|
||||
|
||||
@@ -1,10 +1,18 @@
|
||||
use chiquito::{
|
||||
ast::ToField,
|
||||
backend::halo2::{chiquito2Halo2, ChiquitoHalo2},
|
||||
compiler::{
|
||||
cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder, Compiler,
|
||||
dsl::{
|
||||
circuit, // main function for constructing an AST circuit
|
||||
cb::*, // functions for constraint building
|
||||
},
|
||||
dsl::circuit,
|
||||
ast::{
|
||||
expr::*,
|
||||
},
|
||||
compiler::{
|
||||
cell_manager::SingleRowCellManager, // input for constructing the compiler
|
||||
step_selector::SimpleStepSelectorBuilder, // input for constructing the compiler
|
||||
Compiler, // compiles AST to IR
|
||||
},
|
||||
ir::Circuit, // IR object that the compiler compiles to
|
||||
backend::halo2::{chiquito2Halo2, ChiquitoHalo2}, // compiles to Chiquito Halo2 backend, which can be integrated into Halo2 circuit
|
||||
};
|
||||
use halo2_proofs::{
|
||||
circuit::SimpleFloorPlanner,
|
||||
@@ -13,28 +21,58 @@ use halo2_proofs::{
|
||||
plonk::ConstraintSystem,
|
||||
};
|
||||
|
||||
fn fibo_circuit<F: FieldExt>() -> chiquito::ir::Circuit<F, (), (u64, u64)> {
|
||||
// the main circuit function: returns the compiled IR of a Chiquito circuit
|
||||
// Generic types F, (), (u64, 64) stand for:
|
||||
// 1. type that implements a field trait
|
||||
// 2. empty trace arguments, i.e. (), because there are no external inputs to the Chiquito circuit
|
||||
// 3. two witness generation arguments both of u64 type, i.e. (u64, u64)
|
||||
fn fibo_circuit<F: FieldExt>() -> Circuit<F, (), (u64, u64)> {
|
||||
// PLONKish table for the Fibonacci circuit:
|
||||
// | a | b | c |
|
||||
// | 1 | 1 | 2 |
|
||||
// | 1 | 2 | 3 |
|
||||
// | 2 | 3 | 5 |
|
||||
// | 3 | 5 | 8 |
|
||||
// ...
|
||||
let fibo = circuit::<F, (), (u64, u64), _>("fibonacci", |ctx| {
|
||||
use chiquito::dsl::cb::*;
|
||||
// the following objects (forward signals, steptypes) are defined on the circuit-level
|
||||
|
||||
let a = ctx.forward("a");
|
||||
// forward signals can have constraints across different steps
|
||||
let a = ctx.forward("a");
|
||||
let b = ctx.forward("b");
|
||||
|
||||
// initiate step type for future definition
|
||||
let fibo_step = ctx.step_type("fibo step");
|
||||
let fibo_last_step = ctx.step_type("last step");
|
||||
|
||||
// enforce step type of the first step
|
||||
ctx.pragma_first_step(fibo_step);
|
||||
// enforce step type of the last step
|
||||
ctx.pragma_last_step(fibo_last_step);
|
||||
|
||||
// define step type
|
||||
ctx.step_type_def(fibo_step, |ctx| {
|
||||
// the following objects (constraints, transition constraints, witness generation function)
|
||||
// are defined on the step type-level
|
||||
|
||||
// internal signals can only have constraints within the same step
|
||||
let c = ctx.internal("c");
|
||||
|
||||
// regular constraints are for internal signals only
|
||||
// constrain that a + b == c by calling `eq` function from constraint builder
|
||||
ctx.constr(eq(a + b, c));
|
||||
|
||||
// transition constraints accepts forward signals as well
|
||||
// constrain that b is equal to the next instance of a, by calling `next` on forward signal
|
||||
ctx.transition(eq(b, a.next()));
|
||||
// constrain that c is equal to the next instance of c, by calling `next` on forward signal
|
||||
ctx.transition(eq(c, b.next()));
|
||||
|
||||
// witness generation (wg) function is Turing complete and allows arbitrary user defined logics for assigning witness values
|
||||
// wg function is defined here but no witness value is assigned yet
|
||||
ctx.wg(move |ctx, (a_value, b_value)| {
|
||||
println!("fib line wg: {} {} {}", a_value, b_value, a_value + b_value);
|
||||
// assign arbitrary input values from witness generation function to witnesses
|
||||
ctx.assign(a, a_value.field());
|
||||
ctx.assign(b, b_value.field());
|
||||
ctx.assign(c, (a_value + b_value).field());
|
||||
@@ -44,6 +82,8 @@ fn fibo_circuit<F: FieldExt>() -> chiquito::ir::Circuit<F, (), (u64, u64)> {
|
||||
ctx.step_type_def(fibo_last_step, |ctx| {
|
||||
let c = ctx.internal("c");
|
||||
|
||||
// constrain that a + b == c by calling `eq` function from constraint builder
|
||||
// no transition constraint needed for the next instances of a and b, because it's the last step
|
||||
ctx.constr(eq(a + b, c));
|
||||
|
||||
ctx.wg(move |ctx, (a_value, b_value)| {
|
||||
@@ -59,34 +99,99 @@ fn fibo_circuit<F: FieldExt>() -> chiquito::ir::Circuit<F, (), (u64, u64)> {
|
||||
});
|
||||
});
|
||||
|
||||
// trace function is responsible for adding step instantiations defined in step_type_def function above
|
||||
// trace function is Turing complete and allows arbitrary user defined logics for assigning witness values
|
||||
ctx.trace(move |ctx, _| {
|
||||
// add function adds a step instantiation to the main circuit and calls witness generation function defined in step_type_def
|
||||
// input values for witness generation function are (1, 1) in this step instance
|
||||
ctx.add(&fibo_step, (1, 1));
|
||||
let mut a = 1;
|
||||
let mut b = 2;
|
||||
|
||||
for i in 1..10 {
|
||||
// input values for witness generation function are (a, b) in this step instance
|
||||
ctx.add(&fibo_step, (a, b));
|
||||
|
||||
let prev_a = a;
|
||||
a = b;
|
||||
b = prev_a + b;
|
||||
}
|
||||
|
||||
|
||||
ctx.add(&fibo_last_step, (a, b));
|
||||
})
|
||||
});
|
||||
|
||||
//println!("{:#?}", fibo);
|
||||
|
||||
|
||||
// uncomment for debugging:
|
||||
// println!("{:#?}", fibo);
|
||||
|
||||
// create a new compiler using a cell manager instance and a selector builder instance
|
||||
let compiler = Compiler::new(SingleRowCellManager {}, SimpleStepSelectorBuilder {});
|
||||
|
||||
|
||||
// compile the circuit into an IR object
|
||||
let compiled = compiler.compile(&fibo);
|
||||
|
||||
// uncomment for debugging:
|
||||
//println!("{:#?}", compiled);
|
||||
|
||||
compiled
|
||||
}
|
||||
|
||||
// After compiling Chiquito AST to an IR, it is further parsed by a Chiquito Halo2 backend and integrated into a Halo2 circuit,
|
||||
// which is done by the boilerplate code below.
|
||||
|
||||
// *** Halo2 boilerplate ***
|
||||
#[derive(Clone)]
|
||||
struct FiboConfig<F: FieldExt> {
|
||||
// ChiquitoHalo2 object in the bytecode circuit config struct
|
||||
compiled: ChiquitoHalo2<F, (), (u64, u64)>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> FiboConfig<F> {
|
||||
fn new(meta: &mut ConstraintSystem<F>) -> FiboConfig<F> {
|
||||
// chiquito2Halo2 function in Halo2 backend can convert ir::Circuit object to a ChiquitoHalo2 object,
|
||||
// which can be further integrated into a Halo2 circuit in the example below
|
||||
let mut compiled = chiquito2Halo2(fibo_circuit::<F>());
|
||||
|
||||
// ChiquitoHalo2 objects have their own configure and synthesize functions defined in the Chiquito Halo2 backend
|
||||
compiled.configure(meta);
|
||||
|
||||
FiboConfig { compiled }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Default)]
|
||||
struct FiboCircuit {}
|
||||
|
||||
// integrate Chiquito circuit into a Halo2 circuit
|
||||
impl<F: FieldExt> halo2_proofs::plonk::Circuit<F> for FiboCircuit {
|
||||
type Config = FiboConfig<F>;
|
||||
|
||||
type FloorPlanner = SimpleFloorPlanner;
|
||||
|
||||
// function in Halo2 circuit interface
|
||||
fn without_witnesses(&self) -> Self {
|
||||
Self::default()
|
||||
}
|
||||
|
||||
// function in Halo2 circuit interface
|
||||
fn configure(meta: &mut halo2_proofs::plonk::ConstraintSystem<F>) -> Self::Config {
|
||||
FiboConfig::<F>::new(meta)
|
||||
}
|
||||
|
||||
// function in Halo2 circuit interface
|
||||
fn synthesize(
|
||||
&self,
|
||||
config: Self::Config,
|
||||
mut layouter: impl halo2_proofs::circuit::Layouter<F>,
|
||||
) -> Result<(), halo2_proofs::plonk::Error> {
|
||||
// ChiquitoHalo2 objects have their own configure and synthesize functions defined in the Chiquito Halo2 backend
|
||||
config.compiled.synthesize(&mut layouter, ());
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
// standard main function for a Halo2 circuit
|
||||
fn main() {
|
||||
let circuit = FiboCircuit {};
|
||||
|
||||
@@ -102,47 +207,3 @@ fn main() {
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// *** Halo2 boilerplate ***
|
||||
|
||||
#[derive(Clone)]
|
||||
struct FiboConfig<F: FieldExt> {
|
||||
compiled: ChiquitoHalo2<F, (), (u64, u64)>,
|
||||
}
|
||||
|
||||
impl<F: FieldExt> FiboConfig<F> {
|
||||
fn new(meta: &mut ConstraintSystem<F>) -> FiboConfig<F> {
|
||||
let mut compiled = chiquito2Halo2(fibo_circuit::<F>());
|
||||
|
||||
compiled.configure(meta);
|
||||
|
||||
FiboConfig { compiled }
|
||||
}
|
||||
}
|
||||
|
||||
#[derive(Default)]
|
||||
struct FiboCircuit {}
|
||||
|
||||
impl<F: FieldExt> halo2_proofs::plonk::Circuit<F> for FiboCircuit {
|
||||
type Config = FiboConfig<F>;
|
||||
|
||||
type FloorPlanner = SimpleFloorPlanner;
|
||||
|
||||
fn without_witnesses(&self) -> Self {
|
||||
Self::default()
|
||||
}
|
||||
|
||||
fn configure(meta: &mut halo2_proofs::plonk::ConstraintSystem<F>) -> Self::Config {
|
||||
FiboConfig::<F>::new(meta)
|
||||
}
|
||||
|
||||
fn synthesize(
|
||||
&self,
|
||||
config: Self::Config,
|
||||
mut layouter: impl halo2_proofs::circuit::Layouter<F>,
|
||||
) -> Result<(), halo2_proofs::plonk::Error> {
|
||||
config.compiled.synthesize(&mut layouter, ());
|
||||
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user