From 679de342e747c3ec7236d05e7ec0002c007491db Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Fri, 11 Aug 2023 03:10:30 +0000 Subject: [PATCH 1/2] Taikquito experiment --- examples/taikquito_fibonacci.rs | 77 ++++++++++++++++++ src/frontend/dsl/mod.rs | 2 + src/frontend/dsl/taikquito.rs | 135 ++++++++++++++++++++++++++++++++ src/frontend/mod.rs | 1 + src/lib.rs | 3 + 5 files changed, 218 insertions(+) create mode 100644 examples/taikquito_fibonacci.rs create mode 100644 src/frontend/dsl/taikquito.rs diff --git a/examples/taikquito_fibonacci.rs b/examples/taikquito_fibonacci.rs new file mode 100644 index 00000000..316cebc1 --- /dev/null +++ b/examples/taikquito_fibonacci.rs @@ -0,0 +1,77 @@ +use halo2_proofs::dev::MockProver; +use halo2curves::bn256::Fr; + +use chiquito::{ + ast::ToField, + backend::halo2::{chiquito2Halo2, ChiquitoHalo2Circuit}, + circuit, + compiler::{cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder}, + ir::{assignments::AssignmentGenerator, Circuit}, +}; + +fn fibo_circuit() -> (Circuit, Option>) { + let fibo = circuit!(fibonacci, { + let a = forward!(a); + let b = forward!("b"); + + let fibo_step = step_type_def!(fibo_step { + let c = internal!(c); + + setup!({ + require!(a + b => c); + + require!(transition b => a.next()); + + require!(transition c => b.next()); + }); + + wg!(a_value: u32, b_value: u32 { + assign!(a => a_value.field()); + assign!(b => b_value.field()); + assign!(c => (a_value + b_value).field()); + }) + }); + + pragma_num_steps!(11); + + trace!({ + add!(&fibo_step, (1, 1)); + let mut a = 1; + let mut b = 2; + + for _i in 1..11 { + add!(&fibo_step, (a, b)); + + let prev_a = a; + a = b; + b += prev_a; + } + }); + }); + + println!("=== AST ===\n{:#?}", fibo); + + chiquito::compiler::compile( + chiquito::compiler::config(SingleRowCellManager {}, SimpleStepSelectorBuilder {}), + &fibo, + ) +} + +fn main() { + let (chiquito, wit_gen) = fibo_circuit(); + println!("=== IR ===\n{:#?}", chiquito); + let compiled = chiquito2Halo2(chiquito); + let circuit = ChiquitoHalo2Circuit::new(compiled, wit_gen.map(|g| g.generate(()))); + + let prover = MockProver::::run(7, &circuit, Vec::new()).unwrap(); + + let result = prover.verify_par(); + + println!("{:#?}", result); + + if let Err(failures) = &result { + for failure in failures.iter() { + println!("{}", failure); + } + } +} diff --git a/src/frontend/dsl/mod.rs b/src/frontend/dsl/mod.rs index 4948b9dc..34e969fd 100644 --- a/src/frontend/dsl/mod.rs +++ b/src/frontend/dsl/mod.rs @@ -393,6 +393,8 @@ where pub mod cb; pub mod lb; pub mod sc; +#[macro_use] +pub mod taikquito; #[cfg(test)] mod tests { diff --git a/src/frontend/dsl/taikquito.rs b/src/frontend/dsl/taikquito.rs new file mode 100644 index 00000000..869d3961 --- /dev/null +++ b/src/frontend/dsl/taikquito.rs @@ -0,0 +1,135 @@ +#[macro_export] +macro_rules! circuit { + ($id:ident, $content:block) => {{ + use halo2_proofs::halo2curves::bn256::Fr; + + chiquito::dsl::circuit::(stringify!($id), |ctx| { + use $crate::circuit_context; + circuit_context!(ctx); + + $content + }) + }}; +} + +#[macro_export] +macro_rules! circuit_context { + ($ctx: expr) => { + macro_rules! forward { + ($id_forward:ident) => { + $ctx.forward(stringify!($id_forward)) + }; + + ($id_forward:literal) => { + $ctx.forward($id_forward) + }; + }; + + macro_rules! step_type_def { + ($id_step: ident $step_def_content: block) => { + $ctx.step_type_def(stringify!($id_step), |ctx| { + use $crate::step_type_context; + step_type_context!(ctx, $); + + $step_def_content + }) + }; + + ($id_step: literal $step_def_content: block) => { + $ctx.step_type_def($id_step, |ctx| { + use $crate::step_type_context; + step_type_context!(ctx, $); + + $step_def_content + }) + }; + }; + + macro_rules! pragma_num_steps { + ($num_steps:expr) => { + $ctx.pragma_num_steps($num_steps); + }; + } + + macro_rules! trace { + ($trace_content:block) => { + $ctx.trace(move |ctx, _| { + use $crate::circuit_trace_context; + circuit_trace_context!(ctx); + + $trace_content + }) + }; + } + }; +} + +#[macro_export] +macro_rules! step_type_context { + ($ctx: expr, $d:tt) => { + macro_rules! internal { + ($id_internal:ident) => { + $ctx.internal(stringify!($id_internal)) + }; + } + + macro_rules! setup { + ($setup_content: block) => { + $ctx.setup(|ctx| { + use $crate::step_type_setup_context; + step_type_setup_context!(ctx); + + $setup_content + }); + }; + } + + macro_rules! wg { + ($d($args_id: ident : $args_ty:ty),+ $wg_content: block) => { + $ctx.wg(move |ctx, ($d($args_id),*): ($d($args_ty),*)| { + use $crate::step_type_wg_context; + step_type_wg_context!(ctx); + + $wg_content + }) + }; + } + }; +} + +#[macro_export] +macro_rules! step_type_setup_context { + ($ctx: expr) => { + macro_rules! require { + ($lhs:expr => $rhs:expr) => {{ + $ctx.constr($crate::dsl::cb::eq($lhs, $rhs)); + }}; + + (transition $lhs:expr => $rhs:expr) => {{ + $ctx.transition($crate::dsl::cb::eq($lhs, $rhs)); + }}; + } + }; +} + +#[macro_export] +macro_rules! step_type_wg_context { + ($ctx: expr) => { + macro_rules! assign { + ($signal:expr => $value:expr) => { + $ctx.assign($signal, $value) + }; + } + }; +} + +#[macro_export] +macro_rules! circuit_trace_context { + ($ctx: expr) => { + macro_rules! add { + ($step_type: expr, $args: expr) => { + $ctx.add($step_type, $args); + }; + }; + }; +} diff --git a/src/frontend/mod.rs b/src/frontend/mod.rs index f39746ef..aff290ff 100644 --- a/src/frontend/mod.rs +++ b/src/frontend/mod.rs @@ -1,2 +1,3 @@ +#[macro_use] pub mod dsl; pub mod pychiquito; diff --git a/src/lib.rs b/src/lib.rs index 678d35d7..0ed603a3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,4 +1,7 @@ pub mod ast; +pub mod backend; +pub mod compiler; +#[macro_use] pub mod frontend; pub mod plonkish; pub mod stdlib; From 8e4f4b04b1f142f0c24066a2bbe0b130891fdf93 Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Fri, 11 Aug 2023 03:38:47 +0000 Subject: [PATCH 2/2] Update Debug trait for ast and ir --- examples/taikquito_fibonacci.rs | 12 +++++++----- src/ast/mod.rs | 13 +++++++++++-- src/frontend/dsl/taikquito.rs | 6 +++--- src/lib.rs | 2 -- src/plonkish/ir/mod.rs | 12 +----------- 5 files changed, 22 insertions(+), 23 deletions(-) diff --git a/examples/taikquito_fibonacci.rs b/examples/taikquito_fibonacci.rs index 316cebc1..b52b2fcf 100644 --- a/examples/taikquito_fibonacci.rs +++ b/examples/taikquito_fibonacci.rs @@ -3,10 +3,12 @@ use halo2curves::bn256::Fr; use chiquito::{ ast::ToField, - backend::halo2::{chiquito2Halo2, ChiquitoHalo2Circuit}, circuit, - compiler::{cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder}, - ir::{assignments::AssignmentGenerator, Circuit}, + plonkish::{ + backend::halo2::{chiquito2Halo2, ChiquitoHalo2Circuit}, + compiler::{cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder}, + ir::{assignments::AssignmentGenerator, Circuit}, + }, }; fn fibo_circuit() -> (Circuit, Option>) { @@ -51,8 +53,8 @@ fn fibo_circuit() -> (Circuit, Option>) { println!("=== AST ===\n{:#?}", fibo); - chiquito::compiler::compile( - chiquito::compiler::config(SingleRowCellManager {}, SimpleStepSelectorBuilder {}), + chiquito::plonkish::compiler::compile( + chiquito::plonkish::compiler::config(SingleRowCellManager {}, SimpleStepSelectorBuilder {}), &fibo, ) } diff --git a/src/ast/mod.rs b/src/ast/mod.rs index 0cdfae33..47b79c52 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -31,9 +31,10 @@ pub struct Circuit { pub trace: Option>>, pub fixed_gen: Option>>, + pub num_steps: usize, + pub first_step: Option, pub last_step: Option, - pub num_steps: usize, pub q_enable: bool, pub id: UUID, @@ -43,8 +44,16 @@ impl Debug for Circuit { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { f.debug_struct("Circuit") .field("forward_signals", &self.forward_signals) + .field("shared_signals", &self.shared_signals) + .field("fixed_signals", &self.fixed_signals) .field("halo2_advice", &self.halo2_advice) + .field("halo2_fixed", &self.halo2_fixed) + .field("exposed", &self.exposed) .field("step_types", &self.step_types) + .field("num_steps", &self.num_steps) + .field("first_step", &self.first_step) + .field("last_step", &self.last_step) + .field("q_enable", &self.q_enable) .field("annotations", &self.annotations) .finish() } @@ -450,7 +459,7 @@ impl FixedSignal { } } -#[derive(Clone, Copy)] +#[derive(Debug, Clone, Copy)] pub enum ExposeOffset { First, Last, diff --git a/src/frontend/dsl/taikquito.rs b/src/frontend/dsl/taikquito.rs index 869d3961..b1a2c31d 100644 --- a/src/frontend/dsl/taikquito.rs +++ b/src/frontend/dsl/taikquito.rs @@ -3,7 +3,7 @@ macro_rules! circuit { ($id:ident, $content:block) => {{ use halo2_proofs::halo2curves::bn256::Fr; - chiquito::dsl::circuit::(stringify!($id), |ctx| { + chiquito::frontend::dsl::circuit::(stringify!($id), |ctx| { use $crate::circuit_context; circuit_context!(ctx); @@ -102,11 +102,11 @@ macro_rules! step_type_setup_context { ($ctx: expr) => { macro_rules! require { ($lhs:expr => $rhs:expr) => {{ - $ctx.constr($crate::dsl::cb::eq($lhs, $rhs)); + $ctx.constr($crate::frontend::dsl::cb::eq($lhs, $rhs)); }}; (transition $lhs:expr => $rhs:expr) => {{ - $ctx.transition($crate::dsl::cb::eq($lhs, $rhs)); + $ctx.transition($crate::frontend::dsl::cb::eq($lhs, $rhs)); }}; } }; diff --git a/src/lib.rs b/src/lib.rs index 0ed603a3..c549270f 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -1,6 +1,4 @@ pub mod ast; -pub mod backend; -pub mod compiler; #[macro_use] pub mod frontend; pub mod plonkish; diff --git a/src/plonkish/ir/mod.rs b/src/plonkish/ir/mod.rs index e88066bd..84a0be69 100644 --- a/src/plonkish/ir/mod.rs +++ b/src/plonkish/ir/mod.rs @@ -12,7 +12,7 @@ use self::assignments::Assignments; pub mod assignments; pub mod sc; -#[derive(Clone, Default)] +#[derive(Debug, Clone, Default)] pub struct Circuit { pub columns: Vec, pub exposed: Vec<(Column, i32)>, @@ -26,16 +26,6 @@ pub struct Circuit { pub ast_id: UUID, } -impl Debug for Circuit { - fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { - f.debug_struct("Circuit") - .field("columns", &self.columns) - .field("polys", &self.polys) - .field("lookups", &self.lookups) - .finish() - } -} - #[derive(Clone, Debug, Hash)] pub enum ColumnType { Advice,