consensus/proofs/no_double_finalize.tex

% Copyright (C) 2026, Lux Industries, Inc. All rights reserved.
% SPDX-License-Identifier: BSD-3-Clause-Eco
%
% Safety + liveness of the consensus leaderless BLS quorum-certificate finality
% gate, and the honest non-equivocation discipline the Node enforces. The slot is a
% HEIGHT (not (height,epoch)): the epoch is a proposer-chosen axis and must not
% fragment the equivocation slot. Non-equivocation is made durable across a height's
% whole life by a monotonic decided-height frontier + strictly-below GC (src/node.cpp),
% closing the prune-then-resign fork; per the proposer-fallback acceptance standard.
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb,amsthm}
\usepackage[margin=1in]{geometry}

\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{definition}{Definition}
\newtheorem{corollary}{Corollary}

\title{Agreement and Liveness of the \texttt{consensus} Leaderless\\
       BLS Quorum-Certificate Finality Gate}
\author{Lux Industries --- consensus / node2}
\date{}

\begin{document}
\maketitle

\section{Model}

Let $V=\{v_1,\dots,v_n\}$ be a fixed validator set, each $v_i$ holding a distinct
BLS12-381 key pair (POP ciphersuite, proof-of-possession verified at admission) and
an integer stake $w_i>0$. Write $W=\sum_i w_i$ for the total stake. For a set
$S\subseteq V$ let $w(S)=\sum_{v_i\in S} w_i$.

A \emph{position} is a triple $p=(b,h,e)$: a $32$-byte block id $b$, a height $h$,
and an epoch $e$. Two positions $p,p'$ are \emph{conflicting siblings} when
$h=h'$ and $b\neq b'$ --- \emph{any} two distinct blocks at one height, regardless of
their epochs. The canonical signed message
$\mu(p)$ is a domain-separated, fixed-width encoding of $p$ together with the
protocol tag, version, role, and the $\texttt{accept}=\mathtt{0x01}$ byte
(\texttt{quorum\_cert\_engine.cpp}, \texttt{canonical\_vote\_message}); distinct
positions yield distinct messages, and a signature over $\mu(p)$ verifies for no
$p'\neq p$. The epoch $e$ is folded into $\mu(p)$ (and re-checked by
\texttt{verify\_cert}) purely for anti-replay / cross-epoch binding; it is \emph{not}
a slot axis (see the honest discipline below).

\paragraph{Finality rule (one rule, one place).}
Fix the distinct-voter floor $\alpha\in\{1,\dots,n\}$. A position $p$
\emph{finalizes} at a gate exactly when a set $Q\subseteq V$ of voters satisfies all
three of:
\begin{enumerate}
  \item[(C)] $|Q|\ge\alpha$ \hfill (count floor);
  \item[(S)] $w(Q) > \big\lfloor \tfrac{2}{3}W \big\rfloor$ \hfill (strict $2/3$ stake supermajority);
  \item[(V)] every $v_i\in Q$ produced a BLS signature $\sigma_i$ with
        $\mathrm{Verify}(pk_i,\mu(p),\sigma_i)=1$ \hfill (cryptographic verification).
\end{enumerate}
There is no $k{=}1$, \texttt{ForceAccept}, or count-only path; $W=0$ or an unopened
position never finalizes (fail-closed). The floor $\lfloor 2W/3\rfloor$ is computed
without overflow, byte-identical to the Go reference \texttt{TwoThirdsStakeFloor}.

\paragraph{Adversary.}
A subset $B\subseteq V$ of validators is Byzantine; let $f=w(B)$ be its stake. The
adversary controls $B$'s keys (it may sign any message, including conflicting
siblings) and the network schedule. Honest validators $H=V\setminus B$ follow the
protocol. We assume the standard BFT bound $f < W/3$, i.e. $f \le \lfloor (W-1)/3\rfloor$.
The BLS scheme is EUF-CMA, so the adversary cannot forge a signature for a key it
does not control; condition (V) therefore counts only genuine signatures.

