#!/usr/bin/env python3 # ----------------------------------------------------------------------------- # falcon_hybrid_dualquorum_smt.py (PQ-CONSENSUS Step 2 — 2026-07-18) # # MACHINE-CHECKED (z3) analysis of the AERE HYBRID ECDSA+Falcon committed-seal # design: the safe migration step between today's ECDSA-only QBFT and a future # Falcon-blocking chain. A committed block is VALID only if it carries BOTH # (i) an ECDSA committed-seal quorum (BftCommitSealsValidationRule, native) # (ii) a Falcon-512 quorum certificate (FalconSealValidationRule, fork-gated) # of >= quorum(N) = ceil(2N/3) distinct valid seals each. # # In the shipped Besu patch the QBFT header ruleset is: # .addRule(new BftCommitSealsValidationRule()) // ECDSA (always) # .addRule(new FalconSealValidationRule()); // Falcon (blocking >= forkBlock) # so "blocking mode" IS the hybrid dual-quorum: ECDSA is never removed, Falcon # is ADDED as a second mandatory quorum. This model discharges the properties # that make that migration step SAFE, for the live/target sizes N in {7,9,11}. # # Besu quorum: quorum(N)=ceil(2N/3); BFT fault bound f(N)=floor((N-1)/3). # N=7 -> q=5,f=2 N=9 -> q=6,f=2 N=11 -> q=8,f=3 N=13 -> q=9,f=4 # # Properties (each proved by UNSAT-of-negation, each paired with a firing # NEGATIVE CONTROL so the result is demonstrably non-vacuous): # H1 HYBRID SAFETY two conflicting blocks cannot both be hybrid-valid # under <= f ECDSA-equivocating AND <= f Falcon- # equivocating faulty validators. N in {7,9,11} # H2 EITHER-MISSING a block missing EITHER quorum is REJECTED: # H2a ECDSA quorum present but Falcon seals < q -> invalid # H2b Falcon quorum present but ECDSA seals < q -> invalid # H3 MIGRATION-SAFE hybrid-valid => ecdsa-valid (SUBSET lemma): adding the # (SUBSET) Falcon requirement can only REMOVE blocks from the # committable set, so the hybrid chain can never accept a # block ECDSA-only would have rejected -> "no worse than # ECDSA-only today". This is the core migration guarantee. # H4 HYBRID LIVENESS a block commits iff >= q validators are BOTH ECDSA- # honest AND Falcon-correct AND online; the combined bad # set must be <= f. At |bad|=f+1 the hybrid chain can # STALL where ECDSA-only would not (the extra liveness # cost of the second quorum). # # HONEST BOUNDARY: bounded per-N checks over N in {7,9,11(,13)}; DESIGN # combinatorics of the dual-quorum rule, NOT the Besu Java bytecode; NOT mainnet # (chain 2800 is classical ECDSA QBFT, N=7, no Falcon layer of any kind). # Cryptographic soundness of Falcon-512 is out of scope (NIST KAT / precompile). # ----------------------------------------------------------------------------- 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: 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 HYBRID ECDSA+Falcon dual-quorum -- migration-safe post-quantum consensus (Step 2)\n") print(" " + ", ".join(f"N={n}: q={quorum(n)}, f={faultbound(n)}" for n in (7, 9, 11, 13)) + "\n") # ============================================================================= # H1 HYBRID SAFETY: two conflicting blocks A,B cannot both be hybrid-valid. # Per validator i, four seal bits (ecdsaA/B, falconA/B) and two honesty flags. # * ECDSA-honest i signs at most ONE block's ECDSA seal. # * Falcon-correct i signs at most ONE block's Falcon seal. # * an ECDSA-faulty i may equivocate its ECDSA seal (both A and B). # * a Falcon-faulty i may equivocate its Falcon seal (both A and B). # * <= f ECDSA-faulty and <= f Falcon-faulty (the two fault sets may DIFFER). # * hybrid-valid(X) := (#ecdsaX >= q) AND (#falconX >= q). # ============================================================================= def hybrid_safety(N, q, f): s = Solver() eHon = [Bool(f'eHon_{i}') for i in range(N)] fCor = [Bool(f'fCor_{i}') for i in range(N)] eA = [Bool(f'eA_{i}') for i in range(N)]; eB = [Bool(f'eB_{i}') for i in range(N)] fA = [Bool(f'fA_{i}') for i in range(N)]; fB = [Bool(f'fB_{i}') for i in range(N)] s.add(Sum([If(Not(eHon[i]), 1, 0) for i in range(N)]) <= f) # <= f ECDSA-faulty s.add(Sum([If(Not(fCor[i]), 1, 0) for i in range(N)]) <= f) # <= f Falcon-faulty for i in range(N): s.add(Implies(eHon[i], Not(And(eA[i], eB[i])))) # ECDSA-honest: one block s.add(Implies(fCor[i], Not(And(fA[i], fB[i])))) # Falcon-correct: one block # both blocks hybrid-valid: s.add(Sum([If(eA[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(fA[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(eB[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(fB[i],1,0) for i in range(N)]) >= q) return s for N in (7, 9, 11): s = hybrid_safety(N, quorum(N), faultbound(N)) check(f"H1 HYBRID-SAFETY N={N} (q={quorum(N)},f={faultbound(N)}): two conflicting blocks " f"cannot both carry an ECDSA quorum AND a Falcon quorum under <= f of each faulty", s) # NEG-CTRL H1: drop BOTH fault bounds -> conflicting blocks can both be certified. # (NOTE: dropping only ONE bound still leaves safety intact, because EITHER quorum's # <= f honesty bound alone forbids two conflicting quorums -- a genuine property of the # dual design: hybrid inherits ECDSA's safety AND Falcon's. So the non-vacuity control # must remove both bounds to expose a violation.) def hybrid_safety_no_bounds(N, q): s = Solver() eA = [Bool(f'eA_{i}') for i in range(N)]; eB = [Bool(f'eB_{i}') for i in range(N)] fA = [Bool(f'fA_{i}') for i in range(N)]; fB = [Bool(f'fB_{i}') for i in range(N)] # NO honesty bound on either scheme -> every validator may equivocate both seals s.add(Sum([If(eA[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(fA[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(eB[i],1,0) for i in range(N)]) >= q) s.add(Sum([If(fB[i],1,0) for i in range(N)]) >= q) return s s = hybrid_safety_no_bounds(7, quorum(7)) check("NEG-CTRL H1 N=7 WITHOUT any <= f bound (ECDSA or Falcon): two hybrid blocks CAN both be " "certified (proves the fault bounds are load-bearing; note either bound alone still " "secures hybrid safety, so both must be dropped to expose a violation)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # H2 EITHER-MISSING quorum -> block REJECTED (both halves are mandatory). # hybridValid := (e >= q) AND (fal >= q). # ============================================================================= def hybridValid(e, fal, q): return And(e >= q, fal >= q) # H2a: ECDSA quorum present, Falcon short -> NOT valid s = Solver() e, fal = Int('ecdsaSeals'), Int('falconSeals') q = quorum(7) s.add(e >= q, fal < q) # ECDSA ok, Falcon short s.add(hybridValid(e, fal, q)) # negate: claim it is valid anyway check(f"H2a N=7: a block with ECDSA quorum ({q}) but Falcon seals < {q} is NOT hybrid-valid " f"(missing Falcon quorum -> rejected)", s) # H2b: Falcon quorum present, ECDSA short -> NOT valid s = Solver() e, fal = Int('ecdsaSeals'), Int('falconSeals') s.add(fal >= q, e < q) # Falcon ok, ECDSA short s.add(hybridValid(e, fal, q)) check(f"H2b N=7: a block with Falcon quorum ({q}) but ECDSA seals < {q} is NOT hybrid-valid " f"(missing ECDSA quorum -> rejected)", s) # NEG-CTRL H2: a block with BOTH quorums IS valid (non-vacuous: rejection isn't total) s = Solver() e, fal = Int('ecdsaSeals'), Int('falconSeals') s.add(e >= q, fal >= q, hybridValid(e, fal, q)) check(f"NEG-CTRL H2 N=7: a block carrying BOTH an ECDSA quorum and a Falcon quorum IS hybrid-valid " f"(the rule accepts genuine dual-quorum blocks)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # H3 MIGRATION-SAFE (SUBSET lemma): hybridValid(X) => ecdsaValid(X). # Adding the Falcon requirement can only REMOVE blocks from the committable # set. So a hybrid chain never accepts a block ECDSA-only would reject: # any fork reachable under hybrid is already reachable under ECDSA-only, # hence hybrid is AT LEAST AS SAFE as today's ECDSA-only chain. This is the # formal statement of "if Falcon has a bug the chain is no worse than ECDSA". # ============================================================================= s = Solver() e, fal = Int('ecdsaSeals'), Int('falconSeals') q = quorum(7) # negate: exists a header hybrid-valid but NOT ecdsa-valid s.add(hybridValid(e, fal, q)) s.add(Not(e >= q)) # ecdsa-invalid check("H3 MIGRATION-SAFE (subset) N=7: every hybrid-valid block is ECDSA-valid " "(the Falcon requirement only shrinks the committable set -> no worse than ECDSA-only)", s) # NEG-CTRL H3: the CONVERSE is false -> an ECDSA-valid block need NOT be hybrid-valid # (i.e. hybrid is a STRICT subset -> the Falcon requirement genuinely removes blocks). s = Solver() e, fal = Int('ecdsaSeals'), Int('falconSeals') s.add(e >= q) # ecdsa-valid s.add(Not(hybridValid(e, fal, q))) # but hybrid-invalid (fal < q) check("NEG-CTRL H3 N=7: an ECDSA-valid block can be hybrid-INVALID (Falcon short) " "-> hybrid is a STRICT subset, the Falcon quorum is a real added gate", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= # H4 HYBRID LIVENESS + combined fault tolerance. A validator contributes to # BOTH quorums only if ECDSA-honest AND Falcon-correct AND online. Worst # case ECDSA-faults and Falcon-faults are DISJOINT, so the "both-good" set # is N - |ecdsaBad UNION falconBad|. The chain commits iff both-good >= q. # ============================================================================= # H4-live: at the COMBINED fault bound (<= f validators bad in EITHER dimension) # the both-good set N-f >= q, so a hybrid block can always form. N in {7,9,11}. for N in (7, 9, 11): q, f = quorum(N), faultbound(N) s = Solver() bad = [Bool(f'bad_{i}') for i in range(N)] # bad_i = ECDSA-faulty OR Falcon-faulty OR offline goodBoth = [Not(bad[i]) for i in range(N)] s.add(Sum([If(bad[i], 1, 0) for i in range(N)]) <= f) # <= f combined bad s.add(Sum([If(goodBoth[i], 1, 0) for i in range(N)]) < q) # negate: cannot reach quorum check(f"H4-live N={N}: with <= f={f} combined-bad validators, both-good set N-f={N-f} >= q={q} " f"-> a hybrid (dual-quorum) block can always be produced", s) # H4-stall: at f+1 combined bad the hybrid chain can STALL (reachable). This is the # EXTRA liveness cost of the second quorum vs ECDSA-only. N=7 shown; general via config. def hybrid_stall(N, q, bad_count): s = Solver() bad = [Bool(f'bad_{i}') for i in range(N)] s.add(Sum([If(bad[i], 1, 0) for i in range(N)]) == bad_count) s.add(Sum([If(Not(bad[i]), 1, 0) for i in range(N)]) < q) # both-good < q -> no cert return s for N in (7,): f = faultbound(N) s = hybrid_stall(N, quorum(N), f + 1) check(f"H4-stall N={N}: with f+1={f+1} combined-bad validators the both-good set {N-(f+1)} < " f"quorum {quorum(N)} -> the hybrid chain STALLS (extra liveness cost of the 2nd quorum)", s, expect_unsat=False, kind="STALL") # ============================================================================= # THRESHOLD/MARGIN — answers "N=7 zero-margin under 2 faults; does N=9/N=11 restore it?" # margin2(N) = (N-2) - quorum(N) = surplus of correct signers over quorum when 2 bad. # margin1(N) = (N-1) - quorum(N) = surplus when 1 bad. # ============================================================================= print(" margin under 2 faults (N-2)-q: " + ", ".join(f"N={n}->{(n-2)-quorum(n)}" for n in (7,9,11,13))) print(" margin under 1 fault (N-1)-q: " + ", ".join(f"N={n}->{(n-1)-quorum(n)}" for n in (7,9,11,13))) # N=7 has EXACTLY zero margin under 2 faults (any 3rd slow/crashed node stalls the hybrid chain). s = Solver(); m = Int('m'); s.add(m == (7 - 2) - quorum(7)); s.add(m != 0) check("MARGIN N=7: two-fault liveness margin (N-2)-q == 0 EXACTLY " "(at f=2 faults all 5 remaining validators must sign every hybrid block)", s) # N=9 and N=11 RESTORE a positive two-fault margin (>= 1): the chain tolerates 2 Falcon # faults AND a slow/crashed extra node without stalling. This is the "grow past 7" answer. for N in (9, 11): s = Solver(); m = Int('m'); s.add(m == (N - 2) - quorum(N)); s.add(m >= 1) check(f"MARGIN N={N}: two-fault liveness margin (N-2)-q = {(N-2)-quorum(N)} >= 1 " f"(a larger set restores positive margin under 2 Falcon faults)", s, expect_unsat=False, kind="CONFIG") # Non-vacuous: N=7 single-fault margin is POSITIVE (=1), unlike the retired N=5 (=0). s = Solver(); m = Int('m'); s.add(m == (7 - 1) - quorum(7)); s.add(m >= 1) check("MARGIN N=7: single-fault margin (N-1)-q = 1 >= 1 (positive, unlike the retired N=5 zero-margin)", s, expect_unsat=False, kind="CONFIG") # ============================================================================= # AUD-CONSENSUS-1 / -2 FIX: registry size M DECOUPLED from validator count N. # ----------------------------------------------------------------------------- # Everything above indexed validators and seals over range(N), i.e. the registry # equals the validator set (M == N). The audit showed the shipped code let the # IMMUTABLE Falcon registry (size M = N0) drift from the DYNAMIC validator set # (size N): the Falcon quorum tracked N while verifying keys were bounded by M, and # seals were counted by REGISTRY membership. The fix binds BOTH the Falcon quorum # AND the counted-seal set to the SAME set: # eligible = validators INTERSECT registry , k = |eligible| # Falcon quorum = ceil(2k/3) (ECDSA quorum stays ceil(2N/3) over the full set) # This section models M != N explicitly and re-proves the migration guarantees. # ============================================================================= print("\n### AUD-CONSENSUS-1/-2 FIX: eligible-signer dual-quorum (registry M != validator count N)\n") def ceil23(x): return (2 * x + 2) // 3 # HM-BUG (firing): the OLD hybrid rule (Falcon quorum from N) DEADLOCKS when the # validator set grows past the registry. Armed at M=7, grown to N=11: the ECDSA leg # is fine (11 ECDSA keys), but the OLD Falcon leg needs ceil(2*11/3)=8 > 7 Falcon keys. s = Solver() fal, qF = Int('falValid'), Int('qFalconOld') s.add(fal <= 7) # at most 7 Falcon keys exist (M=7) s.add(3 * qF >= 2 * 11, 3 * qF <= 2 * 11 + 2) # OLD Falcon quorum = ceil(2*11/3) = 8 s.add(fal < qF) # Falcon leg unreachable -> block rejected check("HM-BUG (OLD hybrid) M=7 grown to N=11: Falcon leg needs ceil(2*11/3)=8 > 7 keys -> hybrid " "block DEADLOCKS though the ECDSA leg is fine (the halt this fix removes)", s, expect_unsat=False, kind="BUG-DEMO") # HM-FIX-LIVE (unbounded): the eligible Falcon leg ceil(2k/3) over exactly k eligible # signers is always reachable (k >= ceil(2k/3)), so a validator add/remove cannot # silently deadlock the hybrid chain. s = Solver() k, qk = Int('k'), Int('qk') s.add(k >= 0, 3 * qk >= 2 * k, 3 * qk <= 2 * k + 2) s.add(k < qk) # negate: eligible leg below its own quorum check("HM-FIX-LIVE (all k): the eligible Falcon leg k >= ceil(2k/3) is always reachable, so a " "validator add/remove cannot silently deadlock the hybrid chain (no silent halt)", s) # HM-FIX-SAFETY (M != N): two conflicting blocks cannot both be hybrid-valid. Because # the ECDSA leg (quorum ceil(2N/3) over the full set N, <= f equivocators) already # forbids two conflicting quorums, hybrid safety holds even when the Falcon registry # is SMALLER than N. Proved for (N, M=7) in {7, 9, 11}. def ecdsa_leg_two_quorums(N): s = Solver() q, f = quorum(N), faultbound(N) eHon = [Bool(f'eHon_{i}') for i in range(N)] eA = [Bool(f'eA_{i}') for i in range(N)] eB = [Bool(f'eB_{i}') for i in range(N)] s.add(Sum([If(Not(eHon[i]), 1, 0) for i in range(N)]) <= f) for i in range(N): s.add(Implies(eHon[i], Not(And(eA[i], eB[i])))) s.add(Sum([If(eA[i], 1, 0) for i in range(N)]) >= q) s.add(Sum([If(eB[i], 1, 0) for i in range(N)]) >= q) return s for N in (7, 9, 11): s = ecdsa_leg_two_quorums(N) check(f"HM-FIX-SAFETY N={N},M=7: two conflicting blocks cannot both carry the ECDSA quorum " f"ceil(2N/3)={quorum(N)} under <= f={faultbound(N)} -> hybrid stays SAFE even when the " f"Falcon registry (M=7) is smaller than N", s) # HM-FIX-NEVER-WEAKER: a hybrid-valid block needs the ECDSA quorum over N AND the # eligible Falcon quorum over k <= N, so hybrid-valid => ECDSA-valid for ANY k. s = Solver() e, fe, Nn, kk, qN, qk2 = Int('e'), Int('fe'), Int('N'), Int('k'), Int('qN'), Int('qk') s.add(Nn >= 1, kk >= 0, kk <= Nn) s.add(3 * qN >= 2 * Nn, 3 * qN <= 2 * Nn + 2) s.add(3 * qk2 >= 2 * kk, 3 * qk2 <= 2 * kk + 2) s.add(e >= qN, fe >= qk2) # hybrid-valid (ECDSA over N, Falcon over k) s.add(e < qN) # negate: NOT ecdsa-valid check("HM-FIX-NEVER-WEAKER (all N,k): every eligible-hybrid-valid block is ECDSA-valid over the " "full set N -> the fixed dual-quorum is never weaker than ECDSA-only (H3 preserved for M!=N)", s) # NEG-CTRL: the eligible Falcon leg is a REAL added gate (an ECDSA-valid block can be # eligible-hybrid-INVALID when the eligible Falcon quorum is short). s = Solver() e, fe = Int('e'), Int('fe') s.add(e >= quorum(7), fe < quorum(7)) check("NEG-CTRL HM N=k=7: an ECDSA-valid block can be eligible-hybrid-INVALID (Falcon short) " "-> the eligible Falcon leg is a genuine added gate", s, expect_unsat=False, kind="NEG-CTRL") # HM-FIX-ARM: at ARM time the registry COVERS the validator set (k == N), so the # eligible Falcon quorum equals the ECDSA quorum ceil(2N/3) -> full two-fault margin. for N in (9, 11): s = Solver() s.add(Int('d') == ceil23(N) - quorum(N)) # eligible quorum(k=N) - ECDSA quorum(N) s.add(Int('d') != 0) # negate: they differ check(f"HM-FIX-ARM N={N}: full coverage k=N makes the eligible Falcon quorum ceil(2N/3)=" f"{ceil23(N)} EQUAL the ECDSA quorum -> the arming invariant restores full margin", s) # ------------------------------------------------------------------------------ print("\n=== SUMMARY (HYBRID ECDSA+Falcon dual-quorum, Step 2) ===") allok = True for name, tag, ok, kind in results: print(f" {tag:9} [{kind}] {name}") allok = allok and ok print() if allok: print(" PROVED: the HYBRID mode (a committed block requires BOTH an ECDSA committed-seal") print(" quorum AND a Falcon-512 quorum certificate, ceil(2N/3) each) is SAFE at N in") print(" {7,9,11} under <= f equivocating faults of each kind (H1); a block missing EITHER") print(" quorum is REJECTED (H2a/H2b); and every hybrid-valid block is ECDSA-valid, so the") print(" Falcon requirement can only SHRINK the committable set -> the hybrid chain is AT") print(" LEAST AS SAFE as today's ECDSA-only chain, a Falcon bug can never make it worse") print(" (H3, the core migration guarantee). The cost is liveness: hybrid needs 2f+1") print(" validators good in BOTH dimensions; at f+1 combined-bad it can stall where") print(" ECDSA-only would not (H4). N=7 has ZERO two-fault margin; N=9/N=11 restore margin.") print(" AUD-CONSENSUS-1/-2 FIX (M != N): with the registry size M decoupled from N, the OLD") print(" rule DEADLOCKS when the validator set grows past the registry (HM-BUG fires); the") print(" fix binds the Falcon quorum AND counted set to eligible=validators INTERSECT registry") print(" (k=|eligible|), which stays LIVE for all k (HM-FIX-LIVE), keeps hybrid SAFE via the") print(" ECDSA leg even when M