proofs/fix-trading-channel/proof.tex

\documentclass[11pt,a4paper]{article}

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

\hypersetup{
  colorlinks=true,
  linkcolor=blue!50!black,
  urlcolor=blue!70!black
}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}

\title{ZAP-FIX Latency Model: Formal Bounds}
\author{ZAP Protocol Authors\\\texttt{zap-proto.io}}
\date{\today}

\begin{document}
\maketitle

\begin{abstract}
This document formalises the latency model claimed in the ZAP-FIX
paper. We give a per-message round-trip decomposition, derive a
steady-state per-message bound (Theorem~1), a session-resumption
bound (Theorem~2), and a sequence-determinism lemma. Concrete
numerical budgets are tabulated so that operators can calibrate the
model against their colocated environment.
\end{abstract}

\section{Notation and Model}
\label{sec:model}

\begin{definition}[Per-message round trip]
For two FIX peers $A$ and $B$ on the same session and a FIX
application message $M$ originating at $A$, the round-trip
latency $T_{\mathrm{rtt}}(M)$ is the wall-clock interval from the
moment $A$'s application layer hands $M$ to its FIX session library
to the moment $A$'s application layer observes the corresponding
acknowledgement message $M'$ (typically an
\texttt{ExecutionReport-New}~\texttt{(150=0)}) returned by $B$.
\end{definition}

