papers/lux-restaking/sections/03-formal-model.tex

\section{Formal Model}

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

\subsection{Staking Hypergraph}

\begin{definition}[Staking Hypergraph]
Let $\mathcal{V}$ be the set of \emph{operators} (validator nodes), $\mathcal{S}$ the set
of registered \emph{services} (AVSs and appchains), and $w: \mathcal{V} \to \mathbb{R}_{>0}$
the stake function mapping each operator to their staked LUX. Define the
\emph{staking hypergraph} $\mathcal{H} = (\mathcal{V}, \mathcal{S}, \mathcal{E})$ where
each \emph{restaking commitment} $e_{v,s} \in \mathcal{E}$ encodes operator $v$'s
opt-in to service $s$ with:
\begin{itemize}
  \item an \emph{allocated fraction} $\alpha_{v,s} \in (0,1]$ of $v$'s stake pledged as
    collateral for $s$;
  \item a set of \emph{slashing conditions} $\Sigma_s$ defined by service $s$.
\end{itemize}
\end{definition}

\begin{definition}[Operator Exposure]
The total exposure of operator $v$ is:
\[
  E(v) = \sum_{s: e_{v,s} \in \mathcal{E}} \alpha_{v,s} \cdot w(v).
\]
We say operator $v$ is \emph{over-exposed} if $E(v) > w(v)$, which is disallowed:
\[
  \sum_{s \in \mathcal{S}} \alpha_{v,s} \leq 1 \quad \forall v \in \mathcal{V}.
\]
\end{definition}

\begin{definition}[Service Economic Security]
The economic security of service $s$ is:
\[
  \Pi(s) = \sum_{v: e_{v,s} \in \mathcal{E}} \alpha_{v,s} \cdot w(v).
\]
\end{definition}

\begin{definition}[Corruption Cost]
For a Byzantine fault tolerance threshold $f_s \in (0,1)$ (the minimum fraction of
stake needed to corrupt service $s$), the \emph{corruption cost} is:
\[
  \mathcal{C}(s) = f_s \cdot \Pi(s).
\]
An attack on service $s$ is economically irrational if $\mathcal{C}(s) > \text{ProfitableAttackValue}(s)$.
\end{definition}

\subsection{Aggregate Security}

Let $\{s_1, \ldots, s_k\}$ be a collection of services. Naive addition of their individual
economic security overcounts shared stake. We define \emph{aggregate economic security} as:

\begin{equation}
\Pi_{\text{agg}}(s_1,\ldots,s_k) = \sum_{v \in \mathcal{V}} \max_{s \in \{s_1,\ldots,s_k\}} (\alpha_{v,s} \cdot w(v)).
\label{eq:aggregate}
\end{equation}

This represents the total stake that would be slashed in a simultaneous attack on all $k$
services by every operator. We note:

\begin{proposition}[Subadditivity of Aggregate Security]
\[
  \Pi_{\text{agg}}(s_1,\ldots,s_k) \leq \sum_{i=1}^k \Pi(s_i),
\]
with equality if and only if no operator is committed to more than one service.
\end{proposition}

\begin{proof}
For each operator $v$: $\max_{i}(\alpha_{v,s_i} \cdot w(v)) \leq \sum_i \alpha_{v,s_i} \cdot w(v)$.
Summing over all $v$ gives the result.
\end{proof}

\subsection{Capital Efficiency Ratio}

\begin{definition}[Capital Efficiency Ratio]
Let $W = \sum_{v} w(v)$ be the total staked capital. The capital efficiency ratio is:
\[
  \rho = \frac{\sum_{s \in \mathcal{S}} \Pi(s)}{W} = \frac{\text{Total Security Provided}}{\text{Total Capital Staked}}.
\]
Under isolated staking ($|\mathcal{S}|$ separate staking pools), $\rho_{\text{iso}} = 1$.
Under LRP, $\rho_{\text{LRP}} = \sum_{v,s} \alpha_{v,s} / |\mathcal{V}|$, which can
substantially exceed 1.
\end{definition}

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