From 34733eae8843b6d2cd89c5fcd7d485e25a5ea0ea Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Thu, 13 Apr 2023 15:13:33 +0700 Subject: [PATCH] Add fibonacci example --- examples/fibonacci.rs | 148 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 148 insertions(+) create mode 100644 examples/fibonacci.rs diff --git a/examples/fibonacci.rs b/examples/fibonacci.rs new file mode 100644 index 0000000..56b0607 --- /dev/null +++ b/examples/fibonacci.rs @@ -0,0 +1,148 @@ +use chiquito::{ + ast::ToField, + backend::halo2::{chiquito2Halo2, ChiquitoHalo2}, + compiler::{ + cell_manager::SingleRowCellManager, step_selector::SimpleStepSelectorBuilder, Compiler, + }, + dsl::circuit, +}; +use halo2_proofs::{ + circuit::SimpleFloorPlanner, + dev::MockProver, + halo2curves::{bn256::Fr, FieldExt}, + plonk::ConstraintSystem, +}; + +fn fibo_circuit() -> chiquito::ir::Circuit { + let fibo = circuit::("fibonacci", |ctx| { + use chiquito::dsl::cb::*; + + let a = ctx.forward("a"); + let b = ctx.forward("b"); + + let fibo_step = ctx.step_type("fibo step"); + let fibo_last_step = ctx.step_type("last step"); + + ctx.pragma_first_step(fibo_step); + ctx.pragma_last_step(fibo_last_step); + + ctx.step_type_def(fibo_step, |ctx| { + let c = ctx.internal("c"); + + ctx.constr("a + b == c", eq(a + b, c)); + ctx.transition("b == a.next", eq(b, a.next())); + ctx.transition("c == b.next", eq(c, b.next())); + + ctx.wg(move |ctx, (a_value, b_value)| { + println!("fib line wg: {} {} {}", a_value, b_value, a_value + b_value); + ctx.assign(a, a_value.field()); + ctx.assign(b, b_value.field()); + ctx.assign(c, (a_value + b_value).field()); + }); + }); + + ctx.step_type_def(fibo_last_step, |ctx| { + let c = ctx.internal("c"); + + ctx.constr("a + b == c", eq(a + b, c)); + + ctx.wg(move |ctx, (a_value, b_value)| { + println!( + "fib last line wg: {} {} {}", + a_value, + b_value, + a_value + b_value + ); + ctx.assign(a, a_value.field()); + ctx.assign(b, b_value.field()); + ctx.assign(c, (a_value + b_value).field()); + }); + }); + + ctx.trace(move |ctx, _| { + ctx.add(&fibo_step, (1, 1)); + let mut a = 1; + let mut b = 2; + + for i in 1..10 { + 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); + + let compiler = Compiler::new(SingleRowCellManager {}, SimpleStepSelectorBuilder {}); + + let compiled = compiler.compile(&fibo); + + //println!("{:#?}", compiled); + + compiled +} + +fn main() { + let circuit = FiboCircuit {}; + + 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); + } + } +} + +// *** Halo2 boilerplate *** + +#[derive(Clone)] +struct FiboConfig { + compiled: ChiquitoHalo2, +} + +impl FiboConfig { + fn new(meta: &mut ConstraintSystem) -> FiboConfig { + let mut compiled = chiquito2Halo2(fibo_circuit::()); + + compiled.configure(meta); + + FiboConfig { compiled } + } +} + +#[derive(Default)] +struct FiboCircuit {} + +impl halo2_proofs::plonk::Circuit for FiboCircuit { + type Config = FiboConfig; + + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self::default() + } + + fn configure(meta: &mut halo2_proofs::plonk::ConstraintSystem) -> Self::Config { + FiboConfig::::new(meta) + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl halo2_proofs::circuit::Layouter, + ) -> Result<(), halo2_proofs::plonk::Error> { + config.compiled.synthesize(&mut layouter, ()); + + Ok(()) + } +}