$\newcommand{\adv}{\mathcal A}
\newcommand{\upa}{\mathcal U}
\newcommand{\app}{\mathcal D}
\newcommand{\vk}{\mathsf{vk}}
\newcommand{\inputs}{\mathsf{PI}}
\newcommand{\groth}{\mathsf{Groth16}}
\newcommand{\verify}{\mathsf{Verify}}
\newcommand{\cid}{\mathsf{cid}}
\newcommand{\pid}{\mathsf{pid}}
\newcommand{\cidtag}{\mathsf{tag}^{(cid)}}
\newcommand{\keccak}{\mathsf{Keccak}}
\newcommand{\poseidon}{\mathsf{Poseidon}}
\newcommand{\rel}{\mathcal{R}}
\newcommand{\lang}{\mathcal{L}}
\newcommand{\fd}{\mathsf{fd}}$

(Outline for now)

$\adv$ - Adversary
$\upa$ - UPA system
$\app$ - Application maintainer / developer
$N$ - Batch size (app proofs per aggregated batch)

## Soundness game

1. $\app$ creates a Groth16 circuit, described by the relation $\rel_\lang$ for language $\lang$, and submits the verification key $\vk$ to $\adv$.
2. All parties compute $\cid = \poseidon( \cidtag, \vk)$
3. $\adv$ submits verification keys $( vk_i )_{i=0}^{M}$ to $\upa$, where $\vk_k = \vk$ for some $k \in [M]$.
5. $\adv$ submits a sequence $( \pi_i, \inputs_i, \cid_i )_{i=0}^{mN-1}$ to $\upa$. We assume w.o.l.o.g. that $\groth.\verify( \pi_i, \inputs_i, \vk_i ) = 1$
6. All parties compute
$$\pid_i = \keccak( \cid_i, \inputs_i ) ~~ \text{for} ~~ i=0, \ldots, mN$$

4. $\upa$ returns a sequence $( \Pi_j, \fd_j )_{j=0}^{m-1}$, where $\Pi_j$ is a valid proof of the statement:
> $\exists ( \pid'_i, \pi'_i, \inputs'_i, \vk'_i )_{i=0}^{N - 1}$ s.t.
> a) $fd_j = \keccak( (\pid'_i)_{i=0}^{N - 1} )$
> b) $\pid'_i = \keccak( \cid'_i, \inputs'_i )$ for $i=0, \ldots, N-1$
> c) $\cid'_i = \poseidon( \cidtag, \vk'_i)$ for $i=0, \ldots, N-1$
> d) $\groth.\verify( \pi'_i, \inputs'_i, \vk'_i ) = 1$ for $i=0, \ldots, N-1$
>
and satisfies: $\fd_j = \keccak \left[ ( \pid_i )_{i=jN}^{(j+1)N - 1} \right]$
1. $\adv$ returns $\inputs''$
2. $\adv$ wins if:
1. $\pid'' \in \{ \pid_i \}_{i=0}^{mN-1}$ for $\pid'' = \keccak(\vk, \inputs'')$, AND
2. $\inputs'' \notin \lang$

## Soundness proof sketch

We need to show that $\adv$ has negligible probability of winning.

Let $i$ be s.t. $\pid'' = \pid_i$, and $j$ s.t. $jN \leq i < (j+1)N$.

Then
$$
\fd_j = \keccak \left[ \pid_{jN}, \ldots, \pid_i, \ldots, \pid_{(j+1)N - 1} \right]
$$
and (by the statement of $\Pi_j$)
$$
\fd_j = \keccak \left[ \pid'_{0}, \ldots, \pid_i, \ldots, \pid'_{N - 1} \right]
$$

e.w.n.p.
$$
\pid'' = \pid'_k = \keccak(\cid'_k , PI'_k )
$$
(for $k = i - jN$ being the appropriate index in the statement for $\Pi_j$).

Since (by condition 1) $\pid''$ also satisfies
$$\pid'' = \keccak( \cid, \inputs'' )$$
we have that, e.w.n.p,
$$
\cid'_k = \cid
$$
and
$$
\inputs'_k = \inputs''
$$

Since
$$
\cid'_k = \poseidon( \cidtag, \vk'_k ) = \poseidon( \cidtag, \vk ) ~~ \Bigl( = \cid\Bigr)
$$
e.w.n.p. we have
$$\vk'_k = \vk$$

By (d) in the statement of $\Pi_j$, we have that e.w.n.p. $\exists \pi'_k$ s.t.

$$
\groth.\verify( \pi'_k, \inputs'', \vk) = \groth.\verify( \pi'_k, \inputs'_k, \vk'_k) = 1
$$

therefore e.w.n.p. $\inputs'' \in \lang$.