4a0b48588c
Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so.
163 lines
8.3 KiB
Python
163 lines
8.3 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# qbft_liveness_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) LIVENESS argument for AERE QBFT / IBFT 2.0 under PARTIAL
|
|
# SYNCHRONY (eventual GST). QBFT/IBFT is a partially-synchronous BFT protocol:
|
|
# SAFETY holds always (proven in qbft_safety_smt.py), and LIVENESS (progress) is
|
|
# guaranteed only AFTER GST, when message delays are bounded and the round
|
|
# timeout is eventually long enough for an honest proposer's block to be seen
|
|
# and committed. We model the standard round-change progress argument.
|
|
#
|
|
# Besu uses ROUND-ROBIN proposer selection: proposer(r) = r mod N over the
|
|
# ordered validator list. quorum(N)=ceil(2N/3), f(N)=floor((N-1)/3).
|
|
#
|
|
# ASSUMPTION (stated honestly -- NOT proven here, it is the protocol's premise):
|
|
# PARTIAL SYNCHRONY / post-GST: after the global stabilization time, an honest
|
|
# proposer's PRE-PREPARE and the honest PREPARE/COMMIT messages all arrive
|
|
# within the (adaptively growing) round timeout. Under this premise a round
|
|
# with an honest proposer COMMITS. Asynchronous liveness is impossible (FLP);
|
|
# we do not claim it.
|
|
#
|
|
# Given that premise we MACHINE-CHECK the two combinatorial facts the liveness
|
|
# argument rests on:
|
|
# L-PROGRESS within any window of (f+1) consecutive rounds, round-robin over N
|
|
# distinct proposers hits at least one HONEST proposer (<= f faulty
|
|
# cannot cover f+1 distinct proposers). N in {4,5,7}.
|
|
# L-COMMIT an honest proposer's round commits, because the honest set alone
|
|
# (N-f) is >= quorum, so honest PREPARE+COMMIT reach quorum. (all N)
|
|
# Together: after GST, within f+1 rounds an honest proposer is elected and that
|
|
# round commits -> the chain makes progress. Liveness.
|
|
#
|
|
# NON-VACUITY: a NEGATIVE CONTROL with f+1 faulty shows a window of f+1 rounds
|
|
# can be ALL faulty proposers (no progress) -> the <= f bound is load-bearing.
|
|
#
|
|
# BOUNDARY: L-PROGRESS/L-COMMIT are bounded per-N checks (plus an unbounded
|
|
# liveness identity). The partial-synchrony premise is ASSUMED. This is the QBFT
|
|
# round-change DESIGN, not the Besu Java code.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat)
|
|
|
|
def quorum(n): return (2 * n + 2) // 3
|
|
def faultbound(n): return (n - 1) // 3
|
|
|
|
results = []
|
|
def check(name, s, expect_unsat=True, kind="PROOF"):
|
|
r = s.check()
|
|
if expect_unsat:
|
|
ok = (r == unsat); tag = "PROVED" if ok else "FAILED"
|
|
else:
|
|
ok = (r == sat); tag = "CEX-FOUND" if ok else "FAILED"
|
|
results.append((name, tag, ok, kind))
|
|
print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})")
|
|
if r == sat:
|
|
m = s.model(); wit = {}
|
|
for d in m.decls():
|
|
try: wit[str(d)] = m[d].as_long()
|
|
except Exception:
|
|
try: wit[str(d)] = bool(m[d])
|
|
except Exception: wit[str(d)] = "?"
|
|
print(" witness:", {k: wit[k] for k in sorted(wit)})
|
|
return ok
|
|
|
|
print("### AERE QBFT / IBFT 2.0 -- LIVENESS under partial synchrony (post-GST round-change)\n")
|
|
print(" round-robin proposer(r)=r mod N; "
|
|
+ ", ".join(f"N={n}: q={quorum(n)}, f={faultbound(n)}, window f+1={faultbound(n)+1}"
|
|
for n in (4, 5, 7)) + "\n")
|
|
|
|
# =============================================================================
|
|
# L-PROGRESS -- within f+1 consecutive rounds an HONEST proposer is elected.
|
|
# proposer(r) = r mod N. Over rounds 0..f, the proposers are f+1 DISTINCT indices
|
|
# (since f+1 <= N). With <= f faulty, at least one of them is honest.
|
|
# Encode: is it possible that EVERY proposer in rounds 0..f is faulty while
|
|
# |faulty| <= f? -> must be UNSAT.
|
|
# =============================================================================
|
|
def progress_window(N, fv):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv) # <= f faulty
|
|
# every proposer in the (f+1)-round window is faulty (negation of progress)
|
|
for r in range(fv + 1):
|
|
proposer = r % N
|
|
s.add(Not(honest[proposer]))
|
|
return s
|
|
for N in (4, 5, 7):
|
|
s = progress_window(N, faultbound(N))
|
|
check(f"L-PROGRESS N={N}: some round in the first f+1={faultbound(N)+1} has an HONEST "
|
|
f"proposer (round-robin, <= f faulty cannot cover the window)", s)
|
|
|
|
# ---- sanity: f+1 <= N so the window proposers are distinct (assumption holds) ---
|
|
for N in (4, 5, 7):
|
|
ok = (faultbound(N) + 1) <= N
|
|
s = Solver(); s.add(Int('d') == (0 if ok else 1)); s.add(Int('d') == 0)
|
|
check(f"L-PROGRESS-sanity N={N}: f+1={faultbound(N)+1} <= N (window has distinct proposers)",
|
|
s, expect_unsat=not ok, kind="CONFIG")
|
|
|
|
# ---- NEG-CTRL L-PROGRESS: with f+1 faulty a window CAN be ALL faulty proposers --
|
|
def progress_window_overbound(N, fplus1):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fplus1) # f+1 faulty allowed
|
|
for r in range(fplus1): # a window of f+1 rounds
|
|
proposer = r % N
|
|
s.add(Not(honest[proposer])) # all faulty proposers
|
|
return s
|
|
for N in (4,):
|
|
s = progress_window_overbound(N, faultbound(N) + 1)
|
|
check(f"NEG-CTRL L-PROGRESS N={N} with f+1={faultbound(N)+1} faulty: a window CAN be all "
|
|
f"faulty proposers -> no progress (the <= f bound is load-bearing)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# L-COMMIT -- an honest proposer's round commits (post-GST): the honest set
|
|
# alone (N-f) reaches PREPARE and COMMIT quorum. This is the N-f >= quorum
|
|
# identity (unbounded, all N) plus per-N witnesses.
|
|
# =============================================================================
|
|
s = Solver()
|
|
N, q, f = Int('N'), Int('q'), Int('f')
|
|
s.add(N >= 1)
|
|
s.add(3 * q >= 2 * N, 3 * q <= 2 * N + 2) # q = ceil(2N/3)
|
|
s.add(3 * f <= N - 1, N - 1 <= 3 * f + 2) # f = floor((N-1)/3)
|
|
s.add(N - f < q) # negate: honest set below quorum
|
|
check("L-COMMIT (all N): honest set N-f >= quorum -> honest PREPARE+COMMIT reach quorum "
|
|
"-> an honest proposer's round commits (post-GST)", s)
|
|
|
|
# explicit per-N: the N-f honest validators all PREPARE and COMMIT the proposal;
|
|
# the commit count reaches quorum -> the block commits (progress). Non-vacuous.
|
|
def honest_round_commits(N, qv, fv):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
commit = [Bool(f'commit_{i}') for i in range(N)]
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv)
|
|
for i in range(N):
|
|
s.add(Implies(honest[i], commit[i])) # post-GST: honest all commit the proposal
|
|
s.add(Sum([If(commit[i], 1, 0) for i in range(N)]) >= qv) # commit quorum reached
|
|
return s
|
|
for N in (4, 5, 7):
|
|
s = honest_round_commits(N, quorum(N), faultbound(N))
|
|
check(f"L-COMMIT N={N}: honest set alone reaches the COMMIT quorum {quorum(N)} "
|
|
f"(round with honest proposer makes progress)", s,
|
|
expect_unsat=False, kind="WITNESS")
|
|
|
|
# =============================================================================
|
|
print("\n=== SUMMARY (QBFT LIVENESS under partial synchrony) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" ESTABLISHED (under the PARTIAL-SYNCHRONY / post-GST premise): after GST,")
|
|
print(" round-robin round changes elect an HONEST proposer within any f+1-round")
|
|
print(" window (L-PROGRESS), and an honest proposer's round COMMITS because the")
|
|
print(" honest set alone (N-f) >= quorum (L-COMMIT) -> the chain makes progress.")
|
|
print(" The negative control FIRES: with f+1 faulty a whole window can be faulty")
|
|
print(" proposers, so the <= f bound is load-bearing for liveness. HONEST NOTE:")
|
|
print(" the partial-synchrony premise is ASSUMED, not proven (asynchronous")
|
|
print(" liveness is impossible by FLP); these are bounded per-N checks plus an")
|
|
print(" unbounded N-f>=quorum identity; DESIGN combinatorics, not Besu bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|