From 9b2a69ab6bb713b8cdfa548f190a4b91d2c76e84 Mon Sep 17 00:00:00 2001 From: Aere Network Date: Tue, 27 Oct 2026 06:48:09 +0200 Subject: [PATCH] Dated corrections (2026-10-27): README (a validator refuses an anchor below the threshold; the published follower lowers the count to one seal); formal-consensus models print the chain facts of today or date the ones of their time (ten validators, the anchor certificate enforced since 2026-08-14, votes attributed through post-quantum seals since block 24,300,000); verdicts unchanged (ALL MODELS PASS) --- README.md | 6 ++++-- formal-consensus/anchor_viewchange_smt.py | 2 +- formal-consensus/ap2_mandate_smt.py | 3 ++- formal-consensus/bitstring_status_smt.py | 3 ++- formal-consensus/falcon_blocking_smt.py | 15 ++++++++------ .../falcon_hybrid_dualquorum_smt.py | 6 ++++-- formal-consensus/falcon_logonly_noop_smt.py | 6 ++++-- formal-consensus/partition_safety_smt.py | 3 ++- formal-consensus/pqfinality_smt.py | 3 ++- formal-consensus/qbft_locking_smt.py | 13 ++++++------ formal-consensus/qbft_pqc_activation_smt.py | 20 ++++++++++--------- formal-consensus/qbft_safety_smt.py | 8 +++++--- formal-consensus/recovery_registry_smt.py | 3 ++- formal-consensus/reputation_gate_smt.py | 3 ++- 14 files changed, 57 insertions(+), 37 deletions(-) diff --git a/README.md b/README.md index e6034ca..e2bfc33 100644 --- a/README.md +++ b/README.md @@ -17,9 +17,11 @@ have been live as precompiles since block 9,189,161. You can call them yourself **Consensus on chain 2800 is QBFT, with a post-quantum checkpoint every 32 blocks; since block 24,300,000 (AIP-22 stage 4) every validator attributes each consensus vote only through the verified post-quantum seal of its author (headers are still admitted on their ECDSA commit seals until AIP-22 stage 5).** 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 +17,225,968 to block 20,746,736). Since block 20,715,632 (2026-09-29) a validator rejects an anchor block with fewer than seven valid seals per scheme, as many as the quorum of the ten validators (below block 24,148,752 the seals proved those validators signed the block, not that it was decided, per the AIP-22 erratum of 2026-10-01, and from that block a certificate that carries the quorum of one round proves the decision; this clause corrected on 2026-10-25); the minimum was -three (f+1 of nine, not a quorum) from 2026-08-14 and six from 2026-08-21. That +three (f+1 of nine, not a quorum) from 2026-08-14 and six from 2026-08-21. A node started from the published node package +(aere-node) lowers that count to one seal, at the cost stated in section 6.4 of its `SPEC.md` (corrected 2026-10-27: this said +"a node rejects"). 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). diff --git a/formal-consensus/anchor_viewchange_smt.py b/formal-consensus/anchor_viewchange_smt.py index d985492..bc2432c 100644 --- a/formal-consensus/anchor_viewchange_smt.py +++ b/formal-consensus/anchor_viewchange_smt.py @@ -248,7 +248,7 @@ if allok: 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.") + print(" ADDITIVE post-quantum anchor, as on chain 2800 when this model was written (August 2026).") else: print(" NOT fully established (see FAILED / unexpected result above).") import sys diff --git a/formal-consensus/ap2_mandate_smt.py b/formal-consensus/ap2_mandate_smt.py index 2f65e90..060bd9c 100644 --- a/formal-consensus/ap2_mandate_smt.py +++ b/formal-consensus/ap2_mandate_smt.py @@ -246,7 +246,8 @@ if allok: print(" modelled as the sigValid predicate, not re-proved. mandateHash chain/contract binding") print(" and keccak256 injectivity are [VERIFY], modelled as hash equality.") print(" DESIGN: application-layer payment authorization, holds NO funds (the cap is accounting,") - print(" the AERE402 rail moves value); consensus stays classical ECDSA QBFT. The open path") + print(" the AERE402 rail moves value) and does not touch consensus (classical ECDSA QBFT when") + print(" this model was written, before 2026-08-02; see the aere-node SPEC.md for today). The open path") print(" (SETTLEMENT_EXECUTOR == 0) is verification/test only per the contract's documented L3;") print(" production MUST set the executor, which this model proves closes the vector. This checks") print(" the guard logic under unbounded-Int arithmetic, not the compiled EVM bytecode.") diff --git a/formal-consensus/bitstring_status_smt.py b/formal-consensus/bitstring_status_smt.py index b84a92c..6db07ab 100644 --- a/formal-consensus/bitstring_status_smt.py +++ b/formal-consensus/bitstring_status_smt.py @@ -195,7 +195,8 @@ if allok: print(" and the on-chain path is fail-closed off until configured; its codeless-verifier (L1)") print(" guard and fail-closed binding are covered by the aere-pq-screen Hardhat tests, not") print(" modelled here. Application-layer compliance tooling, no funds, no PII on chain (an") - print(" anonymous bitset keyed by numeric index), consensus classical ECDSA QBFT. DESIGN-level") + print(" anonymous bitset keyed by numeric index), no change to consensus (classical ECDSA QBFT") + print(" when this model was written, before 2026-08-02; see the aere-node SPEC.md for today). DESIGN-level") print(" state logic, not the compiled EVM bytecode.") else: print(" NOT fully established (see FAILED / unexpected CEX above).") diff --git a/formal-consensus/falcon_blocking_smt.py b/formal-consensus/falcon_blocking_smt.py index 599053d..93f7d67 100644 --- a/formal-consensus/falcon_blocking_smt.py +++ b/formal-consensus/falcon_blocking_smt.py @@ -25,9 +25,10 @@ # # HONEST BOUNDARY: B-SAFETY per-N is a BOUNDED check; the intersection lemma and # the N-f>=quorum liveness identity are UNBOUNDED (all N). This is the certificate -# COMBINATORICS of the design, not the Besu Java code, and NOT mainnet: chain -# 2800 runs classical ECDSA QBFT and the Falcon layer there is LOG-ONLY, not -# blocking (blocking requires N>=7 + a re-genesis with a Falcon anchor). +# COMBINATORICS of the design, not the Besu Java code, and NOT mainnet: when this +# model was written (before 2026-08-02) chain 2800 ran classical ECDSA QBFT and its +# Falcon layer was LOG-ONLY, not blocking (dated on 2026-10-27; see the aere-node +# SPEC.md for the chain of today). # ----------------------------------------------------------------------------- from z3 import (Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat) @@ -191,7 +192,7 @@ check("THRESHOLD-T1b N=7 IS safe(f=2) AND live(N-2=5>=q=5) for 2 faults " # (T2) SINGLE-Falcon-fault liveness margin: margin1(N) = (N-1) - quorum(N). # margin1 == 0 EXACTLY at N in {4,5} (a single fault forces ALL remaining # honest to sign; any further crash/slowness halts) and margin1 >= 1 at -# N >= 6. The current AERE mainnet size N=5 has ZERO single-fault margin; +# N >= 6. The AERE mainnet size of that time, N=5, had ZERO single-fault margin; # N=7 (the next BFT-OPTIMAL 3f+1 size) both restores positive margin AND # tolerates 2 Falcon faults (T1) -- that combination is the driver for N>=7. print(" single-fault margin (N-1)-quorum(N): " @@ -425,8 +426,10 @@ 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; mainnet Falcon layer is LOG-ONLY, not") - print(" blocking (blocking needs N>=7 + an ADDRESS-BOUND registry covering the set).") + 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).") 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 e5195a1..a1e9937 100644 --- a/formal-consensus/falcon_hybrid_dualquorum_smt.py +++ b/formal-consensus/falcon_hybrid_dualquorum_smt.py @@ -40,7 +40,8 @@ # # HONEST BOUNDARY: bounded per-N checks over N in {7,9,11(,13)}; DESIGN # combinatorics of the dual-quorum rule, NOT the Besu Java bytecode; NOT mainnet -# (chain 2800 is classical ECDSA QBFT, N=7, no Falcon layer of any kind). +# (chain 2800 was classical ECDSA QBFT, N=7, with no Falcon layer of any kind when +# this model was written, before 2026-08-02; dated on 2026-10-27). # Cryptographic soundness of Falcon-512 is out of scope (NIST KAT / precompile). # ----------------------------------------------------------------------------- from z3 import Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat @@ -356,7 +357,8 @@ if allok: print(" ECDSA leg even when M= q-f (CEX). A single non-locking node") print(" among locking Besu cannot fork the chain, but the second client cannot approach") @@ -266,8 +267,8 @@ if allok: print(" justification, agreement breaks even with every node running it. This is the formal") print(" reason the discretionary-list acceptor was rejected for the signed certificate.") print(" BOUNDARY: bounded per-N/round model checks of the locking combinatorics, not the") - print(" C# bytecode; complements the adversarial soak. Chain 2800 consensus is classical") - print(" ECDSA QBFT.") + print(" C# bytecode; complements the adversarial soak. Chain 2800 consensus was classical") + print(" ECDSA QBFT when this model was written (July 2026); see the aere-node SPEC.md for today.") else: print(" NOT fully established (see FAILED above).") import sys diff --git a/formal-consensus/qbft_pqc_activation_smt.py b/formal-consensus/qbft_pqc_activation_smt.py index eb64294..5dc29a0 100644 --- a/formal-consensus/qbft_pqc_activation_smt.py +++ b/formal-consensus/qbft_pqc_activation_smt.py @@ -52,11 +52,12 @@ # uninterpreted function with an injectivity constraint over the terms used. # # HONEST BOUNDARY: this is the certificate/registry DESIGN combinatorics of the -# activation transition, NOT the Besu Java bytecode, and NOT mainnet. Chain 2800 -# runs classical ECDSA QBFT (N=7, f=2, quorum 5); the Falcon layer there is -# LOG-ONLY, non-gating, and carries no certificate. Activating BLOCKING and the -# contract-anchored registry is isolated-testnet R&D and remains audit-gated and -# founder-gated. A2's per-N conflict check is bounded (N=7); the fork-gate and +# activation transition, NOT the Besu Java bytecode, and NOT mainnet. When this +# model was written (before 2026-08-02) chain 2800 ran classical ECDSA QBFT (N=7, f=2, +# quorum 5) and its Falcon layer was LOG-ONLY, non-gating, with no certificate, and +# activating BLOCKING and the contract-anchored registry was isolated-testnet R&D, +# audit-gated and founder-gated (dated on 2026-10-27; the chain of today is in the +# aere-node SPEC.md). A2's per-N conflict check is bounded (N=7); the fork-gate and # registry lemmas are unbounded over the modeled variables. Cryptographic # soundness of Falcon-512 / keccak256 is out of scope (NIST KAT + precompile). # ----------------------------------------------------------------------------- @@ -88,7 +89,7 @@ def check(name, s, expect_unsat=True, kind="PROOF"): N = 7 q = quorum(N); f = faultbound(N) print("### AERE PQC ACTIVATION transition -- log-only->blocking + contract-anchored Falcon registry\n") -print(f" live/target set N={N}: quorum q={q}, fault bound f={f} (chain 2800 = classical ECDSA QBFT)\n") +print(f" modelled set N={N}: quorum q={q}, fault bound f={f} (the chain 2800 set, then classical ECDSA QBFT, when this model was written, before 2026-08-02)\n") # ============================================================================= # GROUP A -- NO SPLIT ACROSS THE ACTIVATION HEIGHT. @@ -328,9 +329,10 @@ if allok: print(" so each guard (single fork constant, ceil(2N/3), fork-gating, immutability, fail-") print(" closed) is load-bearing.") print(" BOUNDARY: DESIGN combinatorics of the transition, NOT Besu bytecode, NOT mainnet.") - print(" Chain 2800 = classical ECDSA QBFT (N=7,f=2,q=5); the Falcon layer there is LOG-ONLY") - print(" and non-gating. Blocking + contract-anchored registry stay isolated-testnet R&D,") - print(" audit-gated and founder-gated.") + print(" When this model was written, before 2026-08-02, chain 2800 was classical ECDSA QBFT") + print(" (N=7, f=2, q=5) with a log-only, non-gating Falcon layer, and blocking with a") + print(" contract-anchored registry was isolated-testnet R&D; the chain of today is described") + print(" in the aere-node SPEC.md (this paragraph dated on 2026-10-27).") else: print(" NOT fully established (see FAILED / unexpected result above).") import sys diff --git a/formal-consensus/qbft_safety_smt.py b/formal-consensus/qbft_safety_smt.py index fdc2481..e2c65d9 100644 --- a/formal-consensus/qbft_safety_smt.py +++ b/formal-consensus/qbft_safety_smt.py @@ -34,8 +34,9 @@ # A bounded model check is NOT a proof for all N or all executions; it is a # decision procedure over the stated finite configuration. Stated honestly. # * This models the QBFT message combinatorics / locking DESIGN, not the Besu -# Java bytecode. Chain 2800 consensus is classical ECDSA QBFT (NOT post- -# quantum); the Falcon layer is modeled separately (falcon_*_smt.py). +# Java bytecode. Chain 2800 consensus was classical ECDSA QBFT (NOT post- +# quantum) when this model was written, before 2026-08-02 (dated on 2026-10-27); +# the Falcon layer is modeled separately (falcon_*_smt.py). # ----------------------------------------------------------------------------- from z3 import (Int, Bool, Solver, And, Or, Not, Implies, If, Sum, sat, unsat) @@ -246,7 +247,8 @@ if allok: print(" proving the ceil(2N/3) quorum and the locking rule are load-bearing.") print(" BOUNDARY: L1 is unbounded (all N); L2/L3 are bounded model checks over") print(" the stated finite configs; this is the DESIGN combinatorics, not Besu") - print(" bytecode; chain 2800 consensus is classical ECDSA QBFT.") + print(" bytecode; chain 2800 consensus was classical ECDSA QBFT when this model was") + print(" written, before 2026-08-02 (see the aere-node SPEC.md for the chain of today).") else: print(" NOT fully established (see FAILED / unexpected result above).") import sys diff --git a/formal-consensus/recovery_registry_smt.py b/formal-consensus/recovery_registry_smt.py index 60b6b1a..526635a 100644 --- a/formal-consensus/recovery_registry_smt.py +++ b/formal-consensus/recovery_registry_smt.py @@ -179,7 +179,8 @@ if allok: print(" un-activated chain) is a trusted primitive, modelled here as the verify predicate, not") print(" re-proved. keccak256 injectivity (the nonce-bound record hash) is [VERIFY], modelled.") print(" DESIGN: this contract records ATTESTATIONS about recovery events; it does not observe") - print(" consensus, halt the chain, or activate PQ consensus (still classical ECDSA QBFT). The") + print(" consensus, halt the chain, or activate PQ consensus (consensus was classical ECDSA QBFT") + print(" when this model was written, before 2026-08-02; see the aere-node SPEC.md for today). The") print(" uint64 nonce cannot realistically overflow. This checks the guard logic, not the") print(" compiled EVM bytecode.") else: diff --git a/formal-consensus/reputation_gate_smt.py b/formal-consensus/reputation_gate_smt.py index c519db0..84086ee 100644 --- a/formal-consensus/reputation_gate_smt.py +++ b/formal-consensus/reputation_gate_smt.py @@ -168,7 +168,8 @@ if allok: print(" curates WHO may write but cannot set a reputation value or exceed the clamp. The live") print(" AereAIReputation computes the score FROM the delta; this model bounds what the adapter") print(" forwards (authorized + clamped), not the live contract's score formula. Application-") - print(" layer, no funds, consensus classical ECDSA. DESIGN-level guard logic, not the bytecode.") + print(" layer, no funds, no change to consensus (classical ECDSA when this model was written,") + print(" before 2026-08-02; see the aere-node SPEC.md for today). DESIGN-level guard logic, not the bytecode.") else: print(" NOT fully established (see FAILED / unexpected CEX above).") import sys