6cb0140fae
The public history carried kat/__pycache__/mlkem768_reference.cpython-314.pyc, a compiled Python artifact embedding the operator's absolute local path. Text secret scanners do not read compiled binaries, which is exactly how it slipped through, and removing it from the tip would have left it reachable through the old root commits. So this repository is republished from a single clean root. This root also carries, from the previously unpublished line of work: - corrected LICENSE year, LICENSING.md, VERIFY-POLICY.md, and CITATIONS-UNRESOLVED.md remeasured 2026-08-11 (101 paths, README aligned) - O-018: run_consensus_verification.py ran 19 of 29 models and reported PASS; it now runs all 29, and computemarket_smt.py gains resolveByTimeout / reclaimUnsettled cases plus a negative control - O-006: the word 'audited' removed from next to Bouncy Castle, twice, after a concurrent edit resurrected it - O-014: prior art named and dated - Algorand's native falcon_verify shipped about ten months before AERE's precompiles; the primacy claim is withdrawn where it was implied - bench/ scripts parametrized so they actually run for an outsider (the earlier textual sanitization left $STAGING unexpanded inside Python strings) - AIP-2/AIP-3 errata with measured figures, spec remeasurements at 2026-08-01, and the spec-zk-stack retractions (owner is an operational key, not the Foundation; 'maximally sound' withdrawn; aggregator V1 deprecated) The redacted bench-host environment files from the sanitized line are kept exactly as published; the unredacted local variants are not carried.
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)
|