mirror of
https://github.com/privacy-scaling-explorations/chiquito.git
synced 2026-04-23 03:00:09 -04:00
c5097d09d0
High Level Description Simplified syntax for adding and building lookup columns. - Adding lookup: call add_lookup in step_type_def to modify StepTypeContext - Building lookup: call lookup() without a parameter to initialize; call add(source_column, lookup_column) to build lookup match constraints; call enable(enabler_column) to add an enabler column - Example: add_lookup(lookup().add(source_col_1, lookup_col_1).enable(enabler_col).add(source_col_2, lookup_col2) Technical Details (from a user -> dsl -> ast -> ir perspective): 1. Added LookupBuilder to dsl/cb with exposed methods to update Lookup in ast 2. Modified Lookup in ast to include an annotation field, which is now auto generated, as well as an enabler column field 3. Lookup now takes (Constraint, Expr) for (LHS, RHS), where LHS is the source column and RHS is the lookup column; Lookup takes Constraint for the enabler column 4. In ir, PolyLookup takes the auto-generated annotation from Lookup in ast and Halo2 backend takes annotation from PolyLookup in ir. Next Step 1. Test the new lookup syntax on zkEVM bytecode circuit --------- (With lots of inspirations and guidance from Leo Lara) Co-authored-by: Steve Wang <qian.wang.wg24@wharton.upenn.edu>
57 lines
1.5 KiB
Rust
57 lines
1.5 KiB
Rust
use chiquito::{
|
|
ast::{ToExpr, ToField},
|
|
compiler::{
|
|
cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder, Compiler,
|
|
},
|
|
dsl::{circuit, cb::lookup},
|
|
};
|
|
use halo2_proofs::halo2curves::bn256::Fr;
|
|
|
|
fn main() {
|
|
let sc = circuit::<Fr, Vec<i32>, i32, _>("a circuit", |ctx| {
|
|
let a = ctx.forward("a");
|
|
let b = ctx.forward("b");
|
|
let c = ctx.forward("c");
|
|
|
|
let s1 = ctx.step_type("s1");
|
|
ctx.step_type_def(s1, |ctx| {
|
|
let d = ctx.internal("d");
|
|
let f = ctx.internal("f");
|
|
|
|
ctx.constr((a + b) * (c - 1));
|
|
ctx.constr(1.expr() + (a + b) * (c - 1));
|
|
ctx.transition(a + 1);
|
|
|
|
ctx.add_lookup(lookup().add(a, b).enable(d).add(d + a, f * c));
|
|
|
|
ctx.wg(move |ctx, _| {
|
|
ctx.assign(a, 13.field());
|
|
ctx.assign(b, 13.field());
|
|
ctx.assign(c, 13.field());
|
|
|
|
ctx.assign(d, 1.field());
|
|
ctx.assign(f, 2.field());
|
|
});
|
|
});
|
|
|
|
let s2 = ctx.step_type("s2");
|
|
ctx.step_type_def(s2, |ctx| {
|
|
// ...
|
|
|
|
ctx.wg(move |ctx, _| {
|
|
ctx.assign(a, 13.field());
|
|
})
|
|
});
|
|
|
|
ctx.trace(move |ctx, _| {
|
|
let v: i32 = 1;
|
|
ctx.add(&s2, v);
|
|
ctx.add(&s1, v);
|
|
});
|
|
});
|
|
|
|
let compiler = Compiler::new(SingleRowCellManager {}, SimpleStepSelectorBuilder {});
|
|
|
|
println!("{:#?}", compiler.compile(&sc));
|
|
}
|