\paragraph{Honest discipline (the non-equivocation rule).}
The slot is a \emph{height} $h$ --- \textbf{not} $(h,e)$. Each honest validator signs
$\texttt{accept}$ for \emph{at most one} block per height, across its entire execution.
This is enforced in \texttt{src/node.cpp} by two guards, evaluated before signing:
\begin{itemize}
  \item \textbf{per-height slot:} the map $\texttt{committed\_slot\_}:h\mapsto b$ records
        the unique block a node has signed at height $h$; a $\beta$-confirmed
        \textsc{Accept} for a \emph{different} block at an already-committed height is
        refused (a re-solicit of the same block is idempotent).
  \item \textbf{decided-height gate:} a monotonic frontier $\texttt{final\_through\_}$
        marks every height $\le$ it as decided; a $\beta$-confirmed \textsc{Accept} at a
        decided height is refused. This is the analogue of avalanche's
        $\texttt{lastAcceptedHeight}$ frontier (\texttt{topological.go}), where a decided
        height's siblings are removed from the tree and their votes dropped.
\end{itemize}

\paragraph{Why height, not $(h,e)$ (the durable invariant).}
Keying the slot on $(h,e)$ \emph{fragments} it: two honest sibling blocks at one height
can carry \emph{different} epochs --- a bare / pre-fork block and a proposervm-wrapped
block report different underlying P-chain heights, and $e$ is derived from that
proposer-chosen value, not from the finalized value-chain prefix. Under an $(h,e)$ slot an
honest validator could commit \emph{both} siblings (one per $(h,e)$), and two
$>\!2/3$-stake certs would finalize at one height. So the epoch is a proposer-controlled
axis and must never key the equivocation slot; it survives only inside $\mu(p)$ and the
cert. The height-only slot matches the Go reference exactly (\texttt{engine/chain}
\texttt{SlotKey\{Height\}}, \texttt{reserveSlotForSign}). Formally:

\begin{definition}[Honest non-equivocation]\label{def:nonequiv}
For every honest $v_i\in H$ and every height $h$, the set of block ids $b$ for which
$v_i$ ever emits a valid signature over $\mu((b,h,\cdot))$ has size at most one.
\end{definition}

\paragraph{Slot lifecycle (no prune-then-resign).}
$\texttt{committed\_slot\_}$ is garbage-collected only \emph{strictly below} the monotonic
$\texttt{final\_through\_}$ frontier (\texttt{Node::mark\_finalized\_through}), so the
just-decided height's binding is retained as a second in-memory belt and every lower
binding is reclaimed to bound memory. Crucially, GC \emph{cannot} re-enable a signature:
a height at or below the frontier is refused by the decided-height gate whether or not its
slot still exists. Hence Definition~\ref{def:nonequiv} holds across the \emph{entire} run,
not merely while a slot object lives --- closing the ``prune-then-resign'' fork in which an
inclusive prune deleted the decided height's slot and a late, differently-enveloped sibling
(one the DAG reject could not reach, because it hangs off a different outer parent) then
collected a validator's \emph{second} signature at that height. A lower frontier value
never regresses it (monotone).

\paragraph{Durability across a restart.}
The frontier must survive process restart, or a correlated rolling restart of a storming
fresh net reopens the fork: the just-GC'd below-tip slots are gone and, on the Go node, the
\emph{certified} ledger height is a non-authoritative $(0,\text{false})$ hint until the
first post-restart certificate (incident-1082814 PART-A). The Go node (the authoritative
durable path) therefore persists the decided-through floor in the same fsync'd write as the
pruned slot set (\texttt{engine/chain/vote\_guard.go}, \texttt{finalizedThrough}) and
re-seeds \texttt{reserveSlotForSign}'s floor from it on boot, folding in the
\texttt{vm.LastAccepted} hint height as a complementary lower bound --- a SIGN-GATE-ONLY
value that never enters \texttt{byHeight} or the authoritative finality ledger (PART-A
preserved). The \texttt{consensus} \texttt{Node} keeps \texttt{final\_through\_} in memory
only; it is a pure library with no persistence layer, so its embedder (\texttt{node2}) MUST
re-seed the frontier via \texttt{mark\_finalized\_through} from its own persisted decided
height on boot before the node signs. With that boot-seed, Definition~\ref{def:nonequiv}
holds across restarts as well.

\section{Agreement (no double finalize)}

