papers/lux-sovereign-defi/sections/07-formal-properties.tex

\section{Formal Properties}

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

\subsection{Governance Isolation Theorem}

\begin{theorem}[Governance Isolation]
\label{thm:gov-isolation}
Let $\Gov_i$ be the governor of chain $\Chain_i$'s bridge instance $R_i$. Even if $\Gov_i$ is fully compromised (adversary controls the governor key), the adversary cannot:
\begin{enumerate}[nosep]
  \item Mint bridge tokens on any chain without a valid MPC signature.
  \item Modify the nonce bitmap on any chain.
  \item Set $f_b^{(i)} > 100$ bps.
  \item Affect parameters of $R_j$ for any $j \neq i$.
  \item Bypass the 48-hour timelock on stakeholder vault changes.
\end{enumerate}
\end{theorem}

\begin{proof}
We prove each property:

\emph{(1)} The \texttt{bridgeMint} function requires $\texttt{ecrecover}(\sigma) = \texttt{mpcAddress}$. The governor address is checked against \texttt{governor}, not \texttt{mpcAddress}. No code path grants the governor mint authority. The \texttt{onlyGovernor} modifier gates only parameter-setting functions, which are disjoint from the mint/release code paths.

\emph{(2)} Nonce bitmaps are modified only within \texttt{bridgeMint} and \texttt{bridgeRelease}, both of which require valid MPC signatures. No governor-accessible function writes to the nonce bitmap mapping.

\emph{(3)} The \texttt{setBridgeFee} function contains \texttt{require(newFeeBps <= MAX\_FEE\_BPS)}. \texttt{MAX\_FEE\_BPS} is a compile-time constant set to 100. The \texttt{PUSH} opcode embeds this value directly in bytecode; it cannot be modified by any transaction.

\emph{(4)} Follows from Theorem~\ref{thm:instance}: each $R_j$ is a separate contract on a separate chain with independent storage.

\emph{(5)} The \texttt{setStakeholderVault} function stores the new vault address but does not activate it. A separate \texttt{executeVaultChange} function requires $\texttt{block.timestamp} \geq \texttt{vaultChangeTimestamp} + 48 \text{ hours}$. No code path bypasses this check.
\end{proof}

\subsection{Exit Guarantee}

\begin{theorem}[Exit Guarantee]
\label{thm:exit}
Under the assumption that at least $t$ of $n$ MPC signer nodes remain honest and the destination chain is live, any bridge token holder can exit the system (burn bridge tokens and receive underlying assets) within 7 days under all conditions, including:
\begin{enumerate}[nosep]
  \item Governor compromise on any chain.
  \item Single MPC node failure ($< t$ failures).
  \item Pending signer rotation.
  \item Shariah mode changes.
  \item Fee parameter changes.
\end{enumerate}
\end{theorem}

\begin{proof}
The \texttt{burnForWithdrawal} function is callable by any bridge token holder without governor approval. It emits a \texttt{Burn} event. The MPC signer set observes this event and, given $\geq t$ honest nodes, produces a release signature within one attestation period (15 minutes). The \texttt{bridgeRelease} function on the source chain verifies the signature and releases assets. Governor compromise does not affect this path because \texttt{burnForWithdrawal} has no \texttt{onlyGovernor} modifier, and \texttt{bridgeRelease} requires only a valid MPC signature.

During signer rotation, the 7-day timelock ensures that the current signer set remains active throughout the exit window. Shariah mode and fee changes affect only future deposits, not the burn/release path. Fee changes affect only the fee on the next bridge operation; they do not affect previously minted bridge tokens.
\end{proof}

\subsection{Fee Cap Invariant}

\begin{invariant}[Fee Cap]
\label{inv:feecap}
For all chains $\Chain_i$ and all times $t$:
\begin{equation}
  f_b^{(i)}(t) \leq 100 \text{ bps}
\end{equation}
This holds even if the governor is compromised, the MPC set is rotated, or the contract is called via a delegate call from a malicious contract.
\end{invariant}

\begin{proof}
The fee rate is stored as a \texttt{uint256} in contract storage. The only function that modifies this value is \texttt{setBridgeFee}, which contains the hard-coded check \texttt{require(newFeeBps <= 100)}. The constant 100 is embedded in the contract bytecode as a \texttt{PUSH1 0x64} instruction. The contract is non-upgradeable (no proxy pattern, no \texttt{DELEGATECALL} to external implementations). No \texttt{SELFDESTRUCT} is present. The only external call paths are to the MPC signature verification (read-only) and fee recipient transfer (which does not modify fee state). Therefore, the fee cap is maintained for all time.
\end{proof}

\subsection{Conservation Under Shariah Mode}

\begin{property}[Shariah Conservation]
\label{prop:shariah-conservation}
When Shariah mode is enabled on instance $R_i$:
\begin{equation}
  \forall y \in \Strategy_{\text{active}}^{(i)}: \phi(y) = \halal
\end{equation}
No Haram or Conditional strategy can hold deposited assets. Existing deposits in non-Halal strategies are not forcibly withdrawn, but no new deposits flow to them.
\end{property}

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