a2f4d835a3
partition_safety_smt.py (N=9 f=2 q=6): split-brain imposibil, starvatie clasificata, vindecare fara fork. anchor_viewchange_smt.py: o schimbare de runda pe ancora nu da doua certificate valide diferite, si unicitatea vine din legarea de bloc, nu din K=3 sigilii (< cvorum). Rulatorul cablat: 35 modele, 282 PROVED + 149 CEX, 0 FAILED.
251 lines
14 KiB
Python
251 lines
14 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# partition_safety_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) NETWORK-PARTITION SAFETY and LIVENESS characterization for
|
|
# AERE QBFT / IBFT 2.0 (Hyperledger Besu, chain 2800), at the LIVE fleet size
|
|
# N = 9 (f = 2, quorum ceil(2N/3) = 6) and, for the arithmetic core, UNBOUNDED in
|
|
# N. This is the parametric companion to the TLA+ partition model
|
|
# aerenew/formal-tla/QBFTPartition.tla, which TLC checks EXHAUSTIVELY only at
|
|
# N = 4. TLC cannot search N = 9 exhaustively (state explosion), so the same
|
|
# partition-safety property is discharged here by proving the negation UNSAT, in
|
|
# the same style as qbft_safety_smt.py. It formalizes what the test net showed
|
|
# empirically (runs F40 / F52: a lagging node, 1 of 3 down): a side without a
|
|
# quorum cannot finalize, the majority side can, and no two sides finalize
|
|
# conflicting values.
|
|
#
|
|
# A network partition splits the N validators into two groups that cannot
|
|
# exchange messages. While partitioned, any commit quorum for a value must be
|
|
# assembled ENTIRELY within one group's visible senders (cross-group messages are
|
|
# not delivered). We prove:
|
|
# PA SAFETY: two disjoint groups can never both reach a commit quorum for
|
|
# DIFFERENT values -> no partition forks the chain. (unbounded N + N=9)
|
|
# PL LIVENESS LOSS: a partition whose every group is smaller than the quorum
|
|
# finalizes nothing (progress is lost), while a partition with a group at or
|
|
# above the quorum keeps progressing (the majority side). (N=9 enumerated)
|
|
# PH HEAL: once the partition heals (all N visible) the honest set alone
|
|
# (N - f = 7 >= 6) forms a quorum, so progress returns without a fork.
|
|
#
|
|
# NON-VACUITY (rigor): every proof is paired with a NEGATIVE CONTROL that lowers
|
|
# the quorum to the majority ceil(N/2) (or drops a size guard) and the checker
|
|
# MUST return SAT (a balanced partition then forks, or a sub-quorum side
|
|
# "finalizes"). If a control did not fire, the proof would be vacuous.
|
|
#
|
|
# HONEST BOUNDARY: this checks the DESIGN combinatorics of partition-era quorum
|
|
# formation, not the Besu Java bytecode and not the live chain. It is a
|
|
# SINGLE-height agreement argument (the partition is the fault under study);
|
|
# cross-round locking / view change is covered in qbft_safety_smt.py L3,
|
|
# qbft_locking_smt.py and anchor_viewchange_smt.py. It is orthogonal to the block-
|
|
# seal signature scheme: chain 2800 commits with classical secp256k1 ECDSA, and
|
|
# NOTHING here implies post-quantum consensus.
|
|
# -----------------------------------------------------------------------------
|
|
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), Besu fastDivCeiling(2N,3)
|
|
def faultbound(n): return (n - 1) // 3 # floor((N-1)/3)
|
|
def ceil_half(n): return (n + 1) // 2 # ceil(N/2): the (too-low) majority quorum
|
|
|
|
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 -- NETWORK-PARTITION SAFETY / LIVENESS (N=9, f=2, quorum=6; core unbounded)\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, 7, 9)) + "\n")
|
|
|
|
# =============================================================================
|
|
# PA0 ARITHMETIC CORE (UNBOUNDED in N): two disjoint groups that partition all N
|
|
# validators cannot both hold a quorum. s1 + s2 = N, both >= q=ceil(2N/3) is
|
|
# impossible for EVERY N, because 2q > N. Negation UNSAT.
|
|
# =============================================================================
|
|
s = Solver()
|
|
N, q, s1, s2 = Int('N'), Int('q'), Int('s1'), Int('s2')
|
|
s.add(N >= 1)
|
|
s.add(3 * q >= 2 * N, 3 * q <= 2 * N + 2) # q == ceil(2N/3)
|
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N) # a partition of all N validators
|
|
s.add(s1 >= q, s2 >= q) # NEGATION: BOTH sides hold a quorum
|
|
check("PA0 partition arithmetic (ALL N): two disjoint groups covering N cannot "
|
|
"both reach the ceil(2N/3) quorum (2q > N)", s)
|
|
|
|
# ---- NEG-CTRL PA0: majority quorum ceil(N/2) -> a balanced split CAN give both
|
|
# sides a "quorum" (this is exactly the split-brain a too-low quorum allows).
|
|
s = Solver()
|
|
N, q, s1, s2 = Int('N'), Int('q'), Int('s1'), Int('s2')
|
|
s.add(N >= 2)
|
|
s.add(2 * q >= N, 2 * q <= N + 1) # q == ceil(N/2): the too-low quorum
|
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N)
|
|
s.add(s1 >= q, s2 >= q) # both sides reach the lowered quorum
|
|
check("NEG-CTRL PA0 majority quorum ceil(N/2): a balanced partition gives BOTH "
|
|
"sides a quorum (split-brain is possible)", s, expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# PA PARTITION SAFETY, per-validator model at N = 9 (and 4,7). Each validator i
|
|
# sits in group g in {0,1} (its side of the partition) and is honest or Byzantine.
|
|
# During the partition a value is FINALIZED on side g iff >= q side-g validators
|
|
# COMMIT it (cross-side messages invisible). Honest validators commit at most one
|
|
# value; <= f are Byzantine and may equivocate. SAFETY: two DIFFERENT values
|
|
# cannot both be finalized (on the same or on opposite sides). Negation UNSAT.
|
|
# =============================================================================
|
|
def partition_agreement(N, qv, fv, lowered=False):
|
|
s = Solver()
|
|
grp = [Int(f'grp_{i}') for i in range(N)] # 0 or 1: which side of the split
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
cA = [Bool(f'cA_{i}') for i in range(N)] # commits value A
|
|
cB = [Bool(f'cB_{i}') for i in range(N)] # commits value B
|
|
for i in range(N):
|
|
s.add(Or(grp[i] == 0, grp[i] == 1))
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv) # <= f Byzantine
|
|
for i in range(N):
|
|
s.add(Implies(honest[i], Not(And(cA[i], cB[i])))) # honest: one value
|
|
# finalized-on-side counts: only same-side committers are visible
|
|
def side_count(mat, g, v):
|
|
return Sum([If(And(grp[i] == g, mat[i]), 1, 0) for i in range(N)])
|
|
finA = Or(side_count(cA, 0, True) >= qv, side_count(cA, 1, True) >= qv)
|
|
finB = Or(side_count(cB, 0, True) >= qv, side_count(cB, 1, True) >= qv)
|
|
s.add(finA, finB) # NEGATION of safety: A and B both finalized somewhere
|
|
return s
|
|
|
|
for N in (4, 7, 9):
|
|
s = partition_agreement(N, quorum(N), faultbound(N))
|
|
check(f"PA partition safety N={N} (q={quorum(N)},f={faultbound(N)}): during a "
|
|
f"partition two different values cannot both be finalized", s)
|
|
|
|
# ---- NEG-CTRL PA: lower the quorum to ceil(N/2) at N=9 -> a balanced split forks.
|
|
s = partition_agreement(9, ceil_half(9), faultbound(9))
|
|
check(f"NEG-CTRL PA majority quorum ceil(N/2)={ceil_half(9)} at N=9: a partition "
|
|
f"finalizes two different values (split-brain fork)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# PL LIVENESS LOSS vs PROGRESS at N = 9. A value is finalizable during the
|
|
# partition iff SOME group has >= q members. If every group is below the quorum,
|
|
# nothing finalizes (liveness lost); if a group is at/above it, the majority side
|
|
# progresses.
|
|
# =============================================================================
|
|
# PL1: both groups below quorum => no finalization possible. Model: side sizes
|
|
# s1,s2 with s1<q, s2<q, s1+s2=N; commit counts bounded by side size; claim
|
|
# "max side commit >= q" is UNSAT.
|
|
def no_progress_when_starved(N, qv):
|
|
s = Solver()
|
|
s1, s2 = Int('s1'), Int('s2')
|
|
c1, c2 = Int('c1'), Int('c2') # commits gathered on each side (<= side size)
|
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N)
|
|
s.add(s1 < qv, s2 < qv) # BOTH groups starved (below quorum)
|
|
s.add(c1 >= 0, c1 <= s1, c2 >= 0, c2 <= s2)
|
|
s.add(Or(c1 >= qv, c2 >= qv)) # NEGATION: some side still finalizes
|
|
return s
|
|
s = no_progress_when_starved(9, quorum(9))
|
|
check("PL1 liveness loss N=9: if BOTH partition groups are below quorum 6, no side "
|
|
"can finalize (a starved partition makes no progress)", s)
|
|
|
|
# ---- NEG-CTRL PL1: a partition with a majority group (6-3) DOES let that side
|
|
# finalize -> progress is possible, so PL1's UNSAT is specific to starvation.
|
|
s = Solver()
|
|
s1, s2, c1 = Int('s1'), Int('s2'), Int('c1')
|
|
s.add(s1 == 6, s2 == 3, s1 + s2 == 9) # a 6-3 partition: one side has the quorum
|
|
s.add(c1 >= 0, c1 <= s1, c1 >= quorum(9))
|
|
check("NEG-CTRL PL1: a 6-3 partition at N=9 lets the majority side (6 >= quorum) "
|
|
"finalize (progress on the side that keeps a quorum)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# PL2: enumerate every split of N=9 and classify. A split (s1, s2) keeps liveness
|
|
# iff max(s1,s2) >= 6. Prove the classification is exactly right: there is NO
|
|
# split where both sides are < 6 yet some side reaches 6 (already PL1), and NO
|
|
# split with a side >= 6 that cannot finalize. State as: for all splits,
|
|
# (max side >= q) <-> (progress possible). Negation UNSAT.
|
|
s = Solver()
|
|
s1 = Int('s1'); s2 = Int('s2'); q9 = quorum(9)
|
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == 9)
|
|
maxside = If(s1 >= s2, s1, s2)
|
|
progress = maxside >= q9
|
|
# NEGATION: a split where "some side can finalize" disagrees with "max side >= q"
|
|
s.add(progress != (maxside >= q9))
|
|
check("PL2 split classification N=9: a partition makes progress IFF its larger "
|
|
"group is at least the quorum 6 (exhaustive over all 9 splits)", s)
|
|
|
|
# =============================================================================
|
|
# PH HEAL restores progress without a fork. Once healed, all N validators are
|
|
# mutually visible, so the honest set alone (N - f) forms a quorum when N - f >= q.
|
|
# =============================================================================
|
|
# PH1: N - f >= q at N=9 (7 >= 6): the honest validators alone can commit after
|
|
# heal. Prove N - f >= q holds; here as the concrete fact for N=9.
|
|
s = Solver()
|
|
nf, qv = Int('nf'), Int('qv')
|
|
s.add(nf == 9 - faultbound(9), qv == quorum(9))
|
|
s.add(nf < qv) # NEGATION: honest set too small to commit
|
|
check("PH1 heal progress N=9: the honest set alone (N-f = 7) meets the quorum 6, so "
|
|
"the healed network can finalize without any Byzantine help", s)
|
|
|
|
# PH2: after heal, a single value committed by >= q validators is finalized and no
|
|
# SECOND value can be (same one-round agreement, now over ALL N). Negation UNSAT.
|
|
s = Solver()
|
|
N = 9; qv = quorum(9); fv = faultbound(9)
|
|
honest = [Bool(f'h_{i}') for i in range(N)]
|
|
cA = [Bool(f'a_{i}') for i in range(N)]
|
|
cB = [Bool(f'b_{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], Not(And(cA[i], cB[i]))))
|
|
s.add(Sum([If(cA[i], 1, 0) for i in range(N)]) >= qv) # A finalized post-heal
|
|
s.add(Sum([If(cB[i], 1, 0) for i in range(N)]) >= qv) # NEGATION: B too
|
|
check("PH2 heal safety N=9: after the partition heals, two different values still "
|
|
"cannot both reach the quorum (no fork on recovery)", s)
|
|
|
|
# ---- NEG-CTRL PH2: lower the quorum -> post-heal two values can both 'commit'.
|
|
s = Solver()
|
|
N = 9; qv = ceil_half(9); fv = faultbound(9)
|
|
honest = [Bool(f'h_{i}') for i in range(N)]
|
|
cA = [Bool(f'a_{i}') for i in range(N)]
|
|
cB = [Bool(f'b_{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], Not(And(cA[i], cB[i]))))
|
|
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)
|
|
check(f"NEG-CTRL PH2 majority quorum ceil(N/2)={ceil_half(9)} at N=9: post-heal two "
|
|
f"values both reach the lowered quorum (fork) -- the ceil(2N/3) quorum is "
|
|
f"load-bearing on recovery too", s, expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ------------------------------------------------------------------------------
|
|
print("\n=== SUMMARY (NETWORK-PARTITION SAFETY / LIVENESS) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" PROVED at N=9 (f=2, quorum=6), with the arithmetic core unbounded in N:")
|
|
print(" (PA) a network partition cannot fork the chain -- two disjoint groups can")
|
|
print(" never both reach a ceil(2N/3) commit quorum, so at most one side finalizes,")
|
|
print(" and it finalizes a single value. (PL) liveness is LOST exactly when every")
|
|
print(" group is below the quorum (a balanced 5-4 or worse split at N=9), and a")
|
|
print(" partition keeps progressing iff its larger group is at least 6 (the majority")
|
|
print(" side); the split classification is exhaustive over all 9 splits. (PH) once")
|
|
print(" the partition heals, the honest set alone (7 >= 6) forms a quorum, so progress")
|
|
print(" returns with no fork. All negative controls FIRE: lowering the quorum to the")
|
|
print(" majority ceil(N/2) forks a balanced partition and forks on recovery, and a 6-3")
|
|
print(" split shows the starvation result PL1 is not vacuous.")
|
|
print(" This is the parametric N=9 companion to formal-tla/QBFTPartition.tla, which")
|
|
print(" TLC checks exhaustively at N=4; cross-method + cross-scale agreement is the")
|
|
print(" point. BOUNDARY: design combinatorics of partition-era quorum formation, not")
|
|
print(" Besu bytecode; single-height agreement; classical ECDSA (not post-quantum).")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|