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.
399 lines
23 KiB
Python
399 lines
23 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# falcon_blocking_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) analysis of the AERE Falcon-512 quorum certificate in
|
|
# BLOCKING mode (post-fork): a block is VALID only if it carries >= quorum(N)
|
|
# DISTINCT valid Falcon seals over the correct commit hash
|
|
# (FalconSealValidationRule; consensus-pqc/QUORUM-DESIGN.md sec 3, 6).
|
|
#
|
|
# This is the z3 counterpart of formal-consensus/FalconQuorum.qnt (which targets
|
|
# Apalache/TLC and needs Java). It RUNS locally on z3 and proves:
|
|
# B-SAFETY in blocking mode, <= f Falcon-key-faulty validators (which may
|
|
# EQUIVOCATE -- place a valid own-key seal on BOTH conflicting
|
|
# blocks) can never certify two conflicting blocks. N in {4,5,7}.
|
|
# B-LIVENESS at the fault bound, the honest+correct set (N-f) still reaches
|
|
# quorum, so a certificate can always form. Proved UNBOUNDED (all N)
|
|
# and per-N for {4,5,7}.
|
|
# THRESHOLD WHY N>=7 is required to make blocking safe: N>=7 is the smallest
|
|
# validator count that is BOTH safe (f>=2) AND live (N-2>=quorum)
|
|
# against 2 simultaneous Falcon faults; and a SINGLE Falcon fault
|
|
# leaves strictly-more-than-quorum correct signers (liveness margin
|
|
# > 0) only at N>=7. At N in {4,5} blocking can STALL (shown SAT).
|
|
#
|
|
# Besu quorum: quorum(N)=ceil(2N/3); BFT fault bound f(N)=floor((N-1)/3).
|
|
#
|
|
# HONEST BOUNDARY: B-SAFETY per-N is a BOUNDED check; the intersection lemma and
|
|
# the N-f>=quorum liveness identity are UNBOUNDED (all N). This is the certificate
|
|
# COMBINATORICS of the design, not the Besu Java code, and NOT mainnet: chain
|
|
# 2800 runs classical ECDSA QBFT and the Falcon layer there is LOG-ONLY, not
|
|
# blocking (blocking requires N>=7 + a re-genesis with a Falcon anchor).
|
|
# -----------------------------------------------------------------------------
|
|
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 Falcon quorum certificate -- BLOCKING mode: safety, liveness, and the N>=7 threshold\n")
|
|
print(" " + ", ".join(f"N={n}: q={quorum(n)}, f={faultbound(n)}, N-f={n-faultbound(n)}"
|
|
for n in (4, 5, 6, 7)) + "\n")
|
|
|
|
# =============================================================================
|
|
# B-SAFETY -- blocking mode: two conflicting blocks cannot both be certified.
|
|
# Per validator i: honest_i, sealA_i, sealB_i.
|
|
# * HONEST validator signs at most ONE block per height: honest => !(sealA & sealB)
|
|
# * FALCON-FAULTY validator holds its own key and may EQUIVOCATE: a valid seal
|
|
# on BOTH conflicting blocks (counts toward both certs).
|
|
# * <= f Falcon-faulty. A cert needs >= quorum distinct valid seals.
|
|
# =============================================================================
|
|
def blocking_safety(N, qv, fv):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
sealA = [Bool(f'sealA_{i}') for i in range(N)]
|
|
sealB = [Bool(f'sealB_{i}') for i in range(N)]
|
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv) # <= f faulty
|
|
for i in range(N):
|
|
s.add(Implies(honest[i], Not(And(sealA[i], sealB[i])))) # honest: one block
|
|
s.add(Sum([If(sealA[i], 1, 0) for i in range(N)]) >= qv) # cert A formed
|
|
s.add(Sum([If(sealB[i], 1, 0) for i in range(N)]) >= qv) # cert B formed
|
|
return s
|
|
|
|
for N in (4, 5, 7):
|
|
s = blocking_safety(N, quorum(N), faultbound(N))
|
|
check(f"B-SAFETY N={N} (q={quorum(N)},f={faultbound(N)}): two conflicting blocks "
|
|
f"cannot both reach a Falcon quorum under <= f equivocating faulty", s)
|
|
|
|
# ---- NEG-CTRL B-SAFETY: drop the <= f bound -> >f equivocators certify BOTH ------
|
|
def blocking_safety_no_bound(N, qv):
|
|
s = Solver()
|
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
|
sealA = [Bool(f'sealA_{i}') for i in range(N)]
|
|
sealB = [Bool(f'sealB_{i}') for i in range(N)]
|
|
# NO fault bound; faulty may equivocate
|
|
for i in range(N):
|
|
s.add(Implies(honest[i], Not(And(sealA[i], sealB[i]))))
|
|
s.add(Sum([If(sealA[i], 1, 0) for i in range(N)]) >= qv)
|
|
s.add(Sum([If(sealB[i], 1, 0) for i in range(N)]) >= qv)
|
|
return s
|
|
for N in (4,):
|
|
s = blocking_safety_no_bound(N, quorum(N))
|
|
check(f"NEG-CTRL B-SAFETY N={N} WITHOUT the <= f bound: two blocks CAN both be "
|
|
f"certified (proves the <= f assumption is load-bearing)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL B-SAFETY: lower the quorum to ceil(N/2) -> certs collide -----------
|
|
def ceil_half(n): return (n + 1) // 2
|
|
for N in (4,):
|
|
s = blocking_safety(N, ceil_half(N), faultbound(N))
|
|
check(f"NEG-CTRL B-SAFETY N={N} majority quorum ceil(N/2)={ceil_half(N)}: two blocks "
|
|
f"CAN both be certified (proves ceil(2N/3) is load-bearing)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# =============================================================================
|
|
# B-LIVENESS -- at the fault bound, honest+correct (N-f) still forms a quorum.
|
|
# =============================================================================
|
|
# UNBOUNDED (all N): N - f(N) >= quorum(N).
|
|
s = Solver()
|
|
N, q, f = Int('N'), Int('q'), Int('f')
|
|
s.add(N >= 1)
|
|
s.add(3 * q >= 2 * N, 3 * q <= 2 * N + 2) # q = ceil(2N/3)
|
|
s.add(3 * f <= N - 1, N - 1 <= 3 * f + 2) # f = floor((N-1)/3)
|
|
s.add(N - f < q) # negate: honest+correct below quorum
|
|
check("B-LIVENESS (all N): honest+correct set N-f >= quorum(N) -> a cert can always form", s)
|
|
|
|
# per-N witness that the honest set alone certifies (non-vacuous, config theorem)
|
|
for N in (4, 5, 7):
|
|
ok = (N - faultbound(N)) >= quorum(N)
|
|
s = Solver(); s.add(Int('dummy') == (0 if ok else 1)); s.add(Int('dummy') == 0)
|
|
check(f"B-LIVENESS N={N}: N-f={N-faultbound(N)} >= quorum={quorum(N)} "
|
|
f"(honest+correct alone forms the Falcon cert)", s,
|
|
expect_unsat=not ok, kind="CONFIG")
|
|
|
|
# =============================================================================
|
|
# THRESHOLD -- WHY N>=7 is required to activate BLOCKING.
|
|
# -----------------------------------------------------------------------------
|
|
# (T1) To be BOTH safe and live against 2 simultaneous Falcon faults you need
|
|
# safe2(N): f(N) >= 2 AND live2(N): (N-2) >= quorum(N).
|
|
# Claim: no N in {4,5,6} satisfies both; N=7 does. N>=7 is the crossover.
|
|
# =============================================================================
|
|
def safe2(N): return faultbound(N) >= 2
|
|
def live2(N): return (N - 2) >= quorum(N)
|
|
|
|
# no N in {4,5,6} is both safe and live for 2 faults:
|
|
s = Solver()
|
|
Nv = Int('N')
|
|
s.add(Or(Nv == 4, Nv == 5, Nv == 6))
|
|
# express safe2 & live2 for the concrete small set via a disjunction of the true cases
|
|
both_cases = Or(*[And(Nv == n, safe2(n), live2(n)) for n in (4, 5, 6)])
|
|
s.add(both_cases)
|
|
check("THRESHOLD-T1a no N in {4,5,6} is BOTH safe(f>=2) AND live(N-2>=q) for 2 faults", s)
|
|
|
|
# N=7 IS both safe and live for 2 faults (non-vacuous positive witness):
|
|
s = Solver()
|
|
s.add(Int('ok7') == (1 if (safe2(7) and live2(7)) else 0)); s.add(Int('ok7') == 1)
|
|
check("THRESHOLD-T1b N=7 IS safe(f=2) AND live(N-2=5>=q=5) for 2 faults "
|
|
f"(f(7)={faultbound(7)}, N-2=5, q(7)={quorum(7)})", s, expect_unsat=False, kind="CONFIG")
|
|
|
|
# (T2) SINGLE-Falcon-fault liveness margin: margin1(N) = (N-1) - quorum(N).
|
|
# margin1 == 0 EXACTLY at N in {4,5} (a single fault forces ALL remaining
|
|
# honest to sign; any further crash/slowness halts) and margin1 >= 1 at
|
|
# N >= 6. The current AERE mainnet size N=5 has ZERO single-fault margin;
|
|
# N=7 (the next BFT-OPTIMAL 3f+1 size) both restores positive margin AND
|
|
# tolerates 2 Falcon faults (T1) -- that combination is the driver for N>=7.
|
|
print(" single-fault margin (N-1)-quorum(N): "
|
|
+ ", ".join(f"N={n}->{(n-1)-quorum(n)}" for n in (4, 5, 6, 7)))
|
|
for N in (4, 5):
|
|
margin = (N - 1) - quorum(N)
|
|
s = Solver(); s.add(Int('m') == margin); s.add(Int('m') != 0)
|
|
check(f"THRESHOLD-T2 N={N}: single-fault liveness margin (N-1)-q == 0 "
|
|
f"(a single Falcon fault forces ALL {N-1} remaining honest to sign)", s)
|
|
for N in (6, 7):
|
|
margin = (N - 1) - quorum(N)
|
|
s = Solver(); s.add(Int('m') == margin); s.add(Int('m') >= 1)
|
|
check(f"THRESHOLD-T2 N={N}: single-fault liveness margin (N-1)-q = {margin} >= 1 "
|
|
f"(a single Falcon fault does NOT force all-honest participation)", s,
|
|
expect_unsat=False, kind="CONFIG")
|
|
|
|
# (T3) STALL at N<7: with 2 Falcon-faulty (withholding) the correct set is below
|
|
# quorum, so NO post-fork block can be certified -> the chain STALLS.
|
|
def stall_witness(N, qv, faulty):
|
|
"""Correct signers = N-faulty all sign their single canonical block; if
|
|
N-faulty < qv the cert cannot form (block rejected under blocking)."""
|
|
s = Solver()
|
|
sealA = [Bool(f'sealA_{i}') for i in range(N)]
|
|
correct = [Bool(f'correct_{i}') for i in range(N)]
|
|
s.add(Sum([If(Not(correct[i]), 1, 0) for i in range(N)]) == faulty) # 'faulty' Falcon-faulty
|
|
for i in range(N):
|
|
# faulty validators withhold a valid seal (crash / bad key / correlated defect)
|
|
s.add(Implies(Not(correct[i]), Not(sealA[i])))
|
|
# correct validators all sign the one canonical block
|
|
s.add(Implies(correct[i], sealA[i]))
|
|
s.add(Sum([If(sealA[i], 1, 0) for i in range(N)]) < qv) # cert CANNOT form -> stall
|
|
return s
|
|
for N in (5,):
|
|
s = stall_witness(N, quorum(N), faulty=2)
|
|
check(f"THRESHOLD-T3 STALL at N={N} with 2 Falcon-faulty: correct set {N-2} < "
|
|
f"quorum {quorum(N)} -> no cert can form (post-fork block stalls)", s,
|
|
expect_unsat=False, kind="STALL")
|
|
# and at N=7 with 2 faulty NO stall (cert still forms) -> the reason to grow to 7:
|
|
s = stall_witness(7, quorum(7), faulty=2)
|
|
check(f"THRESHOLD-T3 N=7 with 2 Falcon-faulty: correct set 5 == quorum 5 -> cert "
|
|
f"STILL forms (no stall); this is why blocking needs N>=7", s) # expect UNSAT: cannot stall
|
|
|
|
# =============================================================================
|
|
# AUD-CONSENSUS-1 / -2 FIX: registry size M DECOUPLED from validator count N.
|
|
# -----------------------------------------------------------------------------
|
|
# The reviewed defect: the blocking quorum tracked the DYNAMIC validator-set size
|
|
# N (quorum = ceil(2N/3)) while the signer registry was IMMUTABLE at its anchored
|
|
# size M=N0, and seals were counted by REGISTRY membership (not current-validator
|
|
# membership). So (a) adding a validator raised the quorum above the fixed key
|
|
# count -> HALT, and (b) a removed validator's key kept counting -> a safety gap.
|
|
#
|
|
# The FIX binds BOTH the quorum AND the counted-seal set to ONE well-defined set:
|
|
# eligible = currentValidators INTERSECT registry , k = |eligible|
|
|
# quorum = ceil(2k/3)
|
|
# valid = # distinct ELIGIBLE addresses whose Falcon seal verifies
|
|
# and ECDSA stays decisive (a hybrid block also needs ceil(2N/3) ECDSA seals over
|
|
# the full set N). This section models M != N and machine-checks that the fix
|
|
# removes both bugs, stays live under validator changes, and is never weaker than
|
|
# ECDSA. Every PROOF is unsat-of-negation; every claim is paired with a FIRING
|
|
# control (BUG-DEMO / NEG-CTRL) so the results are demonstrably non-vacuous.
|
|
# =============================================================================
|
|
print("\n### AUD-CONSENSUS-1/-2 FIX: eligible-signer set (immutable registry M != validator count N)\n")
|
|
|
|
def ceil23(x):
|
|
return (2 * x + 2) // 3
|
|
|
|
# ---- BUG-DEMO (firing): the OLD rule HALTS when N grows past the registry. ----
|
|
# Armed with an M=7 manifest, grow the validator set to N=11. Old quorum ceil(2N/3)
|
|
# = 8, but only k=7 keyed-and-current validators can produce a verifying seal, so
|
|
# valid <= 7 < 8 and every post-fork block is REJECTED (deadlock reachable = SAT).
|
|
s = Solver()
|
|
Nv, Mv, kv, qold = Int('N'), Int('M'), Int('k'), Int('qold')
|
|
s.add(Mv == 7, Nv == 11, kv == 7) # k = |V ∩ R| = 7 keyed validators
|
|
s.add(3 * qold >= 2 * Nv, 3 * qold <= 2 * Nv + 2) # OLD quorum = ceil(2N/3) = 8
|
|
s.add(kv < qold) # available signers below OLD quorum
|
|
check("BUG-DEMO (OLD rule) M=7, validators grown to N=11: quorum ceil(2N/3)=8 > k=7 keyed "
|
|
"signers -> post-fork DEADLOCK reachable (the halt this fix removes)", s,
|
|
expect_unsat=False, kind="BUG-DEMO")
|
|
|
|
# ---- FIX-F1 LIVENESS (unbounded): the eligible set always meets its OWN quorum. ----
|
|
# quorum = ceil(2k/3) and there are exactly k eligible signers, so k >= ceil(2k/3)
|
|
# for ALL k -> adding or removing validators can never make the eligible Falcon
|
|
# quorum unreachable. No silent block-production halt is possible from a set change.
|
|
s = Solver()
|
|
k, q = Int('k'), Int('q')
|
|
s.add(k >= 0)
|
|
s.add(3 * q >= 2 * k, 3 * q <= 2 * k + 2) # q = ceil(2k/3)
|
|
s.add(k < q) # negate: eligible below its own quorum
|
|
check("FIX-F1 LIVENESS (all k): eligible-set size k >= ceil(2k/3) -> a validator ADD or REMOVE "
|
|
"can NEVER make the eligible Falcon quorum unreachable (no silent halt)", s)
|
|
|
|
# ---- FIX-F1b CONFIG: adding an UNKEYED validator does not raise the eligible quorum. ----
|
|
# Registry M=7 (armed). The eligible set stays the 7 keyed validators, so quorum
|
|
# stays ceil(2*7/3)=5 (LIVE), regardless of N growth, unlike the OLD ceil(2N/3).
|
|
# N=8, M=7 (one unkeyed added validator), 2 keyed validators briefly offline:
|
|
# OLD quorum ceil(2*8/3)=6, valid=5 -> REJECT (margin erased by the unkeyed add);
|
|
# NEW quorum over eligible ceil(2*7/3)=5, valid=5 -> LIVE.
|
|
s = Solver()
|
|
s.add(Int('v') == 5) # 7 keyed - 2 offline = 5 valid seals
|
|
s.add(Int('v') < ceil23(8)) # 5 < OLD quorum 6 -> OLD rejects
|
|
check("FIX-vs-BUG N=8,M=7 (2 keyed offline): OLD quorum ceil(2*8/3)=6 > valid=5 -> OLD rule "
|
|
"REJECTS (an unkeyed add erased the margin)", s, expect_unsat=False, kind="BUG-DEMO")
|
|
s = Solver()
|
|
s.add(Int('ok') == (1 if 5 >= ceil23(7) else 0))
|
|
s.add(Int('ok') == 1)
|
|
check("FIX-F1b N=8,M=7 (2 keyed offline): NEW eligible quorum ceil(2*7/3)=5 <= valid=5 -> LIVE "
|
|
"(the fix keeps the chain producing where the old rule rejected)", s,
|
|
expect_unsat=False, kind="CONFIG")
|
|
# N=11, M=7: OLD quorum ceil(2*11/3)=8 > all 7 keys -> PERMANENT halt; NEW quorum 5 -> live.
|
|
s = Solver()
|
|
s.add(Int('gap') == ceil23(11) - 7)
|
|
s.add(Int('gap') >= 1) # OLD quorum 8 exceeds every keyed signer
|
|
check("FIX-vs-BUG N=11,M=7: OLD quorum ceil(2*11/3)=8 EXCEEDS all 7 keyed signers -> every "
|
|
"post-fork block PERMANENTLY rejected (the chain-halt bug)", s,
|
|
expect_unsat=False, kind="BUG-DEMO")
|
|
s = Solver()
|
|
s.add(Int('ok') == (1 if 7 >= ceil23(7) else 0))
|
|
s.add(Int('ok') == 1)
|
|
check("FIX-F1b N=11,M=7: NEW eligible quorum ceil(2*7/3)=5 <= 7 keyed signers -> LIVE "
|
|
"(quorum over the eligible set, unaffected by N growth)", s,
|
|
expect_unsat=False, kind="CONFIG")
|
|
|
|
# ---- FIX-F2 SAFETY over the ELIGIBLE set (size k): two conflicting eligible ----
|
|
# quorums are impossible under <= f_e = floor((k-1)/3) equivocating faulty signers.
|
|
# Same intersection argument as B-SAFETY, now proved to hold on the eligible set the
|
|
# fixed rule actually uses (k = |V ∩ R|), for k in {5,7}.
|
|
for k in (5, 7):
|
|
s = blocking_safety(k, quorum(k), faultbound(k))
|
|
check(f"FIX-F2 ELIGIBLE-SAFETY k={k} (q={quorum(k)},f={faultbound(k)}): two conflicting "
|
|
f"blocks cannot both reach the eligible Falcon quorum under <= f equivocators", s)
|
|
|
|
# ---- FIX-F3 REMOVAL-SAFETY (AUD-CONSENSUS-2): a registered-but-removed validator's ----
|
|
# seal cannot count. Model N=5 current validators, M=7 registered keys (2 removed
|
|
# without re-anchor). NEW rule counts only eligible (current) indices.
|
|
N, M = 5, 7
|
|
s = Solver()
|
|
inV = [Bool(f'inV_{i}') for i in range(M)] # is registry index i a CURRENT validator?
|
|
counts = [Bool(f'c_{i}') for i in range(M)] # does index i's seal count (NEW rule)?
|
|
s.add(Sum([If(inV[i], 1, 0) for i in range(M)]) == N) # 5 of the 7 keyed are current
|
|
for i in range(M):
|
|
s.add(Implies(counts[i], inV[i])) # NEW: only eligible indices count
|
|
s.add(Or(*[And(counts[i], Not(inV[i])) for i in range(M)])) # negate: an ex-validator counted
|
|
check("FIX-F3 REMOVAL-SAFETY N=5,M=7: no registered-but-removed validator's seal can count "
|
|
"toward the eligible quorum (counted set is a subset of current validators)", s)
|
|
|
|
# NEG-CTRL F3: the OLD registry-membership rule LETS an ex-validator's key count.
|
|
s = Solver()
|
|
inV = [Bool(f'inV_{i}') for i in range(M)]
|
|
counts = [Bool(f'c_{i}') for i in range(M)]
|
|
s.add(Sum([If(inV[i], 1, 0) for i in range(M)]) == N)
|
|
# OLD rule: counting requires only registry membership (every index is registered), NOT inV
|
|
s.add(Or(*[And(counts[i], Not(inV[i])) for i in range(M)]))
|
|
check("NEG-CTRL F3 N=5,M=7: the OLD (registry-membership) rule LETS a removed validator's key "
|
|
"count (proves the current-validator intersection is load-bearing for safety)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- FIX-F4 NEVER-WEAKER-THAN-ECDSA: hybrid-valid => ECDSA-valid, for ANY k. ----
|
|
# A hybrid block needs the ECDSA quorum over the FULL set N and the eligible Falcon
|
|
# quorum over k <= N. So even though the Falcon leg is over a subset, the block is
|
|
# never accepted without the full ECDSA quorum -> never weaker than ECDSA-only.
|
|
s = Solver()
|
|
e, fal, Nn, kk, qN, qk = Int('e'), Int('fal'), 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) # qN = ceil(2N/3) (ECDSA)
|
|
s.add(3 * qk >= 2 * kk, 3 * qk <= 2 * kk + 2) # qk = ceil(2k/3) (eligible Falcon)
|
|
s.add(e >= qN, fal >= qk) # hybrid-valid
|
|
s.add(e < qN) # negate: NOT ecdsa-valid
|
|
check("FIX-F4 NEVER-WEAKER (all N,k): every hybrid-valid block (ECDSA quorum over N AND eligible "
|
|
"Falcon quorum over k) is ECDSA-valid -> the fixed rule is never weaker than ECDSA-only", s)
|
|
|
|
# NEG-CTRL F4: the Falcon eligible quorum is a REAL added gate (ecdsa-valid can be hybrid-invalid).
|
|
s = Solver()
|
|
e, fal, qN7, qk7 = Int('e'), Int('fal'), quorum(7), quorum(7)
|
|
s.add(e >= qN7, fal < qk7) # ECDSA ok, eligible Falcon short
|
|
check("NEG-CTRL F4 N=k=7: an ECDSA-valid block can be hybrid-INVALID when the eligible Falcon "
|
|
"quorum is short (proves the eligible Falcon leg is a genuine added gate)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- FIX-F5 FAIL-CLOSED on an empty eligible set (the fail-OPEN trap). ----
|
|
# With k=0 the naive threshold ceil(2*0/3)=0 is trivially met by valid=0 (fail-OPEN).
|
|
# NEG-CTRL shows the trap; the FIX guards it (k==0 -> REJECT in blocking mode).
|
|
s = Solver()
|
|
valid, q0, k0 = Int('valid'), Int('q0'), Int('k')
|
|
s.add(k0 == 0, 3 * q0 >= 2 * k0, 3 * q0 <= 2 * k0 + 2) # q0 = ceil(0) = 0
|
|
s.add(valid == 0, valid >= q0) # naive accept holds
|
|
check("NEG-CTRL F5 FAIL-OPEN trap: with k=0 the naive check valid(0) >= quorum(0)=0 ACCEPTS "
|
|
"(this is why the fixed rule must fail-closed on an empty eligible set)", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
s = Solver()
|
|
accepted, k0 = Bool('accepted'), Int('k')
|
|
s.add(k0 == 0)
|
|
s.add(Implies(k0 == 0, Not(accepted))) # FIX guard: empty eligible -> reject
|
|
s.add(accepted) # negate: accepted anyway
|
|
check("FIX-F5 FAIL-CLOSED: with the empty-eligible guard, a k=0 (unbound / no-coverage) block "
|
|
"is never accepted in blocking mode (no fail-open)", s)
|
|
|
|
# ---- 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 fault margin.
|
|
for N in (7, 9):
|
|
s = Solver()
|
|
s.add(Int('eq') == (ceil23(N) - quorum(N))) # eligible quorum(k=N) - ECDSA quorum(N)
|
|
s.add(Int('eq') != 0) # negate: they differ
|
|
check(f"FIX-ARM N={N}: with full coverage (k=N) the eligible quorum ceil(2N/3)={ceil23(N)} "
|
|
f"EQUALS the ECDSA quorum -> arming at full margin (the required arming invariant)", s)
|
|
|
|
# =============================================================================
|
|
print("\n=== SUMMARY (Falcon BLOCKING mode) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" PROVED: In BLOCKING mode the Falcon quorum certificate is SAFE -- <= f")
|
|
print(" equivocating Falcon-faulty validators cannot certify two conflicting")
|
|
print(" blocks (N in {4,5,7}) -- and LIVE at the fault bound (N-f >= quorum, all")
|
|
print(" N). The N>=7 requirement is machine-checked: N=7 is the smallest set that")
|
|
print(" is BOTH safe (f>=2) and live (N-2>=quorum) against 2 Falcon faults. It is")
|
|
print(" also the next BFT-optimal 3f+1 size, and unlike the current N=5 (zero")
|
|
print(" single-fault margin) it leaves margin > 0 over quorum for a single fault. At")
|
|
print(" N in {4,5} two Falcon faults drop the correct set below quorum and the")
|
|
print(" post-fork chain STALLS (shown reachable). Negative controls FIRE: dropping")
|
|
print(" the <= f bound or lowering the quorum breaks blocking safety.")
|
|
print(" AUD-CONSENSUS-1/-2 FIX (registry size M != validator count N): the FIXED rule")
|
|
print(" binds BOTH the quorum AND the counted-seal set to eligible = currentValidators")
|
|
print(" INTERSECT registry (k=|eligible|, quorum=ceil(2k/3)). Machine-checked: the OLD")
|
|
print(" rule HALTS when N grows past M (BUG-DEMO fires at N=11,M=7); the fix stays LIVE")
|
|
print(" for all k (F1, k >= ceil(2k/3)); is SAFE over the eligible set (F2); EXCLUDES")
|
|
print(" removed-validator keys (F3, with the OLD-rule leak firing as a control); is")
|
|
print(" NEVER weaker than ECDSA (F4, hybrid-valid => ECDSA-valid over N); FAIL-CLOSES on")
|
|
print(" an empty eligible set (F5, with the fail-open trap firing as a control); and arms")
|
|
print(" at full margin under coverage k=N (FIX-ARM).")
|
|
print(" BOUNDARY: bounded per-N/per-k safety; unbounded liveness identity; DESIGN")
|
|
print(" combinatorics not Besu bytecode; mainnet Falcon layer is LOG-ONLY, not")
|
|
print(" blocking (blocking needs N>=7 + an ADDRESS-BOUND registry covering the set).")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|