From 4bc9f0a711b07240c10faf516ccad4a6d912e2c6 Mon Sep 17 00:00:00 2001
From: Jonathan Wang <31040440+jonathanpwang@users.noreply.github.com>
Date: Thu, 2 Nov 2023 17:30:08 -0700
Subject: [PATCH] [feat] update docs (#211)
* feat: update doc comments with function assumptions
* feat: update readme
* chore: fix CI
---
halo2-base/README.md | 578 ++-----------------
halo2-base/src/gates/flex_gate/mod.rs | 8 +-
halo2-base/src/gates/range/mod.rs | 34 +-
halo2-base/src/safe_types/bytes.rs | 10 +-
halo2-base/src/safe_types/mod.rs | 8 +
halo2-ecc/src/fields/vector.rs | 6 +
halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs | 2 -
7 files changed, 106 insertions(+), 540 deletions(-)
diff --git a/halo2-base/README.md b/halo2-base/README.md
index 6b078ab9..9e7c5a36 100644
--- a/halo2-base/README.md
+++ b/halo2-base/README.md
@@ -1,92 +1,89 @@
-# Halo2-base
+# `halo2-base`
-Halo2-base provides a streamlined frontend for interacting with the Halo2 API. It simplifies circuit programming to declaring constraints over a single advice and selector column and provides built-in circuit configuration and parellel proving and witness generation.
+`halo2-base` provides an embedded domain specific language (eDSL) for writing circuits with the [`halo2`](https://github.com/axiom-crypto/halo2) API. It simplifies circuit programming to declaring constraints over a single advice and selector column and provides built-in circuit tuning and support for multi-threaded witness generation.
-Programmed circuit constraints are stored in `GateThreadBuilder` as a `Vec` of `Context`'s. Each `Context` can be interpreted as a "virtual column" which tracks witness values and constraints but does not assign them as cells within the Halo2 backend. Conceptually, one can think that at circuit generation time, the virtual columns are all concatenated into a **single** virtual column. This virtual column is then re-distributed into the minimal number of true `Column`s (aka Plonkish arithmetization columns) to fit within a user-specified number of rows. These true columns are then assigned into the Plonkish arithemization using the vanilla Halo2 backend. This has several benefits:
+For further details, see the [Rust docs](https://axiom-crypto.github.io/halo2-lib/halo2_base/).
-- The user only needs to specify the desired number of rows. The rest of the circuit configuration process is done automatically because the optimal number of columns in the circuit can be calculated from the total number of cells in the `Context`s. This eliminates the need to manually assign circuit parameters at circuit creation time.
-- In addition, this simplifies the process of testing the performance of different circuit configurations (different Plonkish arithmetization shapes) in the Halo2 backend, since the same virtual columns in the `Context` can be re-distributed into different Plonkish arithmetization tables.
+## Virtual Region Managers
-A user can also parallelize witness generation by specifying a function and a `Vec` of inputs to perform in parallel using `parallelize_in()` which creates a separate `Context` for each input that performs the specified function. These "virtual columns" are then computed in parallel during witness generation and combined back into a single column "virtual column" before cell assignment in the Halo2 backend.
+The core framework under which `halo2-base` operates is that of _virtual cell management_. We perform witness generation in a virtual region (outside of the low-level raw halo2 `Circuit::synthesize`) and only at the very end map it to a "raw/physical" region in halo2's Plonkish arithmetization.
-All assigned values in a circuit are assigned in the Halo2 backend by calling `synthesize()` in `GateCircuitBuilder` (or [`RangeCircuitBuilder`](#rangecircuitbuilder)) which in turn invokes `assign_all()` (or `assign_threads_in` if only doing witness generation) in `GateThreadBuilder` to assign the witness values tracked in a `Context` to their respective `Column` in the circuit within the Halo2 backend.
+We formalize this into a new trait `VirtualRegionManager`. Any `VirtualRegionManager` is associated with some subset of columns (more generally, a physical Halo2 region). It can manage its own virtual region however it wants, but it must provide a deterministic way to map the virtual region to the physical region.
-Halo2-base also provides pre-built [Chips](https://zcash.github.io/halo2/concepts/chips.html) for common arithmetic operations in `GateChip` and range check arguments in `RangeChip`. Our `Chip` implementations differ slightly from ZCash's `Chip` implementations. In Zcash, the `Chip` struct stores knowledge about the `Config` and custom gates used. In halo2-base a `Chip` stores only functions while the interaction with the circuit's `Config` is hidden and done in `GateCircuitBuilder`.
+We have the following examples of virtual region managers:
-The structure of halo2-base is outlined as follows:
+- `SinglePhaseCoreManager`: this is associated with our `BasicGateConfig` which is a simple [vertical custom gate](https://docs.axiom.xyz/zero-knowledge-proofs/getting-started-with-halo2#simplified-interface), in a single halo2 challenge phase. It manages a virtual region with a bunch of virtual columns (these are the `Context`s). One can think of all virtual columns as being concatenated into a single big column. Then given the target number of rows in the physical circuit, it will chunk the single virtual column appropriately into multiple physical columns.
+- `CopyConstraintManager`: this is a global manager to allow virtual cells from different regions to be referenced. Virtual cells are referred to as `AssignedValue`. Despite the name (which is from historical reasons), these values are not actually assigned into the physical circuit. `AssignedValue`s are virtual cells. Instead they keep track of a tag for which virtual region they belong to, and some other identifying tag that loosely maps to a CPU thread. When a virtual cell is referenced and used, a copy is performed and the `CopyConstraintManager` keeps track of the equality. After the virtual cells are all physically assigned, this manager will impose the equality constraints on the physical cells.
+ - This manager also keeps track of constants that are used, deduplicates them, and assigns all constants into dedicated fixed columns. It also imposes the equality constraints between advice cells and the fixed cells.
+ - It is **very important** that all virtual region managers reference the same `CopyConstraintManager` to ensure that all copy constraints are managed properly. The `CopyConstraintManager` must also be raw assigned at the end of `Circuit::synthesize` to ensure the copy constraints are actually communicated to the raw halo2 API.
+- `LookupAnyManager`: for any kind of lookup argument (either into a fixed table or dynamic table), we do not want to enable this lookup argument on every column of the circuit since enabling lookup is expensive. Instead, we allocate special advice columns (with no selector) where the lookup argument is always on. When we want to look up certain values, we copy them over to the special advice cells. This also means that the physical location of the cells you want to look up can be unstructured.
-- `builder.rs`: Contains `GateThreadBuilder`, `GateCircuitBuilder`, and `RangeCircuitBuilder` which implement the logic to provide different arithmetization configurations with different performance tradeoffs in the Halo2 backend.
-- `lib.rs`: Defines the `QuantumCell`, `ContextCell`, `AssignedValue`, and `Context` types which track assigned values within a circuit across multiple columns and provide a streamlined interface to assign witness values directly to the advice column.
-- `utils.rs`: Contains `BigPrimeField` and `ScalerField` traits which represent field elements within Halo2 and provides methods to decompose field elements into `u64` limbs and convert between field elements and `BigUint`.
-- `flex_gate.rs`: Contains the implementation of `GateChip` and the `GateInstructions` trait which provide functions for basic arithmetic operations within Halo2.
-- `range.rs:`: Implements `RangeChip` and the `RangeInstructions` trait which provide functions for performing range check and other lookup argument operations.
+The virtual regions are also designed to be able to interact with raw halo2 sub-circuits. The overall architecture of a circuit that may use virtual regions managed by `halo2-lib` alongside raw halo2 sub-circuits looks as follows:
-This readme compliments the in-line documentation of halo2-base, providing an overview of `builder.rs` and `lib.rs`.
+
-
+## [`BaseCircuitBuilder`](./src/gates/circuit/mod.rs)
-## [**Context**](src/lib.rs)
-
-`Context` holds all information of an execution trace (circuit and its witness values). `Context` represents a "virtual column" that stores unassigned constraint information in the Halo2 backend. Storing the circuit information in a `Context` rather than assigning it directly to the Halo2 backend allows for the pre-computation of circuit parameters and preserves the underlying circuit information allowing for its rearrangement into multiple columns for parallelization in the Halo2 backend.
-
-During `synthesize()`, the advice values of all `Context`s are concatenated into a single "virtual column" that is split into multiple true `Column`s at `break_points` each representing a different sub-section of the "virtual column". During circuit synthesis, all cells are assigned to Halo2 `AssignedCell`s in a single `Region` within Halo2's backend.
-
-For parallel witness generation, multiple `Context`s are created for each parallel operation. After parallel witness generation, these `Context`'s are combined to form a single "virtual column" as above. Note that while the witness generation can be multi-threaded, the ordering of the contents in each `Context`, and the order of the `Context`s themselves, must be deterministic.
-
-```rust ignore
-pub struct Context {
-
- witness_gen_only: bool,
-
- pub context_id: usize,
-
- pub advice: Vec>,
+A circuit builder in `halo2-lib` is a collection of virtual region managers with an associated raw halo2 configuration of columns and custom gates. The precise configuration of these columns and gates can potentially be tuned after witness generation has been performed. We do not yet codify the notion of a circuit builder into a trait.
- pub cells_to_lookup: Vec>,
+The core circuit builder used throughout `halo2-lib` is the `BaseCircuitBuilder`. It is associated to `BaseConfig`, which consists of instance columns together with either `FlexGateConfig` or `RangeConfig`: `FlexGateConfig` is used when no functionality involving bit range checks (usually necessary for less than comparisons on numbers) is needed, otherwise `RangeConfig` consists of `FlexGateConfig` together with a fixed lookup table for range checks.
- pub zero_cell: Option>,
+The basic construction of `BaseCircuitBuilder` is as follows:
- pub selector: Vec,
+```rust
+let k = 10; // your circuit will have 2^k rows
+let witness_gen_only = false; // constraints are ignored if set to true
+let mut builder = BaseCircuitBuilder::new(witness_gen_only).use_k(k);
+// If you need to use range checks, a good default is to set `lookup_bits` to 1 less than `k`
+let lookup_bits = k - 1;
+builder.set_lookup_bits(lookup_bits); // this can be skipped if you are not using range checks. The program will panic if `lookup_bits` is not set when you need range checks.
- pub advice_equality_constraints: Vec<(ContextCell, ContextCell)>,
-
- pub constant_equality_constraints: Vec<(F, ContextCell)>,
+// this is the struct holding basic our eDSL API functions
+let gate = GateChip::default();
+// if you need RangeChip, construct it with:
+let range = builder.range_chip(); // this will panic if `builder` did not set `lookup_bits`
+{
+ // basic usage:
+ let ctx = builder.main(0); // this is "similar" to spawning a new thread. 0 refers to the halo2 challenge phase
+ // do your computations
}
+// `builder` now contains all information from witness generation and constraints of your circuit
+let unusable_rows = 9; // this is usually enough, set to 20 or higher if program panics
+// This tunes your circuit to find the optimal configuration
+builder.calculate_params(Some(unusable_rows));
+
+// Now you can mock prove or prove your circuit:
+// If you have public instances, you must either provide them yourself or extract from `builder.assigned_instances`.
+MockProver::run(k as u32, &builder, instances).unwrap().assert_satisfied();
```
-`witness_gen_only` is set to `true` if we only care about witness generation and not about circuit constraints, otherwise it is set to false. This should **not** be set to `true` during mock proving or **key generation**. When this flag is `true`, we perform certain optimizations that are only valid when we don't care about constraints or selectors.
+### Proving mode
-A `Context` holds all equality and constant constraints as a `Vec` of `ContextCell` tuples representing the positions of the two cells to constrain. `advice` and`selector` store the respective column values of the `Context`'s which may represent the entire advice and selector column or a sub-section of the advice and selector column during parellel witness generation. `cells_to_lookup` tracks `AssignedValue`'s of cells to be looked up in a global lookup table, specifically for range checks, shared among all `Context`'s'.
+`witness_gen_only` is set to `true` if we only care about witness generation and not about circuit constraints, otherwise it is set to false. This should **not** be set to `true` during mock proving or **key generation**. When this flag is `true`, we perform certain optimizations that are only valid when we don't care about constraints or selectors. This should only be done in the context of real proving, when a proving key has already been created.
-### [**ContextCell**](./src/lib.rs):
+## [**Context**](src/lib.rs)
-`ContextCell` is a pointer to a specific cell within a `Context` identified by the Context's `context_id` and the cell's relative `offset` from the first cell of the advice column of the `Context`.
+`Context` holds all information of an execution trace (circuit and its witness values). `Context` represents a "virtual column" that stores unassigned constraint information in the Halo2 backend. Storing the circuit information in a `Context` rather than assigning it directly to the Halo2 backend allows for the pre-computation of circuit parameters and preserves the underlying circuit information allowing for its rearrangement into multiple columns for parallelization in the Halo2 backend.
-```rust ignore
-#[derive(Clone, Copy, Debug)]
-pub struct ContextCell {
- /// Identifier of the [Context] that this cell belongs to.
- pub context_id: usize,
- /// Relative offset of the cell within this [Context] advice column.
- pub offset: usize,
-}
-```
+During `synthesize()`, the advice values of all `Context`s are concatenated into a single "virtual column" that is split into multiple true `Column`s at `break_points` each representing a different sub-section of the "virtual column". During circuit synthesis, all cells are assigned to Halo2 `AssignedCell`s in a single `Region` within Halo2's backend.
+
+For parallel witness generation, multiple `Context`s are created for each parallel operation. After parallel witness generation, these `Context`'s are combined to form a single "virtual column" as above. Note that while the witness generation can be multi-threaded, the ordering of the contents in each `Context`, and the order of the `Context`s themselves, must be deterministic.
### [**AssignedValue**](./src/lib.rs):
-`AssignedValue` represents a specific `Assigned` value assigned to a specific cell within a `Context` of a circuit referenced by a `ContextCell`.
+Despite the name, an `AssignedValue` is a **virtual cell**. It contains the actual witness value as well as a pointer to the location of the virtual cell within a virtual region. The pointer is given by type `ContextCell`. We only store the pointer when not in witness generation only mode as an optimization.
```rust ignore
pub struct AssignedValue {
pub value: Assigned,
-
pub cell: Option,
}
```
### [**Assigned**](./src/plonk/assigned.rs)
-`Assigned` is a wrapper enum for values assigned to a cell within a circuit which stores the value as a fraction and marks it for batched inversion using [Montgomery's trick](https://zcash.github.io/halo2/background/fields.html#montgomerys-trick). Performing batched inversion allows for the computation of the inverse of all marked values with a single inversion operation.
+`Assigned` is not a ZK or circuit-related type.
+`Assigned` is a wrapper enum for a field element which stores the value as a fraction and marks it for batched inversion using [Montgomery's trick](https://zcash.github.io/halo2/background/fields.html#montgomerys-trick). Performing batched inversion allows for the computation of the inverse of all marked values with a single inversion operation.
```rust ignore
pub enum Assigned {
@@ -99,21 +96,15 @@ pub enum Assigned {
}
```
-
-
## [**QuantumCell**](./src/lib.rs)
-`QuantumCell` is a helper enum that abstracts the scenarios in which a value is assigned to the advice column in Halo2-base. Without `QuantumCell` assigning existing or constant values to the advice column requires manually specifying the enforced constraints on top of assigning the value leading to bloated code. `QuantumCell` handles these technical operations, all a developer needs to do is specify which enum option in `QuantumCell` the value they are adding corresponds to.
+`QuantumCell` is a helper enum that abstracts the scenarios in which a value is assigned to the advice column in `halo2-base`. Without `QuantumCell`, assigning existing or constant values to the advice column requires manually specifying the enforced constraints on top of assigning the value leading to bloated code. `QuantumCell` handles these technical operations, all a developer needs to do is specify which enum option in `QuantumCell` the value they are adding corresponds to.
```rust ignore
pub enum QuantumCell {
-
Existing(AssignedValue),
-
Witness(F),
-
WitnessFraction(Assigned),
-
Constant(F),
}
```
@@ -123,468 +114,11 @@ QuantumCell contains the following enum variants.
- **Existing**:
Assigns a value to the advice column that exists within the advice column. The value is an existing value from some previous part of your computation already in the advice column in the form of an `AssignedValue`. When you add an existing cell into the table a new cell will be assigned into the advice column with value equal to the existing value. An equality constraint will then be added between the new cell and the "existing" cell so the Verifier has a guarantee that these two cells are always equal.
- ```rust ignore
- QuantumCell::Existing(acell) => {
- self.advice.push(acell.value);
-
- if !self.witness_gen_only {
- let new_cell =
- ContextCell { context_id: self.context_id, offset: self.advice.len() - 1 };
- self.advice_equality_constraints.push((new_cell, acell.cell.unwrap()));
- }
- }
- ```
-
- **Witness**:
Assigns an entirely new witness value into the advice column, such as a private input. When `assign_cell()` is called the value is wrapped in as an `Assigned::Trivial()` which marks it for exclusion from batch inversion.
- ```rust ignore
- QuantumCell::Witness(val) => {
- self.advice.push(Assigned::Trivial(val));
- }
- ```
-- **WitnessFraction**:
- Assigns an entirely new witness value to the advice column. `WitnessFraction` exists for optimization purposes and accepts Assigned values wrapped in `Assigned::Rational()` marked for batch inverion.
- ```rust ignore
- QuantumCell::WitnessFraction(val) => {
- self.advice.push(val);
- }
- ```
-- **Constant**:
- A value that is a "known" constant. A "known" refers to known at circuit creation time to both the Prover and Verifier. When you assign a constant value there exists another secret "Fixed" column in the circuit constraint table whose values are fixed at circuit creation time. When you assign a Constant value, you are adding this value to the Fixed column, adding the value as a witness to the Advice column, and then imposing an equality constraint between the two corresponding cells in the Fixed and Advice columns.
-
-```rust ignore
-QuantumCell::Constant(c) => {
- self.advice.push(Assigned::Trivial(c));
- // If witness generation is not performed, enforce equality constraints between the existing cell and the new cell
- if !self.witness_gen_only {
- let new_cell =
- ContextCell { context_id: self.context_id, offset: self.advice.len() - 1 };
- self.constant_equality_constraints.push((c, new_cell));
- }
-}
-```
-
-
-
-## [**GateThreadBuilder**](./src/gates/builder.rs) & [**GateCircuitBuilder**](./src/gates/builder.rs)
-
-`GateThreadBuilder` tracks the cell assignments of a circuit as an array of `Vec` of `Context`' where `threads[i]` contains all `Context`'s for phase `i`. Each array element corresponds to a distinct challenge phase of Halo2's proving system, each of which has its own unique set of rows and columns.
-
-```rust ignore
-#[derive(Clone, Debug, Default)]
-pub struct GateThreadBuilder {
- /// Threads for each challenge phase
- pub threads: [Vec>; MAX_PHASE],
- /// Max number of threads
- thread_count: usize,
- /// Flag for witness generation. If true, the gate thread builder is used for witness generation only.
- witness_gen_only: bool,
- /// The `unknown` flag is used during key generation. If true, during key generation witness [Value]s are replaced with Value::unknown() for safety.
- use_unknown: bool,
-}
-```
-
-Once a `GateThreadBuilder` is created, gates may be assigned to a `Context` (or in the case of parallel witness generation multiple `Context`'s) within `threads`. Once the circuit is written `config()` is called to pre-compute the circuits size and set the circuit's environment variables.
-
-[**config()**](./src/gates/builder.rs)
-
-```rust ignore
-pub fn config(&self, k: usize, minimum_rows: Option) -> FlexGateConfigParams {
- let max_rows = (1 << k) - minimum_rows.unwrap_or(0);
- let total_advice_per_phase = self
- .threads
- .iter()
- .map(|threads| threads.iter().map(|ctx| ctx.advice.len()).sum::())
- .collect::>();
- // we do a rough estimate by taking ceil(advice_cells_per_phase / 2^k )
- // if this is too small, manual configuration will be needed
- let num_advice_per_phase = total_advice_per_phase
- .iter()
- .map(|count| (count + max_rows - 1) / max_rows)
- .collect::>();
-
- let total_lookup_advice_per_phase = self
- .threads
- .iter()
- .map(|threads| threads.iter().map(|ctx| ctx.cells_to_lookup.len()).sum::())
- .collect::>();
- let num_lookup_advice_per_phase = total_lookup_advice_per_phase
- .iter()
- .map(|count| (count + max_rows - 1) / max_rows)
- .collect::>();
-
- let total_fixed: usize = HashSet::::from_iter(self.threads.iter().flat_map(|threads| {
- threads.iter().flat_map(|ctx| ctx.constant_equality_constraints.iter().map(|(c, _)| *c))
- }))
- .len();
- let num_fixed = (total_fixed + (1 << k) - 1) >> k;
-
- let params = FlexGateConfigParams {
- strategy: GateStrategy::Vertical,
- num_advice_per_phase,
- num_lookup_advice_per_phase,
- num_fixed,
- k,
- };
- #[cfg(feature = "display")]
- {
- for phase in 0..MAX_PHASE {
- if total_advice_per_phase[phase] != 0 || total_lookup_advice_per_phase[phase] != 0 {
- println!(
- "Gate Chip | Phase {}: {} advice cells , {} lookup advice cells",
- phase, total_advice_per_phase[phase], total_lookup_advice_per_phase[phase],
- );
- }
- }
- println!("Total {total_fixed} fixed cells");
- println!("Auto-calculated config params:\n {params:#?}");
- }
- std::env::set_var("FLEX_GATE_CONFIG_PARAMS", serde_json::to_string(¶ms).unwrap());
- params
-}
-```
-
-For circuit creation a `GateCircuitBuilder` is created by passing the `GateThreadBuilder` as an argument to `GateCircuitBuilder`'s `keygen`,`mock`, or `prover` functions. `GateCircuitBuilder` acts as a middleman between `GateThreadBuilder` and the Halo2 backend by implementing Halo2's`Circuit` Trait and calling into `GateThreadBuilder` `assign_all()` and `assign_threads_in()` functions to perform circuit assignment.
-
-**Note for developers:** We encourage you to always use [`RangeCircuitBuilder`](#rangecircuitbuilder) instead of `GateCircuitBuilder`: the former is smart enough to know to not create a lookup table if no cells are marked for lookup, so `RangeCircuitBuilder` is a strict generalization of `GateCircuitBuilder`.
-
-```rust ignore
-/// Vector of vectors tracking the thread break points across different halo2 phases
-pub type MultiPhaseThreadBreakPoints = Vec;
-
-#[derive(Clone, Debug)]
-pub struct GateCircuitBuilder {
- /// The Thread Builder for the circuit
- pub builder: RefCell>,
- /// Break points for threads within the circuit
- pub break_points: RefCell,
-}
-
-impl Circuit for GateCircuitBuilder {
- type Config = FlexGateConfig;
- type FloorPlanner = SimpleFloorPlanner;
-
- /// Creates a new instance of the circuit without withnesses filled in.
- fn without_witnesses(&self) -> Self {
- unimplemented!()
- }
-
- /// Configures a new circuit using the the parameters specified [Config].
- fn configure(meta: &mut ConstraintSystem) -> FlexGateConfig {
- let FlexGateConfigParams {
- strategy,
- num_advice_per_phase,
- num_lookup_advice_per_phase: _,
- num_fixed,
- k,
- } = serde_json::from_str(&std::env::var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap();
- FlexGateConfig::configure(meta, strategy, &num_advice_per_phase, num_fixed, k)
- }
-
- /// Performs the actual computation on the circuit (e.g., witness generation), filling in all the advice values for a particular proof.
- fn synthesize(
- &self,
- config: Self::Config,
- mut layouter: impl Layouter,
- ) -> Result<(), Error> {
- self.sub_synthesize(&config, &[], &[], &mut layouter);
- Ok(())
- }
-}
-```
-
-During circuit creation `synthesize()` is invoked which passes into `sub_synthesize()` a `FlexGateConfig` containing the actual circuits columns and a mutable reference to a `Layouter` from the Halo2 API which facilitates the final assignment of cells within a `Region` of a circuit in Halo2's backend.
-
-`GateCircuitBuilder` contains a list of breakpoints for each thread across all phases in and `GateThreadBuilder` itself. Both are wrapped in a `RefCell` allowing them to be borrowed mutably so the function performing circuit creation can take ownership of the `builder` and `break_points` can be recorded during circuit creation for later use.
-
-[**sub_synthesize()**](./src/gates/builder.rs)
-```rust ignore
- pub fn sub_synthesize(
- &self,
- gate: &FlexGateConfig,
- lookup_advice: &[Vec>],
- q_lookup: &[Option],
- layouter: &mut impl Layouter,
- ) -> HashMap<(usize, usize), (circuit::Cell, usize)> {
- let mut first_pass = SKIP_FIRST_PASS;
- let mut assigned_advices = HashMap::new();
- layouter
- .assign_region(
- || "GateCircuitBuilder generated circuit",
- |mut region| {
- if first_pass {
- first_pass = false;
- return Ok(());
- }
- // only support FirstPhase in this Builder because getting challenge value requires more specialized witness generation during synthesize
- // If we are not performing witness generation only, we can skip the first pass and assign threads directly
- if !self.builder.borrow().witness_gen_only {
- // clone the builder so we can re-use the circuit for both vk and pk gen
- let builder = self.builder.borrow().clone();
- for threads in builder.threads.iter().skip(1) {
- assert!(
- threads.is_empty(),
- "GateCircuitBuilder only supports FirstPhase for now"
- );
- }
- let assignments = builder.assign_all(
- gate,
- lookup_advice,
- q_lookup,
- &mut region,
- Default::default(),
- );
- *self.break_points.borrow_mut() = assignments.break_points;
- assigned_advices = assignments.assigned_advices;
- } else {
- // If we are only generating witness, we can skip the first pass and assign threads directly
- let builder = self.builder.take();
- let break_points = self.break_points.take();
- for (phase, (threads, break_points)) in builder
- .threads
- .into_iter()
- .zip(break_points.into_iter())
- .enumerate()
- .take(1)
- {
- assign_threads_in(
- phase,
- threads,
- gate,
- lookup_advice.get(phase).unwrap_or(&vec![]),
- &mut region,
- break_points,
- );
- }
- }
- Ok(())
- },
- )
- .unwrap();
- assigned_advices
- }
-```
-
-Within `sub_synthesize()` `layouter`'s `assign_region()` function is invoked which yields a mutable reference to `Region`. `region` is used to assign cells within a contiguous region of the circuit represented in Halo2's proving system.
-
-If `witness_gen_only` is not set within the `builder` (for keygen, and mock proving) `sub_synthesize` takes ownership of the `builder`, and calls `assign_all()` to assign all cells within this context to a circuit in Halo2's backend. The resulting column breakpoints are recorded in `GateCircuitBuilder`'s `break_points` field.
-
-`assign_all()` iterates over each `Context` within a `phase` and assigns the values and constraints of the advice, selector, fixed, and lookup columns to the circuit using `region`.
-
-Breakpoints for the advice column are assigned sequentially. If, the `row_offset` of the cell value being currently assigned exceeds the maximum amount of rows allowed in a column a new column is created.
-
-It should be noted this process is only compatible with the first phase of Halo2's proving system as retrieving witness challenges in later phases requires more specialized witness generation during synthesis. Therefore, `assign_all()` must assert all elements in `threads` are unassigned excluding the first phase.
-
-[**assign_all()**](./src/gates/builder.rs)
-
-```rust ignore
-pub fn assign_all(
- &self,
- config: &FlexGateConfig,
- lookup_advice: &[Vec>],
- q_lookup: &[Option],
- region: &mut Region,
- KeygenAssignments {
- mut assigned_advices,
- mut assigned_constants,
- mut break_points
- }: KeygenAssignments,
- ) -> KeygenAssignments {
- ...
- for (phase, threads) in self.threads.iter().enumerate() {
- let mut break_point = vec![];
- let mut gate_index = 0;
- let mut row_offset = 0;
- for ctx in threads {
- let mut basic_gate = config.basic_gates[phase]
- .get(gate_index)
- .unwrap_or_else(|| panic!("NOT ENOUGH ADVICE COLUMNS IN PHASE {phase}. Perhaps blinding factors were not taken into account. The max non-poisoned rows is {max_rows}"));
- assert_eq!(ctx.selector.len(), ctx.advice.len());
-
- for (i, (advice, &q)) in ctx.advice.iter().zip(ctx.selector.iter()).enumerate() {
- let column = basic_gate.value;
- let value = if use_unknown { Value::unknown() } else { Value::known(advice) };
- #[cfg(feature = "halo2-axiom")]
- let cell = *region.assign_advice(column, row_offset, value).cell();
- #[cfg(not(feature = "halo2-axiom"))]
- let cell = region
- .assign_advice(|| "", column, row_offset, || value.map(|v| *v))
- .unwrap()
- .cell();
- assigned_advices.insert((ctx.context_id, i), (cell, row_offset));
- ...
-
-```
-
-In the case a breakpoint falls on the overlap between two gates (such as chained addition of two cells) the cells the breakpoint falls on must be copied to the next column and a new equality constraint enforced between the value of the cell in the old column and the copied cell in the new column. This prevents the circuit from being undersconstratined and preserves the equality constraint from the overlapping gates.
-
-```rust ignore
-if (q && row_offset + 4 > max_rows) || row_offset >= max_rows - 1 {
- break_point.push(row_offset);
- row_offset = 0;
- gate_index += 1;
-
-// when there is a break point, because we may have two gates that overlap at the current cell, we must copy the current cell to the next column for safety
- basic_gate = config.basic_gates[phase]
- .get(gate_index)
- .unwrap_or_else(|| panic!("NOT ENOUGH ADVICE COLUMNS IN PHASE {phase}. Perhaps blinding factors were not taken into account. The max non-poisoned rows is {max_rows}"));
- let column = basic_gate.value;
-
- #[cfg(feature = "halo2-axiom")]
- {
- let ncell = region.assign_advice(column, row_offset, value);
- region.constrain_equal(ncell.cell(), &cell);
- }
- #[cfg(not(feature = "halo2-axiom"))]
- {
- let ncell = region
- .assign_advice(|| "", column, row_offset, || value.map(|v| *v))
- .unwrap()
- .cell();
- region.constrain_equal(ncell, cell).unwrap();
- }
-}
-
-```
-
-If `witness_gen_only` is set, only witness generation is performed, and no copy constraints or selector values are considered.
-
-Witness generation can be parallelized by a user by calling `parallelize_in()` and specifying a function and a `Vec` of inputs to perform in parallel. `parallelize_in()` creates a separate `Context` for each input that performs the specified function and appends them to the `Vec` of `Context`'s of a particular phase.
-
-[**assign_threads_in()**](./src/gates/builder.rs)
-
-```rust ignore
-pub fn assign_threads_in(
- phase: usize,
- threads: Vec>,
- config: &FlexGateConfig,
- lookup_advice: &[Column],
- region: &mut Region,
- break_points: ThreadBreakPoints,
-) {
- if config.basic_gates[phase].is_empty() {
- assert!(threads.is_empty(), "Trying to assign threads in a phase with no columns");
- return;
- }
-
- let mut break_points = break_points.into_iter();
- let mut break_point = break_points.next();
-
- let mut gate_index = 0;
- let mut column = config.basic_gates[phase][gate_index].value;
- let mut row_offset = 0;
-
- let mut lookup_offset = 0;
- let mut lookup_advice = lookup_advice.iter();
- let mut lookup_column = lookup_advice.next();
- for ctx in threads {
- // if lookup_column is [None], that means there should be a single advice column and it has lookup enabled, so we don't need to copy to special lookup advice columns
- if lookup_column.is_some() {
- for advice in ctx.cells_to_lookup {
- if lookup_offset >= config.max_rows {
- lookup_offset = 0;
- lookup_column = lookup_advice.next();
- }
- // Assign the lookup advice values to the lookup_column
- let value = advice.value;
- let lookup_column = *lookup_column.unwrap();
- #[cfg(feature = "halo2-axiom")]
- region.assign_advice(lookup_column, lookup_offset, Value::known(value));
- #[cfg(not(feature = "halo2-axiom"))]
- region
- .assign_advice(|| "", lookup_column, lookup_offset, || Value::known(value))
- .unwrap();
-
- lookup_offset += 1;
- }
- }
- // Assign advice values to the advice columns in each [Context]
- for advice in ctx.advice {
- #[cfg(feature = "halo2-axiom")]
- region.assign_advice(column, row_offset, Value::known(advice));
- #[cfg(not(feature = "halo2-axiom"))]
- region.assign_advice(|| "", column, row_offset, || Value::known(advice)).unwrap();
-
- if break_point == Some(row_offset) {
- break_point = break_points.next();
- row_offset = 0;
- gate_index += 1;
- column = config.basic_gates[phase][gate_index].value;
-
- #[cfg(feature = "halo2-axiom")]
- region.assign_advice(column, row_offset, Value::known(advice));
- #[cfg(not(feature = "halo2-axiom"))]
- region.assign_advice(|| "", column, row_offset, || Value::known(advice)).unwrap();
- }
-
- row_offset += 1;
- }
- }
-
-```
-
-`sub_synthesize` iterates over all phases and calls `assign_threads_in()` for that phase. `assign_threads_in()` iterates over all `Context`s within that phase and assigns all lookup and advice values in the `Context`, creating a new advice column at every pre-computed "breakpoint" by incrementing `gate_index` and assigning `column` to a new `Column` found at `config.basic_gates[phase][gate_index].value`.
-
-## [**RangeCircuitBuilder**](./src/gates/builder.rs)
-
-`RangeCircuitBuilder` is a wrapper struct around `GateCircuitBuilder`. Like `GateCircuitBuilder` it acts as a middleman between `GateThreadBuilder` and the Halo2 backend by implementing Halo2's `Circuit` Trait.
-
-```rust ignore
-#[derive(Clone, Debug)]
-pub struct RangeCircuitBuilder(pub GateCircuitBuilder);
-
-impl Circuit for RangeCircuitBuilder {
- type Config = RangeConfig;
- type FloorPlanner = SimpleFloorPlanner;
-
- /// Creates a new instance of the [RangeCircuitBuilder] without witnesses by setting the witness_gen_only flag to false
- fn without_witnesses(&self) -> Self {
- unimplemented!()
- }
-
- /// Configures a new circuit using the the parameters specified [Config] and environment variable `LOOKUP_BITS`.
- fn configure(meta: &mut ConstraintSystem) -> Self::Config {
- let FlexGateConfigParams {
- strategy,
- num_advice_per_phase,
- num_lookup_advice_per_phase,
- num_fixed,
- k,
- } = serde_json::from_str(&var("FLEX_GATE_CONFIG_PARAMS").unwrap()).unwrap();
- let strategy = match strategy {
- GateStrategy::Vertical => RangeStrategy::Vertical,
- };
- let lookup_bits = var("LOOKUP_BITS").unwrap_or_else(|_| "0".to_string()).parse().unwrap();
- RangeConfig::configure(
- meta,
- strategy,
- &num_advice_per_phase,
- &num_lookup_advice_per_phase,
- num_fixed,
- lookup_bits,
- k,
- )
- }
-
- /// Performs the actual computation on the circuit (e.g., witness generation), populating the lookup table and filling in all the advice values for a particular proof.
- fn synthesize(
- &self,
- config: Self::Config,
- mut layouter: impl Layouter,
- ) -> Result<(), Error> {
- // 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(())
- }
-}
-```
-
-`RangeCircuitBuilder` differs from `GateCircuitBuilder` in that it contains a `RangeConfig` instead of a `FlexGateConfig` as its `Config`. `RangeConfig` contains a `lookup` table needed to declare lookup arguments within Halo2's backend. When creating a circuit that uses lookup tables `GateThreadBuilder` must be wrapped with `RangeCircuitBuilder` instead of `GateCircuitBuilder` otherwise circuit synthesis will fail as a lookup table is not present within the Halo2 backend.
+- **WitnessFraction**:
+ Assigns an entirely new witness value to the advice column. `WitnessFraction` exists for optimization purposes and accepts Assigned values wrapped in `Assigned::Rational()` marked for batch inverion (see [Assigned](#assigned)).
-**Note:** We encourage you to always use `RangeCircuitBuilder` instead of `GateCircuitBuilder`: the former is smart enough to know to not create a lookup table if no cells are marked for lookup, so `RangeCircuitBuilder` is a strict generalization of `GateCircuitBuilder`.
+- **Constant**:
+ A value that is a "known" constant. A "known" refers to known at circuit creation time to both the Prover and Verifier. When you assign a constant value there exists another secret Fixed column in the circuit constraint table whose values are fixed at circuit creation time. When you assign a Constant value, you are adding this value to the Fixed column, adding the value as a witness to the Advice column, and then imposing an equality constraint between the two corresponding cells in the Fixed and Advice columns.
diff --git a/halo2-base/src/gates/flex_gate/mod.rs b/halo2-base/src/gates/flex_gate/mod.rs
index 286b434b..dc931e5d 100644
--- a/halo2-base/src/gates/flex_gate/mod.rs
+++ b/halo2-base/src/gates/flex_gate/mod.rs
@@ -57,7 +57,6 @@ impl BasicGateConfig {
///
/// Assumes `phase` is in the range [0, MAX_PHASE).
/// * `meta`: [ConstraintSystem] used for the gate
- /// * `strategy`: The [GateStrategy] to use for the gate
/// * `phase`: The phase to add the gate to
pub fn configure(meta: &mut ConstraintSystem, phase: u8) -> Self {
let value = match phase {
@@ -118,10 +117,7 @@ impl FlexGateConfig {
///
/// Assumes `num_advice` is a [Vec] of length [MAX_PHASE]
/// * `meta`: [ConstraintSystem] of the circuit
- /// * `strategy`: [GateStrategy] of the flex gate
- /// * `num_advice`: Number of [Advice] [Column]s in each phase
- /// * `num_fixed`: Number of [Fixed] [Column]s in each phase
- /// * `circuit_degree`: Degree that expresses the size of circuit (i.e., 2^circuit_degree is the number of rows in the circuit)
+ /// * `params`: see [FlexGateConfigParams]
pub fn configure(meta: &mut ConstraintSystem, params: FlexGateConfigParams) -> Self {
// create fixed (constant) columns and enable equality constraints
let mut constants = Vec::with_capacity(params.num_fixed);
@@ -918,7 +914,7 @@ impl Default for GateChip {
}
impl GateChip {
- /// Returns a new [GateChip] with the given [GateStrategy].
+ /// Returns a new [GateChip] with some precomputed values. This can be called out of circuit and has no extra dependencies.
pub fn new() -> Self {
let mut pow_of_two = Vec::with_capacity(F::NUM_BITS as usize);
let two = F::from(2);
diff --git a/halo2-base/src/gates/range/mod.rs b/halo2-base/src/gates/range/mod.rs
index 79cdf155..a9ea1b59 100644
--- a/halo2-base/src/gates/range/mod.rs
+++ b/halo2-base/src/gates/range/mod.rs
@@ -52,12 +52,9 @@ impl RangeConfig {
///
/// Panics if `lookup_bits` > 28.
/// * `meta`: [ConstraintSystem] of the circuit
- /// * `range_strategy`: [GateStrategy] of the range chip
- /// * `num_advice`: Number of [Advice] [Column]s without lookup enabled in each phase
+ /// * `gate_params`: see [FlexGateConfigParams]
/// * `num_lookup_advice`: Number of `lookup_advice` [Column]s in each phase
- /// * `num_fixed`: Number of fixed [Column]s in each phase
/// * `lookup_bits`: Number of bits represented in the LookUp table [0,2^lookup_bits)
- /// * `circuit_degree`: Degree that expresses the size of circuit (i.e., 2^circuit_degree is the number of rows in the circuit)
pub fn configure(
meta: &mut ConstraintSystem,
gate_params: FlexGateConfigParams,
@@ -194,10 +191,13 @@ pub trait RangeInstructions {
num_bits: usize,
);
- /// Performs a range check that `a` has at most `bit_length(b)` bits and then constrains that `a` is less than `b`.
+ /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then constrains that `a` is less than `b`.
///
/// * a: [AssignedValue] value to check
/// * b: upper bound expressed as a [u64] value
+ ///
+ /// ## Assumptions
+ /// * `ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY`
fn check_less_than_safe(&self, ctx: &mut Context, a: AssignedValue, b: u64) {
let range_bits =
(bit_length(b) + self.lookup_bits() - 1) / self.lookup_bits() * self.lookup_bits();
@@ -206,10 +206,13 @@ pub trait RangeInstructions {
self.check_less_than(ctx, a, Constant(F::from(b)), range_bits)
}
- /// Performs a range check that `a` has at most `bit_length(b)` bits and then constrains that `a` is less than `b`.
+ /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then constrains that `a` is less than `b`.
///
/// * a: [AssignedValue] value to check
/// * b: upper bound expressed as a [BigUint] value
+ ///
+ /// ## Assumptions
+ /// * `ceil(b.bits() / lookup_bits) * lookup_bits <= F::CAPACITY`
fn check_big_less_than_safe(&self, ctx: &mut Context, a: AssignedValue, b: BigUint)
where
F: BigPrimeField,
@@ -280,10 +283,14 @@ pub trait RangeInstructions {
/// Constrains and returns `(c, r)` such that `a = b * c + r`.
///
- /// Assumes that `b != 0` and that `a` has <= `a_num_bits` bits.
/// * a: [QuantumCell] value to divide
/// * b: [BigUint] value to divide by
/// * a_num_bits: number of bits needed to represent the value of `a`
+ ///
+ /// ## Assumptions
+ /// * `b != 0` and that `a` has <= `a_num_bits` bits.
+ /// * `a_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+ /// * Unsafe behavior if `a_num_bits >= F::NUM_BITS`
fn div_mod(
&self,
ctx: &mut Context,
@@ -330,6 +337,10 @@ pub trait RangeInstructions {
/// * a_num_bits: number of bits needed to represent the value of `a`
/// * b_num_bits: number of bits needed to represent the value of `b`
///
+ /// ## Assumptions
+ /// * `a_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+ /// * `b_num_bits <= F::CAPACITY = F::NUM_BITS - 1`
+ /// * Unsafe behavior if `a_num_bits >= F::NUM_BITS` or `b_num_bits >= F::NUM_BITS`
fn div_mod_var(
&self,
ctx: &mut Context,
@@ -426,8 +437,13 @@ 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)
+ /// * `lookup_bits`: number of bits represented in the lookup table [0,2lookup_bits)
+ /// * `lookup_manager`: a [LookupAnyManager] for each phase.
+ ///
+ /// **IMPORTANT:** It is **critical** that all `LookupAnyManager`s use the same [`SharedCopyConstraintManager`](crate::virtual_region::copy_constraints::SharedCopyConstraintManager)
+ /// as in your primary circuit builder.
+ ///
+ /// It is not advised to call this function directly. Instead you should call `BaseCircuitBuilder::range_chip`.
pub fn new(lookup_bits: usize, lookup_manager: [LookupAnyManager; MAX_PHASE]) -> Self {
let limb_base = F::from(1u64 << lookup_bits);
let mut running_base = limb_base;
diff --git a/halo2-base/src/safe_types/bytes.rs b/halo2-base/src/safe_types/bytes.rs
index 1182dd8c..ff8bf238 100644
--- a/halo2-base/src/safe_types/bytes.rs
+++ b/halo2-base/src/safe_types/bytes.rs
@@ -41,7 +41,15 @@ impl VarLenBytes {
MAX_LEN
}
- /// Left pads the variable length byte array with 0s to the MAX_LEN
+ /// Left pads the variable length byte array with 0s to the `MAX_LEN`.
+ /// Takes a fixed length array `self.bytes` and returns a length `MAX_LEN` array equal to
+ /// `[[0; MAX_LEN - len], self.bytes[..len]].concat()`, i.e., we take `self.bytes[..len]` and
+ /// zero pad it on the left, where `len = self.len`
+ ///
+ /// Assumes `0 < self.len <= MAX_LEN`.
+ ///
+ /// ## Panics
+ /// If `self.len` is not in the range `(0, MAX_LEN]`.
pub fn left_pad_to_fixed(
&self,
ctx: &mut Context,
diff --git a/halo2-base/src/safe_types/mod.rs b/halo2-base/src/safe_types/mod.rs
index 08bff2c2..d9e3d5ab 100644
--- a/halo2-base/src/safe_types/mod.rs
+++ b/halo2-base/src/safe_types/mod.rs
@@ -259,6 +259,10 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
/// * inputs: Slice representing the byte array.
/// * len: [AssignedValue] witness representing the variable length of the byte array. Constrained to be `<= MAX_LEN`.
/// * MAX_LEN: [usize] representing the maximum length of the byte array and the number of elements it must contain.
+ ///
+ /// ## Assumptions
+ /// * `MAX_LEN < u64::MAX` to prevent overflow (but you should never make an array this large)
+ /// * `ceil((MAX_LEN + 1).bits() / lookup_bits) * lookup_bits <= F::CAPACITY` where `lookup_bits = self.range_chip.lookup_bits`
pub fn raw_to_var_len_bytes(
&self,
ctx: &mut Context,
@@ -275,6 +279,10 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> {
/// * inputs: Vector representing the byte array, right padded to `max_len`. See [VarLenBytesVec] for details about padding.
/// * len: [AssignedValue] witness representing the variable length of the byte array. Constrained to be `<= max_len`.
/// * max_len: [usize] representing the maximum length of the byte array and the number of elements it must contain. We enforce this to be provided explictly to make sure length of `inputs` is determinstic.
+ ///
+ /// ## Assumptions
+ /// * `max_len < u64::MAX` to prevent overflow (but you should never make an array this large)
+ /// * `ceil((max_len + 1).bits() / lookup_bits) * lookup_bits <= F::CAPACITY` where `lookup_bits = self.range_chip.lookup_bits`
pub fn raw_to_var_len_bytes_vec(
&self,
ctx: &mut Context,
diff --git a/halo2-ecc/src/fields/vector.rs b/halo2-ecc/src/fields/vector.rs
index 50d829c3..f007c3bf 100644
--- a/halo2-ecc/src/fields/vector.rs
+++ b/halo2-ecc/src/fields/vector.rs
@@ -245,6 +245,9 @@ where
FieldVector(a.into_iter().map(|coeff| self.fp_chip.carry_mod(ctx, coeff)).collect())
}
+ /// # Assumptions
+ /// * `max_bits <= n * k` where `n = self.fp_chip.limb_bits` and `k = self.fp_chip.num_limbs`
+ /// * `a[i].truncation.limbs.len() = self.fp_chip.num_limbs` for all `i = 0..a.len()`
pub fn range_check(
&self,
ctx: &mut Context,
@@ -432,6 +435,9 @@ macro_rules! impl_field_ext_chip_common {
self.0.carry_mod(ctx, a)
}
+ /// # Assumptions
+ /// * `max_bits <= n * k` where `n = self.fp_chip.limb_bits` and `k = self.fp_chip.num_limbs`
+ /// * `a[i].truncation.limbs.len() = self.fp_chip.num_limbs` for all `i = 0..a.len()`
fn range_check(
&self,
ctx: &mut Context,
diff --git a/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs b/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
index 46bb6481..d3d47da7 100644
--- a/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
+++ b/halo2-ecc/src/secp256k1/tests/ecdsa_tests.rs
@@ -1,5 +1,3 @@
-#![allow(non_snake_case)]
-use crate::ff::Field as _;
use crate::halo2_proofs::{
arithmetic::CurveAffine,
halo2curves::secp256k1::{Fq, Secp256k1Affine},