A suggested aggregation interface

RM/AVM Proof aggregation
1

Compliance and logic relations

For a program[1] \mathsf P, let the image set

\mathcal L_{\mathsf P} := \{u\ |\ \exists w\text{ s.t. } \mathsf P (w)=u\}.

In the context of the resource machine, this captures both, compliance statements ``u\in\mathcal L_c" and resource logic statements ``u\in\mathcal L_l".

The aggregated relation

\mathcal L_\mathsf P is actually the induced language of the NP relation \mathcal R_\mathsf P := \{(u;w)\ |\ \mathsf P (w)=u\}. Statements can be proved with a preprocessing SNARK (setup,prove,verify):

setup(\mathsf P)\to (pk_\mathsf P,vk_\mathsf P) produces a pair of proving and verifying keys for a given program (and implicit security parameter --input omitted).

prove(pk_\mathsf P, u,w)\to \pi produces a proof for instance/witness pairs in \mathcal R_{\mathsf P}.

verify(vk_\mathsf P,u,\pi)\to \{true,false\} accepts the proof only if u\in\mathcal L_\mathsf P (with high probability in the security parameter).

Note: For the RISC0 RM, the proof system is STARK, and verifying keys are the digest of the executed RISC-V program (the so-called image id).

For the following aggregation program

\mathsf P_a (\{vk_i,u_i,\pi_i\}_{i=1}^n) = \begin{cases} \bot \text{ if } verify(vk_i,u_i,\pi_i) = false \text{ for some } i\\ h=commit(u_1,\ldots,u_n), d:=commit(vk_1,\ldots,vk_n) \text{ otherwise (if all proofs are valid)} \end{cases}

where commit is a binding commitment function[2], we define the correct aggregation relation as

\mathcal R_a := \left\{(u:= (h,d,n);w:=(\{vk_i,u_i,\pi_i\}_{i=1}^n))\ |\ \mathsf P_a (w) = u\right\}

Note that n is part of the aggregated instance u. That is, the relation does not fix the number of aggregated base instances u_i. We want to be able to aggregate variable-length batches.

Correct aggregation SNARK. This post discusses a space-efficient proving strategy based in proof-carrying-data (PCD), where instance verification and generation of commitments h,d is done incrementally, using the same SNARK as for the compliance and logic programs. Let’s denote with pk_{ag},vk_{ag} the pair of proving/verifying aggregation keys output by the SNARK setup:

setup(\mathsf P_{ag})\to (pk_{ag},vk_{ag})

Instance reduction. To generate the aggregated instance u we need the base instances u_i, the base verifying keys vk_i, and the function commit.

The aggregation interface

The suggestion (based in the above discussion) is to spec up the following algorithms for aggregation.

Minimal interface

  • to\_transaction\_instance(Transaction)\to u_{tx} =(h_{tx},d_{tx},n). Computes commitments of compliance and logic instances/verifying keys of a transaction. There are n_{tx} total instances in the transaction. This algorithm is used as a subroutine in the next two.

  • aggregate\_transaction(pk_{ag},Transaction)\to \pi_{tx}. Produces a single aggregated proof attesting to the validity of all compliance and logic proofs of the transaction.

  • verify\_transaction\_proof(vk_{ag},Transaction,\pi_{tx})\to b\in\{true,false\}. Accepts or rejects the proof of a transaction.

Note: The minimal interface does not change existing types, nor adds new ones. It would be possible to remove all compliance and logic proofs from a transaction, yielding a CompactTransaction with a single proof: the transaction proof \pi_{tx} (which could be passed to proof verification).

Extended interface

The next algorithms are optional, but nice to have. The observation is that once an aggregated proof \pi_{ag} = prove(pk_{ag},u_{ag},w_{ag}) is produced, it can be passed as a base instance in a subsequent batch for further aggregation (by a different actor). This allows to aggregate proofs of actions.

The extended interface is defined over CompactActions, which have a single (action) proof \pi_{a}, and its (action) aggregation key vk_{a}, and over CombinedTransaction, which are form by compact actions.

Action scope:

  • to\_action\_instance(Action)\to u_a:=(h_a,d_a,n_a). Computes commitments of compliance and logic instances/verifying keys of an action. There are n_a total instances in the action.

  • aggregate\_action(pk_{ag},Action)\to (\pi_{a},CompactAction). Produces a single aggregated proof attesting to the validity of all compliance and logic proofs of the action.

  • verify\_action\_proof(vk_{ag},CompactAction,\pi_{a})\to b\in\{true,false\}. Accepts or rejects the proof.

Transaction scope:

  • to\_combined\_instance(CombinedTransaction)\to u_{ctx}:=(h_{ctx},d_{ctx},n_{ca}). Computes commitments of action instances and action verifying keys of a combined transaction. There are n_{ctx} action instances.

  • aggregate\_transaction(pk_{ag},CombinedTransaction)\to (\pi_{ctx},CompactTransaction). Produces a single aggregated proof attesting to the validity of all action proofs of the combined transaction.

  • verify\_compact\_transaction\_proof(vk_{ag},CompactTransaction,\pi_{ctx})\to b\in\{true,false\}. Accepts or rejects the proof.

  1. By program I mean an efficiently-computable function. ↩︎

  2. We can use a collision-resistant hash function if we are willing to see it as a random oracle. ↩︎

1 Like
2

Thanks for the write up! It generally looks good to me. A couple of comments:

  1. What would be a situation when the prover wants to prove actions first and then aggregate the proofs together?
  2. I would suggest to rename things like to_transaction_instance and verify_transaction_proof to to_aggregated_instance and verify_aggregated_proof respectively and adjust names to align with that so that we can tell if the function is relevant to snark proof aggregation or other proving/verification
3

The users can provide a single proof for their actions in their unbalanced transaction. Solvers, after matching, can generate the transaction proof by aggregating the action proofs.

It can be useful to reduce communication complexity (and intent pool size). Also, you can also see it as distributing the aggregation across different untrusted parties (a solver that assembles large number of actions in a tx might benefit from this).

Fine with me. If it is decided to not aggregate in scopes, then there is no ambiguity: i.e. an aggregation will always mean aggregate in a transaction.

1 Like