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

@@ -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`),
+Aere Network runs post-quantum cryptography natively on mainnet: four signature verifiers,
-Falcon-1024 (`0x0AE2`), ML-DSA-44 (`0x0AE3`), SLH-DSA-128s (`0x0AE4`) and SHAKE256 (`0x0AE5`)
+Falcon-512 (`0x0AE1`), Falcon-1024 (`0x0AE2`), ML-DSA-44 (`0x0AE3`) and SLH-DSA-128s (`0x0AE4`),
-have been live as precompiles since block 9,189,161. You can call them yourself against
+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
+**Consensus on chain 2800 is QBFT with post-quantum layers on top of it, each dated
-checkpoint every 32 blocks.** Since block 13,014,000 anchor blocks carry, under the block hash, a
+(headers are still admitted on their ECDSA commit seals until AIP-22 stage 5).** Since block 13,014,000 every
-certificate of validator post-quantum seals (Falcon-512, with SLH-DSA-SHA2-128s as well since
+anchor block carries a certificate of validator post-quantum seals whose 32-byte digest sits under
-2026-09-04, at every 128th block since 2026-09-29; every anchor was 128 blocks apart from block
+the block hash (Falcon-512, with SLH-DSA-SHA2-128s as well since 2026-09-04, at every 128th block
-17,225,968 to block 20,746,736). Since block 20,715,632 (2026-09-29) a node rejects an anchor block
+since 2026-09-29; every anchor was 128 blocks apart from block 17,225,968 to block 20,746,736).
-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
+Since block 20,715,632 (2026-09-29) a node rejects an anchor block with fewer than seven valid
-three (f+1 of nine, not a quorum) from 2026-08-14 and six from 2026-08-21. That
+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
+The network is operated by ten Foundation-run validators since 2026-09-11 (f=3, commit quorum 7
-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
+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

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
+- No claim about consensus: these are application-layer contract properties only (what
-  application-layer contract properties only.
+  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
+redundancy, **not a defect**. Consensus is
-QBFT; these are application-layer contract properties only. "Proven" means only the
+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
+unaffected: these are application-layer contract properties only (corrected 2026-10-28: this sentence also called AERE classical ECDSA QBFT, in the present tense).
-contract properties only.