Formal: partitii de retea si view-change x certificat PQ dovedite la N=9, cu controale negative
partition_safety_smt.py (N=9 f=2 q=6): split-brain imposibil, starvatie clasificata, vindecare fara fork. anchor_viewchange_smt.py: o schimbare de runda pe ancora nu da doua certificate valide diferite, si unicitatea vine din legarea de bloc, nu din K=3 sigilii (< cvorum). Rulatorul cablat: 35 modele, 282 PROVED + 149 CEX, 0 FAILED.
This commit is contained in:
Aere Network
parent
0164207076
commit
a2f4d835a3
142
formal-consensus/RULEAZA-TOT.md
Normal file
142
formal-consensus/RULEAZA-TOT.md
Normal file
@ -0,0 +1,142 @@
|
|||||||
|
# RULEAZA-TOT: verificarea formala a consensului AERE, un capat la altul
|
||||||
|
|
||||||
|
Rularea completa a tot ce se poate verifica automat pe consensul AERE (QBFT / IBFT 2.0,
|
||||||
|
chain 2800), cu doua metode independente:
|
||||||
|
|
||||||
|
- **SMT (z3)** parametric, in acest dosar (`formal-consensus/*_smt.py`): dovedeste fiecare
|
||||||
|
proprietate aratand ca negatia ei e UNSAT, plus un control negativ care planteaza
|
||||||
|
incalcarea si trebuie sa iasa SAT. Scaleaza la N=9 (flota reala).
|
||||||
|
- **TLA+ / TLC** exhaustiv, in `aerenew/formal-tla/`: verifica prin explorare de stari la
|
||||||
|
scara mica (N=4), unde combinatoria e suficienta.
|
||||||
|
|
||||||
|
Regula peste tot: **niciun model nu se raporteaza verde daca nu poate iesi ROSU.** Fiecare
|
||||||
|
proprietate are un control negativ rulat.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 1. Suita SMT (z3) - o singura comanda
|
||||||
|
|
||||||
|
```
|
||||||
|
cd aerenew/publish-bundle/aere-research/formal-consensus
|
||||||
|
python run_consensus_verification.py
|
||||||
|
```
|
||||||
|
|
||||||
|
Ruleaza TOATE modelele `*_smt.py` din dosar (garda de completitudine refuza sa iasa verde
|
||||||
|
daca vreun model prezent nu e cablat). Tipareste PASS/FAIL per model, timpul fiecaruia, si
|
||||||
|
tally-ul de linii de verdict.
|
||||||
|
|
||||||
|
**Masurat 2026-08-24** (Windows, python 3.14 / z3 4.16.0; timpii variaza cu masina):
|
||||||
|
|
||||||
|
```
|
||||||
|
models run: 35 passed: 35 (14 consensus + 11 contract + 10 application)
|
||||||
|
verdict lines: 282 PROVED 149 CEX-FOUND 0 FAILED
|
||||||
|
wall time: ~39s total (cel mai lent: qbft_safety_smt.py ~23s)
|
||||||
|
coverage: 35 of 35 *_smt.py files wired
|
||||||
|
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)
|
||||||
|
```
|
||||||
|
|
||||||
|
Cele 14 modele de consens includ cele adaugate pe 24 august:
|
||||||
|
|
||||||
|
| model | ce dovedeste | N |
|
||||||
|
|---|---|---|
|
||||||
|
| `qbft_safety_smt.py` | agreement (quorum-intersection unbounded; one-round + cross-round locking) | 4,5,7,10,13,16 |
|
||||||
|
| `qbft_liveness_smt.py` | progres post-GST (f+1 runde ating un proposer onest) | 4,5,7 |
|
||||||
|
| `qbft_locking_smt.py` | locking IBFT 2.0 pe rolurile motorului (view-change / round-change) | 4,5,7 |
|
||||||
|
| `qbft_prepare_counting_smt.py`, `qbft_digest_keyed_smt.py` | numararea voturilor (bug+fix 2026-07-14) | mic |
|
||||||
|
| `falcon_blocking_smt.py`, `anchor_blocking_quorum_smt.py` | pragul de sigilii pe ancora (K=3 din 9) | 9 |
|
||||||
|
| `qbft_pqc_activation_smt.py` | tranzitia log-only -> blocant | - |
|
||||||
|
| **`partition_safety_smt.py`** (NOU) | **partitii de retea: split-brain, starvatie, vindecare** | **9 param.** |
|
||||||
|
| **`anchor_viewchange_smt.py`** (NOU) | **o schimbare de runda pe o ancora nu da doua certificate valide** | **9** |
|
||||||
|
| `pqanchor_ceiling_monotonicity_smt.py` | plafonul de urgenta doar coboara K | - |
|
||||||
|
| `registry_index_binding_smt.py`, `registry_rotation_coverage_smt.py` | registrul de chei pe inaltime | - |
|
||||||
|
|
||||||
|
> Nota: cele trei modele de registru/plafon existau in dosar din 15-19 august dar NU erau
|
||||||
|
> cablate in rulator (garda de completitudine il facea sa iasa cu cod 2). Cablate pe 24 august
|
||||||
|
> impreuna cu cele doua modele noi.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 2. TLA+ / TLC exhaustiv - partitiile de retea (NOU, 24 august)
|
||||||
|
|
||||||
|
Modelul `aerenew/formal-tla/QBFTPartition.tla` face partitia un DEFECT modelat explicit
|
||||||
|
(un predicat pe livrarea mesajelor intre grupuri) si o verifica exhaustiv la N=4. Sase
|
||||||
|
configuratii, fiecare cu perechea ei pozitiv/negativ.
|
||||||
|
|
||||||
|
### Rularea (WSL, mult mai rapid decat pe Windows)
|
||||||
|
|
||||||
|
Scrie un script, copiaza-l, ruleaza-l fara ghilimele inline (comenzile inline se mangleaza
|
||||||
|
prin wsl.exe). Toate rularile folosesc `-deadlock` fiindca protocolul se TERMINA in mod normal
|
||||||
|
(toti au decis) si terminarea nu e un defect:
|
||||||
|
|
||||||
|
```bash
|
||||||
|
# copie dosarul in /root (rulare rapida, in afara /mnt)
|
||||||
|
mkdir -p /root/ftla
|
||||||
|
cp -f /mnt/c/Users/Jessica/Documents/AereNetwork/aerenew/formal-tla/*.tla /root/ftla/
|
||||||
|
cp -f /mnt/c/Users/Jessica/Documents/AereNetwork/aerenew/formal-tla/*.cfg /root/ftla/
|
||||||
|
cp -f /mnt/c/Users/Jessica/Documents/AereNetwork/aerenew/formal-tla/tla2tools.jar /root/ftla/
|
||||||
|
cd /root/ftla
|
||||||
|
for CFG in MCpart_safety MCpart_safety_witness MCpart_safety_negctrl \
|
||||||
|
MCpart_noprogress MCpart_liveness MCpart_liveness_negctrl; do
|
||||||
|
java -XX:+UseParallelGC -cp tla2tools.jar tlc2.TLC QBFTPartition -config ${CFG}.cfg -deadlock
|
||||||
|
done
|
||||||
|
```
|
||||||
|
|
||||||
|
Lanseaza din PowerShell:
|
||||||
|
`MSYS_NO_PATHCONV=1 wsl.exe -d Ubuntu-24.04 -- bash /mnt/c/.../script.sh`
|
||||||
|
|
||||||
|
### Rezultate masurate 2026-08-24 (WSL, OpenJDK 21, exhaustiv, 0 stari ramase in coada)
|
||||||
|
|
||||||
|
| config | ce verifica | asteptat | rezultat | timp |
|
||||||
|
|---|---|---|---|---|
|
||||||
|
| `MCpart_safety` | 3-1, quorum 3, heal: SAFETY se pastreaza | fara eroare | **No error** (1866 stari) | ~3s |
|
||||||
|
| `MCpart_safety_witness` | acelasi, invariant `NoCommit` | VIOLARE (commit e atins) | **NoCommit violated** -> `committed={a}` | ~2s |
|
||||||
|
| `MCpart_safety_negctrl` | 2-2, quorum COBORAT la 2 | VIOLARE (fork) | **NoFork violated** -> `committed={a,b}` (v1->a, v3->b) | ~4s |
|
||||||
|
| `MCpart_noprogress` | 2-2, quorum 3, FARA vindecare, invariant `NoCommit` | fara eroare | **No error** (81 stari; nimic nu se finalizeaza) | ~2s |
|
||||||
|
| `MCpart_liveness` | 2-2, quorum 3, vindecare, `EventualCommit` | fara eroare | **No error** (liveness revine dupa heal) | ~3s |
|
||||||
|
| `MCpart_liveness_negctrl` | 2-2, quorum 3, FARA vindecare, `EventualCommit` | VIOLARE | **EventualCommit violated** (stuttering, `committed={}`) | ~2s |
|
||||||
|
|
||||||
|
Cele trei perechi acopera exact intrebarile cerute:
|
||||||
|
- **SAFETY se pastreaza in ambele parti**: `MCpart_safety` verde, si non-vacuu prin `witness`
|
||||||
|
(partea majoritara chiar finalizeaza). Controlul negativ `safety_negctrl` arata ca ce
|
||||||
|
opreste fork-ul e quorum-ul ceil(2N/3): coborat la 2, cele doua parti finalizeaza `a` si `b`.
|
||||||
|
- **LIVENESS se pierde in grupul fara quorum**: `MCpart_noprogress` (nimic nu se finalizeaza
|
||||||
|
intr-o partitie 2-2 nevindecata).
|
||||||
|
- **LIVENESS revine la vindecare**: `MCpart_liveness` verde; controlul negativ
|
||||||
|
`liveness_negctrl` arata ca fara pasul de vindecare `EventualCommit` PICA (heal e cauza).
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 3. TLA+ / TLC - modelul QBFT complet (agreement + view-change + echivocatie)
|
||||||
|
|
||||||
|
`aerenew/formal-tla/QBFT.tla` cu `MCsafety.cfg` (N=4) / `MCsafety7.cfg` (N=7) si
|
||||||
|
`MCliveness.cfg`. **Masurat 2026-07-19 si 2026-08-24: aceste configuratii NU se termina** in
|
||||||
|
bugetul local (spatiul de stari e de ordinul zecilor de milioane; `MCliveness` a generat
|
||||||
|
543k stari distincte in 197s cu 527k inca in coada). Ce e stabilit acolo e un martor
|
||||||
|
explicit-state partial (9,35 milioane de stari fara violare pe N=4 round-0), NU o verificare
|
||||||
|
completa. Vezi `TLC-RUN-REPORT.md`. Miezul all-N (quorum-intersection, agreement sub locking)
|
||||||
|
e deja dovedit pentru ORICE N de suita SMT; TLA+ e metoda independenta, iar valoarea lui la
|
||||||
|
partitii este ca `QBFTPartition.tla` chiar SE TERMINA exhaustiv (single-height), spre
|
||||||
|
deosebire de modelul complet.
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## 4. Cross-check optional: quint / Apalache
|
||||||
|
|
||||||
|
`FalconQuorum.qnt` e un cross-check secundar (vezi `CONSENSUS-VERIFICATION-2026-07-12.md`
|
||||||
|
pentru comenzile `quint run`).
|
||||||
|
|
||||||
|
---
|
||||||
|
|
||||||
|
## Granita cinstita (se citeste, nu se sare)
|
||||||
|
|
||||||
|
- Model checking **nu e demonstratie completa.** SMT dovedeste combinatoria design-ului
|
||||||
|
(numararea voturilor, intersectia quorum-urilor, legarea certificatului), nu bytecode-ul
|
||||||
|
Besu/EVM. TLC verifica exhaustiv doar configuratia finita enuntata (N=4 la partitii).
|
||||||
|
- SMT parametric la N=9 dovedeste proprietatea pentru **acel** N; miezul aritmetic
|
||||||
|
(quorum-intersection, 2q>N) e unbounded in N.
|
||||||
|
- Consensul chain 2800 comita cu **ECDSA clasic** secp256k1; ancora PQ e ADITIVA. Nimic de
|
||||||
|
aici nu implica "consens post-cuantic".
|
||||||
|
- Primitivele criptografice (injectivitatea keccak, soliditatea gateway-ului SP1, validarea
|
||||||
|
sigiliului Falcon) sunt tratate ca `[VERIFY]`, modelate, nu re-dovedite.
|
||||||
|
- Ancora foloseste K=3 = **f+1**, NU un quorum. Unicitatea certificatului vine din legarea la
|
||||||
|
blocul finalizat (dovada `anchor_viewchange_smt.py`), nu din intersectia sigiliilor.
|
||||||
246
formal-consensus/anchor_viewchange_smt.py
Normal file
246
formal-consensus/anchor_viewchange_smt.py
Normal file
@ -0,0 +1,246 @@
|
|||||||
|
#!/usr/bin/env python3
|
||||||
|
# -----------------------------------------------------------------------------
|
||||||
|
# anchor_viewchange_smt.py
|
||||||
|
#
|
||||||
|
# MACHINE-CHECKED (z3) that a VIEW CHANGE (QBFT round change) during an ANCHOR
|
||||||
|
# height cannot produce two different valid post-quantum anchor certificates.
|
||||||
|
# This closes the interaction the reviewer flagged: pqfinality_smt.py proves the
|
||||||
|
# certificate ACCEPTANCE guards in isolation, and qbft_safety_smt.py L3 proves
|
||||||
|
# cross-round agreement in isolation; this model proves they COMPOSE, so a round
|
||||||
|
# change at an anchor height (13,014,000 + 32k on chain 2800) cannot yield two
|
||||||
|
# conflicting certificates.
|
||||||
|
#
|
||||||
|
# THE HONEST SUBTLETY, stated up front. The anchor certificate carries K = 3
|
||||||
|
# distinct valid Falcon seals, and K = f + 1 (3 of 9) is NOT a quorum. So the
|
||||||
|
# seals ALONE do not make the certificate unique: two different anchor payloads
|
||||||
|
# could each collect 3 distinct valid registry seals if signers equivocate
|
||||||
|
# (NEG-CTRL C proves this). The anchor's uniqueness comes from a different guard:
|
||||||
|
# the 32-byte digest under keccak (vanityData element 0) is BOUND to the block
|
||||||
|
# that QBFT FINALIZED at that height, and QBFT finalizes exactly ONE block there,
|
||||||
|
# across all rounds, by the IBFT 2.0 locking rule. A view change re-proposes the
|
||||||
|
# locked value, so it cannot manufacture a second finalized block, hence not a
|
||||||
|
# second bindable digest.
|
||||||
|
#
|
||||||
|
# We model (N = 9, f = 2, quorum 6):
|
||||||
|
# L ANCHOR VIEW-CHANGE AGREEMENT: a compact two-round per-validator commit
|
||||||
|
# model with IBFT locking shows only ONE block value is finalized at the
|
||||||
|
# anchor height, even across a round change. (self-contained; mirrors L3)
|
||||||
|
# AV1 given that unique finalized block, two valid certificates (built in two
|
||||||
|
# DIFFERENT rounds -- a view change) cannot carry different block digests.
|
||||||
|
# AV2 the composed statement: no view change at an anchor height yields two
|
||||||
|
# valid certificates over different blocks.
|
||||||
|
# Each is paired with a firing NEGATIVE CONTROL:
|
||||||
|
# A drop the "digest bound to the FINALIZED block" guard -> a cert over a merely
|
||||||
|
# PROPOSED block in each round -> two valid certs for different blocks (SAT).
|
||||||
|
# B drop the locking rule -> two rounds finalize different blocks -> two certs
|
||||||
|
# over different blocks (SAT).
|
||||||
|
# C drop the binding and rely on K=3 seals alone -> two different digests each
|
||||||
|
# collect 3 distinct valid registry seals (SAT): proves K=f+1 is NOT what
|
||||||
|
# gives uniqueness, the block binding is.
|
||||||
|
#
|
||||||
|
# keccak256 is modelled as an INJECTIVE uninterpreted function where the argument
|
||||||
|
# rests on "a different block gives a different digest" [VERIFY: keccak256]. This
|
||||||
|
# checks the DESIGN-level composition, NOT the compiled EVM/Besu bytecode.
|
||||||
|
# -----------------------------------------------------------------------------
|
||||||
|
from z3 import (Int, Bool, Function, IntSort, Solver, And, Or, Not, Implies, If,
|
||||||
|
Sum, sat, unsat)
|
||||||
|
|
||||||
|
def quorum(n): return (2 * n + 2) // 3
|
||||||
|
def faultbound(n): return (n - 1) // 3
|
||||||
|
|
||||||
|
N, Q, F = 9, quorum(9), faultbound(9) # live fleet: 9, quorum 6, f 2
|
||||||
|
K = 3 # anchor seal floor (f+1, since 2026-08-14)
|
||||||
|
NKEYS = 9 # registry validators that can seal
|
||||||
|
|
||||||
|
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(f"### AERE anchor x view-change: no round change yields two valid certificates "
|
||||||
|
f"(N={N}, q={Q}, f={F}, K={K})\n")
|
||||||
|
|
||||||
|
NONE, A, B = 0, 1, 2
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# L ANCHOR VIEW-CHANGE AGREEMENT (self-contained). Two rounds r in {0,1} at the
|
||||||
|
# SAME anchor height. prep[i][r], comm[i][r] in {NONE,A,B}. A value is finalized
|
||||||
|
# at round r iff a COMMIT quorum forms, which needs a PREPARE quorum, and honest
|
||||||
|
# validators LOCK: at r>0 they only PREPARE the highest earlier prepared value
|
||||||
|
# (the IBFT round-change justification). Claim: not both A and B finalized across
|
||||||
|
# the two rounds. UNSAT = only one block is finalized at the anchor height, even
|
||||||
|
# through a view change.
|
||||||
|
# =============================================================================
|
||||||
|
def anchor_two_round(locking=True):
|
||||||
|
s = Solver()
|
||||||
|
R = 2
|
||||||
|
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)
|
||||||
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= F)
|
||||||
|
def cnt(mat, r, v): return Sum([If(mat[i][r] == v, 1, 0) for i in range(N)])
|
||||||
|
preparedA = [cnt(prep, r, A) >= Q for r in range(R)]
|
||||||
|
preparedB = [cnt(prep, r, B) >= Q 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) >= Q for r in range(R)]
|
||||||
|
committedB = [cnt(comm, r, B) >= Q for r in range(R)]
|
||||||
|
for i in range(N):
|
||||||
|
for r in range(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 = prepared_val[0] # highest earlier prepared value (only round 0 earlier)
|
||||||
|
s.add(Implies(And(honest[i], prep[i][r] != NONE, hp != NONE), prep[i][r] == hp))
|
||||||
|
return s, committedA, committedB
|
||||||
|
|
||||||
|
s, cA, cB = anchor_two_round(locking=True)
|
||||||
|
s.add(Or(*cA)); s.add(Or(*cB))
|
||||||
|
check("L anchor view-change agreement: across a round change at one anchor height, "
|
||||||
|
"two different blocks cannot both be finalized (IBFT locking)", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL B: drop the locking rule -> a view change finalizes a DIFFERENT
|
||||||
|
# block in round 1, so two blocks are finalized (and later two certificates).
|
||||||
|
s, cA, cB = anchor_two_round(locking=False)
|
||||||
|
s.add(Or(*cA)); s.add(Or(*cB))
|
||||||
|
check("NEG-CTRL B: without IBFT locking, a round change at the anchor height "
|
||||||
|
"finalizes two different blocks (the lock is load-bearing)", s,
|
||||||
|
expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# AV1 CERTIFICATE UNIQUENESS given a unique finalized block. digest is an
|
||||||
|
# INJECTIVE hash of the block [VERIFY: keccak256]. A valid anchor certificate is
|
||||||
|
# BOUND to the finalized block: cert.d == digest(finalizedBlock). Two certificates
|
||||||
|
# built in two DIFFERENT rounds (a view change) are each bound to the SAME unique
|
||||||
|
# finalized block, so their digests are equal. Negation (different digests) UNSAT.
|
||||||
|
# =============================================================================
|
||||||
|
digest = Function('digest', IntSort(), IntSort()) # keccak(block) -> 32-byte id
|
||||||
|
s = Solver()
|
||||||
|
blk = Int('finalizedBlock') # the unique QBFT-finalized block at h
|
||||||
|
r1, r2 = Int('r1'), Int('r2')
|
||||||
|
d1, d2 = Int('d1'), Int('d2') # digests carried by the two certs
|
||||||
|
k1, k2 = Int('k1'), Int('k2') # seal counts of the two certs
|
||||||
|
s.add(r1 != r2) # a view change happened between them
|
||||||
|
# binding guard (real design): each cert's digest is over the finalized block
|
||||||
|
s.add(d1 == digest(blk), d2 == digest(blk))
|
||||||
|
# seal floor guard (both certs carry a valid K-of-N seal set)
|
||||||
|
s.add(k1 >= K, k2 >= K)
|
||||||
|
s.add(d1 != d2) # NEGATION: two DIFFERENT valid digests
|
||||||
|
check("AV1 certificate uniqueness: two certificates built in different rounds, both "
|
||||||
|
"bound to the unique finalized block, cannot carry different digests", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL A: drop the binding guard -> each round's cert carries its OWN
|
||||||
|
# proposed-block digest, and nothing forces the two to agree. Two valid
|
||||||
|
# certificates over different blocks become expressible. (Quantifier-free:
|
||||||
|
# two distinct digests directly stand for two different proposed blocks.)
|
||||||
|
s = Solver()
|
||||||
|
r1, r2 = Int('r1'), Int('r2')
|
||||||
|
d1, d2 = Int('d1'), Int('d2') # each round's own cert digest
|
||||||
|
k1, k2 = Int('k1'), Int('k2')
|
||||||
|
s.add(r1 != r2) # a view change happened
|
||||||
|
# NO binding to a single finalized block: nothing constrains d1, d2 to be equal
|
||||||
|
s.add(k1 >= K, k2 >= K) # both carry a K-of-N seal set
|
||||||
|
s.add(d1 != d2) # two different valid digests
|
||||||
|
check("NEG-CTRL A: without the digest->FINALIZED-block binding, a view change "
|
||||||
|
"produces two valid certificates over different proposals (binding is "
|
||||||
|
"load-bearing)", s, expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# AV2 COMPOSED: a valid certificate exists ONLY for a finalized block; QBFT
|
||||||
|
# finalizes one block at the height (lemma L); therefore no view change yields two
|
||||||
|
# valid certificates over different blocks. We compose L's conclusion (single
|
||||||
|
# finalized value) with the binding: model the finalized block as a single Int and
|
||||||
|
# assert a cert is valid only if bound to it; two valid certs over different blocks
|
||||||
|
# is UNSAT.
|
||||||
|
# =============================================================================
|
||||||
|
s = Solver()
|
||||||
|
blk = Int('finalizedBlock')
|
||||||
|
cert1_blk, cert2_blk = Int('cert1_blk'), Int('cert2_blk')
|
||||||
|
r1, r2 = Int('r1'), Int('r2')
|
||||||
|
s.add(r1 != r2) # view change
|
||||||
|
# validity: a certificate is valid only if its block IS the finalized block
|
||||||
|
valid1 = And(cert1_blk == blk)
|
||||||
|
valid2 = And(cert2_blk == blk)
|
||||||
|
s.add(valid1, valid2)
|
||||||
|
s.add(cert1_blk != cert2_blk) # NEGATION: two valid certs, different blocks
|
||||||
|
check("AV2 composed: with certificate validity requiring the finalized block and "
|
||||||
|
"QBFT finalizing one block per height (lemma L), no view change yields two "
|
||||||
|
"valid certificates over different blocks", s)
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# C THE HONEST BOUNDARY: K=3 (f+1) seals ALONE do NOT give uniqueness. Without
|
||||||
|
# the block binding, two DIFFERENT digests can each collect K distinct valid
|
||||||
|
# registry seals, because a Falcon signer can seal two different anchor payloads
|
||||||
|
# (nothing cryptographic stops equivocation; K=3 < quorum 6 so no intersection).
|
||||||
|
# This is why the binding guard, not the seal count, carries the safety.
|
||||||
|
# =============================================================================
|
||||||
|
s = Solver()
|
||||||
|
# sealX_i / sealY_i: registry validator i produced a valid seal over digest X / Y
|
||||||
|
sealX = [Bool(f'sealX_{i}') for i in range(NKEYS)]
|
||||||
|
sealY = [Bool(f'sealY_{i}') for i in range(NKEYS)]
|
||||||
|
# distinct valid signers for each payload reach the K floor
|
||||||
|
s.add(Sum([If(sealX[i], 1, 0) for i in range(NKEYS)]) >= K)
|
||||||
|
s.add(Sum([If(sealY[i], 1, 0) for i in range(NKEYS)]) >= K)
|
||||||
|
check("NEG-CTRL C: K=3 seals alone do NOT give uniqueness -- two different digests "
|
||||||
|
"each collect 3 distinct valid registry seals (K=f+1 < quorum; uniqueness "
|
||||||
|
"must come from the block binding, not the seal count)", s,
|
||||||
|
expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# ---- C-positive: WITH the binding, the two seal sets are over the SAME digest
|
||||||
|
# (the finalized block's), so there is only one payload to seal -- the seals
|
||||||
|
# are not the thing preventing a second certificate. Sanity: bound digests
|
||||||
|
# equal is consistent (SAT with dX == dY), documenting the design.
|
||||||
|
s = Solver()
|
||||||
|
digest = Function('digest', IntSort(), IntSort())
|
||||||
|
blk = Int('finalizedBlock')
|
||||||
|
dX, dY = Int('dX'), Int('dY')
|
||||||
|
s.add(dX == digest(blk), dY == digest(blk)) # both certs over the finalized block
|
||||||
|
s.add(dX == dY) # so there is a single payload to seal
|
||||||
|
check("C-positive CONFIG: under the binding both certificates seal the SAME "
|
||||||
|
"finalized-block digest (one payload), so the seal sets cannot back two "
|
||||||
|
"different certificates", s, expect_unsat=False, kind="CONFIG")
|
||||||
|
|
||||||
|
# ------------------------------------------------------------------------------
|
||||||
|
print("\n=== SUMMARY (anchor x view-change) ===")
|
||||||
|
allok = True
|
||||||
|
for name, tag, ok, kind in results:
|
||||||
|
print(f" {tag:9} [{kind}] {name}")
|
||||||
|
allok = allok and ok
|
||||||
|
print()
|
||||||
|
if allok:
|
||||||
|
print(" PROVED (N=9, q=6, f=2, K=3): a QBFT round change at an anchor height cannot")
|
||||||
|
print(" produce two valid post-quantum anchor certificates over different blocks.")
|
||||||
|
print(" (L) IBFT locking finalizes ONE block at the height even across a view change;")
|
||||||
|
print(" (AV1) both certificates are bound to that unique finalized block's digest, so")
|
||||||
|
print(" they cannot differ; (AV2) composing validity-requires-finalized-block with the")
|
||||||
|
print(" single finalized value, no view change yields two conflicting certificates.")
|
||||||
|
print(" The negative controls FIRE and locate the safety precisely: dropping the")
|
||||||
|
print(" digest->finalized-block binding (A) or the locking rule (B) each opens two")
|
||||||
|
print(" valid certificates for different blocks, and (C) shows K=3 seals ALONE do not")
|
||||||
|
print(" give uniqueness -- K=f+1 is below the quorum and two digests can each gather 3")
|
||||||
|
print(" distinct valid seals. Uniqueness rests on the block binding, not the seal count.")
|
||||||
|
print(" [VERIFY] keccak256 injectivity (a different block gives a different digest) is")
|
||||||
|
print(" modelled, not re-proved. BOUNDARY: design-level composition of the QBFT lock and")
|
||||||
|
print(" the certificate binding, not Besu/EVM bytecode; classical ECDSA consensus with an")
|
||||||
|
print(" ADDITIVE post-quantum anchor.")
|
||||||
|
else:
|
||||||
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
||||||
|
import sys
|
||||||
|
sys.exit(0 if allok else 1)
|
||||||
250
formal-consensus/partition_safety_smt.py
Normal file
250
formal-consensus/partition_safety_smt.py
Normal file
@ -0,0 +1,250 @@
|
|||||||
|
#!/usr/bin/env python3
|
||||||
|
# -----------------------------------------------------------------------------
|
||||||
|
# partition_safety_smt.py
|
||||||
|
#
|
||||||
|
# MACHINE-CHECKED (z3) NETWORK-PARTITION SAFETY and LIVENESS characterization for
|
||||||
|
# AERE QBFT / IBFT 2.0 (Hyperledger Besu, chain 2800), at the LIVE fleet size
|
||||||
|
# N = 9 (f = 2, quorum ceil(2N/3) = 6) and, for the arithmetic core, UNBOUNDED in
|
||||||
|
# N. This is the parametric companion to the TLA+ partition model
|
||||||
|
# aerenew/formal-tla/QBFTPartition.tla, which TLC checks EXHAUSTIVELY only at
|
||||||
|
# N = 4. TLC cannot search N = 9 exhaustively (state explosion), so the same
|
||||||
|
# partition-safety property is discharged here by proving the negation UNSAT, in
|
||||||
|
# the same style as qbft_safety_smt.py. It formalizes what the test net showed
|
||||||
|
# empirically (runs F40 / F52: a lagging node, 1 of 3 down): a side without a
|
||||||
|
# quorum cannot finalize, the majority side can, and no two sides finalize
|
||||||
|
# conflicting values.
|
||||||
|
#
|
||||||
|
# A network partition splits the N validators into two groups that cannot
|
||||||
|
# exchange messages. While partitioned, any commit quorum for a value must be
|
||||||
|
# assembled ENTIRELY within one group's visible senders (cross-group messages are
|
||||||
|
# not delivered). We prove:
|
||||||
|
# PA SAFETY: two disjoint groups can never both reach a commit quorum for
|
||||||
|
# DIFFERENT values -> no partition forks the chain. (unbounded N + N=9)
|
||||||
|
# PL LIVENESS LOSS: a partition whose every group is smaller than the quorum
|
||||||
|
# finalizes nothing (progress is lost), while a partition with a group at or
|
||||||
|
# above the quorum keeps progressing (the majority side). (N=9 enumerated)
|
||||||
|
# PH HEAL: once the partition heals (all N visible) the honest set alone
|
||||||
|
# (N - f = 7 >= 6) forms a quorum, so progress returns without a fork.
|
||||||
|
#
|
||||||
|
# NON-VACUITY (rigor): every proof is paired with a NEGATIVE CONTROL that lowers
|
||||||
|
# the quorum to the majority ceil(N/2) (or drops a size guard) and the checker
|
||||||
|
# MUST return SAT (a balanced partition then forks, or a sub-quorum side
|
||||||
|
# "finalizes"). If a control did not fire, the proof would be vacuous.
|
||||||
|
#
|
||||||
|
# HONEST BOUNDARY: this checks the DESIGN combinatorics of partition-era quorum
|
||||||
|
# formation, not the Besu Java bytecode and not the live chain. It is a
|
||||||
|
# SINGLE-height agreement argument (the partition is the fault under study);
|
||||||
|
# cross-round locking / view change is covered in qbft_safety_smt.py L3,
|
||||||
|
# qbft_locking_smt.py and anchor_viewchange_smt.py. It is orthogonal to the block-
|
||||||
|
# seal signature scheme: chain 2800 commits with classical secp256k1 ECDSA, and
|
||||||
|
# NOTHING here implies post-quantum consensus.
|
||||||
|
# -----------------------------------------------------------------------------
|
||||||
|
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), Besu fastDivCeiling(2N,3)
|
||||||
|
def faultbound(n): return (n - 1) // 3 # floor((N-1)/3)
|
||||||
|
def ceil_half(n): return (n + 1) // 2 # ceil(N/2): the (too-low) majority quorum
|
||||||
|
|
||||||
|
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 QBFT -- NETWORK-PARTITION SAFETY / LIVENESS (N=9, f=2, quorum=6; core unbounded)\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, 7, 9)) + "\n")
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# PA0 ARITHMETIC CORE (UNBOUNDED in N): two disjoint groups that partition all N
|
||||||
|
# validators cannot both hold a quorum. s1 + s2 = N, both >= q=ceil(2N/3) is
|
||||||
|
# impossible for EVERY N, because 2q > N. Negation UNSAT.
|
||||||
|
# =============================================================================
|
||||||
|
s = Solver()
|
||||||
|
N, q, s1, s2 = Int('N'), Int('q'), Int('s1'), Int('s2')
|
||||||
|
s.add(N >= 1)
|
||||||
|
s.add(3 * q >= 2 * N, 3 * q <= 2 * N + 2) # q == ceil(2N/3)
|
||||||
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N) # a partition of all N validators
|
||||||
|
s.add(s1 >= q, s2 >= q) # NEGATION: BOTH sides hold a quorum
|
||||||
|
check("PA0 partition arithmetic (ALL N): two disjoint groups covering N cannot "
|
||||||
|
"both reach the ceil(2N/3) quorum (2q > N)", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL PA0: majority quorum ceil(N/2) -> a balanced split CAN give both
|
||||||
|
# sides a "quorum" (this is exactly the split-brain a too-low quorum allows).
|
||||||
|
s = Solver()
|
||||||
|
N, q, s1, s2 = Int('N'), Int('q'), Int('s1'), Int('s2')
|
||||||
|
s.add(N >= 2)
|
||||||
|
s.add(2 * q >= N, 2 * q <= N + 1) # q == ceil(N/2): the too-low quorum
|
||||||
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N)
|
||||||
|
s.add(s1 >= q, s2 >= q) # both sides reach the lowered quorum
|
||||||
|
check("NEG-CTRL PA0 majority quorum ceil(N/2): a balanced partition gives BOTH "
|
||||||
|
"sides a quorum (split-brain is possible)", s, expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# PA PARTITION SAFETY, per-validator model at N = 9 (and 4,7). Each validator i
|
||||||
|
# sits in group g in {0,1} (its side of the partition) and is honest or Byzantine.
|
||||||
|
# During the partition a value is FINALIZED on side g iff >= q side-g validators
|
||||||
|
# COMMIT it (cross-side messages invisible). Honest validators commit at most one
|
||||||
|
# value; <= f are Byzantine and may equivocate. SAFETY: two DIFFERENT values
|
||||||
|
# cannot both be finalized (on the same or on opposite sides). Negation UNSAT.
|
||||||
|
# =============================================================================
|
||||||
|
def partition_agreement(N, qv, fv, lowered=False):
|
||||||
|
s = Solver()
|
||||||
|
grp = [Int(f'grp_{i}') for i in range(N)] # 0 or 1: which side of the split
|
||||||
|
honest = [Bool(f'honest_{i}') for i in range(N)]
|
||||||
|
cA = [Bool(f'cA_{i}') for i in range(N)] # commits value A
|
||||||
|
cB = [Bool(f'cB_{i}') for i in range(N)] # commits value B
|
||||||
|
for i in range(N):
|
||||||
|
s.add(Or(grp[i] == 0, grp[i] == 1))
|
||||||
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv) # <= f Byzantine
|
||||||
|
for i in range(N):
|
||||||
|
s.add(Implies(honest[i], Not(And(cA[i], cB[i])))) # honest: one value
|
||||||
|
# finalized-on-side counts: only same-side committers are visible
|
||||||
|
def side_count(mat, g, v):
|
||||||
|
return Sum([If(And(grp[i] == g, mat[i]), 1, 0) for i in range(N)])
|
||||||
|
finA = Or(side_count(cA, 0, True) >= qv, side_count(cA, 1, True) >= qv)
|
||||||
|
finB = Or(side_count(cB, 0, True) >= qv, side_count(cB, 1, True) >= qv)
|
||||||
|
s.add(finA, finB) # NEGATION of safety: A and B both finalized somewhere
|
||||||
|
return s
|
||||||
|
|
||||||
|
for N in (4, 7, 9):
|
||||||
|
s = partition_agreement(N, quorum(N), faultbound(N))
|
||||||
|
check(f"PA partition safety N={N} (q={quorum(N)},f={faultbound(N)}): during a "
|
||||||
|
f"partition two different values cannot both be finalized", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL PA: lower the quorum to ceil(N/2) at N=9 -> a balanced split forks.
|
||||||
|
s = partition_agreement(9, ceil_half(9), faultbound(9))
|
||||||
|
check(f"NEG-CTRL PA majority quorum ceil(N/2)={ceil_half(9)} at N=9: a partition "
|
||||||
|
f"finalizes two different values (split-brain fork)", s,
|
||||||
|
expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# PL LIVENESS LOSS vs PROGRESS at N = 9. A value is finalizable during the
|
||||||
|
# partition iff SOME group has >= q members. If every group is below the quorum,
|
||||||
|
# nothing finalizes (liveness lost); if a group is at/above it, the majority side
|
||||||
|
# progresses.
|
||||||
|
# =============================================================================
|
||||||
|
# PL1: both groups below quorum => no finalization possible. Model: side sizes
|
||||||
|
# s1,s2 with s1<q, s2<q, s1+s2=N; commit counts bounded by side size; claim
|
||||||
|
# "max side commit >= q" is UNSAT.
|
||||||
|
def no_progress_when_starved(N, qv):
|
||||||
|
s = Solver()
|
||||||
|
s1, s2 = Int('s1'), Int('s2')
|
||||||
|
c1, c2 = Int('c1'), Int('c2') # commits gathered on each side (<= side size)
|
||||||
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == N)
|
||||||
|
s.add(s1 < qv, s2 < qv) # BOTH groups starved (below quorum)
|
||||||
|
s.add(c1 >= 0, c1 <= s1, c2 >= 0, c2 <= s2)
|
||||||
|
s.add(Or(c1 >= qv, c2 >= qv)) # NEGATION: some side still finalizes
|
||||||
|
return s
|
||||||
|
s = no_progress_when_starved(9, quorum(9))
|
||||||
|
check("PL1 liveness loss N=9: if BOTH partition groups are below quorum 6, no side "
|
||||||
|
"can finalize (a starved partition makes no progress)", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL PL1: a partition with a majority group (6-3) DOES let that side
|
||||||
|
# finalize -> progress is possible, so PL1's UNSAT is specific to starvation.
|
||||||
|
s = Solver()
|
||||||
|
s1, s2, c1 = Int('s1'), Int('s2'), Int('c1')
|
||||||
|
s.add(s1 == 6, s2 == 3, s1 + s2 == 9) # a 6-3 partition: one side has the quorum
|
||||||
|
s.add(c1 >= 0, c1 <= s1, c1 >= quorum(9))
|
||||||
|
check("NEG-CTRL PL1: a 6-3 partition at N=9 lets the majority side (6 >= quorum) "
|
||||||
|
"finalize (progress on the side that keeps a quorum)", s,
|
||||||
|
expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# PL2: enumerate every split of N=9 and classify. A split (s1, s2) keeps liveness
|
||||||
|
# iff max(s1,s2) >= 6. Prove the classification is exactly right: there is NO
|
||||||
|
# split where both sides are < 6 yet some side reaches 6 (already PL1), and NO
|
||||||
|
# split with a side >= 6 that cannot finalize. State as: for all splits,
|
||||||
|
# (max side >= q) <-> (progress possible). Negation UNSAT.
|
||||||
|
s = Solver()
|
||||||
|
s1 = Int('s1'); s2 = Int('s2'); q9 = quorum(9)
|
||||||
|
s.add(s1 >= 0, s2 >= 0, s1 + s2 == 9)
|
||||||
|
maxside = If(s1 >= s2, s1, s2)
|
||||||
|
progress = maxside >= q9
|
||||||
|
# NEGATION: a split where "some side can finalize" disagrees with "max side >= q"
|
||||||
|
s.add(progress != (maxside >= q9))
|
||||||
|
check("PL2 split classification N=9: a partition makes progress IFF its larger "
|
||||||
|
"group is at least the quorum 6 (exhaustive over all 9 splits)", s)
|
||||||
|
|
||||||
|
# =============================================================================
|
||||||
|
# PH HEAL restores progress without a fork. Once healed, all N validators are
|
||||||
|
# mutually visible, so the honest set alone (N - f) forms a quorum when N - f >= q.
|
||||||
|
# =============================================================================
|
||||||
|
# PH1: N - f >= q at N=9 (7 >= 6): the honest validators alone can commit after
|
||||||
|
# heal. Prove N - f >= q holds; here as the concrete fact for N=9.
|
||||||
|
s = Solver()
|
||||||
|
nf, qv = Int('nf'), Int('qv')
|
||||||
|
s.add(nf == 9 - faultbound(9), qv == quorum(9))
|
||||||
|
s.add(nf < qv) # NEGATION: honest set too small to commit
|
||||||
|
check("PH1 heal progress N=9: the honest set alone (N-f = 7) meets the quorum 6, so "
|
||||||
|
"the healed network can finalize without any Byzantine help", s)
|
||||||
|
|
||||||
|
# PH2: after heal, a single value committed by >= q validators is finalized and no
|
||||||
|
# SECOND value can be (same one-round agreement, now over ALL N). Negation UNSAT.
|
||||||
|
s = Solver()
|
||||||
|
N = 9; qv = quorum(9); fv = faultbound(9)
|
||||||
|
honest = [Bool(f'h_{i}') for i in range(N)]
|
||||||
|
cA = [Bool(f'a_{i}') for i in range(N)]
|
||||||
|
cB = [Bool(f'b_{i}') for i in range(N)]
|
||||||
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv)
|
||||||
|
for i in range(N):
|
||||||
|
s.add(Implies(honest[i], Not(And(cA[i], cB[i]))))
|
||||||
|
s.add(Sum([If(cA[i], 1, 0) for i in range(N)]) >= qv) # A finalized post-heal
|
||||||
|
s.add(Sum([If(cB[i], 1, 0) for i in range(N)]) >= qv) # NEGATION: B too
|
||||||
|
check("PH2 heal safety N=9: after the partition heals, two different values still "
|
||||||
|
"cannot both reach the quorum (no fork on recovery)", s)
|
||||||
|
|
||||||
|
# ---- NEG-CTRL PH2: lower the quorum -> post-heal two values can both 'commit'.
|
||||||
|
s = Solver()
|
||||||
|
N = 9; qv = ceil_half(9); fv = faultbound(9)
|
||||||
|
honest = [Bool(f'h_{i}') for i in range(N)]
|
||||||
|
cA = [Bool(f'a_{i}') for i in range(N)]
|
||||||
|
cB = [Bool(f'b_{i}') for i in range(N)]
|
||||||
|
s.add(Sum([If(Not(honest[i]), 1, 0) for i in range(N)]) <= fv)
|
||||||
|
for i in range(N):
|
||||||
|
s.add(Implies(honest[i], Not(And(cA[i], cB[i]))))
|
||||||
|
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)
|
||||||
|
check(f"NEG-CTRL PH2 majority quorum ceil(N/2)={ceil_half(9)} at N=9: post-heal two "
|
||||||
|
f"values both reach the lowered quorum (fork) -- the ceil(2N/3) quorum is "
|
||||||
|
f"load-bearing on recovery too", s, expect_unsat=False, kind="NEG-CTRL")
|
||||||
|
|
||||||
|
# ------------------------------------------------------------------------------
|
||||||
|
print("\n=== SUMMARY (NETWORK-PARTITION SAFETY / LIVENESS) ===")
|
||||||
|
allok = True
|
||||||
|
for name, tag, ok, kind in results:
|
||||||
|
print(f" {tag:9} [{kind}] {name}")
|
||||||
|
allok = allok and ok
|
||||||
|
print()
|
||||||
|
if allok:
|
||||||
|
print(" PROVED at N=9 (f=2, quorum=6), with the arithmetic core unbounded in N:")
|
||||||
|
print(" (PA) a network partition cannot fork the chain -- two disjoint groups can")
|
||||||
|
print(" never both reach a ceil(2N/3) commit quorum, so at most one side finalizes,")
|
||||||
|
print(" and it finalizes a single value. (PL) liveness is LOST exactly when every")
|
||||||
|
print(" group is below the quorum (a balanced 5-4 or worse split at N=9), and a")
|
||||||
|
print(" partition keeps progressing iff its larger group is at least 6 (the majority")
|
||||||
|
print(" side); the split classification is exhaustive over all 9 splits. (PH) once")
|
||||||
|
print(" the partition heals, the honest set alone (7 >= 6) forms a quorum, so progress")
|
||||||
|
print(" returns with no fork. All negative controls FIRE: lowering the quorum to the")
|
||||||
|
print(" majority ceil(N/2) forks a balanced partition and forks on recovery, and a 6-3")
|
||||||
|
print(" split shows the starvation result PL1 is not vacuous.")
|
||||||
|
print(" This is the parametric N=9 companion to formal-tla/QBFTPartition.tla, which")
|
||||||
|
print(" TLC checks exhaustively at N=4; cross-method + cross-scale agreement is the")
|
||||||
|
print(" point. BOUNDARY: design combinatorics of partition-era quorum formation, not")
|
||||||
|
print(" Besu bytecode; single-height agreement; classical ECDSA (not post-quantum).")
|
||||||
|
else:
|
||||||
|
print(" NOT fully established (see FAILED / unexpected result above).")
|
||||||
|
import sys
|
||||||
|
sys.exit(0 if allok else 1)
|
||||||
@ -20,7 +20,7 @@
|
|||||||
# (The quint/Apalache spec FalconQuorum.qnt is an OPTIONAL secondary cross-check;
|
# (The quint/Apalache spec FalconQuorum.qnt is an OPTIONAL secondary cross-check;
|
||||||
# see CONSENSUS-VERIFICATION-2026-07-12.md for the `quint run` commands.)
|
# see CONSENSUS-VERIFICATION-2026-07-12.md for the `quint run` commands.)
|
||||||
# -----------------------------------------------------------------------------
|
# -----------------------------------------------------------------------------
|
||||||
import subprocess, sys, os, re
|
import subprocess, sys, os, re, time
|
||||||
|
|
||||||
# --- QBFT / Falcon consensus models (unchanged) ---
|
# --- QBFT / Falcon consensus models (unchanged) ---
|
||||||
CONSENSUS_MODELS = [
|
CONSENSUS_MODELS = [
|
||||||
@ -33,6 +33,11 @@ CONSENSUS_MODELS = [
|
|||||||
("QBFT explicit-Prepare counting (2026-07-14 2nd-client bug+fix)", "qbft_prepare_counting_smt.py"),
|
("QBFT explicit-Prepare counting (2026-07-14 2nd-client bug+fix)", "qbft_prepare_counting_smt.py"),
|
||||||
("QBFT digest-keyed vote tally (2026-07-14 Finding-A shipped fix)", "qbft_digest_keyed_smt.py"),
|
("QBFT digest-keyed vote tally (2026-07-14 Finding-A shipped fix)", "qbft_digest_keyed_smt.py"),
|
||||||
("QBFT IBFT 2.0 locking, engine-role model (2026-07-14 Findings D/E)", "qbft_locking_smt.py"),
|
("QBFT IBFT 2.0 locking, engine-role model (2026-07-14 Findings D/E)", "qbft_locking_smt.py"),
|
||||||
|
("QBFT NETWORK-PARTITION safety/liveness (N=9 parametric: split-brain, starvation, heal)", "partition_safety_smt.py"),
|
||||||
|
("Anchor x VIEW-CHANGE (no round change yields two valid PQ certificates, N=9)", "anchor_viewchange_smt.py"),
|
||||||
|
("PqAnchor CEILING monotonicity (minSealsCeiling only lowers K; K_eff <= maxSeals)", "pqanchor_ceiling_monotonicity_smt.py"),
|
||||||
|
("PQ anchor REGISTRY index binding (loader and seal rule read ONE mapping)", "registry_index_binding_smt.py"),
|
||||||
|
("PQ anchor REGISTRY rotation coverage (every anchor height has exactly one registry)", "registry_rotation_coverage_smt.py"),
|
||||||
]
|
]
|
||||||
|
|
||||||
# --- CONTRACT SMT models: fund-flow + registry + PQC-verifier invariants (wired in
|
# --- CONTRACT SMT models: fund-flow + registry + PQC-verifier invariants (wired in
|
||||||
@ -97,12 +102,15 @@ here = os.path.dirname(os.path.abspath(__file__))
|
|||||||
overall = True
|
overall = True
|
||||||
summary = []
|
summary = []
|
||||||
totals = {"PROVED": 0, "CEX-FOUND": 0, "FAILED": 0}
|
totals = {"PROVED": 0, "CEX-FOUND": 0, "FAILED": 0}
|
||||||
|
suite_start = time.time()
|
||||||
for label, fname in MODELS:
|
for label, fname in MODELS:
|
||||||
path = os.path.join(here, fname)
|
path = os.path.join(here, fname)
|
||||||
print("=" * 78)
|
print("=" * 78)
|
||||||
print(f"### {label} [{fname}]")
|
print(f"### {label} [{fname}]")
|
||||||
print("=" * 78)
|
print("=" * 78)
|
||||||
|
t0 = time.time()
|
||||||
r = subprocess.run([sys.executable, path], capture_output=True, text=True)
|
r = subprocess.run([sys.executable, path], capture_output=True, text=True)
|
||||||
|
dt = time.time() - t0
|
||||||
sys.stdout.write(r.stdout)
|
sys.stdout.write(r.stdout)
|
||||||
if r.stderr:
|
if r.stderr:
|
||||||
sys.stderr.write(r.stderr)
|
sys.stderr.write(r.stderr)
|
||||||
@ -112,20 +120,25 @@ for label, fname in MODELS:
|
|||||||
totals[m.group(1)] += 1
|
totals[m.group(1)] += 1
|
||||||
ok = (r.returncode == 0)
|
ok = (r.returncode == 0)
|
||||||
overall = overall and ok
|
overall = overall and ok
|
||||||
summary.append((label, fname, ok))
|
summary.append((label, fname, ok, dt))
|
||||||
|
print(f" [{dt:6.2f}s] {'PASS' if ok else 'FAIL'} {fname}")
|
||||||
print()
|
print()
|
||||||
|
suite_elapsed = time.time() - suite_start
|
||||||
|
|
||||||
print("#" * 78)
|
print("#" * 78)
|
||||||
print("### AERE FORMAL-VERIFICATION SUITE -- OVERALL (consensus + contract + application models)")
|
print("### AERE FORMAL-VERIFICATION SUITE -- OVERALL (consensus + contract + application models)")
|
||||||
print("#" * 78)
|
print("#" * 78)
|
||||||
for label, fname, ok in summary:
|
for label, fname, ok, dt in summary:
|
||||||
print(f" {'PASS' if ok else 'FAIL'} {label:66} ({fname})")
|
print(f" {'PASS' if ok else 'FAIL'} [{dt:6.2f}s] {label:66} ({fname})")
|
||||||
print()
|
print()
|
||||||
print(f" models run: {len(MODELS)} passed: {sum(1 for _,_,ok in summary if ok)}"
|
print(f" models run: {len(MODELS)} passed: {sum(1 for _,_,ok,_ in summary if ok)}"
|
||||||
f" ({len(CONSENSUS_MODELS)} consensus + {len(CONTRACT_MODELS)} contract"
|
f" ({len(CONSENSUS_MODELS)} consensus + {len(CONTRACT_MODELS)} contract"
|
||||||
f" + {len(APPLICATION_MODELS)} application)")
|
f" + {len(APPLICATION_MODELS)} application)")
|
||||||
print(f" verdict lines: {totals['PROVED']} PROVED {totals['CEX-FOUND']} CEX-FOUND "
|
print(f" verdict lines: {totals['PROVED']} PROVED {totals['CEX-FOUND']} CEX-FOUND "
|
||||||
f"{totals['FAILED']} FAILED")
|
f"{totals['FAILED']} FAILED")
|
||||||
|
print(f" wall time: {suite_elapsed:6.2f}s total"
|
||||||
|
+ (f" (slowest: {max(summary, key=lambda x: x[3])[1]} at "
|
||||||
|
f"{max(s[3] for s in summary):.2f}s)" if summary else ""))
|
||||||
print(f" coverage: {len(_wired & _present)} of {len(_present)} *_smt.py files in this"
|
print(f" coverage: {len(_wired & _present)} of {len(_present)} *_smt.py files in this"
|
||||||
f" directory are wired into this run"
|
f" directory are wired into this run"
|
||||||
+ (f" ({len(_INTENTIONALLY_UNWIRED)} intentionally unwired)"
|
+ (f" ({len(_INTENTIONALLY_UNWIRED)} intentionally unwired)"
|
||||||
|
|||||||
Loading…
Reference in New Issue
Block a user