diff --git a/formal-consensus/RULEAZA-TOT.md b/formal-consensus/RULEAZA-TOT.md new file mode 100644 index 0000000..4008367 --- /dev/null +++ b/formal-consensus/RULEAZA-TOT.md @@ -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. diff --git a/formal-consensus/anchor_viewchange_smt.py b/formal-consensus/anchor_viewchange_smt.py new file mode 100644 index 0000000..0e1aa2f --- /dev/null +++ b/formal-consensus/anchor_viewchange_smt.py @@ -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) diff --git a/formal-consensus/partition_safety_smt.py b/formal-consensus/partition_safety_smt.py new file mode 100644 index 0000000..f515c68 --- /dev/null +++ b/formal-consensus/partition_safety_smt.py @@ -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" 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) diff --git a/formal-consensus/run_consensus_verification.py b/formal-consensus/run_consensus_verification.py index b177dcb..190dc40 100644 --- a/formal-consensus/run_consensus_verification.py +++ b/formal-consensus/run_consensus_verification.py @@ -20,7 +20,7 @@ # (The quint/Apalache spec FalconQuorum.qnt is an OPTIONAL secondary cross-check; # 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) --- 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 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 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 @@ -97,12 +102,15 @@ here = os.path.dirname(os.path.abspath(__file__)) overall = True summary = [] totals = {"PROVED": 0, "CEX-FOUND": 0, "FAILED": 0} +suite_start = time.time() for label, fname in MODELS: path = os.path.join(here, fname) print("=" * 78) print(f"### {label} [{fname}]") print("=" * 78) + t0 = time.time() r = subprocess.run([sys.executable, path], capture_output=True, text=True) + dt = time.time() - t0 sys.stdout.write(r.stdout) if r.stderr: sys.stderr.write(r.stderr) @@ -112,20 +120,25 @@ for label, fname in MODELS: totals[m.group(1)] += 1 ok = (r.returncode == 0) 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() +suite_elapsed = time.time() - suite_start print("#" * 78) print("### AERE FORMAL-VERIFICATION SUITE -- OVERALL (consensus + contract + application models)") print("#" * 78) -for label, fname, ok in summary: - print(f" {'PASS' if ok else 'FAIL'} {label:66} ({fname})") +for label, fname, ok, dt in summary: + print(f" {'PASS' if ok else 'FAIL'} [{dt:6.2f}s] {label:66} ({fname})") 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(APPLICATION_MODELS)} application)") print(f" verdict lines: {totals['PROVED']} PROVED {totals['CEX-FOUND']} CEX-FOUND " 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" f" directory are wired into this run" + (f" ({len(_INTENTIONALLY_UNWIRED)} intentionally unwired)"