From 6a1f65a1f99429f3725ef4d6788f5643bb61aa6f Mon Sep 17 00:00:00 2001 From: Ho Date: Fri, 26 Jul 2024 17:51:42 +0800 Subject: [PATCH] fix: propagate `chain_id` over app SNARKs (batch circuit instances) (#1382) * propagate chain_id over recursion circuit instances * generic recursion for "propagated" app PI * mark chain id for "propagated" * fix typo * update doc * fix(doc): check CI run --------- Co-authored-by: Rohit Narurkar Co-authored-by: Rohit Narurkar --- aggregator/README.md | 11 +++++++--- aggregator/src/recursion.rs | 8 +++++++- aggregator/src/recursion/circuit.rs | 31 +++++++++++++++++++++++++---- prover/src/recursion.rs | 5 +++++ 4 files changed, 47 insertions(+), 8 deletions(-) diff --git a/aggregator/README.md b/aggregator/README.md index 1dc187e302..9f2c6db8d9 100644 --- a/aggregator/README.md +++ b/aggregator/README.md @@ -223,6 +223,7 @@ pub trait StateTransition: Sized { fn state_prev_indices() -> Vec fn state_indices() -> Vec fn additional_indices() -> Vec + fn propagate_indices() -> Vec } ``` @@ -230,13 +231,15 @@ pub trait StateTransition: Sized { 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` | `preprocessed_digest` | `init_states` | `final_states` | `propagated_additional_states` | `additional_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$. +- `propagated_additional_states` represent PIs in app states which do not involved in state transition, however, the PIs in recursion circuit must be "propagated" into the corresponding PI in every app circuit being verified recursively. For example, the PI of `chainID` in each batch circuit must be same when they are verified together in the recursion circuit +- `additional_states` represent the PIs in app state which do not involved in state transition, and only the PIs in the last app circuit for this part are "export" transparently. - `round` represents the number of batches being bundled recursively, i.e. $N$. ### Statements @@ -244,6 +247,8 @@ To verify the $k_{th}$ snark, we have 3 PIs from the current circuit, the snark - 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 +- if $N > 0$, $PI(init\_states) = PI_{prev}(init\_states)$, else $PI(init\_states) = PI_{app}(init\_states)$: propagate the init state, and for first recursion, the init state part of PI is passed to app circuit +- $PI_{app}(final\_states) = PI(final\_states)$: transparent pass the PIs in `final_states` to app circuit +- $PI_{app}(all\_additional\_states) = PI(all\_additional\_states)$: ensure the PIs in `propagated_additional_states` and `additional_states` would be passed to app circuit's PI fields, which are being marked by `additional_indices` +- if $N > 0$, $PI_{app}(propagated\_additional\_states) = PI_{prev}(propagated\_additional\_states)$: propagate the additional state being marked by `propagate_indices` - $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/recursion.rs b/aggregator/src/recursion.rs index 8f5a7c55b6..4b2c66dd27 100644 --- a/aggregator/src/recursion.rs +++ b/aggregator/src/recursion.rs @@ -82,7 +82,7 @@ pub trait StateTransition: Sized { /// Following is the indices of the layout of instance /// for StateTransition circuit, the default suppose /// single col of instance, and the layout is: - /// accumulator | prev_state | state | additional + /// accumulator | prev_state | state | additional (propagated) | additional (free) /// /// Notice we do not verify the layout of accumulator /// simply suppose they are put in the beginning @@ -113,4 +113,10 @@ pub trait StateTransition: Sized { let end = Self::num_instance(); (start..end).collect() } + + /// The indices of any "other instances" which should be propagated, i.e. must remain + /// unchanged in PI of each app circuit. + fn propagate_indices() -> Vec { + Vec::new() + } } diff --git a/aggregator/src/recursion/circuit.rs b/aggregator/src/recursion/circuit.rs index 2f61fc9045..392e4bfd23 100644 --- a/aggregator/src/recursion/circuit.rs +++ b/aggregator/src/recursion/circuit.rs @@ -82,7 +82,7 @@ pub struct RecursionCircuit { default_accumulator: KzgAccumulator, /// The SNARK witness from the k-th BatchCircuit. app: SnarkWitness, - /// The SNARK witness from the (k-1)-th BatchCircuit. + /// The SNARK witness from the previous RecursionCircuit, i.e. RecursionCircuit up to the (k-1)-th BatchCircuit. previous: SnarkWitness, /// The recursion round, starting at round=0 and incrementing at every subsequent recursion. round: usize, @@ -302,7 +302,7 @@ impl Circuit for RecursionCircuit { // 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. + // present. The first field in the "additional" fields is the chain ID. 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. @@ -441,6 +441,28 @@ impl Circuit for RecursionCircuit { .map(|(&st, &app_inst)| ("passing cur state to app", st, app_inst)) .collect::>(); + // Pick additional inst part in "previous state", verify the items at the front + // is currently propagated to the app inst which is marked as "propagated" + let propagate_app_states = previous_instances[index_additional_state..index_round] + .iter() + .zip( + ST::propagate_indices() + .into_iter() + .map(|i| &app_instances[i]), + ) + .map(|(&st, &app_propagated_inst)| { + ( + "propagate additional states in app (not first round)", + main_gate.mul( + &mut ctx, + Existing(app_propagated_inst), + Existing(not_first_round), + ), + st, + ) + }) + .collect::>(); + // 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. @@ -465,7 +487,7 @@ impl Circuit for RecursionCircuit { for (comment, lhs, rhs) in [ // Propagate the preprocessed digest. ( - "chain preprocessed digest", + "propagate preprocessed digest", main_gate.mul( &mut ctx, Existing(preprocessed_digest), @@ -475,7 +497,7 @@ impl Circuit for RecursionCircuit { ), // Verify that "round" increments by 1 when not the first round of recursion. ( - "round increment", + "increment recursion round", round, main_gate.add( &mut ctx, @@ -488,6 +510,7 @@ impl Circuit for RecursionCircuit { .chain(initial_state_propagate) .chain(verify_app_state) .chain(verify_app_init_state) + .chain(propagate_app_states) { use halo2_proofs::dev::unwrap_value; debug_assert_eq!( diff --git a/prover/src/recursion.rs b/prover/src/recursion.rs index aa50a41700..8e1694a56e 100644 --- a/prover/src/recursion.rs +++ b/prover/src/recursion.rs @@ -67,4 +67,9 @@ impl<'a, const N_SNARK: usize> StateTransition for RecursionTask<'a, N_SNARK> { fn num_additional_instance() -> usize { ADD_INSTANCE } + + fn propagate_indices() -> Vec { + // the first index of additional indices + vec![Self::additional_indices()[0]] + } }