The naive ``two $>\!2/3$ quorums intersect in $>\!1/3$ stake, which must contain an
honest validator'' argument is \emph{too weak} here: with $W=100$ the strict floor
gives intersection $\ge 2\lfloor 2W/3\rfloor - W + 1 = 33$, which does not strictly
exceed $W/3=33.\overline{3}$, so it cannot by itself exclude an all-Byzantine
intersection at $f=33$. The correct argument uses honest \emph{disjointness} (the
non-equivocation discipline) directly, with the strict integer stake bound.

\begin{lemma}[Honest mass of a finalizing quorum]\label{lem:mass}
If a quorum $Q$ finalizes a position (meets (S) and (V)), then its honest voters
carry stake $w(Q\cap H) \ge \lfloor 2W/3\rfloor + 1 - f$.
\end{lemma}
\begin{proof}
(S) is a strict integer inequality, so $w(Q)\ge \lfloor 2W/3\rfloor + 1$. The
Byzantine voters in $Q$ carry at most $w(B)=f$, so
$w(Q\cap H)=w(Q)-w(Q\cap B)\ge \lfloor 2W/3\rfloor + 1 - f$. By (V) every counted
voter signed genuinely, so $Q\cap H$ are honest validators that actually signed.
\end{proof}

\begin{theorem}[Agreement]\label{thm:agree}
If $f\le\lfloor (W-1)/3\rfloor$ (i.e.\ $f<W/3$), no two conflicting sibling positions
$p_1=(b_1,h,e_1)$ and $p_2=(b_2,h,e_2)$ with $b_1\neq b_2$ (same height, arbitrary
epochs) both finalize.
\end{theorem}
\begin{proof}
Suppose both finalize with verified quorums $Q_1,Q_2$. Let $H_i=Q_i\cap H$. By
Definition~\ref{def:nonequiv} an honest validator signs at most one block at height $h$
(regardless of epoch), hence at most one of $b_1,b_2$; so $H_1\cap H_2=\varnothing$ and
therefore
\[
  w(H_1)+w(H_2)\;=\;w(H_1\cup H_2)\;\le\;w(H)\;=\;W-f .
\]
By Lemma~\ref{lem:mass}, $w(H_i)\ge \lfloor 2W/3\rfloor + 1 - f$ for $i=1,2$, hence
\[
  W-f \;\ge\; w(H_1)+w(H_2) \;\ge\; 2\big(\lfloor 2W/3\rfloor + 1 - f\big)
  \;\;\Longrightarrow\;\; f \;\ge\; 2\lfloor 2W/3\rfloor + 2 - W .
\]
Write $W=3q+r$, $r\in\{0,1,2\}$, so $\lfloor 2W/3\rfloor = 2q+[\,r{=}2\,]$ and the
right-hand side equals $q+2$ for $r\in\{0,2\}$ and $q+1$ for $r=1$. In every case it
exceeds $\lfloor (W-1)/3\rfloor$ (which is $q-1,\,q,\,q$ for $r=0,1,2$). Thus
$f\ge 2\lfloor 2W/3\rfloor+2-W > \lfloor (W-1)/3\rfloor \ge f$, a contradiction.
Hence at most one sibling finalizes.
\end{proof}

\begin{theorem}[Tightness]\label{thm:tight}
If $f\ge 2\lfloor 2W/3\rfloor + 2 - W$ (the smallest Byzantine stake the bound in
Theorem~\ref{thm:agree} admits, which is $\le\lceil W/3\rceil$), the adversary
\emph{can} finalize two conflicting siblings. The threshold is therefore exact and
equals avalanche's $f<n/3$.
\end{theorem}
\begin{proof}
The construction saturates the inequalities of Theorem~\ref{thm:agree}: $f$
equivocators sign both siblings, and the honest stake $W-f$ is split into two
disjoint sets $H_1,H_2$ with $w(H_i)=\lfloor 2W/3\rfloor + 1 - f$ each, which is
feasible exactly when $2(\lfloor 2W/3\rfloor+1-f)\le W-f$, i.e.\ when
$f\ge 2\lfloor 2W/3\rfloor+2-W$. Then $w(Q_i)=f+w(H_i)=\lfloor 2W/3\rfloor+1>
\lfloor 2W/3\rfloor$ and $|Q_i|\ge\alpha$, so both finalize. The witness is realized
concretely in \texttt{test/no\_double\_finalize\_test.cpp} scenario [1]: $W=100$
(uniform $w_i=10$), $\alpha=7$, so $2\lfloor 2W/3\rfloor+2-W=34$; $f=4$ equivocators
($40\ge 34$ stake) with a $3/3$ honest split finalize both branches, while
\emph{every} honest split at $f=3$ ($30<34$ stake; exhaustively enumerated)
finalizes at most one.
\end{proof}

