papers/lp-225-xss-x-chain-settlement-spine/sections/09-safety.tex

\section{Safety properties}
\label{sec:safety}

The properties XSS must satisfy, stated formally. Each names the
mechanism that enforces it and its status. Properties S1--S2 and S5 are
enforceable by X's own checks (extensions of the \IMPL{}
\texttt{lux.VerifyTx} discipline). Properties S3--S4 depend on the
shielded pool and are \CRYPTO{} (Section~\ref{sec:open}).

\paragraph{Notation.} For asset $a$ at height $h$: let $V(a,h)$ be the
sum of spendable X UTXOs, $L(a,h)$ the sum of locked X UTXOs (value
inside live \texttt{XLock}s), $S(a,h)$ the sum of live (un-nullified) Z
note values. $\mathrm{total}(a)$ is the fixed total supply.

\subsection*{S1 --- One X state per unit}

\textbf{Statement.} Every unit of value of asset $a$ is, at every height,
in exactly one of: spendable UTXO, locked UTXO (inside one \texttt{XLock}),
or consumed UTXO. No unit is in two states; no unit is in none.

\textbf{Enforcement.} A UTXO is consumed exactly once (existing
consume-once on inputs). \texttt{LockTx} consumes spendable UTXOs and
produces exactly one \texttt{XLock} (locked). \texttt{UnlockTx}/\texttt{SettleTx}
consume the \texttt{XLock} (locked $\to$ spendable/consumed) and set
\texttt{consumed} once. The state machine has no transition that lands a
unit in two states. \DESIGN{} (extends the \IMPL{} consume-once and
conservation checks).

\subsection*{S2 --- Conservation across all pools}

\textbf{Statement.} For every asset $a$ and every height $h$:
\[
  V(a,h) + L(a,h) + S(a,h) = \mathrm{total}(a),
\]
and in particular the visible/shielded split
$\;[V(a,h)+L(a,h)] + S(a,h) = \mathrm{total}(a)\;$
(visible $+$ shielded $=$ total).

\textbf{Enforcement.} Every primitive's conservation effect
(Section~\ref{sec:primitives}) is net-zero on $\mathrm{total}(a)$:
\texttt{LockTx}/\texttt{UnlockTx} move between $V$ and $L$;
\texttt{SettleTx} moves $L$ into $V$ and/or $S$; shield/unshield move
between $[V{+}L]$ and $S$. X checks the per-asset sum on every
\texttt{SettleTx} and the bridge checks the equal-value link on every
shield/unshield. \DESIGN{}; the visible-side terms extend \IMPL{}
\texttt{lux.VerifyTx}, the shielded term $S(a,h)$ is new and untracked
today (Section~\ref{sec:bridge}).

\subsection*{S3 --- Other chains compute, X settles}

\textbf{Statement.} No chain other than X (and Z via the bridge) can
make a unit of value spendable. A computing module can only produce a
proof or a settlement request; the spendable output exists only after
X's \texttt{SettleTx} (or X's unshield mint).

\textbf{Enforcement.} Spendable UTXOs are created only by X transactions.
A module's settlement is inert until \texttt{SettleTx} on X verifies its
proof (\texttt{VerifyChainCommitment}) and checks conservation. \DESIGN{}.
\textbf{Current-code contradiction:} the P-Chain today \emph{does} make
value spendable on its own --- it mints reward UTXOs and can create
assets (\texttt{txs/executor/proposal\_tx\_executor.go:300--325};
\texttt{create\_asset\_tx.go:61}) --- and the D-Chain credits balances
independently (\texttt{lx/dex/pkg/dchain/state.go}). S3 holds only after
P4 resolves P's mint authority and the modules run \texttt{unified}; it
is the property the migration \emph{establishes}, not one current code
satisfies.

\subsection*{S4 --- Shielded double-spend prevented by nullifiers}

\textbf{Statement.} A shielded note can be consumed (spent on Z or
unshielded to X) at most once.

\textbf{Enforcement.} Spending a note publishes its nullifier; a
nullifier may enter the spent set at most once; a note whose nullifier
is already present is rejected. \IMPL{} persistent nullifier set
(\texttt{lux/chains/zkvm/nullifier\_db.go}) and nullifier computation
(\texttt{precompile/zk/commitment.go}). \textbf{\CRYPTO{}}: that the
nullifier is binding (one note $\to$ one nullifier, unforgeable) and
that the cross-boundary case (cannot unshield on X \emph{and} re-spend
on Z) is sound requires cryptographer sign-off
(Section~\ref{sec:open}).

\subsection*{S5 --- Lock exclusivity}

\textbf{Statement.} A locked UTXO cannot be double-locked and cannot be
freely spent. The value inside an \texttt{XLock} is spendable only via a
\texttt{SettleTx}/\texttt{UnlockTx} that consumes that exact lock, and
each lock is consumed once.

\textbf{Enforcement.} \texttt{LockTx} consumes the source UTXOs (they no
longer exist as spendable, so they cannot be re-locked or spent). The
\texttt{XLock}'s \texttt{consumed} flag is set by exactly one of
\texttt{SettleTx}/\texttt{UnlockTx}; X rejects any second consume. No
\texttt{secp256k1fx} spend path applies to a locked output. \DESIGN{}
(reuses the \IMPL{} consume-once discipline of the atomic rail,
\texttt{lux/chains/dexvm/atomic.go} \texttt{MarkConsumed}).

\subsection*{Summary}

\begin{center}
\begin{tabular}{@{}lll@{}}
\toprule
Property & Enforced by & Status \\
\midrule
S1 one state per unit          & lock state machine, consume-once   & \DESIGN{} (extends \IMPL{}) \\
S2 conservation all pools      & per-primitive net-zero, \texttt{SettleTx} sum & \DESIGN{} (visible \IMPL{}) \\
S3 compute vs settle           & spendable only via X               & \DESIGN{}; P/D contradict today \\
S4 no shielded double-spend    & nullifier set                      & \CRYPTO{} \\
S5 lock exclusivity            & \texttt{consumed} flag, consume-once & \DESIGN{} (reuses \IMPL{}) \\
\bottomrule
\end{tabular}
\end{center}