aere-network/aere-research
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
316ba7171f
aere-research/formal-consensus/RULEAZA-TOT.md

8.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-10-07 (Windows, python 3.14.4 / z3 4.16.0; timpii variaza cu masina):

models run: 37   passed: 37   (16 consensus + 11 contract + 10 application)
verdict lines: 301 PROVED   159 CEX-FOUND   0 FAILED
wall time:  ~37s total   (cel mai lent: qbft_safety_smt.py ~20s)
coverage: 37 of 37 *_smt.py files wired
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)

Istoria cifrelor, datata: 2026-08-24, 35 de modele (14 consens), 282 PROVED / 149 CEX-FOUND, ~39 s; 2026-09-02, + pq_message_enforcement_smt.py (36 of 36); 2026-10-07, + anchor_rewrite_bound_roundfree_smt.py (37 of 37; 13 dovezi, 2 leme, 4 martori, 1 definitie, 8 controale negative; limita de rescriere 32 / 33 sub modelul fara runda, ca functie de K_eff si de cheile PQ tinute; vezi research/rewrite-bound-round-free-seal-2026-10-07.md si anchor_rewrite_bound_roundfree_smt.RESULT.txt).

Cele 16 modele de consens (14 pe 24 august, + 1 pe 2 septembrie, + 1 pe 7 octombrie):

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 -
anchor_rewrite_bound_roundfree_smt.py (2026-10-07) limita de rescriere sub adversarul cu toate cheile clasice: 32 de blocuri (ancora + 31), 33 sub exceptia din erata AIP-22 (fratele nedecis, bunicul comun); marginita exact cand cheile PQ tinute j < K_eff (K_eff = 7 pe validator, 1 pe urmaritorul publicat cu plafon); 128 / 129 in fereastra datata cu interval 128; punctul de referinta fixeaza prefixul (lantul de hash-uri desfasurat 1280 de inaltimi); --plant-bounds = controlul controlului 10, orice K_eff >= 1

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)
AERE_REPO=/calea/catre/clona/depozitului     # radacina clonei tale; dosarul formal-tla/ sta direct sub ea
mkdir -p /root/ftla
cp -f "$AERE_REPO"/formal-tla/*.tla /root/ftla/
cp -f "$AERE_REPO"/formal-tla/*.cfg /root/ftla/
cp -f "$AERE_REPO"/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.