proofs/streaming-tail-latency/proof.tex

\documentclass[11pt,a4paper]{article}

\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amssymb,amsthm}
\usepackage{hyperref}
\usepackage{enumitem}

\hypersetup{colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{assumption}[theorem]{Assumption}

\title{Formal Analysis of ZAP-WS Per-Stream Independence:\\
Tail-Latency Independence and Throughput Composition}

\author{ZAP Protocol Authors\\
\texttt{zap-proto.io}}

\date{2026}

\begin{document}
\maketitle

\begin{abstract}
We formalize the per-stream independence claim of ZAP-WS. Under a
standard packet-erasure channel model, we prove (Theorem 1) that the
arrival-time distribution of any frame on stream $s_i$ is statistically
independent of the existence of, or losses affecting, frames on stream
$s_j$ for $j \ne i$. We prove (Theorem 2) that aggregate throughput
across $N$ streams is bounded by the underlying link capacity but is
otherwise independent of stream count, modulo per-stream framing
overhead. We prove (Lemma) the standard Reed--Solomon FEC overhead
bound: a $(k+m, k)$ code recovers from up to $m$ erasures with bandwidth
overhead exactly $m/k$. The proofs are constructive enough to guide a
conformant implementation.
\end{abstract}

\section{Model}

\subsection{Connections, packets, streams}

A ZAP-WS connection $C$ runs between two peers over an erasure-channel
substrate (UDP, raw IP, etc.). The connection carries a sequence of
\emph{packets} $\pi_1, \pi_2, \ldots$ Each packet is transmitted as a
single substrate datagram and either arrives intact or is lost. Each
packet contains one or more \emph{frames}, each frame belonging to
exactly one of $N$ logical \emph{streams} $s_1, \ldots, s_N$.

\begin{assumption}[Bernoulli erasure]\label{ass:erasure}
Each transmitted packet is independently lost with probability $p$
($0 \le p < 1$) and otherwise arrives after a propagation delay $D$.
Different packets are lost independently.
\end{assumption}

\begin{assumption}[Single-stream packing]\label{ass:packing}
Each packet contains frames belonging to a single stream. (This
assumption strengthens the claim. A weaker, multi-stream-per-packet
model and its consequences are discussed in Section~\ref{sec:packing}.)
\end{assumption}

\begin{assumption}[Independent recovery]\label{ass:recovery}
Each stream uses either independent retransmission with one round-trip
recovery delay $R$, or independent $(k, m)$ Reed--Solomon FEC. The
recovery decision and parameters for stream $s_i$ are made without
reference to any other stream.
\end{assumption}

\subsection{Latency random variable}

For frame $f$ of stream $s_i$, let
\[
L(s_i, f) := T_{\text{deliver}}(s_i, f) - T_{\text{send}}(s_i, f)
\]
be the application-to-application latency. We are interested in the
distribution of $L(s_i, f)$ and how it depends on traffic on other
streams.

\section{Theorem 1: Tail-Latency Independence}

\begin{theorem}[Tail-Latency Independence]\label{thm:independence}
Under Assumptions~\ref{ass:erasure}--\ref{ass:recovery}, for any two
distinct streams $s_i \ne s_j$ on the same ZAP-WS connection, any frame
$f$ on $s_i$, and any threshold $t \ge 0$,
\[
\Pr\!\bigl[L(s_i, f) > t \,\big|\, \mathcal{F}_j\bigr]
= \Pr\!\bigl[L(s_i, f) > t\bigr],
\]
where $\mathcal{F}_j$ is the $\sigma$-algebra generated by all events
(send, loss, recovery) on stream $s_j$.
\end{theorem}

\begin{proof}
We show that $L(s_i, f)$ depends only on the substrate-level packet
events affecting frame $f$, which are independent of substrate-level
events on packets carrying $s_j$ frames.

\paragraph{Step 1: $L(s_i, f)$ as a function of $s_i$ packet events.}
By Assumption~\ref{ass:packing}, every packet that carries any byte of
frame $f$ carries only $s_i$ data. Let $\Pi_i(f) \subseteq \{\pi_1,
\pi_2, \ldots\}$ be the (finite) set of substrate packets that contain
either $f$'s bytes or $s_i$'s FEC parity for $f$'s FEC group, or any
$s_i$ retransmission packet covering $f$. The arrival event of $f$ at
the application is determined by:
\begin{enumerate}[label=(\alph*)]
\item Which packets in $\Pi_i(f)$ are lost (Bernoulli, by
Assumption~\ref{ass:erasure}).
\item Whether any subset of size $\ge k$ of the FEC group survives, if
FEC is used (deterministic given losses).
\item Otherwise, retransmission timing for the lost subset
(deterministic given the recovery rule of Assumption~\ref{ass:recovery},
which references only $s_i$).
\end{enumerate}
Hence $L(s_i, f)$ is a measurable function of the joint loss outcome on
$\Pi_i(f)$ alone.

\paragraph{Step 2: $\Pi_i(f) \cap \Pi_j(\cdot) = \emptyset$.}
For any frame $g$ on $s_j$, let $\Pi_j(g)$ be the analogously defined
packet set. By Assumption~\ref{ass:packing}, packets in $\Pi_i(\cdot)$
contain only $s_i$ frames and packets in $\Pi_j(\cdot)$ contain only
$s_j$ frames; since each substrate packet is generated as a single
ZAP-WS frame plus header, the packet sets are disjoint.

\paragraph{Step 3: Independence of disjoint Bernoulli events.}
By Assumption~\ref{ass:erasure}, the loss outcomes on disjoint sets of
packets are independent. Therefore the loss outcome on $\Pi_i(f)$ is
independent of the loss outcomes on every $\Pi_j(g)$, and hence
independent of $\mathcal{F}_j$.

\paragraph{Step 4: Conclude.}
By Step 1, $L(s_i, f)$ is a function of a random variable independent
of $\mathcal{F}_j$. Hence
\[
\Pr[L(s_i, f) > t \mid \mathcal{F}_j] = \Pr[L(s_i, f) > t]. \qedhere
\]
\end{proof}

\begin{corollary}[No HoL blocking]
For ZAP-WS, an arbitrarily long stall on stream $s_j$ cannot increase
the tail latency $\Pr[L(s_i, f) > t]$ for any frame on stream $s_i$.
\end{corollary}

\paragraph{Contrast with TCP-multiplexed protocols.} For WebSocket and
HTTP/2, the analogue of $\Pi_i(f)$ contains every TCP segment whose
sequence numbers precede $f$'s last byte in the TCP byte stream,
including segments carrying $s_j$ frames. Thus
$\Pi_i(f) \cap \Pi_j(\cdot) \ne \emptyset$ in general, Step 2 fails,
and conditional independence does not hold.

\section{Theorem 2: Throughput Composition}

\begin{theorem}[Throughput Composition]\label{thm:throughput}
Let $\Theta_i$ be the long-run achieved throughput of stream $s_i$ under
saturating offered load and infinite per-stream window. Under
Assumptions~\ref{ass:erasure}--\ref{ass:recovery}, for any partition of
$\{1, \ldots, N\}$,
\[
\sum_{i=1}^N \Theta_i \;\le\; B \cdot (1 - p) - O_h(N),
\]
where $B$ is the link capacity, $p$ is the packet loss probability, and
$O_h(N) = N \cdot \omega$ for a per-stream framing overhead $\omega$
(headers plus FEC parity in the FEC mode). Furthermore, the achievable
$(\Theta_1, \ldots, \Theta_N)$ region is convex and the per-stream
throughput $\Theta_i$ depends on other streams \emph{only} through the
shared capacity constraint.
\end{theorem}

\begin{proof}[Proof sketch]
The substrate is a single physical link of capacity $B$. Each packet
either carries a stream's payload (counts toward that stream's
throughput) or the framing/FEC overhead. Per-stream framing overhead
$\omega$ is additive in $N$ because each stream contributes a constant
header rate. Conservation of bandwidth gives the upper bound. The
achievable region is convex by time-sharing arguments standard in
network capacity analysis. Per-stream loss recovery
(Assumption~\ref{ass:recovery}) implies $\Theta_i$'s loss-recovery
dynamics depend only on $s_i$'s own losses; hence apart from sharing
$B$, the streams are decoupled.
\end{proof}

