mirror of
https://github.com/lux-apps/papers.git
synced 2026-10-30 18:15:21 +00:00
zeekay
abf99d05fc
Restructured from flat .tex/.pdf files into per-paper subdirectories. Added Antje Worring as co-author on all papers. Synced PDFs to pdfs/ for download site.
90 lines
2.8 KiB
TeX
90 lines
2.8 KiB
TeX
\section{The Teleport Specification}
|
|
|
|
|
|
Teleport is Lux Network's cross-chain bridge protocol. The TLA+ specification models
|
|
the complete message lifecycle: deposit on the source chain, attestation by validators,
|
|
relay to the destination chain, and withdrawal.
|
|
|
|
\subsection{State Variables}
|
|
|
|
\begin{lstlisting}[language=TLA,caption={Teleport state variables}]
|
|
---- MODULE Teleport ----
|
|
EXTENDS Integers, FiniteSets, Sequences
|
|
|
|
CONSTANTS
|
|
Chains, \* Set of chain IDs
|
|
Validators, \* Bridge validator set
|
|
MaxFaulty, \* f < n/3
|
|
Users, \* Set of user addresses
|
|
MaxAmount \* Bound for model checking
|
|
|
|
VARIABLES
|
|
sourceBalances, \* [chain][user] -> amount
|
|
destBalances, \* [chain][user] -> amount
|
|
lockedFunds, \* [chain] -> total locked
|
|
pendingMessages, \* Set of cross-chain messages
|
|
attestations, \* [msgId] -> set of attesting validators
|
|
relayedMessages, \* Set of already-relayed message IDs
|
|
faulty \* Set of Byzantine validators
|
|
\end{lstlisting}
|
|
|
|
\subsection{Safety Properties}
|
|
|
|
\begin{lstlisting}[language=TLA,caption={Teleport safety properties}]
|
|
\* No double-spend: a message is relayed at most once
|
|
NoDoubleRelay ==
|
|
\A msg \in relayedMessages :
|
|
Cardinality({m \in relayedMessages : m.id = msg.id}) = 1
|
|
|
|
\* Conservation: total tokens across all chains is constant
|
|
Conservation ==
|
|
LET totalLocked == SumOver(Chains, LAMBDA c : lockedFunds[c])
|
|
totalDest == SumOver(Chains, LAMBDA c :
|
|
SumOver(Users, LAMBDA u : destBalances[c][u]))
|
|
IN totalLocked = totalDest
|
|
|
|
\* Authenticity: relayed messages have quorum attestation
|
|
Authenticity ==
|
|
\A msg \in relayedMessages :
|
|
Cardinality(attestations[msg.id] \ faulty) >= Q
|
|
\end{lstlisting}
|
|
|
|
\subsection{Model Checking Results}
|
|
|
|
We model-check Teleport with the following parameters:
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lrl@{}}
|
|
\toprule
|
|
\textbf{Parameter} & \textbf{Value} & \textbf{Rationale} \\
|
|
\midrule
|
|
Chains & 3 & Source, destination, third chain \\
|
|
Validators & 4 & Minimum for $f = 1$ \\
|
|
MaxFaulty & 1 & $f < n/3 \Rightarrow f \leq 1$ \\
|
|
Users & 2 & Sender and receiver \\
|
|
MaxAmount & 3 & Small values expose arithmetic bugs \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{TLC model checking parameters for Teleport.}
|
|
\end{table}
|
|
|
|
\begin{table}[H]
|
|
\centering
|
|
\small
|
|
\begin{tabular}{@{}lrrl@{}}
|
|
\toprule
|
|
\textbf{Property} & \textbf{States} & \textbf{Time} & \textbf{Result} \\
|
|
\midrule
|
|
TypeOK & 2.4M & 47s & Holds \\
|
|
NoDoubleRelay & 2.4M & 52s & Holds \\
|
|
Conservation & 2.4M & 61s & Holds \\
|
|
Authenticity & 2.4M & 55s & Holds \\
|
|
\bottomrule
|
|
\end{tabular}
|
|
\caption{TLC results for Teleport specification. 16-core machine, 32GB heap.}
|
|
\end{table}
|
|
|
|
%% ============================================================
|