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.
254 lines
13 KiB
Python
254 lines
13 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# qbft_safety_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) SAFETY (AGREEMENT) of AERE consensus: QBFT / IBFT 2.0
|
|
# (Hyperledger Besu, chain 2800). No two DIFFERENT blocks are ever committed at
|
|
# the same height, given <= f Byzantine validators that may equivocate / double-
|
|
# sign up to f.
|
|
#
|
|
# Besu quorum: quorum(N) = ceil(2N/3) (fastDivCeiling(2N,3))
|
|
# BFT fault bound: f(N) = floor((N-1)/3)
|
|
# (For the optimal N = 3f+1 sizes this is the classic "2f+1 of 3f+1".)
|
|
#
|
|
# Three layers, increasing faithfulness:
|
|
# L1 QUORUM-INTERSECTION LEMMA -- UNBOUNDED in N (z3 over Presburger/LIA):
|
|
# any two quorums intersect in >= 2q-N validators, and 2q-N >= f+1 for
|
|
# EVERY N. => any two commit quorums share at least one HONEST validator.
|
|
# L2 ONE-ROUND AGREEMENT -- bounded model check, explicit per-validator
|
|
# COMMIT with an equivocating Byzantine adversary, N in {4,5,7}.
|
|
# L3 CROSS-ROUND AGREEMENT (IBFT 2.0 locking / round-change justification)
|
|
# -- bounded per-validator model over R rounds, N in {4,5,7}. This is the
|
|
# subtle case: even across round changes no two rounds commit different
|
|
# values, because honest validators LOCK on the highest prepared value.
|
|
#
|
|
# NON-VACUITY (rigor): each layer is paired with a NEGATIVE CONTROL that LOWERS
|
|
# the quorum to ceil(N/2) (or DROPS the locking rule) and the checker MUST find
|
|
# an agreement violation (SAT). If a negative control did NOT fire, the model
|
|
# would be vacuous.
|
|
#
|
|
# HONEST BOUNDARY:
|
|
# * L1 is an unbounded arithmetic proof of the intersection bound (all N).
|
|
# * L2/L3 are BOUNDED model checks (N in {4,5,7,10,13,16} for L2, {4,5,7,10,13}
|
|
# for L3; L3 fixed R rounds).
|
|
# A bounded model check is NOT a proof for all N or all executions; it is a
|
|
# decision procedure over the stated finite configuration. Stated honestly.
|
|
# * This models the QBFT message combinatorics / locking DESIGN, not the Besu
|
|
# Java bytecode. Chain 2800 consensus is classical ECDSA QBFT (NOT post-
|
|
# quantum); the Falcon layer is modeled separately (falcon_*_smt.py).
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat)
|
|
|
|
# ---- Besu quorum / fault formulas (Python, for the bounded per-N layers) -----
|
|
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:
|
|
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)] = "?"
|
|
# keep the witness compact
|
|
print(" witness:", {k: wit[k] for k in sorted(wit)})
|
|
return ok
|
|
|
|
print("### AERE QBFT / IBFT 2.0 -- SAFETY (agreement): no two different blocks committed at one height\n")
|
|
print(f" quorum(N)=ceil(2N/3), f(N)=floor((N-1)/3): "
|
|
+ ", ".join(f"N={n}->q={quorum(n)},f={faultbound(n)}" for n in (4, 5, 7)) + "\n")
|
|
|
|
# =============================================================================
|
|
# L1 QUORUM-INTERSECTION LEMMA (UNBOUNDED in N, decidable LIA)
|
|
# -----------------------------------------------------------------------------
|
|
# For a universe of N validators, any two subsets Q_A, Q_B with |Q_A|,|Q_B| >= q
|
|
# satisfy (inclusion-exclusion) |Q_A ∩ Q_B| >= |Q_A| + |Q_B| - N >= 2q - N.
|
|
# We prove the ARITHMETIC core: for EVERY N>=1, with q=ceil(2N/3) and
|
|
# f=floor((N-1)/3), 2q - N >= f + 1. Hence any two quorums overlap in strictly
|
|
# more than f validators => the overlap contains at least one HONEST validator.
|
|
# =============================================================================
|
|
def add_quorum_def(s, N, q):
|
|
# q == ceil(2N/3) <=> 2N <= 3q <= 2N+2
|
|
s.add(3 * q >= 2 * N, 3 * q <= 2 * N + 2)
|
|
def add_faultbound_def(s, N, f):
|
|
# f == floor((N-1)/3) <=> 3f <= N-1 <= 3f+2
|
|
s.add(3 * f <= N - 1, N - 1 <= 3 * f + 2)
|
|
|
|
s = Solver()
|
|
N, q, f = Int('N'), Int('q'), Int('f')
|
|
s.add(N >= 1)
|
|
add_quorum_def(s, N, q)
|
|
add_faultbound_def(s, N, f)
|
|
s.add(2 * q - N <= f) # negate: intersection bound <= f (want >= f+1)
|
|
check("L1 quorum-intersection: 2*quorum(N)-N >= f(N)+1 for ALL N (unbounded LIA proof)", s)
|
|
|
|
# ---- NEG-CTRL L1: a majority quorum ceil(N/2) does NOT guarantee an honest overlap
|
|
s = Solver()
|
|
N, q, f = Int('N'), Int('q'), Int('f')
|
|
s.add(N >= 1)
|
|
s.add(3 * f <= N - 1, N - 1 <= 3 * f + 2) # real fault bound
|
|
# BUG: q == ceil(N/2) <=> N <= 2q <= N+1
|
|
s.add(2 * q >= N, 2 * q <= N + 1)
|
|
s.add(2 * q - N <= f) # find an N where overlap can be <= f (no honest overlap guaranteed)
|
|
check("NEG-CTRL majority quorum ceil(N/2): intersection CAN be <= f (no honest overlap)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# L2 ONE-ROUND AGREEMENT -- bounded, explicit per-validator, equivocating adversary
|
|
# -----------------------------------------------------------------------------
|
|
# Per validator i: honest_i, cA_i (COMMIT for block A), cB_i (COMMIT for B).
|
|
# * HONEST validator commits at most ONE value in a round: honest_i => !(cA_i & cB_i)
|
|
# * BYZANTINE validator is unconstrained: it may double-sign (cA_i & cB_i both true)
|
|
# * adversary controls at most f validators (|faulty| <= f)
|
|
# A and B are DISTINCT blocks. If both reach a COMMIT quorum, agreement is broken.
|
|
# Claim: with the real quorum ceil(2N/3), this is UNSAT for N in {4,5,7}. PROVED.
|
|
# =============================================================================
|
|
def one_round_agreement(N, qv, fv):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
cA = [Bool(f'cA_{i}') for i in range(N)]
|
|
cB = [Bool(f'cB_{i}') for i in range(N)]
|
|
# adversary controls <= f validators
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv)
|
|
# honest commit at most one value; faulty unconstrained (may equivocate)
|
|
for i in range(N):
|
|
s.add(Implies(honest[i], Not(And(cA[i], cB[i]))))
|
|
# both blocks reach a commit quorum
|
|
s.add(Sum([If(cA[i], 1, 0) for i in range(N)]) >= qv)
|
|
s.add(Sum([If(cB[i], 1, 0) for i in range(N)]) >= qv)
|
|
return s
|
|
|
|
for N in (4, 5, 7, 10, 13, 16):
|
|
s = one_round_agreement(N, quorum(N), faultbound(N))
|
|
check(f"L2 one-round agreement N={N} (q={quorum(N)},f={faultbound(N)}): "
|
|
f"two blocks cannot both reach COMMIT quorum", s)
|
|
|
|
# ---- NEG-CTRL L2: lower the quorum to ceil(N/2) -> two blocks CAN both "commit"
|
|
def ceil_half(n): return (n + 1) // 2
|
|
for N in (4,):
|
|
s = one_round_agreement(N, ceil_half(N), faultbound(N))
|
|
check(f"NEG-CTRL L2 majority quorum ceil(N/2)={ceil_half(N)} at N={N}: "
|
|
f"agreement VIOLATED (two blocks both reach the lowered quorum)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# L3 CROSS-ROUND AGREEMENT (IBFT 2.0 locking / round-change justification)
|
|
# -----------------------------------------------------------------------------
|
|
# The subtle case: round changes. A value can be COMMITTED at round r only if a
|
|
# quorum COMMITs it, which requires those validators PREPARED it at r (saw a
|
|
# prepare-quorum). IBFT 2.0's round-change justification forces the proposer of a
|
|
# later round to re-propose the value of the HIGHEST prepared round; honest
|
|
# validators LOCK: they only PREPARE the highest previously-prepared value.
|
|
#
|
|
# Faithful bounded encoding, per validator i, per round r in 0..R-1:
|
|
# prep[i][r] in {0=none,1=A,2=B} -- value i broadcast PREPARE for at round r
|
|
# comm[i][r] in {0=none,1=A,2=B} -- value i broadcast COMMIT for at round r
|
|
# Derived per round r:
|
|
# preparedA[r] := (#prep==A) >= q , preparedB[r] := (#prep==B) >= q
|
|
# committedA[r]:= (#comm==A) >= q , committedB[r]:= (#comm==B) >= q
|
|
# Honest rules (Byzantine validators are UNCONSTRAINED -- may equivocate):
|
|
# (H-commit) honest commits v at r => it PREPARED v at r AND a prepare-quorum
|
|
# for v formed at r.
|
|
# (H-lock/H2')honest PREPARES v at r>0 => either NO earlier round has a
|
|
# prepare-quorum, OR v == value of the HIGHEST earlier round that
|
|
# did (the lock). [This is the IBFT 2.0 round-change justification;
|
|
# it is SOUND because a size-q round-change quorum intersects every
|
|
# earlier prepare-quorum in an honest validator (L1), which carries
|
|
# that prepared certificate forward.]
|
|
# Property (agreement): NOT( committedA[r1] for some r1 AND committedB[r2] for
|
|
# some r2 ). Claim UNSAT for N in {4,5,7}, R rounds. PROVED.
|
|
# =============================================================================
|
|
NONE, A, B = 0, 1, 2
|
|
|
|
def cross_round_model(N, qv, fv, R, locking=True):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
prep = [[Int(f'prep_{i}_{r}') for r in range(R)] for i in range(N)]
|
|
comm = [[Int(f'comm_{i}_{r}') for r in range(R)] for i in range(N)]
|
|
for i in range(N):
|
|
for r in range(R):
|
|
s.add(prep[i][r] >= NONE, prep[i][r] <= B)
|
|
s.add(comm[i][r] >= NONE, comm[i][r] <= B)
|
|
# adversary controls <= f validators
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv)
|
|
|
|
def cnt(mat, r, v): return Sum([If(mat[i][r] == v, 1, 0) for i in range(N)])
|
|
preparedA = [cnt(prep, r, A) >= qv for r in range(R)]
|
|
preparedB = [cnt(prep, r, B) >= qv for r in range(R)]
|
|
prepared_val = [If(preparedA[r], A, If(preparedB[r], B, NONE)) for r in range(R)]
|
|
committedA = [cnt(comm, r, A) >= qv for r in range(R)]
|
|
committedB = [cnt(comm, r, B) >= qv for r in range(R)]
|
|
|
|
# highest earlier prepared value at round r (scan r-1 down to 0)
|
|
def highest_prior(r):
|
|
hp = NONE
|
|
for rp in range(r - 1, -1, -1):
|
|
hp = If(prepared_val[rp] != NONE, prepared_val[rp], hp)
|
|
return hp
|
|
|
|
for i in range(N):
|
|
for r in range(R):
|
|
# (H-commit): honest commits v => prepared v at r AND prepare-quorum for v at r
|
|
s.add(Implies(And(honest[i], comm[i][r] == A),
|
|
And(prep[i][r] == A, preparedA[r])))
|
|
s.add(Implies(And(honest[i], comm[i][r] == B),
|
|
And(prep[i][r] == B, preparedB[r])))
|
|
if locking and r > 0:
|
|
hp = highest_prior(r)
|
|
# (H-lock): honest prepares v (v!=NONE) with some earlier prepared
|
|
# round present => v must equal the highest prior prepared value.
|
|
s.add(Implies(And(honest[i], prep[i][r] != NONE, hp != NONE),
|
|
prep[i][r] == hp))
|
|
return s, committedA, committedB
|
|
|
|
for N in (4, 5, 7, 10, 13):
|
|
R = 3
|
|
s, cA, cB = cross_round_model(N, quorum(N), faultbound(N), R, locking=True)
|
|
s.add(Or(*cA)) # some round commits A
|
|
s.add(Or(*cB)) # some round commits B
|
|
check(f"L3 cross-round agreement N={N} R={R} (IBFT 2.0 locking): "
|
|
f"no two rounds commit different values", s)
|
|
|
|
# ---- NEG-CTRL L3: DROP the locking rule -> a later round can commit a different value
|
|
for N in (4,):
|
|
R = 2
|
|
s, cA, cB = cross_round_model(N, quorum(N), faultbound(N), R, locking=False)
|
|
s.add(Or(*cA))
|
|
s.add(Or(*cB))
|
|
check(f"NEG-CTRL L3 without locking (N={N}): agreement VIOLATED across rounds "
|
|
f"(shows the lock is load-bearing)", s, expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ------------------------------------------------------------------------------
|
|
print("\n=== SUMMARY (QBFT / IBFT 2.0 SAFETY) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" PROVED: QBFT agreement holds. (L1) For EVERY N, two commit quorums")
|
|
print(" intersect in > f validators, so they share an honest validator. (L2)")
|
|
print(" One-round: two distinct blocks cannot both reach a ceil(2N/3) COMMIT")
|
|
print(" quorum under <= f equivocating Byzantine validators (N in {4,5,7,10,13,16}).")
|
|
print(" (L3) Cross-round: even across round changes, IBFT 2.0 locking keeps the")
|
|
print(" committed value unique (N in {4,5,7,10,13}, R=3). All negative controls FIRE:")
|
|
print(" lowering the quorum to ceil(N/2) or dropping the lock breaks agreement,")
|
|
print(" proving the ceil(2N/3) quorum and the locking rule are load-bearing.")
|
|
print(" BOUNDARY: L1 is unbounded (all N); L2/L3 are bounded model checks over")
|
|
print(" the stated finite configs; this is the DESIGN combinatorics, not Besu")
|
|
print(" bytecode; chain 2800 consensus is classical ECDSA QBFT.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|