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 <[email protected]>
Co-authored-by: Rohit Narurkar <[email protected]>

Author: noel2004

aggregator/README.md

@@ -223,27 +223,32 @@ pub trait StateTransition: Sized {
     fn state_prev_indices() -> Vec<usize>
     fn state_indices() -> Vec<usize>
     fn additional_indices() -> Vec<usize>
+    fn propagate_indices() -> Vec<usize>
 }
 ```
 
 ### 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` | `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
 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
+- 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

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<usize> {
+        Vec::new()
+    }
 }

aggregator/src/recursion/circuit.rs

@@ -82,7 +82,7 @@ pub struct RecursionCircuit<ST> {
     default_accumulator: KzgAccumulator<G1Affine, NativeLoader>,
     /// 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<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
                 // 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<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
                     .map(|(&st, &app_inst)| ("passing cur state to app", st, app_inst))
                     .collect::<Vec<_>>();
 
+                // 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::<Vec<_>>();
+
                 // 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<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
                 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<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
                     ),
                     // 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<ST: StateTransition> Circuit<Fr> for RecursionCircuit<ST> {
                 .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!(

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<usize> {
+        // the first index of additional indices
+        vec![Self::additional_indices()[0]]
+    }
 }