aere-network/aere-docs
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Dated corrections (2026-10-27): AERE-PROTOCOL-SPECIFICATION section 7.5, a client built to that checklist alone does not follow chain 2800 (the consensus rules added after it was written are named); REPRODUCE.md, the dated results use the paths of the development tree, and the whole formal suite is one command from a clone of the public research repository (section 3b)

Browse Source
This commit is contained in:
Aere Network 2026-10-27 15:01:34 +02:00
parent 920828ab16
commit e102341850
2 changed files with 27 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
AERE-PROTOCOL-SPECIFICATION.md
View File

@ -694,6 +694,8 @@ This is the minimal, ordered checklist a stock Besu (or Nethermind) operator app
A client built to this checklist validates the live chain, re-executes chain-2800 blocks to byte-identical state roots, and runs the five PQC precompiles byte-for-byte. The reference second client (patched Nethermind 1.39.0) is exactly such a build and has re-validated the full chain to genesis and re-executed real blocks to identical hashes and state roots, and runs the 27/27 PQC KAT vectors identically. A client built to this checklist validates the live chain, re-executes chain-2800 blocks to byte-identical state roots, and runs the five PQC precompiles byte-for-byte. The reference second client (patched Nethermind 1.39.0) is exactly such a build and has re-validated the full chain to genesis and re-executed real blocks to identical hashes and state roots, and runs the 27/27 PQC KAT vectors identically.
> **Corrected 2026-10-27.** This checklist predates the consensus rules that chain 2800 added after it was written, and the paragraph above overstates it: a client built to this checklist alone does not validate chain 2800 from block 13,014,000, where the anchor certificate rules begin, and it also misses the native post-quantum transactions of type `0x50` (AIP-20, from block 19,900,000) and the post-quantum validator identities and later stages of AIP-22 (from block 20,836,228). Item 14 describes the scope this document was written for, not what a client of chain 2800 must implement today. The rules to add are specified in the aere-node SPEC: sections 2 and 3 (consensus and the anchor certificate), section 5.3 (type `0x50`) and section 6 (what a follower must implement). The reference second client implements them as well, so it is not a build of this checklist alone.
--- ---
## 8. Formal state-transition delta (the delta as a set of function modifications) ## 8. Formal state-transition delta (the delta as a set of function modifications)

28
REPRODUCE.md
View File

@ -288,6 +288,28 @@ match a fresh count and must not be repeated until reconciled.]
### 3b. Formal verification (z3 SMT, plus Halmos and Solidity SMTChecker) ### 3b. Formal verification (z3 SMT, plus Halmos and Solidity SMTChecker)
**Note added 2026-10-27.** The results below are dated (2026-07-19) and their commands use the paths of the development
tree, which a clone of the public repositories does not have. From a clone of the public research repository the whole
suite is one command:
```bash
pip install z3-solver
cd aere-research/formal-consensus
python run_consensus_verification.py
```
Measured on 2026-10-27 (Python 3.14.4, z3 4.16.0), exit 0:
```
models run: 37 passed: 37 (16 consensus + 11 contract + 10 application)
verdict lines: 301 PROVED 159 CEX-FOUND 0 FAILED
coverage: 37 of 37 *_smt.py files in this directory are wired into this run
RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired)
```
The runner has wired the hybrid dual-quorum and threshold models since 2026-07-20, so the sentence below that says it omits
them describes the runner of 2026-07-19.
**What it proves.** Safety-critical properties are machine-checked, not argued in prose. Each **What it proves.** Safety-critical properties are machine-checked, not argued in prose. Each
property P is proved by asserting NOT P under the exact protocol guards and showing z3 returns property P is proved by asserting NOT P under the exact protocol guards and showing z3 returns
UNSAT (no counterexample). Every proof is paired with a **negative control**: the same model with UNSAT (no counterexample). Every proof is paired with a **negative control**: the same model with
@ -341,9 +363,9 @@ only an owner-authorized feedback author can move a score, and the forwarded del
version history is append-only, every retrieval names a committed version 1..current, and a priced version history is append-only, every retrieval names a committed version 1..current, and a priced
receipt is consumed at most once), and `bitstring_status_smt` (AereBitstringStatusList: a Revocation receipt is consumed at most once), and `bitstring_status_smt` (AereBitstringStatusList: a Revocation
list's status bit is monotone / terminal so a revoked credential can never be un-revoked, the epoch list's status bit is monotone / terminal so a revoked credential can never be un-revoked, the epoch
strictly increases, and setting one bit leaves every other credential's bit unchanged). The runner strictly increases, and setting one bit leaves every other credential's bit unchanged). On 2026-07-19 the runner
still omits the hybrid dual-quorum and threshold consensus models from its list, though those `.py` still omitted the hybrid dual-quorum and threshold consensus models from its list, though those `.py`
files are present in the same directory and are run under the staging suite above. files were present in the same directory and were run under the staging suite above (wired since 2026-07-20).
```bash ```bash
cd aerenew/formal-consensus cd aerenew/formal-consensus