diff --git a/README.md b/README.md index e2bfc33..5a24a61 100644 --- a/README.md +++ b/README.md @@ -55,8 +55,8 @@ Two more limits, both of which cut against claims made in this repository: ## Layout -- `formal-consensus/` Z3 / SMT models of consensus and contract safety properties (30 Python - models plus a Quint spec `FalconQuorum.qnt`), driven by `run_consensus_verification.py`. These +- `formal-consensus/` Z3 / SMT models of consensus and contract safety properties (37 Python + models, counted on 2026-10-27, plus a Quint spec `FalconQuorum.qnt`), driven by `run_consensus_verification.py`. These cover QBFT safety and liveness, the money-contract invariants, and a PROPOSED hybrid dual-quorum activation that is modelled research and is NOT running on chain 2800, and the invariants. `CONSENSUS-VERIFICATION-2026-07-12.md` documents the results. @@ -84,8 +84,9 @@ python run_consensus_verification.py ``` The STARK references are cross-checked against their ground-truth vectors; see each -`spec-*.md` and the `test_*.py` files. Full commands and expected outputs are in the `aere-docs` -repository (`REPRODUCE.md`). +`spec-*.md` and the `test_*.py` files. Full commands and expected outputs, dated, are in the `aere-docs` +repository (`REPRODUCE.md`; its section 3b gives the result of the command above as measured on 2026-10-27, and +the older runs it records use the paths of the development tree). ## What is deliberately not here diff --git a/formal-consensus/RULEAZA-TOT.md b/formal-consensus/RULEAZA-TOT.md index 8084324..ed48614 100644 --- a/formal-consensus/RULEAZA-TOT.md +++ b/formal-consensus/RULEAZA-TOT.md @@ -1,83 +1,85 @@ -# RULEAZA-TOT: verificarea formala a consensului AERE, un capat la altul +# RULEAZA-TOT: the formal verification of AERE consensus, end to end -Rularea completa a tot ce se poate verifica automat pe consensul AERE (QBFT / IBFT 2.0, -chain 2800), cu doua metode independente: +*Translated into English and dated on 2026-10-27. Until that date this document was in Romanian and stated, without a date, +facts that were true only of the chain of August 2026 (a set of nine validators, an anchor minimum of three); the +corrections are marked below, and the results it records keep the date they were measured on.* -- **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. +A complete run of everything that can be checked automatically about AERE consensus (QBFT / IBFT 2.0, chain 2800), with two +independent methods: -Regula peste tot: **niciun model nu se raporteaza verde daca nu poate iesi ROSU.** Fiecare -proprietate are un control negativ rulat. +- **SMT (z3)**, parametric, in this directory (`formal-consensus/*_smt.py`): each property is proved by showing that its + negation is UNSAT, plus a negative control that plants the violation and must come back SAT. The models scale to N=9, + the validator set of 2026-08-24, when the table below was written; the set has had ten validators since 2026-09-11, and + the models state the N each one is run at. +- **TLA+ / TLC**, exhaustive, in `formal-tla/` of the development tree (not in this repository): it explores the state + space at a small scale (N=4), where the combinatorics is enough. + +The rule everywhere: **no model is reported green unless it can come out RED.** Every property has a negative control +that is run. --- -## 1. Suita SMT (z3) - o singura comanda +## 1. The SMT suite (z3): one command ``` -cd aerenew/publish-bundle/aere-research/formal-consensus +cd 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. +It runs ALL the `*_smt.py` models in this directory (the completeness guard refuses a green result if a model that is +present is not wired). It prints PASS / FAIL per model, the time of each, and the tally of verdict lines. -**Masurat 2026-10-07** (Windows, python 3.14.4 / z3 4.16.0; timpii variaza cu masina): +**Measured 2026-10-07** (Windows, Python 3.14.4 / z3 4.16.0; the times vary with the machine): ``` 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) +wall time: ~37s total (slowest: 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; +The history of the figures, dated: 2026-08-24, 35 models (14 consensus), 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`). +(37 of 37; 13 proofs, 2 lemmas, 4 witnesses, 1 definition, 8 negative controls; the rewrite bound is 32 / 33 under the +round-free model, as a function of K_eff and of the post-quantum keys held; see +`research/rewrite-bound-round-free-seal-2026-10-07.md` and `anchor_rewrite_bound_roundfree_smt.RESULT.txt`). -Cele 16 modele de consens (14 pe 24 august, + 1 pe 2 septembrie, + 1 pe 7 octombrie): +The 16 consensus models (14 on 24 August, + 1 on 2 September, + 1 on 7 October): -| model | ce dovedeste | N | +| model | what it proves | 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 | +| `qbft_safety_smt.py` | agreement (quorum intersection unbounded; one-round + cross-round locking) | 4,5,7,10,13,16 | +| `qbft_liveness_smt.py` | progress after GST (f+1 rounds reach an honest proposer) | 4,5,7 | +| `qbft_locking_smt.py` | IBFT 2.0 locking on the engine roles (view change / round change) | 4,5,7 | +| `qbft_prepare_counting_smt.py`, `qbft_digest_keyed_smt.py` | the counting of votes (bug and fix of 2026-07-14) | small | +| `falcon_blocking_smt.py`, `anchor_blocking_quorum_smt.py` | the anchor seal threshold of 2026-08-15 (K=3 of 9; the minimum is 7 of 10 since block 20,715,632) | 9 | +| `qbft_pqc_activation_smt.py` | the log-only -> blocking transition | - | +| **`partition_safety_smt.py`** (new on 2026-08-24) | **network partitions: split brain, starvation, healing** | **9, parametric** | +| **`anchor_viewchange_smt.py`** (new on 2026-08-24) | **a round change at an anchor does not give two valid certificates, in the model, under its finalized-block guard (the code has no such guard: note added 2026-10-01)** | **9** | +| `pqanchor_ceiling_monotonicity_smt.py` | the emergency ceiling only lowers K | - | +| `registry_index_binding_smt.py`, `registry_rotation_coverage_smt.py` | the key registry by height (the registries of 2026-08-15) | - | +| **`anchor_rewrite_bound_roundfree_smt.py`** (2026-10-07) | **the rewrite bound under the adversary holding every classical key: 32 blocks (the anchor + 31), 33 under the exception of the AIP-22 erratum (the undecided sibling, the common grandparent); bounded exactly when the post-quantum keys held j < K_eff (K_eff = 7 on a validator, 1 on the published follower with its ceiling); 128 / 129 in the dated window with interval 128; the reference point pins the prefix (the hash chain unrolled over 1280 heights); `--plant-bounds` is the control of the control** | 10, any 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. +> Note: the three registry / ceiling models were in the directory from 15 to 19 August but were NOT wired into the runner +> (the completeness guard made it exit with code 2). They were wired on 24 August together with the two new models. --- -## 2. TLA+ / TLC exhaustiv - partitiile de retea (NOU, 24 august) +## 2. TLA+ / TLC, exhaustive: network partitions (new on 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. +The model `formal-tla/QBFTPartition.tla` (development tree) makes the partition an explicitly modelled FAULT (a predicate +on the delivery of messages between groups) and checks it exhaustively at N=4. Six configurations, each with its positive +/ negative pair. -### Rularea (WSL, mult mai rapid decat pe Windows) +### The run (much faster under Linux, or WSL on Windows, than natively on 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: +Write a script, copy it, run it without inline quotes. Every run uses `-deadlock`, because the protocol TERMINATES +normally (everyone has decided) and termination is not a defect: ```bash -# 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 +# copy the directory outside any mounted Windows drive (a faster run) +AERE_REPO=/path/to/the/clone # the root of your clone; the formal-tla/ directory sits directly under it mkdir -p /root/ftla cp -f "$AERE_REPO"/formal-tla/*.tla /root/ftla/ cp -f "$AERE_REPO"/formal-tla/*.cfg /root/ftla/ @@ -89,62 +91,61 @@ for CFG in MCpart_safety MCpart_safety_witness MCpart_safety_negctrl \ done ``` -Lanseaza din PowerShell: -`MSYS_NO_PATHCONV=1 wsl.exe -d Ubuntu-24.04 -- bash /mnt/c/.../script.sh` +### Results measured 2026-08-24 (WSL, OpenJDK 21, exhaustive, 0 states left in the queue) -### Rezultate masurate 2026-08-24 (WSL, OpenJDK 21, exhaustiv, 0 stari ramase in coada) - -| config | ce verifica | asteptat | rezultat | timp | +| config | what it checks | expected | result | time | |---|---|---|---|---| -| `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 | +| `MCpart_safety` | 3-1, quorum 3, heal: SAFETY holds | no error | **No error** (1866 states) | ~3s | +| `MCpart_safety_witness` | the same, invariant `NoCommit` | VIOLATION (a commit is reached) | **NoCommit violated** -> `committed={a}` | ~2s | +| `MCpart_safety_negctrl` | 2-2, quorum LOWERED to 2 | VIOLATION (fork) | **NoFork violated** -> `committed={a,b}` (v1->a, v3->b) | ~4s | +| `MCpart_noprogress` | 2-2, quorum 3, NO healing, invariant `NoCommit` | no error | **No error** (81 states; nothing finalizes) | ~2s | +| `MCpart_liveness` | 2-2, quorum 3, healing, `EventualCommit` | no error | **No error** (liveness returns after the heal) | ~3s | +| `MCpart_liveness_negctrl` | 2-2, quorum 3, NO healing, `EventualCommit` | VIOLATION | **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). +The three pairs answer exactly the questions asked: +- **SAFETY holds on both sides**: `MCpart_safety` is green, and non-vacuous through `witness` (the majority side does + finalize). The negative control `safety_negctrl` shows that what stops the fork is the ceil(2N/3) quorum: lowered to 2, + the two sides finalize `a` and `b`. +- **LIVENESS is lost in the group without a quorum**: `MCpart_noprogress` (nothing finalizes in an unhealed 2-2 + partition). +- **LIVENESS returns on healing**: `MCpart_liveness` is green; the negative control `liveness_negctrl` shows that without + the healing step `EventualCommit` FAILS (the heal is the cause). --- -## 3. TLA+ / TLC - modelul QBFT complet (agreement + view-change + echivocatie) +## 3. TLA+ / TLC: the complete QBFT model (agreement + view change + equivocation) -`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. +`formal-tla/QBFT.tla` (development tree) with `MCsafety.cfg` (N=4) / `MCsafety7.cfg` (N=7) and `MCliveness.cfg`. +**Measured 2026-07-19 and 2026-08-24: these configurations do NOT terminate** within the local budget (the state space is +in the tens of millions; `MCliveness` generated 543k distinct states in 197 s with 527k still queued). What is established +there is a partial explicit-state witness (9.35 million states without a violation at N=4 round 0), NOT a complete +check (`TLC-RUN-REPORT.md`, development tree). The all-N core (quorum intersection, agreement under locking) is already +proved for ANY N by the SMT suite; TLA+ is the independent method, and its value for partitions is that +`QBFTPartition.tla` does TERMINATE exhaustively (single height), unlike the complete model. --- -## 4. Cross-check optional: quint / Apalache +## 4. Optional cross-check: quint / Apalache -`FalconQuorum.qnt` e un cross-check secundar (vezi `CONSENSUS-VERIFICATION-2026-07-12.md` -pentru comenzile `quint run`). +`FalconQuorum.qnt` is a secondary cross-check (see `CONSENSUS-VERIFICATION-2026-07-12.md` for the `quint run` +commands). --- -## Granita cinstita (se citeste, nu se sare) +## The honest boundary (read it, do not skip it) -- 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. +- Model checking **is not a complete proof.** SMT proves the combinatorics of the design (vote counting, quorum + intersection, the binding of the certificate), not the Besu / EVM bytecode. TLC checks exhaustively only the finite + configuration stated (N=4 for partitions). +- Parametric SMT at N=9 proves the property for **that** N; the arithmetic core (quorum intersection, 2q > N) is + unbounded in N. +- When these models were written (July to October 2026), chain 2800 committed its blocks with **classical** secp256k1 + ECDSA seals and the post-quantum anchor was ADDITIVE; nothing here implies "post-quantum consensus". The chain of today + is described in the aere-node SPEC.md. (Corrected 2026-10-27: this point was stated in the present tense.) +- The cryptographic primitives (keccak injectivity, the soundness of the SP1 gateway, the validation of the Falcon seal) + are treated as `[VERIFY]`: modelled, not re-proved. +- In the models of August 2026 the anchor used K=3 = **f+1**, NOT a quorum; since block 20,715,632 the minimum is 7 of + 10 per scheme, as many as the QBFT quorum of the ten validators (corrected 2026-10-27: this point was stated in the + present tense). In the model, the uniqueness of the certificate comes from its binding to the finalized block, the + guard of `anchor_viewchange_smt.py`, not from an intersection of seals; the client code has no such guard (note added + 2026-10-01 in the runner). diff --git a/formal-consensus/anchor_blocking_quorum_smt.py b/formal-consensus/anchor_blocking_quorum_smt.py index e047b06..00dc850 100644 --- a/formal-consensus/anchor_blocking_quorum_smt.py +++ b/formal-consensus/anchor_blocking_quorum_smt.py @@ -155,9 +155,12 @@ class Block: falcon_ok = If(is_anchor(self.h), anykey >= self.K_eff(), BoolVal(True)) return And(self.qbft >= QBFT_Q, falcon_ok) -print("### AERE anchor BLOCKING-QUORUM SAFETY -- fork at 14,050,000, K=3, N=9, q=6\n") +print("### AERE anchor THRESHOLD SAFETY on the chain of 2026-08-15 (K=3, N=9, q=6, registries R1 of 7 keys and R2 of 9)") +print("### modelled for anchor heights >= 14,050,000, called 'the fork' below. Corrected 2026-10-27: that height is the bound of") +print("### this model, not a blocking fork: the property armed there changed no enforcement (correction of 2026-08-19), and the K=3") +print("### step is from 13,034,000. Today: ten validators since 2026-09-11, minimum 7 per scheme since block 20,715,632.\n") print(f" anchor grid: every {ANCHOR_INTERVAL} blocks from {ANCHOR_START}; " - f"fork {FORK_BLOCKING} is {'ON' if (FORK_BLOCKING-ANCHOR_START)%ANCHOR_INTERVAL==0 else 'OFF'} the grid " + f"model bound {FORK_BLOCKING} is {'ON' if (FORK_BLOCKING-ANCHOR_START)%ANCHOR_INTERVAL==0 else 'OFF'} the grid " f"((14050000-13014000)/32 = {(FORK_BLOCKING-ANCHOR_START)//ANCHOR_INTERVAL})\n") # ============================================================================= @@ -165,14 +168,14 @@ print(f" anchor grid: every {ANCHOR_INTERVAL} blocks from {ANCHOR_START}; " # ============================================================================= s = Solver() s.add(Int('r') == (FORK_BLOCKING - ANCHOR_START) % ANCHOR_INTERVAL, Int('r') != 0) -check("S0a CONFIG: the blocking-fork height 14,050,000 lies ON the anchor grid " +check("S0a CONFIG: the model bound 14,050,000 lies ON the anchor grid " "(it is itself an anchor height)", s) s = Solver() h = Int('h') s.add(h >= FORK_BLOCKING, sched_K(h) != K_TARGET) -check("S0b SCHEDULE (all h >= fork): the min-seals schedule pins K == 3 at every " - "blocking-era height (13034000:3 step is below the fork)", s) +check("S0b SCHEDULE (all h >= 14,050,000, schedule of 2026-08-15): the min-seals schedule pins K == 3 at every " + "modelled height (the 13034000:3 step is below the bound)", s) s = Solver() h = Int('h') @@ -185,8 +188,8 @@ check("S0c REGISTRY PARTITION (all h): every height from 13,014,000 on is covere s = Solver() h = Int('h') s.add(h >= FORK_BLOCKING, Not(h >= REG2_START)) -check("S0d REGISTRY AT FORK (all h >= fork): the active registry in the blocking " - "era is the 9-key registry (fork 14,050,000 > rotation 13,600,000)", s) +check("S0d REGISTRY AT THE BOUND (all h >= 14,050,000): the active registry in the " + "modelled range is the 9-key registry (14,050,000 > rotation 13,600,000)", s) # ============================================================================= # S1 -- THE INVARIANT (positive result). An anchor block at h >= fork, with the @@ -198,7 +201,7 @@ s = Solver(); s.add(b.wf()) s.add(b.h >= FORK_BLOCKING, is_anchor(b.h), Not(b.ceil_set)) s.add(b.finalized()) s.add(b.distinct_eligible_valid() <= 2) -check("S1 BLOCKING-QUORUM SAFETY: post-fork ANCHOR block finalized with <= 2 " +check("S1 THRESHOLD SAFETY: post-fork ANCHOR block finalized with <= 2 " "distinct valid eligible Falcon seals is IMPOSSIBLE (K=3 floor holds)", s) # same, with the ceiling engaged but at/above K: still no hole below 3 @@ -338,21 +341,22 @@ s = Solver() s.add(c >= 0, w == If(c <= 2, c, 2)) # planted cap 2 < K s.add(c >= K_TARGET, w < K_TARGET) check("S7b NEG-CTRL: PLANT a cap of 2 < K -> a 3-seal certificate is written short " - "of the quorum (why maxSeals below the schedule K is refused at load)", s, + "of K (why maxSeals below the schedule K is refused at load)", s, expect_unsat=False, kind="NEG-CTRL") # ============================================================================= -print("\n=== SUMMARY (anchor BLOCKING-QUORUM SAFETY) ===") +print("\n=== SUMMARY (anchor THRESHOLD SAFETY, chain of 2026-08-15) ===") allok = True for name, tag, ok, kind in results: print(f" {tag:9} [{kind}] {name}") allok = allok and ok print() if allok: - print(" PROVED: with the blocking fork active (h >= 14,050,000) no anchor block") + print(" PROVED: on the chain of 2026-08-15, at anchor heights >= 14,050,000 (the bound of this model; that") + print(" height changed no enforcement, correction of 2026-08-19) no anchor block") print(" can be finalized with fewer than K=3 valid Falcon seals from DISTINCT") print(" signers of the registry active at that height (the 9-key registry, since") - print(" the fork lies above the 13,600,000 rotation), and non-anchor blocks") + print(" the bound lies above the 13,600,000 rotation), and non-anchor blocks") print(" require no seals at all (proved in both directions). The mandated") print(" negative control FIRES: a planted rule permitting 2 seals finalizes an") print(" anchor block with exactly 2 seals (SAT), so the K>=3 guard is load-") @@ -362,7 +366,8 @@ if allok: print(" (and is the single designed path below 3); the maxSeals=5 write cap can") print(" never starve a certificate below K, and a planted cap of 2 does.") print(" BOUNDARY: design combinatorics of the finalization predicate, not Besu") - print(" bytecode, not the live chain; registries modelled as index sets.") + print(" bytecode, not the live chain; registries modelled as index sets. Today the set has ten validators") + print(" (since 2026-09-11) and the minimum is 7 per scheme (since block 20,715,632): not modelled here.") else: print(" NOT fully established (see FAILED / unexpected result above).") import sys diff --git a/formal-consensus/falcon_blocking_smt.py b/formal-consensus/falcon_blocking_smt.py index 93f7d67..20428b2 100644 --- a/formal-consensus/falcon_blocking_smt.py +++ b/formal-consensus/falcon_blocking_smt.py @@ -411,7 +411,7 @@ if allok: print(" blocks (N in {4,5,7}) -- and LIVE at the fault bound (N-f >= quorum, all") print(" N). The N>=7 requirement is machine-checked: N=7 is the smallest set that") print(" is BOTH safe (f>=2) and live (N-2>=quorum) against 2 Falcon faults. It is") - print(" also the next BFT-optimal 3f+1 size, and unlike the current N=5 (zero") + print(" also the next BFT-optimal 3f+1 size, and unlike N=5, the mainnet size when this model was written (2026-07-12; zero") print(" single-fault margin) it leaves margin > 0 over quorum for a single fault. At") print(" N in {4,5} two Falcon faults drop the correct set below quorum and the") print(" post-fork chain STALLS (shown reachable). Negative controls FIRE: dropping") @@ -426,10 +426,13 @@ if allok: print(" an empty eligible set (F5, with the fail-open trap firing as a control); and arms") print(" at full margin under coverage k=N (FIX-ARM).") print(" BOUNDARY: bounded per-N/per-k safety; unbounded liveness identity; DESIGN") - print(" combinatorics not Besu bytecode; the mainnet Falcon layer was log-only, not blocking,") - print(" until 2026-08-14 (blocking needs N>=7 + an ADDRESS-BOUND registry covering the set);") - print(" since then a validator refuses an anchor block whose certificate holds fewer valid seals than") - print(" the schedule requires (aere-node SPEC.md).") + print(" combinatorics not Besu bytecode; the mainnet per-block Falcon layer was log-only until block") + print(" 13,014,000 (2026-08-09), when the anchor rules were armed (blocking needs N>=7 + an ADDRESS-BOUND") + print(" registry covering the set): minimum 0 in the warm-up, then from block 13,034,000 a schedule step") + print(" to 3, held at an effective one by the emergency ceiling until 2026-08-14 (anchors of 2026-08-10 to") + print(" 2026-08-14 that carry fewer than three are named in the production client's two dated windows);") + print(" since 2026-08-14 a validator refuses an anchor block whose certificate holds fewer valid seals than") + print(" the schedule requires (aere-node SPEC.md; corrected 2026-10-27: this said log-only until 2026-08-14).") else: print(" NOT fully established (see FAILED / unexpected result above).") import sys diff --git a/formal-consensus/falcon_hybrid_dualquorum_smt.py b/formal-consensus/falcon_hybrid_dualquorum_smt.py index a1e9937..5bd9e34 100644 --- a/formal-consensus/falcon_hybrid_dualquorum_smt.py +++ b/formal-consensus/falcon_hybrid_dualquorum_smt.py @@ -346,7 +346,7 @@ if allok: print(" {7,9,11} under <= f equivocating faults of each kind (H1); a block missing EITHER") print(" quorum is REJECTED (H2a/H2b); and every hybrid-valid block is ECDSA-valid, so the") print(" Falcon requirement can only SHRINK the committable set -> the hybrid chain is AT") - print(" LEAST AS SAFE as today's ECDSA-only chain, a Falcon bug can never make it worse") + print(" LEAST AS SAFE as the ECDSA-only chain of 2026-07-18, when this model was written; a Falcon bug can never make it worse") print(" (H3, the core migration guarantee). The cost is liveness: hybrid needs 2f+1") print(" validators good in BOTH dimensions; at f+1 combined-bad it can stall where") print(" ECDSA-only would not (H4). N=7 has ZERO two-fault margin; N=9/N=11 restore margin.") diff --git a/formal-consensus/pqanchor_ceiling_monotonicity_smt.py b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py index 5a2a985..93ba13d 100644 --- a/formal-consensus/pqanchor_ceiling_monotonicity_smt.py +++ b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py @@ -16,7 +16,8 @@ # chain-stopping validity rule; min() makes that inexpressible by construction, # and this file machine-checks it. # -# Chain facts modelled as LAW (chain 2800, live values): +# Chain facts modelled as LAW (chain 2800 as of 2026-08-15; corrected 2026-10-27: this line said 'live values'. +# Today the set has ten validators, since 2026-09-11, and the minimum is 7 per scheme since block 20,715,632): # N = 9 validators, QBFT quorum = ceil(2N/3) = 6 # anchor heights: every 32 blocks from 13,014,000 # K schedule (height:K): 13,014,000 -> 0 ; 13,034,000 -> 3 @@ -50,14 +51,14 @@ K_STEP_HEIGHT = 13_034_000 # schedule step: K goes 0 -> 3 here K_WARMUP = 0 # schedule K on [13,014,000 .. 13,034,000) K_ARMED = 3 # schedule K from 13,034,000 on MAX_SEALS = 5 # write cap aere.pq.anchor.maxSeals -BLOCKING_FORK = 14_050_000 # no block finalizes without the Falcon quorum +BLOCKING_FORK = 14_050_000 # the withdrawn 'blocking fork' height (2026-08-19: it changed no enforcement); the FORK-* checks model the retired rule from here REG1_HEIGHT, REG1_KEYS = 13_014_000, 7 # registry window 1 REG2_HEIGHT, REG2_KEYS = 13_600_000, 9 # registry window 2 (rotation) N_VALIDATORS = 9 QBFT_QUORUM = 6 # ceil(2*9/3) def k_schedule(h): - """Height-indexed schedule 13014000:0, 13034000:3 (the live orar).""" + """Height-indexed schedule 13014000:0, 13034000:3 (the schedule of 2026-08-15; the published one has 14961456:6, 17102384:0, 17102416:6 and 20715632:7 too).""" return If(h >= K_STEP_HEIGHT, K_ARMED, K_WARMUP) def k_eff(h, ceil_set, ceiling): @@ -97,7 +98,10 @@ def check(name, s, expect_unsat=True, kind="PROOF"): return ok print("### AERE PQ anchor -- CEILING MONOTONICITY: minSealsCeiling can only LOWER K_eff,") -print("### and K_eff <= maxSeals at every height (a conforming producer always suffices)\n") +print("### and K_eff <= maxSeals at every height (a conforming producer always suffices)") +print("### Chain of 2026-08-15: N=9, K schedule 13014000:0, 13034000:3, registries of 7 then 9 keys. The FORK-* rows") +print("### model the per-block rule withdrawn on 2026-08-19 at 14,050,000, which changed no enforcement (dated") +print("### 2026-10-27; today: ten validators, minimum 7 per scheme since block 20,715,632).\n") # ---- CONFIG sanity: the quorum arithmetic and the height lattice are coherent - s = Solver() @@ -115,7 +119,7 @@ check(f"CONFIG K-step height {K_STEP_HEIGHT:,} lands ON the 32-block anchor latt s = Solver() s.add(Int('ok') == (1 if (BLOCKING_FORK - ANCHOR_START) % ANCHOR_STEP == 0 else 0)) s.add(Int('ok') == 1) -check(f"CONFIG blocking fork {BLOCKING_FORK:,} lands ON the 32-block anchor lattice", s, +check(f"CONFIG the withdrawn fork height {BLOCKING_FORK:,} lands ON the 32-block anchor lattice", s, expect_unsat=False, kind="CONFIG") # ============================================================================= @@ -223,7 +227,7 @@ h, ceiling, ceil_set = Int('h'), Int('ceiling'), Bool('ceil_set') s.add(is_anchor_height(h), h >= BLOCKING_FORK, ceiling >= 0) keff = k_eff(h, ceil_set, ceiling) s.add(Or(keff > MAX_SEALS, keff > reg_keys(h))) # negate: unsatisfiable threshold -check(f"FORK-1 blocking era (h >= {BLOCKING_FORK:,}): NO ceiling makes the anchor " +check(f"FORK-1 modelled range (h >= {BLOCKING_FORK:,}): NO ceiling makes the anchor " "threshold unsatisfiable (K_eff <= maxSeals AND K_eff <= registry keys)", s) # ============================ NEGATIVE CONTROLS ============================== @@ -248,7 +252,7 @@ s = Solver() h, ceiling = Int('h'), Int('ceiling') s.add(is_anchor_height(h), h >= BLOCKING_FORK, ceiling >= 0) s.add(k_eff_buggy_max(h, True, ceiling) > MAX_SEALS) -check(f"NEG-CTRL 2 PLANTED max() ceiling, blocking era: K_eff CAN exceed " +check(f"NEG-CTRL 2 PLANTED max() ceiling, h >= {BLOCKING_FORK:,}: K_eff CAN exceed " f"maxSeals={MAX_SEALS} (a settable value becomes a chain-stop switch)", s, expect_unsat=False, kind="NEG-CTRL") @@ -292,11 +296,11 @@ if allok: print(" threshold -- K_eff = min(K_schedule, ceiling), K_eff <= K_schedule for every") print(" height and every ceiling (a raising case is UNSAT, i.e. inexpressible), a") print(" ceiling at/above the schedule is a no-op, and K_eff <= maxSeals=5 and") - print(" K_eff <= registry keys (7 then 9) at every height including the blocking era") - print(" from 14,050,000 -- so a conforming producer (heard >= K_eff) always writes") + print(" K_eff <= registry keys (7 then 9, the registries of 2026-08-15) at every height,") + print(" 14,050,000 and above included -- so a conforming producer (heard >= K_eff) always writes") print(" min(heard, maxSeals) >= K_eff and the valve can never become a halt switch.") print(" Negative controls FIRE: the planted max() variant raises K_eff (SAT), pushes") - print(" it past the write cap in the blocking era (SAT, a chain-stop), a planted") + print(" it past the write cap at h >= 14,050,000 (SAT, a chain-stop), a planted") print(" under-cap without the loader guard yields only rejected certificates (SAT,") print(" why AERE-PQC-ANCHOR-CONF-01 exists), and the valve itself is non-vacuous (SAT).") print(" BOUNDARY: design arithmetic of the threshold pipeline, not Besu bytecode;") diff --git a/formal-consensus/registry_rotation_coverage_smt.py b/formal-consensus/registry_rotation_coverage_smt.py index 56a2e62..044f811 100644 --- a/formal-consensus/registry_rotation_coverage_smt.py +++ b/formal-consensus/registry_rotation_coverage_smt.py @@ -66,7 +66,7 @@ ANCHOR_STEP = 32 K_STEP_HEIGHT = 13_034_000 # K schedule: 13014000:0, 13034000:3 K_MIN_SEALS = 3 MAX_SEALS = 5 # write cap -FORK_BLOCKING = 14_050_000 # no finality without the Falcon quorum from here +FORK_BLOCKING = 14_050_000 # the withdrawn 'blocking fork' height (2026-08-19: it changed no enforcement), kept as a modelled bound REG1_HEIGHT = 13_014_000 REG1_KEYS = 7 REG2_HEIGHT = 13_600_000 @@ -123,7 +123,9 @@ def check(name, s, expect_unsat=True, kind="PROOF"): return ok print("### AERE PQ anchor -- REGISTRY ROTATION COVERAGE" - " (R1@13,014,000 x7 keys, R2@13,600,000 x9 keys)\n") + " (R1@13,014,000 x7 keys, R2@13,600,000 x9 keys: the registries of 2026-08-15)") +print("### (dated 2026-10-27: later epochs, ten keys from 2026-09-11 and post-quantum ids from block 20,836,228, are not") +print("### modelled here; 14,050,000 below is the withdrawn 'blocking fork' height, which changed no enforcement)\n") # ============================================================================= # C1a NO GAP: every anchor height >= 13,014,000 has at least one registry @@ -178,7 +180,7 @@ check("boundary: K-step height 13,034,000 IS anchor-aligned " s = Solver() k, r = Int('k'), Int('r') s.add(FORK_BLOCKING == ANCHOR0 + ANCHOR_STEP * k + r, r >= 1, r <= 31) -check("boundary: blocking fork 14,050,000 IS anchor-aligned " +check("boundary: the withdrawn fork height 14,050,000 IS anchor-aligned " "(remainder 1..31 is infeasible)", s) # ============================================================================= @@ -223,7 +225,7 @@ h = Int('h') add_anchor(s, h, 'k') s.add(h >= FORK_BLOCKING) s.add(Or(Not(active_r2(h)), active_r1(h))) # negate: not-R2 or still-R1 -check("blocking era: every anchor >= 14,050,000 is covered by the 9-key R2 " +check("modelled range: every anchor >= 14,050,000 is covered by the 9-key R2 " "and only by it", s) # the active registry at any blocking-era anchor can supply the Falcon quorum @@ -232,8 +234,8 @@ h = Int('h') add_anchor(s, h, 'k') s.add(h >= FORK_BLOCKING) s.add(reg_size(lookup(h)) < QBFT_QUORUM) # negate: registry too small -check("blocking era: active registry size (9) >= Falcon quorum (6) at every " - "blocking-era anchor", s) +check("modelled range: active registry size (9) >= Falcon quorum (6) at every " + "anchor >= 14,050,000", s) # minSealsCeiling only LOWERS K; effective K never exceeds K=3, the write cap # maxSeals=5, or the size of the registry active at any covered anchor @@ -308,9 +310,9 @@ if allok: print(" active-until-next semantics) covers every anchor height >= 13,014,000") print(" with EXACTLY one registry, unbounded in height: no gap, no overlap.") print(" The rotation boundary 13,600,000 is not anchor-aligned and interval") - print(" coverage loses no anchor; the K-step and blocking-fork heights are") + print(" coverage loses no anchor; the K-step height and the withdrawn fork height are") print(" anchor-aligned. Anchor-keyed validation is replay-stable and rejects") - print(" R2-only keys on R1-era anchors; the blocking era >= 14,050,000 is") + print(" R2-only keys on R1-era anchors; with the registries of 2026-08-15, every anchor >= 14,050,000 is") print(" served entirely by the 9-key registry, which always covers the Falcon") print(" quorum (6) and the effective K (<= 3 <= maxSeals 5). All four negative") print(" controls FIRE: a gapped schedule orphans an anchor, a forgotten") diff --git a/formal-consensus/run_consensus_verification.py b/formal-consensus/run_consensus_verification.py index b0ef206..62e4e08 100644 --- a/formal-consensus/run_consensus_verification.py +++ b/formal-consensus/run_consensus_verification.py @@ -27,7 +27,7 @@ CONSENSUS_MODELS = [ ("QBFT/IBFT 2.0 SAFETY (agreement)", "qbft_safety_smt.py"), ("Falcon LOG-ONLY no-op", "falcon_logonly_noop_smt.py"), ("Falcon BLOCKING safety/liveness/N>=7", "falcon_blocking_smt.py"), - ("Anchor THRESHOLD safety (K=3 of 9 on anchor blocks since 2026-08-14, registry rotation)", "anchor_blocking_quorum_smt.py"), + ("Anchor THRESHOLD safety (the chain of 2026-08-15: K=3 of 9 on anchor blocks, registry rotation; 7 of 10 since block 20,715,632)", "anchor_blocking_quorum_smt.py"), ("PQC ACTIVATION transition safety (log-only->blocking + contract-anchored registry)", "qbft_pqc_activation_smt.py"), ("QBFT LIVENESS (partial synchrony)", "qbft_liveness_smt.py"), ("QBFT explicit-Prepare counting (2026-07-14 2nd-client bug+fix)", "qbft_prepare_counting_smt.py"),