Smart Range Builder

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<F: ScalarField> GateThreadBuilder<F> {
             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(&params).unwrap());
+        set_var("FLEX_GATE_CONFIG_PARAMS", serde_json::to_string(&params).unwrap());
         params
     }
 
@@ -568,7 +569,7 @@ impl<F: ScalarField> Circuit<F> for GateCircuitBuilder<F> {
             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<F: ScalarField> Circuit<F> for GateCircuitBuilder<F> {
 pub struct RangeCircuitBuilder<F: ScalarField>(pub GateCircuitBuilder<F>);
 
 impl<F: ScalarField> RangeCircuitBuilder<F> {
-    /// 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<F>) -> Self {
         Self(GateCircuitBuilder::keygen(builder))
     }
@@ -598,7 +599,7 @@ impl<F: ScalarField> RangeCircuitBuilder<F> {
         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<F>,
         break_points: MultiPhaseThreadBreakPoints,
@@ -624,11 +625,11 @@ impl<F: ScalarField> Circuit<F> for RangeCircuitBuilder<F> {
             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<F: ScalarField> Circuit<F> for RangeCircuitBuilder<F> {
         config: Self::Config,
         mut layouter: impl Layouter<F>,
     ) -> 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::<usize>() != 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<F: ScalarField> {
+    /// The underlying range configuration
+    pub range: RangeConfig<F>,
+    /// The public instance column
+    pub instance: Column<Instance>,
+}
+
+/// 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<F: ScalarField> {
+    /// The underlying circuit builder
+    pub circuit: RangeCircuitBuilder<F>,
+    /// The assigned instances to expose publicly at the end of circuit synthesis
+    pub assigned_instances: Vec<AssignedValue<F>>,
+}
+
+impl<F: ScalarField> RangeWithInstanceCircuitBuilder<F> {
+    /// See [`RangeCircuitBuilder::keygen`]
+    pub fn keygen(
+        builder: GateThreadBuilder<F>,
+        assigned_instances: Vec<AssignedValue<F>>,
+    ) -> Self {
+        Self { circuit: RangeCircuitBuilder::keygen(builder), assigned_instances }
+    }
+
+    /// See [`RangeCircuitBuilder::mock`]
+    pub fn mock(builder: GateThreadBuilder<F>, assigned_instances: Vec<AssignedValue<F>>) -> Self {
+        Self { circuit: RangeCircuitBuilder::mock(builder), assigned_instances }
+    }
+
+    /// See [`RangeCircuitBuilder::prover`]
+    pub fn prover(
+        builder: GateThreadBuilder<F>,
+        assigned_instances: Vec<AssignedValue<F>>,
+        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<F>, assigned_instances: Vec<AssignedValue<F>>) -> Self {
+        Self { circuit, assigned_instances }
+    }
+
+    /// Calls [`GateThreadBuilder::config`]
+    pub fn config(&self, k: u32, minimum_rows: Option<usize>) -> 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<F> {
+        self.assigned_instances.iter().map(|v| *v.value()).collect()
+    }
+}
+
+impl<F: ScalarField> Circuit<F> for RangeWithInstanceCircuitBuilder<F> {
+    type Config = RangeWithInstanceConfig<F>;
+    type FloorPlanner = SimpleFloorPlanner;
+
+    fn without_witnesses(&self) -> Self {
+        unimplemented!()
+    }
+
+    fn configure(meta: &mut ConstraintSystem<F>) -> 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<F>,
+    ) -> 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::<usize>() != 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,

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;
 

halo2-base/src/gates/range.rs

@@ -59,11 +59,10 @@ pub struct RangeConfig<F: ScalarField> {
 }
 
 impl<F: ScalarField> RangeConfig<F> {
-
     /// 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<F: ScalarField> RangeConfig<F> {
         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<F: ScalarField> RangeConfig<F> {
 
 /// Trait that implements methods to constrain a field element number `x` is within a range of bits.
 pub trait RangeInstructions<F: ScalarField> {
-
     /// The type of Gate used within the instructions.
     type Gate: GateInstructions<F>;
 
@@ -195,7 +196,7 @@ pub trait RangeInstructions<F: ScalarField> {
     fn lookup_bits(&self) -> usize;
 
     /// Checks and constrains that `a` lies in the range [0, 2<sup>range_bits</sup>).
-    /// 
+    ///
     /// 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<F: ScalarField> {
     /// 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<F: ScalarField> {
     );
 
     /// 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<F>, a: AssignedValue<F>, b: u64) {
         let range_bits =
@@ -259,7 +260,7 @@ pub trait RangeInstructions<F: ScalarField> {
     ) -> AssignedValue<F>;
 
     /// 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<F: ScalarField> {
     }
 
     /// 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<F: ScalarField> {
             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<F: ScalarField> {
     /// 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<F: ScalarField> {
 }
 
 impl<F: ScalarField> RangeChip<F> {
-
     /// 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,2<sup>lookup_bits</sup>)
@@ -489,11 +489,11 @@ impl<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
     }
 
     /// Checks and constrains that `a` lies in the range [0, 2<sup>range_bits</sup>).
-    /// 
+    ///
     /// 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, 2<sup>lookup_bits</sup>).
     /// 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<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
     /// 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<F: ScalarField> RangeInstructions<F> for RangeChip<F> {
         // 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())
     }
-}
+}

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<Bn256>,
     pk: &ProvingKey<G1Affine>,
@@ -36,6 +36,7 @@ pub fn gen_proof(
     transcript.finalize()
 }
 
+/// helper function to verify a proof
 pub fn check_proof(
     params: &ParamsKZG<Bn256>,
     vk: &VerifyingKey<G1Affine>,