\begin{corollary}
Doubling the number of streams (with fixed aggregate offered load) does
not change tail latency on any individual stream
(Theorem~\ref{thm:independence}) and reduces aggregate goodput only by
$\omega$ per added stream.
\end{corollary}

\section{Lemma: Reed--Solomon FEC Overhead Bound}

\begin{lemma}[FEC overhead bound]\label{lem:fec}
Let a stream use a systematic $(k+m, k)$ Reed--Solomon code over
$\mathrm{GF}(2^q)$, $q \ge \lceil \log_2(k+m) \rceil$, applied per FEC
group of $k$ data frames. Then:
\begin{enumerate}[label=(\roman*)]
\item Any subset of $k$ of the $k+m$ transmitted frames is sufficient
to reconstruct the $k$ original data frames.
\item The bandwidth overhead of FEC is exactly $m/k$.
\end{enumerate}
\end{lemma}

\begin{proof}
\textbf{(i)} A Reed--Solomon code is a maximum-distance separable (MDS)
code: its minimum distance is $m+1$ and any $k$ symbols of the
codeword uniquely determine the message
\cite{reed1960}. Standard.

\textbf{(ii)} For each $k$ data frames the encoder emits $k+m$
codeword frames. The ratio of transmitted bytes to data bytes is
$(k+m)/k = 1 + m/k$, so the overhead above the data rate is $m/k$,
exactly. \qed
\end{proof}

