From 771d63728930d1ee4740acf7b9d5332e5959380f Mon Sep 17 00:00:00 2001 From: Aere Network Date: Thu, 29 Oct 2026 00:25:30 +0200 Subject: [PATCH] Runda 11 a reviziei prozei (2026-10-28): corecturi datate (nota de consens 17,250,000 / 17,700,000; clientul 2 al zecelea validator din 2026-09-11; 0,62 s masurat fata de tinta de 0,5 s; zece validatori, cvorum 7) si declaratiile de citari aduse la zi --- README.md | 37 +++++++++++++++++++++----------- test/formal/PROVEN-PROPERTIES.md | 13 +++++------ 2 files changed, 32 insertions(+), 18 deletions(-) diff --git a/README.md b/README.md index 6c52df2..348b7d1 100644 --- a/README.md +++ b/README.md @@ -11,18 +11,28 @@ runtime through environment variables (see `hardhat.config.js`). ## Scope, stated up front -Aere Network runs post-quantum signature verification natively on mainnet: Falcon-512 (`0x0AE1`), -Falcon-1024 (`0x0AE2`), ML-DSA-44 (`0x0AE3`), SLH-DSA-128s (`0x0AE4`) and SHAKE256 (`0x0AE5`) -have been live as precompiles since block 9,189,161. You can call them yourself against +Aere Network runs post-quantum cryptography natively on mainnet: four signature verifiers, +Falcon-512 (`0x0AE1`), Falcon-1024 (`0x0AE2`), ML-DSA-44 (`0x0AE3`) and SLH-DSA-128s (`0x0AE4`), +and the SHAKE256 hash (`0x0AE5`) have been live as precompiles since block 9,189,161 (corrected +2026-10-28: this listed SHAKE256 among the signature verifiers). You can call them yourself against `https://rpc.aere.network` without asking us for anything. -**Consensus on chain 2800 is classical secp256k1 ECDSA QBFT on every block, with a post-quantum -checkpoint every 32 blocks.** Since block 13,014,000 anchor blocks carry, under the block hash, a -certificate of validator post-quantum seals (Falcon-512, with SLH-DSA-SHA2-128s as well since -2026-09-04, at every 128th block since 2026-09-29; every anchor was 128 blocks apart from block -17,225,968 to block 20,746,736). Since block 20,715,632 (2026-09-29) a node rejects an anchor block -with fewer than seven valid seals per scheme, as many as the quorum of the ten validators (the seals prove those validators signed the block, not that it was decided, per the AIP-22 erratum of 2026-10-01); the minimum was -three (f+1 of nine, not a quorum) from 2026-08-14 and six from 2026-08-21. That +**Consensus on chain 2800 is QBFT with post-quantum layers on top of it, each dated +(headers are still admitted on their ECDSA commit seals until AIP-22 stage 5).** Since block 13,014,000 every +anchor block carries a certificate of validator post-quantum seals whose 32-byte digest sits under +the block hash (Falcon-512, with SLH-DSA-SHA2-128s as well since 2026-09-04, at every 128th block +since 2026-09-29; every anchor was 128 blocks apart from block 17,225,968 to block 20,746,736). +Since block 20,715,632 (2026-09-29) a node rejects an anchor block with fewer than seven valid +seals per scheme, as many as the quorum of the ten validators; the minimum was three (f+1 of nine, +not a quorum) from 2026-08-14 and six from 2026-08-21. Below block 24,148,752 (AIP-22 stage R, +2026-10-24) those seals proved that the validators signed the block, not that it was decided +(AIP-22 erratum of 2026-10-01); from that block a certificate that carries the quorum of one round +proves the decision. Every validator refuses a commit without a valid Falcon-512 seal of its +author, and since block 24,300,000 (AIP-22 stage 4, 2026-10-25) the Besu-derived validators, nine +of the ten, count a consensus vote only through the verified post-quantum seal of its author. +(Corrected 2026-10-28: until that date this paragraph opened by calling consensus on chain 2800 +classical secp256k1 ECDSA QBFT on every block, and said without a date that the seals prove +signing, not decision.) That checkpoint lives in the aere-node repository (patch 0003 and `anchor/`), not in this one: nothing in this repository makes consensus post-quantum, and the chain is not "post-quantum consensus" without that qualification (the per-block quorum claim published on 2026-08-15 was withdrawn on 2026-08-19). @@ -34,8 +44,11 @@ Two further limits worth knowing before you judge anything else here: - The on-chain zero-knowledge verifiers are classical BN254. They are broken by Shor's algorithm like any other elliptic-curve construction, and we do not describe them as quantum-safe. -The network is operated by nine Foundation-run validators (f=2, commit quorum 6 of 9; seven until -2026-08-09), so its Nakamoto coefficient is effectively one today. That is a real limitation, it is on the roadmap, and it is not fixed by any +The network is operated by ten Foundation-run validators since 2026-09-11 (f=3, commit quorum 7 +of 10; nine, with quorum 6 of 9, from 2026-08-09, and seven before; corrected 2026-10-28: this +said nine), nine of them on the Besu-derived client and the tenth, since 2026-09-11, on a second, +Nethermind-derived client that proposes and seals blocks, so its Nakamoto coefficient is +effectively one today. That is a real limitation, it is on the roadmap, and it is not fixed by any code in this repository. ## Layout diff --git a/test/formal/PROVEN-PROPERTIES.md b/test/formal/PROVEN-PROPERTIES.md index f387f11..283c7a1 100644 --- a/test/formal/PROVEN-PROPERTIES.md +++ b/test/formal/PROVEN-PROPERTIES.md @@ -1,5 +1,7 @@ # Formally analysed properties, AERE PQC contracts +> **Note added 2026-10-28.** The note below is dated 2026-08-19 and describes that day. Since then the minimum certificate of an anchor block was raised to six valid seals on 2026-08-21 and, at block 20,715,632 (2026-09-29), to seven of each required scheme (Falcon-512, with SLH-DSA-SHA2-128s as well since 2026-09-04, at every 128th block since 2026-09-29), as many as the quorum of the ten validators; anchors were every 128th block from block 17,225,968 to block 20,746,736 and are every 32nd again since. How blocks are final on chain 2800 is set out, stage by stage and dated, in AIP-22. None of the contract properties analysed here depends on any of this. + > **Note added 2026-08-19.** Statements in this document that consensus on chain 2800 is (or remains) classical secp256k1 ECDSA QBFT were written before the post-quantum header anchor went live, and remain true for block-by-block finality. Since block 13,014,000 anchor blocks (every 32nd block, on every one since block 13,889,296) also carry, under the block hash, a certificate of validator Falcon-512 seals, and since 2026-08-14 a node rejects an anchor block with fewer than three valid seals (f+1 of nine; eight or nine are carried in practice). That is a post-quantum checkpoint about every 16 seconds, not a per-block quorum: the claim published on 2026-08-15 that from block 14,050,000 no block finalizes without a post-quantum quorum was wrong (the per-block rule armed at that height is retired in the shipped code in favour of the anchor rules) and was withdrawn on 2026-08-19. Details: https://aere.network/quantum.html and the aere-node repository, anchor/README.md. Symbolic execution with **halmos 0.3.3** (Z3 4.12.6) over **Solidity 0.8.23** builds @@ -140,8 +142,8 @@ vacuously passing. - Not "formally verified" as a blanket statement, only P1–P4, R1–R3 within the bounds above. - No claim about the PQC precompiles' cryptographic correctness (oracle assumption). -- No claim about consensus: AERE consensus remains classical ECDSA QBFT; these are - application-layer contract properties only. +- No claim about consensus: these are application-layer contract properties only (what + consensus on chain 2800 is, stage by stage and dated, is in AIP-22; corrected 2026-10-28: this line called AERE consensus classical ECDSA QBFT, in the present tense). - No proof for byte lengths / `_count` values outside the enumerated bounds. --- @@ -243,8 +245,8 @@ real counterexample to a should-hold invariant was found.** One benign, non-expl observation: `AereAgentDID.authorize`'s overflow guard `s.spent + amount < s.spent` is **dead code** under Solidity-0.8 checked arithmetic (the addition reverts before the comparison can be true), it fails **safe** (revert = no state change), so it is a -redundancy, **not a defect**. Consensus is unaffected: AERE remains classical ECDSA -QBFT; these are application-layer contract properties only. "Proven" means only the +redundancy, **not a defect**. Consensus is +unaffected: these are application-layer contract properties only (corrected 2026-10-28: this sentence also called AERE classical ECDSA QBFT, in the present tense). "Proven" means only the specific properties + bounds + assumptions listed, **not** "formally verified" as a blanket claim. @@ -326,5 +328,4 @@ controls fire as expected (confirming the guards are load-bearing). The only `sa result on a "should-hold" phrasing was the AereLendingMarket **L3-note**, which is a **1-wei rounding-dust** discrepancy in the protocol-favouring (safe) direction, documented above as expected DeFi rounding, **not a defect**. Consensus is -unaffected: AERE remains classical ECDSA QBFT; these are application-layer -contract properties only. +unaffected: these are application-layer contract properties only (corrected 2026-10-28: this sentence also called AERE classical ECDSA QBFT, in the present tense).