\section{Liveness (route around faults)}

Let the \emph{non-contributors} for a proposed block $p$ be $N\subseteq V$: every
validator that is down (silent) or wedged (emits no valid \textsc{accept} for $p$),
together with all Byzantine validators (who, worst case, withhold support for $p$).
The live honest contributors are $L=H\setminus N$.

\begin{theorem}[Liveness]\label{thm:live}
If the live honest contributors satisfy $|L|\ge\alpha$ and $w(L)>\lfloor 2W/3\rfloor$
(equivalently $w(N) < W-\lfloor 2W/3\rfloor=\lceil W/3\rceil$), and they all
$\beta$-confirm $p$, then $p$ finalizes on every honest gate using only the votes of
$L$ --- no input from $N$ is required.
\end{theorem}
\begin{proof}
$L$ meets all three finality conditions: (C) by $|L|\ge\alpha$; (S) by
$w(L)>\lfloor 2W/3\rfloor$; (V) because each $v_i\in L$ is honest and signs $\mu(p)$
genuinely. Since the rule is monotone (adding the missing $N$ votes can only keep a
position final), $L$ alone certifies $p$: a down or wedged validator is routed
around, never waited on. A wedged validator that floods \emph{garbage} (bad-signature
votes, or votes for an unopened position) is harmless: such inputs fail (V) or are
rejected before collection, so they are evicted at the quorum check and never join a
finalizing $Q$ (\texttt{quorum\_cert\_engine.cpp}: batch verify $+$
\texttt{evict\_invalid}). Combined with Theorem~\ref{thm:agree}, when
$w(N)<\lceil W/3\rceil$ the protocol both makes progress and forks nowhere ---
self-healing across heights without manual intervention.
\end{proof}

\noindent The concrete instantiation $W=100$, $w_i=10$, $\alpha=7$ gives
$\lfloor 2W/3\rfloor=66$: $|L|=7$ live ($70>66$) finalizes with $3$ down; $|L|=6$
($60\le 66$) safely stalls (no fork) --- the boundary of Theorem~\ref{thm:live},
witnessed in \texttt{test/liveness\_test.cpp} and, over real TCP, in
\texttt{node2/test/node2\_liveness\_test.cpp}.

\section{Acceptance window}

The leaderless gate has no proposer ``turn''. Eligibility degenerates to: (i) a
position collects votes only after \texttt{submit} opens it
(\texttt{RejectedNoSuchBlock} otherwise --- no early acceptance), and (ii) every vote
and cert binds $\mu(p)=(b,h,e,\dots)$, so a stale/cross-position signature is not
liftable (it fails (V)). Out-of-set, forged, stale, sub-quorum, and tampered inputs
all fail one of (C),(S),(V); cert re-verification (\texttt{verify\_cert}) recomputes
(C),(S) from the authoritative set and checks the aggregate signature, never trusting
cert-carried fields. See \texttt{test/out\_of\_turn\_test.cpp}. A future node2
proposer schedule adds a deterministic eligible-proposer predicate \emph{on top of}
these invariants; it does not change them.

\section{Round-scoped refinement (view-change): liveness under competing siblings}
\label{sec:roundscoped}

The height-only slot of Definition~\ref{def:nonequiv} makes the \emph{signature}
irrevocable: an honest validator signs \textsc{accept} for at most one block per height
\emph{across its entire execution}. This is what gives Agreement
(Theorem~\ref{thm:agree}) --- but it is \emph{also} a liveness hazard when competing
siblings appear at one height under a zero-margin quorum (the operational $415\!\to\!416$
freeze). If honest validators bind their one signature to \emph{different} siblings ---
which asynchronous, asymmetric gossip forces the moment the settle window is shorter than
the sibling-propagation delay --- no sibling reaches $\alpha$, and the irrevocable rule
forbids any validator from switching. The split is \emph{permanent}: a pure liveness
deadlock with zero Byzantine faults. Formally, with $n$ honest validators exactly equal to
$\alpha$ (one validator down), a single validator bound to a losing sibling makes $\alpha$
unreachable forever.

