papers/chain-first-architecture/sections/03-correctness-properties.tex

\section{Correctness Properties}

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

\subsection{Cache Consistency}

\begin{theorem}[Cache Consistency]
\label{thm:consistency}
If the indexer processes every block from genesis through block $h$
without skipping or reordering, then $\mathcal{D}_h = \mathcal{C}_h$.
\end{theorem}

\begin{proof}
By induction on block height $h$.

\emph{Base case ($h = 0$).}  The cache is initialized from the genesis
configuration, which is identical to $\mathcal{C}_0$.  Therefore
$\mathcal{D}_0 = \mathcal{C}_0$.

\emph{Inductive step ($h \to h+1$).}  Assume
$\mathcal{D}_h = \mathcal{C}_h$.  Block $h+1$ produces events
$e_1, \ldots, e_k$, and the chain state transitions to
$\mathcal{C}_{h+1} = \mathcal{T}_{h+1}(\mathcal{C}_h)$.  The indexer
applies $\delta(e_1) \circ \cdots \circ \delta(e_k)$ to
$\mathcal{D}_h$.  Because the indexer's $\delta$ functions are the
deterministic projection of the chain's state transition function
$\mathcal{T}$ onto the cached dimensions (balances, positions,
transaction history), and because the events $e_i$ encode exactly the
state changes made by $\mathcal{T}_{h+1}$, we have
$\mathcal{D}_{h+1} = \mathcal{C}_{h+1}$.
\end{proof}

\subsection{Crash Recovery}

\begin{theorem}[Crash Recovery]
\label{thm:recovery}
If the cache is destroyed at any point, it can be fully reconstructed
by replaying all chain blocks from genesis.
\end{theorem}

\begin{proof}
Initialize an empty cache $\mathcal{D}'_0 = \mathcal{C}_0$ (from the
genesis configuration).  For each block $h = 1, 2, \ldots, H$ (where
$H$ is the current chain height), apply the indexer's $\delta$
functions to the events in block $h$.  By
Theorem~\ref{thm:consistency}, the reconstructed cache
$\mathcal{D}'_H = \mathcal{C}_H$.

The reconstruction is deterministic: given the same chain, the same
cache is produced regardless of when the reconstruction occurs.  The
chain is the only input; no external state is required.
\end{proof}

\subsection{Chain Independence}

\begin{theorem}[Chain Independence]
\label{thm:independence}
If the chain becomes temporarily unavailable, the API layer continues
to serve reads from the cache (reflecting the last known chain state)
and queues writes for later settlement.  No data is lost.
\end{theorem}

\begin{proof}
Reads are served from the cache $\mathcal{D}_h$ where $h$ is the last
processed block.  The cache is a local database (SQLite or PostgreSQL)
that does not depend on chain connectivity.

Writes (new orders, trades) are recorded in the
\texttt{pending\_settlements} table in the local database.  The
settlement cron retries pending settlements on a 30-second interval.
When chain connectivity is restored, the cron processes all queued
settlements.  The \texttt{pending\_settlements} table acts as a durable
write-ahead log.

No data is lost because:
\begin{enumerate}[nosep]
  \item Reads serve stale-but-consistent data (consistent as of block
        $h$).
  \item Writes are durably queued and will be settled when the chain
        returns.
  \item The chain's append-only property guarantees that blocks
        processed before the outage are still valid after the outage.
\end{enumerate}
\end{proof}

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