# Recursive proof aggregation

**URL:** <https://forum.anoma.net/t/recursive-proof-aggregation/1643>\
**Category:** Proof aggregation\
**Created:** [June 20, 2025, 3:12pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643 "2025-06-20T15:12:27Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![kike](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/kike/32/745_2.png) [@kike](https://forum.anoma.net/u/kike)\
**Post date:** [June 20, 2025, 3:12pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/1 "2025-06-20T15:12:27Z")

</div>

In this post I will explain a concrete technique to aggregate all the proofs of a final (balanced) transaction. It is yet to be tested in practice. Pointing out mistakes, improvements, or opinions are welcome.

Given a program \mathsf P and an output x, the computational integrity statement that a proof \pi attests to is:

``\text{for program }\mathsf P \text{ and output }x, \text{ there exists an input } w \text{ such that } \mathsf P(w) = x."

The NP relation we are dealing with is \mathcal R:=\{(\mathsf p, x);w)\ |\ \mathsf P(w) = x\}. Thus, the input w is the _witness_. The description of the program (in lowercase \mathsf p) and the output form the _instance_. Let (\mathsf P, \mathsf V) be a proof system for \mathcal R.

Since the aggregation technique leverages recursive verification, we require succinct verification. This means the runtime of the verifier \mathsf V on instance (\mathsf p, x) is polylogarithmic in the runtime of the program \mathsf P on input x. Many SNARKs provide succinct verifiers (including the STARK scheme used in RISC0).

**What this post covers.** I will start explaining the basic idea, and then show how aggregations can be combined. From there we will see how to generalize to ‘universal’ aggregations, and finalize sketching how to connect the RM layer with the settlement layer via aggregating transaction proofs.

## Aggregating proofs – the basic idea

In the simplest case, all proofs are for the same program. Let us take as example the compliance logic (program) \mathsf P\_{c}(w\_c) \rightarrow x\_c run over compliance units. The exact structure of the witness w\_c, instance x\_c , and description of \mathsf P\_{c} is unimportant for the purposes of aggregation. We only care about the existence of a SNARK with succinct verification \mathbf{V}:

\mathbf{V}(\mathsf p\_{c},x\_c,\pi\_c) =1 \text{ if } \exists\ w\_c\text{ s.t. } \mathsf P\_{c}(w\_c) = x\_c

We aggregate compliance proofs one step at a time. At each step, a fresh output x\_c of the compliance program is verified using proof \pi\_c, and accumulated in a chaining hash h, (the bytes of x\_c are hashed). Also, the previous aggregation is verified. In pseudocode:

> \mathsf P\_{ac}(\mathsf p^{in},h^{in},\pi^{in},x\_c,\pi\_c)\rightarrow (\mathsf p^{out},h^{out}):
> 
> 1. Check 1 = \mathbf V (\mathsf p\_{c},x\_c,\pi\_c) // the description of the compliance program \mathsf P\_{c} is hard-coded in \mathsf P\_{ac}
> 2. If h^{in}\neq h\_0, check 1 = \mathbf V (\mathsf p^{in},h^{in},\pi^{in})
> 3. Output h^{out} := Hash(x\_{c},h^{in}) and \mathsf p^{out}:=\mathsf p^{in}

The aggregation program takes as input its own description \mathsf p^{in} := \mathsf p\_{ac}. This just means that it verifies an execution of itself for a previous chained hash h^{in}. In other words, the aggregation is an incrementally verifiable computation (IVC).

Generated transcripts are dynamic, and of virtually any length. One action with two compliance units will aggregate twice, but another action with three compliance units can performs three aggregations.

 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/2X/4/469ccc4d900d4aa5cc15707774412bd147bd2f79.png)

## Combining aggregations

With the IVC approach outlined above, a single actor can aggregate all the individual compliance proofs, independently of whether the proofs are from the same action (scope) or not.

Another possibility is that different actors aggregate in turns. For example, users announce unbalanced transactions with actions containing a single aggregated compliance proof \pi\_a. The solver compiles the final transaction, and in the process aggregates the aggregations.

How do we aggregate aggregations? The process is the same, noting that executions of \mathsf P\_{ac} can be verified incrementally once again.

