diff --git a/halo2-base/src/gates/builder.rs b/halo2-base/src/gates/builder.rs index c90ec8fc..9cd68db0 100644 --- a/halo2-base/src/gates/builder.rs +++ b/halo2-base/src/gates/builder.rs @@ -5,15 +5,16 @@ use super::{ use crate::{ halo2_proofs::{ circuit::{self, Layouter, Region, SimpleFloorPlanner, Value}, - plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Selector}, + plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector}, }, utils::ScalarField, - Context, SKIP_FIRST_PASS, + AssignedValue, Context, SKIP_FIRST_PASS, }; use serde::{Deserialize, Serialize}; use std::{ cell::RefCell, collections::{HashMap, HashSet}, + env::{set_var, var}, }; /// Vector of thread advice column break points @@ -180,7 +181,7 @@ impl GateThreadBuilder { println!("Total {total_fixed} fixed cells"); log::info!("Auto-calculated config params:\n {params:#?}"); } - std::env::set_var("FLEX_GATE_CONFIG_PARAMS", serde_json::to_string(¶ms).unwrap()); + set_var("FLEX_GATE_CONFIG_PARAMS", serde_json::to_string(¶ms).unwrap()); params } @@ -568,7 +569,7 @@ impl Circuit for GateCircuitBuilder { num_lookup_advice_per_phase: _, num_fixed, k, - } = serde_json::from_str(&std::env::var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap(); + } = serde_json::from_str(&var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap(); FlexGateConfig::configure(meta, strategy, &num_advice_per_phase, num_fixed, k) } @@ -588,7 +589,7 @@ impl Circuit for GateCircuitBuilder { pub struct RangeCircuitBuilder(pub GateCircuitBuilder); impl RangeCircuitBuilder { - /// Creates an instance of the [RangeCircuitBuilder] and executes the keygen phase. + /// Creates an instance of the [RangeCircuitBuilder] and executes in keygen mode. pub fn keygen(builder: GateThreadBuilder) -> Self { Self(GateCircuitBuilder::keygen(builder)) } @@ -598,7 +599,7 @@ impl RangeCircuitBuilder { Self(GateCircuitBuilder::mock(builder)) } - /// Creates an instance of the [RangeCircuitBuilder] and executes the prover phase. + /// Creates an instance of the [RangeCircuitBuilder] and executes in prover mode. pub fn prover( builder: GateThreadBuilder, break_points: MultiPhaseThreadBreakPoints, @@ -624,11 +625,11 @@ impl Circuit for RangeCircuitBuilder { num_lookup_advice_per_phase, num_fixed, k, - } = serde_json::from_str(&std::env::var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap(); + } = serde_json::from_str(&var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap(); let strategy = match strategy { GateStrategy::Vertical => RangeStrategy::Vertical, }; - let lookup_bits = std::env::var("LOOKUP_BITS").unwrap().parse().unwrap(); + let lookup_bits = var("LOOKUP_BITS").unwrap_or_else(|_| "0".to_string()).parse().unwrap(); RangeConfig::configure( meta, strategy, @@ -646,14 +647,142 @@ impl Circuit for RangeCircuitBuilder { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { - config.load_lookup_table(&mut layouter).expect("load lookup table should not fail"); + // only load lookup table if we are actually doing lookups + if config.lookup_advice.iter().map(|a| a.len()).sum::() != 0 + || !config.q_lookup.iter().all(|q| q.is_none()) + { + config.load_lookup_table(&mut layouter).expect("load lookup table should not fail"); + } self.0.sub_synthesize(&config.gate, &config.lookup_advice, &config.q_lookup, &mut layouter); Ok(()) } } +/// Configuration with [`RangeConfig`] and a single public instance column. +#[derive(Clone, Debug)] +pub struct RangeWithInstanceConfig { + /// The underlying range configuration + pub range: RangeConfig, + /// The public instance column + pub instance: Column, +} + +/// This is an extension of [`RangeCircuitBuilder`] that adds support for public instances (aka public inputs+outputs) +/// +/// The intended design is that a [`GateThreadBuilder`] is populated and then produces some assigned instances, which are supplied as `assigned_instances` to this struct. +/// The [`Circuit`] implementation for this struct will then expose these instances and constrain them using the Halo2 API. +#[derive(Clone, Debug)] +pub struct RangeWithInstanceCircuitBuilder { + /// The underlying circuit builder + pub circuit: RangeCircuitBuilder, + /// The assigned instances to expose publicly at the end of circuit synthesis + pub assigned_instances: Vec>, +} + +impl RangeWithInstanceCircuitBuilder { + /// See [`RangeCircuitBuilder::keygen`] + pub fn keygen( + builder: GateThreadBuilder, + assigned_instances: Vec>, + ) -> Self { + Self { circuit: RangeCircuitBuilder::keygen(builder), assigned_instances } + } + + /// See [`RangeCircuitBuilder::mock`] + pub fn mock(builder: GateThreadBuilder, assigned_instances: Vec>) -> Self { + Self { circuit: RangeCircuitBuilder::mock(builder), assigned_instances } + } + + /// See [`RangeCircuitBuilder::prover`] + pub fn prover( + builder: GateThreadBuilder, + assigned_instances: Vec>, + break_points: MultiPhaseThreadBreakPoints, + ) -> Self { + Self { circuit: RangeCircuitBuilder::prover(builder, break_points), assigned_instances } + } + + /// Creates a new instance of the [RangeWithInstanceCircuitBuilder]. + pub fn new(circuit: RangeCircuitBuilder, assigned_instances: Vec>) -> Self { + Self { circuit, assigned_instances } + } + + /// Calls [`GateThreadBuilder::config`] + pub fn config(&self, k: u32, minimum_rows: Option) -> FlexGateConfigParams { + self.circuit.0.builder.borrow().config(k as usize, minimum_rows) + } + + /// Gets the break points of the circuit. + pub fn break_points(&self) -> MultiPhaseThreadBreakPoints { + self.circuit.0.break_points.borrow().clone() + } + + /// Gets the number of instances. + pub fn instance_count(&self) -> usize { + self.assigned_instances.len() + } + + /// Gets the instances. + pub fn instance(&self) -> Vec { + self.assigned_instances.iter().map(|v| *v.value()).collect() + } +} + +impl Circuit for RangeWithInstanceCircuitBuilder { + type Config = RangeWithInstanceConfig; + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + unimplemented!() + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let range = RangeCircuitBuilder::configure(meta); + let instance = meta.instance_column(); + meta.enable_equality(instance); + RangeWithInstanceConfig { range, instance } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + // copied from RangeCircuitBuilder::synthesize but with extra logic to expose public instances + let range = config.range; + let circuit = &self.circuit.0; + // only load lookup table if we are actually doing lookups + if range.lookup_advice.iter().map(|a| a.len()).sum::() != 0 + || !range.q_lookup.iter().all(|q| q.is_none()) + { + range.load_lookup_table(&mut layouter).expect("load lookup table should not fail"); + } + // we later `take` the builder, so we need to save this value + let witness_gen_only = circuit.builder.borrow().witness_gen_only(); + let assigned_advices = circuit.sub_synthesize( + &range.gate, + &range.lookup_advice, + &range.q_lookup, + &mut layouter, + ); + + if !witness_gen_only { + // expose public instances + let mut layouter = layouter.namespace(|| "expose"); + for (i, instance) in self.assigned_instances.iter().enumerate() { + let cell = instance.cell.unwrap(); + let (cell, _) = assigned_advices + .get(&(cell.context_id, cell.offset)) + .expect("instance not assigned"); + layouter.constrain_instance(*cell, config.instance, i); + } + } + Ok(()) + } +} + /// Defines stage of the circuit builder. -#[derive(Clone, Copy, Debug)] +#[derive(Clone, Copy, Debug, PartialEq, Eq)] pub enum CircuitBuilderStage { /// Keygen phase Keygen, diff --git a/halo2-base/src/gates/mod.rs b/halo2-base/src/gates/mod.rs index cd25c06f..3e96bdba 100644 --- a/halo2-base/src/gates/mod.rs +++ b/halo2-base/src/gates/mod.rs @@ -1,7 +1,11 @@ +/// Module that helps auto-build circuits pub mod builder; +/// Module implementing our simple custom gate and common functions using it pub mod flex_gate; +/// Module using a single lookup table for range checks pub mod range; +/// Tests #[cfg(any(test, feature = "test-utils"))] pub mod tests; diff --git a/halo2-base/src/gates/range.rs b/halo2-base/src/gates/range.rs index 0b35de35..012e409e 100644 --- a/halo2-base/src/gates/range.rs +++ b/halo2-base/src/gates/range.rs @@ -59,11 +59,10 @@ pub struct RangeConfig { } impl RangeConfig { - /// Generates a new [RangeConfig] with the specified parameters. /// /// If `num_columns` is 0, then we assume you do not want to perform any lookups in that phase. - /// + /// /// Panics if `lookup_bits` > 28. /// * `meta`: [ConstraintSystem] of the circuit /// * `range_strategy`: [GateStrategy] of the range chip @@ -120,7 +119,10 @@ impl RangeConfig { let mut config = Self { lookup_advice, q_lookup, lookup, lookup_bits, gate, _strategy: range_strategy }; - config.create_lookup(meta); + // sanity check: only create lookup table if there are lookup_advice columns + if !num_lookup_advice.is_empty() { + config.create_lookup(meta); + } config.gate.max_rows = (1 << circuit_degree) - meta.minimum_rows(); assert!( (1 << lookup_bits) <= config.gate.max_rows, @@ -181,7 +183,6 @@ impl RangeConfig { /// Trait that implements methods to constrain a field element number `x` is within a range of bits. pub trait RangeInstructions { - /// The type of Gate used within the instructions. type Gate: GateInstructions; @@ -195,7 +196,7 @@ pub trait RangeInstructions { fn lookup_bits(&self) -> usize; /// Checks and constrains that `a` lies in the range [0, 2range_bits). - /// + /// /// Assumes that both `a`<= `range_bits` bits. /// * a: [AssignedValue] value to be range checked /// * range_bits: number of bits to represent the range @@ -204,7 +205,7 @@ pub trait RangeInstructions { /// Constrains that 'a' is less than 'b'. /// /// Assumes that `a` and `b` have bit length <= num_bits bits. - /// + /// /// Note: This may fail silently if a or b have more than num_bits. /// * a: [QuantumCell] value to check /// * b: upper bound expressed as a [QuantumCell] @@ -218,8 +219,8 @@ pub trait RangeInstructions { ); /// Performs a range check that `a` has at most `bit_length(b)` bits and then constrains that `a` is less than `b`. - /// - /// * a: [AssignedValue] value to check + /// + /// * a: [AssignedValue] value to check /// * b: upper bound expressed as a [u64] value fn check_less_than_safe(&self, ctx: &mut Context, a: AssignedValue, b: u64) { let range_bits = @@ -259,7 +260,7 @@ pub trait RangeInstructions { ) -> AssignedValue; /// Performs a range check that `a` has at most `bit_length(b)` and then constrains that `a` is in `[0,b)`. - /// + /// /// Returns 1 if `a` < `b`, otherwise 0. /// /// * a: [AssignedValue] value to check @@ -278,7 +279,7 @@ pub trait RangeInstructions { } /// Performs a range check that `a` has at most `bit_length(b)` and then constrains that `a` is in `[0,b)`. - /// + /// /// Returns 1 if `a` < `b`, otherwise 0. /// /// * a: [AssignedValue] value to check @@ -329,7 +330,7 @@ pub trait RangeInstructions { div, BigUint::one().shl(a_num_bits as u32) / &b + BigUint::one(), ); - // Constrain that remainder is less than divisor (i.e. `r < b`). + // Constrain that remainder is less than divisor (i.e. `r < b`). self.check_big_less_than_safe(ctx, rem, b); (div, rem) } @@ -341,7 +342,7 @@ pub trait RangeInstructions { /// that `a` has <= `a_num_bits` bits. /// that `b` has <= `b_num_bits` bits. /// - /// Note: + /// Note: /// Let `X = 2 ** b_num_bits` /// Write `a = a1 * X + a0` and `c = c1 * X + c0` /// If we write `b * c0 + r = d1 * X + d0` then @@ -442,7 +443,6 @@ pub struct RangeChip { } impl RangeChip { - /// Creates a new [RangeChip] with the given strategy and lookup_bits. /// * strategy: [GateStrategy] for advice values in this chip /// * lookup_bits: number of bits represented in the lookup table [0,2lookup_bits) @@ -489,11 +489,11 @@ impl RangeInstructions for RangeChip { } /// Checks and constrains that `a` lies in the range [0, 2range_bits). - /// + /// /// This is done by decomposing `a` into `k` limbs, where `k = (range_bits + lookup_bits - 1) / lookup_bits`. /// Each limb is constrained to be within the range [0, 2lookup_bits). /// The limbs are then combined to form `a` again with the last limb having `rem_bits` number of bits. - /// + /// /// * `a`: [AssignedValue] value to be range checked /// * `range_bits`: number of bits in the range /// * `lookup_bits`: number of bits in the lookup table @@ -543,7 +543,7 @@ impl RangeInstructions for RangeChip { /// Constrains that 'a' is less than 'b'. /// /// Assumes that`a` and `b` are known to have <= num_bits bits. - /// + /// /// Note: This may fail silently if a or b have more than num_bits /// * a: [QuantumCell] value to check /// * b: upper bound expressed as a [QuantumCell] @@ -625,4 +625,4 @@ impl RangeInstructions for RangeChip { // ctx.cells_to_lookup.last() will have the (k + 1)-th limb of `a - b + 2^{k * limb_bits}`, which is zero iff `a < b` self.gate.is_zero(ctx, *ctx.cells_to_lookup.last().unwrap()) } -} \ No newline at end of file +} diff --git a/halo2-base/src/gates/tests/mod.rs b/halo2-base/src/gates/tests/mod.rs index de6234e7..e7ebb386 100644 --- a/halo2-base/src/gates/tests/mod.rs +++ b/halo2-base/src/gates/tests/mod.rs @@ -17,7 +17,7 @@ mod general; #[cfg(test)] mod idx_to_indicator; -// helper functions +/// helper function to generate a proof with real prover pub fn gen_proof( params: &ParamsKZG, pk: &ProvingKey, @@ -36,6 +36,7 @@ pub fn gen_proof( transcript.finalize() } +/// helper function to verify a proof pub fn check_proof( params: &ParamsKZG, vk: &VerifyingKey, diff --git a/halo2-base/src/lib.rs b/halo2-base/src/lib.rs index bc1745fc..45224578 100644 --- a/halo2-base/src/lib.rs +++ b/halo2-base/src/lib.rs @@ -1,3 +1,4 @@ +//! Base library to build Halo2 circuits. #![feature(stmt_expr_attributes)] #![feature(trait_alias)] #![deny(clippy::perf)] @@ -40,6 +41,7 @@ pub mod gates; /// Utility functions for converting between different types of field elements. pub mod utils; +/// Constant representing whether the Layouter calls `synthesize` once just to get region shape. #[cfg(feature = "halo2-axiom")] pub const SKIP_FIRST_PASS: bool = false; #[cfg(feature = "halo2-pse")] @@ -72,7 +74,7 @@ impl From> for QuantumCell { impl QuantumCell { /// Returns an immutable reference to the underlying [ScalarField] value of a QuantumCell. - /// + /// /// Panics if the QuantumCell is of type WitnessFraction. pub fn value(&self) -> &F { match self { @@ -96,7 +98,7 @@ pub struct ContextCell { } /// Pointer containing cell value and location within [Context]. -/// +/// /// Note: Performs a copy of the value, should only be used when you are about to assign the value again elsewhere. #[derive(Clone, Copy, Debug)] pub struct AssignedValue { @@ -109,7 +111,7 @@ pub struct AssignedValue { impl AssignedValue { /// Returns an immutable reference to the underlying value of an AssignedValue. - /// + /// /// Panics if the AssignedValue is of type WitnessFraction. pub fn value(&self) -> &F { match &self.value { @@ -123,7 +125,6 @@ impl AssignedValue { /// * We keep the naming [Context] for historical reasons. #[derive(Clone, Debug)] pub struct Context { - /// Flag to determine whether only witness generation or proving and verification key generation is being performed. /// * If witness gen is performed many operations can be skipped for optimization. witness_gen_only: bool, @@ -134,7 +135,7 @@ pub struct Context { /// Single column of advice cells. pub advice: Vec>, - /// [Vec] tracking all cells that lookup is enabled for. + /// [Vec] tracking all cells that lookup is enabled for. /// * When there is more than 1 advice column all `advice` cells will be copied to a single lookup enabled column to perform lookups. pub cells_to_lookup: Vec>, @@ -156,12 +157,12 @@ pub struct Context { // TODO: gates that use fixed columns as selectors? /// A [Vec] tracking equality constraints between pairs of [Context] `advice` cells. - /// + /// /// Assumes both `advice` cells are in the same [Context]. pub advice_equality_constraints: Vec<(ContextCell, ContextCell)>, /// A [Vec] tracking pairs equality constraints between Fixed values and [Context] `advice` cells. - /// + /// /// Assumes the constant and `advice` cell are in the same [Context]. pub constant_equality_constraints: Vec<(F, ContextCell)>, } @@ -234,7 +235,7 @@ impl Context { /// Returns the [AssignedValue] of the cell at the given `offset` in the `advice` column of [Context] /// * `offset`: the offset of the cell to be fetched /// * `offset` may be negative indexing from the end of the column (e.g., `-1` is the last cell) - /// * Assumes `offset` is a valid index in `advice`; + /// * Assumes `offset` is a valid index in `advice`; /// * `0` <= `offset` < `advice.len()` (or `advice.len() + offset >= 0` if `offset` is negative) pub fn get(&self, offset: isize) -> AssignedValue { let offset = if offset < 0 { @@ -259,7 +260,7 @@ impl Context { } /// Pushes multiple advice cells to the `advice` column of [Context] and enables them by enabling the corresponding selector specified in `gate_offset`. - /// + /// /// * `inputs`: Iterator that specifies the cells to be assigned /// * `gate_offsets`: specifies relative offset from current position to enable selector for the gate (e.g., `0` is inputs[0]). /// * `offset` may be negative indexing from the end of the column (e.g., `-1` is the last previously assigned cell) @@ -293,7 +294,7 @@ impl Context { /// Pushes multiple advice cells to the `advice` column of [Context] and enables them by enabling the corresponding selector specified in `gate_offset` and returns the last assigned cell. /// /// Assumes `gate_offsets` is the same length as `inputs` - /// + /// /// Returns the last assigned cell /// * `inputs`: Iterator that specifies the cells to be assigned /// * `gate_offsets`: specifies indices to enable selector for the gate; assume `gate_offsets` is sorted in increasing order @@ -311,9 +312,9 @@ impl Context { } /// Pushes multiple advice cells to the `advice` column of [Context] and enables them by enabling the corresponding selector specified in `gate_offset`. - /// - /// Allows for the specification of equality constraints between cells at `equality_offsets` within the `advice` column and external advice cells specified in `external_equality` (e.g, Fixed column). - /// * `gate_offsets`: specifies indices to enable selector for the gate; + /// + /// Allows for the specification of equality constraints between cells at `equality_offsets` within the `advice` column and external advice cells specified in `external_equality` (e.g, Fixed column). + /// * `gate_offsets`: specifies indices to enable selector for the gate; /// * `offset` may be negative indexing from the end of the column (e.g., `-1` is the last cell) /// * `equality_offsets`: specifies pairs of indices to constrain equality /// * `external_equality`: specifies an existing cell to constrain equality with the cell at a certain index