papers/dag-evm-formal/sections/04-dag-z-chain.tex

\section{DAG-Z-Chain}

\label{sec:dagzchain}
%% ============================================================================

The Z-Chain operates the classical ZK-UTXO model: each transaction reveals
a set of nullifiers (the anonymous counterparts of spent UTXOs), creates
new commitments, and carries a ZK proof (Groth16 or Plonk) that the
nullifier/commitment relationship is valid under a known verification
key. The Z-state is the pair $(\mathsf{spent}, \mathsf{committed})$ with
both components monotone (never shrink).

The conflict rule is dramatically simpler than in the EVM:
\[
\mathsf{conflicts}(v_1, v_2) \iff N(v_1) \cap N(v_2) \neq \emptyset
\]
where $N(v)$ is the union of nullifier sets across the transactions of $v$.

\begin{theorem}[Z-Chain No Double Spend, Lean: \texttt{no\_double\_spend}]
No nullifier appears in two distinct accepted vertices of the Z-Chain DAG.
\end{theorem}

\begin{theorem}[Batch Verification Soundness, axiom: \texttt{batch\_sound}]
Groth16 (and Plonk) batch verification is sound iff each constituent proof
is individually sound. GPU-accelerated batch verify preserves this property
under the pairing-based (resp.\ polynomial-commitment) assumption.
\end{theorem}

\begin{theorem}[FHE Commutativity, Lean: \texttt{fhe\_linearity\_preserved}]
If two Z-Chain vertices each perform an additive FHE balance update on
disjoint nullifier keys, the two updates commute.
\end{theorem}

These together give DAG-Z-Chain the same parallelism profile as DAG-EVM
while preserving all of the ZK-UTXO security invariants, \emph{without}
additional cryptographic assumptions beyond those already underlying the
proof system.

%% ============================================================================