We decompose
\begin{equation}
  T_{\mathrm{rtt}}(M)
   \;=\;
   T_{\mathrm{ser}}^A(M) + T_{\mathrm{tx}}^A(M)
   + T_{\mathrm{net}}^{AB}(M)
   + T_{\mathrm{rx}}^B(M) + T_{\mathrm{parse}}^B(M)
   + T_{\mathrm{app}}^B(M)
   + T_{\mathrm{rev}}^{BA}(M')
  \label{eq:budget}
\end{equation}
where the components are: serialisation
($T_{\mathrm{ser}}$); kernel transmit including NIC posting
($T_{\mathrm{tx}}$); on-wire and switch fabric ($T_{\mathrm{net}}$);
kernel receive including NIC delivery ($T_{\mathrm{rx}}$);
session-layer parse ($T_{\mathrm{parse}}$); application processing
including matching, risk, and acknowledgement formation
($T_{\mathrm{app}}$); and the symmetric reverse-path total
($T_{\mathrm{rev}}$).

\begin{definition}[Transport binding]
A \emph{transport binding} $\Pi$ for FIX is a triple
$(\sigma_\Pi, \pi_\Pi, \kappa_\Pi)$ where $\sigma_\Pi$ is a serialiser
$M \to \mathrm{bytes}$, $\pi_\Pi$ is the parser
$\mathrm{bytes} \to M$, and $\kappa_\Pi$ is the channel cost: a
function from message size to (kernel, NIC, fabric) cost.
\end{definition}

We compare $\Pi_{\mathrm{tls}}$ (TCP+TLS-FIX, SOH text body) with
$\Pi_{\mathrm{zap}}$ (ZAP-FIX, envelope; text or binary body
mode).

\section{Steady-State Per-Message Bound}
\label{sec:steady}

\begin{lemma}[Channel cost monotonicity]
\label{lem:channel}
For any reliable byte-oriented or frame-oriented channel and a
message of size $s$ bytes,
\[
  \kappa(s) \;=\; \kappa_0 + \kappa_1 \cdot s
\]
with $\kappa_0$ a per-message constant (kernel call, NIC doorbell,
fabric arbitration) and $\kappa_1$ a per-byte constant
(serialisation onto wire). Both are non-negative.
\end{lemma}

The lemma is standard; it captures the empirical observation that
for messages well under one MTU, $\kappa_0$ dominates $\kappa_1
\cdot s$. We use it only to argue monotonicity in $s$.

\begin{theorem}[Steady-state per-message latency]
\label{thm:steady}
Let $M$ be a FIX message exchanged in steady state (no handshake,
no resend). Let $s_\Pi(M) = |\sigma_\Pi(M)|$. Define
$\Delta_{\mathrm{ser}}(M) = T_{\mathrm{ser}}^{\Pi_{\mathrm{tls}}}(M)
- T_{\mathrm{ser}}^{\Pi_{\mathrm{zap}}}(M)$ and analogously
$\Delta_{\mathrm{parse}}(M)$. Then
\[
  T_{\mathrm{rtt}}^{\Pi_{\mathrm{zap}}}(M)
  \;\leq\;
  T_{\mathrm{rtt}}^{\Pi_{\mathrm{tls}}}(M)
  - \big(\Delta_{\mathrm{ser}}(M) + \Delta_{\mathrm{parse}}(M)\big)
  - \kappa_1 \cdot \big(s_{\Pi_{\mathrm{tls}}}(M)
                        - s_{\Pi_{\mathrm{zap}}}(M)\big).
\]
\end{theorem}

\begin{proof}
By Equation~\eqref{eq:budget}, the only components that differ
between $\Pi_{\mathrm{tls}}$ and $\Pi_{\mathrm{zap}}$ in steady
state are $T_{\mathrm{ser}}$, $T_{\mathrm{parse}}$, and the channel
contribution $T_{\mathrm{tx}} + T_{\mathrm{net}} + T_{\mathrm{rx}}$,
which by Lemma~\ref{lem:channel} differs by exactly $\kappa_1
\cdot \Delta s$, with $\Delta s =
s_{\Pi_{\mathrm{tls}}}(M) - s_{\Pi_{\mathrm{zap}}}(M)$. The
$\kappa_0$ contribution is identical because both bindings emit
exactly one message-bearing unit (one TLS record carrying one FIX
message versus one ZAP frame carrying one FIX message). Substituting
into~\eqref{eq:budget} yields the claim.
\end{proof}

\paragraph{Concrete numerical bound.}
Table~\ref{tab:bound} substitutes representative values for an
optimised colocated client. Values are in nanoseconds.

\begin{table}[h]
\centering
\begin{tabular}{lrrr}
\toprule
Component                                    & TCP+TLS-FIX & ZAP-FIX (text) & ZAP-FIX (binary) \\
\midrule
Serialise (\texttt{NewOrderSingle})         & 1500--3000 & 1600--3100 & 200--500 \\
Kernel transmit                              & 300--800   & 300--800   & 300--800 \\
Fabric one-way (1$\times$10G, 1 hop)         & 600--900   & 600--900   & 600--900 \\
Bytes on wire                                & 220        & 240        & 130 \\
Per-byte cost contribution                   & 35--90     & 38--96     & 21--52 \\
Kernel receive                               & 300--800   & 300--800   & 300--800 \\
Parse (SOH walk \emph{vs.}~envelope)         & 800--1500  & 100--250   & 50--150 \\
Application matching (typical)               & 5000--15000 & 5000--15000 & 5000--15000 \\
Reverse-path symmetric                       & $\approx$ above & $\approx$ above & $\approx$ above \\
\midrule
Total round trip $T_{\mathrm{rtt}}$          & 50000--200000 & 50000--200000 & 47000--195000 \\
\bottomrule
\end{tabular}
\caption{Indicative per-component latency budget (ns) for a
\texttt{NewOrderSingle}/\texttt{ExecutionReport-New} round trip.
The transport-attributable difference $\Delta_{\mathrm{ser}} +
\Delta_{\mathrm{parse}} + \kappa_1\Delta s$ is roughly
$1.5$--$3~\mu\mathrm{s}$ (text mode improvement on parse alone) and
roughly $3$--$8~\mu\mathrm{s}$ (binary mode), against a colocated
budget of $50$--$200~\mu\mathrm{s}$. In multi-hop or
non-colocated deployments the byte-count saving compounds.}
\label{tab:bound}
\end{table}

\section{Session-Resumption Bound}
\label{sec:resume}

We model session resumption as the wall-clock interval from the
moment a peer detects an unhealthy transport (TCP RST, missed
heartbeat, pod migration signal) to the moment the FIX session is
back in normal flow with no application-visible gap.

\begin{definition}[Resumption time]
$T_{\mathrm{resume}}^\Pi$ is the time from disconnection detection
$t_0$ to the moment $t_1$ at which both peers have re-established a
session and the in-flight gap (if any) has been closed by FIX
\texttt{ResendRequest}/\texttt{SequenceReset}.
\end{definition}

For TCP+TLS-FIX,
\begin{equation}
  T_{\mathrm{resume}}^{\Pi_{\mathrm{tls}}}
   \;=\;
   T_{\mathrm{tcp}} + T_{\mathrm{tls}} + T_{\mathrm{logon}}
   + T_{\mathrm{gapdetect}}^{\mathrm{stream}} + T_{\mathrm{resend}}
   + T_{\mathrm{backoff}}
  \label{eq:tls-resume}
\end{equation}
where $T_{\mathrm{tcp}}$ is one round trip plus possible retransmit
backoff after the loss event, $T_{\mathrm{tls}}$ is one round trip
for TLS~1.3 \texttt{1-RTT} (or \texttt{0-RTT} resumption with
replay-window risk), $T_{\mathrm{gapdetect}}^{\mathrm{stream}}$ is
the cost of byte-stream scanning to locate FIX message boundaries,
and $T_{\mathrm{backoff}}$ accumulates middle-box and retry
backoffs.

For ZAP-FIX,
\begin{equation}
  T_{\mathrm{resume}}^{\Pi_{\mathrm{zap}}}
   \;=\;
   T_{\mathrm{zap}} + T_{\mathrm{logon}}
   + T_{\mathrm{gapdetect}}^{\mathrm{frame}} + T_{\mathrm{resend}}
  \label{eq:zap-resume}
\end{equation}
where $T_{\mathrm{zap}}$ is the single-RTT ZAP handshake (with
post-quantum hybrid KEM) and
$T_{\mathrm{gapdetect}}^{\mathrm{frame}} = O(1)$ because the next
envelope header carries the next \texttt{MsgSeqNum} explicitly.

\begin{theorem}[Session-resumption bound]
\label{thm:resume}
There exist $C_1, C_2 > 0$, dependent only on the deployed
colocation environment, such that
\[
  T_{\mathrm{resume}}^{\Pi_{\mathrm{zap}}}
   \;\leq\;
   T_{\mathrm{rtt-net}} + T_{\mathrm{logon}}
   + C_1 + C_2 \cdot N_{\mathrm{gap}}
\]
where $T_{\mathrm{rtt-net}}$ is one network round trip and
$N_{\mathrm{gap}}$ is the number of FIX messages in the gap.
By contrast,
\[
  T_{\mathrm{resume}}^{\Pi_{\mathrm{tls}}}
   \;\geq\;
   2 \cdot T_{\mathrm{rtt-net}} + T_{\mathrm{logon}}
   + C_1' + C_2' \cdot N_{\mathrm{gap}}
   + T_{\mathrm{backoff}}
\]
with $C_1' \geq C_1$ and $C_2' \geq C_2$, and $T_{\mathrm{backoff}}$
non-negative.
\end{theorem}

\begin{proof}
The ZAP bound follows from~\eqref{eq:zap-resume}: $T_{\mathrm{zap}}$
contributes one round trip; gap detection is $O(1)$ per missed
message because each frame's envelope header is independently
addressable (set $C_1$ to cover the constant per-frame cost and
$C_2$ to cover the per-resent-message cost). The TLS bound
follows from~\eqref{eq:tls-resume}: TCP and TLS each contribute one
round trip; byte-stream scanning costs at least the per-frame cost
of ZAP and typically more because boundary detection requires
parsing each message's length-or-checksum field; $T_{\mathrm{backoff}}$
is non-negative and is incurred whenever the disconnect cause is
loss-driven rather than peer-initiated.
\end{proof}

\paragraph{Corollary.}
For pod-migration scenarios common in containerised venue
infrastructure, where a TCP connection is unavoidably terminated
even when both endpoints survive, ZAP-FIX recovers in approximately
$T_{\mathrm{rtt-net}} + T_{\mathrm{logon}}$, which on a
$1~\mathrm{ms}$-RTT wide-area path is on the order of
$1$--$2~\mathrm{ms}$. TCP+TLS-FIX recovery on the same path
includes TCP three-way handshake plus TLS key exchange plus
session-state reconstruction; the dominant residual cost is
$T_{\mathrm{backoff}}$, which can be tens of milliseconds in the
presence of competing flows.

\section{Order-of-Fills Determinism}
\label{sec:determinism}

\begin{lemma}[Sequence preservation]
\label{lem:seq}
For any two consecutive FIX application messages $M_i, M_{i+1}$
emitted on a ZAP-FIX session by the same peer, the corresponding
ZAP frames $F(M_i), F(M_{i+1})$ satisfy:
\begin{enumerate}
  \item $F(M_i)$ is delivered before $F(M_{i+1})$ at the receiver.
  \item $\texttt{MsgSeqNum}(F(M_{i+1})) =
        \texttt{MsgSeqNum}(F(M_i)) + 1$.
\end{enumerate}
\end{lemma}

\begin{proof}
Property~(i) is the in-order delivery guarantee of the ZAP session
binding: ZAP frames on a single session form a totally ordered
stream, and the send-side serialiser emits one frame per message
without coalescing or reordering. Property~(ii) follows from the
construction of Section~3.3 of the paper, which fixes the
\texttt{MsgSeqNum} field of the envelope header to the FIX session
\texttt{MsgSeqNum} at emission time and refuses out-of-order
emission.
\end{proof}

\begin{corollary}[Order-of-fills determinism]
A matching engine consuming application messages from a ZAP-FIX
session observes the same per-session arrival order as it would
under a TCP+TLS-FIX binding with identical wire conditions. The
FIX session-layer invariant in Equation~(1) of the paper is
preserved.
\end{corollary}

\section{Threats Outside the Model}
\label{sec:threats}

The bounds above hold against:
\begin{itemize}
  \item Loss-driven TCP recovery (TLS-FIX pays $T_{\mathrm{backoff}}$
        that ZAP-FIX does not, given a stateless re-handshake).
  \item Cryptographic harvest-now-decrypt-later: ZAP-FIX inherits
        post-quantum hybrid KEM from the underlying ZAP transport;
        TLS~1.3 in deployed profiles does not.
  \item CompID-spoofing at session establishment: ZAP-FIX binds the
        FIX \texttt{SenderCompID} to the ZAP identity at handshake
        time, and the gateway rejects mismatches; TLS-FIX with
        client-cert authentication achieves a comparable bind, but
        the deployed default is server-only TLS plus FIX-layer
        password.
\end{itemize}
The bounds do \emph{not} address:
\begin{itemize}
  \item Application-layer matching cost $T_{\mathrm{app}}$, which is
        unaffected by the transport choice.
  \item Cross-venue race conditions, which are governed by
        venue-side scheduling rather than the institutional channel.
  \item Adversarial NIC behaviour or hardware-clock skew exceeding
        the RTS~25 envelope; both bindings depend on the underlying
        PTP discipline.
\end{itemize}

\section{Summary}

Theorem~\ref{thm:steady} establishes that, in steady state and for
every FIX message $M$, ZAP-FIX per-message latency is no greater
than TCP+TLS-FIX latency, and is strictly less by the
serialisation, parse, and per-byte savings tabulated above.
Theorem~\ref{thm:resume} establishes that ZAP-FIX session
resumption is bounded above by a single network round trip plus a
FIX Logon, regardless of pod migration or partition, while
TCP+TLS-FIX pays at least two round trips plus loss-driven
backoff. Lemma~\ref{lem:seq} establishes that ZAP-FIX preserves the
FIX session-layer determinism that all downstream
order-handling and audit logic depend on.

\end{document}