From 6f199a1f4de1a7fb05d035ac119e21561e49efe2 Mon Sep 17 00:00:00 2001 From: Rohit Narurkar Date: Tue, 16 Jul 2024 14:42:13 +0100 Subject: [PATCH] Update `aggregator` doc (#1365) * Adjust documentation * Fix typo * Update README.md To emphase the "continuous" in aggregated data * doc: more inline documentation for RecursionCircuit * rephrase comment * Add more context to comment * Add more context to comment * rephrase comment * rephrase comment and add more context * nit-pick --------- Co-authored-by: Ray Gao Co-authored-by: Ho --- aggregator/README.md | 183 +++++++++++++++++++++------- aggregator/src/batch.rs | 3 - aggregator/src/recursion/circuit.rs | 128 ++++++++++++++----- 3 files changed, 232 insertions(+), 82 deletions(-) diff --git a/aggregator/README.md b/aggregator/README.md index 26723acf36..1dc187e302 100644 --- a/aggregator/README.md +++ b/aggregator/README.md @@ -1,20 +1,24 @@ Proof Aggregation ----- -![Architecture](./figures/architecture.jpg) +# Mechanism +Aggregation allows larger amounts of data to be verified on-chain using fewer proofs. +Currently, chunks (a list of continuous blocks) are first aggregated into a batch, then multiple batches are aggregated using a recursive scheme into a bundle. +The `bundle` is the current apex entity that will be verified on-chain. + + # Params |param|meaning | |:---:|:---| |k | number of valid chunks| -|n | max number of chunks per batch| +|n | max number of chunks per batch (hard-coded)| |t | number of rounds for the final hash $\lceil32\times n/136\rceil$ | -Currently `n` is hard coded to `10`. # Structs ## Chunk -A __chunk__ is a list of continuous blocks. It consists of 5 hashes: +A __chunk__ is a list of L2 `blocks` and will be proven by the `ChunkCircuit` (this is in fact the ZkEVM `SuperCircuit`). It consists of 5 hashes: - state root before this chunk - state root after this chunk - the withdraw root of this chunk @@ -47,93 +51,119 @@ If $k< n$, $(n-k)$ padded chunks are padded to the list. A padded chunk has the ## Batch -A __batch__ consists of continuous chunks of size `k`. If the input chunks' size `k` is less than `n`, we pad the input with `(n-k)` chunks identical to `chunk[k]`. +A __batch__ is a list of continuous `chunks` of size `k` that will be aggregated using the `BatchCircuit`. If the input chunks' size `k` is less than `n`, we pad the input with `(n-k)` chunks identical to `chunk[k]`. The batch is represented by the preimage fields to the `batch_hash`, which is constructed as: +``` +batchHash := keccak256(version || batch_index || l1_message_popped || total_l1_message_popped || batch_data_hash || versioned_hash || parent_batch_hash || last_block_timestamp || z || y) +``` +All preimage fields' values are provided to the batch through the `BatchHeader` struct, so it can correctly construct the hash state transition from `parent_batch_hash` to `batch_hash` (for current batch). + +Note that there are also implicit constraints between state roots before/after batch and the state roots of the chunks it has aggregated: +``` +prev_state_root := c_0.prev_state_root +post_state_root := c_k.post_state_root +``` + +## BatchHeader +The current schema for batch header is: + +|Field|Bytes|Type|Index|Comments| +|:---|:---|:---|:---|:---| +|version | 1 | uint8| 0| The batch version| +|batchIndex | 8 | uint64| 1| The index of the batch| +|l1MessagePopped | 8 | uint64| 9| Number of L1 messages popped in the batch| +|totalL1MessagePopped | 8 | uint64| 17| Number of total L1 messages popped after the batch| +|dataHash | 32 | bytes32| 25| The data hash of the batch| +|blobVersionedHash | 32 | bytes32| 57| The versioned hash of the blob with this batch’s data| +|parentBatchHash | 32 | bytes32| 89| The parent batch hash| +|lastBlockTimestamp | 8 | uint64| 121| The timestamp of the last block in this batch| +|blobDataProof | 64 | bytes64| 129| The blob data proof: z (32), y (32)| + +## Continuous batches +A list of continuous batches $b_1, \dots, b_k$ satisfy +``` +b_i.batch_hash == b_{i+1}.parent_batch_hash AND +b_i.post_state_root == b_{i+1}.prev_state_root +``` +for $i \in [1, k-1]$. +Unlike chunks aggregation, the last layer of recursive batch aggregation can accept an arbitrary number of batches. There's no explicit upper limit. Instead, the number of rounds of recursion can solely be defined by the latency target on L1 for those batches. As a result, continuous batches are never padded. + +## Bundle +A __bundle__ is a list of continuous `batches` that will be aggregated recursively using the `RecursionCircuit`. The __bundle__ is the current apex entity whose proof will be verified on-chain. # Circuits ## Chunk circuit -Circuit proving the relationship for a chunk is indeed the zkEVM circuit. It will go through 2 layers of compression circuit, and becomes a __snark__ struct. We do not list its details here. Abstractly, a snark circuit has the following properties: +Circuit proving the relationship for a chunk is the zkEVM circuit. It will go through 2 layers of compression circuit, and becomes a __snark__ struct. We do not list its details here. Abstractly, a snark circuit has the following properties: - it takes 44 elements as public inputs - 12 from accumulators - 32 from public input hash +## Batch Circuit -![Architecture](./figures/hashes.jpg) - -## Aggregation Circuit - -We want to aggregate `k` snarks, each from a valid chunk. We generate `(n-k)` padded chunks, and obtain a total of `n` snarks. - -In the above example, we have `k = 2` valid chunks, and `2` padded chunks. - -The padded snarks are identical the the last valid snark, so the aggregator does not need to generate snarks for padded chunks. +We want to aggregate `k` snarks, each from a valid chunk. We generate `(n-k)` padded chunks (by repeating the last non-padding chunk), and obtain a total of `n` snarks. +Additionally, the batch circuit has to ascertain the correct hash transition from the parent batch. ### Configuration -There will be three configurations for Aggregation circuit. -- FpConfig; used for snark aggregation -- KeccakConfig: used to build keccak table -- RlcConfig: used to compute RLC of hash inputs +There are several configuration subcomponents for batch circuit. +- FpConfig; used for snark aggregation. +- KeccakConfig: used to build keccak table. +- RlcConfig: used to compute RLC of hash inputs. +- BlobDataConfig: used for representing the zstd-encoded form of batch data, with `4096 * 31` rows. Each row is a byte value. An EIP-4844 blob consists of `4096 * 32` bytes, where we set the most-significant byte in each 32-bytes chunk as `0` to guarantee that each 32-bytes chunk is a valid BLS12-381 scalar field element. +- BatchDataConfig: used for representing the raw batch bytes, effectively constructing the random challenge point `z` for the KZG opening proof. +- DecoderConfig: implements an in-circuit zstd-decoder that decodes blob data into batch data +- BarycentricEvaluationConfig: used for evaluating the interpolated blob polynomial at an arbitrary challenge point `z`, where both `z` and the evaluation `y` are included in the `BatchHeader`. ### Public Input -The public input of the aggregation circuit consists of +The public input of the batch circuit consists of - 12 elements from accumulator -- 32 elements of `batch_pi_hash` +- 2 elements of `parent_state_root` (split by hi/lo) +- 2 elements of `parent_batch_hash` +- 2 elements of `current_state_root` +- 2 elements of `current_batch_hash` +- 1 element of `chain_id` +- 2 elements of `current_withdraw_root` -### Statements -For snarks $s_1,\dots,s_k,\dots, s_n$ the aggregation circuit argues the following statements. - -1. batch_data_hash digest is reused for public input hash. __Static__. +Note that `parent_state_root` is the same as `chunk[0].prev_state_root` and `current_state_root` is the same as `chunk[k].post_state_root`. When these chunk fields are assigned into keccak preimages, their cells are constrained against the public input to ensure equality. If any public input appears in the preimage of the `batch_hash`, their corresponding assigned preimage cells will be equality constrained as well. -2. batch_pi_hash used same roots as chunk_pi_hash. __Static__. -``` -batch_pi_hash := keccak(chain_id || chunk_1.prev_state_root || chunk_n.post_state_root || chunk_n.withdraw_root || batch_data_hash || z || y || versioned_hash) -``` -and `batch_pi_hash` matches public input. +### Statements +For snarks $s_1,\dots,s_k,\dots, s_n$ the batch circuit argues the following statements. -3. batch_data_hash and chunk[i].pi_hash use a same chunk[i].data_hash when chunk[i] is not padded +1. batch_data_hash digest is reused for batch hash. __Static__. +2. batch_data_hash and chunk[i].pi_hash use a same chunk[i].data_hash when chunk[i] is not padded ``` for i in 1 ... n chunk_pi_hash := keccak(chain_id || prev_state_root || post_state_root || withdraw_root || chunk_data_hash || chunk_txdata_hash) ``` - This is done by computing the RLCs of chunk[i]'s data_hash for `i=0..k`, and then check the RLC matches the one from the keccak table. -4. chunks are continuous when they are not padded: they are linked via the state roots. - +3. chunks are continuous when they are not padded: they are linked via the state roots. ``` for i in 1 ... k-1 c_i.post_state_root == c_{i+1}.prev_state_root ``` - -5. All the chunks use the same chain id. __Static__. +4. All the chunks use the same chain id. __Static__. ``` for i in 1 ... n batch.chain_id == chunk[i].chain_id ``` - -6. The last `(n-k)` chunk[i] are padding +5. The last `(n-k)` chunk[i] are padded chunks ``` for i in 1 ... n: if is_padding: chunk[i]'s chunk_pi_hash_rlc_cells == chunk[i-1].chunk_pi_hash_rlc_cells ``` This is done via comparing the `data_rlc` of `chunk_{i-1}` and ` chunk_{i}`. -7. the hash input length is correct -- hashes[0] has 200 bytes -- hashes[1..N_SNARKS+1] has 168 bytes input -- batch's data_hash length is 32 * number_of_valid_snarks -8. batch data hash is correct w.r.t. its RLCs -9. is_final_cells are set correctly +6. the hash input length is correct +- hashes[0] has 193 bytes (`batch_hash` preimage) +- hashes[1..N_SNARKS+1] has 168 bytes input (`chunk_pi_hash` preimages) +- batch's data_hash length is 32 * number_of_valid_snarks (`batch_data_hash` preimage) ### Handling dynamic inputs - - ![Dynamic_inputs](./figures/hash_table.jpg) - Our keccak table uses $2^{19}$ rows. Each keccak round takes `300` rows. When the number of round is less than $2^{19}/300$, the cell manager will fill in the rest of the rows with dummy hashes. The only hash that uses a dynamic number of rounds is the last hash. @@ -158,3 +188,62 @@ For the output of the final data hash Additional checks for dummy chunk - if `is_padding` for `i`-th chunk, we constrain `chunk[i]'s chunk_pi_hash_rlc_cells == chunk[i-1].chunk_pi_hash_rlc_cells` + +## Recursion Circuit + +`RecursionCircuit` aggregates $N$ SNARKs from a generic circuit (called `AppCircuit`). It achieves this aggregation by repeatedly combine each `AppCircuit`'s SNARK with a SNARK generated from last round of aggregation (hence the name `recursion`). In each round of recursion, the Recursion circuit verifies a SNARK from the `AppCircuit` and its SNARK from the “previous” round. For the first round of aggregation, a dummy SNARK is generated to combine with the first `AppCircuit` SNARK. Essentially, we have: + +$RC_{Snark}(N) \colonequals verify(App_{Snark}(N)) \bigvee verify(RC_{Snark}(N-1))$ + +where $RC$ indicates the Recursion circuit. +With `accumulator_indices` , Recursion Circuit can merge `AppCircuit` ’s accumulator, in case `AppCircuit` itself is also a Batch Circuit. + +### StateTransition Trait +The `AppCircuit` must follow a layout that `RecursionCircuit` accepts. The layout is described in the `StateTransition` trait which describes a data which can transition from prev state to current state, with methods clearly indicating the indices of accumulators, states (prev and post) and additional exported PI fields. + +```rust +pub trait StateTransition: Sized { + type Input: Clone; + type Circuit: CircuitExt; + + // Describes the state transition + fn state_transition(&self, round: usize) -> Self::Input; + + // Count of the fields used to represent state. The public input consists of twice + // this number as both the previous and current states are included in the public input. + fn num_transition_instance() -> usize + + // Other counts of instance variables + fn num_additional_instance() -> usize + fn num_instance() -> usize + fn num_accumulator_instance() -> usize + + // Location of accumulator, state variables and additional exported PIs + fn accumulator_indices() -> Vec + fn state_prev_indices() -> Vec + fn state_indices() -> Vec + fn additional_indices() -> Vec +} +``` + +### Public Inputs +All parts of $PI$ in `AppCircuit` is also put into the $PI$ of recursion circuit, the recursion circuit has a single column of $PI$ with following layout: + +```markdown +`accumulator` | `preprocessed_digest` | `init_states` | `final_states` | `round` +``` + +- `accumulator` accumulates all of the accumulators from the $N$ $snark_{app}$, all the accumulators exported from the $PI$ of these snarks (if there is any), and accumulators generated by the $N$ steps verification of snarks from recursion circuit. +- `preprocessed_digest` represents the Recursion Circuit itself. There would be an unique value for every recursion circuit which can bundle (any number of) snarks from specified `AppCircuit` +- `init_states` represent the initial state $S_0$. +- `final_states` represent the final state, along with the exported $PI$ from $S_N$. +- `round` represents the number of batches being bundled recursively, i.e. $N$. + +### Statements +To verify the $k_{th}$ snark, we have 3 PIs from the current circuit, the snark of $k_{th}$ `AppCircuit` , and the snark of $(k-1)_{th}$ recursion circuit respectively. We named it $PI$, $PI_{app}$ and $PI_{prev}$. We have following equality constraints for them: + +- if $N > 0$, $PI(preprocessed\_digest) = PI_{prev}(preprocessed\_digest)$: ensure the snark for “previous recursion circuit” is the same circuit of current one +- if $N > 0$, $PI(round) = PI_{prev}(round) + 1$: ensure the round number is increment so the first snark from app circuit has round = 0 +- $PI_{app}(final\_states) = PI(final\_states)$: transparent pass the PI to app circuit +- if $N > 0$, $PI(init\_states) = PI_{prev}(init\_states)$, else $PI(init\_states) = PI_{app}(init\_states)$c: propagate the init state, and for first recursion, the init state part of PI is passed to app circuit +- $PI_{app}(init\_states) = PI_{prev}(final\_states)$: the init state part of PI for app circuit must be “chained” with previous recursion round diff --git a/aggregator/src/batch.rs b/aggregator/src/batch.rs index bcfebe39d2..046a71c6e2 100644 --- a/aggregator/src/batch.rs +++ b/aggregator/src/batch.rs @@ -131,9 +131,6 @@ impl BatchHeader { /// - the first k chunks are from real traces /// - the last (#N_SNARKS-k) chunks are from empty traces /// A BatchHash consists of 2 hashes. -/// - batch_pi_hash := keccak(chain_id || chunk_0.prev_state_root || chunk_k-1.post_state_root || -/// chunk_k-1.withdraw_root || batch_data_hash || z || y || versioned_hash) -/// /// - batchHash := keccak256(version || batch_index || l1_message_popped || total_l1_message_popped || /// batch_data_hash || versioned_hash || parent_batch_hash || last_block_timestamp || z || y) /// - batch_data_hash := keccak(chunk_0.data_hash || ... || chunk_k-1.data_hash) diff --git a/aggregator/src/recursion/circuit.rs b/aggregator/src/recursion/circuit.rs index 7cb7cb8a9e..5ae92c0f7b 100644 --- a/aggregator/src/recursion/circuit.rs +++ b/aggregator/src/recursion/circuit.rs @@ -25,14 +25,21 @@ use sv_halo2_base::{ QuantumCell::Existing, }; -use crate::param::ConfigParams as BatchCircuitConfigParams; +use crate::param::ConfigParams as RecursionCircuitConfigParams; use super::*; +/// Convenience type to represent the verifying key. type Svk = KzgSuccinctVerifyingKey; + +/// Convenience type to represent the polynomial commitment scheme. type Pcs = Kzg; + +/// Convenience type to represent the accumulation scheme for accumulating proofs from multiple +/// SNARKs. type As = KzgAs; +/// Select condition ? LHS : RHS. fn select_accumulator<'a>( loader: &Rc>, condition: &AssignedValue, @@ -56,6 +63,7 @@ fn select_accumulator<'a>( )) } +/// Accumulate a value into the current accumulator. fn accumulate<'a>( loader: &Rc>, accumulators: Vec>>>, @@ -68,21 +76,39 @@ fn accumulate<'a>( #[derive(Clone)] pub struct RecursionCircuit { + /// The verifying key for the circuit. svk: Svk, + /// The default accumulator to initialise the circuit. default_accumulator: KzgAccumulator, + /// The SNARK witness from the k-th BatchCircuit. app: SnarkWitness, + /// The SNARK witness from the (k-1)-th BatchCircuit. previous: SnarkWitness, + /// The recursion round, starting at round=0 and incrementing at every subsequent recursion. round: usize, + /// The public inputs to the RecursionCircuit itself. instances: Vec, + /// The accumulation of the SNARK proofs recursed over thus far. as_proof: Value>, - app_is_aggregation: bool, + _marker: PhantomData, } impl RecursionCircuit { + /// The index of the preprocessed digest in the [`RecursionCircuit`]'s instances. Note that we + /// need a single cell to hold this value as it is a poseidon hash over the bn256 curve, hence + /// it fits within an [`Fr`] cell. + /// + /// [`Fr`]: halo2_proofs::halo2curves::bn256::Fr const PREPROCESSED_DIGEST_ROW: usize = 4 * LIMBS; + + /// The index within the instances to find the "initial" state in the state transition. const INITIAL_STATE_ROW: usize = Self::PREPROCESSED_DIGEST_ROW + 1; + /// Construct a new instance of the [`RecursionCircuit`] given the SNARKs from the current and + /// previous [`BatchCircuit`], and the recursion round. + /// + /// [`BatchCircuit`]: aggregator::BatchCircuit pub fn new( params: &ParamsKZG, app: Snark, @@ -180,7 +206,6 @@ impl RecursionCircuit { round, instances, as_proof: Value::known(as_proof), - app_is_aggregation: true, _marker: Default::default(), } } @@ -206,7 +231,14 @@ impl RecursionCircuit { /// Returns the number of instance cells in the Recursion Circuit, help to refine the CircuitExt trait pub fn num_instance_fixed() -> usize { - // [..lhs, ..rhs, preprocessed_digest, initial_state, state, round] + // [ + // ..lhs (accumulator LHS), + // ..rhs (accumulator RHS), + // preprocessed_digest, + // initial_state, + // state, + // round + // ] 4 * LIMBS + 2 * ST::num_transition_instance() + ST::num_additional_instance() + 2 } } @@ -225,14 +257,13 @@ impl Circuit for RecursionCircuit { instances: self.instances.clone(), as_proof: Value::unknown(), _marker: Default::default(), - app_is_aggregation: self.app_is_aggregation, } } fn configure(meta: &mut ConstraintSystem) -> Self::Config { let path = std::env::var("BUNDLE_CONFIG") .unwrap_or_else(|_| "configs/bundle_circuit.config".to_owned()); - let params: BatchCircuitConfigParams = serde_json::from_reader( + let params: RecursionCircuitConfigParams = serde_json::from_reader( File::open(path.as_str()).unwrap_or_else(|err| panic!("{err:?}")), ) .unwrap(); @@ -251,7 +282,7 @@ impl Circuit for RecursionCircuit { let mut first_pass = halo2_base::SKIP_FIRST_PASS; // assume using simple floor planner let assigned_instances = layouter.assign_region( - || "", + || "recursion circuit", |region| -> Result, Error> { if first_pass { first_pass = false; @@ -266,20 +297,29 @@ impl Circuit for RecursionCircuit { }, ); - let init_state_row_beg = Self::INITIAL_STATE_ROW; - let state_row_beg = init_state_row_beg + ST::num_transition_instance(); - let addition_state_beg = state_row_beg + ST::num_transition_instance(); - let round_row = addition_state_beg + ST::num_additional_instance(); + // The index of the "initial state", i.e. the state last finalised on L1. + let index_init_state = Self::INITIAL_STATE_ROW; + // The index of the "state", i.e. the state achieved post the current batch. + let index_state = index_init_state + ST::num_transition_instance(); + // The index where the "additional" fields required to define the state are + // present. + let index_additional_state = index_state + ST::num_transition_instance(); + // The index to find the "round" of recursion in the current instance of the + // Recursion Circuit. + let index_round = index_additional_state + ST::num_additional_instance(); + log::debug!( - "state position: init {}|cur {}|add {}", - state_row_beg, - addition_state_beg, - round_row + "indices within instances: init {} |cur {} | add {} | round {}", + index_init_state, + index_state, + index_additional_state, + index_round, ); + // Get the field elements representing the "preprocessed digest" and "recursion round". let [preprocessed_digest, round] = [ self.instances[Self::PREPROCESSED_DIGEST_ROW], - self.instances[round_row], + self.instances[index_round], ] .map(|instance| { main_gate @@ -287,7 +327,8 @@ impl Circuit for RecursionCircuit { .unwrap() }); - let initial_state = self.instances[init_state_row_beg..state_row_beg] + // Get the field elements representing the "initial state" + let initial_state = self.instances[index_init_state..index_state] .iter() .map(|&instance| { main_gate @@ -296,7 +337,9 @@ impl Circuit for RecursionCircuit { }) .collect::>(); - let state = self.instances[state_row_beg..round_row] + // Get the field elements representing the "state" post batch. This includes the + // additional state fields as well. + let state = self.instances[index_state..index_round] .iter() .map(|&instance| { main_gate @@ -305,6 +348,7 @@ impl Circuit for RecursionCircuit { }) .collect::>(); + // Whether or not we are in the first round of recursion. let first_round = main_gate.is_zero(&mut ctx, &round); let not_first_round = main_gate.not(&mut ctx, Existing(first_round)); @@ -318,6 +362,8 @@ impl Circuit for RecursionCircuit { Some(preprocessed_digest), ); + // Choose between the default accumulator or the previous accumulator depending on + // whether or not we are in the first round of recursion. let default_accumulator = self.load_default_accumulator(&loader)?; let previous_accumulators = previous_accumulators .iter() @@ -331,6 +377,8 @@ impl Circuit for RecursionCircuit { }) .collect::, Error>>()?; + // Accumulate the accumulators over the previous accumulators, to compute the + // accumulator values for this instance of the Recursion Circuit. let KzgAccumulator { lhs, rhs } = accumulate( &loader, [app_accumulators, previous_accumulators].concat(), @@ -343,9 +391,15 @@ impl Circuit for RecursionCircuit { let previous_instances = previous_instances.pop().unwrap(); let mut ctx = loader.ctx_mut(); + + ////////////////////////////////////////////////////////////////////////////////// + /////////////////////////////// CONSTRAINTS ////////////////////////////////////// + ////////////////////////////////////////////////////////////////////////////////// + + // Propagate the "initial state" let initial_state_propagate = initial_state .iter() - .zip_eq(previous_instances[init_state_row_beg..state_row_beg].iter()) + .zip_eq(previous_instances[index_init_state..index_state].iter()) .zip_eq( ST::state_prev_indices() .into_iter() @@ -353,21 +407,23 @@ impl Circuit for RecursionCircuit { ) .flat_map(|((&st, &previous_st), &app_inst)| { [ - // Propagate initial_state - ( - main_gate.mul(&mut ctx, Existing(st), Existing(not_first_round)), - previous_st, - ), - // Verify initial_state is same as the first application snark + // Verify initial_state is same as the first application snark in the + // first round of recursion. ( main_gate.mul(&mut ctx, Existing(st), Existing(first_round)), main_gate.mul(&mut ctx, Existing(app_inst), Existing(first_round)), ), + // Propagate initial_state for subsequent rounds of recursion. + ( + main_gate.mul(&mut ctx, Existing(st), Existing(not_first_round)), + previous_st, + ), ] }) .collect::>(); - // Verify current state is same as the current application snark + // Verify that the current "state" is the same as the state defined in the + // application SNARK. let verify_app_state = state .iter() .zip_eq( @@ -383,8 +439,10 @@ impl Circuit for RecursionCircuit { .map(|(&st, &app_inst)| (st, app_inst)) .collect::>(); - // Verify previous state (additional state not included) is same as the current application snark - let verify_app_init_state = previous_instances[state_row_beg..addition_state_beg] + // Verify that the "previous state" (additional state not included) is the same + // as the previous state defined in the current application SNARK. This check is + // meaningful only in subsequent recursion rounds after the first round. + let verify_app_init_state = previous_instances[index_state..index_additional_state] .iter() .zip_eq( ST::state_prev_indices() @@ -399,8 +457,10 @@ impl Circuit for RecursionCircuit { }) .collect::>(); + // Finally apply the equality constraints between the (LHS, RHS) values constructed + // above. for (lhs, rhs) in [ - // Propagate preprocessed_digest + // Propagate the preprocessed digest. ( main_gate.mul( &mut ctx, @@ -409,13 +469,13 @@ impl Circuit for RecursionCircuit { ), previous_instances[Self::PREPROCESSED_DIGEST_ROW], ), - // Verify round is increased by 1 when not at first round + // Verify that "round" increments by 1 when not the first round of recursion. ( round, main_gate.add( &mut ctx, Existing(not_first_round), - Existing(previous_instances[round_row]), + Existing(previous_instances[index_round]), ), ), ] @@ -427,13 +487,15 @@ impl Circuit for RecursionCircuit { ctx.region.constrain_equal(lhs.cell(), rhs.cell())?; } - // IMPORTANT: + // Mark the end of this phase. config.base_field_config.finalize(&mut ctx); + #[cfg(feature = "display")] dbg!(ctx.total_advice); #[cfg(feature = "display")] println!("Advice columns used: {}", ctx.advice_alloc[0][0].0 + 1); + // Return the computed instance cells for this Recursion Circuit. Ok([lhs.x(), lhs.y(), rhs.x(), rhs.y()] .into_iter() .flat_map(|coordinate| coordinate.limbs()) @@ -447,6 +509,8 @@ impl Circuit for RecursionCircuit { )?; assert_eq!(assigned_instances.len(), self.num_instance()[0]); + + // Ensure that the computed instances are in fact the instances for this circuit. for (row, limb) in assigned_instances.into_iter().enumerate() { layouter.constrain_instance(limb, config.instance, row)?; }