> \mathsf P\_{aa}(\mathsf p^{in},h^{in},\pi^{in},x\_{ac},\pi\_{ac},)\rightarrow (\mathsf p^{out},h^{out}):
> 
> 1. Check 1 = \mathbf V (\mathsf p\_{ac},x\_c,\pi\_c) // the description of the aggregation program \mathsf P\_{ac} is hard-coded in \mathsf P\_{aa}
> 2. If h^{in}\neq h\_0, check 1 = \mathbf V (\mathsf p^{in},h^{in},\pi^{in})
> 3. Output h^{out} := Hash(x\_{ac},h^{in}) and \mathsf p^{out}:=\mathsf p^{in}

The two-round aggregation process is depicted below.

 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/2X/e/eb5f153f85a64885f73ffeb257a42954edb36ef4.jpeg)

## Non-uniform aggregation

Suppose we have a total of \ell programs \mathcal P :=\{P\_1,\ldots, P\_\ell\}. In practice, these are the \ell different resource logics of a given scope. Whether the scope is an action or a transaction only matters to decide if we aggregate in turns or in one go. The programs are numbered as they appear in resources (resources are assumed to be canonically ordered in the scope). In particular, they may repeat, i.e. \mathcal P is a multiset, meaning that for i\neq j, we may have P\_i = P\_j.

The blueprint presented for aggregation of compliance proofs is:

- at each step, verify an output of a specific program (the incremental verification),

- accumulate the verified output in a chained hash,

- verify correct aggregation up to the previous step (by recursive proof verification).

The blueprint can be translated to arbitrary program verification. The difference is that now at each incremental step we need to verify a _different_ program. The first idea that comes to mind is to hard-code the \ell programs in the aggregation circuit. But that would yield rigid aggregations. Each multiset \mathcal P of programs would necessitate their own aggregation program.

We seek a _universal_ aggregator that works for any two \mathcal P \neq \mathcal P'. To achieve it, the program P\_{j\_i} verified in the i-th incremental step is passed as an input. To keep track of what program is verified, the same trick as for outputs is used: the aggregation includes the (description of the) program P\_{j\_i} in a chained hash.

The pseudocode of the universal aggregator is as follows:

> \mathsf P\_{ua}(\mathsf p^{in},h^{in},d^{in},\pi^{in},\mathsf p,x,\pi)\rightarrow (\mathsf p^{out},h^{out},d^{out}):
> 
> 1. Check 1 = \mathbf V (\mathsf p,x,\pi) // the description of the verified program \mathsf p is an input of \mathsf P\_{ua}
> 2. If h^{in}\neq h\_0, d^{in}\neq d\_0, check 1 = \mathbf V (\mathsf p^{in},h^{in},d^{in},\pi^{in})
> 3. Output h^{out} := Hash(x,h^{in}), d^{out} := Hash(\mathsf p,d^{out}), and \mathsf p^{out}:=\mathsf p^{in}

#### Soundness

Sound aggregation relies on the knowledge soundness of the proof system (\mathbf P, \mathbf V), and on the collision resistance of the hash function. Hash.

Let a bunch of programs \mathsf P\_1,\ldots, \mathsf P\_\ell, and a bunch of outputs x\_1,\ldots,x\_\ell. If there exists a valid proof \pi\_{ua}, such that for chained hashes:

- h = Hash(x\_\ell,Hash(x\_{\ell-1},\cdots,Hash(x\_1,x\_{IV}))\cdots )

- d = Hash(\mathsf p\_\ell,Hash(\mathsf p\_{\ell-1},\cdots,Hash(\mathsf p\_1,x\_{IV}))\cdots )

