a2f4d835a3
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.
143 lines
7.5 KiB
Markdown
143 lines
7.5 KiB
Markdown
# 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.
|