\paragraph{The refinement.}
Replace the height-only irrevocable signature with a two-phase, round-scoped protocol
(Tendermint/HotStuff view-change), \emph{keeping} the finality rule (C),(S),(V)
unchanged. For each height $h$ run rounds $r=0,1,2,\dots$. Each validator maintains a
lock $(\ell_r,\ell_b)\in(\mathbb{N}\times\mathrm{Id})\cup\{\bot\}$, initially $\bot$.
\begin{itemize}
  \item \textbf{Prevote (non-binding).} In round $r$ a validator casts \emph{one} signed
        \textsc{prevote} (domain \texttt{LUX/chain/prevote/v1}, disjoint from
        $\mu(p)$) for a target value. Prevotes are \emph{fluid}: a validator prevotes a
        different value in a later round freely, subject only to the lock rule below.
  \item \textbf{POL.} A \emph{proof-of-lock} $\mathrm{POL}(v,r)$ is a set of
        $\ge\alpha$ distinct prevotes for value $v$ at round $r$. Because a validator
        casts at most one prevote per $(h,r)$, at most one value attains $\ge\alpha$
        prevotes per round (Lemma~\ref{lem:poluniq}): \emph{a POL is unique per round}.
  \item \textbf{Precommit (binding = the (C),(S),(V) signature).} On observing
        $\mathrm{POL}(v,r)$ at the current round, the validator casts its \textsc{accept}
        signature over $\mu(v)$ and \textsc{locks} $(\ell_r,\ell_b)\gets(r,v)$. This is
        the \emph{one} irrevocable cert vote, now scoped to $(h,r)$.
  \item \textbf{Lock/unlock.} A locked validator prevotes $\ell_b$, and may prevote a
        conflicting $v'\neq\ell_b$ in round $r'>r$ \emph{only} if it has observed
        $\mathrm{POL}(v',r'')$ for some $r''>\ell_r$ (a fresher justification).
  \item \textbf{Round-skip (liveness).} On observing prevotes/precommits from $\ge f{+}1$
        \emph{distinct} validators at a round $r>$ its own, at least one is honest and
        genuinely ahead, so the validator jumps to round $r$. This re-aligns a validator
        left phase-offset by asymmetric gossip (the residual freeze).
\end{itemize}

\begin{lemma}[POL uniqueness]\label{lem:poluniq}
For any height $h$ and round $r$, at most one value $v$ satisfies
$|\{\text{honest prevotes for }v\text{ at }(h,r)\}|+f_{\mathrm{cnt}}\ge\alpha$, where
$f_{\mathrm{cnt}}\le f$ is the Byzantine count. Two values each reaching $\alpha$ prevotes
would need $\ge 2\alpha-n$ validators prevoting both at round $r$; honest validators cast
one prevote per $(h,r)$, so those are Byzantine, requiring $2\alpha-n\le f$. Under the
$\alpha$-bound $2\alpha-n>f$ this is impossible. $\qed$
\end{lemma}

\begin{theorem}[Agreement, round-scoped]\label{thm:agree-rs}
Under $2\alpha-n>f$ (equivalently on the stake metric $2w(\text{quorum})-W>f$), no two
conflicting siblings both finalize at one height. \emph{Proof sketch.} A value $v$
finalizes only via $\ge\alpha$ precommits at a common round $r$; by the precommit rule
each such signer holds a lock $(\,\ge r? ,v)$ formed on $\mathrm{POL}(v,r)$. For a
conflicting $v'$ to finalize at round $r'>r$, $\ge\alpha$ precommit $v'$, so
$\mathrm{POL}(v',r')$ exists; the $\ge 2\alpha-n$ validators in both quorums are locked on
$v$ at rounds $\le r$ and, by the lock rule, prevote $v'$ at $r'$ only with
$\mathrm{POL}(v',r'')$, $r''>r$. Take the \emph{least} such $r^\star>r$: at $r^\star$,
$\ge\alpha$ prevote $v'$, but $\ge 2\alpha-n>f$ of them are honest and locked on $v$ at
rounds $<r^\star$ with no qualifying earlier POL --- contradiction. Hence no such $v'$
finalizes; a single finalized value per height, preserving the guarantee of
Theorem~\ref{thm:agree}. The round-scoping refines the slot from $h$ to $(h,r)$; the
finality conditions (C),(S),(V) are unchanged. $\qed$
\end{theorem}

\begin{theorem}[Liveness, round-scoped]\label{thm:live-rs}
Under eventual synchrony and $f<W/3$, every height finalizes. Prevotes are fluid, so a
split round forms no POL and locks nobody (locking requires a POL); round-skip re-aligns
lagging honest validators to a common round; all honest validators converge their prevote
on the value carrying the highest-round POL (\emph{validValue}, computed from the shared
gossiped tallies), so within $O(1)$ synchronous rounds $\ge\alpha$ prevote one value, a
POL forms, they precommit, and (C),(S),(V) are met. A durable per-height
\emph{lock round} (v3 vote-guard) lets a restarted validator re-converge rather than
stall. $\qed$
\end{theorem}

\paragraph{Tightness.} The $\alpha$-bound $2\alpha-n>f$ is tight: at $2\alpha-n=f$
(e.g. $n=5,\alpha=3,f=1$) a single equivocator sits in two disjoint $\alpha$-quorums and
double-finalizes; the engine \emph{refuses} to run the view-change (fail-secure halt) on
any committee failing the bound. This mirrors Theorem~\ref{thm:tight} on the round-scoped
slot.

\paragraph{Go\,$\leftrightarrow$\,C++ parity (delta).}
The round-scoped view-change ships in the Go reference
\texttt{luxfi/consensus} \texttt{v1.35.6} (\texttt{engine/chain/round\_view.go}:
prevote/POL/lock/unlock/round-skip; \texttt{integration.go}: the driver + prevote
gossip; \texttt{vote\_guard.go}: v3 lock-round persistence), \emph{opt-in} per network
(\texttt{config.ViewChange}, default off; the legacy height-only path of
\S\ref{sec:roundscoped} preamble is unchanged when off), and is proven there by an
adversarial suite (an $f{=}1$ equivocator that double-prevotes and double-precommits every
sibling at every round; $0/200$ non-uniform-visibility liveness; a storm under the race
detector; the $\alpha{=}3$ tightness fork). \texttt{consensus} currently implements the
\emph{height-only} \texttt{committed\_slot\_} of \S\ref{sec:model} (\texttt{src/node.cpp}):
Theorem~\ref{thm:agree} holds, but it is subject to the competing-sibling liveness
deadlock above. Porting \texttt{round\_view.go} to a \texttt{round\_view.hpp/cpp} on top of
the existing \texttt{wave} preference layer (whose confidence-reset-on-switch already
models fluid preference) --- and wiring the prevote message into \texttt{Node} --- is the
tracked follow-up to restore full Go$\leftrightarrow$C++ parity; Theorems~\ref{thm:agree-rs}
and~\ref{thm:live-rs} are the specification it must satisfy.

\section{Relation to avalanche}

The gate \emph{extends} the avalanche/snow family without weakening it: the liveness/
preference layer (\texttt{photon} sampling $+$ \texttt{wave}/focus $\beta$-confidence,
ported from \texttt{luxfi/consensus}) decides \emph{which} block honest validators
prefer, exactly as snowball does; the cryptographic finality (a signed $>2/3$-stake
quorum certificate) replaces the implicit ``$k$ consecutive polls'' commit with an
explicit, portable, post-quantum-upgradeable witness. Theorems~\ref{thm:agree}
and~\ref{thm:live} reproduce avalanche's $f<n/3$ safety and liveness on the stake
metric; Theorem~\ref{thm:tight} shows the threshold is identical, not merely
sufficient. The PQ extension (Pulsar / Corona / Magnetar) changes only the contents
of condition (V) --- the signature scheme verified per voter --- leaving (C),(S), the
non-equivocation discipline, and all three theorems unchanged.

\end{document}