\begin{corollary}[Recovery without retransmission]
With $(k, m)$ FEC and per-packet erasure probability $p$, the
probability that a FEC group fails to reconstruct (i.e., suffers $> m$
erasures out of $k+m$) is
\[
\Pr[\text{FEC fail}] = \sum_{j=m+1}^{k+m}
\binom{k+m}{j} p^j (1-p)^{k+m-j}.
\]
For $p$ small and $m$ chosen so that $(k+m) p < m$, this is exponentially
small in $m$ (Chernoff). Tuning $m$ thus exchanges bandwidth for tail
latency: each unit increase in $m$ exponentially reduces retransmission
probability and thereby reduces $\Pr[L(s_i, f) > D + R]$ exponentially.
\end{corollary}

\section{Multi-Stream-Per-Packet Packing}\label{sec:packing}

In practice, ZAP-WS implementations may pack frames from multiple
streams into a single substrate packet to amortize header overhead. We
quantify the cost.

\begin{proposition}[Soft HoL under co-packing]\label{prop:soft-hol}
Suppose with probability $\alpha$ a substrate packet carries frames from
two or more streams. Then the conditional independence statement of
Theorem~\ref{thm:independence} holds with conditional dependence
contribution at most $\alpha$. Specifically,
\[
\bigl| \Pr[L(s_i, f) > t \mid \mathcal{F}_j]
- \Pr[L(s_i, f) > t] \bigr| \le \alpha.
\]
\end{proposition}

\begin{proof}[Proof sketch]
The argument of Theorem 1 fails only on the event $E$ that a packet in
$\Pi_i(f)$ also belongs to $\Pi_j(\cdot)$ for some $j$. By construction
$\Pr[E] \le \alpha$. Outside $E$, the conditional probability equals
the unconditional one. By total probability the difference is bounded
by $\alpha$.
\end{proof}

\begin{corollary}
A conformant implementation that wishes to preserve the bound of
Theorem~\ref{thm:independence} exactly should refuse to pack frames from
multiple streams in one substrate packet, accepting the per-stream
header overhead. Implementations that prioritize throughput may set
$\alpha > 0$ but must document the resulting weakening.
\end{corollary}

\section{Liveness}

\begin{theorem}[Per-stream liveness]
Under Assumptions~\ref{ass:erasure}--\ref{ass:recovery}, suppose
stream $s_i$ has retransmission enabled with bounded RTO. Then for any
frame $f$ on $s_i$, $\Pr[L(s_i, f) < \infty] = 1$ regardless of the
behaviour of any other stream $s_j$, $j \ne i$.
\end{theorem}

\begin{proof}
Each retransmission of $f$ is an independent Bernoulli trial of success
probability $1-p > 0$. By Borel--Cantelli, infinitely many trials yield
a success almost surely, hence $f$ arrives in finite time a.s. The
behaviour of $s_j$ is irrelevant by the disjoint-packet-set argument of
Theorem~\ref{thm:independence}.
\end{proof}

\section{Discussion}

The proofs above identify three load-bearing assumptions:
\begin{enumerate}
\item \textbf{Erasure independence (Assumption~\ref{ass:erasure}).}
Real networks exhibit bursty loss; the i.i.d.\ assumption is a useful
first approximation but burstiness can correlate losses across streams
that share queues. This is a property of the network, not of ZAP-WS.
\item \textbf{Single-stream packing (Assumption~\ref{ass:packing}).}
The cleanest independence holds when each substrate packet belongs to a
single stream. Implementations may relax this for throughput;
Proposition~\ref{prop:soft-hol} bounds the cost.
\item \textbf{Independent recovery (Assumption~\ref{ass:recovery}).}
Per-stream loss detection and either per-stream retransmission or
per-stream FEC. This is exactly the design choice that distinguishes
QUIC and ZAP-WS from TCP.
\end{enumerate}

A stream substrate that violates any of these (e.g., a single shared
ARQ window across all streams, as in TCP) re-introduces head-of-line
blocking through the shared component.

\section{Conclusion}

Theorem~\ref{thm:independence} formalizes the core ZAP-WS claim:
per-stream tail latency is statistically independent of other streams.
Theorem~\ref{thm:throughput} establishes that throughput composes up to
shared link capacity. Lemma~\ref{lem:fec} bounds the FEC bandwidth cost
exactly. Together, these results justify the engineering claim that
ZAP-WS provides per-stream flow control with bounded, predictable tail
latency under loss, on top of post-quantum mutual authentication
inherited from the ZAP handshake.

\bibliographystyle{plain}
\begin{thebibliography}{9}
\bibitem{reed1960}
Irving S. Reed and Gustave Solomon.
\newblock Polynomial Codes Over Certain Finite Fields.
\newblock {\em Journal of SIAM}, 8(2):300--304, 1960.

\bibitem{rfc9000}
J. Iyengar and M. Thomson.
\newblock {QUIC}: A {UDP}-Based Multiplexed and Secure Transport.
\newblock RFC 9000, IETF, 2021.

\bibitem{rfc9114}
M. Bishop.
\newblock {HTTP/3}.
\newblock RFC 9114, IETF, 2022.
\end{thebibliography}

\end{document}