papers/lux-fraud-proofs/sections/04-interactive-bisection-game.tex

\section{Interactive Bisection Game}


The bisection game is the core mechanism for efficiently identifying the specific point of disagreement between challenger and defender.

\subsection{N-Step Execution Trace}

The defender (asserter) publishes an execution trace representing the state at various checkpoints:

\begin{definition}[Execution Trace]
An $n$-step execution trace is a sequence $\mathcal{E} = \{S_0, S_{k}, S_{2k}, ..., S_n\}$ where each $S_i$ represents the complete state after executing $i$ steps, and $k$ is the checkpoint interval.
\end{definition}

\subsection{Challenge Identification}

The challenger identifies the first disputed checkpoint by comparing their computed states with the defender's claims:

\begin{equation}
i^* = \min\{i : S_i^{\text{claimed}} \neq S_i^{\text{computed}}\}
\end{equation}

\subsection{Binary Search Protocol}

The protocol proceeds through $\log_2(n)$ rounds of bisection:

\begin{theorem}[Bisection Complexity]
For an $n$-step computation, the bisection protocol identifies the disputed step in at most $\lceil\log_2(n)\rceil$ rounds.
\end{theorem}

\begin{proof}
Each round eliminates half of the remaining search space. Starting with $n$ possible disputed steps, after $k$ rounds the search space is reduced to $n/2^k$. The protocol terminates when the search space reaches size 1, requiring $k = \lceil\log_2(n)\rceil$ rounds.
\end{proof}

\subsection{Convergence to Single Step}

The bisection process guarantees convergence to a single disputed instruction:

\begin{lemma}[Convergence Guarantee]
Given honest participation from at least one party, the bisection protocol converges to a unique disputed step $(s_i, t_i, s_{i+1})$ where the parties disagree on whether $s_{i+1} = \text{STF}(s_i, t_i)$.
\end{lemma}