the proof is valid \mathbf V (\mathsf p\_{ua},(\mathsf p\_{ua},h,d),\pi\_{ua}) = 1, then we can use the knowledge extractor to get an input (\mathsf p\_{ext},h\_{ext},d\_{ext},\pi\_{ext},\mathsf p\_{ext},x\_{ext},\pi'\_{ext}) such that h = Hash(x\_{ext}, h\_{ext}), and d = Hash(\mathsf p\_{ext}, h\_{ext}). Also, \pi'\_{ext} is a valid proof for program \mathsf p\_{ext} and output x\_{ext}.

If x\_{ext} \neq x\_\ell, or \mathsf p\_{ext} \neq \mathsf p\_{\ell}, the extractor is an algorithm that finds collisions for Hash. This process can be repeated to argue that x\_i is a verified output of the program \mathsf P\_i.

#### Parallel proving

Proof carrying data is a generalization of IVC that allows to generate any type of transcripts (not just sequential transcript). Esentially, the witness is split into input and local data. In our case the input/output of the aggregation is the running chained hash, and the local data is the instance and proof that is verified incrementally. Suppose we want aggregate validation of three outputs x\_1,x\_2,x\_3 of three programs \mathsf P\_1, \mathsf P\_2, \mathsf P\_3. The universal aggregator can be modified to accept two running pair of hashes (h^{in}\_1,d^{in}\_1), (h^{in}\_2,d^{in}\_2), and perform two recursive proof validations, one for each pair. Incremental aggregation is now more complex, but allows parallelizing via tree-like transcripts.

## Aggregating transaction proofs: from RM to settlement layer

The universal aggregator allows to generate a single proof for all proofs appearing in a transaction. Therefore, logic and compliance proofs can be accumulated together. This can be done either way, in two rounds, (aggregate within actions, then across actions), or in a single round (aggregate all individual logic and compliance proofs).

Well, you see where this is going. There is no reason we cannot aggregate transaction proofs. In the incremental proof generation, the digest and proof of the previous transaction is used to generate the proof of the new transaction. Obviously, this aggregation must be sequential and inherently two-round. Once the new proof is generated, the old one can be deleted. At all times, there will be a single proof attesting to the correctness of the logic and compliance predicates of all resources of the RM state. We can see this last aggregated proof as attesting to the _well-formedness of the RM state_.

 ![image](https://europe1.discourse-cdn.com/flex013/uploads/anoma1/original/2X/9/955118768d5faf85efbf32962a6a0e29a5ef345e.jpeg)

**Instance generation.** The instance of an aggregation will always consist of two chained hashes. The first hash (h) contains all the accumulated instances of the incremental programs being verified. In other words, all the resources of the transaction. The second hash (d) contains all the programs. That is, the compliance and logic predicates. How exactly the hashes are formed depends on the aggregation strategy: the fan-in and ordering used to form the transcript. In the picture above we can see two different aggregation strategies.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [June 24, 2025, 9:45am UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/2 "2025-06-24T09:45:41Z")

</div>

Thank you for the write up! Some comments after the first read:

> [@kike](#):
>
> we require succinct verification. This means the runtime of the verifier \mathsf V on instance (\mathsf p, x) is polylogarithmic in the runtime of the program \mathsf P on input x.

This is not the regular succinctness property of SNARKs. Where does it come from?

> [@kike](#):
>
> P\_{ac}(p^{in},h^{in},π^{in},x\_c,π\_c)→(p^{out},h^{out})

Shouldn’t we also output \pi^{out} here? Or is the aggregated proof just a hash? But then in the combined aggregation you use the same interface but if there is no proof in the output, what do you pass as input when aggregating aggregated proofs?

> and p^{out} := p^{in}

So it is always the same value?

> [@kike](#):
>
> If h^{in}\neq h\_0, check 1 = \mathbf V (\mathsf p^{in},(\mathsf p^{in},h^{in}),\pi^{in})

What is the value of h\_0?

> [@kike](#):
>
> Generated transcripts are dynamic, and of virtually any length

Do you mean that we can aggregate any number of proofs or are you talking of the resulting value being arbitrary length?

> [@kike](#):
>
> Output h^{out} := Hash(x\_{c},h^{in}) and \mathsf p^{out}:=\mathsf p^{in}

Shouldn’t this hash \pi^{in} in as well? Or generally anything that identifies the circuit

#### General comments:

1. Could you please define each variable in each pseudocode entry? It is really hard to remember the meaning of all inputs especially when there are ~8 of them
2. I think it would be helpful if you also defined how verification goes for each aggregated proof type (same or different circuits)
3. This post describes the approach using generic terms. I think it would be helpful to describe it using the terms we use so that we don’t have to keep in our head the mapping when reading (e.g., program description vs proving/verifying key)
4. Your point is basically that we use IVC for aggregation. I think it would be good to start with that (if that is the classic IVC definition or explain how it is different if it isn’t).
  1. Do we need anything on the risc0 side to use it?
  2. Does risc0 zkvm already support it or do we need to enable it ourselves?
  3. Can you specify what we need to use on risc0 side and what to implement additionally to enable aggregated proofs, at least in broad terms?

5. Perhaps including the relevant links to risc0 recursion (if needed), IVC definition we are referring to, and any other sources you used would be helpful

---

<div class="post-metadata">

**Author:** ![kike](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/kike/32/745_2.png) [@kike](https://forum.anoma.net/u/kike)\
**Post date:** [June 25, 2025, 6:18am UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/3 "2025-06-25T06:18:18Z")

</div>

> [@vveiln](#):
>
> This is not the regular succinctness property of SNARKs. Where does it come from?

To be able to recurse by _verifying_ proofs. Succinct verification is a well-known property, but not all the schemes have it. (For example, Bullletproofs has a linear-time verifier.)

> [@vveiln](#):
>
> Shouldn’t we also output \pi^{out} here? Or is the aggregated proof just a hash? But then in the combined aggregation you use the same interface but if there is no proof in the output, what do you pass as input when aggregating aggregated proofs?

After each aggregation step, the prover produces a proof of correct aggregation. This would be \pi^{out}, which then is fed as input to the next iteration step.

> [@vveiln](#):
>
> So it is always the same value?

Yes.

> [@vveiln](#):
>
> What is the value of h\_0?

A default, fixed value. For example, all-zero bytes.

> [@vveiln](#):
>
> Do you mean that we can aggregate any number of proofs or are you talking of the resulting value being arbitrary length?

We can aggregate any number of proofs. The number of aggregated profs is not fixed.

> [@vveiln](#):
>
> Shouldn’t this hash \pi^{in} in as well?

\pi^{in} is the proof of correct aggregation. If you mean the proof of the incremental verification (e.g. the compliance proof \pi\_c), I didn’t want to hash it so it doesn’t become part of the aggregated instance (the chained hash). We don’t really care what exact proof has been verified, but rather that there exists one.

> [@vveiln](#):
>
> Or generally anything that identifies the circuit

What do you mean?

> [@vveiln](#):
>
> Could you please define each variable in each pseudocode entry? It is really hard to remember the meaning of all inputs especially when there are ~8 of them

Which ones are unclear to you? I included pictures with the hope things will be clearer.

> [@vveiln](#):
>
> I think it would be helpful if you also defined how verification goes for each aggregated proof type (same or different circuits)

Not sure I follow here, sorry. For the same program (circuit), verification goes by hard-coding the verifier in the aggregation program. For aggregating proofs of different programs, it goes by hashing the verifier description, and those become part of the aggregated instance (together with the hash for the aggregated instances)

> [@vveiln](#):
>
> Your point is basically that we use IVC for aggregation. I think it would be good to start with that (if that is the classic IVC definition or explain how it is different if it isn’t).
> 
> 1. Do we need anything on the risc0 side to use it?
> 2. Does risc0 zkvm already support it or do we need to enable it ourselves?
> 3. Can you specify what we need to use on risc0 side and what to implement additionally to enable aggregated proofs, at least in broad terms?

I’d say the idea is to use PCD, which generalizes IVC, and committed relations. Thus, no need to do sequential aggregation (see parallel proving and the last diagram), and commit (hash) to keep track of what has been verified. Comitting also has the advantage that the size of the aggregated instance will be constant, so the verifier runtime will not depend on how many instances where aggregated/verified incrementally.

As for RISC0, next step is to assess its feasibility. We basically need the ability to pass the program image ID as input to the guest program. And for non-uniform aggregation, different ones at each step. I’m working on this now.

> [@vveiln](#):
>
> Perhaps including the relevant links to risc0 recursion (if needed), IVC definition we are referring to, and any other sources you used would be helpful

If you are curious you can read about PCDs [here](https://eprint.iacr.org/2014/595) and [here](https://eprint.iacr.org/2015/377). Proof recursion via succinct verifiers was established [here](https://eprint.iacr.org/2012/095.pdf). But not sure how much would help to understand the post. Below there is a list of articles on proof aggregation that I still need to go through. The most relevant seems to be Snarkfold. They are also taking the IVC-approach, but they are _folding_ (relaxed) R1CS instances of the verifier – I’m not sure we can do that in RISC0.

- Snarkpack [https://eprint.iacr.org/2021/529.pdf](https://eprint.iacr.org/2021/529.pdf)

- Stackproofs [https://eprint.iacr.org/2024/1281.pdf](https://eprint.iacr.org/2024/1281.pdf)

- aplonk [aPlonK : Aggregated PlonK from Multi-Polynomial Commitment Schemes](https://eprint.iacr.org/2022/1352)

- → snarkfold [SnarkFold: Efficient Proof Aggregation from Incrementally Verifiable Computation and Applications](https://eprint.iacr.org/2023/1946)

- → unifold [UniPlonk: Plonk with Universal Verifier](https://eprint.iacr.org/2023/869)

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [June 26, 2025, 1:35pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/4 "2025-06-26T13:35:55Z")

</div>

> [@kike](#):
>
> To be able to recurse by _verifying_ proofs. Succinct verification is a well-known property, but not all the schemes have it

I understand. I’m asking for a source with a formal definition of the property.

> [@kike](#):
>
> Which ones are unclear to you? I included pictures with the hope things will be clearer.

It would be helpful to see the description of inputs right next to the function that takes the inputs so that I don’t have to look in the rest of the document to remember what letter corresponds to what value. For example,

> [@kike](#):
>
> P\_{aa}(p^{in},h^{in},π^{in},x\_{ac},π\_{ac})→(p^{out},h^{out})

is difficult to read because I have to remember what all these variables are. It would be helpful to have them defined right above.

#### Regarding verification question:

So in resource plasma it is gonna roughly work as follows:  
the user and the solver create individual proofs, then the solver/controller aggregate the proofs into one RM proof. This aggregated proof is verified on the Anoma contract (if it is inside the executor proof or not doesn’t matter here).

Let’s ignore the details on how the RM proofs are generated and imagine we have a single function `RM.prove(...)` that outputs a transaction with all the proofs required. We would like to have aggregation interface that takes the transaction / RM proofs as inputs and outputs the transaction and/or the aggregated proofs, something like:  
`Aggregator.aggregate: Tx -> [AggregatedProof; n]`

(Here for generality we output not a single proof but `n` proofs where `n` is constant)

On the Ethereum side, we want to be able to verify the aggregated proof, e.g.:  
`Aggregator.verify: [AggregatedProof; n] -> ... -> Bool`

I think it would be helpful to specify:

- what the aggregate function takes and what it outputs
- what the verify function takes as input
- what other functions `Aggregator` (the name can change) exposes in the API
- what steps these functions perform

---

<div class="post-metadata">

**Author:** ![kike](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/kike/32/745_2.png) [@kike](https://forum.anoma.net/u/kike)\
**Post date:** [June 26, 2025, 3:19pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/5 "2025-06-26T15:19:23Z")

</div>

> [@vveiln](#):
>
> I understand. I’m asking for a source with a formal definition of the property.

> [@kike](#):
>
> Proof recursion via succinct verifiers was established [here](https://eprint.iacr.org/2012/095.pdf).

> [@vveiln](#):
>
> It would be helpful to see the description of inputs right next to the function that takes the inputs so that I don’t have to look in the rest of the document to remember what letter corresponds to what value. For example,
> 
> > [@kike](#):
> >
> > P\_{aa}(p^{in},h^{in},π^{in},x\_{ac},π\_{ac})→(p^{out},h^{out})
> 
> is difficult to read because I have to remember what all these variables are. It would be helpful to have them defined right above.

But I think I defined and described everything in text surrounding the pseudocode. The paragraph just above it describes the algorithm:

> [@kike](#):
>
> In the simplest case, all proofs are for the same program. Let us take as example the compliance logic (program) \mathsf P\_{c}(w\_c) \rightarrow x\_c run over compliance units. The exact structure of the witness w\_c, instance x\_c , and description of \mathsf P\_{c} is unimportant for the purposes of aggregation. We only care about the existence of a SNARK with succinct verification \mathbf{V}:
> 
> \mathbf{V}(\mathsf p\_{c},x\_c,\pi\_c) =1 \text{ if } \exists\ w\_c\text{ s.t. } \mathsf P\_{c}(w\_c) = x\_c
> 
> We aggregate compliance proofs one step at a time. At each step, a fresh output x\_c of the compliance program is verified using proof \pi\_c, and accumulated in a chaining hash h, (the bytes of x\_c are hashed). Also, the previous aggregation is verified. In pseudocode:
> 
> > \mathsf P\_{ac}(\mathsf p^{in},h^{in},\pi^{in},x\_c,\pi\_c)\rightarrow (\mathsf p^{out},h^{out}):
> > 
> > 1. Check 1 = \mathbf V (\mathsf p\_{c},x\_c,\pi\_c) // the description of the compliance program \mathsf P\_{c} is hard-coded in \mathsf P\_{ac}
> > 2. If h^{in}\neq h\_0, check 1 = \mathbf V (\mathsf p^{in},h^{in},\pi^{in})
> > 3. Output h^{out} := Hash(x\_{c},h^{in}) and \mathsf p^{out}:=\mathsf p^{in}
> 
> The aggregation program takes as input its own description \mathsf p^{in} := \mathsf p\_{ac}. This just means that it verifies an execution of itself for a previous chained hash h^{in}. In other words, the aggregation is an incrementally verifiable computation (IVC).

I am not sure if you want more clarifications for better understanding, or because you want a place where everything is explained nicely and clearer. This post was conceived to just transmit the idea – it as an sketch to quickly share the key points, don’t take it as definite. If we are happy with the approach, I will write up the proposal more precisely. I’m still unsure whether you and @xuyang are happy with it or want to explore other non-IVC based possibilities. IMO:

**pros**

- Aggregation can be paused and resumed by different parties → can aggregate in scope
- individual proofs can be removed as soon as they are aggregated
- tree-like provers: can utilize all the nodes of the tree, not just the leaves – yields less recursion overhead in general

**cons**

- recursion overhead at each node might bee expensive
- unclear whether can unleash full advantage of risc0. Ideally, I’d like to use the [recursion](https://docs.rs/risc0-zkvm/2.1.0/risc0_zkvm/recursion/index.html) module for the aggregation programs because the AIR being proved is optimized for STARK verifiers, which is what aggregation mainly do.

> [@vveiln](#):
>
> `Aggregator.aggregate: Tx -> [AggregatedProof; n]`
> 
> (Here for generality we output not a single proof but `n` proofs where `n` is constant)
> 
> On the Ethereum side, we want to be able to verify the aggregated proof, e.g.:  
> `Aggregator.verify: [AggregatedProof; n] -> ... -> Bool`
> 
> I think it would be helpful to specify:
> 
> - what the aggregate function takes and what it outputs
> - what the verify function takes as input
> - what other functions `Aggregator` (the name can change) exposes in the API
> - what steps these functions perform

Yes, all this need to be specified. I would distinguish at least two scopes: action and transaction, and two aggregations strategies: sequential and tree-like. I first want to integrate the PoC in the arm-risc0 codebase and see how it plays out.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [June 26, 2025, 4:19pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/6 "2025-06-26T16:19:06Z")

</div>

> [@kike](#):
>
> I am not sure if you want more clarifications for better understanding, or because you want a place where everything is explained nicely and clearer. This post was conceived to just transmit the idea – it as an sketch to quickly share the key points, don’t take it as definite.

The former. It’s a bit challenging to fully evaluate the proposal without the RM context. Including some sketches for `aggregate` and `verify`, along with more detailed pseudocode that explicitly defines the inputs, would help clarify how the proposed proof aggregation scheme fits in the whole model

---

<div class="post-metadata">

**Author:** ![kike](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/kike/32/745_2.png) [@kike](https://forum.anoma.net/u/kike)\
**Post date:** [June 27, 2025, 1:10pm UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/7 "2025-06-27T13:10:17Z")

</div>

Here there is a bit more of detail. Hope it helps.

### Aggregating proofs inside actions

Let n\_c be the number of compliance units in the action. Let n\_r be the total number of resources (consumed and created) in the action.

There are n\_c compliance proofs, and n\_r logic proofs in the action.

**Aggregate compliance and logic proofs:**

- Inputs:

- Output:

**Steps** :

1. Set the initial aggregated instance to two zero-bytes arrays h\_0,d\_0, and the initial aggregated proof to a dummy value \pi\_{a,0}.

2. Let avk the verifying key of the universal aggregator program/circuit \mathsf{P}\_{ua}. (See first post.)

3. For j \in 1,\ldots n\_c: // First aggregate the compliance proofs

4. Reset h\_0 = h\_{n\_{c}}, d\_0 = d\_{n\_{c}}, \pi\_{a,0}= \pi\_{a,n\_c}

5. For j \in 1,\ldots, n\_r: // Now aggregate the logic proofs

6. Output \pi\_{a,{n\_c+n\_r}}

**Verify aggregation of compliance and logic proofs:**

- Inputs:
  - cvk: The verifying key of the compliance circuit.
  - (cst\_{j})\_{j\in \leq n\_c}: The n\_c instances of the compliance circuit.
  - (lvk\_j,lst\_{j})\_{j\leq n\_r}: The n\_r verifying keys and instances of the resource logic circuits.
  - \pi\_a: The aggregated proof for the action.

- Output: b\in\{true,false\}

**Steps**

1. Derive the action instance from compliance and logic instances of the action:

2. Output verify(avk,ast,\pi\_a)

### Aggregate proofs in transactions (aggregate all compliance and logic proofs)

The same way as aggregating/verifying them within actions (see above). One first collects compliance and logic instances and proofs from all the actions in the transaction.

### Aggregate proofs in transactions (aggregate action proofs)

This assumes actions come with their compliance and logic proofs already aggregated. Let n\_a be the number of actions in transaction T. There are n\_a action proofs generated as explained above.

**Aggregate actions proofs:**

- Inputs:

- Output:

**Steps** :

1. Set the initial aggregated instance to two zero-bytes arrays h\_0,d\_0, and the initial aggregated proof to a dummy value \pi\_{t,0}.

2. Let avk the verifying key of the universal aggregator program/circuit \mathsf{P}\_{ua}. (See first post.)

3. For j \in 1,\ldots n\_a:

4. Output \pi\_{t,{n\_a}}

**Verify aggregation of action proofs**

- Inputs:
  - avk: The verifying key of the compliance circuit.
  - (ast\_{j})\_{j\in \leq n\_a}: The n\_a action instances of the transaction.
  - \pi\_t: The aggregated proof for the action.

- Output: b\in\{true,false\}

**Steps**

1. Derive the transaction instance:

2. Output verify(avk,tst,\pi\_t)

### Parallelizing provers

The universal aggregator program \mathsf{P}\_{ua} can be modified so it accepts as input 2 aggregated instances and proofs (instead of one).  
To aggregate a total of N = \sum\_{l=0}^d n/{2^l} proofs, the N incremental proofs produced by the prover can be arranged into d layers. In the l-th layer, n/{2^l} proofs are generated in parallel and fed as input to the next layer.

**Instance generation.** The chained hashes h\_j,d\_j are computed accordingly: use the two input pair of hashes at each incremental step.

### Mixing aggregation strategies

Sequential and parallel provers via binary tree transcripts are two examples of aggregation strategies. Most likely the ones we will want to use the most (sequential for few aggregations, parallel for many aggregations).

Each transaction (or each action within a transaction) can aggregate with their own strategy. Aggregating two proofs resulting from different strategies is possible.

---

<div class="post-metadata">

**Author:** ![vveiln](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/vveiln/32/60_2.png) [@vveiln](https://forum.anoma.net/u/vveiln)\
**Post date:** [July 2, 2025, 7:40am UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/8 "2025-07-02T07:40:01Z")

</div>

Thank you, this is very helpful! A couple of thoughts:

1. This IVC-style approach is strictly sequential and processes one proof at a time, which means the only way to parallelise it, as far as I can see, is to make the sequences shorter and then aggregate the aggregated proofs sequentially. I wonder if there are approaches that can take, for example, two proofs as input and aggregate them into one, so that instead `(old_aggregated_proof, incoming_proof) -> new_aggregated_proof` we can get something like `incoming_proof_1, incoming_proof_2 -> aggregated_proof_12`
2. Could it make sense to focus on vk-based domain separation, i.e., we aggregate proofs with the same vk first and then aggregate the resulting proofs? Do you think it can have some benefits, e.g., could be faster?

> [@kike](#):
>
> For j \in 1,\ldots n\_c: // First aggregate the compliance proofs
> 
> 1. Compute h\_j = Hash(cst\_j,h\_{j-1})
> 2. Compute d\_j = Hash(cvk,d\_{j-1})
> 3. Set ast\_j = (avk,h\_j,d\_j) // The j-th aggregated action instance
> 4. Set aw\_j = (cvk,h\_{j-1},d\_{j-1},\pi\_{a,j-1},\pi\_{c,j}) // The j-th aggregated action witness
> 5. Compute \pi\_{a,j} = prove(\mathsf{P}\_{ua},ast\_j,aw\_j) // The j-th aggregated action proof.

1. The compliance verifying key doesn’t change. What is the value of recomputing d\_j at each step? Is it just for the circuit generality?
2. What are the constraints of the aggregation circuit?

---

<div class="post-metadata">

**Author:** ![kike](https://dub1.discourse-cdn.com/flex013/user_avatar/forum.anoma.net/kike/32/745_2.png) [@kike](https://forum.anoma.net/u/kike)\
**Post date:** [July 2, 2025, 11:32am UTC](https://forum.anoma.net/t/recursive-proof-aggregation/1643/9 "2025-07-02T11:32:10Z")

</div>

> [@vveiln](#):
>
> This IVC-style approach is strictly sequential and processes one proof at a time, which means the only way to parallelise it, as far as I can see, is to make the sequences shorter and then aggregate the aggregated proofs sequentially. I wonder if there are approaches that can take, for example, two proofs as input and aggregate them into one, so that instead `(old_aggregated_proof, incoming_proof) -> new_aggregated_proof` we can get something like `incoming_proof_1, incoming_proof_2 -> aggregated_proof_12`

Tree-like transcripts are possible. (For an expanded answer, see [this part](https://forum.anoma.net/t/recursive-proof-aggregation/1643/7#p-6573-parallelizing-provers-4) and [this](https://forum.anoma.net/t/recursive-proof-aggregation/1643#p-6413-parallel-proving-5).)

With the PCD approach, each node of the tree verifies an instance of the transaction (see the last picture in the first post). Compare this with e.g. the way [recursion is implemented in RISC-0](https://dev.risczero.com/api/recursion#recursive-proving-process), where the instances to verify are place in the leaves of the tree. Proofs in leaves yields trees with more nodes – more recursion overhead.

> [@vveiln](#):
>
> Could it make sense to focus on vk-based domain separation, i.e., we aggregate proofs with the same vk first and then aggregate the resulting proofs? Do you think it can have some benefits, e.g., could be faster?

Hmm, maybe. I’m not sure. Perhaps can avoid hashing the verifying key while going through instances for the same key, and simply pass it from input to output. This adds complexity (in coding). It would be good to give it some thinking, but I will wait to first get something prototyped.

> [@vveiln](#):
>
> The compliance verifying key doesn’t change. What is the value of recomputing d\_j at each step? Is it just for the circuit generality?

We need to keep track of the verifying keys each of the instances are verified against. Otherwise can verify against other (dummy) programs that are always satisfiable. [Here](https://forum.anoma.net/t/recursive-proof-aggregation/1643#p-6413-soundness-4) I elaborate a bit more about the soundness of the aggregation.

> [@vveiln](#):
>
> What are the constraints of the aggregation circuit?

The universal aggregation program. Specified [here](https://forum.anoma.net/t/recursive-proof-aggregation/1643#p-6413-non-uniform-aggregation-3): it verifies input aggregations, and the incremental instance.