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.
224 lines
12 KiB
Python
224 lines
12 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# qbft_prepare_counting_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) model of the EXACT interop defect fixed on 2026-07-14 in
|
|
# the AERE second execution client (patched Nethermind QBFT producer), and of
|
|
# the fix that closed it. This turns a field bug + empirical soak result into a
|
|
# re-runnable formal artifact, and proves the fix is SAFE.
|
|
#
|
|
# THE DEFECT (observed against Hyperledger Besu 26.4.0 on an isolated testnet):
|
|
# Besu tallies the PREPARE quorum from EXPLICIT Prepare messages. It does NOT
|
|
# count the Proposal as an implicit Prepare from the proposer. The Nethermind
|
|
# proposer emitted a Proposal but no explicit self-Prepare, so a block it
|
|
# proposed was left one Prepare short of quorum and never committed -> the
|
|
# chain stalled. Empirically this bit ONLY at the fault boundary (kill 2 of 7,
|
|
# f=2): throughput collapsed from Besu-parity to ~1/3. THE FIX: the proposer
|
|
# now also broadcasts an explicit Prepare for its own block (round 0 and
|
|
# round>0). After the fix the mixed 3-Besu+2-NM set ran at Besu parity.
|
|
#
|
|
# Besu formulas: quorum(N)=ceil(2N/3)=fastDivCeiling(2N,3); f(N)=floor((N-1)/3).
|
|
#
|
|
# WHY THE BUG IS EXACTLY A FAULT-BOUNDARY BUG (the arithmetic this model proves):
|
|
# With D validators down and the proposer alive, the explicit Prepares available
|
|
# are (alive non-proposers) = N-D-1 under the BUGGY rule, or N-D under the FIXED
|
|
# rule (proposer adds its own). At the boundary D=f and the optimal size N=3f+1:
|
|
# alive A = N-f = 2f+1 = quorum(N)
|
|
# BUGGY count = A-1 = 2f = quorum-1 -> DEADLOCK (1 short), even all-honest
|
|
# FIXED count = A = 2f+1 = quorum -> COMMITS (exactly meets quorum)
|
|
# For D<f the buggy rule still reaches quorum, which is why the defect only
|
|
# surfaced under the kill-2 (f=2) adversarial soak, not in the healthy set.
|
|
#
|
|
# PROPERTIES (each a PROOF paired with a firing NEGATIVE CONTROL, per the
|
|
# formal-consensus/ house convention -> non-vacuous):
|
|
# P1 BUGGY RULE => GUARANTEED STALL at D=f: even with every alive validator
|
|
# honest and preparing, the explicit-Prepare count cannot reach quorum.
|
|
# (bounded per-N, PROVED unsat). Neg-control: FIXED rule same config is
|
|
# committable (SAT) -> the missing self-Prepare is the whole cause.
|
|
# P2 FIXED RULE => LIVENESS RESTORED for ALL N (UNBOUNDED, Presburger): the
|
|
# alive honest set at the boundary, N-f, is >= quorum(N). Neg-control:
|
|
# the BUGGY count N-f-1 < quorum(N) for some N (SAT) -> load-bearing.
|
|
# P3 FIXED RULE PRESERVES SAFETY: adding the proposer's single honest explicit
|
|
# Prepare (to the one value it proposed) cannot make two distinct values
|
|
# both reach quorum, under <= f equivocating Byzantine validators (bounded
|
|
# per-N, PROVED unsat). Neg-control: lowering the quorum to ceil(N/2)
|
|
# lets two values both commit (SAT) -> the quorum threshold, not the
|
|
# implicit/explicit distinction, is what carries safety; the fix is neutral
|
|
# to it.
|
|
#
|
|
# HONEST BOUNDARY:
|
|
# * P1/P3 are BOUNDED per-N checks (decision procedures over finite configs),
|
|
# P2 is an UNBOUNDED arithmetic identity over all N. None is a proof of the
|
|
# Besu/Nethermind bytecode; this models the QBFT PREPARE-counting rule and
|
|
# the round's message combinatorics. It is consistent with, and explains,
|
|
# the empirical soaks (0 forks; parity throughput after the fix).
|
|
# * Chain 2800 consensus is classical ECDSA QBFT (NOT post-quantum). This model
|
|
# is about the second-client interop, orthogonal to the Falcon layer.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat)
|
|
|
|
def quorum(n): return (2 * n + 2) // 3 # ceil(2N/3)
|
|
def faultbound(n): return (n - 1) // 3 # floor((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 and not expect_unsat:
|
|
pass
|
|
return ok
|
|
|
|
# Optimal BFT sizes N = 3f+1 where the boundary is tightest (A = quorum exactly).
|
|
OPTIMAL_N = [4, 7, 10, 13]
|
|
ALL_N = [4, 5, 7, 10, 13, 16, 22]
|
|
|
|
print("=" * 78)
|
|
print("P1 BUGGY RULE => GUARANTEED STALL at the fault boundary D=f")
|
|
print("=" * 78)
|
|
# Faithful per-validator model of ONE round's PREPARE tally under the BUGGY rule.
|
|
# Validators 0..N-1; proposer is index 0 and is alive (else round-change). D=f of
|
|
# the OTHERS are crashed (down). Every alive non-proposer is HONEST and Prepares.
|
|
# Under the buggy rule the proposer emits NO explicit self-Prepare.
|
|
for N in OPTIMAL_N:
|
|
f = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
down = [Bool(f"down_{i}") for i in range(N)]
|
|
prep = [Bool(f"prep_{i}") for i in range(N)]
|
|
s.add(Not(down[0])) # proposer alive
|
|
s.add(Sum([If(down[i], 1, 0) for i in range(1, N)]) == f) # exactly f others down
|
|
s.add(Sum([If(down[i], 1, 0) for i in range(N)]) == f) # total down = f
|
|
for i in range(N):
|
|
s.add(Implies(down[i], Not(prep[i]))) # crashed -> no message
|
|
for i in range(1, N):
|
|
s.add(Implies(Not(down[i]), prep[i])) # alive honest non-proposer Prepares
|
|
s.add(Not(prep[0])) # BUGGY: proposer sends no explicit Prepare
|
|
count = Sum([If(prep[i], 1, 0) for i in range(N)])
|
|
s.add(count >= q) # try to reach quorum -> should be impossible
|
|
check(f"N={N} f={f} q={q}: buggy rule (no self-Prepare), D=f down, all-honest "
|
|
f"=> explicit-Prepare count reaches quorum", s, expect_unsat=True, kind="PROOF")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P1-NEG Same config but the FIXED rule (proposer self-Prepares) IS committable")
|
|
print("=" * 78)
|
|
for N in OPTIMAL_N:
|
|
f = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
down = [Bool(f"down_{i}") for i in range(N)]
|
|
prep = [Bool(f"prep_{i}") for i in range(N)]
|
|
s.add(Not(down[0]))
|
|
s.add(Sum([If(down[i], 1, 0) for i in range(1, N)]) == f)
|
|
s.add(Sum([If(down[i], 1, 0) for i in range(N)]) == f)
|
|
for i in range(N):
|
|
s.add(Implies(down[i], Not(prep[i])))
|
|
for i in range(1, N):
|
|
s.add(Implies(Not(down[i]), prep[i]))
|
|
s.add(prep[0]) # FIX: proposer self-Prepares (alive)
|
|
count = Sum([If(prep[i], 1, 0) for i in range(N)])
|
|
s.add(count >= q) # quorum reachable?
|
|
check(f"N={N} f={f} q={q}: fixed rule (self-Prepare), D=f down, all-honest "
|
|
f"=> quorum {q} reachable", s, expect_unsat=False, kind="NEG-CONTROL")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P2 FIXED RULE => LIVENESS RESTORED for ALL N (unbounded Presburger)")
|
|
print("=" * 78)
|
|
# Unbounded: for EVERY N>=1, the alive honest set at the boundary D=f has size
|
|
# N-f(N) and meets quorum(N). Prove the negation UNSAT over all N.
|
|
n = Int("N"); f = Int("f"); q = Int("q")
|
|
s = Solver()
|
|
s.add(n >= 1)
|
|
s.add(f * 3 <= n - 1); s.add((f + 1) * 3 > n - 1) # f = floor((N-1)/3)
|
|
s.add(q * 3 >= 2 * n); s.add((q - 1) * 3 < 2 * n) # q = ceil(2N/3)
|
|
s.add((n - f) < q) # negation: fixed count falls short
|
|
check("ALL N: fixed alive-honest set (N-f) >= quorum(N) at the boundary D=f "
|
|
"(liveness restored everywhere)", s, expect_unsat=True, kind="PROOF")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P2-NEG BUGGY count (N-f-1) falls short of quorum for some N (load-bearing)")
|
|
print("=" * 78)
|
|
n = Int("N"); f = Int("f"); q = Int("q")
|
|
s = Solver()
|
|
s.add(n >= 1)
|
|
s.add(f * 3 <= n - 1); s.add((f + 1) * 3 > n - 1)
|
|
s.add(q * 3 >= 2 * n); s.add((q - 1) * 3 < 2 * n)
|
|
s.add((n - f - 1) < q) # buggy count strictly below quorum
|
|
check("EXISTS N: buggy count (N-f-1) < quorum(N) -> a real deadlock exists "
|
|
"(so the self-Prepare is load-bearing for liveness)", s, expect_unsat=False, kind="NEG-CONTROL")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P3 FIXED RULE PRESERVES SAFETY (no two values both reach quorum)")
|
|
print("=" * 78)
|
|
# Two candidate values v0,v1. Each HONEST validator Prepares exactly one value
|
|
# (the value it accepted); up to f BYZANTINE validators may equivocate and Prepare
|
|
# BOTH. The proposer is honest and, under the fix, Prepares its one proposed value
|
|
# explicitly. Assert BOTH values reach quorum -> must be UNSAT.
|
|
for N in [4, 7, 10, 13]:
|
|
fb = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
byz = [Bool(f"byz_{i}") for i in range(N)]
|
|
p0 = [Bool(f"p0_{i}") for i in range(N)] # validator i Prepares value 0
|
|
p1 = [Bool(f"p1_{i}") for i in range(N)] # validator i Prepares value 1
|
|
s.add(Sum([If(byz[i], 1, 0) for i in range(N)]) <= fb) # <= f Byzantine
|
|
for i in range(N):
|
|
# honest validators Prepare exactly one value; Byzantine may do anything
|
|
s.add(Implies(Not(byz[i]), Not(And(p0[i], p1[i]))))
|
|
# proposer (index 0) is honest and Prepares its proposed value (say v0) explicitly.
|
|
s.add(Not(byz[0])); s.add(p0[0]); s.add(Not(p1[0]))
|
|
c0 = Sum([If(p0[i], 1, 0) for i in range(N)])
|
|
c1 = Sum([If(p1[i], 1, 0) for i in range(N)])
|
|
s.add(c0 >= q); s.add(c1 >= q) # both reach quorum -> impossible?
|
|
check(f"N={N} f={fb} q={q}: with the proposer's explicit self-Prepare, two "
|
|
f"distinct values BOTH reach quorum (safety break)", s, expect_unsat=True, kind="PROOF")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P3-NEG Lowering quorum to ceil(N/2) DOES break safety (threshold is load-bearing)")
|
|
print("=" * 78)
|
|
for N in [4, 7, 10]:
|
|
fb = faultbound(N); qbad = (N + 1) // 2 # ceil(N/2) -- too low
|
|
s = Solver()
|
|
byz = [Bool(f"byz_{i}") for i in range(N)]
|
|
p0 = [Bool(f"p0_{i}") for i in range(N)]
|
|
p1 = [Bool(f"p1_{i}") for i in range(N)]
|
|
s.add(Sum([If(byz[i], 1, 0) for i in range(N)]) <= fb)
|
|
for i in range(N):
|
|
s.add(Implies(Not(byz[i]), Not(And(p0[i], p1[i]))))
|
|
s.add(Not(byz[0])); s.add(p0[0]); s.add(Not(p1[0]))
|
|
c0 = Sum([If(p0[i], 1, 0) for i in range(N)])
|
|
c1 = Sum([If(p1[i], 1, 0) for i in range(N)])
|
|
s.add(c0 >= qbad); s.add(c1 >= qbad)
|
|
check(f"N={N} f={fb} qbad=ceil(N/2)={qbad}: two values both reach the LOWERED "
|
|
f"quorum (safety violated)", s, expect_unsat=False, kind="NEG-CONTROL")
|
|
|
|
# =============================================================================
|
|
print("\n=== SUMMARY (QBFT explicit-Prepare counting: the 2026-07-14 bug + fix) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" ESTABLISHED: Besu's explicit-Prepare quorum rule makes a proposer that")
|
|
print(" omits its own self-Prepare deadlock EXACTLY at the fault boundary D=f")
|
|
print(" (P1: N-f-1 = quorum-1, one short, proven for N=3f+1). The 2026-07-14 fix")
|
|
print(" -- proposer broadcasts an explicit self-Prepare -- restores liveness for")
|
|
print(" ALL N (P2: N-f >= quorum, unbounded) and is SAFETY-NEUTRAL (P3: one extra")
|
|
print(" honest Prepare to a single value cannot make two values both reach quorum;")
|
|
print(" safety rests on the ceil(2N/3) threshold, unchanged by the fix). Every")
|
|
print(" negative control FIRED (non-vacuous). This matches the empirical soaks:")
|
|
print(" 0 forks throughout, and Besu-parity throughput once the self-Prepare lands.")
|
|
print(" HONEST: bounded per-N checks + one unbounded identity; QBFT Prepare-tally")
|
|
print(" DESIGN combinatorics, not Besu/Nethermind bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|