Aere Network a2f4d835a3 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.

2026-08-24 20:02:07 +03:00

7.5 KiB

Raw Blame History

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:

# 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.

7.5 KiB Raw Blame History