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.
364 lines
21 KiB
Python
364 lines
21 KiB
Python
#!/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<N (HM-FIX-SAFETY), is never weaker than ECDSA (HM-FIX-NEVER-")
|
|
print(" WEAKER), and restores full margin under coverage k=N (HM-FIX-ARM).")
|
|
print(" All negative controls FIRE. BOUNDARY: bounded per-N/per-k design combinatorics, not")
|
|
print(" Besu bytecode, not mainnet (chain 2800 = classical ECDSA QBFT, no Falcon layer).")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|