From c9ba6d4bec8c81af294c9ae072a20b0f28910edb Mon Sep 17 00:00:00 2001 From: Aere Network Date: Thu, 1 Oct 2026 17:10:21 +0300 Subject: [PATCH] AIP-21 erratum and AIP-23 note (2026-10-01), formal models annotated: the post-quantum commit seal carries no round AIP-21: a record that reaches `post-quantum` shows that the commit quorum of distinct validators sealed the block post-quantum in some round; it does not by itself prove that the block was decided (follows the AIP-22 erratum of the same day). AIP-23: dated note on what the finality level rests on; level names unchanged. Three formal models carry a dated note where they treated certificate uniqueness as a property of the code rather than of the model. Co-Authored-By: Claude Opus 5.5 --- aips/AIP-21.md | 25 ++++++++++++++++++- aips/AIP-23.md | 6 +++++ formal-consensus/anchor_viewchange_smt.py | 9 +++++++ .../pqanchor_ceiling_monotonicity_smt.py | 3 +++ .../registry_rotation_coverage_smt.py | 3 +++ .../run_consensus_verification.py | 2 +- 6 files changed, 46 insertions(+), 2 deletions(-) diff --git a/aips/AIP-21.md b/aips/AIP-21.md index d897c3f..f0b3371 100644 --- a/aips/AIP-21.md +++ b/aips/AIP-21.md @@ -4,6 +4,12 @@ > chain 2800 from block 17,225,968 to block 20,746,736 (2026-09-05 to 2026-09-29). Since block 20,746,736 (AIP-22 > stage 2) a Falcon-512 certificate is carried every 32nd block and SLH-DSA seals every 128th, with at least seven of > ten seals per scheme since block 20,715,632 (AIP-22 stage 1). +> +> **Correction added 2026-10-01.** The commit seal this record counts carries no round, and the store keeps seals by block +> hash across rounds. A record that reaches `post-quantum` shows that at least the commit quorum of distinct validators +> sealed the block post-quantum, in some round; it does not by itself prove that the block was decided. See the Errata entry +> of that date, which follows the AIP-22 erratum of the same day. Chain 2800 today, below AIP-22 stage 5, is not affected: +> a node imports a block only with the ECDSA commit quorum of a single round. ## Preamble @@ -254,7 +260,24 @@ local, so the record is read on the validator, or through Aere Cloud when that r ## Errata -None. +- 2026-10-01, Abstract, Motivation, "The record" (the verdict `post-quantum`) and "The permanent record": the record counts + Falcon-512 seals over `M(B) = keccak256(RLP["AERE-PQ-COMMIT-1", chainId, number(B), hash(B)])`, kept by the block's on-chain + hash; neither the seal nor the key carries the round. In QBFT an honest validator can commit a block in one round while a + different block is decided in a later round, and seals over `M(B)` made in different rounds cannot be told apart (AIP-22, + Errata, 2026-10-01). Measured on 2026-10-01 in the reference client: seven valid Falcon-512 seals over `M(p)` from rounds 0 + and 2 on a block `p` that no round decided (test class `AereRoundFreeCertificateTest`), and a quorum of one round assembled + from the post-quantum seals of rounds 0 and 2 in the decision collector, which counts the same seals, under the adversary of + AIP-22 who forges ECDSA (`AereRoundFreeCommitTest`, case RF2-Q1). For `aere_getPqFinality` itself this is derived from the + code (the same seal store, kept by hash), not run against the method. Withdrawn as written, until the commit seal binds the + round: (1) "the immediate post-quantum finality of a block has been true" (Abstract) and the reading of the record as the + answer to "is this block final under post-quantum assumptions" (Motivation); (2) the verdict `post-quantum` as finality: the + field and its values stay (clients read them) and mean that at least the commit quorum of distinct validators' seals over + `M(B)` verify now, which is evidence of participation, not of the decision; (3) "The permanent record": the anchor + certificate is the permanent record of the same participation, and the AIP-22 erratum says what it proves. Not affected: + chain 2800 below AIP-22 stage 5, where a node imports a block only with the ECDSA commit quorum of one round, so the block of + a record is final there against an adversary who cannot forge ECDSA; the record as evidence of which validators sealed the + block; and the agreement of the two clients on the same record. The remedy is the one the AIP-22 erratum proposes: a commit + seal that binds the round, with a quorum of one round; it is a coordinated fork and is not scheduled. ## Post-Acceptance Outcome Record diff --git a/aips/AIP-23.md b/aips/AIP-23.md index b9f2153..e46010a 100644 --- a/aips/AIP-23.md +++ b/aips/AIP-23.md @@ -1,5 +1,11 @@ # AIP-23: AERE Proof Protocol (a portable, verifiable statement + on-chain finality envelope) +> **Note added 2026-10-01.** "Finality" and the level `post-quantum` in this document name what the verifier checks: that the +> notary's record is in a state under a header whose hash the seals of a verified anchor certificate signed (section 4). Since +> the AIP-22 erratum of 2026-10-01, such a certificate is evidence that its signers sealed that block post-quantum, in some +> round; it does not by itself prove that the block was decided. The level names, the verdicts and the verifier's output stay +> as they are; consumers read them. + ## Preamble | Field | Value | diff --git a/formal-consensus/anchor_viewchange_smt.py b/formal-consensus/anchor_viewchange_smt.py index 0e1aa2f..d985492 100644 --- a/formal-consensus/anchor_viewchange_smt.py +++ b/formal-consensus/anchor_viewchange_smt.py @@ -41,6 +41,15 @@ # 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. +# +# Note added 2026-10-01 (AIP-22 erratum of that date). The guard this model's uniqueness rests on, "the +# certificate's digest is bound to the block QBFT FINALIZED", is NOT a rule of the shipped code: the anchor rules +# (PqAnchorDigestRule, PqAnchorSealsRule) check that the certificate sits under the anchor's hash and that K +# distinct valid seals sign M(parent), and M carries no round. The code therefore behaves as NEGATIVE CONTROL A +# below, and the erratum measures it in the reference client: seven valid seals over a block that no round +# decided, and an anchor over it that passes both rules (AereRoundFreeCertificateTest). AV1 and AV2 are +# properties of this model, not of chain 2800. Below AIP-22 stage 5 such an anchor's own header still needs the +# ECDSA commit quorum of one round, which an adversary without the classical keys cannot produce. # ----------------------------------------------------------------------------- from z3 import (Int, Bool, Function, IntSort, Solver, And, Or, Not, Implies, If, Sum, sat, unsat) diff --git a/formal-consensus/pqanchor_ceiling_monotonicity_smt.py b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py index a2dfd6e..5a2a985 100644 --- a/formal-consensus/pqanchor_ceiling_monotonicity_smt.py +++ b/formal-consensus/pqanchor_ceiling_monotonicity_smt.py @@ -23,6 +23,9 @@ # write cap maxSeals = 5 # emergency ceiling minSealsCeiling: only LOWERS K (that is the theorem) # blocking fork at 14,050,000: no block finalizes without the Falcon quorum +# Note added 2026-10-01: the "blocking fork at 14,050,000" premise was withdrawn on 2026-08-19 (that height +# armed a per-block rule the anchor rules had already retired, and it changed no enforcement). The FORK-* +# checks below model that retired rule; they say nothing about the chain after that height. # registry rotation: 13,014,000 -> 7 keys ; 13,600,000 -> 9 keys ; # every height is covered by EXACTLY one registry # diff --git a/formal-consensus/registry_rotation_coverage_smt.py b/formal-consensus/registry_rotation_coverage_smt.py index c8f3a7f..56a2e62 100644 --- a/formal-consensus/registry_rotation_coverage_smt.py +++ b/formal-consensus/registry_rotation_coverage_smt.py @@ -24,6 +24,9 @@ # K schedule 13,014,000:0 then 13,034,000:3 (K=3 minimum Falcon seals) # write cap maxSeals = 5; emergency minSealsCeiling can only LOWER K # blocking fork at 14,050,000: no block finalizes without the Falcon quorum +# Note added 2026-10-01: the "blocking fork at 14,050,000" premise was withdrawn on 2026-08-19 (that height +# armed a per-block rule the anchor rules had already retired, and it changed no enforcement). The FORK-* +# checks below model that retired rule; they say nothing about the chain after that height. # registry rotation 13,014,000 -> 7 keys, 13,600,000 -> 9 keys # # Schedule semantics (the design being proved): a registry is active from its diff --git a/formal-consensus/run_consensus_verification.py b/formal-consensus/run_consensus_verification.py index d0aac4c..9cc2f4b 100644 --- a/formal-consensus/run_consensus_verification.py +++ b/formal-consensus/run_consensus_verification.py @@ -34,7 +34,7 @@ CONSENSUS_MODELS = [ ("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"), + ("Anchor x VIEW-CHANGE (MODEL only, under its finalized-block guard: no round change yields two valid PQ certificates, N=9; the code has no such guard, Note added 2026-10-01)", "anchor_viewchange_smt.py"), ("PQ MESSAGE-LAYER ENFORCEMENT (SPEC 2.6: armed-requires-valid, no cross-domain/position/author replay, below-fork unchanged, commit form under armed anchor = D-311)", "pq_message_enforcement_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"),