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.
144 lines
7.1 KiB
Python
144 lines
7.1 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# qbft_digest_keyed_smt.py
|
|
#
|
|
# MACHINE-CHECKED (z3) model of the DIGEST-KEYED VOTE-TALLY fix applied to the AERE
|
|
# second-client QBFT engine on 2026-07-14 (audit Finding A). This is the fix that
|
|
# actually SHIPPED after two proposal-adoption patches were soak-rejected: instead
|
|
# of gating adoption, keep the prepare/commit tallies keyed BY DIGEST and count a
|
|
# quorum only over the CURRENT digest.
|
|
#
|
|
# THE BUG (Finding A): the tallies were flat sets keyed by voter address only. On a
|
|
# conflicting proposal that changed the current digest from D0 to D1 at the same
|
|
# (height,round), the prepares already cast for D0 stayed in the flat set and were
|
|
# then counted toward D1 -> an UNJUSTIFIED commit quorum for a block nobody prepared
|
|
# -> cross-client double-commit / fork.
|
|
#
|
|
# THE FIX: tallies are maps `digest -> voters`; `PrepareCount()`/`CommitCount()`
|
|
# count only `tally[current_digest]`. A vote cast for D0 lives under D0 and can never
|
|
# be counted toward D1.
|
|
#
|
|
# This model proves the fix removes the mis-attribution, and its NEGATIVE CONTROL
|
|
# shows the flat tally genuinely had the bug (non-vacuous). Besu quorum
|
|
# quorum(N)=ceil(2N/3), fault bound f(N)=floor((N-1)/3).
|
|
# HONEST BOUNDARY: bounded per-N checks of the counting rule (message combinatorics),
|
|
# not the C# bytecode; complements the shipped fix's adversarial-soak verification
|
|
# (0 forks, Besu parity). Chain 2800 consensus is classical ECDSA QBFT.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat
|
|
|
|
def quorum(n): return (2 * n + 2) // 3
|
|
def faultbound(n): return (n - 1) // 3
|
|
|
|
results = []
|
|
def check(name, s, expect_unsat=True, kind="PROOF"):
|
|
r = s.check()
|
|
ok = (r == unsat) if expect_unsat else (r == sat)
|
|
tag = ("PROVED" if ok else "FAILED") if expect_unsat else ("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'})")
|
|
return ok
|
|
|
|
OPT = [4, 7, 10, 13] # N = 3f+1 optimal sizes
|
|
|
|
print("=" * 78)
|
|
print("P1 FLAT TALLY (the BUG) => a conflicting-digest mis-count can fake a quorum")
|
|
print("=" * 78)
|
|
# Per-validator model at one (height,round). Each validator i either voted for D0, for
|
|
# D1, or not at all. A FLAT tally (the pre-fix bug) that adopts D1 counts EVERY voter
|
|
# (D0-voters + D1-voters) toward D1. Show: even when FEWER than quorum validators
|
|
# actually voted D1, the flat count can reach quorum -> a fake quorum for D1. (SAT.)
|
|
for N in OPT:
|
|
f = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
v0 = [Bool(f"v0_{i}") for i in range(N)] # voted for D0
|
|
v1 = [Bool(f"v1_{i}") for i in range(N)] # voted for D1
|
|
for i in range(N):
|
|
s.add(Not(And(v0[i], v1[i]))) # an honest voter votes at most one digest
|
|
real_d1 = Sum([If(v1[i], 1, 0) for i in range(N)])
|
|
flat_d1 = Sum([If(Or(v0[i], v1[i]), 1, 0) for i in range(N)]) # BUG: pool D0+D1 voters
|
|
s.add(real_d1 < q) # D1 did NOT truly reach quorum
|
|
s.add(flat_d1 >= q) # ...but the flat (buggy) count says it did
|
|
check(f"N={N} q={q}: flat tally reports quorum for D1 while real D1 votes < q "
|
|
f"(fake quorum from mis-attribution)", s, expect_unsat=False, kind="NEG-CONTROL")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P2 DIGEST-KEYED TALLY (the FIX) => the count equals the REAL per-digest votes")
|
|
print("=" * 78)
|
|
# The fix counts tally[D1] = only D1-voters. Prove: it is IMPOSSIBLE for the digest-keyed
|
|
# count of D1 to reach quorum while the real number of D1 voters is below quorum. (UNSAT.)
|
|
for N in OPT:
|
|
f = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
v0 = [Bool(f"v0_{i}") for i in range(N)]
|
|
v1 = [Bool(f"v1_{i}") for i in range(N)]
|
|
for i in range(N):
|
|
s.add(Not(And(v0[i], v1[i])))
|
|
keyed_d1 = Sum([If(v1[i], 1, 0) for i in range(N)]) # FIX: count only D1's own voters
|
|
real_d1 = keyed_d1
|
|
s.add(real_d1 < q)
|
|
s.add(keyed_d1 >= q) # can the fixed count over-report? -> UNSAT
|
|
check(f"N={N} q={q}: digest-keyed count for D1 reaches quorum while real D1 votes < q "
|
|
f"(over-count impossible)", s, expect_unsat=True, kind="PROOF")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P3 SAFETY under the fix => two distinct digests cannot BOTH reach quorum")
|
|
print("=" * 78)
|
|
# With per-digest counts, D0 and D1 both reaching quorum needs q honest-or-byzantine
|
|
# voters each. Honest validators vote at most one digest; up to f Byzantine may vote
|
|
# BOTH. Prove both-quorum is impossible (the classical intersection, now expressed on
|
|
# the digest-keyed tally so the fix is shown to preserve agreement). UNSAT.
|
|
for N in OPT:
|
|
f = faultbound(N); q = quorum(N)
|
|
s = Solver()
|
|
byz = [Bool(f"byz_{i}") for i in range(N)]
|
|
v0 = [Bool(f"v0_{i}") for i in range(N)]
|
|
v1 = [Bool(f"v1_{i}") for i in range(N)]
|
|
s.add(Sum([If(byz[i], 1, 0) for i in range(N)]) <= f)
|
|
for i in range(N):
|
|
s.add(Implies(Not(byz[i]), Not(And(v0[i], v1[i])))) # honest: one digest only
|
|
c0 = Sum([If(v0[i], 1, 0) for i in range(N)])
|
|
c1 = Sum([If(v1[i], 1, 0) for i in range(N)])
|
|
s.add(c0 >= q); s.add(c1 >= q) # both reach the (correct) digest-keyed quorum
|
|
check(f"N={N} f={f} q={q}: digest-keyed tallies let two distinct digests BOTH reach "
|
|
f"quorum (safety break)", s, expect_unsat=True, kind="PROOF")
|
|
|
|
print()
|
|
print("=" * 78)
|
|
print("P3-NEG lowering quorum to ceil(N/2) DOES let both reach quorum (threshold load-bearing)")
|
|
print("=" * 78)
|
|
for N in [4, 7, 10]:
|
|
f = faultbound(N); qbad = (N + 1) // 2
|
|
s = Solver()
|
|
byz = [Bool(f"byz_{i}") for i in range(N)]
|
|
v0 = [Bool(f"v0_{i}") for i in range(N)]
|
|
v1 = [Bool(f"v1_{i}") for i in range(N)]
|
|
s.add(Sum([If(byz[i], 1, 0) for i in range(N)]) <= f)
|
|
for i in range(N):
|
|
s.add(Implies(Not(byz[i]), Not(And(v0[i], v1[i]))))
|
|
c0 = Sum([If(v0[i], 1, 0) for i in range(N)]); c1 = Sum([If(v1[i], 1, 0) for i in range(N)])
|
|
s.add(c0 >= qbad); s.add(c1 >= qbad)
|
|
check(f"N={N} qbad=ceil(N/2)={qbad}: two digests both reach the LOWERED quorum", s,
|
|
expect_unsat=False, kind="NEG-CONTROL")
|
|
|
|
print("\n=== SUMMARY (digest-keyed vote tally: the shipped Finding-A fix) ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print(" ESTABLISHED: the FLAT tally could report a quorum for a digest from votes cast")
|
|
print(" for a DIFFERENT digest (P1, the Finding-A bug, CEX-FOUND); the DIGEST-KEYED tally")
|
|
print(" cannot over-count (P2, PROVED) and preserves agreement - two distinct digests")
|
|
print(" can never both reach the ceil(2N/3) quorum (P3, PROVED). The threshold is")
|
|
print(" load-bearing (P3-NEG fires at ceil(N/2)). This is the counting-rule proof behind")
|
|
print(" the shipped fix, which additionally passed adversarial soaks (0 forks, Besu parity).")
|
|
print(" HONEST: bounded per-N checks of the tally combinatorics, not the C# bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|