diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 63c4fdc7..a1fbae44 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -4,7 +4,7 @@ on: push: branches: ["main"] pull_request: - branches: ["main", "develop", "community-edition"] + branches: ["main", "develop", "community-edition", "release-*"] env: CARGO_TERM_COLOR: always @@ -40,6 +40,7 @@ jobs: working-directory: "hashes/zkevm" run: | cargo test packed_multi_keccak_prover::k_14 + cargo t test_vanilla_keccak_kat_vectors lint: name: Lint @@ -62,4 +63,12 @@ jobs: run: cargo fmt --all -- --check - name: Run clippy - run: cargo clippy --all -- -D warnings + run: cargo clippy --all --all-targets -- -D warnings + + - name: Generate Cargo.lock + run: cargo generate-lockfile + + - name: Run cargo audit + uses: actions-rs/audit-check@v1 + with: + token: ${{ secrets.GITHUB_TOKEN }} diff --git a/halo2-base/Cargo.toml b/halo2-base/Cargo.toml index 95ed9721..05387084 100644 --- a/halo2-base/Cargo.toml +++ b/halo2-base/Cargo.toml @@ -1,49 +1,48 @@ [package] -name="halo2-base" -version="0.4.0" -edition="2021" +name = "halo2-base" +version = "0.4.0" +edition = "2021" [dependencies] -itertools="0.11" -num-bigint={ version="0.4", features=["rand"] } -num-integer="0.1" -num-traits="0.2" -rand_chacha="0.3" -rustc-hash="1.1" -rayon="1.7" -serde={ version="1.0", features=["derive"] } -serde_json="1.0" -log="0.4" -getset="0.1.2" -ark-std={ version="0.3.0", features=["print-trace"], optional=true } +itertools = "0.11" +num-bigint = { version = "0.4", features = ["rand"] } +num-integer = "0.1" +num-traits = "0.2" +rand_chacha = "0.3" +rustc-hash = "1.1" +rayon = "1.8" +serde = { version = "1.0", features = ["derive"] } +serde_json = "1.0" +log = "0.4" +getset = "0.1.2" +ark-std = { version = "0.3.0", features = ["print-trace"], optional = true } # Use Axiom's custom halo2 monorepo for faster proving when feature = "halo2-axiom" is on -halo2_proofs_axiom={ git="https://github.com/axiom-crypto/halo2.git", package="halo2-axiom", optional=true } +halo2_proofs_axiom = { version = "0.4", package = "halo2-axiom", optional = true } # Use PSE halo2 and halo2curves for compatibility when feature = "halo2-pse" is on -halo2_proofs={ git="https://github.com/privacy-scaling-explorations/halo2.git", rev="7a21656", optional=true } +halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2.git", rev = "7a21656", optional = true } # This is Scroll's audited poseidon circuit. We only use it for the Native Poseidon spec. We do not use the halo2 circuit at all (and it wouldn't even work because the halo2_proofs tag is not compatbile). # We forked it to upgrade to ff v0.13 and removed the circuit module -poseidon-rs={ git="https://github.com/axiom-crypto/poseidon-circuit.git", rev="1aee4a1" } +poseidon-rs = { package = "poseidon-primitives", version = "=0.1.1" } # plotting circuit layout -plotters={ version="0.3.0", optional=true } -tabbycat={ version="0.1", features=["attributes"], optional=true } +plotters = { version = "0.3.0", optional = true } # test-utils rand={ version="0.8", optional=true } [dev-dependencies] -ark-std={ version="0.3.0", features=["print-trace"] } -rand="0.8" -pprof={ version="0.11", features=["criterion", "flamegraph"] } -criterion="0.4" -criterion-macro="0.4" -test-case="3.1.0" -test-log="0.2.12" -env_logger="0.10.0" -proptest="1.1.0" +ark-std = { version = "0.3.0", features = ["print-trace"] } +rand = "0.8" +pprof = { version = "0.13", features = ["criterion", "flamegraph"] } +criterion = "0.5.1" +criterion-macro = "0.4" +test-case = "3.1.0" +test-log = "0.2.12" +env_logger = "0.10.0" +proptest = "1.1.0" # native poseidon for testing -pse-poseidon={ git="https://github.com/axiom-crypto/pse-poseidon.git" } +pse-poseidon = { git = "https://github.com/axiom-crypto/pse-poseidon.git" } # memory allocation [target.'cfg(not(target_env = "msvc"))'.dependencies] @@ -52,23 +51,23 @@ jemallocator={ version="=0.5", optional=true } mimalloc={ version="=0.1", default-features=false, optional=true } [features] -default=["halo2-axiom", "display", "test-utils"] -asm=["halo2_proofs_axiom?/asm"] -dev-graph=["halo2_proofs?/dev-graph", "halo2_proofs_axiom?/dev-graph", "plotters"] -halo2-pse=["halo2_proofs/circuit-params"] -halo2-axiom=["halo2_proofs_axiom"] -display=[] -profile=["halo2_proofs_axiom?/profile"] -test-utils=["dep:rand", "ark-std"] +default = ["halo2-axiom", "display", "test-utils"] +asm = ["halo2_proofs_axiom?/asm"] +dev-graph = ["halo2_proofs/dev-graph", "plotters"] # only works with halo2-pse for now +halo2-pse = ["halo2_proofs/circuit-params"] +halo2-axiom = ["halo2_proofs_axiom"] +display = [] +profile = ["halo2_proofs_axiom?/profile"] +test-utils = ["dep:rand", "ark-std"] [[bench]] name="mul" harness=false [[bench]] -name="inner_product" -harness=false +name = "inner_product" +harness = false [[example]] -name="inner_product" -required-features=["test-utils"] +name = "inner_product" +required-features = ["test-utils"] diff --git a/halo2-base/README.md b/halo2-base/README.md index 6b078ab9..94cbbc58 100644 --- a/halo2-base/README.md +++ b/halo2-base/README.md @@ -1,92 +1,92 @@ -# 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`. +![Virtual regions with raw sub-circuit](https://user-images.githubusercontent.com/31040440/263155207-c5246cb1-f7f5-4214-920c-d4ae34c19e9c.png) -
+## [`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. + +**Warning:** If you create your own `Context` in a new virtual region not provided by our libraries, you must ensure that the `type_id: &str` of the context is a globally unique identifier for the virtual region, distinct from the other `type_id` strings used to identify other virtual regions. We suggest that you either include your crate name as a prefix in the `type_id` or use [`module_path!`](https://doc.rust-lang.org/std/macro.module_path.html) to generate a prefix. +In the future we will introduce a macro to check this uniqueness at compile time. ### [**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 +99,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 +117,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/circuit/builder.rs b/halo2-base/src/gates/circuit/builder.rs index 980abee9..dabd50f1 100644 --- a/halo2-base/src/gates/circuit/builder.rs +++ b/halo2-base/src/gates/circuit/builder.rs @@ -34,12 +34,12 @@ pub type RangeCircuitBuilder = BaseCircuitBuilder; /// A circuit builder is a collection of virtual region managers that together assign virtual /// regions into a single physical circuit. /// -/// [BaseCircuitBuilder] is a circuit builder to create a circuit where the columns correspond to [PublicBaseConfig]. -/// This builder can hold multiple threads, but the [Circuit] implementation only evaluates the first phase. -/// The user will have to implement a separate [Circuit] with multi-phase witness generation logic. +/// [BaseCircuitBuilder] is a circuit builder to create a circuit where the columns correspond to [super::BaseConfig]. +/// This builder can hold multiple threads, but the `Circuit` implementation only evaluates the first phase. +/// The user will have to implement a separate `Circuit` with multi-phase witness generation logic. /// -/// This is used to manage the virtual region corresponding to [FlexGateConfig] and (optionally) [RangeConfig]. -/// This can be used even if only using [GateChip] without [RangeChip]. +/// This is used to manage the virtual region corresponding to [super::FlexGateConfig] and (optionally) [RangeConfig]. +/// This can be used even if only using [`GateChip`](crate::gates::flex_gate::GateChip) without [RangeChip]. /// /// The circuit will have `NI` public instance (aka public inputs+outputs) columns. #[derive(Clone, Debug, Getters, MutGetters, Setters)] @@ -71,12 +71,12 @@ impl BaseCircuitBuilder { /// * If false, the builder also imposes constraints (selectors, fixed columns, copy constraints). Primarily used for keygen and mock prover (but can also be used for real prover). /// /// By default, **no** circuit configuration parameters have been set. - /// These should be set separately using [use_params], or [use_k], [use_lookup_bits], and [config]. + /// These should be set separately using `use_params`, or `use_k`, `use_lookup_bits`, and `calculate_params`. /// /// Upon construction, there are no public instances (aka all witnesses are private). /// The intended usage is that _before_ calling `synthesize`, witness generation can be done to populate /// assigned instances, which are supplied as `assigned_instances` to this struct. - /// The [`Circuit`] implementation for this struct will then expose these instances and constrain + /// The `Circuit` implementation for this struct will then expose these instances and constrain /// them using the Halo2 API. pub fn new(witness_gen_only: bool) -> Self { let core = MultiPhaseCoreManager::new(witness_gen_only); @@ -209,7 +209,7 @@ impl BaseCircuitBuilder { } /// Creates a new [MultiPhaseCoreManager] with `use_unknown` flag set. - /// * `use_unknown`: If true, during key generation witness [Value]s are replaced with Value::unknown() for safety. + /// * `use_unknown`: If true, during key generation witness `Value`s are replaced with `Value::unknown()` for safety. pub fn unknown(mut self, use_unknown: bool) -> Self { self.core = self.core.unknown(use_unknown); self @@ -321,7 +321,7 @@ impl BaseCircuitBuilder { /// /// ## Special case /// Just for [RangeConfig], we have special handling for the case where there is a single (physical) - /// advice column in [FlexGateConfig]. In this case, `RangeConfig` does not create extra lookup advice columns, + /// advice column in [super::FlexGateConfig]. In this case, `RangeConfig` does not create extra lookup advice columns, /// the single advice column has lookup enabled, and there is a selector to toggle when lookup should /// be turned on. pub fn assign_lookups_in_phase( @@ -372,3 +372,15 @@ pub struct RangeStatistics { /// Total special advice cells that need to be looked up, per phase pub total_lookup_advice_per_phase: Vec, } + +impl AsRef> for BaseCircuitBuilder { + fn as_ref(&self) -> &BaseCircuitBuilder { + self + } +} + +impl AsMut> for BaseCircuitBuilder { + fn as_mut(&mut self) -> &mut BaseCircuitBuilder { + self + } +} diff --git a/halo2-base/src/gates/circuit/mod.rs b/halo2-base/src/gates/circuit/mod.rs index 46dec873..8b3e6f60 100644 --- a/halo2-base/src/gates/circuit/mod.rs +++ b/halo2-base/src/gates/circuit/mod.rs @@ -19,7 +19,7 @@ pub mod builder; /// A struct defining the configuration parameters for a halo2-base circuit /// - this is used to configure [BaseConfig]. -#[derive(Clone, Default, Debug, Serialize, Deserialize)] +#[derive(Clone, Default, Debug, Hash, Serialize, Deserialize)] pub struct BaseCircuitParams { // Keeping FlexGateConfigParams expanded for backwards compatibility /// Specifies the number of rows in the circuit to be 2k @@ -146,12 +146,12 @@ impl Circuit for BaseCircuitBuilder { self.config_params.clone() } - /// Creates a new instance of the [RangeCircuitBuilder] without witnesses by setting the witness_gen_only flag to false + /// Creates a new instance of the [BaseCircuitBuilder] without witnesses by setting the witness_gen_only flag to false fn without_witnesses(&self) -> Self { unimplemented!() } - /// Configures a new circuit using [`BaseConfigParams`] + /// Configures a new circuit using [`BaseCircuitParams`] fn configure_with_params(meta: &mut ConstraintSystem, params: Self::Params) -> Self::Config { BaseConfig::configure(meta, params) } @@ -215,3 +215,15 @@ impl CircuitBuilderStage { matches!(self, CircuitBuilderStage::Prover) } } + +impl AsRef> for BaseConfig { + fn as_ref(&self) -> &BaseConfig { + self + } +} + +impl AsMut> for BaseConfig { + fn as_mut(&mut self) -> &mut BaseConfig { + self + } +} diff --git a/halo2-base/src/gates/flex_gate/mod.rs b/halo2-base/src/gates/flex_gate/mod.rs index 2938381b..e3031293 100644 --- a/halo2-base/src/gates/flex_gate/mod.rs +++ b/halo2-base/src/gates/flex_gate/mod.rs @@ -30,9 +30,9 @@ pub(super) const MAX_PHASE: usize = 3; /// # Vertical Gate Strategy: /// `q_0 * (a + b * c - d) = 0` /// where -/// * a = value[0], b = value[1], c = value[2], d = value[3] -/// * q = q_enable[0] -/// * q is either 0 or 1 so this is just a simple selector +/// * `a = value[0], b = value[1], c = value[2], d = value[3]` +/// * `q = q_enable[0]` +/// * `q` is either 0 or 1 so this is just a simple selector /// We chose `a + b * c` instead of `a * b + c` to allow "chaining" of gates, i.e., the output of one gate because `a` in the next gate. /// /// A configuration for a basic gate chip describing the selector, and advice column values. @@ -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 { @@ -116,12 +115,8 @@ pub struct FlexGateConfig { impl FlexGateConfig { /// Generates a new [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); @@ -739,7 +734,7 @@ pub trait GateInstructions { /// and that `indicator` has at most one `1` bit. /// * `ctx`: [Context] to add the constraints to /// * `a`: Iterator of [QuantumCell]'s that contains field elements - /// * `indicator`: Iterator of [AssignedValue]'s where indicator[i] == 1 if i == `idx`, otherwise 0 + /// * `indicator`: Iterator of [AssignedValue]'s where `indicator[i] == 1` if `i == idx`, otherwise `0` fn select_by_indicator( &self, ctx: &mut Context, @@ -858,7 +853,7 @@ pub trait GateInstructions { /// Constrains and returns little-endian bit vector representation of `a`. /// - /// Assumes `range_bits <= number of bits in a`. + /// Assumes `range_bits >= bit_length(a)`. /// * `a`: [QuantumCell] of the value to convert /// * `range_bits`: range of bits needed to represent `a` fn num_to_bits( @@ -948,7 +943,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/flex_gate/threads/multi_phase.rs b/halo2-base/src/gates/flex_gate/threads/multi_phase.rs index 40ce5103..ae893fb1 100644 --- a/halo2-base/src/gates/flex_gate/threads/multi_phase.rs +++ b/halo2-base/src/gates/flex_gate/threads/multi_phase.rs @@ -10,7 +10,7 @@ use crate::{ use super::SinglePhaseCoreManager; -/// Virtual region manager for [FlexGateConfig] in multiple phases. +/// Virtual region manager for [`FlexGateConfig`](super::super::FlexGateConfig) in multiple phases. #[derive(Clone, Debug, Default, CopyGetters)] pub struct MultiPhaseCoreManager { /// Virtual region for each challenge phase. These cannot be shared across threads while keeping circuit deterministic. @@ -20,7 +20,7 @@ pub struct MultiPhaseCoreManager { /// Flag for witness generation. If true, the gate thread builder is used for witness generation only. #[getset(get_copy = "pub")] 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. + /// The `unknown` flag is used during key generation. If true, during key generation witness `Value`s are replaced with `Value::unknown()` for safety. #[getset(get_copy = "pub")] use_unknown: bool, } @@ -59,7 +59,7 @@ impl MultiPhaseCoreManager { } /// Creates a new [MultiPhaseCoreManager] with `use_unknown` flag set. - /// * `use_unknown`: If true, during key generation witness [Value]s are replaced with Value::unknown() for safety. + /// * `use_unknown`: If true, during key generation witness values are replaced with `Value::unknown()` for safety. pub fn unknown(mut self, use_unknown: bool) -> Self { self.use_unknown = use_unknown; for pm in &mut self.phase_manager { diff --git a/halo2-base/src/gates/flex_gate/threads/single_phase.rs b/halo2-base/src/gates/flex_gate/threads/single_phase.rs index dd8b30d5..f9359814 100644 --- a/halo2-base/src/gates/flex_gate/threads/single_phase.rs +++ b/halo2-base/src/gates/flex_gate/threads/single_phase.rs @@ -1,4 +1,4 @@ -use std::{any::TypeId, cell::RefCell}; +use std::cell::RefCell; use getset::CopyGetters; @@ -13,14 +13,11 @@ use crate::{ Context, ContextCell, }; use crate::{ - halo2_proofs::{ - circuit::{Region, Value}, - plonk::{FirstPhase, SecondPhase, ThirdPhase}, - }, + halo2_proofs::circuit::{Region, Value}, virtual_region::manager::VirtualRegionManager, }; -/// Virtual region manager for [Vec] in a single challenge phase. +/// Virtual region manager for [`Vec`] in a single challenge phase. /// This is the core manager for [Context]s. #[derive(Clone, Debug, Default, CopyGetters)] pub struct SinglePhaseCoreManager { @@ -43,8 +40,8 @@ pub struct SinglePhaseCoreManager { } impl SinglePhaseCoreManager { - /// Creates a new [GateThreadBuilder] and spawns a main thread. - /// * `witness_gen_only`: If true, the [GateThreadBuilder] is used for witness generation only. + /// Creates a new [SinglePhaseCoreManager] and spawns a main thread. + /// * `witness_gen_only`: If true, the [SinglePhaseCoreManager] is used for witness generation only. /// * If true, the gate thread builder only does witness asignments and does not store constraint information -- this should only be used for the real prover. /// * If false, the gate thread builder is used for keygen and mock prover (it can also be used for real prover) and the builder stores circuit information (e.g. copy constraints, fixed columns, enabled selectors). /// * These values are fixed for the circuit at key generation time, and they do not need to be re-computed by the prover in the actual proving phase. @@ -64,7 +61,7 @@ impl SinglePhaseCoreManager { Self { phase, ..self } } - /// Creates a new [GateThreadBuilder] depending on the stage of circuit building. If the stage is [CircuitBuilderStage::Prover], the [GateThreadBuilder] is used for witness generation only. + /// Creates a new [SinglePhaseCoreManager] depending on the stage of circuit building. If the stage is [CircuitBuilderStage::Prover], the [SinglePhaseCoreManager] is used for witness generation only. pub fn from_stage( stage: CircuitBuilderStage, copy_manager: SharedCopyConstraintManager, @@ -73,7 +70,7 @@ impl SinglePhaseCoreManager { .unknown(stage == CircuitBuilderStage::Keygen) } - /// Creates a new [GateThreadBuilder] with `use_unknown` flag set. + /// Creates a new [SinglePhaseCoreManager] with `use_unknown` flag set. /// * `use_unknown`: If true, during key generation witness [Value]s are replaced with Value::unknown() for safety. pub fn unknown(self, use_unknown: bool) -> Self { Self { use_unknown, ..self } @@ -114,11 +111,11 @@ impl SinglePhaseCoreManager { } /// A distinct tag for this particular type of virtual manager, which is different for each phase. - pub fn type_of(&self) -> TypeId { + pub fn type_of(&self) -> &'static str { match self.phase { - 0 => TypeId::of::<(Self, FirstPhase)>(), - 1 => TypeId::of::<(Self, SecondPhase)>(), - 2 => TypeId::of::<(Self, ThirdPhase)>(), + 0 => "halo2-base:SinglePhaseCoreManager:FirstPhase", + 1 => "halo2-base:SinglePhaseCoreManager:SecondPhase", + 2 => "halo2-base:SinglePhaseCoreManager:ThirdPhase", _ => panic!("Unsupported phase"), } } diff --git a/halo2-base/src/gates/range/mod.rs b/halo2-base/src/gates/range/mod.rs index 0222cde1..bba88228 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, @@ -235,7 +238,7 @@ pub trait RangeInstructions { num_bits: usize, ) -> AssignedValue; - /// Performs a range check that `a` has at most `ceil(bit_length(b) / lookup_bits) * lookup_bits` and then constrains that `a` is in `[0,b)`. + /// Performs a range check that `a` has at most `ceil(bit_length(b) / lookup_bits) * lookup_bits` and then returns whether `a` is in `[0,b)`. /// /// Returns 1 if `a` < `b`, otherwise 0. /// @@ -254,14 +257,14 @@ pub trait RangeInstructions { self.is_less_than(ctx, a, Constant(F::from(b)), range_bits) } - /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then constrains that `a` is in `[0,b)`. + /// Performs a range check that `a` has at most `ceil(b.bits() / lookup_bits) * lookup_bits` bits and then returns whether `a` is in `[0,b)`. /// /// Returns 1 if `a` < `b`, otherwise 0. /// /// * a: [AssignedValue] value to check /// * b: upper bound as [BigUint] value /// - /// For the current implementation using [`is_less_than`], we require `ceil(b.bits() / lookup_bits) + 1 < F::NUM_BITS / lookup_bits` + /// For the current implementation using `is_less_than`, we require `ceil(b.bits() / lookup_bits) + 1 < F::NUM_BITS / lookup_bits` fn is_big_less_than_safe( &self, ctx: &mut Context, @@ -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, @@ -437,7 +448,7 @@ pub trait RangeInstructions { pub struct RangeChip { /// Underlying [GateChip] for this chip. pub gate: GateChip, - /// Lookup manager for each phase, lazily initiated using the [SharedCopyConstraintManager] from the [Context] + /// Lookup manager for each phase, lazily initiated using the [`SharedCopyConstraintManager`](crate::virtual_region::copy_constraints::SharedCopyConstraintManager) from the [Context] /// that first calls it. /// /// The lookup manager is used to store the cells that need to be looked up in the range check lookup table. @@ -452,8 +463,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/gates/tests/flex_gate.rs b/halo2-base/src/gates/tests/flex_gate.rs index 53cf9513..49243dd5 100644 --- a/halo2-base/src/gates/tests/flex_gate.rs +++ b/halo2-base/src/gates/tests/flex_gate.rs @@ -100,7 +100,7 @@ pub fn test_inner_product_left_last( } #[test_case([4,5,6].map(Fr::from).to_vec(), [1,2,3].map(|x| Constant(Fr::from(x))).to_vec() => (Fr::from(32), [4,5,6].map(Fr::from).to_vec()); -"inner_product_left(): <[1,2,3],[4,5,6]> Constant b starts with 1")] +"inner_product_left(): <[4,5,6],[1,2,3]> Constant b starts with 1")] #[test_case([1,2,3].map(Fr::from).to_vec(), [4,5,6].map(|x| Witness(Fr::from(x))).to_vec() => (Fr::from(32), [1,2,3].map(Fr::from).to_vec()); "inner_product_left(): <[1,2,3],[4,5,6]> Witness")] pub fn test_inner_product_left(a: Vec, b: Vec>) -> (Fr, Vec) { diff --git a/halo2-base/src/gates/tests/general.rs b/halo2-base/src/gates/tests/general.rs index 06f32f20..6e686332 100644 --- a/halo2-base/src/gates/tests/general.rs +++ b/halo2-base/src/gates/tests/general.rs @@ -59,19 +59,19 @@ fn plot_gates() { let k = 5; use plotters::prelude::*; + use crate::gates::circuit::builder::BaseCircuitBuilder; + let root = BitMapBackend::new("layout.png", (1024, 1024)).into_drawing_area(); root.fill(&WHITE).unwrap(); let root = root.titled("Gates Layout", ("sans-serif", 60)).unwrap(); let inputs = [Fr::zero(); 3]; - let builder = GateThreadBuilder::new(false); + let mut builder = BaseCircuitBuilder::new(false).use_k(k); gate_tests(builder.main(0), inputs); // auto-tune circuit - builder.config(k, Some(9)); - // create circuit - let circuit = RangeCircuitBuilder::keygen(builder); - halo2_proofs::dev::CircuitLayout::default().render(k, &circuit, &root).unwrap(); + builder.calculate_params(Some(9)); + halo2_proofs::dev::CircuitLayout::default().render(k as u32, &builder, &root).unwrap(); } */ diff --git a/halo2-base/src/lib.rs b/halo2-base/src/lib.rs index 8b86c582..669bc1ad 100644 --- a/halo2-base/src/lib.rs +++ b/halo2-base/src/lib.rs @@ -9,8 +9,6 @@ #![warn(clippy::default_numeric_fallback)] #![warn(missing_docs)] -use std::any::TypeId; - use getset::CopyGetters; use itertools::Itertools; // Different memory allocator options: @@ -82,16 +80,16 @@ pub enum QuantumCell { } impl From> for QuantumCell { - /// Converts an [AssignedValue] into a [QuantumCell] of [type Existing(AssignedValue)] + /// Converts an [`AssignedValue`] into a [`QuantumCell`] of enum variant `Existing`. fn from(a: AssignedValue) -> Self { Self::Existing(a) } } impl QuantumCell { - /// Returns an immutable reference to the underlying [ScalarField] value of a QuantumCell. + /// Returns an immutable reference to the underlying [ScalarField] value of a [`QuantumCell`]. /// - /// Panics if the QuantumCell is of type WitnessFraction. + /// Panics if the [`QuantumCell`] is of type `WitnessFraction`. pub fn value(&self) -> &F { match self { Self::Existing(a) => a.value(), @@ -104,14 +102,16 @@ impl QuantumCell { } } -/// Unique tag for a context across all virtual regions -pub type ContextTag = (TypeId, usize); +/// Unique tag for a context across all virtual regions. +/// In the form `(type_id, context_id)` where `type_id` should be a unique identifier +/// for the virtual region this context belongs to, and `context_id` is a counter local to that virtual region. +pub type ContextTag = (&'static str, usize); /// Pointer to the position of a cell at `offset` in an advice column within a [Context] of `context_id`. #[derive(Clone, Copy, Debug, Hash, PartialEq, Eq, PartialOrd, Ord)] pub struct ContextCell { - /// The [TypeId] of the virtual region that this cell belongs to. - pub type_id: TypeId, + /// The unique string identifier of the virtual region that this cell belongs to. + pub type_id: &'static str, /// Identifier of the [Context] that this cell belongs to. pub context_id: usize, /// Relative offset of the cell within this [Context] advice column. @@ -120,7 +120,10 @@ pub struct ContextCell { impl ContextCell { /// Creates a new [ContextCell] with the given `type_id`, `context_id`, and `offset`. - pub fn new(type_id: TypeId, context_id: usize, offset: usize) -> Self { + /// + /// **Warning:** If you create your own `Context` in a new virtual region not provided by our libraries, you must ensure that the `type_id: &str` of the context is a globally unique identifier for the virtual region, distinct from the other `type_id` strings used to identify other virtual regions. We suggest that you either include your crate name as a prefix in the `type_id` or use [`module_path!`](https://doc.rust-lang.org/std/macro.module_path.html) to generate a prefix. + /// In the future we will introduce a macro to check this uniqueness at compile time. + pub fn new(type_id: &'static str, context_id: usize, offset: usize) -> Self { Self { type_id, context_id, offset } } } @@ -144,9 +147,9 @@ impl<'a, F: ScalarField> From<&'a AssignedValue> for AssignedValue { } impl AssignedValue { - /// Returns an immutable reference to the underlying value of an AssignedValue. + /// Returns an immutable reference to the underlying value of an [`AssignedValue`]. /// - /// Panics if the AssignedValue is of type WitnessFraction. + /// Panics if the witness value is of type [Assigned::Rational] or [Assigned::Zero]. pub fn value(&self) -> &F { match &self.value { Assigned::Trivial(a) => a, @@ -180,9 +183,11 @@ pub struct Context { /// The challenge phase that this [Context] will map to. #[getset(get_copy = "pub")] phase: usize, - /// Identifier for what virtual region this context is in + /// Identifier for what virtual region this context is in. + /// Warning: the circuit writer must ensure that distinct virtual regions have distinct names as strings to prevent possible errors. + /// We do not use [std::any::TypeId] because it is not stable across rust builds or dependencies. #[getset(get_copy = "pub")] - type_id: TypeId, + type_id: &'static str, /// Identifier to reference cells from this [Context]. context_id: usize, @@ -207,10 +212,13 @@ impl Context { /// Creates a new [Context] with the given `context_id` and witness generation enabled/disabled by the `witness_gen_only` flag. /// * `witness_gen_only`: flag to determine whether public key generation or only witness generation is being performed. /// * `context_id`: identifier to reference advice cells from this [Context] later. + /// + /// **Warning:** If you create your own `Context` in a new virtual region not provided by our libraries, you must ensure that the `type_id: &str` of the context is a globally unique identifier for the virtual region, distinct from the other `type_id` strings used to identify other virtual regions. We suggest that you either include your crate name as a prefix in the `type_id` or use [`module_path!`](https://doc.rust-lang.org/std/macro.module_path.html) to generate a prefix. + /// In the future we will introduce a macro to check this uniqueness at compile time. pub fn new( witness_gen_only: bool, phase: usize, - type_id: TypeId, + type_id: &'static str, context_id: usize, copy_manager: SharedCopyConstraintManager, ) -> Self { @@ -240,8 +248,7 @@ impl Context { ContextCell::new(self.type_id, self.context_id, self.advice.len() - 1) } - /// Pushes a [QuantumCell] to the end of the `advice` column ([Vec] of advice cells) in this [Context]. - /// * `input`: the cell to be assigned. + /// Virtually assigns the `input` within the current [Context], with different handling depending on the [QuantumCell] variant. pub fn assign_cell(&mut self, input: impl Into>) { // Determine the type of the cell and push it to the relevant vector match input.into() { @@ -319,7 +326,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]). + /// * `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) pub fn assign_region( &mut self, diff --git a/halo2-base/src/poseidon/hasher/mod.rs b/halo2-base/src/poseidon/hasher/mod.rs index 10a03034..68cf64c6 100644 --- a/halo2-base/src/poseidon/hasher/mod.rs +++ b/halo2-base/src/poseidon/hasher/mod.rs @@ -8,7 +8,7 @@ use crate::{ ScalarField, }; -use getset::Getters; +use getset::{CopyGetters, Getters}; use num_bigint::BigUint; use std::{cell::OnceCell, mem}; @@ -23,8 +23,10 @@ pub mod spec; pub mod state; /// Stateless Poseidon hasher. -#[derive(Clone, Debug)] +#[derive(Clone, Debug, Getters)] pub struct PoseidonHasher { + /// Spec, contains round constants and optimized matrices. + #[getset(get = "pub")] spec: OptimizedPoseidonSpec, consts: OnceCell>, } @@ -51,13 +53,16 @@ impl PoseidonHasherConsts { - // Right padded inputs. No constrains on paddings. + /// Right padded inputs. No constrains on paddings. + #[getset(get = "pub")] inputs: [AssignedValue; RATE], - // is_final = 1 triggers squeeze. + /// is_final = 1 triggers squeeze. + #[getset(get_copy = "pub")] is_final: SafeBool, - // Length of `inputs`. + /// Length of `inputs`. + #[getset(get_copy = "pub")] len: AssignedValue, } @@ -87,11 +92,13 @@ impl PoseidonCompactInput { } /// A compact chunk input for Poseidon hasher. The end of a logical input could only be at the boundary of a chunk. -#[derive(Clone, Debug)] +#[derive(Clone, Debug, Getters, CopyGetters)] pub struct PoseidonCompactChunkInput { - // Inputs of a chunk. All witnesses will be absorbed. + /// Inputs of a chunk. All witnesses will be absorbed. + #[getset(get = "pub")] inputs: Vec<[AssignedValue; RATE]>, - // is_final = 1 triggers squeeze. + /// is_final = 1 triggers squeeze. + #[getset(get_copy = "pub")] is_final: SafeBool, } @@ -103,13 +110,13 @@ impl PoseidonCompactChunkInput { } /// 1 logical row of compact output for Poseidon hasher. -#[derive(Copy, Clone, Debug, Getters)] +#[derive(Copy, Clone, Debug, CopyGetters)] pub struct PoseidonCompactOutput { /// hash of 1 logical input. - #[getset(get = "pub")] + #[getset(get_copy = "pub")] hash: AssignedValue, /// is_final = 1 ==> this is the end of a logical input. - #[getset(get = "pub")] + #[getset(get_copy = "pub")] is_final: SafeBool, } diff --git a/halo2-base/src/poseidon/hasher/tests/hasher.rs b/halo2-base/src/poseidon/hasher/tests/hasher.rs index 043bf221..7b55c3c4 100644 --- a/halo2-base/src/poseidon/hasher/tests/hasher.rs +++ b/halo2-base/src/poseidon/hasher/tests/hasher.rs @@ -1,6 +1,6 @@ use crate::{ gates::{range::RangeInstructions, RangeChip}, - halo2_proofs::halo2curves::bn256::Fr, + halo2_proofs::{arithmetic::Field, halo2curves::bn256::Fr}, poseidon::hasher::{ spec::OptimizedPoseidonSpec, PoseidonCompactChunkInput, PoseidonCompactInput, PoseidonHasher, @@ -9,7 +9,6 @@ use crate::{ utils::{testing::base_test, ScalarField}, Context, }; -use halo2_proofs_axiom::arithmetic::Field; use itertools::Itertools; use pse_poseidon::Poseidon; use rand::Rng; @@ -161,7 +160,7 @@ fn hasher_compact_chunk_inputs_compatiblity_verification< for (compact_output, chunk_input) in compact_outputs.iter().zip(chunk_inputs) { // into() doesn't work if ! is in the beginning in the bool expression... let is_final_input = chunk_input.is_final.as_ref().value(); - let is_final_output = compact_output.is_final().as_ref().value(); + let is_final_output = compact_output.is_final.as_ref().value(); assert_eq!(is_final_input, is_final_output); if is_final_output == &Fr::ONE { assert_eq!(native_results[output_offset], *compact_output.hash().value()); diff --git a/halo2-base/src/safe_types/bytes.rs b/halo2-base/src/safe_types/bytes.rs index e1a5e03d..ff8bf238 100644 --- a/halo2-base/src/safe_types/bytes.rs +++ b/halo2-base/src/safe_types/bytes.rs @@ -27,8 +27,8 @@ pub struct VarLenBytes { } impl VarLenBytes { - // VarLenBytes can be only created by SafeChip. - pub(super) fn new(bytes: [SafeByte; MAX_LEN], len: AssignedValue) -> Self { + /// Slightly unsafe constructor: it is not constrained that `len <= MAX_LEN`. + pub fn new(bytes: [SafeByte; MAX_LEN], len: AssignedValue) -> Self { assert!( len.value().le(&F::from(MAX_LEN as u64)), "Invalid length which exceeds MAX_LEN {MAX_LEN}", @@ -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, @@ -76,8 +84,8 @@ pub struct VarLenBytesVec { } impl VarLenBytesVec { - // VarLenBytesVec can be only created by SafeChip. - pub(super) fn new(bytes: Vec>, len: AssignedValue, max_len: usize) -> Self { + /// Slightly unsafe constructor: it is not constrained that `len <= max_len`. + pub fn new(bytes: Vec>, len: AssignedValue, max_len: usize) -> Self { assert!( len.value().le(&F::from(max_len as u64)), "Invalid length which exceeds MAX_LEN {}", @@ -118,8 +126,8 @@ pub struct FixLenBytes { } impl FixLenBytes { - // FixLenBytes can be only created by SafeChip. - pub(super) fn new(bytes: [SafeByte; LEN]) -> Self { + /// Constructor + pub fn new(bytes: [SafeByte; LEN]) -> Self { Self { bytes } } @@ -143,8 +151,8 @@ pub struct FixLenBytesVec { } impl FixLenBytesVec { - // FixLenBytes can be only created by SafeChip. - pub(super) fn new(bytes: Vec>, len: usize) -> Self { + /// Constructor + pub fn new(bytes: Vec>, len: usize) -> Self { assert_eq!(bytes.len(), len, "bytes length doesn't match"); Self { bytes } } diff --git a/halo2-base/src/safe_types/mod.rs b/halo2-base/src/safe_types/mod.rs index 5f874fd5..205c314e 100644 --- a/halo2-base/src/safe_types/mod.rs +++ b/halo2-base/src/safe_types/mod.rs @@ -1,5 +1,5 @@ use std::{ - borrow::{Borrow, BorrowMut}, + borrow::Borrow, cmp::{max, min}, }; @@ -28,16 +28,16 @@ type RawAssignedValues = Vec>; const BITS_PER_BYTE: usize = 8; -/// SafeType's goal is to avoid out-of-range undefined behavior. -/// When building circuits, it's common to use multiple AssignedValue to represent -/// a logical variable. For example, we might want to represent a hash with 32 AssignedValue -/// where each AssignedValue represents 1 byte. However, the range of AssignedValue is much -/// larger than 1 byte(0~255). If a circuit takes 32 AssignedValue as inputs and some of them +/// [`SafeType`]'s goal is to avoid out-of-range undefined behavior. +/// When building circuits, it's common to use multiple [`AssignedValue`]s to represent +/// a logical variable. For example, we might want to represent a hash with 32 [`AssignedValue`] +/// where each [`AssignedValue`] represents 1 byte. However, the range of [`AssignedValue`] is much +/// larger than 1 byte(0~255). If a circuit takes 32 [`AssignedValue`] as inputs and some of them /// are actually greater than 255, there could be some undefined behaviors. -/// SafeType guarantees the value range of its owned AssignedValue. So circuits don't need to +/// [`SafeType`] gurantees the value range of its owned [`AssignedValue`]. So circuits don't need to /// do any extra value checking if they take SafeType as inputs. -/// TOTAL_BITS is the number of total bits of this type. -/// BYTES_PER_ELE is the number of bytes of each element. +/// - `TOTAL_BITS` is the number of total bits of this type. +/// - `BYTES_PER_ELE` is the number of bytes of each element. #[derive(Clone, Debug)] pub struct SafeType { // value is stored in little-endian. @@ -255,10 +255,13 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { /// Converts a slice of AssignedValue(treated as little-endian) to VarLenBytes. /// - /// * ctx: Circuit [Context] to assign witnesses to. /// * inputs: Slice representing the byte array. - /// * len: [AssignedValue] witness representing the variable length of the byte array. Constrained to be `<= MAX_LEN`. + /// * 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, @@ -271,10 +274,13 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { /// Converts a vector of AssignedValue to [VarLenBytesVec]. Not encouraged to use because `MAX_LEN` cannot be verified at compile time. /// - /// * ctx: Circuit [Context] to assign witnesses to. /// * 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 explicitly to make sure length of `inputs` is determinstic. + /// * 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, @@ -292,7 +298,6 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { /// Converts a slice of AssignedValue(treated as little-endian) to FixLenBytes. /// - /// * ctx: Circuit [Context] to assign witnesses to. /// * inputs: Slice representing the byte array. /// * LEN: length of the byte array. pub fn raw_to_fix_len_bytes( @@ -305,9 +310,8 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { /// Converts a slice of AssignedValue(treated as little-endian) to FixLenBytesVec. /// - /// * ctx: Circuit [Context] to assign witnesses to. /// * inputs: Slice representing the byte array. - /// * len: length of the byte array. We enforce this to be provided explicitly to make sure length of `inputs` is determinstic. + /// * len: length of the byte array. We enforce this to be provided explictly to make sure length of `inputs` is determinstic. pub fn raw_to_fix_len_bytes_vec( &self, ctx: &mut Context, @@ -320,6 +324,7 @@ impl<'a, F: ScalarField> SafeTypeChip<'a, F> { ) } + /// Assumes that `bits <= inputs.len() * 8`. fn add_bytes_constraints( &self, ctx: &mut Context, diff --git a/halo2-base/src/safe_types/primitives.rs b/halo2-base/src/safe_types/primitives.rs index 86726595..92e00f2d 100644 --- a/halo2-base/src/safe_types/primitives.rs +++ b/halo2-base/src/safe_types/primitives.rs @@ -1,17 +1,21 @@ +use std::ops::Deref; + +use crate::QuantumCell; + use super::*; /// SafeType for bool (1 bit). /// -/// This is a separate struct from [`CompactSafeType`] with the same behavior. Because +/// This is a separate struct from `CompactSafeType` with the same behavior. Because /// we know only one [`AssignedValue`] is needed to hold the boolean value, we avoid -/// using [`CompactSafeType`] to avoid the additional heap allocation from a length 1 vector. +/// using `CompactSafeType` to avoid the additional heap allocation from a length 1 vector. #[derive(Clone, Copy, Debug)] pub struct SafeBool(pub(super) AssignedValue); /// SafeType for byte (8 bits). /// -/// This is a separate struct from [`CompactSafeType`] with the same behavior. Because +/// This is a separate struct from `CompactSafeType` with the same behavior. Because /// we know only one [`AssignedValue`] is needed to hold the boolean value, we avoid -/// using [`CompactSafeType`] to avoid the additional heap allocation from a length 1 vector. +/// using `CompactSafeType` to avoid the additional heap allocation from a length 1 vector. #[derive(Clone, Copy, Debug)] pub struct SafeByte(pub(super) AssignedValue); @@ -23,21 +27,17 @@ macro_rules! safe_primitive_impls { } } - impl AsMut> for $SafePrimitive { - fn as_mut(&mut self) -> &mut AssignedValue { - &mut self.0 - } - } - impl Borrow> for $SafePrimitive { fn borrow(&self) -> &AssignedValue { &self.0 } } - impl BorrowMut> for $SafePrimitive { - fn borrow_mut(&mut self) -> &mut AssignedValue { - &mut self.0 + impl Deref for $SafePrimitive { + type Target = AssignedValue; + + fn deref(&self) -> &Self::Target { + &self.0 } } @@ -46,6 +46,12 @@ macro_rules! safe_primitive_impls { safe_primitive.0 } } + + impl From<$SafePrimitive> for QuantumCell { + fn from(safe_primitive: $SafePrimitive) -> Self { + QuantumCell::Existing(safe_primitive.0) + } + } }; } diff --git a/halo2-base/src/utils/halo2.rs b/halo2-base/src/utils/halo2.rs index 510f7d25..463b128f 100644 --- a/halo2-base/src/utils/halo2.rs +++ b/halo2-base/src/utils/halo2.rs @@ -3,6 +3,8 @@ use crate::halo2_proofs::{ circuit::{AssignedCell, Cell, Region, Value}, plonk::{Advice, Assigned, Column, Fixed}, }; +use crate::virtual_region::copy_constraints::{CopyConstraintManager, SharedCopyConstraintManager}; +use crate::AssignedValue; /// Raw (physical) assigned cell in Plonkish arithmetization. #[cfg(feature = "halo2-axiom")] @@ -71,3 +73,43 @@ pub fn raw_constrain_equal(region: &mut Region, left: Cell, right: #[cfg(not(feature = "halo2-axiom"))] region.constrain_equal(left, right).unwrap(); } + +/// Assign virtual cell to raw halo2 cell in column `column` at row offset `offset` within the `region`. +/// Stores the mapping between `virtual_cell` and the raw assigned cell in `copy_manager`, if provided. +/// +/// `copy_manager` **must** be provided unless you are only doing witness generation +/// without constraints. +pub fn assign_virtual_to_raw<'v, F: Field + Ord>( + region: &mut Region, + column: Column, + offset: usize, + virtual_cell: AssignedValue, + copy_manager: Option<&SharedCopyConstraintManager>, +) -> Halo2AssignedCell<'v, F> { + let raw = raw_assign_advice(region, column, offset, Value::known(virtual_cell.value)); + if let Some(copy_manager) = copy_manager { + let mut copy_manager = copy_manager.lock().unwrap(); + let cell = virtual_cell.cell.unwrap(); + copy_manager.assigned_advices.insert(cell, raw.cell()); + drop(copy_manager); + } + raw +} + +/// Constrains that `virtual` is equal to `external`. The `virtual` cell must have +/// **already** been raw assigned, with the raw assigned cell stored in `copy_manager`. +/// +/// This should only be called when `witness_gen_only` is false, otherwise it will panic. +/// +/// ## Panics +/// If witness generation only mode is true. +pub fn constrain_virtual_equals_external( + region: &mut Region, + virtual_cell: AssignedValue, + external_cell: Cell, + copy_manager: &CopyConstraintManager, +) { + let ctx_cell = virtual_cell.cell.unwrap(); + let acell = copy_manager.assigned_advices.get(&ctx_cell).expect("cell not assigned"); + region.constrain_equal(*acell, external_cell); +} diff --git a/halo2-base/src/virtual_region/copy_constraints.rs b/halo2-base/src/virtual_region/copy_constraints.rs index d9fe6742..5ab80d3b 100644 --- a/halo2-base/src/virtual_region/copy_constraints.rs +++ b/halo2-base/src/virtual_region/copy_constraints.rs @@ -1,4 +1,3 @@ -use std::any::TypeId; use std::collections::{BTreeMap, HashMap}; use std::ops::DerefMut; use std::sync::{Arc, Mutex, OnceLock}; @@ -80,14 +79,15 @@ impl CopyConstraintManager { self.load_external_cell_impl(Some(cell)) } - /// Mock to load an external cell for base circuit simulation. If any mock external cell is loaded, calling [assign_raw] will panic. + /// Mock to load an external cell for base circuit simulation. If any mock external cell is loaded, calling `assign_raw` will panic. pub fn mock_external_assigned(&mut self, v: F) -> AssignedValue { let context_cell = self.load_external_cell_impl(None); AssignedValue { value: Assigned::Trivial(v), cell: Some(context_cell) } } fn load_external_cell_impl(&mut self, cell: Option) -> ContextCell { - let context_cell = ContextCell::new(TypeId::of::(), 0, self.external_cell_count); + let context_cell = + ContextCell::new("halo2-base:External Raw Halo2 Cell", 0, self.external_cell_count); self.external_cell_count += 1; if let Some(cell) = cell { self.assigned_advices.insert(context_cell, cell); diff --git a/halo2-base/src/virtual_region/lookups.rs b/halo2-base/src/virtual_region/lookups.rs index bf82f211..3e301921 100644 --- a/halo2-base/src/virtual_region/lookups.rs +++ b/halo2-base/src/virtual_region/lookups.rs @@ -8,12 +8,15 @@ use crate::halo2_proofs::{ circuit::{Region, Value}, plonk::{Advice, Column}, }; -use crate::utils::halo2::raw_assign_advice; +use crate::utils::halo2::{constrain_virtual_equals_external, raw_assign_advice}; use crate::{AssignedValue, ContextTag}; use super::copy_constraints::SharedCopyConstraintManager; use super::manager::VirtualRegionManager; +/// Basic dynamic lookup table gadget. +pub mod basic; + /// A manager that can be used for any lookup argument. This manager automates /// the process of copying cells to designed advice columns with lookup enabled. /// It also manages how many such advice columns are necessary. @@ -29,12 +32,12 @@ use super::manager::VirtualRegionManager; /// /// We want this manager to be CPU thread safe, while ensuring that the resulting circuit is /// deterministic -- the order in which the cells to lookup are added matters. -/// The current solution is to tag the cells to lookup with the context id from the [Context] in which +/// The current solution is to tag the cells to lookup with the context id from the [`Context`](crate::Context) in which /// it was called, and add virtual cells sequentially to buckets labelled by id. /// The virtual cells will be assigned to physical cells sequentially by id. /// We use a `BTreeMap` for the buckets instead of sorting to cells, to ensure that the order of the cells /// within a bucket is deterministic. -/// The assumption is that the [Context] is thread-local. +/// The assumption is that the [`Context`](crate::Context) is thread-local. /// /// Cheap to clone across threads because everything is in [Arc]. #[derive(Clone, Debug, Getters, CopyGetters, Setters)] @@ -122,6 +125,7 @@ impl VirtualRegionManager type Config = Vec<[Column; ADVICE_COLS]>; fn assign_raw(&self, config: &Self::Config, region: &mut Region) { + let copy_manager = (!self.witness_gen_only).then(|| self.copy_manager().lock().unwrap()); let cells_to_lookup = self.cells_to_lookup.lock().unwrap(); // Copy the cells to the config columns, going left to right, then top to bottom. // Will panic if out of rows @@ -135,12 +139,8 @@ impl VirtualRegionManager for (advice, &column) in advices.iter().zip(config[lookup_col].iter()) { let bcell = raw_assign_advice(region, column, lookup_offset, Value::known(advice.value)); - if !self.witness_gen_only { - let ctx_cell = advice.cell.unwrap(); - let copy_manager = self.copy_manager.lock().unwrap(); - let acell = - copy_manager.assigned_advices.get(&ctx_cell).expect("cell not assigned"); - region.constrain_equal(*acell, bcell.cell()); + if let Some(copy_manager) = copy_manager.as_ref() { + constrain_virtual_equals_external(region, *advice, bcell.cell(), copy_manager); } } diff --git a/halo2-base/src/virtual_region/lookups/basic.rs b/halo2-base/src/virtual_region/lookups/basic.rs new file mode 100644 index 00000000..3b214545 --- /dev/null +++ b/halo2-base/src/virtual_region/lookups/basic.rs @@ -0,0 +1,204 @@ +use std::iter::zip; + +use crate::{ + halo2_proofs::{ + circuit::{Layouter, Region, Value}, + halo2curves::ff::Field, + plonk::{Advice, Column, ConstraintSystem, Fixed, Phase}, + poly::Rotation, + }, + utils::{ + halo2::{ + assign_virtual_to_raw, constrain_virtual_equals_external, raw_assign_advice, + raw_assign_fixed, + }, + ScalarField, + }, + virtual_region::copy_constraints::SharedCopyConstraintManager, + AssignedValue, +}; + +/// A simple dynamic lookup table for when you want to verify some length `KEY_COL` key +/// is in a provided (dynamic) table of the same format. +/// +/// Note that you can also use this to look up (key, out) pairs, where you consider the whole +/// pair as the new key. +/// +/// We can have multiple sets of dedicated columns to be looked up: these can be specified +/// when calling `new`, but typically we just need 1 set. +/// +/// The `table` consists of advice columns. Since this table may have poisoned rows (blinding factors), +/// we use a fixed column `table_selector` which is default 0 and only 1 on enabled rows of the table. +/// The dynamic lookup will check that for `(key, key_is_enabled)` in `to_lookup` we have `key` matches one of +/// the rows in `table` where `table_selector == key_is_enabled`. +/// Reminder: the Halo2 lookup argument will ignore the poisoned rows in `to_lookup` +/// (see [https://zcash.github.io/halo2/design/proving-system/lookup.html#zero-knowledge-adjustment]), but it will +/// not ignore the poisoned rows in `table`. +/// +/// Part of this design consideration is to allow a key of `[F::ZERO; KEY_COL]` to still be used as a valid key +/// in the lookup argument. By default, unfilled rows in `to_lookup` will be all zeros; we require +/// at least one row in `table` where `table_is_enabled = 0` and the rest of the row in `table` are also 0s. +#[derive(Clone, Debug)] +pub struct BasicDynLookupConfig { + /// Columns for cells to be looked up. Consists of `(key, key_is_enabled)`. + pub to_lookup: Vec<([Column; KEY_COL], Column)>, + /// Table to look up against. + pub table: [Column; KEY_COL], + /// Selector to enable a row in `table` to actually be part of the lookup table. This is to prevent + /// blinding factors in `table` advice columns from being used in the lookup. + pub table_is_enabled: Column, +} + +impl BasicDynLookupConfig { + /// Assumes all columns are in the same phase `P` to make life easier. + /// We enable equality on all columns because we envision both the columns to lookup + /// and the table will need to talk to halo2-lib. + pub fn new( + meta: &mut ConstraintSystem, + phase: impl Fn() -> P, + num_lu_sets: usize, + ) -> Self { + let mut make_columns = || { + let advices = [(); KEY_COL].map(|_| { + let advice = meta.advice_column_in(phase()); + meta.enable_equality(advice); + advice + }); + let is_enabled = meta.fixed_column(); + (advices, is_enabled) + }; + let (table, table_is_enabled) = make_columns(); + let to_lookup: Vec<_> = (0..num_lu_sets).map(|_| make_columns()).collect(); + + for (key, key_is_enabled) in &to_lookup { + meta.lookup_any("dynamic lookup table", |meta| { + let table = table.map(|c| meta.query_advice(c, Rotation::cur())); + let table_is_enabled = meta.query_fixed(table_is_enabled, Rotation::cur()); + let key = key.map(|c| meta.query_advice(c, Rotation::cur())); + let key_is_enabled = meta.query_fixed(*key_is_enabled, Rotation::cur()); + zip(key, table).chain([(key_is_enabled, table_is_enabled)]).collect() + }); + } + + Self { table_is_enabled, table, to_lookup } + } + + /// Assign managed lookups + /// + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_to_lookup_to_raw( + &self, + mut layouter: impl Layouter, + keys: impl IntoIterator; KEY_COL]>, + copy_manager: Option<&SharedCopyConstraintManager>, + ) { + #[cfg(not(feature = "halo2-axiom"))] + let keys = keys.into_iter().collect::>(); + layouter + .assign_region( + || "[BasicDynLookupConfig] Advice cells to lookup", + |mut region| { + self.assign_virtual_to_lookup_to_raw_from_offset( + &mut region, + #[cfg(feature = "halo2-axiom")] + keys, + #[cfg(not(feature = "halo2-axiom"))] + keys.clone(), + 0, + copy_manager, + ); + Ok(()) + }, + ) + .unwrap(); + } + + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_to_lookup_to_raw_from_offset( + &self, + region: &mut Region, + keys: impl IntoIterator; KEY_COL]>, + mut offset: usize, + copy_manager: Option<&SharedCopyConstraintManager>, + ) { + let copy_manager = copy_manager.map(|c| c.lock().unwrap()); + // Copied from `LookupAnyManager::assign_raw` but modified to set `key_is_enabled` to 1. + // Copy the cells to the config columns, going left to right, then top to bottom. + // Will panic if out of rows + let mut lookup_col = 0; + for key in keys { + if lookup_col >= self.to_lookup.len() { + lookup_col = 0; + offset += 1; + } + let (key_col, key_is_enabled_col) = self.to_lookup[lookup_col]; + // set key_is_enabled to 1 + raw_assign_fixed(region, key_is_enabled_col, offset, F::ONE); + for (advice, column) in zip(key, key_col) { + let bcell = raw_assign_advice(region, column, offset, Value::known(advice.value)); + if let Some(copy_manager) = copy_manager.as_ref() { + constrain_virtual_equals_external(region, advice, bcell.cell(), copy_manager); + } + } + + lookup_col += 1; + } + } + + /// Assign virtual table to raw. + /// + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_table_to_raw( + &self, + mut layouter: impl Layouter, + rows: impl IntoIterator; KEY_COL]>, + copy_manager: Option<&SharedCopyConstraintManager>, + ) { + #[cfg(not(feature = "halo2-axiom"))] + let rows = rows.into_iter().collect::>(); + layouter + .assign_region( + || "[BasicDynLookupConfig] Dynamic Lookup Table", + |mut region| { + self.assign_virtual_table_to_raw_from_offset( + &mut region, + #[cfg(feature = "halo2-axiom")] + rows, + #[cfg(not(feature = "halo2-axiom"))] + rows.clone(), + 0, + copy_manager, + ); + Ok(()) + }, + ) + .unwrap(); + } + + /// `copy_manager` **must** be provided unless you are only doing witness generation + /// without constraints. + pub fn assign_virtual_table_to_raw_from_offset( + &self, + region: &mut Region, + rows: impl IntoIterator; KEY_COL]>, + mut offset: usize, + copy_manager: Option<&SharedCopyConstraintManager>, + ) { + for row in rows { + // Enable this row in the table + raw_assign_fixed(region, self.table_is_enabled, offset, F::ONE); + for (col, virtual_cell) in self.table.into_iter().zip(row) { + assign_virtual_to_raw(region, col, offset, virtual_cell, copy_manager); + } + offset += 1; + } + // always assign one disabled row with all 0s, so disabled to_lookup works for sure + raw_assign_fixed(region, self.table_is_enabled, offset, F::ZERO); + for col in self.table { + raw_assign_advice(region, col, offset, Value::known(F::ZERO)); + } + } +} diff --git a/halo2-base/src/virtual_region/tests/lookups/memory.rs b/halo2-base/src/virtual_region/tests/lookups/memory.rs index 66df4085..6117b80c 100644 --- a/halo2-base/src/virtual_region/tests/lookups/memory.rs +++ b/halo2-base/src/virtual_region/tests/lookups/memory.rs @@ -1,11 +1,15 @@ -use crate::halo2_proofs::{ - arithmetic::Field, - circuit::{Layouter, SimpleFloorPlanner, Value}, - dev::MockProver, - halo2curves::bn256::Fr, - plonk::{keygen_pk, keygen_vk, Advice, Circuit, Column, ConstraintSystem, Error}, - poly::Rotation, +use crate::{ + halo2_proofs::{ + arithmetic::Field, + circuit::{Layouter, SimpleFloorPlanner}, + dev::MockProver, + halo2curves::bn256::Fr, + plonk::{keygen_pk, keygen_vk, Assigned, Circuit, ConstraintSystem, Error}, + }, + virtual_region::lookups::basic::BasicDynLookupConfig, + AssignedValue, ContextCell, }; +use halo2_proofs_axiom::plonk::FirstPhase; use rand::{rngs::StdRng, Rng, SeedableRng}; use test_log::test; @@ -16,25 +20,22 @@ use crate::{ }, utils::{ fs::gen_srs, - halo2::raw_assign_advice, testing::{check_proof, gen_proof}, ScalarField, }, - virtual_region::{lookups::LookupAnyManager, manager::VirtualRegionManager}, + virtual_region::manager::VirtualRegionManager, }; #[derive(Clone, Debug)] struct RAMConfig { cpu: FlexGateConfig, - copy: Vec<[Column; 2]>, - // dynamic lookup table - memory: [Column; 2], + memory: BasicDynLookupConfig<2>, } #[derive(Clone, Default)] struct RAMConfigParams { cpu: FlexGateConfigParams, - copy_columns: usize, + num_lu_sets: usize, } struct RAMCircuit { @@ -44,7 +45,7 @@ struct RAMCircuit { ptrs: [usize; CYCLES], cpu: SinglePhaseCoreManager, - ram: LookupAnyManager, + mem_access: Vec<[AssignedValue; 2]>, params: RAMConfigParams, } @@ -57,8 +58,8 @@ impl RAMCircuit { witness_gen_only: bool, ) -> Self { let cpu = SinglePhaseCoreManager::new(witness_gen_only, Default::default()); - let ram = LookupAnyManager::new(witness_gen_only, cpu.copy_manager.clone()); - Self { memory, ptrs, cpu, ram, params } + let mem_access = vec![]; + Self { memory, ptrs, cpu, mem_access, params } } fn compute(&mut self) { @@ -67,9 +68,9 @@ impl RAMCircuit { let mut sum = ctx.load_constant(F::ZERO); for &ptr in &self.ptrs { let value = self.memory[ptr]; - let ptr = ctx.load_witness(F::from(ptr as u64 + 1)); + let ptr = ctx.load_witness(F::from(ptr as u64)); let value = ctx.load_witness(value); - self.ram.add_lookup((ctx.type_id(), ctx.id()), [ptr, value]); + self.mem_access.push([ptr, value]); sum = gate.add(ctx, sum, value); } } @@ -89,30 +90,12 @@ impl Circuit for RAMCircuit { } fn configure_with_params(meta: &mut ConstraintSystem, params: Self::Params) -> Self::Config { - let k = params.cpu.k; - let mut cpu = FlexGateConfig::configure(meta, params.cpu); - let copy: Vec<_> = (0..params.copy_columns) - .map(|_| { - [(); 2].map(|_| { - let advice = meta.advice_column(); - meta.enable_equality(advice); - advice - }) - }) - .collect(); - let mem = [meta.advice_column(), meta.advice_column()]; - - for copy in © { - meta.lookup_any("dynamic memory lookup table", |meta| { - let mem = mem.map(|c| meta.query_advice(c, Rotation::cur())); - let copy = copy.map(|c| meta.query_advice(c, Rotation::cur())); - vec![(copy[0].clone(), mem[0].clone()), (copy[1].clone(), mem[1].clone())] - }); - } + let memory = BasicDynLookupConfig::new(meta, || FirstPhase, params.num_lu_sets); + let cpu = FlexGateConfig::configure(meta, params.cpu); + log::info!("Poisoned rows: {}", meta.minimum_rows()); - cpu.max_rows = (1 << k) - meta.minimum_rows(); - RAMConfig { cpu, copy, memory: mem } + RAMConfig { cpu, memory } } fn configure(_: &mut ConstraintSystem) -> Self::Config { @@ -124,21 +107,43 @@ impl Circuit for RAMCircuit { config: Self::Config, mut layouter: impl Layouter, ) -> Result<(), Error> { + // Make purely virtual cells so we can raw assign them + let memory = self.memory.iter().enumerate().map(|(i, value)| { + let idx = Assigned::Trivial(F::from(i as u64)); + let idx = + AssignedValue { value: idx, cell: Some(ContextCell::new("RAM Config", 0, i)) }; + let value = Assigned::Trivial(*value); + let value = AssignedValue { value, cell: Some(ContextCell::new("RAM Config", 1, i)) }; + [idx, value] + }); + + let copy_manager = (!self.cpu.witness_gen_only()).then_some(&self.cpu.copy_manager); + + config.memory.assign_virtual_table_to_raw( + layouter.namespace(|| "memory"), + memory, + copy_manager, + ); + layouter.assign_region( - || "RAM Circuit", + || "cpu", |mut region| { - // Raw assign the private memory inputs - for (i, &value) in self.memory.iter().enumerate() { - // I think there will always be (0, 0) in the table so we index starting from 1 - let idx = Value::known(F::from(i as u64 + 1)); - raw_assign_advice(&mut region, config.memory[0], i, idx); - raw_assign_advice(&mut region, config.memory[1], i, Value::known(value)); - } self.cpu.assign_raw( &(config.cpu.basic_gates[0].clone(), config.cpu.max_rows), &mut region, ); - self.ram.assign_raw(&config.copy, &mut region); + Ok(()) + }, + )?; + config.memory.assign_virtual_to_lookup_to_raw( + layouter.namespace(|| "memory accesses"), + self.mem_access.clone(), + copy_manager, + ); + // copy constraints at the very end for safety: + layouter.assign_region( + || "copy constraints", + |mut region| { self.cpu.copy_manager.assign_raw(&config.cpu.constants, &mut region); Ok(()) }, @@ -155,7 +160,6 @@ fn test_ram_mock() { let memory: Vec<_> = (0..mem_len).map(|_| Fr::random(&mut rng)).collect(); let ptrs = [(); CYCLES].map(|_| rng.gen_range(0..memory.len())); let usable_rows = 2usize.pow(k) - 11; // guess - let copy_columns = CYCLES / usable_rows + 1; let params = RAMConfigParams::default(); let mut circuit = RAMCircuit::new(memory, ptrs, params, false); circuit.compute(); @@ -166,10 +170,43 @@ fn test_ram_mock() { num_advice_per_phase: vec![num_advice], num_fixed: 1, }; - circuit.params.copy_columns = copy_columns; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; MockProver::run(k, &circuit, vec![]).unwrap().assert_satisfied(); } +#[test] +#[should_panic = "called `Result::unwrap()` on an `Err` value: [Lookup dynamic lookup table(index: 2) is not satisfied in Region 2 ('[BasicDynLookupConfig] Advice cells to lookup') at offset 16]"] +fn test_ram_mock_failed_access() { + let k = 5u32; + const CYCLES: usize = 50; + let mut rng = StdRng::seed_from_u64(0); + let mem_len = 16usize; + let memory: Vec<_> = (0..mem_len).map(|_| Fr::random(&mut rng)).collect(); + let ptrs = [(); CYCLES].map(|_| rng.gen_range(0..memory.len())); + let usable_rows = 2usize.pow(k) - 11; // guess + let params = RAMConfigParams::default(); + let mut circuit = RAMCircuit::new(memory, ptrs, params, false); + circuit.compute(); + + // === PRANK === + // Try to claim memory[0] = 0 + let ctx = circuit.cpu.main(); + let ptr = ctx.load_witness(Fr::ZERO); + let value = ctx.load_witness(Fr::ZERO); + circuit.mem_access.push([ptr, value]); + // === end prank === + + // auto-configuration stuff + let num_advice = circuit.cpu.total_advice() / usable_rows + 1; + circuit.params.cpu = FlexGateConfigParams { + k: k as usize, + num_advice_per_phase: vec![num_advice], + num_fixed: 1, + }; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; + MockProver::run(k, &circuit, vec![]).unwrap().verify().unwrap(); +} + #[test] fn test_ram_prover() { let k = 10u32; @@ -182,7 +219,6 @@ fn test_ram_prover() { let ptrs = [0; CYCLES]; let usable_rows = 2usize.pow(k) - 11; // guess - let copy_columns = CYCLES / usable_rows + 1; let params = RAMConfigParams::default(); let mut circuit = RAMCircuit::new(memory, ptrs, params, false); circuit.compute(); @@ -192,7 +228,7 @@ fn test_ram_prover() { num_advice_per_phase: vec![num_advice], num_fixed: 1, }; - circuit.params.copy_columns = copy_columns; + circuit.params.num_lu_sets = CYCLES / usable_rows + 1; let params = gen_srs(k); let vk = keygen_vk(¶ms, &circuit).unwrap(); diff --git a/halo2-ecc/Cargo.toml b/halo2-ecc/Cargo.toml index d3da45fc..5177476e 100644 --- a/halo2-ecc/Cargo.toml +++ b/halo2-ecc/Cargo.toml @@ -1,7 +1,7 @@ [package] -name="halo2-ecc" -version="0.4.0" -edition="2021" +name = "halo2-ecc" +version = "0.4.0" +edition = "2021" [dependencies] itertools="0.10" @@ -16,27 +16,29 @@ serde_json="1.0" rayon="1.6.1" test-case="3.1.0" -halo2-base={ path="../halo2-base", default-features=false } +halo2-base = { path = "../halo2-base", default-features = false } + +# plotting circuit layout +plotters = { version = "0.3.0", optional = true } [dev-dependencies] -ark-std={ version="0.3.0", features=["print-trace"] } -pprof={ version="0.11", features=["criterion", "flamegraph"] } -criterion="0.4" -criterion-macro="0.4" -halo2-base={ path="../halo2-base", default-features=false, features=["test-utils"] } -test-log="0.2.12" -env_logger="0.10.0" -pairing="0.23.0" +ark-std = { version = "0.3.0", features = ["print-trace"] } +pprof = { version = "0.13", features = ["criterion", "flamegraph"] } +criterion = "0.5.1" +criterion-macro = "0.4" +halo2-base = { path = "../halo2-base", default-features = false, features = ["test-utils"] } +test-log = "0.2.12" +env_logger = "0.10.0" [features] -default=["jemallocator", "halo2-axiom", "display"] -dev-graph=["halo2-base/dev-graph"] -display=["halo2-base/display"] -asm=["halo2-base/asm"] -halo2-pse=["halo2-base/halo2-pse"] -halo2-axiom=["halo2-base/halo2-axiom"] -jemallocator=["halo2-base/jemallocator"] -mimalloc=["halo2-base/mimalloc"] +default = ["jemallocator", "halo2-axiom", "display"] +dev-graph = ["halo2-base/dev-graph", "plotters"] +display = ["halo2-base/display"] +asm = ["halo2-base/asm"] +halo2-pse = ["halo2-base/halo2-pse"] +halo2-axiom = ["halo2-base/halo2-axiom"] +jemallocator = ["halo2-base/jemallocator"] +mimalloc = ["halo2-base/mimalloc"] [[bench]] name="fp_mul" @@ -47,5 +49,5 @@ name="msm" harness=false [[bench]] -name="fixed_base_msm" -harness=false +name = "fixed_base_msm" +harness = false diff --git a/halo2-ecc/src/bigint/big_is_zero.rs b/halo2-ecc/src/bigint/big_is_zero.rs index aa67c842..df4be33f 100644 --- a/halo2-ecc/src/bigint/big_is_zero.rs +++ b/halo2-ecc/src/bigint/big_is_zero.rs @@ -18,7 +18,7 @@ pub fn positive( gate.is_zero(ctx, sum) } -/// Given ProperUint `a`, returns 1 iff every limb of `a` is zero. Returns 0 otherwise. +/// Given `ProperUint` `a`, returns 1 iff every limb of `a` is zero. Returns 0 otherwise. /// /// It is almost always more efficient to use [`positive`] instead. /// diff --git a/halo2-ecc/src/bn254/tests/bls_signature.rs b/halo2-ecc/src/bn254/tests/bls_signature.rs index 8475f677..adacce89 100644 --- a/halo2-ecc/src/bn254/tests/bls_signature.rs +++ b/halo2-ecc/src/bn254/tests/bls_signature.rs @@ -4,6 +4,7 @@ use std::{ }; use super::*; +use crate::halo2curves::pairing::{group::ff::Field, MillerLoopResult}; use crate::{ bn254::bls_signature::BlsSignatureChip, fields::FpStrategy, halo2_proofs::halo2curves::bn256::G2Affine, @@ -14,8 +15,6 @@ use halo2_base::{ utils::BigPrimeField, Context, }; -extern crate pairing; -use pairing::{group::ff::Field, MillerLoopResult}; use rand_core::OsRng; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] diff --git a/halo2-ecc/src/bn254/tests/pairing.rs b/halo2-ecc/src/bn254/tests/pairing.rs index 6b192ada..55291bfa 100644 --- a/halo2-ecc/src/bn254/tests/pairing.rs +++ b/halo2-ecc/src/bn254/tests/pairing.rs @@ -6,9 +6,7 @@ use std::{ use super::*; use crate::fields::FieldChip; use crate::{fields::FpStrategy, halo2_proofs::halo2curves::bn256::G2Affine}; -use halo2_base::{ - gates::RangeChip, halo2_proofs::arithmetic::Field, utils::BigPrimeField, Context, -}; +use halo2_base::{gates::RangeChip, utils::BigPrimeField, Context}; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] struct PairingCircuitParams { @@ -59,70 +57,6 @@ fn test_pairing() { }); } -fn pairing_check_test( - ctx: &mut Context, - range: &RangeChip, - params: PairingCircuitParams, - P: G1Affine, - Q: G2Affine, - S: G1Affine, -) { - let fp_chip = FpChip::::new(range, params.limb_bits, params.num_limbs); - let chip = PairingChip::new(&fp_chip); - let P_assigned = chip.load_private_g1(ctx, P); - let Q_assigned = chip.load_private_g2(ctx, Q); - let S_assigned = chip.load_private_g1(ctx, S); - let T_assigned = chip.load_private_g2(ctx, G2Affine::generator()); - chip.pairing_check(ctx, &Q_assigned, &P_assigned, &T_assigned, &S_assigned); -} - -/* - * Samples a random α,β in Fr and does the pairing check - * e(H_1^α, H_2^β) = e(H_1^(α*β), H_2), where H_1 is the generator for G1 and - * H_2 for G2. - */ -#[test] -fn test_pairing_check() { - let path = "configs/bn254/pairing_circuit.config"; - let params: PairingCircuitParams = serde_json::from_reader( - File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), - ) - .unwrap(); - let mut rng = StdRng::seed_from_u64(0); - let alpha = Fr::random(&mut rng); - let beta = Fr::random(&mut rng); - let P = G1Affine::from(G1Affine::generator() * alpha); - let Q = G2Affine::from(G2Affine::generator() * beta); - let S = G1Affine::from(G1Affine::generator() * alpha * beta); - base_test().k(params.degree).lookup_bits(params.lookup_bits).run(|ctx, range| { - pairing_check_test(ctx, range, params, P, Q, S); - }) -} - -/* - * Samples a random α,β in Fr and does an incorrect pairing check - * e(H_1^α, H_2^β) = e(H_1^α, H_2), where H_1 is the generator for G1 and - * H_2 for G2. - */ -#[test] -fn test_pairing_check_fail() { - let path = "configs/bn254/pairing_circuit.config"; - let params: PairingCircuitParams = serde_json::from_reader( - File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")), - ) - .unwrap(); - let mut rng = StdRng::seed_from_u64(0); - let alpha = Fr::random(&mut rng); - let beta = Fr::random(&mut rng); - let P = G1Affine::from(G1Affine::generator() * alpha); - let Q = G2Affine::from(G2Affine::generator() * beta); - base_test().k(params.degree).lookup_bits(params.lookup_bits).expect_satisfied(false).run( - |ctx, range| { - pairing_check_test(ctx, range, params, P, Q, P); - }, - ) -} - #[test] fn bench_pairing() -> Result<(), Box> { let config_path = "configs/bn254/bench_pairing.config"; diff --git a/halo2-ecc/src/fields/fp.rs b/halo2-ecc/src/fields/fp.rs index 579ac39a..5d0e0faa 100644 --- a/halo2-ecc/src/fields/fp.rs +++ b/halo2-ecc/src/fields/fp.rs @@ -337,17 +337,17 @@ impl<'range, F: BigPrimeField, Fp: BigPrimeField> FieldChip for FpChip<'range fn range_check( &self, ctx: &mut Context, - a: impl Into>, + a: impl Into>, max_bits: usize, // the maximum bits that a.value could take ) { let n = self.limb_bits; let a = a.into(); let mut remaining_bits = max_bits; - debug_assert!(a.value.bits() as usize <= max_bits); + debug_assert!(a.0.value.bits() as usize <= max_bits); // range check limbs of `a` are in [0, 2^n) except last limb should be in [0, 2^last_limb_bits) - for cell in a.truncation.limbs { + for cell in a.0.truncation.limbs { let limb_bits = cmp::min(n, remaining_bits); remaining_bits -= limb_bits; self.range.range_check(ctx, cell, limb_bits); diff --git a/halo2-ecc/src/fields/mod.rs b/halo2-ecc/src/fields/mod.rs index 10e1ae6f..469397df 100644 --- a/halo2-ecc/src/fields/mod.rs +++ b/halo2-ecc/src/fields/mod.rs @@ -126,12 +126,7 @@ pub trait FieldChip: Clone + Send + Sync { fn carry_mod(&self, ctx: &mut Context, a: Self::UnsafeFieldPoint) -> Self::FieldPoint; - fn range_check( - &self, - ctx: &mut Context, - a: impl Into, - max_bits: usize, - ); + fn range_check(&self, ctx: &mut Context, a: impl Into, max_bits: usize); /// Constrains that `a` is a reduced representation and returns the wrapped `a`. fn enforce_less_than( diff --git a/halo2-ecc/src/fields/tests/fp/mod.rs b/halo2-ecc/src/fields/tests/fp/mod.rs index d88d6a1a..b87de4bf 100644 --- a/halo2-ecc/src/fields/tests/fp/mod.rs +++ b/halo2-ecc/src/fields/tests/fp/mod.rs @@ -62,6 +62,8 @@ fn test_range_check() { #[cfg(feature = "dev-graph")] #[test] fn plot_fp() { + use halo2_base::gates::circuit::builder::BaseCircuitBuilder; + use halo2_base::halo2_proofs; use plotters::prelude::*; let root = BitMapBackend::new("layout.png", (1024, 1024)).into_drawing_area(); @@ -72,10 +74,14 @@ fn plot_fp() { let a = Fq::zero(); let b = Fq::zero(); - let mut builder = GateThreadBuilder::keygen(); - fp_mul_test(builder.main(0), k - 1, 88, 3, a, b); + let mut builder = BaseCircuitBuilder::new(false).use_k(k).use_lookup_bits(k - 1); + let range = builder.range_chip(); + let chip = FpChip::::new(&range, 88, 3); + let ctx = builder.main(0); + let [a, b] = [a, b].map(|x| chip.load_private(ctx, x)); + let c = chip.mul(ctx, a, b); - let config_params = builder.config(k, Some(10), Some(k - 1)); - let circuit = RangeCircuitBuilder::keygen(builder, config_params); - halo2_proofs::dev::CircuitLayout::default().render(k as u32, &circuit, &root).unwrap(); + let cp = builder.calculate_params(Some(10)); + dbg!(cp); + halo2_proofs::dev::CircuitLayout::default().render(k as u32, &builder, &root).unwrap(); } diff --git a/halo2-ecc/src/fields/vector.rs b/halo2-ecc/src/fields/vector.rs index d27dc25f..f007c3bf 100644 --- a/halo2-ecc/src/fields/vector.rs +++ b/halo2-ecc/src/fields/vector.rs @@ -245,13 +245,16 @@ 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, a: impl IntoIterator, max_bits: usize, ) where - A: Into, + A: Into, { for coeff in a { self.fp_chip.range_check(ctx, coeff, max_bits); @@ -432,10 +435,13 @@ 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, - a: impl Into, + a: impl Into, max_bits: usize, ) { self.0.range_check(ctx, a.into(), max_bits) 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}, diff --git a/halo2-ecc/src/secp256k1/tests/mod.rs b/halo2-ecc/src/secp256k1/tests/mod.rs index b83720b1..e12afc1c 100644 --- a/halo2-ecc/src/secp256k1/tests/mod.rs +++ b/halo2-ecc/src/secp256k1/tests/mod.rs @@ -22,11 +22,9 @@ use crate::{ pub mod ecdsa; pub mod ecdsa_tests; -pub mod schnorr_signature; -pub mod schnorr_signature_tests; #[derive(Clone, Copy, Debug, Serialize, Deserialize)] -pub struct CircuitParams { +struct CircuitParams { strategy: FpStrategy, degree: u32, num_advice: usize, diff --git a/hashes/zkevm/Cargo.toml b/hashes/zkevm/Cargo.toml index 28703f24..169bf018 100644 --- a/hashes/zkevm/Cargo.toml +++ b/hashes/zkevm/Cargo.toml @@ -12,18 +12,15 @@ itertools = "0.11" lazy_static = "1.4" log = "0.4" num-bigint = { version = "0.4" } -halo2-base = { path = "../../halo2-base", default-features = false, features = [ - "test-utils", -] } -rayon = "1.7" +halo2-base = { path = "../../halo2-base", default-features = false, features = ["test-utils"] } +serde = { version = "1.0", features = ["derive"] } +rayon = "1.8" sha3 = "0.10.8" -# always included but without features to use Native poseidon -snark-verifier = { git = "https://github.com/axiom-crypto/snark-verifier.git", branch = "develop", default-features = false } +# always included but without features to use Native poseidon and get CircuitExt trait +snark-verifier-sdk = { git = "https://github.com/axiom-crypto/snark-verifier.git", branch = "release-0.1.7-rc", default-features = false } getset = "0.1.2" [dev-dependencies] -criterion = "0.3" -ctor = "0.1.22" ethers-signers = "2.0.8" hex = "0.4.3" itertools = "0.11" @@ -35,9 +32,9 @@ test-case = "3.1.0" [features] default = ["halo2-axiom", "display"] -display = ["halo2-base/display", "snark-verifier/display"] -halo2-pse = ["halo2-base/halo2-pse", "snark-verifier/halo2-pse"] -halo2-axiom = ["halo2-base/halo2-axiom", "snark-verifier/halo2-axiom"] +display = ["snark-verifier-sdk/display"] +halo2-pse = ["halo2-base/halo2-pse"] +halo2-axiom = ["halo2-base/halo2-axiom"] jemallocator = ["halo2-base/jemallocator"] mimalloc = ["halo2-base/mimalloc"] asm = ["halo2-base/asm"] diff --git a/hashes/zkevm/src/keccak/component/circuit/shard.rs b/hashes/zkevm/src/keccak/component/circuit/shard.rs index e77496d2..469cee39 100644 --- a/hashes/zkevm/src/keccak/component/circuit/shard.rs +++ b/hashes/zkevm/src/keccak/component/circuit/shard.rs @@ -7,7 +7,10 @@ use crate::{ get_words_to_witness_multipliers, num_poseidon_absorb_per_keccak_f, num_word_per_witness, }, - output::{dummy_circuit_output, KeccakCircuitOutput}, + output::{ + calculate_circuit_outputs_commit, dummy_circuit_output, + multi_inputs_to_circuit_outputs, KeccakCircuitOutput, + }, param::*, }, vanilla::{ @@ -17,7 +20,7 @@ use crate::{ }, util::eth_types::Field, }; -use getset::{CopyGetters, Getters}; +use getset::{CopyGetters, Getters, MutGetters}; use halo2_base::{ gates::{ circuit::{builder::BaseCircuitBuilder, BaseCircuitParams, BaseConfig}, @@ -33,27 +36,35 @@ use halo2_base::{ PoseidonHasher, }, safe_types::{SafeBool, SafeTypeChip}, + virtual_region::copy_constraints::SharedCopyConstraintManager, AssignedValue, Context, QuantumCell::Constant, }; use itertools::Itertools; +use serde::{Deserialize, Serialize}; +use snark_verifier_sdk::CircuitExt; /// Keccak Component Shard Circuit -#[derive(Getters)] +#[derive(Getters, MutGetters)] pub struct KeccakComponentShardCircuit { + /// The multiple inputs to be hashed. + #[getset(get = "pub")] inputs: Vec>, /// Parameters of this circuit. The same parameters always construct the same circuit. - #[getset(get = "pub")] + #[getset(get_mut = "pub")] params: KeccakComponentShardCircuitParams, - base_circuit_builder: RefCell>, + /// Poseidon hasher. Stateless once initialized. + #[getset(get = "pub")] hasher: RefCell>, + /// Stateless gate chip + #[getset(get = "pub")] gate_chip: GateChip, } /// Parameters of KeccakComponentCircuit. -#[derive(Default, Clone, CopyGetters)] +#[derive(Default, Clone, CopyGetters, Serialize, Deserialize)] pub struct KeccakComponentShardCircuitParams { /// This circuit has 2^k rows. #[getset(get_copy = "pub")] @@ -61,8 +72,8 @@ pub struct KeccakComponentShardCircuitParams { // Number of unusable rows withhold by Halo2. #[getset(get_copy = "pub")] num_unusable_row: usize, - /// Max keccak_f this circuits can aceept. The circuit can at most process of inputs - /// with < NUM_BYTES_TO_ABSORB bytes or an input with * NUM_BYTES_TO_ABSORB - 1 bytes. + /// Max keccak_f this circuits can aceept. The circuit can at most process `capacity` of inputs + /// with < NUM_BYTES_TO_ABSORB bytes or an input with `capacity * NUM_BYTES_TO_ABSORB - 1` bytes. #[getset(get_copy = "pub")] capacity: usize, // If true, publish raw outputs. Otherwise, publish Poseidon commitment of raw outputs. @@ -84,7 +95,7 @@ impl KeccakComponentShardCircuitParams { ) -> Self { assert!(1 << k > num_unusable_row, "Number of unusable rows must be less than 2^k"); let max_rows = (1 << k) - num_unusable_row; - // Derived from [crate::keccak::native_circuit::keccak_packed_multi::get_keccak_capacity]. + // Derived from [crate::keccak::vanilla::keccak_packed_multi::get_keccak_capacity]. let rows_per_round = max_rows / (capacity * (NUM_ROUNDS + 1) + 1 + NUM_WORDS_TO_ABSORB); assert!(rows_per_round > 0, "No enough rows for the speficied capacity"); let keccak_circuit_params = KeccakConfigParams { k: k as u32, rows_per_round }; @@ -125,12 +136,12 @@ impl Circuit for KeccakComponentShardCircuit { self.params.clone() } - /// Creates a new instance of the [KeccakCoprocessorLeafCircuit] without witnesses by setting the witness_gen_only flag to false + /// Creates a new instance of the [KeccakComponentShardCircuit] without witnesses by setting the witness_gen_only flag to false fn without_witnesses(&self) -> Self { unimplemented!() } - /// Configures a new circuit using [`BaseConfigParams`] + /// Configures a new circuit using [`BaseCircuitParams`] fn configure_with_params(meta: &mut ConstraintSystem, params: Self::Params) -> Self::Config { let keccak_circuit_config = KeccakCircuitConfig::new(meta, params.keccak_circuit_params); let base_circuit_params = params.base_circuit_params; @@ -291,31 +302,11 @@ impl KeccakComponentShardCircuit { ) -> Vec> { let rows_per_round = self.params.keccak_circuit_params.rows_per_round; let base_circuit_builder = self.base_circuit_builder.borrow(); - let mut copy_manager = base_circuit_builder.core().copy_manager.lock().unwrap(); - assigned_rows - .into_iter() - .step_by(rows_per_round) - // Skip the first round which is dummy. - .skip(1) - .chunks(NUM_ROUNDS + 1) - .into_iter() - .map(|rounds| { - let mut rounds = rounds.collect_vec(); - assert_eq!(rounds.len(), NUM_ROUNDS + 1); - let bytes_left = copy_manager.load_external_assigned(rounds[0].bytes_left.clone()); - let output_row = rounds.pop().unwrap(); - let word_values = core::array::from_fn(|i| { - let assigned_row = &rounds[i]; - copy_manager.load_external_assigned(assigned_row.word_value.clone()) - }); - let is_final = SafeTypeChip::unsafe_to_bool( - copy_manager.load_external_assigned(output_row.is_final), - ); - let hash_lo = copy_manager.load_external_assigned(output_row.hash_lo); - let hash_hi = copy_manager.load_external_assigned(output_row.hash_hi); - LoadedKeccakF { bytes_left, word_values, is_final, hash_lo, hash_hi } - }) - .collect() + transmute_keccak_assigned_to_virtual( + &base_circuit_builder.core().copy_manager, + assigned_rows, + rows_per_round, + ) } /// Generate witnesses of the base circuit. @@ -362,7 +353,7 @@ impl KeccakComponentShardCircuit { lookup_key_per_keccak_f.iter().zip_eq(loaded_keccak_fs) { let is_final = AssignedValue::from(loaded_keccak_f.is_final); - let key = gate.select(ctx, *compact_output.hash(), dummy_key_witness, is_final); + let key = gate.select(ctx, compact_output.hash(), dummy_key_witness, is_final); let hash_lo = gate.select(ctx, loaded_keccak_f.hash_lo, dummy_keccak_lo_witness, is_final); let hash_hi = @@ -381,7 +372,7 @@ impl KeccakComponentShardCircuit { let mut base_circuit_builder_mut = self.base_circuit_builder.borrow_mut(); let ctx = base_circuit_builder_mut.main(0); - // TODO: wrap this into a function which should be shared with App circuits. + // TODO: wrap this into a function which should be shared wiht App circuits. let output_commitment = self.hasher.borrow().hash_fix_len_array( ctx, gate, @@ -421,15 +412,15 @@ pub(crate) fn create_hasher() -> PoseidonHasher::new(spec) } -/// Encode raw inputs from Keccak circuit witnesses into lookup keys. +/// Packs raw inputs from Keccak circuit witnesses into fewer field elements for the purpose of creating lookup keys. +/// The packed field elements can be either random linearly combined (RLC'd) or Poseidon-hashed into lookup keys. /// /// Each element in the return value corrresponds to a Keccak chunk. If is_final = true, this element is the lookup key of the corresponding logical input. -pub fn encode_inputs_from_keccak_fs( +pub fn pack_inputs_from_keccak_fs( ctx: &mut Context, gate: &impl GateInstructions, - initialized_hasher: &PoseidonHasher, loaded_keccak_fs: &[LoadedKeccakF], -) -> Vec> { +) -> Vec> { // Circuit parameters let num_poseidon_absorb_per_keccak_f = num_poseidon_absorb_per_keccak_f::(); let num_word_per_witness = num_word_per_witness::(); @@ -445,6 +436,7 @@ pub fn encode_inputs_from_keccak_fs( let mut compact_chunk_inputs = Vec::with_capacity(loaded_keccak_fs.len()); let mut last_is_final = one_const; + // TODO: this could be parallelized for loaded_keccak_f in loaded_keccak_fs { // If this keccak_f is the last of a logical input. let is_final = loaded_keccak_f.is_final; @@ -474,6 +466,95 @@ pub fn encode_inputs_from_keccak_fs( compact_chunk_inputs.push(PoseidonCompactChunkInput::new(compact_inputs, is_final)); last_is_final = is_final.into(); } + compact_chunk_inputs +} +/// Encode raw inputs from Keccak circuit witnesses into lookup keys. +/// +/// Each element in the return value corrresponds to a Keccak chunk. If is_final = true, this element is the lookup key of the corresponding logical input. +pub fn encode_inputs_from_keccak_fs( + ctx: &mut Context, + gate: &impl GateInstructions, + initialized_hasher: &PoseidonHasher, + loaded_keccak_fs: &[LoadedKeccakF], +) -> Vec> { + let compact_chunk_inputs = pack_inputs_from_keccak_fs(ctx, gate, loaded_keccak_fs); initialized_hasher.hash_compact_chunk_inputs(ctx, gate, &compact_chunk_inputs) } + +/// Converts the pertinent raw assigned cells from a keccak_f permutation into virtual `halo2-lib` cells so they can be used +/// by [halo2_base]. This function doesn't create any new witnesses/constraints. +/// +/// This function is made public for external libraries to use for compatibility. It is the responsibility of the developer +/// to ensure that `rows_per_round` **must** match the configuration of the vanilla zkEVM Keccak circuit itself. +/// +/// ## Assumptions +/// - `rows_per_round` **must** match the configuration of the vanilla zkEVM Keccak circuit itself. +/// - `assigned_rows` **must** start from the 0-th row of the keccak circuit. This is because the first `rows_per_round` rows are dummy rows. +pub fn transmute_keccak_assigned_to_virtual( + copy_manager: &SharedCopyConstraintManager, + assigned_rows: Vec>, + rows_per_round: usize, +) -> Vec> { + let mut copy_manager = copy_manager.lock().unwrap(); + assigned_rows + .into_iter() + .step_by(rows_per_round) + // Skip the first round which is dummy. + .skip(1) + .chunks(NUM_ROUNDS + 1) + .into_iter() + .map(|rounds| { + let mut rounds = rounds.collect_vec(); + assert_eq!(rounds.len(), NUM_ROUNDS + 1); + let bytes_left = copy_manager.load_external_assigned(rounds[0].bytes_left.clone()); + let output_row = rounds.pop().unwrap(); + let word_values = core::array::from_fn(|i| { + let assigned_row = &rounds[i]; + copy_manager.load_external_assigned(assigned_row.word_value.clone()) + }); + let is_final = SafeTypeChip::unsafe_to_bool( + copy_manager.load_external_assigned(output_row.is_final), + ); + let hash_lo = copy_manager.load_external_assigned(output_row.hash_lo); + let hash_hi = copy_manager.load_external_assigned(output_row.hash_hi); + LoadedKeccakF { bytes_left, word_values, is_final, hash_lo, hash_hi } + }) + .collect() +} + +impl CircuitExt for KeccakComponentShardCircuit { + fn instances(&self) -> Vec> { + let circuit_outputs = multi_inputs_to_circuit_outputs(&self.inputs, self.params.capacity); + if self.params.publish_raw_outputs { + vec![ + circuit_outputs.iter().map(|o| o.key).collect(), + circuit_outputs.iter().map(|o| o.hash_lo).collect(), + circuit_outputs.iter().map(|o| o.hash_hi).collect(), + ] + } else { + vec![vec![calculate_circuit_outputs_commit(&circuit_outputs)]] + } + } + + fn num_instance(&self) -> Vec { + if self.params.publish_raw_outputs { + vec![self.params.capacity; OUTPUT_NUM_COL_RAW] + } else { + vec![1; OUTPUT_NUM_COL_COMMIT] + } + } + + fn accumulator_indices() -> Option> { + None + } + + fn selectors(config: &Self::Config) -> Vec { + // the vanilla keccak circuit does not use selectors + // this is from the BaseCircuitBuilder + config.base_circuit_config.gate().basic_gates[0] + .iter() + .map(|basic| basic.q_enable) + .collect() + } +} diff --git a/hashes/zkevm/src/keccak/component/encode.rs b/hashes/zkevm/src/keccak/component/encode.rs index 33230bee..8767c404 100644 --- a/hashes/zkevm/src/keccak/component/encode.rs +++ b/hashes/zkevm/src/keccak/component/encode.rs @@ -8,7 +8,7 @@ use halo2_base::{ }; use itertools::Itertools; use num_bigint::BigUint; -use snark_verifier::loader::native::NativeLoader; +use snark_verifier_sdk::{snark_verifier, NativeLoader}; use crate::{ keccak::vanilla::{keccak_packed_multi::get_num_keccak_f, param::*}, @@ -24,6 +24,27 @@ use super::param::*; /// Encode a native input bytes into its corresponding lookup key. This function can be considered as the spec of the encoding. pub fn encode_native_input(bytes: &[u8]) -> F { + let witnesses_per_keccak_f = pack_native_input(bytes); + // Absorb witnesses keccak_f by keccak_f. + let mut native_poseidon_sponge = + snark_verifier::util::hash::Poseidon::::new::< + POSEIDON_R_F, + POSEIDON_R_P, + POSEIDON_SECURE_MDS, + >(&NativeLoader); + for witnesses in witnesses_per_keccak_f { + for absorbing in witnesses.chunks(POSEIDON_RATE) { + // To avoid absorbing witnesses crossing keccak_fs together, pad 0s to make sure absorb.len() == RATE. + let mut padded_absorb = [F::ZERO; POSEIDON_RATE]; + padded_absorb[..absorbing.len()].copy_from_slice(absorbing); + native_poseidon_sponge.update(&padded_absorb); + } + } + native_poseidon_sponge.squeeze() +} + +/// Pack native input bytes into num_word_per_witness field elements which are more poseidon friendly. +pub fn pack_native_input(bytes: &[u8]) -> Vec> { assert!(NUM_BITS_PER_WORD <= u128::BITS as usize); let multipliers: Vec = get_words_to_witness_multipliers::(); let num_word_per_witness = num_word_per_witness::(); @@ -68,22 +89,7 @@ pub fn encode_native_input(bytes: &[u8]) -> F { .collect_vec() }) .collect_vec(); - // Absorb witnesses keccak_f by keccak_f. - let mut native_poseidon_sponge = - snark_verifier::util::hash::Poseidon::::new::< - POSEIDON_R_F, - POSEIDON_R_P, - POSEIDON_SECURE_MDS, - >(&NativeLoader); - for witnesses in witnesses_per_keccak_f { - for absorbing in witnesses.chunks(POSEIDON_RATE) { - // To avoid absorbing witnesses crossing keccak_fs together, pad 0s to make sure absorb.len() == RATE. - let mut padded_absorb = [F::ZERO; POSEIDON_RATE]; - padded_absorb[..absorbing.len()].copy_from_slice(absorbing); - native_poseidon_sponge.update(&padded_absorb); - } - } - native_poseidon_sponge.squeeze() + witnesses_per_keccak_f } /// Encode a VarLenBytesVec into its corresponding lookup key. @@ -117,7 +123,7 @@ pub fn encode_var_len_bytes_vec( initialized_hasher.hash_compact_chunk_inputs(ctx, range_chip.gate(), &chunk_inputs); range_chip.gate().select_by_indicator( ctx, - compact_outputs.into_iter().map(|o| *o.hash()), + compact_outputs.into_iter().map(|o| o.hash()), f_indicator, ) } @@ -154,7 +160,7 @@ pub const fn num_word_per_witness() -> usize { /// Number of witnesses to represent inputs in a keccak_f. /// -/// Assume the representation of is not longer than a Keccak word. +/// Assume the representation of \ is not longer than a Keccak word. /// /// When `F` is `bn254::Fr`, this is 6. pub const fn num_witness_per_keccak_f() -> usize { @@ -197,7 +203,7 @@ pub(crate) fn get_bytes_to_words_multipliers() -> Vec { multipliers } -fn format_input( +pub fn format_input( ctx: &mut Context, gate: &impl GateInstructions, bytes: &[SafeByte], diff --git a/hashes/zkevm/src/keccak/component/ingestion.rs b/hashes/zkevm/src/keccak/component/ingestion.rs index cc0b2c3f..c65ebc0c 100644 --- a/hashes/zkevm/src/keccak/component/ingestion.rs +++ b/hashes/zkevm/src/keccak/component/ingestion.rs @@ -42,12 +42,12 @@ impl KeccakIngestionFormat { /// Very similar to [crate::keccak::component::encode::encode_native_input] except we do not do the /// encoding part (that will be done in circuit, not natively). /// -/// Returns `Err(true_capacity)` if `true_capacity > capacity`, where `true_capacity` is the number of keccak_f needed -/// to compute all requests. +/// Returns `(ingestions, true_capacity)`, where `ingestions` is resized to `capacity` length +/// and `true_capacity` is the number of keccak_f needed to compute all requests. pub fn format_requests_for_ingestion( requests: impl IntoIterator)>, capacity: usize, -) -> Result, usize> +) -> (Vec, usize) where B: AsRef<[u8]>, { @@ -77,10 +77,7 @@ where last_mut.hash_lo = u128::from_be_bytes(hash[16..].try_into().unwrap()); } log::info!("Actual number of keccak_f used = {}", ingestions.len()); - if ingestions.len() > capacity { - Err(ingestions.len()) - } else { - ingestions.resize_with(capacity, Default::default); - Ok(ingestions) - } + let true_capacity = ingestions.len(); + ingestions.resize_with(capacity, Default::default); + (ingestions, true_capacity) } diff --git a/hashes/zkevm/src/keccak/component/output.rs b/hashes/zkevm/src/keccak/component/output.rs index fa010bbe..2fe46ecb 100644 --- a/hashes/zkevm/src/keccak/component/output.rs +++ b/hashes/zkevm/src/keccak/component/output.rs @@ -2,7 +2,7 @@ use super::{encode::encode_native_input, param::*}; use crate::{keccak::vanilla::keccak_packed_multi::get_num_keccak_f, util::eth_types::Field}; use itertools::Itertools; use sha3::{Digest, Keccak256}; -use snark_verifier::loader::native::NativeLoader; +use snark_verifier_sdk::{snark_verifier, NativeLoader}; /// Witnesses to be exposed as circuit outputs. #[derive(Clone, Copy, PartialEq, Debug)] diff --git a/hashes/zkevm/src/keccak/vanilla/keccak_packed_multi.rs b/hashes/zkevm/src/keccak/vanilla/keccak_packed_multi.rs index 335862bd..6a78efc9 100644 --- a/hashes/zkevm/src/keccak/vanilla/keccak_packed_multi.rs +++ b/hashes/zkevm/src/keccak/vanilla/keccak_packed_multi.rs @@ -55,7 +55,7 @@ pub(crate) struct SqueezeData { packed: F, } -/// KeccakRow. Field definitions could be found in [KeccakCircuitConfig]. +/// KeccakRow. Field definitions could be found in [super::KeccakCircuitConfig]. #[derive(Clone, Debug)] pub struct KeccakRow { pub(crate) q_enable: bool, @@ -132,7 +132,7 @@ impl KeccakRegion { } } -/// Keccak Table, used to verify keccak hashing from RLC'ed input. +/// Keccak Table, used to verify keccak hash digests from input spread out across multiple rows. #[derive(Clone, Debug)] pub struct KeccakTable { /// True when the row is enabled @@ -489,7 +489,7 @@ pub(crate) mod transform { } } -// Transforms values to cells +// Transfroms values to cells pub(crate) mod transform_to { use crate::{ halo2_proofs::plonk::{ConstraintSystem, TableColumn}, diff --git a/hashes/zkevm/src/keccak/vanilla/mod.rs b/hashes/zkevm/src/keccak/vanilla/mod.rs index 89fce6bb..11baa66f 100644 --- a/hashes/zkevm/src/keccak/vanilla/mod.rs +++ b/hashes/zkevm/src/keccak/vanilla/mod.rs @@ -17,6 +17,7 @@ use halo2_base::utils::halo2::{raw_assign_advice, raw_assign_fixed}; use itertools::Itertools; use log::{debug, info}; use rayon::prelude::{IntoParallelRefIterator, ParallelIterator}; +use serde::{Deserialize, Serialize}; use std::marker::PhantomData; pub mod cell_manager; @@ -30,7 +31,7 @@ pub mod util; pub mod witness; /// Configuration parameters to define [`KeccakCircuitConfig`] -#[derive(Copy, Clone, Debug, Default)] +#[derive(Copy, Clone, Debug, Default, Serialize, Deserialize)] pub struct KeccakConfigParams { /// The circuit degree, i.e., circuit has 2k rows pub k: u32, @@ -277,7 +278,7 @@ impl KeccakCircuitConfig { // multiple rows with lookups in a way that doesn't require any // extra additional cells or selectors we have to put all `s[i]`'s on the same // row. This isn't that strong of a requirement actually because we the - // words are split into multiple parts, and so only the parts at the same + // words are split into multipe parts, and so only the parts at the same // position of those words need to be on the same row. let target_word_sizes = target_part_sizes(part_size); let num_word_parts = target_word_sizes.len(); @@ -635,7 +636,7 @@ impl KeccakCircuitConfig { }); // Logically here we want !q_input[cur] && !start_new_hash(cur) ==> bytes_left[cur + num_rows_per_round] == bytes_left[cur] // In practice, in order to save a degree we use !(q_input[cur] ^ start_new_hash(cur)) ==> bytes_left[cur + num_rows_per_round] == bytes_left[cur] - // When q_input[cur] is true, the above constraint q_input[cur] ==> bytes_left[cur + num_rows_per_round] + word_len == bytes_left[cur] has + // When q_input[cur] is true, the above constraint q_input[cur] ==> bytes_left[cur + num_rows_per_round] + word_len == bytes_left[cur] has // already been enabled. Even is_final in start_new_hash(cur) is true, it's just over-constrainted. // Note: At the first row of any round except the last round, is_final could be either true or false. cb.condition(not::expr(q(q_input, meta) + start_new_hash(meta, Rotation::cur())), |cb| { diff --git a/hashes/zkevm/src/keccak/vanilla/tests.rs b/hashes/zkevm/src/keccak/vanilla/tests.rs index f79aa4b7..efade6c7 100644 --- a/hashes/zkevm/src/keccak/vanilla/tests.rs +++ b/hashes/zkevm/src/keccak/vanilla/tests.rs @@ -21,6 +21,7 @@ use crate::halo2_proofs::{ use halo2_base::{ halo2_proofs::halo2curves::ff::FromUniformBytes, utils::value_to_option, SKIP_FIRST_PASS, }; +use hex::FromHex; use rand_core::OsRng; use sha3::{Digest, Keccak256}; use test_case::test_case; @@ -291,3 +292,33 @@ fn packed_multi_keccak_prover(k: u32, rows_per_round: usize) { >(&verifier_params, pk.get_vk(), strategy, &[&[]], &mut verifier_transcript) .expect("failed to verify bench circuit"); } + +// Keccak Known Answer Test (KAT) vectors from https://keccak.team/obsolete/KeccakKAT-3.zip. +// Only selecting a small subset for now (add more later) +// KAT includes inputs at the bit level; we only include the ones that are bytes +#[test] +fn test_vanilla_keccak_kat_vectors() { + let _ = env_logger::builder().is_test(true).try_init(); + + // input, output, Len in bits + let test_vectors = vec![ + ("", "C5D2460186F7233C927E7DB2DCC703C0E500B653CA82273B7BFAD8045D85A470"), // ShortMsgKAT_256 Len = 0 + ("CC", "EEAD6DBFC7340A56CAEDC044696A168870549A6A7F6F56961E84A54BD9970B8A"), // ShortMsgKAT_256 Len = 8 + ("B55C10EAE0EC684C16D13463F29291BF26C82E2FA0422A99C71DB4AF14DD9C7F33EDA52FD73D017CC0F2DBE734D831F0D820D06D5F89DACC485739144F8CFD4799223B1AFF9031A105CB6A029BA71E6E5867D85A554991C38DF3C9EF8C1E1E9A7630BE61CAABCA69280C399C1FB7A12D12AEFC", "0347901965D3635005E75A1095695CCA050BC9ED2D440C0372A31B348514A889"), // ShortMsgKAT_256 Len = 920 + ("2EDC282FFB90B97118DD03AAA03B145F363905E3CBD2D50ECD692B37BF000185C651D3E9726C690D3773EC1E48510E42B17742B0B0377E7DE6B8F55E00A8A4DB4740CEE6DB0830529DD19617501DC1E9359AA3BCF147E0A76B3AB70C4984C13E339E6806BB35E683AF8527093670859F3D8A0FC7D493BCBA6BB12B5F65E71E705CA5D6C948D66ED3D730B26DB395B3447737C26FAD089AA0AD0E306CB28BF0ACF106F89AF3745F0EC72D534968CCA543CD2CA50C94B1456743254E358C1317C07A07BF2B0ECA438A709367FAFC89A57239028FC5FECFD53B8EF958EF10EE0608B7F5CB9923AD97058EC067700CC746C127A61EE3", "DD1D2A92B3F3F3902F064365838E1F5F3468730C343E2974E7A9ECFCD84AA6DB"), // ShortMsgKAT_256 Len = 1952, + ("724627916C50338643E6996F07877EAFD96BDF01DA7E991D4155B9BE1295EA7D21C9391F4C4A41C75F77E5D27389253393725F1427F57914B273AB862B9E31DABCE506E558720520D33352D119F699E784F9E548FF91BC35CA147042128709820D69A8287EA3257857615EB0321270E94B84F446942765CE882B191FAEE7E1C87E0F0BD4E0CD8A927703524B559B769CA4ECE1F6DBF313FDCF67C572EC4185C1A88E86EC11B6454B371980020F19633B6B95BD280E4FBCB0161E1A82470320CEC6ECFA25AC73D09F1536F286D3F9DACAFB2CD1D0CE72D64D197F5C7520B3CCB2FD74EB72664BA93853EF41EABF52F015DD591500D018DD162815CC993595B195", "EA0E416C0F7B4F11E3F00479FDDF954F2539E5E557753BD546F69EE375A5DE29"), // LongMsgKAT_256 Len = 2048 + ("6E1CADFB2A14C5FFB1DD69919C0124ED1B9A414B2BEA1E5E422D53B022BDD13A9C88E162972EBB9852330006B13C5B2F2AFBE754AB7BACF12479D4558D19DDBB1A6289387B3AC084981DF335330D1570850B97203DBA5F20CF7FF21775367A8401B6EBE5B822ED16C39383232003ABC412B0CE0DD7C7DA064E4BB73E8C58F222A1512D5FE6D947316E02F8AA87E7AA7A3AA1C299D92E6414AE3B927DB8FF708AC86A09B24E1884743BC34067BB0412453B4A6A6509504B550F53D518E4BCC3D9C1EFDB33DA2EACCB84C9F1CAEC81057A8508F423B25DB5500E5FC86AB3B5EB10D6D0BF033A716DDE55B09FD53451BBEA644217AE1EF91FAD2B5DCC6515249C96EE7EABFD12F1EF65256BD1CFF2087DABF2F69AD1FFB9CF3BC8CA437C7F18B6095BC08D65DF99CC7F657C418D8EB109FDC91A13DC20A438941726EF24F9738B6552751A320C4EA9C8D7E8E8592A3B69D30A419C55FB6CB0850989C029AAAE66305E2C14530B39EAA86EA3BA2A7DECF4B2848B01FAA8AA91F2440B7CC4334F63061CE78AA1589BEFA38B194711697AE3AADCB15C9FBF06743315E2F97F1A8B52236ACB444069550C2345F4ED12E5B8E881CDD472E803E5DCE63AE485C2713F81BC307F25AC74D39BAF7E3BC5E7617465C2B9C309CB0AC0A570A7E46C6116B2242E1C54F456F6589E20B1C0925BF1CD5F9344E01F63B5BA9D4671ABBF920C7ED32937A074C33836F0E019DFB6B35D865312C6058DFDAFF844C8D58B75071523E79DFBAB2EA37479DF12C474584F4FF40F00F92C6BADA025CE4DF8FAF0AFB2CE75C07773907CA288167D6B011599C3DE0FFF16C1161D31DF1C1DDE217CB574ED5A33751759F8ED2B1E6979C5088B940926B9155C9D250B479948C20ACB5578DC02C97593F646CC5C558A6A0F3D8D273258887CCFF259197CB1A7380622E371FD2EB5376225EC04F9ED1D1F2F08FA2376DB5B790E73086F581064ED1C5F47E989E955D77716B50FB64B853388FBA01DAC2CEAE99642341F2DA64C56BEFC4789C051E5EB79B063F2F084DB4491C3C5AA7B4BCF7DD7A1D7CED1554FA67DCA1F9515746A237547A4A1D22ACF649FA1ED3B9BB52BDE0C6996620F8CFDB293F8BACAD02BCE428363D0BB3D391469461D212769048219220A7ED39D1F9157DFEA3B4394CA8F5F612D9AC162BF0B961BFBC157E5F863CE659EB235CF98E8444BC8C7880BDDCD0B3B389AAA89D5E05F84D0649EEBACAB4F1C75352E89F0E9D91E4ACA264493A50D2F4AED66BD13650D1F18E7199E931C78AEB763E903807499F1CD99AF81276B615BE8EC709B039584B2B57445B014F6162577F3548329FD288B0800F936FC5EA1A412E3142E609FC8E39988CA53DF4D8FB5B5FB5F42C0A01648946AC6864CFB0E92856345B08E5DF0D235261E44CFE776456B40AEF0AC1A0DFA2FE639486666C05EA196B0C1A9D346435E03965E6139B1CE10129F8A53745F80100A94AE04D996C13AC14CF2713E39DFBB19A936CF3861318BD749B1FB82F40D73D714E406CBEB3D920EA037B7DE566455CCA51980F0F53A762D5BF8A4DBB55AAC0EDDB4B1F2AED2AA3D01449D34A57FDE4329E7FF3F6BECE4456207A4225218EE9F174C2DE0FF51CEAF2A07CF84F03D1DF316331E3E725C5421356C40ED25D5ABF9D24C4570FED618CA41000455DBD759E32E2BF0B6C5E61297C20F752C3042394CE840C70943C451DD5598EB0E4953CE26E833E5AF64FC1007C04456D19F87E45636F456B7DC9D31E757622E2739573342DE75497AE181AAE7A5425756C8E2A7EEF918E5C6A968AEFE92E8B261BBFE936B19F9E69A3C90094096DAE896450E1505ED5828EE2A7F0EA3A28E6EC47C0AF711823E7689166EA07ECA00FFC493131D65F93A4E1D03E0354AFC2115CFB8D23DAE8C6F96891031B23226B8BC82F1A73DAA5BB740FC8CC36C0975BEFA0C7895A9BBC261EDB7FD384103968F7A18353D5FE56274E4515768E4353046C785267DE01E816A2873F97AAD3AB4D7234EBFD9832716F43BE8245CF0B4408BA0F0F764CE9D24947AB6ABDD9879F24FCFF10078F5894B0D64F6A8D3EA3DD92A0C38609D3C14FDC0A44064D501926BE84BF8034F1D7A8C5F382E6989BFFA2109D4FBC56D1F091E8B6FABFF04D21BB19656929D19DECB8E8291E6AE5537A169874E0FE9890DFF11FFD159AD23D749FB9E8B676E2C31313C16D1EFA06F4D7BC191280A4EE63049FCEF23042B20303AECDD412A526D7A53F760A089FBDF13F361586F0DCA76BB928EDB41931D11F679619F948A6A9E8DBA919327769006303C6EF841438A7255C806242E2E7FF4621BB0F8AFA0B4A248EAD1A1E946F3E826FBFBBF8013CE5CC814E20FEF21FA5DB19EC7FF0B06C592247B27E500EB4705E6C37D41D09E83CB0A618008CA1AAAE8A215171D817659063C2FA385CFA3C1078D5C2B28CE7312876A276773821BE145785DFF24BBB24D590678158A61EA49F2BE56FDAC8CE7F94B05D62F15ADD351E5930FD4F31B3E7401D5C0FF7FC845B165FB6ABAFD4788A8B0615FEC91092B34B710A68DA518631622BA2AAE5D19010D307E565A161E64A4319A6B261FB2F6A90533997B1AEC32EF89CF1F232696E213DAFE4DBEB1CF1D5BBD12E5FF2EBB2809184E37CD9A0E58A4E0AF099493E6D8CC98B05A2F040A7E39515038F6EE21FC25F8D459A327B83EC1A28A234237ACD52465506942646AC248EC96EBBA6E1B092475F7ADAE4D35E009FD338613C7D4C12E381847310A10E6F02C02392FC32084FBE939689BC6518BE27AF7842DEEA8043828E3DFFE3BBAC4794CA0CC78699722709F2E4B0EAE7287DEB06A27B462423EC3F0DF227ACF589043292685F2C0E73203E8588B62554FF19D6260C7FE48DF301509D33BE0D8B31D3F658C921EF7F55449FF3887D91BFB894116DF57206098E8C5835B", "3C79A3BD824542C20AF71F21D6C28DF2213A041F77DD79A328A0078123954E7B"), // LongMsgKAT_256 Len = 16664 + ("7ADC0B6693E61C269F278E6944A5A2D8300981E40022F839AC644387BFAC9086650085C2CDC585FEA47B9D2E52D65A2B29A7DC370401EF5D60DD0D21F9E2B90FAE919319B14B8C5565B0423CEFB827D5F1203302A9D01523498A4DB10374", "4CC2AFF141987F4C2E683FA2DE30042BACDCD06087D7A7B014996E9CFEAA58CE"), // ShortMsgKAT_256 Len = 752 + ]; + + let mut inputs = vec![]; + for (input, output) in test_vectors { + let input = Vec::from_hex(input).unwrap(); + let output = Vec::from_hex(output).unwrap(); + // test against native sha3 implementation because that's what we will test circuit against + let native_out = Keccak256::digest(&input); + assert_eq!(&output[..], &native_out[..]); + inputs.push(input); + } + verify::(KeccakConfigParams { k: 12, rows_per_round: 5 }, inputs, true); +} diff --git a/hashes/zkevm/src/keccak/vanilla/witness.rs b/hashes/zkevm/src/keccak/vanilla/witness.rs index d97d487d..bba2f05a 100644 --- a/hashes/zkevm/src/keccak/vanilla/witness.rs +++ b/hashes/zkevm/src/keccak/vanilla/witness.rs @@ -409,7 +409,6 @@ fn keccak( .into_iter() .take(8) .collect::>() - .to_vec() }) .collect::>(); debug!("hash: {:x?}", &(hash_bytes[0..4].concat())); diff --git a/hashes/zkevm/src/lib.rs b/hashes/zkevm/src/lib.rs index 272e4bf8..e17f02a9 100644 --- a/hashes/zkevm/src/lib.rs +++ b/hashes/zkevm/src/lib.rs @@ -1,5 +1,5 @@ //! The zkEVM keccak circuit implementation, with some minor modifications -//! Credit goes to https://github.com/privacy-scaling-explorations/zkevm-circuits/tree/main/zkevm-circuits/src/keccak_circuit +//! Credit goes to use halo2_base::halo2_proofs; diff --git a/hashes/zkevm/src/util/eth_types.rs b/hashes/zkevm/src/util/eth_types.rs index 6fed74a5..4e5574e9 100644 --- a/hashes/zkevm/src/util/eth_types.rs +++ b/hashes/zkevm/src/util/eth_types.rs @@ -9,7 +9,7 @@ pub use ethers_core::types::{ Address, Block, Bytes, Signature, H160, H256, H64, U256, U64, }; -/// Trait used to reduce verbosity with the declaration of the [`FieldExt`] +/// Trait used to reduce verbosity with the declaration of the [`PrimeField`] /// trait and its repr. pub trait Field: BigPrimeField + PrimeField {}