From e4cead319dcb09dc7f3efbc566d0aa2b7ba96953 Mon Sep 17 00:00:00 2001 From: Aere Network Date: Mon, 20 Jul 2026 01:01:36 +0300 Subject: [PATCH] Initial public release Aere Network public source. Everything here can be checked against the live chain (chain id 2800, https://rpc.aere.network). Scope note, stated up front rather than buried: consensus on chain 2800 is classical secp256k1 ECDSA QBFT. The post-quantum work in this repository is at the signature, precompile, account and transport layers. Nothing here makes the consensus post-quantum, and no document in it should be read as claiming so. --- AERE-AIP-PROCESS-AND-INDEX.md | 374 ++++++++ AERE-ARCHITECTURE-MAP.md | 104 +++ AERE-BENCHMARK-REPORT.md | 403 +++++++++ AERE-BUILD-LOOP-SUMMARY-2026-07-19.md | 80 ++ AERE-CERTORA-FORMAL-VERIFICATION.md | 821 ++++++++++++++++++ AERE-COMPUTE-MARKET-V3-SUMMARY.md | 60 ++ AERE-COMPUTE-MARKET-V3.md | 156 ++++ AERE-CROSS-CLIENT-DETERMINISM.md | 480 ++++++++++ AERE-DEPLOY-RUNBOOK-SUMMARY.md | 55 ++ AERE-EIP-COMPATIBILITY-MATRIX.md | 126 +++ AERE-ENGINEERING-SECURITY-SPEC.md | 313 +++++++ AERE-ENTROPY-BEACON-FIX.md | 125 +++ AERE-ERC7683-DESTINATION-SUMMARY.md | 59 ++ AERE-ERC7683-DESTINATION.md | 188 ++++ AERE-ERC8004-SUMMARY.md | 62 ++ AERE-ERC8004-X402-CONFORMANCE.md | 236 +++++ AERE-FAULT-INJECTION-HARNESS.md | 123 +++ AERE-FORMAL-BROADEN-REPORT.md | 115 +++ AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md | 191 ++++ AERE-FORMAL-FINAL-COVERAGE.md | 130 +++ AERE-MIGRATION-TOOLKIT.md | 103 +++ AERE-NEW-CONTRACTS-DEPLOY-RUNBOOK.md | 521 +++++++++++ AERE-NIST-VALIDATION-STATUS.md | 90 ++ AERE-POST-QUANTUM-GOVERNANCE.md | 217 +++++ AERE-PQ-AGGREGATE-SUMMARY.md | 57 ++ AERE-PQ-AGGREGATE.md | 210 +++++ AERE-PQ-FINALITY-CERTIFICATE-SUMMARY.md | 56 ++ AERE-PQ-FINALITY-CERTIFICATE.md | 285 ++++++ AERE-PQ-SCREEN-SUMMARY.md | 61 ++ AERE-PQ-SCREEN.md | 207 +++++ AERE-PROTOCOL-SPECIFICATION.md | 682 +++++++++++++++ AERE-QA-CONSOLIDATION-REPORT.md | 91 ++ AERE-QUANTUM-MIGRATION-SUMMARY.md | 62 ++ AERE-QUANTUM-MIGRATION.md | 306 +++++++ AERE-QUANTUM-SAFE-NETWORKING.md | 464 ++++++++++ AERE-REPRODUCIBLE-BUILDS.md | 495 +++++++++++ AERE-SECURITY-FIXES.md | 51 ++ AERE-SECURITY-REVIEW-NEW-CONTRACTS.md | 103 +++ AERE-SHADOW-PRODUCER-SUMMARY.md | 63 ++ AERE-SHADOW-PRODUCER.md | 302 +++++++ AERE-STARK-AIR-QUOTIENT-SUMMARY.md | 121 +++ AERE-STARK-BABYBEAR-FIELD-SUMMARY.md | 85 ++ AERE-STARK-CORE-ADVANCE-SUMMARY.md | 78 ++ AERE-STARK-DOC-CAVEAT-SWEEP.md | 190 ++++ AERE-STARK-FRI-SUMMARY.md | 76 ++ AERE-STARK-MMCS-SUMMARY.md | 97 +++ AERE-STARK-POSEIDON2-CONSTANTS-CONFIRMED.md | 77 ++ AERE-STARK-POSEIDON2-SUMMARY.md | 94 ++ ...ARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md | 65 ++ AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md | 474 ++++++++++ AERE-STARK-TRANSCRIPT-SUMMARY.md | 96 ++ AERE-STARK-VERIFIER-PORT-SPEC.md | 751 ++++++++++++++++ AERE-TLA-FORMAL-SPEC.md | 87 ++ AERE-VSM-SUMMARY.md | 61 ++ AERE-VSM.md | 250 ++++++ AERE-XMSS-AGGREGATION-CIRCUIT.md | 395 +++++++++ AERE-XMSS-CIRCUIT-CORE-SUMMARY.md | 98 +++ AIP-PQ-TX-2026-07-18.md | 386 ++++++++ LICENSE | 21 + README.md | 46 + REPRODUCE.md | 442 ++++++++++ 61 files changed, 12617 insertions(+) create mode 100644 AERE-AIP-PROCESS-AND-INDEX.md create mode 100644 AERE-ARCHITECTURE-MAP.md create mode 100644 AERE-BENCHMARK-REPORT.md create mode 100644 AERE-BUILD-LOOP-SUMMARY-2026-07-19.md create mode 100644 AERE-CERTORA-FORMAL-VERIFICATION.md create mode 100644 AERE-COMPUTE-MARKET-V3-SUMMARY.md create mode 100644 AERE-COMPUTE-MARKET-V3.md create mode 100644 AERE-CROSS-CLIENT-DETERMINISM.md create mode 100644 AERE-DEPLOY-RUNBOOK-SUMMARY.md create mode 100644 AERE-EIP-COMPATIBILITY-MATRIX.md create mode 100644 AERE-ENGINEERING-SECURITY-SPEC.md create mode 100644 AERE-ENTROPY-BEACON-FIX.md create mode 100644 AERE-ERC7683-DESTINATION-SUMMARY.md create mode 100644 AERE-ERC7683-DESTINATION.md create mode 100644 AERE-ERC8004-SUMMARY.md create mode 100644 AERE-ERC8004-X402-CONFORMANCE.md create mode 100644 AERE-FAULT-INJECTION-HARNESS.md create mode 100644 AERE-FORMAL-BROADEN-REPORT.md create mode 100644 AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md create mode 100644 AERE-FORMAL-FINAL-COVERAGE.md create mode 100644 AERE-MIGRATION-TOOLKIT.md create mode 100644 AERE-NEW-CONTRACTS-DEPLOY-RUNBOOK.md create mode 100644 AERE-NIST-VALIDATION-STATUS.md create mode 100644 AERE-POST-QUANTUM-GOVERNANCE.md create mode 100644 AERE-PQ-AGGREGATE-SUMMARY.md create mode 100644 AERE-PQ-AGGREGATE.md create mode 100644 AERE-PQ-FINALITY-CERTIFICATE-SUMMARY.md create mode 100644 AERE-PQ-FINALITY-CERTIFICATE.md create mode 100644 AERE-PQ-SCREEN-SUMMARY.md create mode 100644 AERE-PQ-SCREEN.md create mode 100644 AERE-PROTOCOL-SPECIFICATION.md create mode 100644 AERE-QA-CONSOLIDATION-REPORT.md create mode 100644 AERE-QUANTUM-MIGRATION-SUMMARY.md create mode 100644 AERE-QUANTUM-MIGRATION.md create mode 100644 AERE-QUANTUM-SAFE-NETWORKING.md create mode 100644 AERE-REPRODUCIBLE-BUILDS.md create mode 100644 AERE-SECURITY-FIXES.md create mode 100644 AERE-SECURITY-REVIEW-NEW-CONTRACTS.md create mode 100644 AERE-SHADOW-PRODUCER-SUMMARY.md create mode 100644 AERE-SHADOW-PRODUCER.md create mode 100644 AERE-STARK-AIR-QUOTIENT-SUMMARY.md create mode 100644 AERE-STARK-BABYBEAR-FIELD-SUMMARY.md create mode 100644 AERE-STARK-CORE-ADVANCE-SUMMARY.md create mode 100644 AERE-STARK-DOC-CAVEAT-SWEEP.md create mode 100644 AERE-STARK-FRI-SUMMARY.md create mode 100644 AERE-STARK-MMCS-SUMMARY.md create mode 100644 AERE-STARK-POSEIDON2-CONSTANTS-CONFIRMED.md create mode 100644 AERE-STARK-POSEIDON2-SUMMARY.md create mode 100644 AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md create mode 100644 AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC.md create mode 100644 AERE-STARK-TRANSCRIPT-SUMMARY.md create mode 100644 AERE-STARK-VERIFIER-PORT-SPEC.md create mode 100644 AERE-TLA-FORMAL-SPEC.md create mode 100644 AERE-VSM-SUMMARY.md create mode 100644 AERE-VSM.md create mode 100644 AERE-XMSS-AGGREGATION-CIRCUIT.md create mode 100644 AERE-XMSS-CIRCUIT-CORE-SUMMARY.md create mode 100644 AIP-PQ-TX-2026-07-18.md create mode 100644 LICENSE create mode 100644 README.md create mode 100644 REPRODUCE.md diff --git a/AERE-AIP-PROCESS-AND-INDEX.md b/AERE-AIP-PROCESS-AND-INDEX.md new file mode 100644 index 0000000..75eabc7 --- /dev/null +++ b/AERE-AIP-PROCESS-AND-INDEX.md @@ -0,0 +1,374 @@ +# spec-25: The Aere Improvement Proposal (AIP) Process, Index, and Design-Decision Records + +| Field | Value | +| --- | --- | +| Spec | 25 | +| Title | The Aere Improvement Proposal (AIP) Process, Index, and Design-Decision Records | +| Author | Aere Network Foundation | +| Status | For publication | +| Created | 2026-07-19 | +| Chain | Aere Network, chain ID 2800 | + +## 0. Purpose of this document + +This document does three things. + +1. It formalizes the **AIP process**: what an Aere Improvement Proposal is, the lifecycle it moves through, who may propose one, where proposals live, and how they are ratified today. +2. It publishes a **canonical index** of every AIP that currently exists in the Aere repositories, with its real number, title, status, and path. It records the real state, including the fact that the process is young and the numbering is short. +3. It drafts the **key design-decision records** for load-bearing architecture choices that are not yet captured under a numbered AIP, continuing the real existing numbering. + +The goal is a transparent, numbered, dated record of Aere's reasoning that any auditor, integrator, or automated agent can read and, if they disagree, fork. This is the same intent behind Ethereum's EIP/ERC process and Rust's RFCs. Because it is published, everything in it must be honest. + +### 0.1 Honesty note on community review (read this first) + +An AIP process is worth running from day one, even before an external technical community exists, because its first job is transparent decision documentation: a stable, plain-text home for the motivation, mechanism, on-chain proof, and honest limitations of each change. That value does not depend on anyone commenting. + +The comment and review mechanism defined below is **open**: anyone may author an AIP, raise an issue on one, or fork the record. But it must be stated plainly that Aere has essentially **no external technical community commenting yet**. The network's decentralization is thin (an effective Nakamoto coefficient of about 1, since all validators are Foundation-operated on a single client), and real external usage is thin. Public comment on AIPs becomes meaningful only as an external developer and validator community forms. + +Therefore this document, and the AIPs it indexes, contain **no fabricated community discussion**: no invented "the community debated," no fake review threads, no imagined external participants, and no comment counts. Where an AIP records a decision, it records who actually decided (today, the Foundation) and on what evidence. The review mechanism exists now; organic external comment is expected later, and will be recorded honestly when it happens, not simulated in advance. + +--- + +## 1. The process + +### 1.1 What an AIP is + +An AIP (Aere Improvement Proposal) is a design document describing a change to the Aere Network (chain ID 2800), its contracts, its consensus parameters, or its processes. An AIP records the motivation for a change, the exact mechanism, the rationale for the design, and, when the change is already live, the on-chain addresses and transactions that prove it exists. AIPs are Aere's equivalent of Ethereum's EIP/ERC process. They exist so that a reader, human or machine, can reconstruct why the chain works the way it does from a single canonical plain-text source instead of from marketing pages. + +**What belongs in an AIP:** a protocol or consensus change (block time, fee routing, precompiles); a new contract standard or interface other builders integrate against; a token-standard or account-standard convention (ARC); a process or governance change (Meta). + +**What does not belong in an AIP:** bug-fix redeploys that preserve an existing interface (tracked in the SDK address registry's deprecation notes), routine parameter tuning inside an already-ratified bound, and pure documentation. + +### 1.2 Lifecycle + +The normative lifecycle is `Draft -> Review -> Last Call -> Final`. `Living` replaces `Final` for standards that keep evolving (an index, a registry). `Withdrawn` and `Stagnant` are the off-ramps. + +| Status | Meaning | +| --- | --- | +| Draft | Well-formed, has an author, may still change substantially. | +| Review | Author has requested wider scrutiny; open questions are tracked in the AIP. | +| Last Call | A stated final-review window (default 14 days). If no blocking issue is raised, it advances. | +| Final | Accepted. For shipped work, live on chain 2800. Breaking changes after Final require a new AIP that supersedes it. | +| Living | Accepted and expected to keep being updated. | +| Withdrawn | Abandoned. Terminal; the number is retired, not reused. | +| Stagnant | Inactive in Draft or Review beyond 6 months. Revivable by any author. | + +Retro-filed AIPs (documents written after the change already shipped) enter directly at `Final` or `Living` and state in their Abstract that they backfill history. + +### 1.3 Categories and types + +Types are **Standards Track**, **Meta**, and **Informational**. Informational AIPs give guidance and do not mandate anything. A Standards Track AIP names exactly one category: + +- **Core:** consensus, block production, fee and burn accounting, precompiles, genesis and client configuration. +- **Networking:** peer-to-peer protocol and sync. +- **Interface:** contract interfaces, ABIs, RPC conventions, verification surfaces. +- **ARC** (Aere Request for Comment): application and token standards (ERC-20, ERC-4626, ERC-4337, ERC-6551 conventions as adopted on Aere). + +Meta and Informational carry no category. + +### 1.4 Roles + +- **Author.** Anyone may author an AIP. The author writes the document, drives it through the statuses, and answers review questions. +- **Editor.** Checks that an AIP is well-formed, correctly numbered and categorized, and technically coherent, and that every cited address, transaction, and number is real. The editor does not judge whether a proposal is a good idea; that is the ratifier's job. Until decentralization, the editor is the Foundation. +- **Ratifier.** The party whose approval moves an AIP to Final. Until decentralization this is the Foundation account `0x0243A4f47D44b40b65D33f20329dE20D00c6f3C3`, a single-key, Foundation-controlled account (not a deployed multisig). + +### 1.5 How to file an AIP + +1. Copy the template to `AIP-N.md`, where N is the next free integer. +2. Fill in every required section (Preamble, Abstract, Motivation, Specification, Rationale, Backwards Compatibility, Security Considerations, Reference Implementation and On-Chain Deployment, Copyright). A section that does not apply keeps its header with the body "None". +3. Cite on-chain addresses verbatim from the canonical SDK registry (`sdk-js/src/addresses.ts`). Never invent an address, transaction hash, or gas number. If a number has not been measured, write "to be measured". +4. Add a row to the index. +5. Open it for editorial review. Anyone may raise an issue against it. Until decentralization, the editor and ratifier is the Foundation. + +### 1.6 Where AIPs live + +- **Canonical scaffold:** `aerenew/aips/` holds `README.md`, `aip-template.md`, and the retro-filed records AIP-1 through AIP-7. This is the seed of a public AIP repository. +- **AIP-8** currently lives as a standalone Draft at `aerenew/docs/AIP-PQ-TX-2026-07-18.md` and has not yet been moved into the `aerenew/aips/` index. This document records that real state; consolidating it into the scaffold index is a housekeeping step. +- **Earlier publish-staging copy:** `aere-research-repo/aips/` holds AIP-1 through AIP-6 with an older governance note (it says "three validators" and describes the Foundation account as a "multisig"). It is stale relative to `aerenew/aips/`, which reflects the current reality of seven validators and a single-key Foundation account. The `aerenew/aips/` copy is authoritative where the two differ. + +### 1.7 Sourcing rules (binding on every AIP) + +- Every on-chain address is copied verbatim from the canonical SDK registry. No address is guessed. If unsure, omit it. +- Every gas figure, transaction hash, and block number is reproducible from the chain or a repo fixture. Unmeasured quantities are written as "to be measured", never invented. +- Design ceilings (for example a theoretical maximum throughput) are never presented as measured throughput. + +### 1.8 Honest governance note and the decentralization path + +Aere is not yet trustlessly governed. Today the network runs seven QBFT validators (f=2, commit quorum 5-of-7) under a single operator, on one client (Hyperledger Besu), with no external security audit and thin real usage. In that reality an AIP is not ratified by an on-chain vote of independent stakeholders. It is **Foundation-ratified**: the Foundation account is the final editor and approver. Every AIP that predates validator and client decentralization carries the label **"Foundation-ratified (pre-decentralization)"** so no reader mistakes editorial ratification for trustless governance. + +The intended migration, each step of which will be its own Meta AIP: (1) open the validator set beyond the current seven Foundation-operated validators and run a second client as a live producer; (2) introduce a public review period the Foundation cannot unilaterally shorten; (3) move ratification to stake-weighted or validator-weighted approval once an independent staker and validator base exists. Until step 3, all Standards Track AIPs carry the pre-decentralization label. The chief risk of a pre-decentralization process, that a single party can both author and ratify, is mitigated only partially today by the editor's sourcing rules and by keeping the honesty label on every proposal; it is fully mitigated only when independent ratifiers exist. This weakness is stated rather than hidden. + +--- + +## 2. Index of existing AIPs (real state) + +The numbering is contiguous from 1 to 8, with no gaps. AIP-1 through AIP-7 are ratified and live in `aerenew/aips/`. AIP-8 is a Draft in `aerenew/docs/`. No AIP numbered 9 or higher exists in any Aere repository as of this writing; the records in Section 3 below are the first drafts of AIP-9 onward. + +| AIP | Title | Type / Category | Status | Path | +| --- | --- | --- | --- | --- | +| 1 | AIP Purpose and Process | Meta | Living | `aerenew/aips/AIP-1.md` | +| 2 | Coinbase Fee-Burn Routing (37.5%) | Standards Track / Core | Final | `aerenew/aips/AIP-2.md` | +| 3 | Sub-Second Block Period (500 ms QBFT) | Standards Track / Core | Final | `aerenew/aips/AIP-3.md` | +| 4 | On-Chain Post-Quantum Signature Verification Suite | Standards Track / Interface | Final | `aerenew/aips/AIP-4.md` | +| 5 | sAERE Receipt Token and AereSink Immutable Flywheel | Standards Track / ARC | Final | `aerenew/aips/AIP-5.md` | +| 6 | ERC-4337 Passkey and Gasless Onboarding Stack | Standards Track / ARC | Final | `aerenew/aips/AIP-6.md` | +| 7 | AerePQC Hard-Fork Activation (Native PQC Precompiles and Extended EIP-2935 Lookback) | Standards Track / Core | Final | `aerenew/aips/AIP-7.md` | +| 8 | Post-Quantum-Authorized Transaction Envelope (EIP-2718 Type 0x2A) | Standards Track / Core | Draft (not live) | `aerenew/docs/AIP-PQ-TX-2026-07-18.md` | + +Notes on real state: + +- AIP-1 through AIP-7 are Foundation-ratified (pre-decentralization). AIP-2 through AIP-7 are retro-filed records of changes already live on chain 2800; AIP-1 is the process document itself. +- AIP-8 is a genuine Draft: it specifies a base-layer post-quantum transaction type that requires a coordinated Besu hard fork and is **not deployed**. It ships with a deploy-today ERC-4337 reference path (`AerePQCTxAccount.sol`) that needs no fork. +- The mechanism specification behind AIP-7 also exists as `aerenew/research/aip-draft-pqc-precompiles.md` (frontmatter `aip: TBD`, marked SHIPPED); it is the design/gas spec, canonically recorded as AIP-7. It is not a separate AIP number. +- A duplicate AIP-1 through AIP-6 set exists under `aere-research-repo/aips/`; it is an older copy and is superseded by `aerenew/aips/` where the two disagree (see 1.6). + +### 2.1 Coverage map: which section-4 decisions already have a record + +The engineering rationale in `aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md` Section 4 enumerates the load-bearing design decisions. Several already have a numbered AIP; the rest are drafted in Section 3. + +| Section 4 decision | Captured by | New record needed | +| --- | --- | --- | +| 4.1 Consensus: QBFT, not HotStuff | (none) | Yes -> AIP-9 | +| 4.2 Execution client: forked Besu with Nethermind second, not Reth | (none) | Yes -> AIP-10 | +| 4.3 Interoperability: Hyperlane-compatible plus zk light clients, not IBC | (none) | Yes -> AIP-11 | +| 4.6 Virtual machine: extend the EVM, not a new VM | (none) | Yes -> AIP-12 | +| 4.4 Post-quantum signatures: Falcon and ML-DSA together, not one lattice family | AIP-4, AIP-7 (mechanism) | Yes, as a distinct decision record -> AIP-13 | +| 4.5 Account abstraction: ERC-4337 with EIP-7702 bridge, not native AA | AIP-6 (stack) | Yes, as a distinct decision record -> AIP-14 | +| 4.7 The burn: validator-reward cut, not a base-fee burn | AIP-2 (mechanism and rationale) | No; already recorded in AIP-2 | +| PQC precompile activation | AIP-7 | No; already recorded in AIP-7 | +| In-place hybrid PQC consensus activation (R&D, not live) | (none) | Yes -> AIP-15 | +| PQ STARK-verify precompile 0x0AE8 (skeleton, not live) | (none) | Yes -> AIP-16 | + +--- + +## 3. Design-decision records drafted here (AIP-9 to AIP-16) + +These are the first drafts of the records that continue the real numbering after AIP-8. AIP-9 through AIP-14 document architecture decisions that are already live and settled, so they enter at Final as Informational records (they explain rationale for a shipped choice rather than mandate a new normative change). AIP-15 and AIP-16 document research and blocked work that is **not live on chain 2800**, so they enter at Draft. Each record is deliberately concise: context, decision, rationale, alternatives rejected, and status. The normative mechanism for a decision that also has a Standards Track AIP (AIP-13 references AIP-4/AIP-7; AIP-14 references AIP-6) stays in that AIP; the record here captures the decision framing. + +The post-quantum scope boundary holds throughout: **Aere consensus is classical secp256k1 ECDSA QBFT.** Post-quantum applies to signatures, accounts, and applications only. No record here claims post-quantum consensus. + +--- + +### AIP-9: Consensus Mechanism: QBFT, not HotStuff + +| Field | Value | +| --- | --- | +| AIP | 9 | +| Title | Consensus Mechanism: QBFT, not HotStuff | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** Aere is a settlement layer whose core promise is deterministic, single-slot finality at a sub-second cadence. It runs a small, permissioned validator set: seven validators today, with a roadmap target in the 9 to 21 range. + +**Decision.** Use QBFT, the Byzantine-fault-tolerant IBFT-family protocol as implemented in Hyperledger Besu, producing deterministic single-block finality at a target block time of about 0.5 s. At N=7, QBFT tolerates f=2 Byzantine or crashed validators with a commit quorum of 2f+1 = 5-of-7. + +**Rationale.** At Aere's validator-set size, QBFT's O(N^2) message complexity is negligible in absolute terms (a 5-of-7 quorum verify costs on the order of a few milliseconds per block, a small fraction of the 500 ms slot). Against that non-cost, QBFT gives three concrete advantages: deterministic instant single-block finality (the exact settlement guarantee the network sells), maturity and existing integration in Besu (no new-protocol implementation risk), and the fact that Aere's post-quantum consensus research, second-client work, and zk finality proofs are all built against QBFT. + +**Alternatives rejected.** HotStuff and its pipelined variants, whose linear per-round communication complexity is engineered to scale BFT to hundreds of validators. That scaling regime is one Aere does not operate in and does not plan to enter under this design, so HotStuff's headline benefit is unavailable, while adopting it would add the risk and integration cost of a protocol less battle-tested in the chosen client. + +**Honest limitation.** At N=7 the fault tolerance against node outages is real, but all validators are Foundation-operated. Decentralization, not the consensus mechanism, is the binding trust assumption. The block-period choice (500 ms) is documented separately in AIP-3. + +**Status.** Final. Live on chain 2800. + +--- + +### AIP-10: Execution Client: Forked Besu with Nethermind as the Second Client, not Reth + +| Field | Value | +| --- | --- | +| AIP | 10 | +| Title | Execution Client: Forked Besu with Nethermind as the Second Client, not Reth | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** A production chain needs a producing client and, to retire single-implementation risk, a second independent client. Aere already ships QBFT, which is Besu-specific: no off-the-shelf Geth, Reth, Erigon, or stock Nethermind produces QBFT-compatible blocks. + +**Decision.** A fork of Hyperledger Besu v26.4.0 (Java, base commit d2032017, JDK 21 toolchain) is the sole live mainnet producer. The fork adds the native post-quantum precompiles and extended EIP-2935 lookback (live since block 9,189,161, AIP-7) and the 1-Gwei base-fee floor (live since block 10,141,734). A patched Nethermind 1.39.0 (.NET) is the second, independent client. + +**Rationale.** Besu already carries QBFT and already carries the codebase into which the PQC precompile fork and base-fee changes were integrated. Nethermind was chosen as the second client specifically for implementation diversity: a different codebase in a different language (.NET versus Java), so a consensus-relevant bug in one is unlikely to exist in the other. The patched Nethermind validates the live chain, runs the five PQC precompiles byte-for-byte identically (27 of 27 NIST KAT vectors), and, on an isolated test network, produces byte-identical QBFT blocks that stock Besu accepts through full BFT validation (with a one-byte-tampered seal rejected). + +**Alternatives rejected.** Reth (Rust) as the base client: it has no notion of QBFT, so it would require building QBFT production into a client that lacks it before producing a single block; and the September 2025 Reth halt is the reference case for why depending on one producing implementation is a systemic risk. A second Besu instance instead of Nethermind: that is not client diversity, since it shares every bug with the first. + +**Honest limitation.** Cross-client production is proven on an isolated testnet (offline import and, later, live devp2p between test nodes), and a listen-only Nethermind follower has run against the live network. Nethermind is **not yet a live gossiping producer on chain 2800**. Besu remains the sole live producer; the second client is a client-diversity cross-check and fail-safe today, not a second live validator. Making Nethermind a live producer is a founder-supervised change, because a producer bug on a live chain can halt or fork it. + +**Status.** Final (as the decision and the current live topology). Live producer: Besu only. + +--- + +### AIP-11: Interoperability: Hyperlane-Compatible Messaging plus zk Light Clients, not IBC + +| Field | Value | +| --- | --- | +| AIP | 11 | +| Title | Interoperability: Hyperlane-Compatible Messaging plus zk Light Clients, not IBC | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** Aere's value proposition is that it is an ordinary EVM chain. Cross-chain interop must serve permissionless, EVM-familiar builders while also offering trust-minimized verification of a counterparty's finality. + +**Decision.** An EVM-native, Hyperlane-compatible messaging layer (a Mailbox-compatible `AereMessenger`, an interchain gas paymaster `AereIGP`), an ERC-7683 intent layer, and an Across-v3-compatible spoke pool. Alongside it, a zero-knowledge interop path: on-chain zk light clients that verify a counterparty's consensus finality (inbound Ethereum sync-committee finality, outbound Aere QBFT finality) from inside a contract, via SP1 Groth16 proofs. + +**Rationale.** IBC's design philosophy, verifying the counterparty's consensus rather than trusting a bridge committee, is the right one, and Aere adopts it directly. Aere splits the problem: for permissionless developer-familiar interop it uses the Hyperlane-compatible interfaces the EVM tooling ecosystem already speaks; for the trust-minimization that is IBC's real contribution it built the zk light clients, which capture "verify the counterparty's consensus, do not trust a relayer" without leaving the EVM world. + +**Alternatives rejected.** IBC as a protocol: it is built around Tendermint-style light clients and a non-EVM connection, channel, and packet model. Adopting it natively would import a substantial non-EVM stack and its tooling into a chain whose entire premise is that it is an ordinary EVM. + +**Honest limitation.** The Hyperlane-compatible endpoints are interface-faithful and deployed, but a live decentralized relayer and interchain-security-module network is not yet stood up (the current bridge path runs through a single Foundation signer with a relayer pending). The zk light clients are trust-minimized, not trustless, and not quantum-safe: their committed seals are classical secp256k1 and the proof wrap is Groth16 over BN254 (Shor-breakable). + +**Status.** Final (as the decision). Deployed interfaces; decentralized relayer pending. + +--- + +### AIP-12: The Virtual Machine: Extend the EVM, not a New VM + +| Field | Value | +| --- | --- | +| AIP | 12 | +| Title | The Virtual Machine: Extend the EVM, not a New VM | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** Aere differentiates on post-quantum verification, parallel execution, and extended block-hash lookback. It must add these without taxing the developer surface it depends on. + +**Decision.** Keep the EVM. Solidity, EVM bytecode, JSON-RPC, and the developer tooling are unchanged. Differentiation is added as precompiles and client-fork rules at otherwise-empty reserved addresses, not as a new instruction set or a new language, and activated by client-only forks in the same manner Ethereum activates its own hard forks. + +**Rationale.** A mature VM has years of implementation hardening, a known cost model, and an operational history; a new VM starts that clock at zero, maximizing technical and adoption risk. The EVM is the single largest smart-contract developer surface in existence, and every deviation (a nonstandard opcode, account model, or RPC) is a tax on every developer and tool. Aere's thesis is settlement, not a novel programming model, so the design keeps the tested execution environment intact and adds differentiation only at the EVM's standard extension points (precompiles at reserved addresses). Nothing about Aere's account, passkey, or post-quantum surface depends on a nonstandard EVM. + +**Alternatives rejected.** Designing a new, purpose-built VM (a new bytecode, language, or non-EVM environment) optimized around Aere's differentiators. + +**Honest limitation.** Some ambitions (base-layer parallel execution, an EVM-in-a-zkVM) must be reached inside the existing model rather than designed in from scratch. Those remain roadmap and are labeled as such. + +**Status.** Final. Live on chain 2800. + +--- + +### AIP-13: Post-Quantum Signatures: Falcon and ML-DSA Together, not a Single Lattice Family + +| Field | Value | +| --- | --- | +| AIP | 13 | +| Title | Post-Quantum Signatures: Falcon and ML-DSA Together, not a Single Lattice Family | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Requires | 4, 7 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** Aere verifies post-quantum signatures on-chain at both the contract layer (AIP-4) and, since block 9,189,161, the native precompile layer (AIP-7). A choice of scheme family is a bet on a mathematical assumption. + +**Decision.** Support multiple post-quantum signature schemes across two distinct lattice families, Falcon (Falcon-512 and Falcon-1024) and ML-DSA (Dilithium2 / ML-DSA-44), alongside hash-based schemes (SLH-DSA, XMSS, WOTS+). The live precompiles for SHAKE256, Falcon-512, Falcon-1024, ML-DSA-44, and SLH-DSA-SHA2-128s occupy the 0x0AE1 to 0x0AE5 band. + +**Rationale.** Cryptographic-risk diversification. Falcon rests on NTRU lattices; ML-DSA rests on module lattices with Fiat-Shamir-with-aborts. Supporting both means a cryptanalytic break or a standardization flaw in one lattice family does not, by itself, remove Aere's ability to verify post-quantum signatures: accounts and settlement authorization can migrate to the surviving family. This mirrors the hybrid `AereHybridAuth` account, which requires both a classical ECDSA and a Falcon-512 signature so that neither a broken curve nor a broken lattice alone suffices to forge. + +**Alternatives rejected.** Standardizing on a single lattice scheme (ML-DSA alone as the NIST primary, or Falcon alone for its compact signatures). The cost of supporting several schemes is more verifier surface to implement, validate, and eventually audit; that cost is accepted deliberately rather than betting the network's post-quantum future on a single assumption. + +**Scope boundary (binding).** This is post-quantum at the signature, account, and application layer only. Consensus remains classical (validators sign secp256k1 QBFT), and the zk verification is classical (BN254 Groth16, Shor-breakable). Aere never claims post-quantum consensus. + +**Honest limitation.** The verifiers and precompiles carry an internal self-audit only; an external audit is pending before they should secure material value. Their assurance today rests on bit-for-bit agreement with official NIST KAT and ACVP vectors and cross-checks against independent reimplementations. + +**Status.** Final. Precompiles live on chain 2800; the normative mechanism is in AIP-4 (contract suite) and AIP-7 (precompile activation). + +--- + +### AIP-14: Account Abstraction: ERC-4337 with EIP-7702 Bridge, not Native AA + +| Field | Value | +| --- | --- | +| AIP | 14 | +| Title | Account Abstraction: ERC-4337 with EIP-7702 Bridge, not Native AA | +| Author | Aere Network Foundation | +| Type | Informational | +| Status | Final | +| Created | 2026-07-19 | +| Requires | 6 | +| Ratification | Foundation-ratified (pre-decentralization) | + +**Context.** Aere wants programmable accounts (recovery, passkey ownership, post-quantum ownership, gas sponsorship) without breaking EVM and EOA compatibility. + +**Decision.** ERC-4337 (v0.7) smart accounts as the account-abstraction path, with EIP-7702 (live under the Pectra ruleset) as the migration bridge that lets existing externally-owned accounts (EOAs) delegate to smart-account code. + +**Rationale.** ERC-4337 needs no consensus change, is an established standard with an existing bundler and tooling ecosystem, and delivers programmable accounts (including the Falcon-owned post-quantum smart account `AerePQCAccountFactory`) without touching the protocol, preserving exact EVM and Ethereum compatibility. EIP-7702 is the chosen bridge precisely because it upgrades existing EOAs in place without forcing a disruptive "everything is a contract" change. + +**Alternatives rejected.** Native, protocol-level account abstraction up to an "all accounts are smart accounts by default" end-state: it changes what an account fundamentally is, breaking existing tooling, contracts, and user keys. EIP-3074, an earlier EOA-empowerment proposal: it was superseded by EIP-7702, which is the mechanism Aere carries; Aere does not implement EIP-3074. + +**Honest limitation.** The EntryPoints are Aere's own ERC-4337-compatible implementations, compatible in shape and interface but not byte-identical to Ethereum's canonical audited singleton; integrators should treat them as Aere-specific. Gasless onboarding is subsidized (Foundation-funded, rate-limited), not free. These contracts have not had an external audit. + +**Status.** Final. Live on chain 2800; the normative stack (accounts, factories, paymasters, EntryPoints) is in AIP-6. + +--- + +### AIP-15: In-Place Hybrid PQC Consensus Activation via On-Chain Anchor Contract, not Re-Genesis + +| Field | Value | +| --- | --- | +| AIP | 15 | +| Title | In-Place Hybrid PQC Consensus Activation via On-Chain Anchor Contract, not Re-Genesis | +| Author | Aere Network Foundation | +| Type | Standards Track | +| Category | Core | +| Status | Draft (isolated-testnet R&D; not live on chain 2800) | +| Created | 2026-07-19 | +| Ratification | Not ratified; external-audit and founder gated | + +**Context.** Aere's hybrid consensus research (Stage 1 and Stage 2) proved a gossiped, blocking Falcon-512 quorum certificate that runs alongside the ECDSA committed-seal quorum, empirically at N=4 (2 s) and N=7 (0.5 s). Its Falcon registry, however, was bound to chain identity at genesis (folding `keccak256(manifest)` into the genesis state root). Chain 2800 launched long before any Falcon manifest existed, so blocking activation was previously recorded as "requires a re-genesis," a non-starter for a live chain because re-genesis destroys history and chain identity. + +**Decision.** Bind the Falcon manifest to on-chain state **post-genesis**, via a minimal, immutable, ownerless anchor contract deployed by one ordinary transaction at an activation height. The contract commits `keccak256(manifest)` to storage slot 0 (its runtime code is a single STOP byte; it is never callable and has no admin). On every block import the validation rule resolves the manifest from the **parent block's world state** at the anchor address and activates the pending registry only if the observed hash matches, failing closed on any mismatch. The re-genesis requirement is removed. + +**Rationale.** The late anchor folds `keccak256(manifest)` into every block hash from the deployment block onward, so two nodes that agree on the chain past that block necessarily agree on the anchored hash: the same integrity guarantee the genesis ceremony gave, minus the re-genesis. The deploy address is deterministic (`keccak256(rlp[deployer, nonce])[12:]`), so validators can be pre-configured before deployment, and activation is idempotent and retried each block, so deploy-then-configure and configure-then-deploy both converge. + +**Alternatives rejected.** Re-genesis carrying a Falcon anchor in genesis alloc (destroys history and chain identity). A shared per-node manifest file with no on-chain root (a node with a tampered manifest could join silently; the on-chain anchor makes it fail closed instead). + +**Evidence and honest scope.** Proven end-to-end on an **isolated N=4 @ 0.5 s testnet** (chainId 440855) whose genesis is byte-shape-identical to a classical ECDSA-only chain: classical start, deploy anchor at block 16, activate from the contract at block 17, flip to blocking at fork block 150, with 0 forks, 0.5 s cadence maintained, pre-activation blocks still valid, a post-activation sub-quorum block rejected (chain halts), and recovery in place with no re-genesis. **Nothing here is live on chain 2800.** Chain 2800 consensus remains classical secp256k1 ECDSA QBFT at N=7, with no Falcon layer of any kind in its headers. The hybrid can only shrink the committable set, so it is never worse than the ECDSA-only chain; ECDSA committed seals remain the decisive safety and liveness seal. + +**Remaining gates to a live flip.** No longer a gate: re-genesis. Still required: an external audit of the Falcon consensus patch (quorum, gossip, assembly, late-anchor Java) and of BouncyCastle Falcon-512 on the consensus path; finalizing the full target validator set (N >= 9 recommended, since N=7 blocking has a zero two-fault margin) with an address-bound manifest re-anchored for the full set; a live isolated N=7 (ideally N=9) soak of the combined activation; and an explicit founder GO. No agent activates blocking consensus on chain 2800. + +**Status.** Draft. Reference patch: `aerenew/consensus-pqc/besu-consensus-pqc-fork-activation.patch` with evidence under `aerenew/consensus-pqc/inplace-activation-evidence/`. + +--- + +### AIP-16: PQ STARK-Verify Precompile (0x0AE8) + +| Field | Value | +| --- | --- | +| AIP | 16 | +| Title | PQ STARK-Verify Precompile (0x0AE8) | +| Author | Aere Network Foundation | +| Type | Standards Track | +| Category | Core | +| Status | Draft (reference skeleton; verifies nothing; not live on any Aere network) | +| Created | 2026-07-19 | +| Ratification | Not ratified; prerequisite-gated, external-audit gated, founder gated | + +**Context.** Aere's zk interop and validity paths currently wrap proofs as Groth16 over BN254, which is classical and Shor-breakable. A post-quantum-sound proof system (a FRI-based STARK, hash-commitment only, no pairing) would remove that assumption. A native precompile is the natural home for STARK verification, matching the same reasoning used for the PQC signature precompiles in AIP-7. + +**Decision.** Reserve precompile address 0x0AE8 for a PQ STARK-verify precompile that verifies a hash-based STARK directly on-chain (removing a BN254 pairing check). It is specified to activate under a new, forward-dated milestone (PQ-3), never folded into an already-crossed milestone, so that pre-activation history is byte-identical on old and new binaries and the upgrade itself carries no fork risk. + +**Scope caveat (2026-07-19 research finding).** An earlier draft described this as verifying "an SP1 inner-STARK (FRI over a Poseidon2 commitment)". That is corrected: the verifier skeleton built so far is a BabyBear + FRI STARK verifier, conformance-confirmed against Plonky3 `0.4.3-succinct`, which targets Aere's OWN Plonky3 circuits, NOT SP1 6.1.0. The pinned SP1 6.1.0 is a Hypercube release (KoalaBear multilinear: BaseFold plus sumcheck-zerocheck plus LogUp-GKR), so FRI does not apply to it and this skeleton does not verify SP1 6.1.0 proofs; retargeting 0x0AE8 to the SP1 Hypercube stack is a separate ~22 to 32 person-week effort. See `AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`. + +**Rationale.** A forward-dated, non-retroactive milestone plus a rolling binary upgrade (the same zero-liveness-risk posture proven for the base-fee floor and the in-place activation) means the address stays an empty account, and every consumer adapter fails closed, until the announced activation time. A migrated consumer can keep both the new 0x0AE8 path and the existing BN254 gateway required during a defense-in-depth window before dropping the classical path. + +**Alternatives rejected.** Folding 0x0AE8 into the crossed `futureEipsTime` milestone (block 9,189,161): every historical block that called the currently-empty address would re-execute with different return data on the upgraded binary, a state divergence and a consensus split. Presenting the current artifact as a working verifier: it is not one. + +**Honest scope (critical).** This is the record's load-bearing honesty statement. **0x0AE8 is not activated on any Aere network. As of this date it is a reference skeleton that fail-closes (returns EMPTY for every input): it is not a working verifier and must not be presented as one.** Mainnet 2800 has exactly five PQC precompiles (0x0AE1 to 0x0AE5, block 9,189,161). The sibling ML-KEM-768 (0x0AE6) and Falcon HashToPoint (0x0AE7) precompiles are testnet-only. `AerePQStarkVerifier.sol` is a fail-closed adapter that denies every proof (safe by construction). Consensus is untouched by all of this; it remains classical ECDSA QBFT. + +**Prerequisite and gates.** Activation cannot begin until the crypto core is ported from maintained references (Plonky3 FRI/Poseidon2/uni-stark, SP1 stark) or a pinned native wrap is built and reproducible; a real SP1 v6.1.0 inner-STARK vector corpus exists and the precompile accepts every valid vector and rejects every tampered or wrong-public-values vector, including cross-agreement with the live BN254 gateway; a soundcalc receipt for the exact pinned FriConfig is recorded (no 128-bit claim without the receipt); and a benchmark confirms a real verify fits under the EIP-7825 2^24 per-transaction gas cap. Beyond the prerequisite: a specialist external STARK/FRI audit of the consensus-critical crypto, a conformance gate green on the frozen artifact, an isolated N=7 soak across a simulated milestone crossing, and an explicit founder GO. Until all hold, 0x0AE8 stays a skeleton. + +**Status.** Draft (blocked on the prerequisite crypto-core port). References: `aerenew/docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md` (design), `aerenew/docs/PQ-STARK-VERIFIER-ACTIVATION-2026-07-18.md` (gated activation plan), `aerenew/contracts/contracts/zkverify/AerePQStarkVerifier.sol` (fail-closed adapter). + +--- + +## 4. Copyright + +Released to the public domain (CC0). No rights reserved. diff --git a/AERE-ARCHITECTURE-MAP.md b/AERE-ARCHITECTURE-MAP.md new file mode 100644 index 0000000..ab20380 --- /dev/null +++ b/AERE-ARCHITECTURE-MAP.md @@ -0,0 +1,104 @@ +# Aere Network Architecture Map + +Aere Network is a public, EVM-compatible Layer 1 (chain ID 2800). One diagram replaces pages of prose here: the architecture is best read as a layered stack (Consensus at the bottom, then Execution, Accounts, and Applications on top) with a set of cross-cutting concerns (post-quantum cryptography, zero-knowledge verification, and crypto-agility) that traverse every layer rather than sitting in any single one. This is deliberately not one linear top-to-bottom column: the layers stack, and the transversal concerns cut across all of them. + +The single most important honesty point, stated up front: consensus today is classical ECDSA (secp256k1) QBFT. Only signatures, accounts, and precompiles are post-quantum. There is no post-quantum consensus live on mainnet, and the on-chain zero-knowledge verifiers are classical BN254 (Shor-breakable) today. Everything below is marked LIVE (on mainnet 2800) or "(roadmap)" (built and tested, but not activated on mainnet). + +## Diagram + +```mermaid +flowchart TB + classDef live fill:#e7f6ec,stroke:#1a7f37,color:#0b2b16; + classDef road fill:#fff3e0,stroke:#b26a00,color:#3d2600,stroke-dasharray:5 3; + classDef cross fill:#eaeefb,stroke:#3b46c4,color:#1a1f5c; + + legend["Legend. Green solid, LIVE on mainnet 2800. Orange dashed, roadmap (built and tested, not yet live). Blue, cross-cutting concern. Suffix (roadmap) also marks any not-yet-live item inside a label."]:::cross + + subgraph APP["Applications layer"] + direction TB + app_defi["DeFi. lending, sAERE staking, AereSink burn"]:::live + app_settle["Settlement. SettlementHub, state channels, AERE402 machine payments"]:::live + app_bridge_l["Bridge and interop. Hyperlane-compatible bus, zk light clients inbound and outbound"]:::live + app_bridge_r["ERC-7683 intent settlement route (roadmap)"]:::road + app_id_l["Identity and compliance. ZKScreen, compliant privacy pool, AereProof registry"]:::live + app_id_r["zk-KYC and over-18 attribute proofs (roadmap)"]:::road + app_ai_l["AI agents. AgentDID, AIReputation, agent bond, InferNet audit log"]:::live + app_ai_r["AI runtime and zk proof of inference (roadmap)"]:::road + end + + subgraph ACC["Accounts layer"] + direction TB + acc_eoa["EOA"]:::live + acc_pk["WebAuthn P-256 passkey accounts"]:::live + acc_4337["ERC-4337 v0.7 smart accounts"]:::live + acc_7702["EIP-7702 EOA delegation"]:::live + acc_falcon["Falcon-512 and hybrid ECDSA plus Falcon accounts"]:::live + acc_thr["t-of-n PQC threshold accounts"]:::live + acc_note["Note. flawed originals superseded, some V2 redeploys founder-gated"]:::cross + end + + subgraph EXE["Execution layer"] + direction TB + exe_evm["EVM. Pectra plus Fusaka parity"]:::live + exe_pqc["PQC precompiles 0x0AE1 to 0x0AE5"]:::live + exe_pqc2["PQC precompiles ML-KEM-768 and HashToPoint, 0x0AE6 to 0x0AE7 (roadmap)"]:::road + exe_stm["Parallel execution, Block-STM (roadmap)"]:::road + exe_zk["zk validity rollup, revm in SP1 (roadmap)"]:::road + end + + subgraph CON["Consensus layer"] + direction TB + con_qbft["QBFT, classical ECDSA secp256k1"]:::live + con_besu["Hyperledger Besu producer, N equals 7"]:::live + con_fin["about 0.5s deterministic finality"]:::live + con_nm["Nethermind 2nd client, validate and follow"]:::live + con_nmp["Nethermind live block producer (roadmap)"]:::road + end + + subgraph XC["Cross-cutting concerns, span all layers"] + direction TB + x_pqc["PQC. precompiles, accounts, signatures LIVE. Consensus PQC (roadmap)"]:::cross + x_zk["ZK verify. on-chain BN254 Groth16 via SP1, Halo2, RISC Zero, all classical LIVE. PQ STARK verifier (roadmap)"]:::cross + x_agile["Crypto-agility. schemes addressable and swappable by the calling contract"]:::cross + end + + APP -->|builds on| ACC + ACC -->|builds on| EXE + EXE -->|builds on| CON + + XC -.spans.-> APP + XC -.spans.-> ACC + XC -.spans.-> EXE + XC -.spans.-> CON +``` + +## Layer-by-layer map + +### Consensus (LIVE) +Aere Network runs QBFT (Istanbul BFT family) with a Hyperledger Besu block producer, signing blocks with classical ECDSA over secp256k1. The live validator set is N=7 (f=2, commit quorum 5 of 7), all Foundation-operated, at a 500 ms target block period with sub-second deterministic finality. A second execution client, a patched Nethermind 1.39.0, is LIVE as a client-diversity cross-check: it peers with the Besu validators over devp2p and independently validates and follows the live chain (verification-layer diversity). Nethermind producing live QBFT blocks is roadmap: block production and adversarial recovery are proven on isolated testnets and via offline import (Besu imports Nethermind-sealed blocks byte-for-byte), but it is not yet a live producing validator on mainnet. Consensus is classical today, not post-quantum. + +### Execution (LIVE base, frontier roadmap) +The EVM is at Pectra plus Fusaka parity with Ethereum mainnet (Prague/Cancun activated at block 2,075,363; Osaka at block 2,106,606), including EIP-7702, EIP-2537 BLS12-381, EIP-2935 historical block hashes, transient storage, and the RIP-7951 P-256 precompile at 0x100. Five native post-quantum precompiles are LIVE on mainnet since block 9,189,161 (Falcon-512, Falcon-1024, ML-DSA-44, SLH-DSA-128s, SHAKE256 at 0x0AE1 through 0x0AE5), NIST KAT-validated on-chain. Roadmap execution items, all built and tested but not activated on mainnet: two further precompiles (ML-KEM-768 at 0x0AE6 and Falcon HashToPoint at 0x0AE7, KAT-verified on isolated testnet); parallel execution via a Block-STM engine (correctness proven bit-identical to sequential, near-linear execution-phase scaling, but no end-to-end throughput win claimed and not enabled on L1); and a full-EVM zk validity rollup (revm in the SP1 zkVM), which is verified on-chain as a proof-of-approach on small real blocks, not yet a production-throughput rollup. + +### Accounts (LIVE, some V2 redeploys founder-gated) +Aere supports the full modern account spectrum: plain EOAs; WebAuthn / P-256 passkey accounts (backed by the native 0x100 precompile); ERC-4337 v0.7 smart accounts (AereEntryPointV2 live); EIP-7702 EOA delegation; a Falcon-512 post-quantum account whose sole owner is a Falcon public key; hybrid ECDSA plus Falcon authorization; and non-custodial t-of-n post-quantum threshold accounts (AereThresholdAccountFactory V2 live on mainnet, each committee leg verified by the live PQC precompiles). Honest caveat: several first-generation account contracts had audited defects and were superseded by fixed V2 redeploys that hold zero value; some corrected factories are deployed inert and the live migration of any funds-bearing path is founder-gated. + +### Applications (mixed LIVE and roadmap) +- DeFi (LIVE): an isolated-market lending engine (AereLendingMarket, proven end-to-end with real supply/borrow/repay), the sAERE staking-receipt vault, and the immutable AereSink burn-and-buyback router. Note that sAERE has a corrected V2 whose migration is founder-gated. +- Settlement (LIVE): AereSettlementHub, AereStateChannels (24h challenge window), and AERE402 machine-to-machine payments (AereAgentV2 plus AERE402FacilitatorV2). The settlement hub is deployed in a bootstrap state holding no value pending a founder-supervised migration. +- Bridge and interop: Hyperlane-compatible message bus (AereMessenger) is LIVE, as are the inbound zk Ethereum light client and the outbound zk QBFT-finality light client (both proven live end-to-end, trust-minimized, classical BN254). ERC-7683 intent settlement (SpokePool path) is roadmap: the corrected contracts exist but are deployed inert, so no live intent route is enrolled. +- Identity and compliance: ZKScreen v3 sanctions screening is LIVE, as is a compliant, sanctions-gated privacy pool (deposit/withdraw circuit proofs are still being generated) and the AereProof proof-anchoring registry. zk-KYC and the over-18 attribute proof are roadmap (proofs generated, pending a Foundation registration signature). +- AI agents: AgentDID (Falcon-rooted decentralized identity), AIReputation, the slashable agent bond, and the InferNet inference-audit-log commitments (EU AI Act style) are LIVE. A general AI runtime and a zero-knowledge proof-of-inference (zkML) verifier are roadmap. + +### Cross-cutting: PQC (transversal) +Post-quantum cryptography is not a layer, it runs through the stack. LIVE: the execution-layer PQC precompiles, the PQC accounts, and application-layer PQC signature verification (for example AerePQCAttestation, proven usable end-to-end on mainnet). Roadmap: post-quantum consensus. A hybrid ECDSA plus Falcon dual-quorum design, an on-chain Falcon registry, and in-place activation without re-genesis are all proven on isolated testnets and formally analyzed as no-worse-than-ECDSA, but they are not activated on mainnet and remain audit-plus-founder gated. Consensus stays classical ECDSA QBFT today. + +### Cross-cutting: ZK verification (transversal) +Aere exposes a multi-prover verification surface. The on-chain verifiers that are LIVE today are all classical BN254: the SP1 Groth16 gateway, a Halo2 PLONK-over-BN254 (KZG) verifier, and a RISC Zero Groth16 verifier. These underpin ZKScreen, the privacy pool, the zk light clients, and the zk validity rollup anchors. Because BN254 pairings are Shor-breakable, this surface is not post-quantum. A post-quantum STARK verifier is roadmap. Scope caveat (2026-07-19 finding): the 0x0AE8 verifier skeleton built so far is a BabyBear + FRI STARK verifier, conformance-confirmed against Plonky3 and targeting Aere's OWN circuits; it does NOT yet verify SP1 6.1.0 proofs, because the pinned SP1 6.1.0 is a Hypercube (KoalaBear multilinear) system, a different stack. Replacing the SP1 BN254 Groth16 path is a separate ~22 to 32 person-week retarget (`AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`), not done or imminent. + +### Cross-cutting: crypto-agility (transversal) +Signature and proof schemes are addressable and swappable by the calling contract rather than hard-wired. AereCryptoRegistry (live) maps scheme identifiers to concrete precompiles or verifiers, with additional reserved scheme slots and a governance rotation runbook, so applications can migrate primitives (for example add or rotate a PQC scheme) without redesigning the stack. + +--- + +Convention recap: plain / green means LIVE on mainnet chain 2800; "(roadmap)" / orange dashed means built and tested but not yet activated on mainnet. Consensus is classical ECDSA QBFT; PQC is signatures, accounts, and precompiles only; on-chain ZK verifiers are classical BN254. diff --git a/AERE-BENCHMARK-REPORT.md b/AERE-BENCHMARK-REPORT.md new file mode 100644 index 0000000..155546b --- /dev/null +++ b/AERE-BENCHMARK-REPORT.md @@ -0,0 +1,403 @@ +# Aere Network: Reproducible Benchmark Report (spec-18) + +**Status date:** 2026-07-19 +**Chain:** Aere Network mainnet, chain ID 2800 (Hyperledger Besu QBFT). +**Scope:** chain performance, zkVM proof-verification economics, and post-quantum +cryptographic-operation gas, stated with a hard separation between what is +freshly measured, what is cited from a committed repo artifact, and what still +needs a measurement command run. + +## The absolute rule this report obeys + +No performance number (TPS, latency, gas, proof size, proving time) appears here +unless it was either (a) freshly measured by running a command this session, or +(b) found in a committed repo artifact that is cited by path. Anything that +cannot be measured or sourced is written as a measurement command and marked +`[MEASURE]`. Anything sourceable only from memory and not yet confirmed against +code is marked `[VERIFY]`. A fabricated benchmark would be a catastrophic +failure of this document, so the labels below are load-bearing, not decoration. + +### Label legend + +| Label | Meaning | +|---|---| +| `[MEASURED-FRESH]` | Run by this report on this machine, output shown or summarized. | +| `[CITED: path]` | Value read from a committed repo artifact at the cited path. | +| `[MEASURE: cmd]` | Not measured here. The command that would measure it is given. | +| `[VERIFY: note]` | Sourceable but needs confirmation against live code or a live node. | + +### Scope boundary that never moves + +Aere Network validators sign classical secp256k1 QBFT consensus messages. +Nothing in this report makes Aere consensus post-quantum. The post-quantum work +is an application and account layer capability. Any claim of post-quantum +consensus would be false and is not made here. + +--- + +## PART A: CHAIN PERFORMANCE + +### A.0 The one honesty point, stated first + +The "273,000 TPS" figure is an ARCHITECTURAL CEILING derived from block-space +arithmetic under ideal conditions. It is NOT the live mainnet transaction rate, +it has never been a measured result, and it is not asserted as one. Three +distinct quantities must never be conflated: + +| Quantity | Value | Label | +|---|---|---| +| Architectural ceiling (design maximum) | ~273,000 TPS | `[CITED]`, explicitly labeled a ceiling | +| Testnet-measured L1 throughput | none exists | see A.1 | +| Live-mainnet-observed throughput | far below the ceiling, demand-limited | see A.1 | + +`[CITED: aerenew/docs/WHITEPAPER-V2.md lines 73, 117, 633; aerenew/docs/wp2-sections/01-overview.md:59; 02-architecture.md:21; 09-governance-roadmap.md:294]` +The whitepaper states it verbatim: the block parameters "admit a design ceiling +on the order of 273,000 transactions per second; this is a theoretical maximum +implied by the gas and block configuration, not a measured or sustained figure, +and realized throughput on the live network is a small fraction of it." It is +described as "a design ceiling derived from block-space arithmetic under ideal +conditions" that "has never been a measured result." + +**On the derivation itself.** The repo labels 273,000 as a block-space-arithmetic +ceiling but does not publish the explicit factors. The two facts that are +sourceable: + +- Block period 0.5 s. `[CITED: aerenew/docs/wp2-sections/02-architecture.md:19; genesis-subsecond.json (blockperiodmilliseconds: 500)]` +- Genesis block gas limit is ambiguous across genesis artifacts: `0x2625a00` + (40,000,000) in `aerenew/genesis.json`, versus `0x1fffffffffffff` + (9,007,199,254,740,991, effectively unbounded) in `aere-genesis-current.json` + and `genesis-subsecond.json`. `[VERIFY: which gas limit is live on 2800]` + +Implied arithmetic (transparent, not a new claim): 273,000 TPS at a 0.5 s block +is 136,500 tx per block, and at the 21,000-gas simple-transfer floor that is +about 2.87 billion gas per block. That is far above the 40M limit and far below +the effectively-unbounded limit, so the ceiling presumes an effectively- +unbounded block gas limit AND the cheapest possible transaction, not the +EIP-7825-capped realistic workload the chain actually runs. `[VERIFY: publish the +explicit block-space arithmetic behind 273,000 so the ceiling is reproducible]` + +### A.1 Testnet-measured and live-observed throughput (the honest gap) + +**There is no testnet measurement that validates 273,000 TPS for L1.** The +closest measured throughput number in the repo is a rollup-executor +microbenchmark, and the artifact that produces it says plainly it neither +reaches nor implies the ceiling. + +`[CITED: aerenew/parallel-executor/BLOCKSTM-ENDTOEND-THROUGHPUT-2026-07-13.md section 7]` +The Block-STM end-to-end harness measured about 247,000 to 270,000 TPS at +`gas=80` on a 16-vCPU box, but this is (a) the rollup executor with a light +commit proxy, not L1, not a real Merkle Patricia Trie, and (b) entirely a +function of the assumed per-transaction cost: the same box reports 115,000 to +500,000 TPS as the per-transaction weight changes. The `gas=80` proximity to +273,000 is called out in the artifact as a coincidence, not a validation. + +**Live mainnet 2800 runs far below the ceiling, and this is by demand, not by +capacity.** `[CITED: aerenew/research/specs/spec-zk-stack.md section 0.2; aerenew/docs/wp2-sections/01-overview.md:59]` +On-chain usage is thin (single-digit proof records for most verifiers; six +genesis user wallets per project memory). Real throughput is demand-limited, not +capacity-limited: the chain has ample block-space headroom and almost no load to +fill it. `[MEASURE: sample a live window with eth_getBlockByNumber over N recent +blocks against https://rpc.aere.network and divide total tx by elapsed time to +publish an observed sustained TPS; expected result is near zero on an idle chain]` + +### A.2 Block time and finality + +Deterministic single-slot QBFT finality at a 0.5 s block period. Because QBFT +finalizes on commit rather than by accumulation of work, a transaction is +irreversible in well under a second from inclusion, with no confirmation count +and no reorg. `[CITED: aerenew/docs/wp2-sections/02-architecture.md:19]` + +The 0.5 s period was reached by a mid-chain QBFT parameter change at block +2,138,451, halved from the launch value of one second, with no re-genesis. +`[CITED: aerenew/docs/wp2-sections/01-overview.md:59; aerenew/docs/WHITEPAPER-V2.md:73; genesis-subsecond.json (blockperiodseconds: 0, blockperiodmilliseconds: 500)]` + +Finality is a latency-to-irreversibility claim and is separate from throughput. +The 0.5 s finality claim follows mechanically from QBFT plus the block period; it +says nothing about TPS. + +### A.3 Parallel execution (Block-STM): the honest result + +The honest result has three parts, and only the first is a mainnet-relevant +guarantee. No end-to-end L1 throughput win is claimed, and Block-STM is NOT +enabled on L1. + +**(1) Correctness proven bit-identical to sequential.** `[MEASURED-FRESH]` This +session ran the executor's `bench` on this Windows dev machine. The +`parallel==sequential` gate (committed state and keccak state root identical to +the sequential oracle) passed on all four conflict profiles: + +``` +LOW-CONFLICT parallel==sequential check: PASS +MEDIUM-CONFLICT parallel==sequential check: PASS +HIGH-CONFLICT parallel==sequential check: PASS +PATHOLOGICAL parallel==sequential check: PASS +``` + +This corroborates the cited larger runs: a 6,000-comparison correctness harness +with 0 mismatches, and a re-import plus validation of 253 real exported blocks +with zero state-root mismatch. `[CITED: aerenew/parallel-executor/BLOCKSTM-ENDTOEND-THROUGHPUT-2026-07-13.md section 3 and section 8]` + +**(2) Near-linear execution-phase scaling on parallelizable workloads.** +`[MEASURED-FRESH]` on this machine (fewer physical cores than the reference +16-core Linux box, so absolute speedup is lower, which is expected and honest): + +| Workload (this box, 16 threads) | speedup vs sequential | abort% | +|---|--:|--:| +| Low-conflict (~2%) | 4.36x | 0.3% | +| Medium-conflict (~15%) | 4.96x | 2.3% | +| High-conflict (single hot counter) | 1.92x | 24.8% | +| Pathological (all same slot) | 0.43x (correctly slower) | 11.5% | + +`[CITED: same artifact, section 4-5]` The reference 16-core Linux box measured +about 8.3x to 9.4x execution-phase and about 8.3x to 9.1x end-to-end on realistic +0 to 50 percent conflict. The pathological all-same-slot profile is honestly +slower than sequential (correct Block-STM behavior), on both boxes. + +**(3) No end-to-end throughput win claimed, and not on L1.** +`[CITED: aerenew/research/specs/spec-parallel-execution.md section 9; BLOCKSTM-ENDTOEND section 7-8]` +The Aere L1 mainnet executes sequentially on Besu. The parallel executor is a +bounded four-kind VM (Transfer, Sweep, Increment, AmmSwap) over a balance and +storage map, not a full EVM, and its measured speedups are single-machine +microbenchmarks, not a network throughput or TPS claim. The real forked client's +commit path was separately measured to anti-scale (parallel commit was slower +than sequential), so the real-client end-to-end ceiling is tighter than the Rust +harness, not looser. The invariant deliverable is the correctness gate plus the +speedup curve and its Amdahl bound, not an absolute TPS. + +--- + +## PART B: ZKVM COMPARATIVE (SP1 vs RISC Zero vs Halo2) + +Every cell is labeled. Gas and proof-size values that are cited come from repo +deployment artifacts and are measured single-run values, not benchmarked +averages (the source spec states this explicitly). `[CITED: aerenew/research/specs/spec-zk-stack.md footer]` + +### B.1 Comparison table + +| Prover (version) | Proving time (off-chain) | On-chain gas to verify | Proof size | Verification latency | +|---|---|---|---|---| +| SP1 Groth16 (v6.1.0) | app-dependent, CITED single-runs: zkscreen ~72 to 75 s, over18 ~71 to 73 s, zkml-mnist ~200 to 205 s, aggregation Groth16 526.1 s `[CITED: contracts/deployments/proof-aggregator-scale.json]` | ~300k typical `[CITED: spec-zk-stack section 2]`; measured records: storage-proof 348,345, zkML 326,492, aggregation ~390k flat `[CITED: proof-aggregator-scale.json, zkml/storage-proof artifacts]` | ~260 to 356 bytes `[CITED: spec-zk-stack section 2]` | one staticcall, final at next block (~0.5 s) `[MEASURE: time eth_call wall-clock]` | +| SP1 Plonk (v6.1.0) | `[MEASURE: prove a fixture with the Plonk prover]` | "somewhat higher than Groth16" `[CITED: spec-zk-stack section 2]`, exact `[MEASURE]` | `[MEASURE]` | one staticcall `[MEASURE]` | +| RISC Zero Groth16 (5.0.0-rc.1) | `[MEASURE: r0vm prove the factor-guest]`, not recorded in repo | `[MEASURE: eth_call gas on RiscZeroVerifierRouter.verify]`, no gas number committed | seal 260 bytes `[CITED: contracts/deployments/risc0-verifier-fix.json sealLen]` | one staticcall `[MEASURE]` | +| Halo2 (bn254 / KZG, SHPLONK) | `[MEASURE: halo2 prover on the cubic circuit]` | ~449,517 gas `[CITED: contracts/deployments/halo2-cubic.json; spec-zk-stack section 6]` (revm gas ~300,144) | 1,152 bytes `[CITED: same]` | one call `[MEASURE]` | +| KZG / EIP-4844 point-eval precompile (0x0A) | n/a (precompile, no prover) | ~255,719 gas `[CITED: contracts/deployments/kzg-verifier.json; spec-zk-stack section 5]` | 192-byte precompile input `[CITED: same]` | one staticcall | + +Notes on the two recursion facts worth keeping, both `[CITED: proof-aggregator-scale.json; spec-zk-stack section 7]`: +- A 10-proof recursive SP1 aggregation records on-chain in ~393,844 gas, roughly + flat versus the 3-proof fold (~387,858 gas). Constant on-chain verification cost + regardless of fold count is the point of recursion. +- The proving side of that same 10-fold cost 526.1 s for the aggregation Groth16 + plus 988 s of inner proving (measured, off-chain, single run). + +### B.2 Routing logic (which prover for which job, and why) + +`[CITED: aerenew/research/specs/spec-zk-stack.md sections 1-3, 7-11]` Routing is +by selector: the first 4 bytes of the proof pick the concrete verifier. + +- `SP1VerifierGateway` routes SP1 proofs by leading selector (Groth16 route + `0x4388a21c`, Plonk `0x5a093a2f`). +- `RiscZeroVerifierRouter` routes a RISC Zero seal by leading selector + (`0xef6cb709` for 5.0.0-rc.1). + +Which prover is chosen: + +- **SP1 is the workhorse.** Every Aere application circuit routes through SP1: + zk-KYC screen, over-18, zkML MNIST, compliance pool, storage-proof coprocessor, + rollup validity anchor, and the recursive aggregator. The reason is concrete: + smallest proofs (~260 to 356 bytes), lowest typical verify gas (~300k), one Rust + guest toolchain, and native recursion via `verify_sp1_proof` inside the zkVM. +- **RISC Zero is the diversity path.** A second independent RISC-V zkVM, kept so + the verification surface is not single-prover; a real Groth16 factorization + receipt is recorded on-chain. +- **Halo2 / KZG is the direct-circuit path.** For circuits authored directly as a + PLONK arithmetization (bn254 / KZG / SHPLONK), plus the raw EIP-4844 + point-evaluation precompile for blob and commitment openings. + +The honest framing the source insists on: this is a multi-prover verification +surface behind one gateway, unusual to have in one place, but not a claim that no +other chain can verify any one of these. + +### B.3 Why the on-chain-gas column motivates the STARK-verifier roadmap + +SP1 Groth16, RISC Zero Groth16, and Halo2 all terminate their on-chain check in a +**BN254 pairing** (Groth16 or KZG). Two problems live in that column: the check +costs ~300k to ~450k gas, and BN254 pairing security rests on +discrete-log / pairing hardness, which is **Shor-breakable**. That single +elliptic-curve link is the only quantum-vulnerable step in an otherwise +hash-based SP1 proof chain. + +Roadmap item: replace the BN254 Groth16 wrap with a direct hash-based STARK +verifier. `[CITED: aerenew/pqc-fork/pq-stark/README.md; aerenew/docs/PQ-STARK-VERIFIER-PRECOMPILE-2026-07-18.md]` +The design is a native precompile at `0x0AE8`. The generic verifier skeleton built +so far verifies a BabyBear / Plonky3 FRI STARK directly, with no BN254 wrap, so its +security rests only on hash collision-resistance and Reed-Solomon proximity gaps. + +**Scope caveat (2026-07-19 research finding)** `[CITED: aerenew/docs/AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md]`: +the six generic components confirmed so far verify **BabyBear + FRI STARKs** +(Aere's OWN Plonky3 circuits), NOT SP1 6.1.0 proofs. The pinned SP1 6.1.0 is a +**Hypercube** release (KoalaBear multilinear: BaseFold plus sumcheck-zerocheck +plus LogUp-GKR), so its inner proof is hash-based but NOT a BabyBear FRI STARK, and +FRI plus DEEP-ALI do not apply to it. Replacing the SP1 BN254 Groth16 wrap on real +SP1 proofs is therefore a SEPARATE ~22 to 32 person-week retarget and a founder +decision, not a completion of the skeleton below. + +**Honest status of that roadmap item, stated plainly** `[CITED: same README, "HONEST STATUS"]`: +it is a REFERENCE SKELETON plus DESIGN. It is NOT audited, NOT a working +verifier for SP1 proofs, and NOT activated on any Aere network. It fail-closes +(returns "not verified" for every input, cannot emit a false accept). The +SP1-recursion-specific crypto core is un-ported, and per the caveat above the +SP1 target is a different (Hypercube) proof system entirely. Mainnet 2800 has +exactly the five PQC precompiles `0x0AE1..0x0AE5`; `0x0AE8` is not live anywhere. + +--- + +## PART C: CRYPTO-OP GAS (PQC vs ECDSA) + +### C.1 Table (measured marginal precompile verify-op gas, with sources) + +| Operation | Address | Marginal gas | Full verify-and-record tx gasUsed | Source | +|---|---|--:|--:|---| +| ECDSA (ecrecover) | 0x01 | ~3,000 | n/a | protocol constant `[VERIFY: G_ecrecover = 3000 is a fixed EVM constant, not Aere-specific]` | +| P-256 / passkey (RIP-7951, aka RIP-7212) | 0x100 | ~3,450 | n/a | `[CITED: aerenew/docs/wp2-sections/02-architecture.md:36; aerenew/research/aip-draft-pqc-precompiles.md section 4, "repo-sourced from the Fusaka notes"]` | +| SHAKE256 (FIPS 202) | 0x0AE5 | 60 base + 12/word | 21,470 | `[CITED: aerenew/pqc-fork/precompiles/HashToPointPrecompiledContract.java lines 51-52 (BASE_GAS=60, GAS_PER_WORD=12); aip-draft section 3 table]` | +| Falcon-512 (NIST round-3) | 0x0AE1 | 40,000 | 86,336 | `[CITED: aip-draft section 4 and Reference table]` | +| ML-DSA-44 (FIPS 204) | 0x0AE3 | 55,000 | 351,050 | `[CITED: aip-draft section 6 and Reference table]` | +| ML-KEM-768 (FIPS 203, encapsulation) | 0x0AE6 | 60,000 (fixed) | n/a (KEM, testnet-only) | `[CITED: aerenew/pqc-fork/precompiles/MLKEM768PrecompiledContract.java line 73 (GAS = 60_000)]` | +| Falcon-1024 (NIST round-3) | 0x0AE2 | 75,000 | 145,496 | `[CITED: aip-draft section 5 and Reference table]` | +| SLH-DSA-SHA2-128s (FIPS 205) | 0x0AE4 | 350,000 | 558,276 | `[CITED: aip-draft section 7 and Reference table]` | + +All marginal-gas values are the scratch-fork (chain 28099) measured constants; +the verify-and-record tx gasUsed values are on-chain receipts. `[CITED: aerenew/research/aip-draft-pqc-precompiles.md Reference Implementation table]` +The five signature and hash precompiles (`0x0AE1..0x0AE5`) are live on mainnet +2800, activated at block 9,189,161. ML-KEM-768 (`0x0AE6`) and Falcon HashToPoint +(`0x0AE7`) are KAT-validated on an isolated testnet and remain founder-gated for +mainnet. `[CITED: aerenew/pqc-fork/README chain, pqc-fork memory]` + +Scope reminder attached to this table: these precompiles are an application and +account layer capability. They do not make Aere consensus post-quantum. + +### C.2 Two fresh cross-checks run this session + +`[MEASURED-FRESH]` The SHAKE256 gas schedule (60 base plus 12 per word) is +confirmed present in source, and the HashToPoint precompile's own gas was freshly +computed from that exact source formula (`gasRequirement`, lines 78-93): + +``` +Falcon-512 (n=512) 32-byte message, 73-byte input: words=38 -> gasRequirement = 516 +Falcon-1024 (n=1024) 32-byte message, 73-byte input: words=73 -> gasRequirement = 936 +``` + +516 gas matches the source javadoc's "one ~500-gas staticcall" claim, which is +the mechanism by which HashToPoint cuts a full Solidity Falcon-512 verify. This +is the precompile's own intrinsic gas; it is distinct from the end-to-end verify +gas below, and the two must not be conflated. + +`[CITED: aerenew/pqc-fork/results/bench-results.json]` The HashToPoint-precompile +optimization measured on the scratch fork (chain 28777), full Falcon-512 verify: +9,140,858 gas in pure EVM dropping to 7,186,367 gas with the precompile, a 21.4 +percent reduction across 8 test vectors, all accept and tamper-reject checks +passing. + +### C.3 The honest story the numbers tell + +Post-quantum verification is materially more expensive than ECDSA. Ratios below +are fresh arithmetic from the cited marginal-gas constants divided by the +3,000-gas ecrecover: + +| Scheme | Marginal gas | Cost vs ECDSA (3,000) | +|---|--:|--:| +| Falcon-512 | 40,000 | ~13.3x | +| ML-DSA-44 | 55,000 | ~18.3x | +| ML-KEM-768 | 60,000 | ~20.0x | +| Falcon-1024 | 75,000 | ~25.0x | +| SLH-DSA-SHA2-128s | 350,000 | ~116.7x | + +So PQC verification runs roughly 13x (Falcon-512) to about 117x +(SLH-DSA-SHA2-128s) the cost of an ECDSA recover. That premium is exactly what +motivates two roadmap directions: + +- **Aggregation.** Amortize one expensive PQC verify across many authentications + rather than paying per signature. `[VERIFY: the specific "AerePQAggregate" + contract name is not found in the repo; PQC aggregation is a documented roadmap + direction, see aerenew/docs/FRONTIER-PROGRAM-2026-07-12.md]` +- **Finality certificate.** Carry post-quantum finality as a certificate over a + finalized block rather than re-verifying PQC signatures per transaction. This + ties to the dual-quorum PQ-consensus design work. `[CITED: aerenew/docs/PQ-CONSENSUS-STEP2-2026-07-18.md]` + Note the scope line: this is design and attestation alongside QBFT, it does not + make consensus post-quantum. + +--- + +## PART D: INDEPENDENT REPRODUCTION + +### D.1 The strongest benchmarks should be third-party reproduced + +The credibility of every number above rises sharply when a party other than Aere +reruns it. The honest reproduction candidates, in priority order: + +- **The Nethermind team (warmest angle).** Aere already runs a patched Nethermind + as a second client that validates and follows live chain 2800, and it runs the + PQC precompiles and can produce QBFT blocks Besu accepts. `[CITED: aerenew/docs/wp2-sections/09-governance-roadmap.md:199, 253; NETHERMIND-2ND-CLIENT-LIVE memory]` + That existing relationship makes them the natural first ask for an independent + client-side reproduction of the precompile gas and the consensus behavior. +- **A university lab.** Cheap under a research grant and citable in a way a vendor + benchmark is not; a good fit for the Block-STM correctness-and-scaling harness + and the zkVM proving-time measurements, which are self-contained and need no + Aere infrastructure. +- **Explicitly NOT the expensive audit firms.** The audit-firm budget is reserved + for the security audit, which is a different deliverable from a performance + reproduction. `[CITED: aerenew/docs/mainnet_authority context; AUDIT-OUTREACH-2026-07-12.md]` + +The outreach kit is prepared by us. The actual third-party run and the +relationship are founder and business gated, not something this report initiates. + +### D.2 The run-it-yourself manifest (REPRODUCE) + +This report is the NUMBERS and how they were measured. The run-it-yourself +commands live in the reproducibility bundle. Today that bundle is split across +several committed files rather than one consolidated `REPRODUCE.md`; the honest +recommendation is to consolidate them, but each is real and runnable now: + +| Domain | Where to run it | File | +|---|---|---| +| Block-STM correctness + scaling (Part A.3, freshly run here) | `cd aerenew/parallel-executor && cargo test --release && cargo run --release -- bench` and `-- endtoend` | `aerenew/parallel-executor/BLOCKSTM-ENDTOEND-THROUGHPUT-2026-07-13.md` section 10 | +| PQC precompile KATs + gas (Part C) | `aerenew/pqc-fork/run-kats.sh`, `aerenew/pqc-fork/bench/bench.py` | `aerenew/pqc-fork/` (results in `results/bench-results.json`, `results/kat-results-*.json`) | +| Reproducible Besu client build | `docker build ... -f aerenew/node/Dockerfile.reproducible` then `aerenew/scripts/verify-besu-image.sh` | `aerenew/node/REPRODUCIBLE.md` (note: public digest manifest publication is still roadmap, so the third-party comparison step is not yet live) | +| PQ-consensus reproduction | committed harness | `aerenew/research-stage/formal-consensus/REPRODUCE.md`, `aerenew/audit-package-pq-consensus/REPRODUCE.md` | + +`[MEASURE: create a single top-level aerenew/REPRODUCE.md that indexes all four +domains above with pinned commands, so a third party has one entry point]` + +--- + +## Appendix: provenance summary of every number + +**Freshly measured this session `[MEASURED-FRESH]`:** +- Block-STM `parallel==sequential` gate: PASS on all 4 conflict profiles (this Windows box). +- Block-STM 16-thread execution-phase speedup this box: low 4.36x, medium 4.96x, high 1.92x, pathological 0.43x. +- HashToPoint precompile intrinsic gas from source formula: 516 gas (Falcon-512, 32-byte message), 936 gas (Falcon-1024). + +**Cited from committed repo artifacts `[CITED]`:** +- 273,000 TPS is a design ceiling, never measured (WHITEPAPER-V2, wp2-sections). +- 0.5 s block period, halved at block 2,138,451, single-slot QBFT finality (wp2-sections, genesis-subsecond.json). +- Rollup end-to-end harness ~247k to 270k TPS at gas=80, swinging 115k to 500k, not the L1 ceiling (BLOCKSTM-ENDTOEND section 7). +- Reference 16-core Block-STM ~8.3x to 9.4x exec, ~8.3x to 9.1x end-to-end (same artifact). +- SP1 Groth16 ~300k gas, ~260 to 356 byte proofs; measured records storage-proof 348,345, zkML 326,492, aggregation ~390k (spec-zk-stack; deployment artifacts). +- SP1 proving times: zkscreen ~72 to 75 s, over18 ~71 to 73 s, zkml-mnist ~200 to 205 s, aggregation Groth16 526.1 s (proof-aggregator-scale.json). +- RISC Zero Groth16 seal 260 bytes, 5.0.0-rc.1 (risc0-verifier-fix.json). +- Halo2 ~449,517 gas, 1,152-byte proof; KZG point-eval ~255,719 gas (deployment artifacts, spec-zk-stack). +- PQC marginal gas: Falcon-512 40,000, Falcon-1024 75,000, ML-DSA-44 55,000, SLH-DSA-128s 350,000, ML-KEM-768 60,000, SHAKE256 60+12/word; verify-and-record tx: 86,336 / 145,496 / 351,050 / 558,276 / 21,470 (aip-draft, precompile source, bench-results.json). +- P-256 ~3,450 gas (wp2-sections, aip-draft). +- HashToPoint optimization 9,140,858 to 7,186,367 gas, -21.4% (bench-results.json). + +**To measure `[MEASURE]` or verify `[VERIFY]` (open items):** +- `[MEASURE]` Observed live mainnet sustained TPS over a real block window. +- `[MEASURE]` SP1 Plonk proving time, gas, proof size. +- `[MEASURE]` RISC Zero on-chain verify gas and proving time. +- `[MEASURE]` Halo2 proving time. +- `[MEASURE]` Wall-clock verification latency per prover. +- `[MEASURE]` Consolidated top-level aerenew/REPRODUCE.md. +- `[VERIFY]` The explicit block-space arithmetic behind 273,000 TPS. +- `[VERIFY]` Which genesis gas limit is live on 2800 (40M vs effectively unbounded). +- `[VERIFY]` ECDSA ecrecover 3,000 is a fixed protocol constant (not Aere-specific). +- `[VERIFY]` The "AerePQAggregate" contract name (not found in repo; aggregation is a documented roadmap direction). diff --git a/AERE-BUILD-LOOP-SUMMARY-2026-07-19.md b/AERE-BUILD-LOOP-SUMMARY-2026-07-19.md new file mode 100644 index 0000000..22cc940 --- /dev/null +++ b/AERE-BUILD-LOOP-SUMMARY-2026-07-19.md @@ -0,0 +1,80 @@ +# Aere Network: Autonomous Build Loop Summary (2026-07-19) + +A single clean record of the non-stop build loop. Every item below was verified before it was marked done: real numbers where measured, honest `[MEASURE]` / `[VERIFY]` markers where not, and the post-quantum scope boundary kept everywhere (consensus is classical secp256k1 ECDSA QBFT; only signatures, accounts, and precompiles are post-quantum). Nothing here was deployed to mainnet; every activation stays founder-gated. + +## Consolidation QA (proof it all coexists) + +- Full rebuild: `hardhat clean && compile` compiled 339 Solidity files, zero errors, all new contracts present. +- Tests: 118 passing, 1 pending (a deliberate not-applicable case), 0 failing across the 10 new test files. +- Cross-document consistency: 0 contradictions. Burn is 37.5% of the validator reward (cap 50%, not a base-fee burn); live precompiles are 0x0AE1..0x0AE5; consensus is N=7 / f=2 / quorum 5; the 273k TPS figure is labeled a ceiling, never a measured rate. +- Report: `aerenew/docs/AERE-QA-CONSOLIDATION-REPORT.md`. + +## Depth verification phase (after the roadmap breadth was built) + +The new contracts were not just built and unit-tested; they were then reviewed, hardened, and formally proven: + +- Adversarial security review (17 contracts, fund-flow first): 0 CRITICAL, 0 HIGH, 1 MEDIUM, 3 LOW. The 4 money contracts are clean on all priority properties (CEI plus reentrancy, per-asset escrow solvency with no double-count, no double-pay, no pay-without-proof, fee-on-transfer rejected, fail-closed PQC consumption). Report: `AERE-SECURITY-REVIEW-NEW-CONTRACTS.md`. +- All findings fixed and re-tested: M1 (feedback-author allowlist), L1 (codeless-gateway guard in 3 verifiers), L2 (VectorStore receipt bound to provider), L3 (documented, executor-gated). Report: `AERE-SECURITY-FIXES.md`. +- Formal verification broadened from the existing consensus corpus to the new contracts: 7 new z3 SMT models (3 fund-flow, 4 registry/verifier), each proved with a firing negative control (non-vacuous), wired into the canonical runner. Fresh canonical run: 15 models, 15 of 15 pass, 128 properties PROVED, 79 counterexample negative controls fired, 0 failed. Reports: `AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md`, `AERE-FORMAL-BROADEN-REPORT.md`; `aerenew/REPRODUCE.md` updated with the real fresh count. +- Full regression after the security fixes: compile green, 122 tests passing, 0 failing, 1 pending (a deliberate not-applicable case). No regression. + +Net state of the new contract suite: built, unit-tested (122 passing), QA-compiled (339 files), security-reviewed and hardened (0 critical/high open), and formally proven (15 z3 models). All founder-gated, none deployed. + +## Wave 1: the credibility document cluster (13 docs, the "grade 10" package) + +All under `aerenew/docs/` (plus `aerenew/REPRODUCE.md` and `aerenew/formal-tla/`). + +| # | Deliverable | File | +|---|---|---| +| 17 | Engineering and security specification (threat model, guarantees table, 11 assumptions, design rationale, failure analysis, engineering principles) | AERE-ENGINEERING-SECURITY-SPEC.md | +| 22 | Architecture map (layered stack plus cross-cutting concerns, Mermaid) | AERE-ARCHITECTURE-MAP.md | +| 20 | Ethereum EIP compatibility matrix (EIP by EIP, plus deliberate deviations) | AERE-EIP-COMPATIBILITY-MATRIX.md | +| 19 | NIST validation status (ACVP for FIPS-final schemes, KAT for Falcon, honest "not a certification") | AERE-NIST-VALIDATION-STATUS.md | +| 18 | Reproducible benchmark report (chain, zkVM comparative, crypto-op gas; fresh Block-STM run) | AERE-BENCHMARK-REPORT.md | +| 23 | Reproducibility manifest (fresh SMT 10/10 + 8/8, contract SMT 9/9 green, Hardhat spot-check) | aerenew/REPRODUCE.md | +| 25 | AIP / RFC process and index (real AIP-1..8 inventory, drafted AIP-9..16, no fabricated discussion) | AERE-AIP-PROCESS-AND-INDEX.md | +| 24 | Protocol specification (the delta over Ethereum + QBFT, reimplementable) | AERE-PROTOCOL-SPECIFICATION.md | +| 26 | Cross-client determinism (Besu vs Nethermind byte-identical evidence) | AERE-CROSS-CLIENT-DETERMINISM.md | +| 28 | Reproducible builds and deterministic release | AERE-REPRODUCIBLE-BUILDS.md | +| 29 | Post-quantum governance design | AERE-POST-QUANTUM-GOVERNANCE.md | +| 30 | Quantum-safe networking (transport layer, PQ TLS + devp2p) | AERE-QUANTUM-SAFE-NETWORKING.md | + +## New contracts built and tested (all founder-gated, none deployed) + +| # | Contract(s) | Tests | Notes | +|---|---|---|---| +| 9 | AereRandomnessBeaconV2 (oracle) | 15 passing | Real BLS12-381 drand verify via EIP-2537, replaces a `return true` stub, fail-closed. Ran against live drand quicknet vectors. | +| 3 | AereRecoveryRegistry | 10 passing | Falcon-attested consensus-recovery registry + chaos matrix scaffold + watchtower design. | +| 5 | erc8004/ (Identity, Reputation, Validation, AP2 mandate) | 18 passing | Thin adapters over the live agent stack; PQC validation registry is the differentiator. | +| 7 | compliance/ (TrustRegistry, VerifiableCredential, BitstringStatusList) | 12 passing | Institution-grade compliance passport, W3C VC 2.0 + eIDAS-aligned trust registry + zk non-revocation interface. | +| 8 | intents/AereDestinationSettler | 4 passing | ERC-7683 destination fill, wired to the QBFT finality light client for repayment. | +| 10 | depin/AereComputeMarketV3 | 13 passing | Proof-carrying compute jobs (replay / zk-verified / optimistic) + PQC settlement + escrow solvency invariant. | +| 12 | agentic/AereVectorStore | 8 passing | Verifiable semantic memory for AI agents (Falcon-signed commits, attested retrieval, AERE402 paid query). | +| 14 | pqc/AereAccountMigrator | 9 passing | Atomic ECDSA-account to PQC-account migration (the last account-layer quantum gap). | +| 6 | mpc/AerePQAggregateVerifier + modular/AerePQAggregateModule | 17 passing | One SP1 proof attests a t-of-n PQC committee, cost O(1) in n (measured 61.8k gas flat), ERC-7579 portable. | +| 4 | pqfinality/AerePQAttestationKeyRegistry + AereFinalityCertificateVerifier | 12 passing | Additive post-quantum finality certificate; no consensus flip, no re-genesis. | + +For every contract above, the Falcon precompile (0x0AE1) and the SP1 gateway are mocked in the unit tests and hard-wired to the live addresses for production; the real-precompile path is proven separately against live mainnet. + +## Formal methods, research, and tooling + +| # | Deliverable | Status | +|---|---|---| +| 21 | Certora CVL formal specs for burn / sAERE / registries / threshold | Written; running the prover is `[MEASURE]` (Certora free tier). No rule claimed proved. | +| 27 | TLA+ specification of QBFT (safety + liveness, N=4 and N=7 configs) | Written and structurally checked; running TLC is `[MEASURE]`. Complements the z3 corpus. | +| 2 | Native STARK-verify (0x0AE8) porting spec + generic BabyBear+FRI components | Honest: a ~11-16 person-week port. The six generic components (BabyBear field, Poseidon2, MMCS, FRI, transcript, generic AIR quotient) are conformance-confirmed against Plonky3 `0.4.3-succinct`. SCOPE CAVEAT (2026-07-19 finding): those components verify BabyBear+FRI STARKs (Aere's OWN Plonky3 zk-circuits), NOT SP1 6.1.0, which is Hypercube (KoalaBear multilinear); FRI/DEEP-ALI do not apply to SP1 6.1.0. This does NOT let us "verify SP1 proofs now"; replacing the SP1 BN254 Groth16 wrap is a separate ~22-32 person-week retarget (`AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`). Top-level verifier stays fail-closed and verifies nothing. | +| 31 | Quantum Migration Toolkit (scanner + SDK + cost simulator) | Runnable tool. Scanner ran against live RPC (chain 2800). `aerenew/pqc-migration-toolkit/`. | + +## Off-roadmap issues caught and flagged (spawned as separate tasks) + +- A stale AIP copy in `aere-research-repo/aips/` still claims "three validators" and a Foundation "multisig", contradicting the current seven-validator, single-key reality. Flagged for fix-to-honest. +- The `Dockerfile.reproducible` base-image digests are placeholders, so the reproducible build cannot resolve until real registry digests are pinned. Flagged. + +## What remains gated (needs you, not code) + +- External audit (Trail of Bits / NCC Group): the single largest credibility gate, business-funded. +- Consensus post-quantum activation, first non-Foundation validator, contract-ownership transfer to the Timelock, Season 1 funding, bug-bounty funding: all founder-gated and, where relevant, audit-gated and N greater-than-or-equal-to 9 plus soak gated. +- First live CoreBook market, institutional compliance adoption, real GPU/prover supply: business and counterparty gated. +- Deferred by founder decision (queued, not run): encrypted mempool (#15), economic-soundness simulation (#16). + +Nothing in this loop moved real funds, created a token, or touched the live validators or the production infra box. diff --git a/AERE-CERTORA-FORMAL-VERIFICATION.md b/AERE-CERTORA-FORMAL-VERIFICATION.md new file mode 100644 index 0000000..c977232 --- /dev/null +++ b/AERE-CERTORA-FORMAL-VERIFICATION.md @@ -0,0 +1,821 @@ +# Spec 21: Certora formal-verification specifications for Aere Network's safety-critical contracts + +Status date: 2026-07-19. Author: Aere Network engineering (self-authored CVL). + +## HONEST STATUS BANNER (read first) + +This document contains **written-and-ready** Certora Verification Language (CVL) specifications. It does +**not** contain proof results. Every CVL rule and invariant here is authored against the real contract +source in this repository, but **none has been executed by the Certora Prover**, so **nothing in this +document is claimed "proved."** + +Running these specs requires the Certora Prover, which is an external tool: + +- Free tier available at `prover.certora.com` (needs an account). +- Local driver is the `certora-cli` Python package (`pip install certora-cli`), which uploads the job + to Certora's cloud solver back end. +- The prover is **not installed or run in this environment.** + +Wherever a proof result would go, this document writes a `[MEASURE]` marker naming the exact command to +run and the artifact to publish. A rule graduates from "written" to "proved" only after `certoraRun` +returns `Verified` for it and the HTML rule report is published. Until then the correct description is +**"CVL authored, not yet run."** + +Scope boundary preserved throughout: these are **application / account / tokenomics-layer** contracts. +Aere Network consensus remains classical ECDSA QBFT (Besu). No rule here asserts post-quantum consensus; +the PQC content is signature verification and key custody at the contract layer only. + +--- + +## 1. Why Certora, and how it complements the existing formal work + +Aere already runs two layers of machine-checked reasoning: + +| Layer | Tool | What it checks | Where it lives | +|---|---|---|---| +| Design-level SMT | z3 (Python) | Property holds over an abstract model of the contract logic (guards, arithmetic, status machine) | `aerenew/formal-consensus/*_smt.py` | +| Symbolic bytecode | Halmos / forge | Property holds over the compiled EVM bytecode for symbolic inputs, bounded | `aerenew/formal-contracts/specs/*.symbolic.t.sol`, `aerenew/contracts/test/formal/*.symbolic.t.sol` | +| Property fuzzing | Foundry / Medusa | Property survives large random input campaigns (sampling) | `aerenew/contracts/test/**` | + +Fuzzing **samples** the input and state space. It runs a property against many concrete inputs and +reports the ones it happened to try. A clean fuzz run is strong evidence, but it is evidence about the +paths that were sampled, not a statement about the paths that were not. + +The Certora Prover is different in kind. It compiles the contract to a logical transition system and asks +an SMT solver whether the negation of a rule is satisfiable **over all inputs and all reachable states** +(subject to declared loop bounds and summaries). A rule that verifies is a statement that no input, in no +ordering, from no reachable state, can violate the property. A rule that fails returns a concrete +counterexample transaction. + +Certora sits above the existing work rather than replacing it: + +- It shares the z3 models' **property statements** (the "what to prove"), which is why this document + reuses the invariants already written in `threshold_account_smt.py`, `cryptoregistry_smt.py`, and + `pqckeyregistry_smt.py` verbatim as the source of truth, now expressed in CVL. +- Unlike the z3 models, which reason over a hand-built abstraction, CVL rules are checked against the + **actual compiled contract**, closing the gap the z3 files honestly flag as their own boundary + ("a design model, not the Solidity bytecode"). +- Unlike Halmos, which is symbolic-execution based and bounded per call, the Certora Prover reasons + inductively across an arbitrary method sequence via `invariant` and parametric `rule` constructs, and + gives first-class support for `ghost` state and storage `hook`s. + +The three tools are complementary: z3 fixes the property at design time, Halmos and Certora both check it +against bytecode (Halmos by bounded symbolic execution, Certora by inductive SMT over all methods), and +fuzzing provides cheap continuous regression coverage. + +--- + +## 2. Target contracts and the properties to prove + +Each subsection: (1) the real interface as read from source, with file path and the exact state +variables / function signatures the CVL binds to, then (2) the CVL rules and invariants. + +Convention in the CVL: `env e` is the calling environment, `mathint` is the unbounded integer sort (used +to make arithmetic assertions overflow-free), `currentContract` is the contract under verification, and +`nativeBalances[a]` is the native-AERE balance of address `a`. A `using X as y` line links a second +contract (for example the ERC-20 asset) so its storage is observable inside a rule. + +--- + +### 2.a Burn stack + +#### 2.a.1 `AereSink` (immutable 3-bucket router) + +Source: `aerenew/contracts/contracts/sink/AereSink.sol`. Read confirms: + +- `is ReentrancyGuard` only. **No `Ownable`, no admin role, no setters** (`grep` for `onlyOwner`, + `setBucket`, `setRecipient` returns nothing; the NatSpec asserts this and the source matches). +- Immutable state (each exposed by an auto getter): `address AERE`, `address BURN_VAULT`, + `address SAERE_VAULT`, `address DEX_ROUTER`, `uint16 BURN_BPS`, `uint16 BUYBACK_BPS`, + `uint16 STAKER_YIELD_BPS`, `uint16 MAX_SLIPPAGE_BPS`, `address ORACLE`. +- Constructor reverts with `BpsMustSumTo10000` unless `BURN_BPS + BUYBACK_BPS + STAKER_YIELD_BPS == 10000`. +- Mutating entrypoints: `flush(address token, uint256 amount)`, `sweepDust(address token)`. In the + `token == AERE` branch both dispatch only to `BURN_VAULT` and `SAERE_VAULT` via `_safeTransfer`; the + `token != AERE` branch routes the same two addresses through `_swapAndForward`, where `recipient` is + only ever `BURN_VAULT` or `SAERE_VAULT` (proven set by inspection). + +Properties (matching the z3 / Halmos SK-series and the SECURITY-POSTURE "no path sends to an arbitrary +address" statement): + +```cvl +// certora/specs/AereSink.spec +using DummyERC20A as aere; // the AERE / WAERE asset, linked so its balances are observable + +methods { + function BURN_BPS() external returns (uint16) envfree; + function BUYBACK_BPS() external returns (uint16) envfree; + function STAKER_YIELD_BPS() external returns (uint16) envfree; + function BURN_VAULT() external returns (address) envfree; + function SAERE_VAULT() external returns (address) envfree; + function DEX_ROUTER() external returns (address) envfree; + function AERE() external returns (address) envfree; + function aere.balanceOf(address) external returns (uint256) envfree; +} + +// SK-INV-1 the three bucket splits always sum to exactly 10000 basis points. +// Immutable, so the constructor's BpsMustSumTo10000 guard is the whole proof; the +// invariant asserts no reachable state breaks it. +invariant bpsSumTo10000() + to_mathint(BURN_BPS()) + to_mathint(BUYBACK_BPS()) + to_mathint(STAKER_YIELD_BPS()) == 10000; + +// SK-INV-2 the bucket recipients can never be redirected: no method changes the +// immutable BURN_VAULT / SAERE_VAULT addresses. This is the "no owner/admin can +// redirect funds" property expressed as an all-methods parametric rule. +rule recipientsImmutable(method f, env e, calldataarg args) { + address burnBefore = BURN_VAULT(); + address saereBefore = SAERE_VAULT(); + f(e, args); + assert BURN_VAULT() == burnBefore, "BURN_VAULT is immutable"; + assert SAERE_VAULT() == saereBefore, "SAERE_VAULT is immutable"; +} + +// SK-RULE-3 NO ARBITRARY RECIPIENT: a flush of AERE never increases the AERE +// balance of any address that is not one of the fixed buckets, the router, or the +// sink itself. There is no code path that pays a caller-chosen address. +rule noFundsToArbitraryAddress(env e, uint256 amount, address stranger) { + require stranger != BURN_VAULT(); + require stranger != SAERE_VAULT(); + require stranger != DEX_ROUTER(); + require stranger != currentContract; + mathint before = aere.balanceOf(stranger); + flush(e, AERE(), amount); + mathint after = aere.balanceOf(stranger); + assert after <= before, + "flush must never credit an address outside the immutable bucket set"; +} + +// SK-RULE-4 same guarantee for the permissionless sweepDust path. +rule sweepDustNoArbitraryAddress(env e, address stranger) { + require stranger != BURN_VAULT(); + require stranger != SAERE_VAULT(); + require stranger != DEX_ROUTER(); + require stranger != currentContract; + mathint before = aere.balanceOf(stranger); + sweepDust(e, AERE()); + assert aere.balanceOf(stranger) <= before; +} +``` + +Note on the token != AERE branch: `_swapAndForward` calls out to `DEX_ROUTER`, an external address. +Certora leaves the router call to its default havoc, which conservatively allows the router to move funds +however it likes; the CVL above therefore restricts SK-RULE-3/4 to the `token == AERE` direct-settle +branch (no external callback), exactly the branch the Halmos SK-series covers. The router branch is +argued by inspection (identical `recipient` set) and is a `[MEASURE]` extension: add a `DISPATCHER` +summary for `IAereV2Router.swapExactTokensForTokens` that forwards only to `recipient`. + +#### 2.a.2 `AereCoinbaseSplitterV2` + +Source: `aerenew/contracts/contracts/AereCoinbaseSplitterV2.sol`. Read confirms: + +- `is Ownable, ReentrancyGuard`. Mutable `uint256 burnBps` (default 3750), `uint256 sinkBps` (default 1500). +- Constants: `BPS = 10000`, `MAX_BURN_BPS = 5000`, `MAX_SINK_BPS = 3000`, `SINK_CHANGE_TIMELOCK = 7 days`. +- `setBps(uint256 _burnBps, uint256 _sinkBps)` is `onlyOwner` and reverts `BpsOutOfRange` unless + `_burnBps <= MAX_BURN_BPS`, `_sinkBps <= MAX_SINK_BPS`, and `_burnBps + _sinkBps <= BPS`. +- `rebateBps()` view returns `BPS - burnBps - sinkBps` (derived, so it must stay non-negative). + +```cvl +// certora/specs/AereCoinbaseSplitterV2.spec +methods { + function burnBps() external returns (uint256) envfree; + function sinkBps() external returns (uint256) envfree; + function BPS() external returns (uint256) envfree; + function MAX_BURN_BPS() external returns (uint256) envfree; + function MAX_SINK_BPS() external returns (uint256) envfree; + function owner() external returns (address) envfree; +} + +// CS-INV-1 burnBps is capped at MAX_BURN_BPS (5000) in every reachable state. +// This is the on-chain form of "validator-reward burn cut, hard-capped at 50%". +invariant burnBpsWithinCap() + burnBps() <= MAX_BURN_BPS(); + +// CS-INV-2 sinkBps is capped at MAX_SINK_BPS (3000). +invariant sinkBpsWithinCap() + sinkBps() <= MAX_SINK_BPS(); + +// CS-INV-3 burn + sink never exceed the total, so the derived rebateBps +// (BPS - burnBps - sinkBps) can never underflow / go negative. +invariant burnPlusSinkWithinTotal() + to_mathint(burnBps()) + to_mathint(sinkBps()) <= to_mathint(BPS()); + +// CS-RULE-4 only the owner can move the bps, and only within the caps. Any method +// that changes burnBps or sinkBps must be called by the owner and must land inside +// the caps (so no path, owner or not, exceeds MAX_BURN_BPS). +rule onlyOwnerChangesBpsWithinCaps(method f, env e, calldataarg args) { + uint256 b0 = burnBps(); + uint256 s0 = sinkBps(); + f(e, args); + bool changed = (burnBps() != b0) || (sinkBps() != s0); + assert changed => e.msg.sender == owner(), "only owner may change bps"; + assert burnBps() <= MAX_BURN_BPS(), "post-state respects the burn cap"; + assert to_mathint(burnBps()) + to_mathint(sinkBps()) <= to_mathint(BPS()); +} +``` + +#### 2.a.3 `AereFeeBurnVault` + +Source: `aerenew/contracts/contracts/AereFeeBurnVault.sol`. Read confirms: + +- No `Ownable`, no admin. Functions: `receive()`, `burn()` (payable), `burnToken(address,uint256)`, + `sweepToZero()`, `currentAEREBalance()` view. **There is no `withdraw`, no `rescue`, no admin escape.** +- `uint256 totalBurnedAERE` increments on every native inflow; `uint256 totalSentToZero` increments in + `sweepToZero`; `mapping(address => uint256) totalBurnedToken`. +- `sweepToZero()` sends the whole native balance to `address(0)` (the burn sink) and to nowhere else. + +```cvl +// certora/specs/AereFeeBurnVault.spec +methods { + function totalBurnedAERE() external returns (uint256) envfree; + function totalSentToZero() external returns (uint256) envfree; +} + +// FB-INV-1 the lifetime burn counter is monotonic non-decreasing (it is a running +// total of arrivals; no path decrements it). +rule totalBurnedMonotonic(method f, env e, calldataarg args) { + mathint before = totalBurnedAERE(); + f(e, args); + assert to_mathint(totalBurnedAERE()) >= before; +} + +// FB-RULE-2 NO WITHDRAW PATH: the vault's own native balance is monotonic +// non-decreasing for EVERY method except sweepToZero. sweepToZero is the only +// method that can reduce the balance, and (FB-RULE-3) it can only send to the burn +// sink (address(0)), never to a caller-chosen address. +rule balanceMonotonicExceptBurnSink(method f, env e, calldataarg args) + filtered { f -> f.selector != sig:sweepToZero().selector } { + mathint before = nativeBalances[currentContract]; + f(e, args); + assert nativeBalances[currentContract] >= before, + "no non-sweep method may reduce the vault balance (there is no withdraw)"; +} + +// FB-RULE-3 the only sink is address(0): sweepToZero credits no non-zero address. +// (address(0) is the burn destination; every other account's balance is untouched +// or reduced, never increased by the vault's operation.) +rule sweepGoesOnlyToBurnSink(env e, address r) { + require r != 0; // any real, non-burn address + require r != currentContract; + mathint before = nativeBalances[r]; + sweepToZero(e); + assert nativeBalances[r] <= before, + "sweepToZero must not credit any address other than the address(0) burn sink"; +} +``` + +`[MEASURE: run certoraRun certora/conf/burnstack.conf and publish the AereSink / AereCoinbaseSplitterV2 +/ AereFeeBurnVault rule report]` + +--- + +### 2.b Tokenomics: `sAERE` (ERC-4626 staking receipt) + +Target the corrected `sAEREv2`. Source: `aerenew/contracts/contracts/staking/sAEREv2.sol` (the R7-fixed +redeploy; the live `sAERE` at `0xA212...50b0` shares the same interface but not the R7 fix, see the note +on SR-RULE-3). Read confirms: + +- `is ERC4626`. **No admin / owner / pause / upgrade proxy / parameter setters.** Constants + `DRIP_DURATION = 7 days`, `DRIP_RESTART_THRESHOLD_BPS = 100`, `DEAD_SHARES_SEED_WAERE = 1000 wei`, + `_decimalsOffset() == 6`. +- State: `uint256 rewardRate`, `uint256 periodFinish`, `uint256 lastObservedBalance`. +- `totalAssets()` returns `syncedBalance - undistributed`, where `syncedBalance = min(assetBalance, + lastObservedBalance)` (the R7 fix) and `undistributed = _undistributedNow()`. +- `sync()` is permissionless and only observes arrivals; it never moves funds out. Public `deposit`, + `mint`, `withdraw`, `redeem` each call `sync()` first, then the OZ super. + +Properties (donation-inflation resistance, totalAssets consistency, exchange-rate monotonicity under the +drip): + +```cvl +// certora/specs/sAEREv2.spec +using DummyERC20A as waere; // the underlying WAERE asset + +methods { + function totalSupply() external returns (uint256) envfree; + function totalAssets() external returns (uint256) envfree; + function undistributedRewards() external returns (uint256) envfree; + function convertToAssets(uint256) external returns (uint256) envfree; + function asset() external returns (address) envfree; + function waere.balanceOf(address) external returns (uint256) envfree; +} + +// SR-RULE-1 DONATION / INFLATION RESISTANCE: no bare transfer into the vault, and +// no sync(), mints shares. Share supply can increase ONLY through deposit or mint. +// A raw WAERE.transfer to the vault (the classic ERC-4626 first-depositor inflation +// donation) leaves totalSupply untouched. +rule noShareMintOnDonationOrSync(method f, env e, calldataarg args) + filtered { f -> f.selector != sig:deposit(uint256,address).selector + && f.selector != sig:mint(uint256,address).selector } { + mathint tsBefore = totalSupply(); + f(e, args); + assert to_mathint(totalSupply()) <= tsBefore, + "only deposit / mint may increase sAERE share supply"; +} + +// SR-INV-2 totalAssets CONSISTENCY: reported assets never exceed the vault's real +// WAERE balance (the R7 fix subtracts the undistributed reserve from the SYNCED +// balance, so an un-synced donation is never counted early and totalAssets is a +// true lower bound on redeemable backing). +invariant totalAssetsNeverExceedsBalance() + to_mathint(totalAssets()) <= to_mathint(waere.balanceOf(currentContract)); + +// SR-INV-3 the unvested drip reserve is fully backed: undistributedRewards never +// exceeds the real balance (so the reserve can never be double-counted into a +// payout, the exact R7 defect that drove totalAssets to 0 in v1). +invariant reserveFullyBacked() + to_mathint(undistributedRewards()) <= to_mathint(waere.balanceOf(currentContract)); + +// SR-RULE-4 EXCHANGE-RATE MONOTONICITY UNDER THE DRIP: calling sync() never lowers +// the value of a share. With share supply unchanged across the call, the assets a +// fixed share amount converts to does not fall. In v2 an arrival folded into the +// reserve is rate-neutral at the sync instant (R7) and then vests upward over time; +// it never steps down. Running this same rule against the pre-R7 sAERE.sol produces +// a counterexample (v1 counts the arrival in totalAssets first, so sync() drops the +// rate): that CEX is the R7 bug, which is why sAEREv2 is the verification target. +rule syncNeverLowersShareValue(env e, uint256 shareAmt) { + require shareAmt > 0; + mathint supplyBefore = totalSupply(); + mathint assetsPerShareBefore = convertToAssets(shareAmt); + sync(e); + assert to_mathint(totalSupply()) == supplyBefore, "sync mints/burns no shares"; + assert to_mathint(convertToAssets(shareAmt)) >= assetsPerShareBefore, + "a share is never worth less after sync (drip is up-only)"; +} +``` + +`[MEASURE: run certoraRun certora/conf/sAEREv2.conf and publish the rule report]`. Note the deliberate +demonstration value of SR-RULE-4: it is written to PASS on `sAEREv2.sol` and to FAIL (with a printed +counterexample) on the un-fixed `sAERE.sol`, matching the R7 finding in +`SECURITY-POSTURE-VERIFICATION-2026-07-15.md`. Do not claim either result until the prover has run both. + +--- + +### 2.c Registries + +#### 2.c.1 `AereCryptoRegistry` + +Source: `aerenew/contracts/contracts/pqc/AereCryptoRegistry.sol`. Read confirms: + +- `is Ownable`. Storage: `mapping(uint256 => Algorithm) _algorithms`, `uint256 _count`, `bool _seeded`. + Ids are 1-based and monotonic (`_count += 1` in `_addAlgorithm`, never decremented). +- `Algorithm` fields set once at `addAlgorithm` and never rewritten afterward: `name`, `scheme`, + `verifier`, `pubKeyLen`, `sigLen`, `esigHeader`, `addedBlock`, `isSignature`. Only `status` + (`setStatus`) and `successorId` (`setSuccessor`) are ever mutated post-registration. +- `enum Status { UNKNOWN, ACTIVE, DEPRECATED, REVOKED }`. `verify(...)` is fail-closed: returns false + (never reverts) for a non-existent id, a hash-only row (`isSignature == false`), or a row whose status + is `UNKNOWN` or `REVOKED`, BEFORE the `a.verifier.staticcall`. + +Properties mirror `cryptoregistry_smt.py` (R1 fail-closed, plus the append-only / no-re-point statements +required by the task): + +```cvl +// certora/specs/AereCryptoRegistry.spec +methods { + function algorithmCount() external returns (uint256) envfree; + function statusOf(uint256) external returns (AereCryptoRegistry.Status) envfree; + function owner() external returns (address) envfree; + // verify staticcalls an external verifier; leave it to the prover's default + // havoc so the fail-closed rules must hold for ANY verifier answer. +} + +// CR-INV-1 algorithm ids are append-only: the count never decreases, so an id that +// exists can never be un-registered (rows are added, never removed). +rule algorithmCountMonotonic(method f, env e, calldataarg args) { + mathint before = algorithmCount(); + f(e, args); + assert to_mathint(algorithmCount()) >= before; +} + +// CR-RULE-2 NO UNAUTHORIZED RE-POINT: an existing row's verifier address is +// immutable. Once a scheme id maps to a verifier, no method (setStatus, +// setSuccessor, addAlgorithm of a later id, seedLiveSchemes) can silently rewrite +// it. To change a verifier you must add a NEW id; the old id -> verifier binding is +// write-once. This is the "recorded entries are append-only, cannot be silently +// rewritten" property. +rule verifierNeverRepointed(method f, env e, calldataarg args, uint256 id) { + require id != 0 && id <= algorithmCount(); + AereCryptoRegistry.Algorithm a0 = getAlgorithm(e, id); + f(e, args); + require id <= algorithmCount(); + AereCryptoRegistry.Algorithm a1 = getAlgorithm(e, id); + assert a1.verifier == a0.verifier, "verifier address is write-once"; + assert a1.scheme == a0.scheme, "scheme tag is write-once"; + assert a1.pubKeyLen == a0.pubKeyLen, "pubKeyLen is write-once"; + assert a1.sigLen == a0.sigLen, "sigLen is write-once"; + assert a1.esigHeader == a0.esigHeader, "wire-format header is write-once"; + assert a1.isSignature == a0.isSignature, "signature/hash flag is write-once"; + assert a1.addedBlock == a0.addedBlock, "addedBlock is write-once"; +} + +// CR-RULE-3 only the owner can mutate the registry (add / setStatus / setSuccessor +// / seed). The onlyOwner modifier reverts otherwise, so a completed mutating call +// implies the caller was the owner. +rule onlyOwnerMutates(method f, env e, calldataarg args) + filtered { f -> f.selector == sig:addAlgorithm(string,uint8,address,uint16,uint32,uint8,uint256,bool).selector + || f.selector == sig:setStatus(uint256,AereCryptoRegistry.Status).selector + || f.selector == sig:setSuccessor(uint256,uint256).selector + || f.selector == sig:seedLiveSchemes().selector } { + f(e, args); + assert e.msg.sender == owner(), "registry mutation requires owner"; +} + +// CR-RULE-4 FAIL-CLOSED verify (mirrors cryptoregistry_smt.py R1a): a REVOKED id +// never verifies, whatever the routed verifier would answer (the status gate short- +// circuits before the staticcall, so the prover's havoc of the verifier is +// irrelevant). +rule verifyFailClosedOnRevoked(env e, uint256 id, bytes pubKey, bytes32 messageHash, bytes signature) { + require statusOf(id) == AereCryptoRegistry.Status.REVOKED; + bool result = verify(e, id, pubKey, messageHash, signature); + assert result == false, "a REVOKED row must never verify"; +} + +// CR-RULE-5 FAIL-CLOSED verify for an UNKNOWN id (R1b): a never-registered id +// (id == 0 or id > count) never verifies. +rule verifyFailClosedOnUnknown(env e, uint256 id, bytes pubKey, bytes32 messageHash, bytes signature) { + require id == 0 || id > algorithmCount(); + assert verify(e, id, pubKey, messageHash, signature) == false; +} + +// CR-RULE-6 resolveActive returns ONLY an ACTIVE id (mirrors R3a): if it returns +// (does not revert), the returned id's status is ACTIVE. +rule resolveActiveReturnsActive(env e, uint256 startId) { + uint256 resolved = resolveActive(e, startId); + assert statusOf(resolved) == AereCryptoRegistry.Status.ACTIVE, + "resolveActive never returns a non-ACTIVE id"; +} +``` + +#### 2.c.2 `AerePQCKeyRegistry` (the PQC key registry) + +Source: `aerenew/contracts/contracts/pqc/AerePQCKeyRegistry.sol`. Read confirms: + +- Permissionless (no `Ownable`). Storage: `KeyRecord[] _keys` (append-only; keyId is the array index, + pushed in `_registerWithPoP`, never removed), `mapping(address => uint64) identityNonce` (monotonic), + `mapping(address => uint256[]) _identityKeys`. +- Status constants: `STATUS_NONE=0, STATUS_ACTIVE=1, STATUS_ROTATED=2, STATUS_REVOKED=3`. `revokeKey` + is terminal. +- `KeyRecord.owner` is set once (`owner: owner` in the push) and never rewritten. `rotateKey` stores the + successor with `owner == msg.sender == old.owner`. +- `verifyWithKey` is fail-closed: returns false for an unknown key, `STATUS_REVOKED`, or `STATUS_NONE`. + +Properties mirror `pqckeyregistry_smt.py` K3 (revoked never verifies), K4 (rotation preserves owner), plus +the append-only statements: + +```cvl +// certora/specs/AerePQCKeyRegistry.spec +methods { + function keyCount() external returns (uint256) envfree; + function statusOf(uint256) external returns (uint8) envfree; + function ownerOf(uint256) external returns (address) envfree; + function schemeOf(uint256) external returns (uint8) envfree; + function identityNonce(address) external returns (uint64) envfree; +} + +// KR-INV-1 keys are append-only: keyCount is monotonic non-decreasing, so a +// registered keyId is never removed or its slot reused. +rule keyCountMonotonic(method f, env e, calldataarg args) { + mathint before = keyCount(); + f(e, args); + assert to_mathint(keyCount()) >= before; +} + +// KR-RULE-2 the owner binding of an existing key is immutable: no method rewrites +// an already-registered key's owner (the record's owner field is write-once). This +// is the "recorded entries cannot be silently rewritten" property for identities. +rule keyOwnerImmutable(method f, env e, calldataarg args, uint256 keyId) { + require keyId < keyCount(); + address ownerBefore = ownerOf(keyId); + uint8 schemeBefore = schemeOf(keyId); + f(e, args); + assert ownerOf(keyId) == ownerBefore, "a key's owner is write-once"; + assert schemeOf(keyId) == schemeBefore, "a key's scheme is write-once"; +} + +// KR-RULE-3 REVOKED is terminal (K3 precondition): once a key is REVOKED it stays +// REVOKED across every subsequent method. +rule revokeIsTerminal(method f, env e, calldataarg args, uint256 keyId) { + require statusOf(keyId) == 3; // STATUS_REVOKED + f(e, args); + assert statusOf(keyId) == 3, "a REVOKED key can never leave REVOKED"; +} + +// KR-RULE-4 FAIL-CLOSED verifyWithKey on a REVOKED key (mirrors pqckeyregistry_smt +// K3): a revoked key never verifies, whatever the precompile would answer. +rule verifyWithKeyFailClosedRevoked(env e, uint256 keyId, bytes32 message, bytes signature) { + require statusOf(keyId) == 3; // STATUS_REVOKED + assert verifyWithKey(e, keyId, message, signature) == false; +} + +// KR-RULE-5 the per-identity PoP nonce is monotonic (K2 backbone): every +// registration advances identityNonce, and no method decreases it, so a consumed +// proof-of-possession challenge can never recur for the same identity. +rule identityNonceMonotonic(method f, env e, calldataarg args, address who) { + mathint before = to_mathint(identityNonce(who)); + f(e, args); + assert to_mathint(identityNonce(who)) >= before; +} +``` + +The K1 / K2 domain-separation results (the PoP challenge binds owner and nonce so a proof cannot be +replayed across identities or re-used by the same identity) rest on keccak injectivity. In Certora that is +provable by hashing the challenge tuple through the linked `keccak` model and asserting the two challenge +preimages differ; it is written as a `[MEASURE]` extension (`AerePQCKeyRegistry_pop.spec`) because it +needs the hashing summary set up, and it restates `pqckeyregistry_smt.py` K1/K2 at the bytecode layer. + +`[MEASURE: run certoraRun certora/conf/registries.conf and publish the AereCryptoRegistry / +AerePQCKeyRegistry rule report]` + +--- + +### 2.d Threshold / precompile callers: the duplicate-committee-key fix + +Source: `aerenew/contracts/contracts/mpc/AereThresholdAccount.sol` (ERC-4337 t-of-n PQC account) and the +shared library `aerenew/contracts/contracts/mpc/AerePQCThreshold.sol`. The sibling +`AereThresholdPQCRegistry.registerCommittee(uint8,uint8,bytes[])` carries the identical fix. Read confirms: + +- `initialize(address _entryPoint, uint8 _scheme, uint8 _threshold, bytes[] pubKeys)` is factory-only and + one-shot (`AlreadyInitialized` if re-called). It validates `1 <= _threshold <= n <= 255` and, at the + one place a committee is ever set, **rejects duplicate public keys**: it hashes each key and reverts + `DuplicatePubKey(i)` if `keccak256(pubKeys[i]) == keccak256(pubKeys[j])` for any `j < i`. +- Authorization (`validateUserOp`, `executeThreshold`) counts distinct signers by member INDEX via the + `seen` bitmask in `_countMem`, and returns success only when `valid >= threshold`. +- `scheme`, `threshold`, `size`, `membersHash`, `_pubKeys` are immutable after `initialize`. + +This is the exact target of `aerenew/formal-consensus/threshold_account_smt.py` (P1: with distinct keys, +no single keyholder can reach threshold `t >= 2`). The CVL splits it into the part provable at bytecode +level and the combinatorial part that stays in z3, keeping the same boundary the z3 file itself declares. + +```cvl +// certora/specs/AereThresholdAccount.spec +methods { + function threshold() external returns (uint8) envfree; + function size() external returns (uint8) envfree; + function scheme() external returns (uint8) envfree; + function membersHash() external returns (bytes32) envfree; + function entryPoint() external returns (address) envfree; + function pubKeyAt(uint8) external returns (bytes) envfree; +} + +// TH-RULE-1 committee bounds hold after a successful initialize: a real committee +// always has 1 <= threshold <= size <= 255. In particular threshold >= 1, so an +// empty signer set never authorizes, and threshold <= size, so the committee is +// satisfiable only by genuine members. +rule committeeBoundsAfterInit(env e, address ep, uint8 sch, uint8 t, bytes[] pubKeys) { + initialize(e, ep, sch, t, pubKeys); + assert threshold() >= 1, "threshold is at least 1"; + assert threshold() <= size(), "threshold never exceeds committee size"; + assert to_mathint(size()) == pubKeys.length; +} + +// TH-RULE-2 the committee is set ONCE and is immutable thereafter: a second +// initialize always reverts, and no method changes scheme / threshold / size / +// membersHash after the first init. So the distinct-key set fixed at init can never +// be swapped for a duplicate-laden one later. +rule committeeImmutableAfterInit(method f, env e, calldataarg args) { + require entryPoint() != 0; // already initialized + uint8 t0 = threshold(); + uint8 n0 = size(); + uint8 s0 = scheme(); + bytes32 mh0 = membersHash(); + f(e, args); + assert threshold() == t0, "threshold immutable post-init"; + assert size() == n0, "size immutable post-init"; + assert scheme() == s0, "scheme immutable post-init"; + assert membersHash() == mh0, "membersHash immutable post-init"; +} + +// TH-RULE-3 DISTINCT KEYS ENFORCED AT INIT (the 2026-07-15 dup-key fix): if +// initialize succeeds, then no two stored committee members share a public key. +// Expressed over the two-member witness that the pairwise loop rejects: for any +// distinct in-range indices i, j, the stored keys differ. This is the bytecode-level +// statement of "the same keyholder cannot occupy two committee slots". +rule initRejectsDuplicateKeys(env e, address ep, uint8 sch, uint8 t, bytes[] pubKeys, + uint8 i, uint8 j) { + initialize(e, ep, sch, t, pubKeys); // reverts on any duplicate; reaching here => no dup + require i < size() && j < size() && i != j; + assert keccak256(pubKeyAt(i)) != keccak256(pubKeyAt(j)), + "no two committee members share a public key after a successful init"; +} +``` + +Design-level restatement of `threshold_account_smt.py` P1, expressed in CVL over an abstract committee +(the same combinatorial layer, and the same boundary, that the z3 file declares: it models the counting +logic, not the full Solidity `_countMem` loop over an unbounded `Leg[]`): + +```cvl +// certora/specs/ThresholdCounting.spec (abstract-committee model) +// +// key(i) = the id of the keyholder controlling slot i. count(h) = number of slots h +// controls. The seen-bitmask counts distinct INDICES, so "valid signers" <= number of +// distinct indices supplied. TH-RULE-3 gives distinct KEYS per index, hence distinct +// keyholders per counted index. This ghost model proves the P1 consequence: with +// pairwise-distinct keys, no single keyholder h controls >= threshold slots for t >= 2. + +ghost mapping(uint256 => uint256) key; // slot -> keyholder id +ghost uint256 committeeSize; + +// P1: distinct committee keys => every keyholder fills at most one slot, so reaching +// a threshold t >= 2 requires at least t distinct keyholders. +rule distinctKeysImplyThresholdNeedsDistinctHolders(uint256 h, uint256 t) { + require t >= 2; + // committee keys are pairwise distinct (established on-chain by TH-RULE-3): + require forall uint256 a. forall uint256 b. + (a < committeeSize && b < committeeSize && a != b) => key[a] != key[b]; + // NEGATION: some single keyholder h controls >= t slots. + mathint slotsForH = 0; + // (in the runnable spec this is a bounded fold over committeeSize; shown here as + // the property the fold asserts) + assert !(exists uint256 s1. exists uint256 s2. + s1 < committeeSize && s2 < committeeSize && s1 != s2 + && key[s1] == h && key[s2] == h), + "with distinct keys no keyholder occupies two slots, so t>=2 needs t distinct holders"; +} +``` + +Honesty note on TH: TH-RULE-1/2/3 are bytecode-level rules against the real `AereThresholdAccount`. The +abstract-committee P1 rule is the CVL transcription of the z3 combinatorial proof and carries the same +"not the compiled counting loop" boundary that `threshold_account_smt.py` states in its own summary. The +z3 negative controls (P2/P3: without the distinct-key check one keyholder reaches threshold alone) remain +in z3; the CVL equivalent is simply TH-RULE-3 failing if the `DuplicatePubKey` guard is removed. + +`[MEASURE: run certoraRun certora/conf/threshold.conf and publish the AereThresholdAccount rule report]` + +--- + +## 3. `certora/` layout, run config, and commands + +Proposed tree under the contracts package (`aerenew/contracts/`, so `certoraRun` resolves imports through +the existing Hardhat / Foundry remappings): + +``` +aerenew/contracts/ + certora/ + specs/ + AereSink.spec + AereCoinbaseSplitterV2.spec + AereFeeBurnVault.spec + sAEREv2.spec + AereCryptoRegistry.spec + AerePQCKeyRegistry.spec + AerePQCKeyRegistry_pop.spec # K1/K2 keccak domain-separation (MEASURE extension) + AereThresholdAccount.spec + ThresholdCounting.spec # abstract-committee P1 model + harness/ + DummyERC20A.sol # faithful minimal ERC20 for the linked asset + AereSinkHarness.sol # exposes internal getters if needed + conf/ + burnstack.conf + sAEREv2.conf + registries.conf + threshold.conf + README.md # this status doc's run section, copied for the repo +``` + +`harness/DummyERC20A.sol` is the same faithful minimal ERC-20 the Halmos suite already uses +(`aerenew/formal-contracts/specs/AereSink.symbolic.t.sol` MockERC20): exact-amount `transfer`, +`transferFrom`, `approve`, `balanceOf`. Fee-on-transfer and rebasing tokens are out of scope (excluded by +the asset-listing policy), the same bound the Halmos SK-series declares. + +Example run config (Certora conf files are JSON): + +```json +// certora/conf/burnstack.conf +{ + "files": [ + "contracts/sink/AereSink.sol", + "contracts/AereCoinbaseSplitterV2.sol", + "contracts/AereFeeBurnVault.sol", + "certora/harness/DummyERC20A.sol" + ], + "verify": "AereSink:certora/specs/AereSink.spec", + "link": [ "AereSink:AERE=DummyERC20A" ], + "solc": "solc0.8.23", + "optimistic_loop": true, + "loop_iter": "3", + "rule_sanity": "basic", + "msg": "Aere burn stack: sink 3-bucket immutability + splitter caps + burn-vault no-withdraw" +} +``` + +```json +// certora/conf/sAEREv2.conf +{ + "files": [ + "contracts/staking/sAEREv2.sol", + "certora/harness/DummyERC20A.sol" + ], + "verify": "sAEREv2:certora/specs/sAEREv2.spec", + "link": [ "sAEREv2:_asset=DummyERC20A" ], + "solc": "solc0.8.23", + "optimistic_loop": true, + "rule_sanity": "basic", + "msg": "sAERE v2: donation resistance + totalAssets consistency + drip monotonicity" +} +``` + +```json +// certora/conf/registries.conf +{ + "files": [ + "contracts/pqc/AereCryptoRegistry.sol", + "contracts/pqc/AerePQCKeyRegistry.sol" + ], + "verify": "AereCryptoRegistry:certora/specs/AereCryptoRegistry.spec", + "solc": "solc0.8.23", + "optimistic_loop": true, + "rule_sanity": "basic", + "msg": "Aere PQC registries: fail-closed verify + append-only rows + no re-point" +} +``` + +```json +// certora/conf/threshold.conf +{ + "files": [ + "contracts/mpc/AereThresholdAccount.sol", + "contracts/mpc/AerePQCThreshold.sol" + ], + "verify": "AereThresholdAccount:certora/specs/AereThresholdAccount.spec", + "solc": "solc0.8.23", + "optimistic_loop": true, + "loop_iter": "4", + "rule_sanity": "basic", + "msg": "Aere threshold account: distinct-key committee + set-once immutability" +} +``` + +Exact commands (each requires the `certora-cli` package and a `CERTORAKEY` from `prover.certora.com`): + +```bash +# one-time setup (NOT run in this environment) +pip install certora-cli +export CERTORAKEY= + +# from aerenew/contracts/ +certoraRun certora/conf/burnstack.conf +certoraRun certora/conf/sAEREv2.conf +certoraRun certora/conf/registries.conf +certoraRun certora/conf/threshold.conf + +# run a single rule while iterating: +certoraRun certora/conf/burnstack.conf --rule noFundsToArbitraryAddress + +# separate registry spec run (AerePQCKeyRegistry has its own verify target): +certoraRun certora/conf/registries.conf --verify AerePQCKeyRegistry:certora/specs/AerePQCKeyRegistry.spec +``` + +Each `certoraRun` uploads the job to Certora's cloud back end and returns a job URL whose HTML report +lists every rule as `Verified`, `Violated` (with a counterexample), or `Timeout`. That report is the +artifact to publish. + +--- + +## 4. Honest status + +### 4.1 What is written here versus what is proved + +Everything in Section 2 is **CVL that is authored and matched to the real contract interfaces read from +source in this repository.** The method signatures, state-variable getters, enum members, status +constants, and function selectors are taken from the actual `.sol` files, not from documentation. + +**No rule in this document is proved.** The Certora Prover has not been run. The distinction matters: +"authored and interface-matched" is a claim about the CVL text; "proved" is a claim about a solver result, +and we do not have one. + +### 4.2 Which targets have real CVL versus flags + +| Target | Source file read | CVL status | +|---|---|---| +| `AereSink` | `contracts/sink/AereSink.sol` | Real CVL against real getters (`BURN_BPS`, `BURN_VAULT`, `flush`, `sweepDust`). AERE-branch rules exact; router branch is a marked `[MEASURE]` extension. | +| `AereCoinbaseSplitterV2` | `contracts/AereCoinbaseSplitterV2.sol` | Real CVL (`burnBps`, `sinkBps`, `MAX_BURN_BPS`, `setBps`, `owner`). | +| `AereFeeBurnVault` | `contracts/AereFeeBurnVault.sol` | Real CVL (`totalBurnedAERE`, `sweepToZero`, `nativeBalances`). | +| `sAEREv2` | `contracts/staking/sAEREv2.sol` | Real CVL (`totalAssets`, `undistributedRewards`, `sync`, `convertToAssets`). SR-RULE-4 designed to distinguish v2 from the un-fixed v1. | +| `AereCryptoRegistry` | `contracts/pqc/AereCryptoRegistry.sol` | Real CVL (`getAlgorithm`, `statusOf`, `verify`, `resolveActive`, `Status` enum). | +| `AerePQCKeyRegistry` | `contracts/pqc/AerePQCKeyRegistry.sol` | Real CVL (`keyCount`, `ownerOf`, `statusOf`, `verifyWithKey`, `identityNonce`). K1/K2 keccak domain-separation flagged `[MEASURE]` extension. | +| `AereThresholdAccount` + `AerePQCThreshold` | `contracts/mpc/AereThresholdAccount.sol`, `AerePQCThreshold.sol` | Real CVL for init bounds / set-once / distinct-key (TH-1/2/3). The P1 keyholder-counting theorem is an abstract-ghost model, same boundary as `threshold_account_smt.py`. | +| `AereThresholdPQCRegistry` | `contracts/mpc/AereThresholdPQCRegistry.sol` | Not separately specced here; its `registerCommittee` dup-key guard is byte-identical to `AereThresholdAccount.initialize`, so TH-RULE-3 transfers. Adding a dedicated spec is a `[MEASURE]` follow-up. | + +No target required a `[VERIFY: locate .sol]` flag: every contract named in the task was located +and read. The only interface caveat is the sAERE target selection, which points at `sAEREv2.sol` (the +R7-fixed redeploy) rather than the live `sAERE.sol`; this is stated inline at Section 2.b. + +### 4.3 The measurement gate (nothing is proved until these run) + +| # | Command | Publishes | +|---|---|---| +| M1 | `certoraRun certora/conf/burnstack.conf` | `[MEASURE]` PASS/FAIL for SK-INV-1/2, SK-RULE-3/4, CS-INV-1/2/3, CS-RULE-4, FB-INV-1, FB-RULE-2/3 | +| M2 | `certoraRun certora/conf/sAEREv2.conf` | `[MEASURE]` PASS/FAIL for SR-RULE-1, SR-INV-2/3, SR-RULE-4 | +| M3 | `certoraRun certora/conf/registries.conf` | `[MEASURE]` PASS/FAIL for CR-INV-1, CR-RULE-2..6, KR-INV-1, KR-RULE-2..5 | +| M4 | `certoraRun certora/conf/threshold.conf` | `[MEASURE]` PASS/FAIL for TH-RULE-1/2/3 and the P1 ghost model | + +`[MEASURE: run each conf above with certoraRun and publish the resulting Certora rule report (the job-URL +HTML listing every rule as Verified / Violated / Timeout). Only after a rule shows Verified may it be +described as proved. Until then it is CVL authored, not run.]` + +### 4.4 Publication statement + +When this document is published, the accurate framing is: "Aere Network has authored Certora CVL +specifications for its most safety-critical contracts (burn stack, sAERE, the crypto and PQC-key +registries, and the post-quantum threshold account), matched to the deployed contract interfaces and +reusing the property statements already checked at the design level in z3. Executing them to a machine +report requires the Certora Prover (free tier at prover.certora.com; `certora-cli`), which produces the +per-rule Verified / Violated result. That run is pending; no rule is claimed proved before it." diff --git a/AERE-COMPUTE-MARKET-V3-SUMMARY.md b/AERE-COMPUTE-MARKET-V3-SUMMARY.md new file mode 100644 index 0000000..143fed0 --- /dev/null +++ b/AERE-COMPUTE-MARKET-V3-SUMMARY.md @@ -0,0 +1,60 @@ +# Spec 10: Aere Compute Market V3 (proof-carrying DePIN) + +## Delivered + +1. `aerenew/contracts/contracts/depin/AereComputeMarketV3.sol` (new; deployed V1/V2 untouched) +2. `aerenew/contracts/test/AereComputeMarketV3.test.js` (13 tests, all passing) +3. `aerenew/docs/AERE-COMPUTE-MARKET-V3.md` + +## What it does + +Proof-carrying compute marketplace. Requester posts a job (specHash, reward escrow, deadline, +verification mode); provider claims + runs off-chain; result acceptance depends on the mode: + +- REPLAY (0): deterministic recompute. Result bytes emitted; challenge window; dispute records the + challenger's recomputed hash; arbiter resolves. +- ZK_VERIFIED (1): SP1 proof verified on-chain via the deployed SP1 gateway (ISP1Verifier). publicValues + bound to the job (abi.encode(specHash, resultHash), specHash must match). Paid in the SAME tx, only on + a valid proof. No other pay path exists for a ZK job. +- OPTIMISTIC (2): challenge window + provider bond. Successful dispute slashes provider bond to the + challenger, refunds requester. + +PQC settlement path: any job can set pqcSettlement + an 897-byte Falcon-512 key. Final payout then +requires a Falcon-512 signature (verified via live precompile 0x0AE1) over a digest binding +(chainId, contract, jobId, provider, token, amount, resultHash). Fail-closed. This is payout +authorization only; it does NOT make consensus post-quantum (documented). + +Settlement asset: native AERE (address(0)) or an allowlisted ERC-20 (governance-gated allowlist). +Bonds always native AERE. No new token. + +## Fail-closed / invariants (all tested) + +- Escrow solvency: totalLiabilities[token] = sum(open rewards + posted bonds); contract balance always + >= liabilities per asset. isSolvent() view. Asserted after every mutating step in every test. +- No double-pay: terminal statuses (Paid/Refunded/Slashed) reached once; nonReentrant; CEI ordering. +- No pay-without-proof (ZK): settle inside submitResultZK after verifyProof (reverts on invalid). +- No admin drain: no owner, no sweep. Arbiter only routes a DISPUTED job's escrow; governance only + flips a token-allowlist bool. +- Fee-on-transfer/rebasing reward tokens rejected at escrow (received must equal stated reward). + +## Real test result + +`npx hardhat test test/AereComputeMarketV3.test.js` (from aerenew/contracts): +13 passing (~2s). Covers: ZK pay-on-valid + reject-invalid + wrong-spec rejection; OPTIMISTIC +finalize + dispute-slash; REPLAY dispute (provider upheld) + off-chain re-run match; ERC-20 reward +allowlist accept/reject; Falcon valid-accept + tampered-reject + wrong-amount-reject + +sig-on-nonpqc-job reject; solvency across a mixed batch; deadline reclaim with bond slash. + +## Grounding used + +- Built on AereComputeMarketV2 job/escrow model (depin/). +- ZK: ISP1Verifier.sol + SP1VerifierGateway.sol; deployed gateway 0x9ca479C8c52C0EbB4599319a36a5a017BCC70628. +- Falcon: input encoding + fail-closed raw-32-byte return pattern from AerePQCMessageVerifier.sol; + test uses MockPQCPrecompile(1) @0x0AE1 and MockSp1Verifier (reverts on invalid), MockERC20Lending. + +## Flags + +- [VERIFY] ZK path tested vs MockSp1Verifier (mirrors gateway revert-on-invalid); real gateway wired at deploy. +- [VERIFY] Falcon path tested vs MockPQCPrecompile; real wire encoding KAT-proven elsewhere; 0x0AE1 live on 2800. +- [MEASURE] Real GPU supply, off-chain provers, real SP1 proving are external (adoption, not code). +- Not deployed; founder-gated. diff --git a/AERE-COMPUTE-MARKET-V3.md b/AERE-COMPUTE-MARKET-V3.md new file mode 100644 index 0000000..542d628 --- /dev/null +++ b/AERE-COMPUTE-MARKET-V3.md @@ -0,0 +1,156 @@ +# Aere Compute Market V3 + +Proof-carrying decentralized compute (DePIN) settlement for Aere Network. + +## What it is + +`AereComputeMarketV3` is the on-chain verification and settlement rail for a decentralized compute +marketplace. A REQUESTER posts a job (a commitment to the workload spec, a reward held in escrow, a +deadline, and a required verification mode). A PROVIDER claims the job, runs the work off-chain, and +submits a result. The provider is paid only against verifiable evidence, never on trust alone. Which +evidence counts, and when payment releases, is decided by the job's VERIFICATION MODE. + +V3 unifies the verification rails that were split across the earlier coordination layer +(`AereComputeMarketV2`, which offered a single optimistic path with Foundation arbitration) and adds a +post-quantum settlement gate. The deployed V1 and V2 DePIN contracts are untouched; V3 is a new, +independent contract. + +Source: `aerenew/contracts/contracts/depin/AereComputeMarketV3.sol` +Test: `aerenew/contracts/test/AereComputeMarketV3.test.js` (13 passing) + +## The three verification modes + +A requester picks one mode per job. Each mode answers one question: what makes a submitted result +payable? + +### REPLAY (mode 0) + +The result is a deterministic function of the input. On submission the provider posts the full result +bytes, which the contract emits (and anchors as `keccak256(result)`), so any watcher can re-run the +spec locally and compare `keccak256(localResult)` against the on-chain `resultHash`. The result is +accepted after a challenge window unless a challenger posts a matching bond and disputes. On a dispute +the challenger records the `resultHash` they recomputed, so the arbiter (and any observer) can +mechanically verify who is correct. The arbiter then resolves. + +When to use it. Workloads that are pure, deterministic, and cheap to re-execute (batch transforms, +deterministic simulations, reproducible builds). Disputes are objectively decidable by re-running, so +the arbiter's role is mechanical rather than judgemental. + +### ZK_VERIFIED (mode 1) + +The result carries a zero-knowledge proof, verified ON-CHAIN through the existing deployed SP1 gateway +verifier. The provider submits the SP1 public values (ABI-encoded as `(bytes32 specHash, bytes32 +resultHash)`) and the proof. The contract binds the proof to the job by requiring the proven `specHash` +to equal the job's committed spec, records the proven `resultHash`, then calls the gateway's +`verifyProof`. The reward releases in the SAME transaction, and ONLY if the proof verifies. There is no +other code path that pays a `ZK_VERIFIED` job, so paying one without a valid proof is impossible. + +When to use it. Workloads where correctness must be enforced without trusting a challenge window or an +arbiter: verifiable inference, zk coprocessing, anything where the requester wants finality on delivery +rather than after a delay. The cost is that the provider must run a real prover. + +The verifier reference. V3 calls the `ISP1Verifier` interface +(`aerenew/contracts/contracts/zkverify/ISP1Verifier.sol`), the same interface implemented by the +deployed `SP1VerifierGateway` at `0x9ca479C8c52C0EbB4599319a36a5a017BCC70628` on Aere Network chain +2800. V3 does not reimplement proof verification; it references and calls the existing gateway. The +gateway routes on the proof's first four bytes to the correct SP1 verifier and reverts on an invalid +proof, which is exactly the fail-closed behavior V3 relies on. + +### OPTIMISTIC (mode 2) + +The result is accepted after a challenge window unless a challenger posts a bond and disputes. A +successful dispute slashes the PROVIDER bond to the CHALLENGER and refunds the reward to the requester. +Unlike REPLAY, the result is not assumed cheaply re-derivable, so the provider stakes a bond as skin in +the game and the challenge is a general fraud claim rather than a mechanical recomputation. + +When to use it. Workloads that are checkable but not cheaply reproducible (large or non-deterministic +pipelines, results that are expensive to recompute but easy to spot-check). The bond sizes the cost of +lying. + +## Post-quantum settlement path + +Any job (in any mode) can set `pqcSettlement = true` and register an 897-byte Falcon-512 settlement +key. When set, the final release of funds to the provider additionally requires a Falcon-512 signature +by that key over a domain-separated settlement digest binding `(chainId, contract, jobId, provider, +token, amount, resultHash)`. The signature is verified IN FULL on-chain by the live native precompile +at `0x0AE1` (activated on Aere mainnet 2800 at block 9,189,161), using the same input encoding proven +against the live precompile in `AerePQCMessageVerifier`. + +The point: the payout authorization is post-quantum. A quantum adversary who forged the classical +secp256k1 transaction sender still cannot authorize a payout without the Falcon private key. The digest +binds the exact payout figure and result, so an authorization can never be replayed to another job, +chain, contract, or amount. A tampered or missing signature reverts the release and nothing is paid +(fail-closed). + +Scope boundary. This gate authorizes PAYOUTS. It does NOT make Aere consensus post-quantum. Blocks +remain Besu QBFT with classical secp256k1 validators. What is post-quantum here is the authenticity of +the settlement authorization, not block production. + +Disputed jobs are settled by the arbiter's ruling rather than the happy-path release, so the Falcon +gate applies to the normal accept/finalize/ZK settle paths; arbiter resolution of a disputed job is the +arbiter's authority. + +## Escrow-solvency guarantee + +The contract tracks `totalLiabilities[token]` for every asset: the sum of open job rewards plus posted +bonds in that asset. Every escrow or bond increments it; every payout, refund, or slash decrements it by +the same amount, with effects applied before transfers. The invariant + +``` +balanceOf(contract, token) >= totalLiabilities[token] for every asset +``` + +therefore holds at all times, where `token == address(0)` is native AERE. The public view `isSolvent` +checks it. Rewards settle in native AERE or an allowlisted ERC-20; provider and challenger bonds are +always native AERE, so solvency is tracked per asset. Fee-on-transfer or rebasing reward tokens are +rejected at escrow time (the contract requires the received amount to equal the stated reward). + +The test asserts `isSolvent` (and the raw balance-versus-liability comparison) after every mutating step +of every scenario, including a mixed batch of jobs across all three modes carried to their terminal +states. + +## Fail-closed properties + +- No double-pay. Every job reaches a terminal status (`Paid`, `Refunded`, `Slashed`) exactly once. All + fund-moving entrypoints are reentrancy-guarded and set the terminal status before any transfer. +- No pay-without-proof in ZK_VERIFIED. Settlement happens inside `submitResultZK`, after the gateway + `verifyProof` call. An invalid proof reverts the whole transaction. +- No admin drain. There is no owner and no sweep. The arbiter can only route a DISPUTED job's escrow + between its requester, provider, and challenger. Governance can only flip a token allowlist boolean. + Neither can withdraw escrowed funds. +- Deadlines. A claimed job that misses its deadline without a submission lets the requester reclaim the + reward and slashes the provider bond to the requester. + +## Job lifecycle (summary) + +``` +postJob Open requester escrows reward (+ mode/pqc params) +claimJob Claimed provider posts the required native-AERE bond (0 for ZK) +submitResult Submitted REPLAY / OPTIMISTIC: result bytes emitted, window starts +submitResultZK Paid ZK_VERIFIED: proof verified on-chain, paid in the same tx +acceptResult Paid requester accepts a Submitted result early +finalize Paid anyone, after the window closes with no dispute +dispute Disputed challenger posts a matching bond within the window +resolveDispute Paid/Slashed arbiter rules; a bad result slashes the provider bond to the challenger +cancelJob Refunded requester reclaims an unclaimed job's escrow +reclaimExpired Refunded requester reclaims a claimed job that blew its deadline (bond slashed) +``` + +## Honest status + +- Contract: built and tested. `AereComputeMarketV3.sol` compiles under solc 0.8.23 (the repo standard) + and the 13-case Hardhat suite passes, covering all three modes, the Falcon settlement gate, the ERC-20 + reward path, the solvency invariant, and no-double-pay. +- ZK verification path [VERIFY]: exercised against `MockSp1Verifier`, which mirrors the deployed gateway + semantics (reverts on an invalid proof). The reference verifier is the deployed `SP1VerifierGateway` + at `0x9ca479C8c52C0EbB4599319a36a5a017BCC70628`; wiring V3 to it on mainnet is a deploy-time + constructor argument. +- Falcon settlement path [VERIFY]: exercised against `MockPQCPrecompile` at `0x0AE1`, which parses the + Falcon-512 spec offsets. The real wire encoding is separately KAT-proven in `AerePQCMessageVerifier` + and against the live mainnet precompile. On mainnet 2800 the precompile at `0x0AE1` is live. +- Real compute supply [MEASURE]: real GPU / accelerator supply, the off-chain provers, and the real SP1 + proving are EXTERNAL to this contract. They require actual hardware providers running the reference + provider daemon. This is adoption, not code, exactly like validator decentralization. V3 is the trust + and settlement rail; it does not by itself constitute a live compute market with real providers. +- No new token. Rewards, escrow, bonds, and payment are native AERE or an allowlisted existing ERC-20. +- Not deployed. This contract is built for publication and review. Deployment is founder-gated. diff --git a/AERE-CROSS-CLIENT-DETERMINISM.md b/AERE-CROSS-CLIENT-DETERMINISM.md new file mode 100644 index 0000000..6968a88 --- /dev/null +++ b/AERE-CROSS-CLIENT-DETERMINISM.md @@ -0,0 +1,480 @@ +# Aere Network Cross-Client Determinism + +Technical specification. Chain 2800 (Aere Network mainnet). + +Grounding and consistency: this document is the reproducible proof behind Aere's +client-diversity claim. It is consistent by construction with section 5.5 of +`aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md` (the two clients disagree on state) +and the consensus row of `aerenew/docs/AERE-ARCHITECTURE-MAP.md`. Where those documents +and this one describe the same status, they say the same thing. If they ever diverge, +the engineering spec 5.5 is authoritative and this document is wrong. + +Evidence cited here lives in `aerenew/nethermind-pqc/` (the second-client work and its +proof logs), `aerenew/conformance/` (the executable conformance vector suite), +`aerenew/docs/NETHERMIND-2ND-CLIENT-LIVE-2026-07-17.md`, +`aerenew/docs/DECENTRALIZATION-2ND-CLIENT-RUNBOOK.md`, and +`aerenew/docs/AERE-ENGINEERING-SECURITY-SPEC.md`. + +--- + +## 1. Why cross-client determinism matters, and the honest scope + +### 1.1 A single producing client is a systemic risk + +A blockchain is a deterministic state machine: for one ordered sequence of inputs (the +blocks) there is exactly one correct output (the state). A network that runs a single +client implementation has no independent check on whether that implementation computes +the one correct output. If the sole client has a consensus-relevant bug, the whole +network inherits it, and there is nothing to compare against that would reveal the error +before it is finalized. + +The reference case is the September 2025 Reth halt. A chain whose block production +depended on one implementation stopped when that implementation hit a bug. The failure +was not in the protocol; it was in the monoculture. This is the exact risk Aere's +second-client program exists to retire, and it is the reason `AERE-ENGINEERING-SECURITY-SPEC.md` +section 4.2 records "a single producing client is a demonstrated systemic risk" as the +design driver. + +Aere's live mainnet today runs one production client: a fork of Hyperledger Besu v26.4.0 +(base commit d2032017, JDK 21), the sole producer for all seven QBFT validators. A second, +independent implementation that computes the same state from the same inputs turns "trust +the one client" into "two independent implementations agree", which is a materially +different and stronger assurance. + +### 1.2 What this proves, and what it does not + +The second client is a patched Nethermind 1.39.0 (.NET), chosen for implementation +diversity: a different codebase in a different language, so a consensus-relevant bug in +one is unlikely to exist in the other. A second Besu instance would not be client +diversity, because it would share every Besu bug. + +This document proves one specific property: + +> **State-computation determinism across two independent implementations.** For the same +> chain-2800 inputs, the patched Besu producer and the patched Nethermind client compute +> byte-identical block hashes and byte-identical state roots, and agree on seal validity +> and post-quantum precompile outputs. + +This document does **not** claim any of the following, and the reader should not infer them: + +- It does **not** claim Nethermind is a live producing validator on mainnet. It is not. + Nethermind runs as a non-validating follower and as a cross-check; it takes zero part in + live consensus. Besu remains the sole live producer. +- It does **not** claim client-diverse consensus or a "two-client mainnet". Making + Nethermind a live sealer is a separate, founder-gated, high-risk change documented in + `DECENTRALIZATION-2ND-CLIENT-RUNBOOK.md` Phase B, not started and not authorized here. +- It does **not** claim post-quantum consensus. Consensus is classical secp256k1 ECDSA + QBFT. The post-quantum surface is signatures, accounts, and applications only. This scope + boundary holds throughout every section below. + +The value delivered is real and bounded: two independent implementations demonstrably +compute the same state, so a consensus-relevant divergence between them is detectable +rather than silent. The gap between that assurance and a fully automated live fail-safe +gate is stated plainly in section 4. + +--- + +## 2. The determinism protocol + +This is the method a third party uses to verify cross-client determinism directly. It has +five parts, each an independent check on the same underlying property. Each part states +what is asserted and what evidence supports it. Reproduction commands are in section 5. + +### 2.a Full re-validation to genesis (zero invalid seals) + +**Assertion.** The patched Nethermind re-validates chain-2800 blocks from genesis forward +through its own header-import and seal-validation code path, accepting every genuine header +and asserting zero invalid seals, and rejecting any tampered header. + +**Method.** Nethermind reproduces the genesis exactly +(`0xd86d57a899cbfa580669f0e1c7cd4ae5f525247c3c823f8f75df176a0c5d7f1a`), then for each block +recomputes the QBFT canonical block hash (extraData re-encoded seal-stripped, round kept), +recovers each 65-byte committed seal to a distinct in-set validator address, and requires +the recovered-signer count to meet the QBFT quorum `ceil(2N/3)` (N=7, quorum 5). This runs +inside Nethermind's production `HeaderValidator` / `ISealValidator` seam, subclassed as +`AereQbftHeaderValidator` and `AereQbftSealValidator`, so it is the client's own validation +logic, not a bespoke script. + +**Evidence.** +- `aerenew/nethermind-pqc/QBFT-VALIDATION-2026-07-12.md` and + `aerenew/nethermind-pqc/QBFT-FOLLOWER-2026-07-12.md`: real chain-2800 headers driven + through Nethermind's own `HeaderValidator.Validate()`; genuine headers accepted, four + tamper modes rejected. Vectors in `aerenew/nethermind-pqc/test/AerePqc.Tests/qbft-vectors.json` + (16 real chain-2800 headers). +- Live follower re-validation from genesis forward with zero invalid-seal rejects over the + synced range (section 2.c). + +**Honest boundary.** Header and seal re-validation is proven over sampled real headers and +over the contiguous ranges the follower has synced from genesis. A single unbroken +re-validation across the entire history to current head, asserting zero invalid seals over +all of it, completes when the permanent follower finishes its sync to head. +[VERIFY: at-head, full-history re-validation with a zero-invalid-seal count over the complete +0..head range is pending the permanent follower reaching head; per +`NETHERMIND-2ND-CLIENT-LIVE-2026-07-17.md` section 6 this is an explicit open TODO.] + +### 2.b Byte-identical re-execution (block hash AND state root at each height) + +**Assertion.** Replaying real chain-2800 blocks through both clients yields an identical +block hash **and** an identical state root at each height. State-root identity is the strong +check: it means both implementations executed every transaction, applied every reward and +fee rule, and arrived at the same world state, not merely copied a header. + +**Method.** Full-sync mode (`FastSync/SnapSync/FastBlocks = false`) so every block is +executed and its post-state root is recomputed by the node, then compared against the +reference client's state root at the same height. + +**Evidence.** +- `aerenew/nethermind-pqc/QBFT-GENESIS-SYNC-FIX-2026-07-13.md`: a real Nethermind node + full-syncs from genesis, re-executes all transactions, and every node-computed state root + matches the real chain exactly. Genesis stateRoot + `0x2d2255d41483c22e8a2d51ca18249157e25a47f949e8a6c54552d0f790b7b127`. Spot-checked + read-only against the live chain: + + | height | node-computed stateRoot | live chain-2800 stateRoot | match | + |---|---|---|---| + | 458 | `0xc314d2c3…` | `0xc314d2c3…` | yes | + | 694 | `0xf0a4309e…` | `0xf0a4309e…` | yes | + | 872 | `0xcda2107d…` | `0xcda2107d…` | yes | + | 1661 | `0x44baac17…` | `0x44baac17…` | yes | + | 3000 | `0x44baac178e561fe2…243e8575` | `0x44baac178e561fe2…243e8575` | yes | + + This run is bounded to the first 3000 blocks (22 transactions re-executed), genuine + full-state re-derivation over that range, not a header copy. +- `aerenew/docs/NETHERMIND-2ND-CLIENT-LIVE-2026-07-17.md` section 4: the live permanent + follower matches `rpc.aere.network` on block hash AND state root at heights 1, 100, 1,000, + 10,000, 11,133, and 11,136 (head at check time). + +**Honest boundary.** Byte-identical re-execution is proven over the ranges executed to date +(offline genesis..3000, and the live follower's synced heights). The cross-boundary check at +the AerePQC precompile fork (block 9,189,161) and at current head completes when the +permanent follower crosses that height. +[MEASURE: state-root identity at the fork boundary 9,189,160 and 9,189,161 and at current +head, per `DECENTRALIZATION-2ND-CLIENT-RUNBOOK.md` A.6, is verified once the follower is at +head. A mismatch at or across the boundary would indicate a wrong precompile gate.] + +### 2.c Live follower cross-check + +**Assertion.** A listen-only Nethermind following the live chain over devp2p matches the +live RPC's block hash and state root at each checked height, with zero invalid-seal rejects. + +**Method.** The follower is hardened to be non-validating: no validator key, no `AERE_*` +environment, `eth/68`-only on the wire (the `istanbul/100` QBFT capability is stripped), so +the engine, producer, and importer paths are inert. It peers to nodes under Foundation +control (rpc2 primary, infra secondary), full-syncs from genesis, and its per-height +hash and state root are compared to `rpc.aere.network`. + +**Evidence.** +- `aerenew/docs/NETHERMIND-2ND-CLIENT-LIVE-2026-07-17.md`: the permanent second client + `aere-client2` (a dedicated second-client host, Helsinki, dedicated firewall, + JSON-RPC bound to `127.0.0.1` only, durable `systemd` service). Parity table of hash and + state root MATCH at 1 / 100 / 1,000 / 10,000 / 11,133 / 11,136; zero invalid-seal rejects + in range. +- The first live-devp2p run (recorded in the memory note `client_diversity_2026-07-13` and + the live doc) full-executed genesis to block 182,777 and matched hash and state root at + 1 / 100 / 1,000 / 10,000 / 100,000 / 111,130 / 182,777, with zero divergence in range. + +**Honest boundary.** The follower is a listen-only cross-check, not a validator. As of the +recorded state it is syncing toward head (honest ETA roughly 18 hours from the recorded +start; DB projected near 48 GB at head). +[VERIFY: "at head, tracking within a few blocks of `rpc.aere.network`, zero divergence over a +sustained soak" per runbook A.6/A.7 is the completion criterion and is pending the follower +reaching and holding head.] + +### 2.d Generated edge-case corpus + +**Assertion.** Adversarial and edge-case inputs, run through both clients, widen coverage +beyond organic blocks. Organic chain-2800 blocks are near-empty, so replaying only real +blocks under-exercises the state-transition surface. A generated corpus of adversarial +transactions and malformed inputs closes that gap. + +**Status, split by layer:** + +- **Precompile edge-case corpus: EXISTS.** `aerenew/conformance/conformance-vectors.json` + carries the adversarial precompile surface directly: valid, wrong-key, tampered-signature, + tampered-nonce or message, wrong-header-byte, wrong-length, empty, too-short, + below-minimum, and at-minimum-all-zero cases for each verifier, plus the full vendored NIST + ACVP negative test groups (ML-DSA-sigVer-FIPS204 tg8: 15 records, 3 pass / 12 fail; + SLH-DSA-sigVer-FIPS205 tg31: 14 records, 2 pass / 12 fail) and the SHAKE256 output-length + domain including the over-cap truncation edge. These are the "trap for a second client" + cases and they are pinned as vectors (`aerenew/conformance/README.md`). + +- **Block-level and transaction-level adversarial corpus: [MEASURE], to build.** A dedicated + corpus of adversarial or edge-case transactions (deep call stacks, storage-collision + patterns, gas-edge and revert-edge transactions, EIP-2935 lookback boundary calls, base-fee + floor boundary blocks) executed through both clients with state-root diff at each step does + not yet exist as a committed artifact. It is the corpus to build to widen coverage beyond + organic blocks. [MEASURE: generate an adversarial block/transaction corpus, replay through + both clients, assert identical state root per step; store under `aerenew/conformance/` next + to the precompile vectors.] + +### 2.e PQC precompile parity + +**Assertion.** Both clients produce identical outputs for the same NIST vectors through the +0x0AE1..0x0AE5 precompiles (Falcon-512, Falcon-1024, ML-DSA-44, SLH-DSA-SHA2-128s, SHAKE256). + +**Method.** The five Aere post-quantum precompiles are compiled into a real Nethermind +1.39.0 process via its own `IPrecompileProvider` extension seam (the same interface Optimism +and Taiko use), gated to activate at the fork boundary. NIST KAT and conformance vectors are +driven through the running Nethermind JSON-RPC by `eth_call` and compared byte-for-byte +against the Besu fork's output for the same input. + +**Evidence.** +- `aerenew/nethermind-pqc/REAL-NETHERMIND-PQC-2026-07-12.md`: 27 of 27 NIST-KAT and + conformance vectors pass byte-for-byte via `eth_call` inside a genuine running Nethermind + 1.39.0 (commit `14aca2c5`), matching the Besu 26.4.0 fork. Includes the tampered-signature + negative for each of Falcon-512, Falcon-1024, ML-DSA-44, and SLH-DSA-128s (each returns the + 32-byte zero word, not-verified). +- `aerenew/conformance/`: the executable conformance suite has since grown to 83 precompile + vectors (Falcon-512 x12, Falcon-1024 x12, ML-DSA-44 x22, SLH-DSA-SHA2-128s x21, SHAKE256 + x16), 112 vectors total including QBFT, EIP-2935, and extraData. Last live run: 112/112 + passed against the chain-2800 Besu reference (`aerenew/conformance/README.md`). Note the + distinction: the 27/27 figure is the set re-run byte-for-byte inside the actual Nethermind + process; the 112/112 figure is the full suite confirmed against the live Besu reference by + `runner.mjs`. + +**Precompile fail-closed semantics (both clients must match).** On malformed input the +signature precompiles (0x0AE1..0x0AE4) return a 32-byte zero word (not-verified) and never +revert; SHAKE256 (0x0AE5) returns empty when input is under 32 bytes or `outLen` is zero, and +truncates an over-cap `outLen` to 65536 rather than reverting. A second client that reverts, +or returns empty where the reference returns a zero word, diverges. These semantics are +observed-live, not assumed, and are pinned as vectors. + +**Gate parity (a real divergence trap).** The precompiles must activate at exactly the Aere +fork boundary, block 9,189,161 (the first block with timestamp >= 1783820272), gated by +`chainId == 2800`. An ungated build (active from block 0) would diverge state if any pre-fork +block ever called an `0x0AE*` address as an ordinary account. The permanent follower gates on +the futureEips timestamp in `ReleaseSpec.cs` (`IsAerePqcEnabled`) and +`ChainSpecBasedSpecProvider.CreateReleaseSpec`, verified inactive pre-fork by an `eth_call` +to `0x0AE5` returning `0x` on the pre-fork head versus the SHAKE output on the post-fork head +(`NETHERMIND-2ND-CLIENT-LIVE-2026-07-17.md` section 3). + +--- + +## 3. Existing evidence (byte-identical production and import) + +Beyond the follower and precompile parity above, the second client has been shown to produce +QBFT blocks that the reference client accepts byte-for-byte, and to have that acceptance be +non-vacuous (a tampered seal is rejected). This is the production-encoding half of client +diversity. All of it is on an isolated test network; the live chain, the live validators, and +the infra box were never touched. + +### 3.1 Byte-for-byte block production, then Besu import + +`aerenew/nethermind-pqc/QBFT-PRODUCER-2ND-CLIENT-2026-07-13.md` (with proof log +`proofs/qbft-producer-besu-import-proof-2026-07-13.txt` and +`proofs/qbft-producer-manifest-2026-07-13.json`): + +- **Byte-exact calibration.** Given the same key, genesis, and timestamp, the Nethermind-side + producer's full block RLP is byte-for-byte identical to Besu's `debug_getRawBlock(1)`: 1286 + hex characters equal, including the ECDSA committed seal and the block hash + `0xa34f5e43…f6c616`. +- **Production interop.** The producer sealed 8 empty QBFT blocks; a fresh stock Besu 24.12.2 + node imported all 8 through its real BFT block-validation path (offline `blocks import`, + which runs the same `BftCommitSealsValidationRule` and `MainnetBlockValidator` as live + import). Every imported block hash equals the producer's manifest; miner is the Nethermind + validator address. + +### 3.2 Non-vacuity: a one-byte-tampered seal is rejected + +Same proof, control C: one byte of block 1's committed seal was flipped +(`0x8d -> 0x72`), leaving the block hash unchanged so the check isolates the seal. Genuine +block imported; tampered block rejected by Besu's own rule +(`BftCommitSealsValidationRule | Invalid block header: Not all committers are in the locally +maintained validator list`, `tampered exit: 1`). The 8-block acceptance is therefore genuine +cryptographic agreement, not a rubber stamp. + +### 3.3 Cross-client hash agreement across proposers + +`aerenew/nethermind-pqc/proofs/mixed-client/proposer/01-onchain-alternation-hashmatch.txt`: on +a mixed set, proposers strictly alternate Besu and Nethermind, and the on-chain block hash +computed by the Nethermind node equals the Besu node's hash at every one of 20 consecutive +blocks (NM_hash == Besu_hash, YES, blocks 1..20). At N=4 (2 Besu + 2 Nethermind), all four +nodes agree on the head hash (`proofs/mixed-client/follower-sync/REGRESSION-n4.txt`, 4-way head +hash agreement at block `0x2d`). + +### 3.4 PQC precompile parity inside a real Nethermind + +Section 2.e: 27/27 NIST KAT and conformance vectors byte-for-byte via `eth_call` inside a +running Nethermind, matching the Besu fork +(`aerenew/nethermind-pqc/REAL-NETHERMIND-PQC-2026-07-12.md`); the broader 112/112 conformance +suite against the live Besu reference (`aerenew/conformance/`). + +--- + +## 4. Honest status + +This is the load-bearing honesty section. It states, without rounding up, exactly what is +proven and what is remaining operational work. It matches section 5.5 of +`AERE-ENGINEERING-SECURITY-SPEC.md`; the two must stay consistent. + +**PROVEN, as a validation cross-check.** The second client demonstrably re-derives state +independently and would detect a state divergence. Concretely, it re-validates chain-2800 +headers and seals through its own validation code (accept genuine, reject tampered); +re-executes real blocks to byte-for-byte identical block hashes and state roots (offline over +genesis..3000, and as a live listen-only follower matching the live RPC's hash and state root +at every checked height in range); and produces identical outputs for the five PQC precompiles +on the same NIST vectors. Because there is exactly one definition of correct state and two +independent implementations computing it, a consensus-relevant divergence (a differing state +root, a differing block hash, a differing seal decision) between Besu and Nethermind is +detectable by comparing the two. It does not silently pass. This is real client-diversity +assurance. + +**NOT yet a live automated divergence gate.** The cross-check is not yet wired into production +monitoring as an automated, alerting fail-safe that watches Besu and Nethermind continuously +and raises an alarm on the first byte of divergence. Today the comparison is run and +spot-checked; it is not a continuously-armed live gate. + +**NOT yet a live producing validator.** Nethermind is a non-validating follower and a +cross-check. It takes zero part in live consensus. Besu is the sole live producer on chain +2800. A Nethermind disagreement flags a discrepancy against the producer; it does not arbitrate +consensus, because Nethermind casts no vote and seals no block on mainnet. + +**Behavior on a detected divergence.** This is a fail-safe, not an automatic consensus action. +A detected divergence is a signal to halt and investigate before the divergent block is +trusted, not something that itself forks or halts the live chain. In all adversarial fault +testing to date, zero forks were observed; the chain's failure posture is to halt and later +recover, not to fork. + +**The remaining operational work** is turning the proven cross-check into an automated live +fail-safe gate: a supervised process that continuously reads both clients at head, diffs block +hash and state root per block, and alerts (and gates trust) on the first divergence, with the +permanent follower held at head under a sustained soak. Separately and further out, making +Nethermind a live sealing validator is the founder-gated, high-risk Phase B in +`DECENTRALIZATION-2ND-CLIENT-RUNBOOK.md` (extended mixed-client soak at production shape, +independent audit of the Nethermind QBFT engine, a rehearsed one-block rollback vote, and +fault tolerance preserved by construction), not started and not authorized by this document. + +Public-copy rule that travels with this status: a second independent client follows and +validates live chain 2800 as a non-validating full node. Do not write "client-diverse +consensus", "two-client mainnet", or anything implying the second client seals live blocks. +The Nakamoto coefficient by operator is still about 1; a follower does not change it. Never +claim mainnet consensus is post-quantum; it is classical secp256k1 ECDSA. + +--- + +## 5. Reproduction + +A third party reproduces the differential by building both clients, replaying blocks, and +diffing state roots. Steps that need the fork host or a heavy full-history build are marked +[MEASURE] with the command rather than an asserted fresh number, because the numbers above +were measured on Foundation infrastructure and the point of reproduction is that an independent +party gets the same bytes, not that they trust ours. + +### 5.1 Precompile parity and conformance suite (light, no chain build) + +The executable spec runs read-only against the live reference and needs only `ethers` v6: + +```bash +cd aerenew/conformance +node runner.mjs # validates every vector against the live Besu reference (read-only) +node build-vectors.mjs # regenerates vectors from NIST KATs + real chain-2800 headers +``` + +Expected: all vectors pass; `runner.mjs` re-confirms the live N=7 validator set and the +`validator_set_root` before asserting the QBFT vectors. This reproduces the precompile-output +half of determinism (section 2.e) against the reference without building a client. + +To reproduce the same 27/27 inside a second client rather than against the reference, build +the patched Nethermind (5.2) and drive the vectors through its `eth_call`, per +`aerenew/nethermind-pqc/REAL-NETHERMIND-PQC-2026-07-12.md`. + +### 5.2 Build the two clients + +- **Reference (Besu fork).** Hyperledger Besu v26.4.0, base commit d2032017, JDK 21, plus the + Aere PQC precompile and EIP-2935 fork rules. [MEASURE: build on a scratch box, not infra; + Aere's live producer is not rebuilt for this. See `ops_no_heavy_compute_on_infra`.] +- **Second client (patched Nethermind).** Nethermind 1.39.0 commit `14aca2c5`, .NET SDK + 10.0.30x, with the in-tree `Nethermind.AerePqc` project applied: + + ```bash + cd aerenew/nethermind-pqc/nethermind-intree + ./apply.sh && ./apply2.sh && ./apply3.sh # precompiles + release-spec gate + # for the header/seal follower add through apply9.sh; for the producer path add apply5.sh + dotnet build src/Nethermind/Nethermind.Runner -c Release + ``` + + For the non-validating follower build, exclude the istanbul-dependent QBFT engine and the + producer so the binary is `eth/68`-only, and leave `AERE_PRODUCER_KEY` and `AERE_QBFT_KEY` + unset (this is the invariant that keeps it non-validating). Gate the precompiles on the + futureEips timestamp so they activate at block 9,189,161, not block 0. + +### 5.3 Full re-validation to genesis (2.a) + +Start the follower in full-sync from genesis against a node under your control and confirm +zero invalid-seal rejects in the logs: + +```bash +# config: chainspec with the reproduced genesis 0xd86d57a8…0c5d7f1a, +# --Sync FullSync (FastSync/SnapSync/FastBlocks = false), static peer to a Besu node, +# discovery off, RPC bound to 127.0.0.1 +dotnet Nethermind.Runner.dll --config aere-live-config.json +``` + +[MEASURE: full-history re-validation to head with a zero-invalid-seal count over 0..head +requires the multi-hour full-history sync on the fork host; assert the count once the follower +is at head.] + +### 5.4 Byte-identical re-execution, diff the state roots (2.b) + +For each checked height, pull the state root from both clients and diff. Read-only, via each +client's own RPC (the follower on `127.0.0.1:8545`, the reference on its node RPC): + +```bash +for h in 1 100 1000 10000 3000; do + a=$(cast rpc eth_getBlockByNumber $(printf '0x%x' $h) false --rpc-url http://127.0.0.1:8545 | jq -r .stateRoot) + b=$(cast rpc eth_getBlockByNumber $(printf '0x%x' $h) false --rpc-url | jq -r .stateRoot) + [ "$a" = "$b" ] && echo "$h stateRoot MATCH" || echo "$h stateRoot DIVERGE a=$a b=$b" +done +``` + +Do the same for `.hash` (block hash) at each height. Expected: MATCH at every height, per the +tables in section 2.b. + +[MEASURE: extend the height list across the fork boundary (9,189,160 and 9,189,161) and to +current head once the follower has executed past 9,189,161. A mismatch at or across the +boundary indicates a wrong precompile gate; stop and fix.] + +**baseFee reproduction trap.** Compare state roots and block hashes against a raw Besu node, +not the public `rpc.aere.network`. The public RPC is behind a proxy that overwrites +`baseFeePerGas` with a constant 1 Gwei for display; that shimmed value does not reproduce the +real block hash for blocks whose true base fee differs. A client reading directly from a Besu +node gets the true consensus value and needs no override (`aerenew/conformance/README.md`, +baseFee shim caveat). + +### 5.5 Production interop and tamper control (3.1, 3.2) + +On an isolated testnet, have the Nethermind-side producer seal a short chain and import it with +a stock Besu, then repeat with one seal byte flipped: + +```bash +# produce N blocks -> nm-blocks.rlp (isolated chainId, single validator), then: +besu --data-path blocks import --from nm-blocks.rlp # expect exit 0, all hashes match the manifest +# flip one byte of a committed seal, re-import -> expect BftCommitSealsValidationRule rejection, exit 1 +``` + +Expected: genuine chain imports with byte-identical hashes; the tampered chain is rejected by +Besu's own BFT rule. This is the non-vacuity control, reproduced from +`aerenew/nethermind-pqc/QBFT-PRODUCER-2ND-CLIENT-2026-07-13.md`. + +### 5.6 Live follower cross-check (2.c) + +Run the non-validating follower against the live chain and diff hash and state root against a +raw live node at a spread of heights: + +[MEASURE: the live follower cross-check at head requires the follower to be fully synced (honest +ETA roughly 18 hours) and peered to a live node; assert per-height hash and state-root MATCH and +zero divergence over a sustained soak per `DECENTRALIZATION-2ND-CLIENT-RUNBOOK.md` A.6 and A.7.] + +--- + +## 6. Summary + +Two independent implementations, in different languages, compute the same chain-2800 state: +identical block hashes, identical state roots, matching seal decisions, and byte-for-byte +identical post-quantum precompile outputs, with a tampered seal provably rejected. That is +proven as a validation cross-check. It is not yet a continuously-armed automated live +divergence gate, and Nethermind is not yet a live producing validator; those are the remaining +operational and founder-gated steps. The claim this document supports is precise and defensible: +Aere's client-diversity assurance is a demonstrated, reproducible cross-check on state +computation, not a marketing line, and its boundaries are stated in the same words as the +engineering spec it is consistent with. diff --git a/AERE-DEPLOY-RUNBOOK-SUMMARY.md b/AERE-DEPLOY-RUNBOOK-SUMMARY.md new file mode 100644 index 0000000..9b7c4b1 --- /dev/null +++ b/AERE-DEPLOY-RUNBOOK-SUMMARY.md @@ -0,0 +1,55 @@ +# Summary: AERE-NEW-CONTRACTS-DEPLOY-RUNBOOK.md + +Deliverable written to `aerenew/docs/AERE-NEW-CONTRACTS-DEPLOY-RUNBOOK.md`. Covers 17 new founder-gated +contracts, read directly from source under `aerenew/contracts/contracts/`. Nothing is deployed; every one +is founder-gated (confirmed: none has a `deployments/*.json` entry, none in `sdk-js/src/addresses.ts`). + +## Method +- Read every contract's real constructor. +- Cross-referenced live addresses from `sdk-js/src/addresses.ts` and precompiles from + `docs/AERE-EIP-COMPATIBILITY-MATRIX.md` (0x0AE1 Falcon-512, 0x0AE3 ML-DSA-44, both live block 9,189,161). +- Mapped per-contract risk from `docs/AERE-SECURITY-REVIEW-NEW-CONTRACTS.md` + `AERE-SECURITY-FIXES.md`. +- Named the Hardhat test file for each contract. + +## Live wiring addresses used +- SP1VerifierGateway 0x9ca479C8c52C0EbB4599319a36a5a017BCC70628 +- AerePQCKeyRegistry 0x1eCa3c5ADcBD0b22636D8672b00faC6D89363691 +- AereAgentDID 0xce641d7d7C10553D82b06B7C21d423550e7522C5 +- AereAIReputation 0x781ef746c08760aa854cDa4621d54db6734bfeBF +- AerePQCAccountFactory 0xd5315Ea7caa60d320c4f34b1bEd70dd9cc02CE58 (runtime ref for migrator) +- AERE402FacilitatorV2 0xFC2f7FAa94919caF1126b3c995F0F6AcCef291de +- Foundation 0x0243A4f47D44b40b65D33f20329dE20D00c6f3C3 +- Deployer 0xbeB33D20dFBBD49eC7AC1F617667f1f02dfd6465 + +## Deploy order (topological) +Wave A (no sibling dep): AereAccountMigrator, AereRandomnessBeaconV2, AereRecoveryRegistry, +AereDestinationSettler, AerePQAttestationKeyRegistry, AereBitstringStatusList(0), AereIdentityRegistry8004(DID), +AereValidationRegistry8004(reg,DID), AereAP2MandateVerifier(reg,executor), AereTrustRegistry(reg), +AereVectorStore(facilitator), AereComputeMarketV3(gateway,arbiter,governance). +Wave B: AereReputationRegistry8004(reputation, identity=A7), AereVerifiableCredential(trust=A10, statusList=A6). +Wave C (circuit-gated): AerePQAggregateVerifier(gateway, aggVkey), AereFinalityCertificateVerifier(gateway, finVkey, registry=A5). +Wave D: AerePQAggregateModule(verifier=C1). + +## Gate buckets +- Deploy-when-ready (low risk): Migrator, RandomnessBeaconV2, RecoveryRegistry, DestinationSettler, + IdentityRegistry8004, ValidationRegistry8004, VerifiableCredential, BitstringStatusList, VectorStore. +- Founder-config/action before useful: AP2 (executor), TrustRegistry (owner+accredit), + ReputationRegistry8004 (attestor grant + owner), AttestationKeyRegistry (enroll+keys), ComputeMarketV3 + (arbiter+governance). +- External-audit-gated (fund flow, strongest = ComputeMarketV3): also recommended for VectorStore, + DestinationSettler, AccountMigrator. +- MUST NOT deploy until a circuit exists: AerePQAggregateVerifier, AereFinalityCertificateVerifier, + AerePQAggregateModule, and the zk non-revocation path of AereBitstringStatusList. + +## [VERIFY] items at deploy +- AP2 settlementExecutor (non-zero, required in prod; L3). +- ReputationRegistry8004 reputation instance for write-through (new instance listing the adapter). +- VectorStore facilitator (AERE402FacilitatorV2; confirm settle ABI). +- ComputeMarketV3 arbiter + governance (Foundation recommended). +- vkeys (immutable, circuit not built): AerePQAggregateVerifier.aggregateProgramVKey, + AereFinalityCertificateVerifier.programVKey, AereBitstringStatusList.setNonRevocationVKey. + +## Security-review carry-through +No CRITICAL/HIGH. M1 (reputation write gate) fixed, L1 x3 (code-less-gateway guard) fixed in +AerePQAggregateVerifier/AereComputeMarketV3/AereBitstringStatusList, L2 (vector-store receipt-provider bind) +fixed, L3 (AP2 open-path replay) documented as accepted risk closed by the executor gate. diff --git a/AERE-EIP-COMPATIBILITY-MATRIX.md b/AERE-EIP-COMPATIBILITY-MATRIX.md new file mode 100644 index 0000000..1200ad3 --- /dev/null +++ b/AERE-EIP-COMPATIBILITY-MATRIX.md @@ -0,0 +1,126 @@ +# Aere Network: Ethereum EIP Compatibility Matrix + +**Chain:** Aere Network mainnet, chain ID 2800 (`0xaf0`). Execution client: Hyperledger Besu 26.4.0 with QBFT consensus (classical secp256k1 ECDSA, N=7 validators, f=2), approximately 0.5 second blocks. This document is a developer reference: it states, EIP by EIP, where Aere's EVM matches Ethereum mainnet and where it deliberately differs. + +Aere tracks Ethereum's hard forks so that its EVM surface matches mainnet at the same addresses and opcodes: London and Shanghai apply from genesis, Cancun and Prague (Pectra) activated together at block 2,075,363, and Osaka (Fusaka) at block 2,106,606. A small set of deviations is intentional and disclosed here, because Aere is a QBFT chain with no separate beacon (consensus) layer and no blob data availability market. Anything not matching Ethereum is a design decision, not an oversight, and each is called out in the matrix and again in the deviations recap at the end. + +## How to read this + +- **Status** is one of: **Supported** (matches Ethereum), **Partial** (present but materially limited on Aere), **Not implemented** (absent), **No-op** (present in the ruleset but neutralized, returns a defined zero/empty value under QBFT). +- Every row is intended to be literally true. Cells that could not be verified against the repository's genesis or fork configuration carry an explicit **[VERIFY: ...]** note for a human to confirm before publication. +- "The fork" or "the AerePQC hard fork" refers to Aere's client-only Besu `futureEips` milestone (`futureEipsTime = 1783820272`), which activated at block 9,189,161 (2026-07-12) and bundled the native post-quantum precompiles, the EIP-2935 write path, and EIP-7939. No re-genesis was involved. + +### Fork timeline on chain 2800 + +| Ethereum fork | Aere activation | Notes | +|---|---|---| +| London, Shanghai | Genesis (block 0) | `londonBlock: 0`, `shanghaiTime: 0` in genesis config | +| Cancun + Prague (Pectra) | Block 2,075,363 | `cancunTime == pragueTime == 1780189051`; Cancun and Prague share one activation instant on Aere | +| Osaka (Fusaka) | Block 2,106,606 | `osakaTime == 1780220351` | +| AerePQC milestone (post-Osaka) | Block 9,189,161 | Besu `futureEipsTime == 1783820272`; PQC precompiles + EIP-2935 write path + EIP-7939 | + +[VERIFY: block heights 2,075,363 and 2,106,606. The genesis config gates Cancun/Prague/Osaka by timestamp (1780189051 / 1780189051 / 1780220351), not by block number, so these heights are the observed first-block-past-timestamp and should be confirmed against the live chain's head history.] + +--- + +## The Matrix + +### London and Shanghai era (active from genesis) + +| EIP | Name | Status | Difference from Ethereum | +|---|---|---|---| +| 1559 | Fee market (base fee, type-2 txs) | Partial | Fee-market mechanics present, plus a 1 Gwei base-fee floor live since block 10,141,734 (raised the real minimum from 7 wei). Aere adds no consensus base-fee burn narrative: its "burn" is a separate validator-reward cut (see deviations). [VERIFY: base-fee disposal on chain 2800, whether the 1559 base fee is protocol-burned as on Ethereum or credited.] | +| 3198 | BASEFEE opcode | Supported | Returns the current base fee, which is floored at 1 Gwei (see EIP-1559). | +| 3529 | Reduction in refunds | Supported | Matches Ethereum. | +| 3541 | Reject contract code starting with 0xEF | Supported | Matches Ethereum. Reserves the 0xEF lead byte (the EOF prefix). | +| 3651 | Warm COINBASE | Supported | Matches Ethereum. | +| 3855 | PUSH0 instruction | Supported | Matches Ethereum. | +| 3860 | Limit and meter initcode | Supported | Matches Ethereum. | +| 4895 | Beacon chain push withdrawals as operations | No-op | Withdrawal-operation ruleset present, but Aere has no beacon layer to originate withdrawals, so none are produced. | + +### Cancun (block 2,075,363) + +| EIP | Name | Status | Difference from Ethereum | +|---|---|---|---| +| 1153 | Transient storage (TLOAD / TSTORE) | Supported | Matches Ethereum. | +| 4844 | Shard blob transactions | Partial | Type-3 blob transactions are present in the EVM, but Aere runs no blob data-availability market, so blobs carry no fee and are not served/persisted as on Ethereum. See EIP-7516. | +| 4788 | Beacon block root in the EVM | No-op | The beacon-root ring buffer returns 0x0: a QBFT chain has no separate beacon/consensus layer to expose a root from. | +| 5656 | MCOPY instruction | Supported | Matches Ethereum. | +| 6780 | SELFDESTRUCT only in same transaction | Supported | Matches Ethereum. | +| 7516 | BLOBBASEFEE opcode | No-op | Returns 0: there is no blob market, so there is no blob base fee. | + +### Prague / Pectra (block 2,075,363) + +| EIP | Name | Status | Difference from Ethereum | +|---|---|---|---| +| 2537 | BLS12-381 curve precompiles | Supported | Matches Ethereum. | +| 2935 | Save historical block hashes in state | Supported | Standard 8191-block history-storage ring buffer at `0x0000F90827F1C53a10cb7A02335B175320002935`, written by consensus. Nominally listed at Pectra but the system contract was not populated on mainnet until the AerePQC fork (block 9,189,161) added the write path; from that block `eth_getCode` returns the canonical runtime and the 8191-block window is live. | +| 6110 | Supply validator deposits on chain | Partial | The deposit-request ruleset is part of the Pectra parity Aere tracks, but Aere has no beacon layer to consume deposits, so a deposit does not create or fund a QBFT validator (the validator set is QBFT-managed). [VERIFY: whether the deposit system contract is actually populated on mainnet 2800; EIP-2935's contract was not populated until block 9,189,161, so this must be checked directly.] | +| 7002 | Execution-layer triggerable withdrawals/exits | Partial | Withdrawal-request ruleset present, but no beacon layer consumes exits, so it does not affect the QBFT validator set. [VERIFY: system contract populated on mainnet; header requests handling.] | +| 7251 | Increase MAX_EFFECTIVE_BALANCE (consolidations) | Partial | Consolidation-request ruleset present, but no beacon layer to act on it under QBFT. [VERIFY: system contract populated on mainnet.] | +| 7549 | Move committee index outside signature | Not implemented | Beacon consensus-layer change only, with no execution-layer/EVM surface. It has no applicability under QBFT. | +| 7623 | Increase calldata cost | Supported | Matches Ethereum (calldata floor-cost accounting). | +| 7685 | General purpose execution layer requests | Partial | The requests framework (the umbrella for 6110/7002/7251) exists in the ruleset, but Aere has no beacon layer to consume the requests. [VERIFY: whether mainnet block headers carry a non-empty requests hash and the request system contracts are populated.] | +| 7702 | Set EOA account code (delegation) | Supported | Matches Ethereum. This is the EOA-delegation primitive Aere carries (and the reason EIP-3074 is not needed). | +| 7691 | Blob throughput increase | Partial | The blob schedule is raised at Prague (target 6, max 9) in config, but with no blob data-availability market the increase has no practical effect. | + +### Fusaka / Osaka (block 2,106,606) and the post-Osaka milestone + +| EIP | Name | Status | Difference from Ethereum | +|---|---|---|---| +| 7825 | Transaction gas limit cap (2^24 = 16,777,216) | Supported | Matches Ethereum; the per-transaction gas cap is enforced on chain 2800 (real transactions have executed under it). | +| 7939 | Count leading zeros (CLZ) opcode | Supported | Present. On Aere it activated at the post-Osaka AerePQC milestone (block 9,189,161), which the live EIP-2124 fork-id folds in. [VERIFY: activation height for 7939 specifically, confirmed against the live fork schedule.] | +| 7594 | PeerDAS (peer data availability sampling) | Not implemented | No active role under QBFT: Aere runs no blob data-availability market, so there is no data-availability sampling role to perform. | +| 7805 | FOCIL (fork-choice enforced inclusion lists) | Not implemented | No-op under QBFT: there is no fork-choice or proposer-inclusion layer to enforce inclusion lists against. | +| 7692 | EOF (EVM Object Format) mega-set | Not implemented | Not activated under the current ruleset; the 0xEF prefix stays reserved by EIP-3541 (legacy behavior). [VERIFY: confirm the AerePQC `futureEips` protocol spec (futureEipsTime = 1783820272, block 9,189,161) does NOT enable the EOF opcode set or EIP-3540/3670 container validation. Corroboration that EOF is off: the served genesis config and the Nethermind live-sync fork-id mirror both carry no EOF transition, and the engineering spec states EOF is not activated. The one residual risk is that this milestone rides Besu's `futureEips` key, which in stock Besu is EOF's staging ground, so the fork build's spec definition should be inspected to confirm EOF was not pulled in.] | + +### Superseded + +| EIP | Name | Status | Difference from Ethereum | +|---|---|---|---| +| 3074 | AUTH / AUTHCALL (sponsored EOA actions) | Not implemented | Deliberately absent. It was superseded by EIP-7702, which Aere carries as its EOA-delegation primitive. | + +--- + +## Aere additions beyond Ethereum + +These are callable addresses that are not part of the base Ethereum mainnet precompile set. The post-quantum band `0x0AE1`..`0x0AE5` is genuinely Aere-specific and live on mainnet; `0x0AE6`..`0x0AE8` are not on mainnet; the secp256r1 precompile at `0x100` is a shared RIP that Ethereum is standardizing in Osaka (listed here because it sits outside the classic precompile set). + +| Address | Name | Status | Notes | +|---|---|---|---| +| `0x0AE1` | Falcon-512 signature verify | Live on mainnet | Activated at block 9,189,161 (AerePQC fork). Thin wrapper over Bouncy Castle 1.83; NIST KAT verified. | +| `0x0AE2` | Falcon-1024 signature verify | Live on mainnet | Activated at block 9,189,161. NIST KAT verified. | +| `0x0AE3` | ML-DSA-44 signature verify (FIPS 204) | Live on mainnet | Activated at block 9,189,161. ACVP verified. | +| `0x0AE4` | SLH-DSA-SHA2-128s signature verify (FIPS 205) | Live on mainnet | Activated at block 9,189,161. ACVP verified. | +| `0x0AE5` | SHAKE256 (FIPS 202) | Live on mainnet | Activated at block 9,189,161. | +| `0x0AE6` | ML-KEM-768 encapsulation (FIPS 203) | Testnet only | Built and ACVP-verified (25/25) on an isolated QBFT testnet. NOT on mainnet 2800; a mainnet staticcall hits an empty account and returns empty. Founder- and audit-gated. | +| `0x0AE7` | Falcon HashToPoint (SHAKE256 sampler) | Testnet only | Built and KAT-verified (12/12) on isolated testnet. NOT on mainnet 2800. Founder- and audit-gated. | +| `0x0AE8` | BabyBear/FRI STARK verify (skeleton) | Reference skeleton only | Non-working, fail-closed by construction (returns empty for every input). Not deployed on mainnet and explicitly must not be activated until the crypto core is ported. Scope caveat (2026-07-19 finding): the generic components confirmed so far verify BabyBear + FRI STARKs (Aere's OWN Plonky3 circuits), NOT SP1 6.1.0, which is Hypercube (KoalaBear multilinear); retargeting to SP1 6.1.0 is a separate ~22 to 32 person-week effort. See `AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`. | +| `0x100` | P256Verify / secp256r1 (RIP-7212 / RIP-7951) | Live on mainnet | Native P-256 signature verification for passkeys/WebAuthn at a fixed cost of about 3,450 gas. Active from the Osaka/Fusaka ruleset. Note: this is a shared Rollup Improvement Proposal being standardized into Ethereum's Osaka, so it is standards-aligned rather than Aere-proprietary. | + +All post-quantum precompiles are signature/hash/KEM verifiers on the EVM path. None of them make Aere's consensus post-quantum: mainnet 2800 still seals blocks with classical secp256k1 QBFT. + +--- + +## Deliberate deviations recap + +The intentional differences from Ethereum, all a consequence of Aere being a QBFT chain with no beacon layer and no blob market: + +1. **Base fee floor plus a validator-reward burn, not a consensus base-fee burn.** Aere applies a 1 Gwei EIP-1559 base-fee floor (live since block 10,141,734). Separately, Aere's "burn" is a cut of the validator coinbase block reward (37.5% under the current configuration, hard-capped at 50%), routed through the `AereCoinbaseSplitterV2` splitter into immutable destinations. This must not be described as a base-fee burn. +2. **EIP-4844 blobs present, EIP-7516 BLOBBASEFEE returns 0.** Blob transactions exist in the EVM, but there is no blob data-availability market, so the blob base fee is 0. +3. **EIP-4788 parent beacon block root returns 0x0.** A QBFT chain has no separate beacon/consensus layer to source a root from. +4. **EIP-3074 not implemented, superseded by EIP-7702.** EIP-7702 is the EOA-delegation primitive Aere carries. +5. **PeerDAS (EIP-7594), FOCIL (EIP-7805), and EOF (EIP-7692) have no active role under QBFT.** PeerDAS has no data-availability role (no blob market), FOCIL has no fork-choice/proposer-inclusion layer to enforce, and EOF is not activated under the current ruleset (0xEF stays reserved by EIP-3541). +6. **Validator-lifecycle requests (EIP-6110/7002/7251/7685) have no beacon consumer.** The requests ruleset is tracked for Pectra parity, but Aere's validator set is QBFT-managed, so deposits/withdrawals/consolidations do not drive it. +7. **EIP-2935 became functionally live at the AerePQC fork (block 9,189,161), not at Pectra.** The Pectra ruleset nominally listed it, but the history-storage contract was not populated on mainnet until the write path shipped in the AerePQC fork. + +--- + +## Open [VERIFY] flags for the human before external publication + +1. **Pectra/Fusaka block heights (2,075,363 / 2,106,606).** Genesis gates these by timestamp, not block number. Confirm the heights against the live chain's head history. +2. **EOF off under `futureEips`.** Confirm the AerePQC `futureEips` protocol spec (futureEipsTime = 1783820272, block 9,189,161) does not enable the EOF opcode set / EIP-3540/3670 container validation. Served genesis, the Nethermind fork-id mirror, and the engineering spec all indicate EOF is off; inspect the fork build's spec definition to close the loop, since the milestone rides Besu's `futureEips` key (EOF's usual staging ground in stock Besu). +3. **EIP-1559 base-fee disposal.** Confirm whether the 1559 base fee is protocol-burned (as on Ethereum) or credited on chain 2800. The documented Aere "burn" is a separate validator-reward cut, so the base-fee disposal itself should be stated precisely. +4. **Validator-lifecycle request contracts (6110/7002/7251/7685).** Verify whether the deposit/withdrawal/consolidation system contracts are actually populated on mainnet (EIP-2935's contract was not populated until block 9,189,161) and whether mainnet block headers carry a requests hash. Regardless of the outcome, no beacon layer consumes these requests, so the "Partial" status and the no-effect-on-validator-set caveat hold. +5. **EIP-7939 activation height.** Confirm CLZ activated at the post-Osaka AerePQC milestone (block 9,189,161) rather than at Osaka (block 2,106,606); the Nethermind live-sync mirror maps it to the post-Osaka boundary. +6. **P256Verify framing.** Confirmed at `0x100`, about 3,450 gas, from the Osaka/Fusaka ruleset (RIP-7212 / RIP-7951). Noted as standards-aligned rather than Aere-proprietary; keep that framing if publishing under an "additions" heading. diff --git a/AERE-ENGINEERING-SECURITY-SPEC.md b/AERE-ENGINEERING-SECURITY-SPEC.md new file mode 100644 index 0000000..53c8e2b --- /dev/null +++ b/AERE-ENGINEERING-SECURITY-SPEC.md @@ -0,0 +1,313 @@ +# Aere Network Engineering and Security Specification + +**Status:** Internal draft for adversarial review and for the external audit that follows. Every claim is meant to be checkable against the repository, the live chain (chain ID 2800), or the cited formal-verification artifacts. This document is internally verified and adversarially self-reviewed; it is not yet externally audited. Read every guarantee as "internally verified, not externally attested" until an independent audit completes. + +A single framing statement governs the entire document and is repeated because it is the most common thing to get wrong about Aere: smart contracts and accounts on Aere can verify post-quantum signatures (Falcon, ML-DSA, SLH-DSA) through live EVM precompiles; consensus remains classical ECDSA / QBFT, and the on-chain zero-knowledge verifiers remain classical BN254 pairing checks. Aere is post-quantum at the signature and precompile layer and classical at the consensus and ZK verification layers. The chain as a whole is not post-quantum, and this document never claims it is. + +--- + +## Engineering Principles + +Aere Network is built on a small set of engineering principles. This chapter is not marketing: each principle is stated with the evidence that backs it, and where a principle is an aspiration not yet fully earned, that is said plainly. A principle without evidence is a slogan, and the point of this document is to avoid slogans. + +### Principles we hold and can demonstrate today + +- **Fail closed.** A component that cannot do its job safely refuses rather than guesses. The post-quantum precompiles return a not-verified result (a 32-byte zero word, or empty for the hash function) on malformed or invalid input; they never return a false accept and never revert consensus. (See Section 1.2 and Section 5.) +- **No admin on the economic core.** The value-bearing core (AereSink, the burn vault, sAERE) is ownerless and immutable: a repository-wide sweep of the deployed set finds no owner-withdraw, no upgrade proxy, no selfdestruct, no delegatecall. This is the honest, checkable form of the claim. It is deliberately not a blanket "no admin backdoors anywhere": operational contracts (the NAV oracle, compliance screening, the currently-inert governance) have explicit, documented Foundation roles, and hiding that would be the opposite of this principle. (See Section 1.6 and Section 1.7.) +- **Least privilege.** Every Foundation role that does exist is bounded and documented: the NAV oracle can only propose, dismiss, and attest, and cannot alter an attested snapshot; a program registry can disable a malicious program but cannot invalidate already-recorded proofs. (See Section 1.7.) +- **Determinism over cleverness.** Every precompile is a pure function of its input bytes, reading no chain state and no nondeterministic source, so all nodes compute the identical result and gas charge. Across all adversarial fault testing to date, zero forks were observed: the chain halts and recovers rather than forking. (See Assumption A-10 and Section 5.) +- **Formal verification preferred.** Safety-critical properties are machine-checked, not argued in prose: z3 SMT models of consensus locking and of the escrow and threshold-custody invariants (125 proved properties plus 49 counterexample negative controls at last count), Halmos and Solidity SMTChecker symbolic checking, and 22 invariant-property fuzz suites over the burn, economics, and custody contracts. (See Assumption A-11.) +- **Backward compatibility first.** The EVM, Solidity, bytecode, and JSON-RPC are unchanged; differentiation is added at standard extension points (precompiles at reserved addresses, client-only forks). EIP-7702 is the in-place bridge for existing accounts rather than a compatibility-breaking redesign. (See Section 4.) +- **Security over performance.** The choices that trade performance for safety are deliberate: deterministic QBFT finality over a higher-throughput probabilistic protocol, and keeping the burn out of the consensus-critical path so a policy change cannot halt the chain. + +### Principles we are still earning (stated honestly, not yet claimed as achieved) + +- **Open, reproducible benchmarks.** We are moving toward publishing every benchmark, test, and vector so any third party can reproduce them. This is in progress, not done. Until the repositories and harness are public and the measured coverage number is published, we do not claim it as achieved. +- **Reproducible builds.** A verifiable source-to-SHA256 build of the client and contracts is a roadmap item, not a present guarantee. +- **Independent audit.** Every guarantee in this document is internally verified and adversarially self-reviewed, but not yet externally audited. This document is the bridge to that audit. + +--- + +## 1. Threat Model per Subsystem + +Each subsystem below lists what an attacker could realistically attempt and what actually defends against it, including the cases where the defense is a disclosed limitation rather than a cryptographic or economic guarantee. + +### 1.1 Consensus (QBFT) + +Aere runs Hyperledger Besu (Java, 26.4.0 line) with QBFT, a partially-synchronous BFT protocol. Blocks target roughly 0.5 s. Validator identity is by ECDSA public-key recovery (`ecrecover`) over secp256k1: each committed seal is a 65-byte recoverable signature and the signer address is recovered from it, so there is no stored validator public key at verification time. The live validator set is N = 7, and at N = 7 the QBFT quorum is `ceil(2N/3) = 5` and the Byzantine fault bound is `f = 2`. + +Attacker goals and defenses: + +- **Forge a block or seal without a validator key.** Defended by ECDSA seal recovery plus the requirement that every recovered committer be a member of the stored validator set, with a per-block quorum of 5 distinct committers. Forgery reduces to forging secp256k1 ECDSA, which is classically hard. It is not quantum-hard: a cryptographically-relevant quantum computer running Shor breaks the seal signature, which is the central reason consensus is described honestly as classical, not post-quantum. +- **Equivocate or split the chain (safety attack).** QBFT tolerates up to `f = 2` Byzantine validators at N = 7 with safety unconditional (no fork) under the standard BFT bound. Beyond 2 Byzantine validators (more than one third), safety is lost: a 3-of-7 collusion can violate agreement. This is a hard bound, not a soft target. +- **Stall the chain (liveness attack) at the fault boundary.** With exactly 2 validators down, all 5 survivors must prepare and commit with zero slack. QBFT round-robin proposer selection plus a doubling round-change timeout means an unlucky proposer sequence can exceed a fixed measurement window before an alive proposer's round succeeds. Adversarial soak testing on an isolated testnet (100 kill-2-of-7 cycles: 40 mixed-client RT=4, 40 mixed-client RT=1, 20 pure-Besu) recorded 0 forks and 100/100 self-resync, with a rare (about 5 percent), temporary, self-healing zero-progress window at the exact f = 2 boundary. That tail is inherent to partially-synchronous BFT (FLP: liveness is eventual, not bounded-time, at the boundary) and was not removable by timeout tuning. It is not a fork and not a permanent halt. +- **Grind proposer selection or exploit locking.** IBFT 2.0 locking (retain the prepared block and prepare-certificate, carry it in round-change, re-propose the justified block) is the property that prevents a stale or conflicting proposal from being committed across a round change. It is formally modeled (`formal-consensus/qbft_locking_smt.py`) and enforced by the live Besu producer. +- **The centralization threat itself.** All 7 validators are Foundation-operated. The Nakamoto coefficient is therefore approximately 1: a single operator (the Foundation) can in principle halt or, if it chose to run more than 2 equivocating nodes, break safety. This is the single most important limitation in this document. It is disclosed, not hidden, and is not mitigated by cryptography; the only present mitigation is operator honesty plus a public decentralization roadmap. See Assumption A-3. +- **Second-client cross-check.** A patched Nethermind validates live chain 2800, runs the PQC precompiles, and produces byte-identical QBFT blocks that stock Besu accepts (demonstrated offline via block import, not yet as a live devp2p producer). It currently acts as a client-diversity fail-safe cross-check. It is not a live producing validator, and until the IBFT locking findings are implemented in its engine and soak-verified against an active-Byzantine scenario, it is safe only as an observing or voting participant below the `q - f` threshold, not as a producer. + +### 1.2 Post-Quantum Precompiles + +Five signature and hash precompiles are live on mainnet (activated at block 9,189,161) at the address band `0x0AE1`..`0x0AE5`: Falcon-512 (`0x0AE1`), Falcon-1024 (`0x0AE2`), ML-DSA-44 (`0x0AE3`), SLH-DSA-SHA2-128s (`0x0AE4`), and SHAKE256 (`0x0AE5`). Two further precompiles, ML-KEM-768 (`0x0AE6`) and Falcon HashToPoint (`0x0AE7`), are built and KAT-verified on an isolated testnet only and are not activated on mainnet (activation is founder-gated). A STARK-verify precompile design at `0x0AE8` is a reference skeleton, not a working verifier, and is not activated anywhere. All implementations use Bouncy Castle (`bcprov-jdk18on-1.83.jar`) on the client classpath. Measured marginal verify cost: Falcon-512 40,000 gas, Falcon-1024 75,000 gas, ML-DSA-44 55,000 gas, SLH-DSA-SHA2-128s 350,000 gas, SHAKE256 60 gas base plus 12 gas per word. + +Attacker goals and defenses: + +- **Crash a node or split consensus with malformed input.** A precompile that panicked or behaved non-deterministically on adversarial bytes would be a consensus fault, since every node must compute the identical result and gas charge. The behavior is fail-closed and was verified against the live chain: the signature verifier precompiles (`0x0AE1` through `0x0AE4`) return a 32-byte zero word (read as "not verified") on any signature that does not verify or on malformed input, and SHAKE256 (`0x0AE5`) returns empty on malformed framing; none of them revert. The two non-signature precompiles are additionally source-verified fail-closed: `MLKEM768PrecompiledContract` and `HashToPointPrecompiledContract` catch every `Throwable` and return `Bytes.EMPTY`. (An earlier AIP design draft framed malformed input as "must revert and consume all gas"; that framing was reconciled to the actual as-shipped fail-closed behavior.) +- **Forge a post-quantum signature.** Defended by the NIST-standardized schemes themselves (Falcon, FIPS 204 ML-DSA, FIPS 205 SLH-DSA) as implemented by Bouncy Castle, validated bit-for-bit against official NIST KAT / ACVP vectors committed to the repository, in both accept and crafted-invalid directions. Soundness rests on the NIST PQC hardness assumptions and on the correctness of the Bouncy Castle implementation (Assumptions A-6, A-7). +- **Substitute a weaker curve or downgrade.** The precompile at a given address implements one fixed scheme and parameter set; there is no in-band algorithm negotiation, so there is no downgrade surface at the precompile itself. Algorithm agility is a property of the calling contract, not the precompile. +- **Exhaust gas or denial of service.** Verify cost is fixed per scheme and bounded well below the EIP-7825 per-transaction cap (2^24 gas), so a single verify cannot be inflated by input shape. Falcon-1024 and ML-DSA-44 in pure Solidity exceed the cap and were therefore view-only before the native precompiles; the precompiles are what bring them under the cap for on-chain recording. +- **Confuse "verifies a PQ signature" with "PQ chain".** The threat here is representational, not technical: a reader could over-read the precompiles as post-quantum consensus. The defense is the framing statement at the top of this document, repeated in the guarantees table below. + +### 1.3 Zero-Knowledge Verification + +Aere hosts a multi-prover on-chain verification surface behind a route-by-selector gateway: SP1 (Groth16 and Plonk), RISC Zero (Groth16), a raw KZG / EIP-4844 path, and a generated Halo2 verifier, with a permissionless attestation registry on top. The application verifiers (storage-proof coprocessor, zk-compliance, zkML, rollup validity, recursive aggregator) hold the SP1 gateway address rather than a concrete verifier, so a new prover version is a single upstream route change. + +Attacker goals and defenses: + +- **Submit a false proof (soundness break).** Defended by the underlying proof systems (SP1 / Plonky3, RISC Zero, Halo2) being sound, and by the verifiers binding the exact program: an SP1 proof is checked against a `programVKey` that binds a specific guest ELF, a RISC Zero receipt against an `imageId`, and the recursive aggregator binds the inner KoalaBear (SP1Field) verifying-key digest that the recursion verifier actually checked, rather than only the on-chain BN254 vkey. Soundness is an assumption about the proof systems (Assumption A-5), not something this chain proves from first principles. +- **Break the ZK verifier with a quantum computer.** The on-chain verifiers are BN254 Groth16 pairing checks. BN254 pairings are Shor-breakable, so the ZK verification layer is classical and is not post-quantum. This is disclosed. The planned mitigation is a direct hash-based STARK verifier that rests on hash collision-resistance rather than pairings. Scope caveat (2026-07-19 research finding): the skeleton built so far is a real, conformance-confirmed BabyBear + FRI STARK verifier that targets Aere's OWN Plonky3 circuits, and it does NOT verify SP1 6.1.0 proofs. The pinned SP1 6.1.0 is a Hypercube release (KoalaBear multilinear: BaseFold plus sumcheck-zerocheck plus LogUp-GKR, not BabyBear FRI), so removing the SP1 Groth16 wrap is a separate founder-gated retarget to the SP1 Hypercube stack (see `AERE-STARK-SP1-RECURSION-AIR-PORT-SPEC-SUMMARY.md`), not a near-term step. Either way that verifier is presently a reference skeleton that fail-closes on every input and is not activated. Until it is real, retargeted, audited, and activated, the ZK layer's post-quantum posture is a design, not a property. +- **Poison a shared root or side tree.** The storage-proof coprocessor walks the real Merkle-Patricia state trie from `stateRoot` to the claimed value, hashing each node against its parent reference, with no Foundation-seeded side tree. Anchor-poisoning and inner-vkey-enforcement findings from the 2026-07-17 review are fixed with regression tests in the repository. +- **Register a malicious program.** Program registration is permissionless; the Foundation can disable a malicious program but cannot disable a legitimate one and cannot retroactively invalidate already-recorded proofs. This is a bounded, disclosed Foundation role, not an arbitrary override. + +### 1.4 Bridge and Cross-Chain + +The cross-chain surface is optimistic intent settlement (AereSpokePool, ERC-7683 / Across-V3 style), an institutional settlement hub (AereSettlementHubV2), Hyperlane-style warp routes, and zk light clients (QBFT and Ethereum). The escrow accounting of the two core contracts is machine-checked: the SpokePool `balance >= totalLocked + totalBond` invariant and the SettlementHub `balance >= committedLiabilities` invariant are each proved inductive in z3 (`formal-consensus/spokepool_smt.py`, `settlementhub_smt.py`), with negative controls that reproduce a real under-backing counterexample when a guard is removed. + +Attacker goals and defenses: + +- **Drain escrowed principal.** Defended by the proven solvency invariants above: every settle path pays only an allowlisted solver, cancel refunds only the depositor, withdraw returns only the caller's own free bond, and any sweep of residual is strictly bounded to `balance - committed` so it can never touch a parked intent or a posted bond. No path sends funds to an arbitrary caller address. +- **Claim without filling (optimistic-bond attack).** This is the disclosed weak point. A claim does not prove the destination fill; settle releases the user's locked input to the solver after a challenge window unless challenged, and Phase-1 challenge only emits an event (the Foundation arbitrates and slashes off-chain). A rogue or key-compromised allowlisted solver could claim across many orders in one window and lose only the fixed bond, which does not scale with the value at risk. In Phase 1 this is bounded by a permissioned, Foundation-vetted solver allowlist and is documented in the contract NatSpec. It is a trust assumption, not a hidden bug. Before any permissionless phase, the bond must exceed the maximum stealable value per window. +- **Break accounting with a hostile token.** The SpokePool credits nominal input amounts, so a fee-on-transfer or rebasing input token can break its per-token backing invariant (a disclosed low-to-medium finding); the SettlementHubV2 closes this with an explicit asset allowlist that can exclude such tokens. Exposure is nil while inputs are restricted to vetted standard ERC-20s. +- **Forge a cross-chain message or light-client header.** The zk light clients verify proofs of the source chain's consensus rather than trusting a relayer. Their soundness inherits the ZK-layer assumption (Assumption A-5) and, for the QBFT light client, the same classical-BN254 caveat as Section 1.3. + +### 1.5 Accounts and Account Abstraction + +Aere supports ERC-4337 v0.7 (AereEntryPointV2), EIP-7702 upgrade-in-place, WebAuthn / P-256 passkey smart accounts, a Falcon-512-owned post-quantum smart account (AerePQCAccount), a hybrid ECDSA-plus-Falcon authorizer (AereHybridAuth), and a t-of-n post-quantum threshold account. The chain exposes the standard `ecrecover` (3,000 gas) and a P-256 verification precompile (RIP-7212 / RIP-7951 at `0x100`, 3,450 gas), both at their standard protocol gas costs. + +Attacker goals and defenses: + +- **Forge account authorization.** Defended by the account's chosen validator: secp256k1 ECDSA, WebAuthn P-256 (device secure-element key that never leaves the device), Falcon-512 (post-quantum), or a hybrid that requires both an ECDSA and a Falcon signature over the same hash so that neither a broken curve nor a broken lattice alone suffices. Passkey security additionally depends on the device secure element and the WebAuthn ceremony (Assumption A-8). +- **Reach threshold with duplicate committee keys.** A 2026-07-15 finding showed the threshold custody and PQC registry accepted duplicate committee keys (distinctness was by index, not by key), so one keyholder could fill multiple slots. The fix is machine-checked (`threshold_account_smt.py`: with distinct keys no single keyholder reaches threshold t >= 2 for N up to 21) and is deployed on-chain as the PQC registry V2; the account-factory V2 redeploy is founder-gated, and both live buggy contracts are empty (0 committees, 0 accounts created), so exposure is nil either way. +- **Exploit the nonce or paymaster surface.** AereEntryPointV2 uses a strictly sequential single-dimension nonce; accounts that switch validators route on a signature prefix byte rather than a 2D nonce key, a named seam rather than a hidden one. The V2 token and stake-quota paymasters are hardened redeploys that fixed confirmed V1 drain and consent bugs, with the V1 contracts deprecated in place. +- **Quantum forgery of a classical account key.** An ECDSA-only or P-256-only account is not post-quantum; only accounts that use the Falcon or hybrid validators are. This is a per-account property that users opt into, not a chain-wide guarantee. + +### 1.6 Economic Core + +The economic core is immutable and ownerless. AereSink is a 3-bucket router (BURN, BUYBACK, YIELD) with, per its source, no owner, no admin, no governance role, no `setBucket` / `setRecipient` / `setRouter` / `pause`, immutable bucket recipients and immutable basis-point splits that must sum to exactly 10000. sAERE is an ERC-4626 vault. The burn is a cut of the validator block reward, capped by the immutable `MAX_BURN_BPS = 5000` (50 percent) in AereCoinbaseSplitterV2; it is not a base-fee burn. AereFeeBurnVault has no withdraw function and no admin escape hatch. AERE is the native coin; its total supply is fixed at genesis (2.8B) and there is no protocol mint path. + +Attacker goals and defenses: + +- **Rug: mint to self, admin-withdraw, upgrade-swap, selfdestruct, or delegatecall.** A repository-wide primitive sweep across the deployed contract set found 0 `selfdestruct`, 0 `delegatecall`, 0 upgradeable proxies (no UUPS / transparent / `_authorizeUpgrade` / `upgradeTo`), and 0 owner escape hatch (`adminWithdraw` / `rescueTokens` / `sweepTo`). The concrete meaning of "no one can rug the economic core" is that these specific primitives are absent from the deployed set. This is the honest, checkable form of the claim, not a blanket "no backdoors anywhere" (see Section 1.7). +- **Steal routed fees.** Every AereSink routing path terminates at the no-withdraw burn vault or the sAERE vault; no path sends funds to an arbitrary or caller-supplied address, so there is no theft vector. A failed buyback swap degrades to sweepable dust rather than a lock, and flush and sweep are reentrancy-guarded. +- **Inflate the burn beyond policy.** The burn rate is Foundation-settable but hard-capped at 50 percent by an immutable constant; it cannot be pushed higher, and it cuts the validator reward, not the base fee. +- **Manipulate the sAERE exchange rate (first-depositor / donation inflation).** The vault does not mint shares on a raw transfer, so a direct donation lifts the rate rather than being stealable, and the yield bucket transfer pings the vault's sync so value drips linearly instead of as a sandwichable step. These properties are covered by invariant-property fuzz suites over the burn / economics contracts. + +### 1.7 Oracles and Compliance + +Operational contracts, in deliberate contrast to the economic core, do have explicit and documented Foundation roles. This is disclosed and is not a hidden backdoor. The correct statement is: there is no admin on the economic core (ownerless, immutable, verifiable on-chain), and the operational contracts have explicit, documented Foundation roles. + +Attacker goals and defenses: + +- **Falsify a reserve or NAV attestation.** AereNavOracle lets the Foundation (owner) propose, dismiss challenges, and attest a Merkle-rooted reserve snapshot; it explicitly cannot retroactively alter an already-attested snapshot. A proposed snapshot starts a 24-hour challenge window, anyone may challenge, and attestation after a clean window is permissionless. The Foundation's power is bounded to propose / dismiss / attest, and the challenge window plus append-only attestation is the defense against a single bad snapshot; it is a trusted-attestor model, not a decentralized oracle. +- **Abuse compliance or sanctions screening.** Compliance uses SP1 zk-compliance proofs (a user proves off-chain sanctions / residency / jurisdiction screening inside the zkVM, anchoring only a boolean-style clearance, with no PII on chain) and a Privacy-Pools-style compliant-withdrawal pool. The Foundation role here is screening policy, disclosed, not fund custody. +- **Capture governance.** Governor plus Timelock exist but are currently inert (they own nothing and control nothing until an audit-gated transfer). The threat of a captured governance is therefore not live today; it becomes relevant only if and when control is transferred, at which point the Timelock delay is the defense. +- **Oracle staleness or decimals trap.** A known activation-time hazard: AereSink's oracle-floor math assumes 18-decimal tokens, so enabling the oracle against a 6-decimal pair would give false sandwich protection. The oracle is off today (`ORACLE = 0x0` on-chain), and activation is documented as requiring the decimals fix first. No exposure at present. + +--- + +## 2. Guaranteed vs Not-Guaranteed + +This table is the centerpiece of the specification. The left column is what Aere will stand behind; the right column is what Aere explicitly does not promise. A guarantee holds only under the assumptions in Section 3. + +| Component | What we GUARANTEE | What we DO NOT guarantee | +|---|---|---| +| **Consensus (QBFT)** | Safety (no fork / no equivocation) with up to 2 of 7 validators Byzantine; self-recovery and resync after transient faults (0 forks and 100/100 resync across 100 adversarial kill-2 cycles on testnet); IBFT 2.0 locking modeled and enforced by the live producer. | Safety beyond 2 Byzantine validators (a 3-of-7 collusion can fork); bounded-time liveness at the exact f = 2 boundary (FLP: liveness is eventual, not instantaneous); decentralization (all 7 validators are Foundation-operated, Nakamoto coefficient about 1); post-quantum consensus (seals are classical ECDSA). | +| **PQC precompiles** | Live on mainnet at `0x0AE1`..`0x0AE5`; deterministic, gas-metered verification of Falcon-512/1024, ML-DSA-44, SLH-DSA-SHA2-128s, SHAKE256, validated bit-for-bit against NIST KAT/ACVP vectors; fail-closed (return a not-verified zero word or empty, never a fault). | That any signature scheme is unbreakable (soundness rests on NIST PQC hardness and on Bouncy Castle correctness); that `0x0AE6`/`0x0AE7` (ML-KEM, HashToPoint) or `0x0AE8` (STARK) are live on mainnet (they are not); that verifying PQ signatures makes the chain post-quantum. | +| **ZK verification** | A multi-prover on-chain verification surface (SP1 Groth16/Plonk, RISC Zero, KZG, Halo2) that binds the exact program (vkey / imageId), with a permissionless attestation registry and a real Merkle-Patricia storage-proof coprocessor. | Soundness of the underlying proof systems from first principles (assumed, not proven here); post-quantum security of the on-chain verifiers (BN254 pairings are Shor-breakable); that the planned STARK verifier is live (it is a non-activated reference skeleton). | +| **Bridge / cross-chain** | Machine-checked escrow solvency for the two core contracts (`balance >= totalLocked + totalBond`; `balance >= committedLiabilities`), proved inductive in z3; funds route only to allowlisted solver / depositor / own-bond / sink, never to an arbitrary address. | That an allowlisted solver cannot claim-without-filling within a challenge window (the fixed optimistic bond does not scale with value at risk; Phase-1 safety rests on the permissioned, Foundation-vetted solver allowlist); correct accounting under fee-on-transfer / rebasing input tokens on the SpokePool. | +| **Accounts / AA** | ERC-4337 v0.7, EIP-7702, passkey (P-256), Falcon-512, hybrid ECDSA+Falcon, and t-of-n threshold accounts; threshold duplicate-key fix machine-checked and deployed (PQC registry V2); hardened V2 paymasters. | That a classical ECDSA-only or P-256-only account is post-quantum (only Falcon / hybrid accounts are); device / WebAuthn security (out of chain scope); that the founder-gated account-factory V2 redeploy has occurred (buggy factory is live but empty). | +| **Economic core** | Ownerless and immutable AereSink and sAERE: no admin, no governance, no upgrade proxy, no selfdestruct, no delegatecall, no owner withdraw across the deployed set (repo-wide primitive sweep = 0 each); burn hard-capped at 50 percent of validator reward; fixed 2.8B native supply with no mint path. | A blanket "no admin anywhere on the network" (operational contracts have explicit Foundation roles, see next row); protection against a Foundation-set burn rate anywhere between 0 and the 50 percent cap; economic / price outcomes of the burn-buyback-yield mechanism. | +| **Oracles / compliance** | Explicit, documented, bounded Foundation roles: NavOracle can only propose / dismiss / attest and cannot alter an attested snapshot (24-hour challengeable window, permissionless attest); compliance anchors only zk clearance booleans (no PII on chain); Governor / Timelock are inert. | A decentralized or trustless oracle (NAV is a trusted-attestor model); that the Foundation cannot publish a wrong-but-unchallenged snapshot within a window; correctness of any off-chain screening input; anything about governance once control is transferred beyond the Timelock delay. | + +--- + +## 3. Security Assumptions + +The guarantees in Section 2 hold only under the following assumptions. If an assumption is false, the corresponding guarantee does not hold. They are stated plainly so that a reviewer can accept or reject each one on its own terms. + +- **A-1 Partial synchrony.** Validator clocks are loosely synchronized and, after some unknown global stabilization time (GST), message delay is bounded. QBFT safety does not depend on this, but liveness does: under asynchrony, progress is only eventual (FLP), and the rare f = 2 boundary stall is a consequence of this assumption, not a defect. +- **A-2 Byzantine bound.** At most 2 of the 7 validators are Byzantine (`f = 2` at N = 7, quorum = 5). Beyond one third Byzantine, BFT safety fails and a fork becomes reachable. This bound is exact. +- **A-3 Honest-operator trust model (the load-bearing assumption).** All 7 validators are Foundation-operated, so the trust model is honest-operator, not economic or decentralized, and the Nakamoto coefficient is approximately 1. Aere's safety today rests on the Foundation not running more than 2 equivocating nodes and not censoring at will. This is disclosed, is the reason the chain is not yet credibly decentralized, and is the assumption an external reviewer should weigh most heavily. +- **A-4 Keccak collision resistance.** Block hashing, Merkle-Patricia state proofs, and commit-seal pre-images assume keccak-256 is collision-resistant. +- **A-5 Proof-system soundness.** The SP1 / Plonky3, RISC Zero, and Halo2 proof systems are sound: a verifying proof implies the asserted statement, except with negligible probability. The on-chain verifiers are assumed to correctly implement these systems (backed by KAT / fixture tests, not by a from-scratch soundness proof). +- **A-6 NIST PQC hardness.** The hardness assumptions behind Falcon (NTRU lattice), ML-DSA / ML-KEM (module lattice), and SLH-DSA (hash-based) are unbroken. Signature-layer post-quantum guarantees are void if these are broken. +- **A-7 Audited primitive library.** The precompiles rely on the correctness of Bouncy Castle (`bcprov-jdk18on-1.83.jar`) for Falcon / ML-DSA / SLH-DSA / SHAKE. A bug in that library is a bug in the precompiles. +- **A-8 Device and WebAuthn security.** Passkey / P-256 account security assumes the device secure element protects the private key and that the WebAuthn ceremony is not subverted on the client. This is outside the chain's control. +- **A-9 BN254 is honest until replaced.** The on-chain ZK verifiers use BN254 pairings, which are Shor-breakable. They are assumed secure against classical adversaries only, and this assumption is explicitly temporary: it stands until the planned direct hash-based STARK verifier (Section 1.3) is made real, audited, and activated. Under a cryptographically-relevant quantum adversary, the ZK verification layer and the QBFT light client offer no guarantee. +- **A-10 Precompile determinism.** Every precompile is a pure function of its input bytes, reads no chain state or nondeterministic source, and every node runs an identical client build, so all nodes compute the identical result and gas charge. A divergence here would be a consensus fault. +- **A-11 No external audit yet.** The guarantees are backed by internal formal verification (z3 SMT: 125 proved properties plus 49 counterexample negative controls across the consensus and contract models at last count; Halmos; Solidity SMTChecker; and 22 invariant-property fuzz suites over burn / economics / custody; exact per-suite counts are reproducible by running the published verification harness, `run_consensus_verification.py` plus the contract SMT suite) and by adversarial self-review, but not by an independent external audit. This document is the bridge to that audit; until it completes, every guarantee should be read as "internally verified, not externally attested." + +--- + +## 4. Design Rationale ("Why not?") + +This section records, for each load-bearing architecture decision, what was chosen, what the credible alternatives were, and why the alternative was rejected. The intent is to make the trade-offs auditable: every choice below has a cost, and the cost is stated. Where a decision reflects a deliberate deviation from Ethereum's current roadmap, the deviation is documented rather than hidden. + +### 4.1 Consensus: QBFT, not HotStuff + +**Chosen.** QBFT (a Byzantine-fault-tolerant IBFT-family protocol) as implemented in Hyperledger Besu, producing deterministic single-slot finality at a sub-second cadence (~0.5s target block time). At the live validator count N=7, QBFT tolerates f=2 Byzantine or crashed validators, with a commit quorum of 2f+1 = 5 of 7. + +**Alternative considered.** HotStuff (and its pipelined variants), which achieves linear per-round communication complexity and is engineered to scale BFT consensus to hundreds of validators. + +**Why not HotStuff.** HotStuff's headline advantage is communication complexity that stays linear as the validator set grows large. Aere runs a small, permissioned validator set (7 today, with a roadmap target in the 9 to 21 range). At that scale QBFT's O(N^2) message complexity is a non-issue in absolute terms (the crypto and gossip cost of a 5-of-7 quorum verify is on the order of a few milliseconds per block, a small fraction of the 500ms slot). The scaling regime where HotStuff wins is one Aere does not operate in and does not plan to enter under this design. Against that non-benefit, QBFT offers three concrete advantages at our size: (1) it provides deterministic, instant, single-block finality (no probabilistic or multi-round confirmation), which is the settlement guarantee the whole network is built to sell; (2) it is mature and already integrated in Besu, so it carries no new-protocol implementation risk; and (3) it is the protocol our post-quantum consensus research, our second-client work, and our zk finality proofs are all built against. Adopting HotStuff would have meant taking on the risk and integration cost of a less-battle-tested (for our client) protocol to buy scalability we have no use for. The honest limitation of the QBFT choice is disclosed in the threat model: at N=7 the fault tolerance is real against node outages but the validators are all Foundation-operated, so decentralization, not consensus mechanism, is the binding trust assumption. + +### 4.2 Execution client: forked Besu, not Reth, with Nethermind as the second client + +**Chosen.** A fork of Hyperledger Besu v26.4.0 (Java, base commit d2032017, built on a JDK 21 toolchain) as the sole live mainnet producer. The fork adds native post-quantum precompiles and an extended EIP-2935 block-hash lookback (live on mainnet since block 9,189,161) and carries the base-fee-floor change (live since block 10,141,734). A patched Nethermind 1.39.0 (.NET) is the second, independent client. + +**Alternatives considered.** Reth (Rust, high-performance) as the base client; or running a single client indefinitely. + +**Why not Reth.** Two reasons, one structural and one empirical. Structurally, Besu already ships QBFT, and QBFT block production is Besu-specific: no off-the-shelf Geth, Reth, Erigon, or stock Nethermind produces QBFT-compatible blocks. Choosing Reth would have meant building QBFT production into a client that has no notion of it, before we could produce a single block. Besu also already carried the codebase into which our PQC precompile fork and base-fee changes were integrated. Empirically, a single producing client is a demonstrated systemic risk: the September 2025 Reth halt is the reference case for why a chain that depends on one producing implementation can stop when that implementation hits a bug. That event is precisely the risk the second-client program exists to retire. + +**Why Nethermind as the second client (not a second Besu).** A second Besu instance is not client diversity; it shares every bug with the first. Nethermind was chosen specifically for implementation diversity: it is a different codebase in a different language (.NET versus Besu's Java), so a consensus-relevant bug in one is unlikely to exist in the other. The patched Nethermind validates the live chain, runs the five PQC precompiles byte-for-byte identically (27 of 27 NIST KAT vectors), and, on an isolated test network, produces byte-identical QBFT blocks that stock Besu accepts through full BFT validation (with a one-byte-tampered seal rejected). The honest boundary: this cross-client production is proven on an isolated testnet (offline import and, in later work, live devp2p between test nodes), and a listen-only Nethermind follower has been run against the live network; it is not yet a live gossiping producer on chain 2800. Making it one is a founder-supervised change, because a producer bug on a live chain can halt or fork it. Besu remains the sole live producer today; the second client is a client-diversity cross-check and fail-safe, not a second live validator yet. + +### 4.3 Interoperability: Hyperlane-compatible, not IBC, plus a zk-interop path + +**Chosen.** An EVM-native, Hyperlane-compatible messaging layer (a Mailbox-compatible `AereMessenger`, an Interchain Gas Paymaster `AereIGP`), an ERC-7683 intent layer, and an Across-v3-compatible spoke pool. Alongside this sits a zero-knowledge interop path: on-chain zk light clients that verify a counterparty's consensus finality (inbound Ethereum sync-committee finality, outbound Aere QBFT finality) from inside a contract, via SP1 Groth16 proofs. + +**Alternative considered.** IBC (the Inter-Blockchain Communication protocol), the trust-minimized, light-client-based standard from the Cosmos ecosystem. + +**Why not IBC.** IBC's design philosophy, verifying the counterparty's consensus rather than trusting a bridge committee, is the right one, and Aere adopts that philosophy directly. But IBC as a protocol is built around Tendermint-style light clients and a non-EVM connection, channel, and packet model. Adopting it natively would have meant importing a substantial non-EVM stack and its tooling into an EVM chain whose entire value proposition is that it is an ordinary EVM. Instead Aere splits the problem: for permissionless, developer-familiar EVM interop it uses the Hyperlane-compatible interfaces (which the EVM tooling ecosystem already speaks), and for the trust-minimization that is IBC's real contribution it built the zk-interop light clients, which capture the "verify the counterparty's consensus, do not trust a relayer" property without leaving the EVM world. The honest boundary: the Hyperlane-compatible endpoints are interface-faithful and deployed, but a live decentralized relayer and interchain-security-module network is not yet stood up (the current bridge path runs through a single Foundation signer with a relayer pending), and the zk light clients are trust-minimized, not trustless, and not quantum-safe (their committed seals are classical secp256k1 and the proof wrap is Groth16 over BN254). + +### 4.4 Post-quantum signatures: Falcon and ML-DSA together, not one lattice scheme + +**Chosen.** Native on-chain verification of multiple post-quantum signature schemes, including two distinct lattice families: Falcon (Falcon-512 and Falcon-1024) and ML-DSA (Dilithium2 / ML-DSA-44), alongside hash-based schemes (SLH-DSA, XMSS). The precompiles for SHAKE256, Falcon-512, Falcon-1024, ML-DSA-44, and SLH-DSA-SHA2-128s are live on mainnet in the 0x0AE1 to 0x0AE5 band. + +**Alternative considered.** Standardizing on a single lattice signature scheme (for example ML-DSA alone, the NIST primary lattice standard, or Falcon alone for its compact signatures). + +**Why not a single scheme.** Cryptographic-risk diversification. Falcon and ML-DSA rest on different structured-lattice problems (Falcon on NTRU lattices, ML-DSA on module lattices with Fiat-Shamir-with-aborts). Supporting both means that a cryptanalytic break or a standardization flaw in one lattice family does not, by itself, remove Aere's ability to verify post-quantum signatures: accounts and settlement authorization can migrate to the surviving family. This is the same conservative posture as the hybrid `AereHybridAuth` account, which requires both a classical ECDSA and a Falcon-512 signature so that neither a broken curve nor a broken lattice alone suffices to forge. The cost of supporting multiple schemes is more verifier surface to implement, validate, and eventually audit; that cost is accepted deliberately in exchange for not betting the network's post-quantum future on a single mathematical assumption. The critical honest scope, stated wherever post-quantum is discussed: this is post-quantum at the signature, account, and application layer only. Consensus remains classical (validators sign secp256k1 QBFT messages) and the zk verification is classical (BN254 Groth16, Shor-breakable). Aere never claims post-quantum consensus. + +### 4.5 Account abstraction: ERC-4337, not native AA, with EIP-7702 as the bridge + +**Chosen.** ERC-4337 (v0.7) smart accounts as the account-abstraction path, with EIP-7702 (live under the Pectra ruleset) as the migration bridge that lets existing externally-owned accounts (EOAs) delegate to smart-account code. + +**Alternative considered.** Native, protocol-level account abstraction, up to and including the "all accounts are smart accounts by default" end-state. + +**Why not native AA.** ERC-4337 needs no consensus change and is an established standard with an existing tooling and bundler ecosystem; it delivers programmable accounts (including the Falcon-owned post-quantum smart account, `AerePQCAccountFactory`) without touching the protocol, which preserves exact EVM and Ethereum compatibility. Making all accounts smart by default would break EOA and EVM compatibility: it changes what an account fundamentally is, which breaks the assumptions of existing tooling, existing contracts, and existing user keys. Preserving that compatibility was a deliberate design goal, not an oversight. EIP-7702 is the chosen bridge precisely because it upgrades existing EOAs in place (an EOA can delegate to smart-account code) without forcing the disruptive "everything is a contract" change. Note on the Ethereum roadmap lineage: EIP-3074, an earlier EOA-empowerment proposal, was superseded by EIP-7702, which is the mechanism Aere carries; Aere does not implement 3074. + +### 4.6 The virtual machine: extend the EVM, do not build a new VM + +**Chosen.** Keep the EVM. Solidity, EVM bytecode, JSON-RPC, and the developer tooling are all unchanged. Differentiation (post-quantum verification, parallel execution, the block-hash lookback) is added as precompiles and client fork rules at otherwise-empty addresses, not as a new instruction set or a new language. + +**Alternative considered.** Designing a new, purpose-built virtual machine (a new bytecode, a new language, or a non-EVM execution environment) optimized around Aere's differentiators. + +**Why not a new VM.** A new VM maximizes both technical risk and adoption risk. Technically, a mature VM has years of implementation hardening, a known cost model, and a formal-ish operational history; a new VM starts that clock at zero. For adoption, the EVM is the single largest smart-contract developer surface in existence, and every deviation from it (a nonstandard opcode, a nonstandard account model, a nonstandard RPC) is a tax on every developer and every tool. Aere's thesis is settlement, not a novel programming model, so the design keeps the mature, tested execution environment intact and adds its differentiation at the edges where the EVM has explicit, standard extension points (precompiles at reserved addresses, activated by client-only forks in the same manner Ethereum activates its own hard forks). The result: nothing about Aere's account, passkey, or post-quantum surface depends on a nonstandard EVM. The cost of this choice is that some ambitions (base-layer parallel execution, an EVM-in-a-zkVM) must be reached inside the existing model rather than by designing them in from scratch; those remain roadmap and are labeled as such. + +### 4.7 The burn: a cut of the validator reward, not a base-fee burn + +**Chosen.** Aere burns a share (37.5% under the current configuration) of the validator coinbase block reward, applied by a splitter contract (`AereCoinbaseSplitterV2`) that validators or their forwarder daemons call each block. The rate is a Foundation-adjustable parameter, hard-capped at 50% (5000 basis points). It is explicitly not EIP-1559 protocol-level base-fee burning. + +**Alternative considered.** An EIP-1559-style base-fee burn enforced by consensus (the mechanism Ethereum mainnet uses, where the base fee of every transaction is burned as a protocol rule). + +**Why not a base-fee burn.** Being precise here is a credibility matter, and the design is deliberately honest about it. A consensus-level base-fee burn is a protocol rule; the Aere burn is a coinbase-reward split applied above consensus by a contract. The design routes the burn through the coinbase layer rather than enshrining it in consensus for two reasons: it keeps the burn out of the consensus-critical path (a change to the burn rate cannot halt or fork the chain, whereas a change to a consensus base-fee rule is a hard fork), and it lets the destinations be made immutable at the contract layer while the rate stays a bounded, governable dial. What is sealed is not the rate but the endpoints: `AereSink` (no owner, no setters, immutable splits) and `AereFeeBurnVault` (no owner, no admin, no withdraw function), so burned value cannot be rugged or drained regardless of who sets the rate. This document must not describe the Aere burn as a base-fee burn; it is a validator-reward-cut burn, rate-adjustable within a 50% ceiling, into immutable destinations. Separately, and not to be conflated with the burn: Aere does run a base-fee change at the protocol layer, a 1-Gwei EIP-1559 base-fee floor (live since block 10,141,734). That floor sets a minimum base fee; it is not a burn mechanism. + +### 4.8 Deliberate compatibility deviations from the Ethereum roadmap + +Aere tracks Ethereum's hard forks (Pectra activated at block 2,075,363; Fusaka / Osaka at block 2,106,606) so that its EVM surface matches mainnet at the same addresses. Several roadmap features are, however, deliberately neutralized or absent because Aere is a QBFT chain with no separate consensus (beacon) layer and no blob data-availability market. These are design decisions, disclosed here so an integrator is not surprised: + +- **Base fee has a floor plus a validator-reward burn**, not a consensus base-fee burn (see 4.7). The floor is 1 Gwei, live from block 10,141,734. +- **EIP-4844 blob transactions are present in the EVM, but `BLOBBASEFEE` (EIP-7516) returns 0** because there are no blobs: Aere runs no blob data-availability market. +- **EIP-4788 (parent beacon block root) returns 0x0**, because a QBFT chain has no separate beacon / consensus layer to expose a root from. +- **EIP-3074 is not implemented; it is superseded by EIP-7702**, which is the EOA-delegation primitive Aere carries (see 4.5). +- **PeerDAS (EIP-7594), FOCIL, and EOF have no active role under Aere's QBFT model.** PeerDAS has no data-availability role (there is no blob market), FOCIL (proposer inclusion lists) has no fork-choice or proposer-inclusion layer to enforce under QBFT, and EOF is not activated under the current ruleset. + +--- + +## 5. Failure Analysis + +This section describes Aere's behavior under each significant failure mode. For each, it states whether the behavior is PROVEN (demonstrated by a repeatable test or a live event) or EXPECTED (the deterministic consequence of the protocol's rules, not separately soak-tested at that exact configuration), and whether the chain halts safely, forks, or continues. The governing consensus parameters are fixed: N=7 validators, f=2, commit quorum 2f+1 = 5 of 7. + +A safety-first summary that holds across every mode tested: **in all adversarial fault testing to date, zero forks were observed.** The chain's failure posture is to halt (and later recover) rather than to fork. That is the property a settlement layer must have, and it is the property the evidence supports. + +| Failure mode | Outcome | Fork? | Status | +|---|---|---|---| +| 1 validator dies | Chain continues | No | PROVEN | +| 2 validators offline | Continues at the quorum limit (rare, self-recovering stalls) | No | PROVEN | +| 3+ validators offline | Chain halts (safe) | No | EXPECTED (quorum math) + sub-quorum halt demonstrated | +| Network partition | Minority side halts, recovers on reconnect | No | PROVEN (halt-then-recover demonstrated) | +| Nethermind and Besu disagree on state | Divergence detected by client cross-check | No (fail-safe) | PROVEN as a validation cross-check; not yet a live automated gate | +| PQC precompile errors on input | Fail-closed (defined empty / zero output, no revert) | No | PROVEN (live behavior verified) | +| Bridge goes down | Cross-chain messaging halts; L1 keeps running | No | EXPECTED (app-layer isolation) | +| ZK prover unavailable | New proofs pause; chain and verified state keep running | No | EXPECTED (advance is manual / permissionless) | + +### 5.1 One validator dies + +**Behavior.** The chain continues. With one of seven validators down, six remain, which exceeds the commit quorum of five, so blocks continue to be proposed (round-robin skips the dead proposer's slots via round change) and committed. + +**Halt / fork / continue.** Continues. No fork. + +**Status.** PROVEN. Single-fault survival is demonstrated in the fault-tolerance work: in an N=4 (f=1) mixed-client run, killing one validator left the surviving three committing; the pure-Besu N=7 baseline sustains block production well inside the f=2 boundary. This is also the direct consequence of quorum math (six alive > five needed). + +### 5.2 Two validators offline + +**Behavior.** The chain continues, but it is at the exact fault-tolerance limit: with two of seven down, exactly five validators remain, which equals the quorum of five with zero slack. All five survivors must prepare and commit every block. In a 40-cycle adversarial soak (kill two random validators, measure a 45-second fault window, restart, measure recovery), the chain committed blocks in 37 of 40 cycles and, in 3 of 40 cycles, produced a temporary zero-progress ("stall") window. Those three stalls were temporary and self-recovering, not permanent halts and not forks: every stalled cycle resumed the moment the killed nodes restarted, with `fork_during = False` and `resynced_after = True` in all cases. + +**Halt / fork / continue.** Continues at the limit. No fork in any of the 40 cycles. Under specific worst-case two-down proposer arrangements at the exact f=2 boundary, progress can pause briefly, but the chain is neither forked nor permanently stuck. + +**Status.** PROVEN, with the boundary nuance reported honestly rather than rounded to "zero halts." Evidence: `FAULT-TOLERANCE-CHARACTERIZATION-2026-07-14.md` (0 forks / 40, 40/40 killed nodes resynced, 3/40 temporary self-recovering stall windows; pure-Besu N=7 kill-two reference showed 0 forks and 0 stalls over 20 cycles). The rare stall at the boundary is inherent to QBFT running with zero quorum slack, not a fork and not a safety failure. + +### 5.3 Three or more validators offline + +**Behavior.** The chain halts. With three of seven down, only four validators remain, which is below the commit quorum of five, so no block can reach quorum and progress stops. It halts cleanly: it does not fork, because no side can form a quorum, and it resumes exactly where it stopped once enough validators return. + +**Halt / fork / continue.** Halts, safely. No fork. + +**Status.** EXPECTED as the deterministic consequence of quorum math (four alive < five needed), and the sub-quorum halt-then-recover behavior itself is demonstrated (see network partition, below, and the hybrid-consensus negative controls where dropping the set below quorum halted block production in place and recovered on restoration with no re-genesis and no split). This specific "third of seven goes down" configuration follows directly from the quorum rule; it is not separately soak-characterized as its own experiment, and the claim as written rests on quorum math plus the demonstrated sub-quorum halt-and-recover. + +### 5.4 Network partition + +**Behavior.** On a network partition, the side of the partition that does not hold a quorum (at least five of seven validators) cannot commit blocks and halts. It does not fork: a minority partition can never form the 5-of-7 committed-seal quorum required to finalize a block, so it produces no competing finalized chain. When the partition heals and the validators reconnect, the halted side resumes and resyncs to the canonical head. This halt-then-recover behavior was demonstrated directly. + +**Halt / fork / continue.** The minority side halts; the majority side (if one partition holds >= 5 validators) continues; on reconnection the halted side recovers. No fork. + +**Status.** PROVEN (halt-then-recover demonstrated). Evidence: sub-quorum halt and in-place recovery were shown in the in-place PQC activation work (dropping below the required quorum halted block production at a specific height, and restoring the missing signers resumed from that exact height with no re-genesis) and in the hybrid-consensus negative controls (killing enough validators to break quorum halted the chain with no split and recovered in place). The single-operator caveat applies and is disclosed: all seven validators are Foundation-operated on Hetzner infrastructure, so a partition that is really an infrastructure or operator outage is a correlated failure, not an independent one. QBFT's partition safety (no fork) holds regardless; the availability of a quorum-holding side is an operational, not a protocol, guarantee at N=7 under one operator. + +### 5.5 The two clients disagree on state (Nethermind vs Besu) + +**Behavior.** The second client exists precisely to catch this. The patched Nethermind independently re-derives state: it has re-validated the full chain to genesis with zero invalid seals and re-executed real chain-2800 blocks to byte-for-byte identical block hashes and state roots (spot-checked across many heights, and, as a live listen-only follower, matched the live RPC's hash and state root at every checked height in range). Because there is exactly one definition of correct state and two independent implementations computing it, a consensus-relevant divergence between Besu and Nethermind (a differing state root, a differing block hash, a differing seal decision) is detectable by comparing the two: it does not silently pass. + +**Halt / fork / continue.** This is a fail-safe (a cross-check), not an automatic consensus action. A detected divergence is a signal to halt and investigate before the divergent block is trusted, not something that itself forks or halts the live chain. Besu is the sole live producer today, so a Nethermind disagreement flags a discrepancy against the producer; it does not currently arbitrate consensus. + +**Status.** PROVEN as a validation cross-check (full-chain re-validation, byte-identical state-root re-execution, and identical PQC precompile outputs). It is not yet a live, automated, alerting divergence gate wired into production monitoring, and Nethermind is not yet a live producing validator. Framed honestly: the second client demonstrably would detect a state divergence, and this is real client-diversity assurance; turning that into an automated live fail-safe gate is the remaining operational work. + +### 5.6 A PQC precompile errors on its input + +**Behavior.** The precompiles fail closed. On malformed or unexpected input they return a defined non-accepting output rather than reverting: the Falcon, ML-DSA, and SLH-DSA verifier precompiles (0x0AE1 through 0x0AE4) return a 32-byte zero word (which reads as "not verified"), and the SHAKE256 precompile (0x0AE5) returns empty on malformed framing. None of them revert, and none of them can affect consensus: they are pure verification functions at reserved addresses, so a bad input produces a not-verified result and nothing more. The integrator rule that travels with this is explicit: treat a zero-word or empty return as not-verified, and validate input lengths yourself. + +**Halt / fork / continue.** The chain is unaffected. No revert of consensus, no halt, no fork. The calling contract simply sees a not-verified result. + +**Status.** PROVEN. This as-shipped behavior was verified against the live chain and reconciled into the precompile documentation (the earlier draft's "MUST revert" framing was corrected to the actual fail-closed zero-word / empty-output behavior). Evidence: the AIP reconcile in `aerenew/research/aip-draft-pqc-precompiles.md` "As shipped" corrections. + +### 5.7 The bridge goes down + +**Behavior.** Cross-chain messaging stops; the L1 keeps running. The interop layer (the Hyperlane-compatible messenger, the intent and spoke contracts, and any relayer) sits entirely at the application layer and is not in the consensus or execution-critical path. If the bridge relayer or a counterparty deployment goes offline, outbound and inbound cross-chain messages stop being delivered, but Aere chain 2800 continues producing and finalizing blocks exactly as before. + +**Halt / fork / continue.** The L1 continues. Only cross-chain message delivery halts. No fork. + +**Status.** EXPECTED, by architectural isolation: the bridge is app-layer and the current bridge path is not even a live decentralized network yet (it runs through a single Foundation signer with a relayer pending), so its being down affects only cross-chain product surface, never L1 liveness. + +### 5.8 The ZK prover is unavailable + +**Behavior.** New proofs pause; the chain and all existing verified state keep running. The zk components (the rollup-validity anchor, the inbound Ethereum light client, the outbound QBFT light client) advance only when someone submits a proof: advancing is permissionless but not automatic. If the off-chain prover (the SP1 prover, run on dedicated non-infra hardware) is unavailable, no new finality advances or new validity proofs are recorded, but nothing already verified is rolled back, and the L1 itself does not depend on the prover to produce or finalize blocks. + +**Halt / fork / continue.** The L1 continues. Only the production of new zk proofs pauses; previously verified state stands. No fork. + +**Status.** EXPECTED, by design: the light clients' heads move only when a proof is submitted ("permissionless but not automatic"), and proving runs off-chain, off the infra box, so prover downtime cannot halt consensus. The honest boundary already stated for the zk path applies: it is trust-minimized, not trustless, and not quantum-safe (Groth16 over BN254). + +--- + +## 6. Document Status and Reproducibility + +This specification is the bridge between Aere's internal verification and an independent external audit. Its guarantees are backed by machine-checked formal verification and adversarial self-review, and every figure in it is intended to be reproducible from the published repositories and harness (that reproducibility is itself a roadmap item, tracked as the open-benchmark and reproducible-build work). Two standing honesty rules govern any use of this document: + +1. Until an independent external audit completes, every guarantee reads as "internally verified, not externally attested." +2. The post-quantum scope boundary is absolute: signatures and accounts can be post-quantum; consensus (ECDSA / QBFT) and the on-chain ZK verifiers (BN254 Groth16) are classical. The chain as a whole is not post-quantum, and no derived material may claim otherwise. diff --git a/AERE-ENTROPY-BEACON-FIX.md b/AERE-ENTROPY-BEACON-FIX.md new file mode 100644 index 0000000..57f307a --- /dev/null +++ b/AERE-ENTROPY-BEACON-FIX.md @@ -0,0 +1,125 @@ +# Spec 9: Aere entropy honesty fix — real drand BLS verification + +## The gap (what was dishonest) + +`aerenew/contracts/contracts/oracle/AereRandomnessBeacon.sol` (live-deployed at +`0x25b6317efD8C7d425210F56Ee1E204852CD8213C`) shipped with a placeholder +verifier: + +```solidity +function _verify(uint64 /*round*/, bytes calldata /*signature*/) internal pure returns (bool) { + // Phase 2 implementation goes here. + return true; +} +``` + +It verified nothing. Worse, `strictVerifyEnabled` defaults to `false`, so even +that stub was never called: any bytes could be submitted as a "drand round". It +also derived randomness as `keccak256(signature)`, which is NOT drand's +canonical randomness (`SHA-256(signature)`). + +## What I built + +New files (the live beacon was NOT modified): + +- `aerenew/contracts/contracts/oracle/AereRandomnessBeaconV2.sol` + - `library AereDrandQuicknetBLS` — real BLS12-381 verification on EIP-2537: + - `messageForRound` = `SHA-256(round as 8-byte big-endian)` (quicknet is UNCHAINED) + - `hashToField` = RFC 9380 `expand_message_xmd` (SHA-256, len 128) + reduce + mod p via MODEXP. Uses only SHA-256 (0x02) + MODEXP (0x05), so it runs on + any EVM. + - `hashToG1` = RFC 9380 SSWU_RO to G1 via `BLS12_MAP_FP_TO_G1` (0x10) + + `BLS12_G1ADD` (0x0b). (map already clears the cofactor, and cofactor + clearing is a homomorphism, so `map(u0)+map(u1)` equals the RFC result.) + - `decompressG1` = zcash/ETH2 compressed-G1 decompression via MODEXP sqrt + (p ≡ 3 mod 4, sqrt = a^((p+1)/4)); consumes drand's exact 48-byte sig. + - `verifyRoundCompressed` = pairing check `e(H(m),pk) * e(sig,-G2) == 1` via + `BLS12_PAIRING_CHECK` (0x0f). + - `contract AereRandomnessBeaconV2` — `submitRound` ALWAYS verifies (no phase + flag, no admin off-switch); stores canonical `SHA-256(signature)` randomness. +- `aerenew/contracts/test/AereRandomnessBeaconV2.test.js` — real drand vectors. +- `aerenew/contracts/hardhat.config.prague.js` — pins the local `hardhat` + network to the `prague` hardfork so EIP-2537 is available for the full test. + +**Fail-closed everywhere:** any wrong-length input, absent precompile (empty +returndata), wrong-length precompile output, non-square x, point at infinity, or +failed pairing resolves to `false`. There is no path that returns `true` without +a genuine pairing equality. When EIP-2537 is absent, verification returns +`false` and `submitRound` reverts (proven by the fail-closed-absence test). + +## drand chain targeted (pinned, not guessed) + +League of Entropy **quicknet**, scheme `bls-unchained-g1-rfc9380` (confirmed live +at `api.drand.sh//info`): + +- chain hash: `52db9ba70e0cc0f6eaf7803dd07447a1f5477735fd3f661792ba94600c84e971` +- public key (G2, 96-byte compressed): + `83cf0f2896adee7eb8b5f01fcad3912212c437e0073e911fb90022d3e760183c8c4b450b6a0a6c3ac6a5776a2d1064510d1fec758c921cc22b0e17e63aaf4bcb5ed66304de9cf809bd274ca73bab4af5a6e9c76a4bc09e76eae8991ef5ece45a` +- period 3 s, genesis 1692803367, unchained, sigs on G1 / pubkey on G2 +- hash-to-curve DST: `BLS_SIG_BLS12381G1_XMD:SHA-256_SSWU_RO_NUL_` + +All scheme parameters were proven correct BEFORE writing Solidity, by +independently verifying genuine round 1000000 with `@noble/curves` (pairing of +`H(m)` against the pubkey equals pairing of the signature against the G2 +generator → true; wrong round → false). + +## Real test vectors used (genuine, from api.drand.sh) + +- round 1000000: sig `83ad29e4...abe72`, randomness `b22aad47...440af3` +- round 1000001: sig `a5bd91e5...c4218`, randomness `9f45f439...84ff` + (used as a valid-but-wrong-round negative case) + +Confirmed on-chain: `SHA-256(sig)` reproduces the published randomness for both. + +## Test result (REAL, not [MEASURE]) + +Run from `aerenew/contracts`: + +1. Default config (`cancun`, no EIP-2537): + `npx hardhat test test/AereRandomnessBeaconV2.test.js` + -> **11 passing, 5 pending**. Message reconstruction, RFC 9380 hash-to-field + (matches @noble reference), G1 decompression (matches @noble reference), + canonical randomness, input validation, and the fail-closed-absence checks all + pass. The pairing cases correctly report `[MEASURE]` and skip because the + precompiles are absent. + +2. Prague config (EIP-2537 live in the local EDR EVM): + `npx hardhat test test/AereRandomnessBeaconV2.test.js --config hardhat.config.prague.js` + -> **15 passing, 1 pending**. Full on-chain BLS verification: + - hash-to-curve to G1 matches the independent @noble reference + - genuine round 1000000 verifies **true**; genuine round 1000001 verifies **true** + - valid signature submitted for the wrong round verifies **false** + - tampered signature verifies **false** + - `submitRound(1000000, genuineSig)` stores randomness == published + `b22aad47...440af3`; double-submit reverts; a non-verifying signature reverts + fail-closed with no storage. + +The local EDR EVM at the `prague` hardfork implements the same EIP-2537 spec that +is "Supported" on Aere mainnet (per `docs/AERE-EIP-COMPATIBILITY-MATRIX.md`), so +this is a genuine end-to-end pass of the on-chain verification logic. + +## Honest status + +- This is a BUILT-AND-TESTED replacement, NOT a live swap. The deployed beacon + was not touched. Activating V2 (or wiring real verification into the live + contract) on Aere mainnet is founder-gated. +- [MEASURE, optional] A final confirmation run against the actual Aere mainnet + RPC (chain 2800) would close the loop that mainnet's EIP-2537 matches the + local EDR semantics. The compatibility matrix lists 2537 as Supported; the + logic itself is proven locally on an EIP-2537 EVM. +- QUANTUM SCOPE: drand's BLS12-381 is CLASSICAL cryptography and is + Shor-breakable. This fix makes the beacon actually verify what it stores (a + correctness + honesty fix). It does NOT make the randomness post-quantum and + is unrelated to Aere's PQC precompile track (Falcon/ML-DSA/SLH-DSA). + +## [VERIFY] flags + +- None on the drand scheme parameters: the DST, message construction, and G1/G2 + placement are all confirmed by the genuine round verifying true both in + @noble/curves and in the on-chain pairing. +- The embedded `PUBKEY_G2` and `NEG_G2_GENERATOR` constants are off-chain + decompressions of, respectively, the canonical 96-byte compressed quicknet key + and the standard BLS12-381 G2 generator. They are reproducible by anyone and + are transitively validated by the passing pairing (a wrong pubkey/generator + would make round 1000000 fail). Not a blocking [VERIFY], but flagged as a + precomputed constant for an auditor to re-derive. diff --git a/AERE-ERC7683-DESTINATION-SUMMARY.md b/AERE-ERC7683-DESTINATION-SUMMARY.md new file mode 100644 index 0000000..658eeaf --- /dev/null +++ b/AERE-ERC7683-DESTINATION-SUMMARY.md @@ -0,0 +1,59 @@ +# Spec 8 - ERC-7683 Destination Settler for Aere Network + +## What was built (all new files, deployed origin contracts untouched) + +1. `aerenew/contracts/contracts/intents/AereDestinationSettler.sol` + - Implements ERC-7683 `IDestinationSettler.fill(bytes32 orderId, bytes originData, bytes fillerData)` + from the existing `contracts/intents/IERC7683.sol` (reused, not redefined). + - A solver (msg.sender = filler) delivers the promised output straight to the recipient + on Aere via OpenZeppelin SafeERC20 (no custody), records the fill, emits `Filled`. + - `originData` = the origin's declared output leg, matching AereSpokePool `_buildResolved`: + `abi.encode(bytes32 orderId, address outputToken, uint256 outputAmount, bytes32 recipient)`. + - `fillerData` = `abi.encode(address deliveredToken, uint256 deliveredAmount, + address deliveredRecipient, bytes32 repaymentAddress)`. + - Fail-closed reverts: `OrderIdMismatch`, `ZeroRecipient`, `ZeroAmount`/`ZeroAddress`, + `AlreadyFilled` (duplicate), `OutputMismatch` (wrong token/recipient or short amount). + - Views: `fills`, `getFill`, `isFilled`, `fillCount`, and `fillCommitment(orderId)` + (canonical repayment binder = keccak256 over AERE_CHAIN_ID=2800, settler, orderId, + filler, outputToken, outputAmount, recipient, repaymentAddress). + - nonReentrant; checks-effects-interactions. + +2. Finality / repayment wiring (real reference, not a live cross-chain claim): + - Declares `IAereQbftFinalityLightClient` matching the deployed + `contracts/interop/AereZkQbftLightClient.sol` (0xCaDA54FA...6488): the SP1 Groth16 + QBFT-finality prover (guest `qbft-lightclient-guest`, quorum ceil(2N/3) = 5-of-7). + - `FILLED_EVENT_SIG` + `Filled` log + `fillCommitment` are the on-chain surface an + origin-side `AereOutboundVerifierV2`-style verifier consumes: it proves the `Filled` + log was included in a QBFT-final Aere block (validator-set anchored) and repays the + solver, no trusted relayer. + - The light client is deployed on the consuming/origin chain (Aere is native on Aere), + so the settler does NOT call it on-chain; documented, not faked. + +3. `aerenew/contracts/test/destination-settler.test.js` - RAN, 4 passing: + - valid fill: delivers output, records fill, emits Filled, fillCommitment matches + - duplicate fill reverts (AlreadyFilled) + - mismatched-output reverts (OutputMismatch) - tested short amount, wrong recipient, wrong token + - zero-recipient reverts (ZeroRecipient) + - Command: `npx hardhat test test/destination-settler.test.js` from aerenew/contracts. + +4. `aerenew/docs/AERE-ERC7683-DESTINATION.md` - origin+destination composition, solver + flow (lock on origin, fill on destination, prove-and-repay), proof shape, honest status, + and the point that solver liquidity removes the bridge-liquidity bootstrap. + +## REAL test result +Compiled 1 Solidity file successfully. 4 passing (~1s), 0 failing. + +## Flags +- [MEASURE] End-to-end cross-chain repayment (off-chain SP1 prover over the + qbft-lightclient-guest ELF + origin-chain verifier deploy on a 2nd chain) is NOT + exercised on one chain in the unit test. No live cross-chain flow claimed. +- [VERIFY] Exact receipt-trie inclusion encoding for the Filled log: confirm against the + final AereOutboundVerifierV2 guest. +- [VERIFY] ERC-7683 struct shapes taken from the repo's vendored IERC7683.sol (canonical + Input/Output/ResolvedCrossChainOrder/IDestinationSettler); matches AereSpokePool origin side. + +## Scope / honesty +Settlement/interop only. Aere consensus stays classical secp256k1 ECDSA QBFT; the finality +proof is ABOUT that QBFT finality, verified classically (falconVerified required false). +Deployed origin contracts (AereSpokePool, settlement hub) not modified. No em-dashes; brand +"Aere Network"/"Aere", ticker AERE; solc 0.8.23. diff --git a/AERE-ERC7683-DESTINATION.md b/AERE-ERC7683-DESTINATION.md new file mode 100644 index 0000000..fd7ddcb --- /dev/null +++ b/AERE-ERC7683-DESTINATION.md @@ -0,0 +1,188 @@ +# Aere Network ERC-7683 Destination Settler + +The receiving side of cross-chain intents on Aere Network. This document explains how +the origin and destination halves compose, the solver flow, the repayment proof path, +and the honest status of what is on-chain today versus what needs the off-chain solver +and finality prover. + +Contract: `aerenew/contracts/contracts/intents/AereDestinationSettler.sol` +Interface: ERC-7683 `IDestinationSettler` (`contracts/intents/IERC7683.sol`) +Test: `aerenew/contracts/test/destination-settler.test.js` (4 passing) + +## Why a destination settler at all + +Aere Network already ships the ORIGIN side of ERC-7683: `AereSpokePool` +(`contracts/intents/AereSpokePool.sol`) is an `IOriginSettler`. A user locks input +tokens on the origin chain and emits an `Open` event that declares the OUTPUT leg they +want on the destination chain (token, amount, recipient). What was missing is the +DESTINATION half: the contract a solver calls to actually deliver that output and to +record the delivery so the solver can be repaid. `AereDestinationSettler` is that half. + +An intent design like this removes the need to bootstrap bridge liquidity. A classic +lock-and-mint bridge must pre-fund destination-side liquidity before it can serve a +single transfer. An intent bridge does not: the SOLVER fronts their own liquidity to +fill the order, and is repaid the locked input on the origin chain after the fill is +proven final. Aere Network therefore never has to seed or custody bridge liquidity; a +competitive market of solvers supplies it per intent. + +## How origin and destination compose + +``` + ORIGIN CHAIN AERE NETWORK (destination, chain 2800) + ------------ -------------------------------------- + User -> AereSpokePool.open() + locks input, emits Open + (declares output leg) ........> Solver reads Open, calls + AereDestinationSettler.fill(orderId, + originData, fillerData) + - delivers output to recipient + - records the fill + - emits Filled + (fill is included in an Aere block) + | + Aere QBFT finalizes the block + | + Origin-side verifier <........ SP1 proof: "this Filled log was included + (AereOutbound- in a QBFT-final Aere block", validator-set + VerifierV2 pattern) anchored (off-chain prover + on-chain verify) + repays the solver the + locked input +``` + +`originData` is the origin settler's declared output leg. `AereSpokePool` builds it (see +`_buildResolved`) as: + +```solidity +abi.encode(bytes32 orderId, address outputToken, uint256 outputAmount, bytes32 recipient) +``` + +`fillerData` is the solver's actual delivery plus their origin-chain repayment address: + +```solidity +abi.encode(address deliveredToken, uint256 deliveredAmount, address deliveredRecipient, bytes32 repaymentAddress) +``` + +## The solver flow + +1. LOCK on origin. The user calls `AereSpokePool.open()` (or the gasless `openFor` / + `openForPQC`), locking input and emitting `Open` with the declared output leg. +2. FILL on destination. A solver calls `AereDestinationSettler.fill(orderId, originData, + fillerData)` on Aere Network. The settler pulls the output token from the solver and + delivers it straight to the recipient (it never custodies the output), records the + fill, and emits `Filled`. +3. PROVE and REPAY on origin. Once the fill's block is QBFT-final on Aere, an SP1 proof + of finality plus log inclusion is generated off-chain and submitted to an origin-side + verifier, which repays the solver the locked input. No trusted relayer is required; + the proof is validator-set anchored. + +## On-chain fail-closed guarantees + +`fill(orderId, originData, fillerData)` reverts, and records nothing, when: + +| Condition | Error | +| --- | --- | +| `orderId` argument does not equal the id inside `originData` | `OrderIdMismatch` | +| Declared recipient is zero | `ZeroRecipient` | +| Declared output token is zero, or declared amount is zero | `ZeroAddress` / `ZeroAmount` | +| Order already filled once | `AlreadyFilled` | +| Delivered token or recipient does not match the declared output, or delivered amount is short | `OutputMismatch` | + +A fill that delivers the wrong token, to the wrong recipient, or short can never be +recorded, and an order can be filled at most once, so a solver can never be repaid twice +for a single intent. Delivery is atomic: the output is pulled from the solver and sent +to the recipient with OpenZeppelin `SafeERC20` in the same call, after the record is +written (checks, effects, interactions; `nonReentrant`). + +After a successful fill the settler exposes: + +- `fills(orderId)` / `getFill(orderId)`: the full fill record (filler, output token, + amount, recipient, timestamp, block, repayment address). +- `isFilled(orderId)`: whether the order has been filled. +- `fillCommitment(orderId)`: the canonical repayment commitment (see below). + +## Repayment proof path (wiring to Aere's QBFT finality) + +The origin chain must learn "this exact fill was included in a block that is FINAL on +Aere Network" without trusting a relayer. Aere Network already has the machinery, and +the settler is built to plug into it. + +1. FINALITY prover. `contracts/interop/AereZkQbftLightClient.sol` (live on consuming + chains at `0xCaDA54FA...6488`) proves, in the SP1 zkVM (guest + `qbft-lightclient-guest`), that one Aere header is QBFT-final: it decodes the Besu + QBFT `extraData`, recomputes both Besu hash pre-images, ecrecovers each committed + seal, and asserts the distinct-validator count reaches the QBFT quorum `ceil(2N/3)` + (5-of-7 for Aere's live N=7 set), binding to an IMMUTABLE validator-set anchor. The + settler declares this interface as `IAereQbftFinalityLightClient` for reference. This + prover runs on the consuming/origin chain, not on Aere Network (Aere is native there), + so the settler does not call it on-chain. +2. INCLUSION plus delivery. `contracts/interop/AereOutboundVerifierV2.sol` is the + origin-side pattern that CONSUMES such a proof. It accepts an SP1 proof that a + specific Aere log was included in a QBFT-final Aere block (finality plus receipt + inclusion, one guest), binds the proof's committed `validatorSetRoot` to its own + immutable anchor, enforces exactly-once replay, and only then acts. An origin-side + verifier built on this pattern trusts THIS settler as the source address and + `FILLED_EVENT_SIG` as the event, re-derives `fillCommitment` from the proven log, and + repays the solver. + +The on-chain surface the settler must provide for that path is the `Filled` event, the +persisted `FillRecord`, and the `fillCommitment` binder. It provides all three. + +`fillCommitment(orderId)` binds: + +```solidity +keccak256(abi.encode( + AERE_CHAIN_ID, // 2800, matching AereOutboundVerifierV2.AERE_CHAIN_ID + address(this), // this settler + orderId, + filler, // solver, repaid on the origin chain + outputToken, + outputAmount, + recipient, + repaymentAddress // solver's origin-chain repayment address +)) +``` + +### Proof shape + +The origin-side proof is exactly the shape `AereOutboundVerifierV2` already documents: an +SP1 Groth16 proof over Aere QBFT finality plus log inclusion, with the guest committing +`validatorSetRoot` into its public values and the on-chain verifier binding that root to +an immutable anchor. Public values are the 288-byte (9 word) `abi.encode` of `(uint64 +chainId, uint64 blockNumber, bytes32 blockHash, bytes32 root, uint8 claimKind, bytes32 +commitment, bytes32 validatorSetRoot, bool finalized, bool falconVerified)`. The pure +finality proof consumed by `AereZkQbftLightClient` is the narrower 192-byte (6 word) +form. The exact receipt-trie inclusion encoding for this settler's `Filled` log is +[VERIFY: confirm against the final AereOutboundVerifierV2 guest]. + +## Honest status + +ON-CHAIN and tested today (`test/destination-settler.test.js`, 4 passing on Hardhat): + +- A valid fill delivers the output to the recipient, records the fill, emits `Filled`, + and exposes the record plus `fillCommitment`. +- A duplicate fill reverts (`AlreadyFilled`). +- A mismatched-output fill reverts (`OutputMismatch`), tested for short amount, wrong + recipient, and wrong token. +- A zero-recipient fill reverts (`ZeroRecipient`). + +NOT on one chain, marked [MEASURE]: + +- The end-to-end cross-chain flow (off-chain SP1 prover run over the + `qbft-lightclient-guest` ELF, plus the origin-chain verifier deployment that repays the + solver) is NOT exercised by this contract or its unit test. It needs the separate + off-chain prover and a second chain. This is a settlement / interop composition, not a + claim of a live cross-chain transfer. +- The exact receipt-trie inclusion encoding is [VERIFY: confirm against the final + AereOutboundVerifierV2 guest]. + +SCOPE. This is a settlement / interop-layer contract. It does not touch, gate, or change +Aere Network consensus, which remains classical secp256k1 ECDSA QBFT. The finality proof +above is a proof ABOUT that QBFT finality, verified classically today. That is the +honest and intended posture, not a post-quantum consensus claim. The `falconVerified` +slot in the proof public values is recorded and required to be `false` on mainnet. + +Repayment security reduces to the honesty of at least `2f+1` of Aere Network's QBFT +validators (5-of-7 today, all Foundation-operated: an operator assumption, not an +economic one) plus a sound SP1 / Groth16 verifier and the correct validator-set anchor. +Recording a fill here is permissionless and does not, by itself, move any origin funds; +repayment happens only on the origin chain and only behind the proof. diff --git a/AERE-ERC8004-SUMMARY.md b/AERE-ERC8004-SUMMARY.md new file mode 100644 index 0000000..5a0e1dc --- /dev/null +++ b/AERE-ERC8004-SUMMARY.md @@ -0,0 +1,62 @@ +# Spec 5: ERC-8004 + x402/AP2 conformance for Aere's agent stack + +## What was built (all under aerenew/) + +Thin ADAPTERS over the LIVE, already-deployed agent primitives. Nothing live was redeployed or modified. + +New dir: `aerenew/contracts/contracts/erc8004/` +- `IERC8004.sol` - modeled ERC-8004 Identity / Reputation / Validation interfaces ([VERIFY] flagged). +- `AereIdentityRegistry8004.sol` - Identity adapter over the deployed AereAgentDID (0xce64..22C5). + agentId == the DID's Falcon root key id; register binds AgentCard URI + domain to an existing DID agent, + controller-gated; resolve by id/domain/address; DID string did:aere::. +- `AereReputationRegistry8004.sol` - Reputation adapter over the deployed AereAIReputation (0x781e..feBF). + READ path (getScore/getStats) reads the live scoreOf/statsOf directly. WRITE path (giveFeedback) forwards + to live attest; needs the adapter to be a registered attestor (live set is immutable Foundation-only, so + write-through is a founder-gated governance step -> honest AdapterNotAttestor revert + canWriteThrough()). +- `AereValidationRegistry8004.sol` - THE DIFFERENTIATOR. ERC-8004 validation request/respond where the + response proof is a Falcon-512 or ML-DSA-44 signature verified on-chain via the live precompiles + (0x0AE1 / 0x0AE3) through AerePQCKeyRegistry.verifyWithKey. Fail-closed, non-replayable, challenge-bound. +- `AereAP2MandateVerifier.sol` - x402/AP2 payment mandate ("agent X may spend up to N per period for purpose + P") signed with Falcon-512 (PQC), verified via 0x0AE1. verifyMandate (view) + authorizeSpend (enforced: + window + cap + PQC). Settlement routes through the existing AERE402 rail (not redeployed); optional + SETTLEMENT_EXECUTOR gate. + +Test: `aerenew/contracts/test/erc8004-adapters.test.js` +Doc: `aerenew/docs/AERE-ERC8004-X402-CONFORMANCE.md` (mapping table + PQC differentiator + honest status) + +## REAL test result + +`npx hardhat test test/erc8004-adapters.test.js` from aerenew/contracts -> **18 passing** (~2s). +Compiled 5 Solidity files (solc 0.8.23). Covers: identity register/resolve + controller gating; reputation +attest->read (forward into live AereAIReputation, score reads back) + honest not-attestor revert; validation +Falcon-512 (0x0AE1) accepted + ML-DSA-44 (0x0AE3) accepted + tampered rejected fail-closed + score-binding + +stale-precompile-invalid; mandate verify/authorize/cap/expiry/tampered-fail-closed/revoke-halt/executor-gate. + +## Flags + +- [MEASURE] Local Hardhat has no PQC precompile. Test installs the repo's MockPQCPrecompile at 0x0AE1/0x0AE3 + via hardhat_setCode (same as the AereRecoveryRegistry fault-harness). Mock parses at the LIVE precompile + spec offsets (accept iff commitment == keccak256(pk||message)), so a pass proves correct input routing + + fail-closed. Real precompile acceptance is proven separately vs live mainnet 2800 via eth_call (as + AerePQCKeyRegistry/AerePQCAttestation are), NOT re-proven in this unit test. Adapters stay wired to + 0x0AE1/0x0AE3 for production. +- [VERIFY] ERC-8004 exact selectors are evolving (identity trending to ERC-721 register/tokenURI; + reputation/validation arg orders unsettled). Adapters implement documented semantics; selector-level + conformance reconcile pending. Marked in NatSpec + doc. +- [VERIFY] x402/AP2 mandate field set still evolving (AP2 Intent vs Cart; x402 HTTP-402 payload). Struct + captures the common "spend up to N per period for purpose Q" authorization. +- [VERIFY] Reputation write-through needs Foundation to authorize this adapter as an attestor on mainnet + (immutable live set) - external/founder-gated. Read path works against the live instance today. + +## Honesty boundaries respected + +- Adapters wrap live contracts, do NOT redeploy them. Consensus is NOT made post-quantum (still Besu QBFT + classical ECDSA); only the validation-response and mandate AUTHENTICITY are PQC. +- Standard-adoption by the wider ecosystem is external, stated as not controlled by Aere. +- Brand "Aere Network"/"Aere" title case, ticker AERE uppercase; no em-dashes / "--" in doc prose. + +## Live addresses used (chain 2800) +AereAgentDID 0xce641d7d7C10553D82b06B7C21d423550e7522C5 | AereAIReputation 0x781ef746c08760aa854cDa4621d54db6734bfeBF +AereAgentBond 0x32E0015F622a8719d1C380A87CE1a09bcd0cB86A | AerePQCKeyRegistry 0x1eCa3c5ADcBD0b22636D8672b00faC6D89363691 +AERE402FacilitatorV2 0xFC2f7FAa94919caF1126b3c995F0F6AcCef291de | AereSink 0x69581B86A48161b067Ff4E01544780625B231676 +Precompiles: 0x0AE1 Falcon-512, 0x0AE3 ML-DSA-44 (live, activation block 9,189,161) diff --git a/AERE-ERC8004-X402-CONFORMANCE.md b/AERE-ERC8004-X402-CONFORMANCE.md new file mode 100644 index 0000000..ddf4b44 --- /dev/null +++ b/AERE-ERC8004-X402-CONFORMANCE.md @@ -0,0 +1,236 @@ +# Aere Network: ERC-8004 and x402/AP2 Conformance + +Status: adapters built and tested. The live deployed agent contracts are unchanged. Adoption of these +standards by the wider agent ecosystem is external to Aere and is not something Aere controls. + +This document describes how Aere Network conforms to two emerging agent standards through THIN ADAPTERS +over its already deployed, live agent stack, and where Aere adds something no one else has: an on-chain +Validation registry and AP2 style mandates whose proofs are POST-QUANTUM signatures (Falcon-512, +ML-DSA-44), verified in full on-chain by Aere's live native precompiles. + +- ERC-8004 ("Trustless Agents") standardizes on-chain agent Identity, Reputation, and Validation + registries on top of the A2A (Agent-to-Agent) protocol. +- x402 (Coinbase) and AP2 (Google, Visa, and partners) standardize agent payment authorizations and + mandates. + +Conforming to these kills the isolation risk of running a private agent trust layer: an Aere agent +becomes discoverable, rateable, and payable by any tool that speaks these standards. Aere's differentiator +is that the trust and payment proofs can be quantum-durable, while everyone else's are ECDSA and therefore +quantum-forgeable. + +Scope boundary (honest): these are APPLICATION LAYER adapters and verifiers. They do NOT make Aere +consensus post-quantum. Aere blocks are still produced and signed by Besu QBFT validators with classical +secp256k1 ECDSA. What is post-quantum here is the AUTHENTICITY of a validation response and of a payment +mandate, verified by the live precompiles. + +## What was built + +New directory `aerenew/contracts/contracts/erc8004/`: + +| File | Role | +| --- | --- | +| `IERC8004.sol` | The modeled ERC-8004 Identity, Reputation, and Validation registry interfaces. | +| `AereIdentityRegistry8004.sol` | ERC-8004 Identity adapter over the deployed AereAgentDID. | +| `AereReputationRegistry8004.sol` | ERC-8004 Reputation adapter over the deployed AereAIReputation. | +| `AereValidationRegistry8004.sol` | ERC-8004 Validation registry with POST-QUANTUM proofs (the differentiator). | +| `AereAP2MandateVerifier.sol` | x402/AP2 payment mandate verifier with a Falcon-512 (PQC) mandate signature. | + +Test: `aerenew/contracts/test/erc8004-adapters.test.js` (18 passing, see "Test result" below). + +The adapters take the live contract addresses in their constructors and wrap them. They never redeploy +or modify the underlying deployed primitives. + +## Live deployed primitives being adapted (Aere mainnet, chain 2800) + +| Primitive | Address | Notes | +| --- | --- | --- | +| AereAgentDID | `0xce641d7d7C10553D82b06B7C21d423550e7522C5` | Falcon rooted agent identity; agent id is the Falcon root key id. | +| AereAIReputation | `0x781ef746c08760aa854cDa4621d54db6734bfeBF` | Composable reputation keyed by (operator, agentId); attestor set fixed at deploy (Foundation). | +| AereAgentBond | `0x32E0015F622a8719d1C380A87CE1a09bcd0cB86A` | Slashable stake feeding the reputation score. | +| AerePQCKeyRegistry | `0x1eCa3c5ADcBD0b22636D8672b00faC6D89363691` | PQC public key registry; `verifyWithKey` routes to the live precompile for the key's scheme. | +| AERE402FacilitatorV2 | `0xFC2f7FAa94919caF1126b3c995F0F6AcCef291de` | HTTP 402 settlement rail (classical hot session signature), 25 bps fee to AereSink. | +| AERE402FacilitatorPQC | READY, not yet deployed | Falcon rooted settlement rail (built and tested). | +| AereSink | `0x69581B86A48161b067Ff4E01544780625B231676` | Immutable 3 bucket fee router. | + +Live native precompiles (activated on mainnet 2800 at block 9,189,161): + +| Scheme | Precompile | Standard | +| --- | --- | --- | +| Falcon-512 | `0x0AE1` | NIST FIPS 206 draft line | +| ML-DSA-44 | `0x0AE3` | NIST FIPS 204 (Dilithium2) | + +## ERC-8004 mapping table + +| ERC-8004 requirement | Aere adapter (function) | Underlying live contract (call) | +| --- | --- | --- | +| Identity: register an agent with a DID and metadata URI | `AereIdentityRegistry8004.register(agentId, agentDomain, agentCardURI)` | AereAgentDID.agentExists + AerePQCKeyRegistry.ownerOf (controller gate); metadata stored in the adapter (the live DID carries no AgentCard URI). | +| Identity: resolve an agent | `AereIdentityRegistry8004.getAgent / resolveByDomain / resolveByAddress` | AereAgentDID (agent existence) + AerePQCKeyRegistry.ownerOf (current controller as agentAddress). DID string `did:aere::`. | +| Reputation: attest feedback | `AereReputationRegistry8004.giveFeedback(agentId, delta, evidenceHash, uri)` | AereAIReputation.attest(operator, bytes32(agentId), delta, evidenceHash, uri). | +| Reputation: read feedback | `AereReputationRegistry8004.getScore / getStats` | AereAIReputation.scoreOf / statsOf (read straight from the deployed contract). | +| Validation: request | `AereValidationRegistry8004.requestValidation(validatorKeyId, serverAgentId, dataHash)` | AerePQCKeyRegistry (validator key ACTIVE + Falcon-512/ML-DSA-44) + AereAgentDID.agentExists (server agent). | +| Validation: respond with a proof | `AereValidationRegistry8004.respondValidation(requestId, response, pqcProof)` | AerePQCKeyRegistry.verifyWithKey -> live precompile 0x0AE1 / 0x0AE3 (full on-chain PQC verification, fail-closed). | + +### Identity mapping detail + +The ERC-8004 agent id IS the AereAgentDID agent id, which is the Falcon ROOT key id in AerePQCKeyRegistry +(`agentId == rootKeyId`). So an ERC-8004 resolve is a direct pass-through to the live DID: the agent's +on-chain root of authority is a quantum-durable Falcon key, not a bare secp256k1 address. `register` does +not mint a new identity (it already exists in the live DID). It binds an ERC-8004 AgentCard URI and domain +to an existing DID agent, gated to that agent's current controller (the registry owner of the Falcon root +key), so only the party that proved Falcon possession can publish the agent's ERC-8004 metadata. + +`[VERIFY: confirm against the finalized ERC-8004 interface]` The newer ERC-8004 Identity draft leans toward +an ERC-721 registration (`register(tokenURI)` minting a sequential id). Aere anchors the ERC-8004 identity +to the pre-existing Falcon rooted DID id instead, because the trust root is the on-chain Falcon key rather +than a token. The resolve, getAgent, and AgentCard URI semantics match ERC-8004; the id minting selector +differs by design and is documented in the contract NatSpec. + +### Reputation mapping detail + +The live reputation is keyed by (operator address, bytes32 agentId). The adapter derives operator as the +agent's current controller (resolved from the Identity adapter) and agentKey as `bytes32(agentId)`, so an +ERC-8004 read or write addresses exactly one live reputation slot, deterministically. + +Honest write constraint: AereAIReputation's attestor set is fixed at its deploy and has no add path. For +`giveFeedback` to land in the live score, the adapter must be a registered attestor on the reputation +instance it is constructed with. The currently live AereAIReputation lists the Foundation attestor only +(immutable), so pairing this adapter for write-through is a Foundation governance decision, external to this +contract and founder gated. `[VERIFY: on mainnet, register this adapter as an attestor before relying on +giveFeedback, or have the Foundation attestor call the live attest directly.]` The READ path needs no such +authorization and adapts the currently deployed instance as is. The adapter surfaces this with +`canWriteThrough()` and a clear `AdapterNotAttestor` revert, and the test proves both the authorized +write-through path and the unauthorized honest revert. + +`[VERIFY: confirm against the finalized ERC-8004 interface]` Later ERC-8004 reputation drafts carry a richer +feedback payload (score, tag, response URI). Here the feedback signal is normalized to the live model's +delta in {-1, 0, +1} so no information is invented beyond what the deployed contract records. + +## The post-quantum differentiator: Validation registry + +`AereValidationRegistry8004` is the piece no other agent stack offers. It exposes the ERC-8004 Validation +surface (request and respond with a proof), where the validator's RESPONSE proof is a POST-QUANTUM signature +(Falcon-512 or ML-DSA-44), verified in full ON-CHAIN by Aere's live native precompiles (0x0AE1, 0x0AE3) +through the deployed AerePQCKeyRegistry. + +Flow: + +1. `requestValidation(validatorKeyId, serverAgentId, dataHash)`. Records a request that the PQC validator + identified by `validatorKeyId` validate the work the server agent committed to via `dataHash`. The + validator key must be an ACTIVE Falcon-512 or ML-DSA-44 key in the registry; the server agent must exist + in the live AereAgentDID. +2. `respondValidation(requestId, response, pqcProof)`. The validator answers with a score (0..100, the + ERC-8004 convention) and a PQC signature over the contract's domain separated challenge, which binds + (requestId, dataHash, serverAgentId, validatorKeyId, response). The signature is verified on-chain via + the live precompile. On success the response is recorded once. On any invalid or tampered proof the call + REVERTS and records nothing (FAIL-CLOSED). An empty or zero precompile return (a stale, un-activated + chain) is treated as INVALID. + +Non-replayable and non-forgeable: the challenge binds chainId, this contract, the exact request tuple, and +the response, so a proof for one (request, response) can never be reused for another, another contract, or +another chain. A request completes exactly once. Authorship is the PQC signature alone: respond may be +relayed by any sender, since only the validator private key can produce a valid signature over the contract +bound challenge. + +Why it matters: every other agent validation stack authenticates validator responses with ECDSA, which a +quantum computer forges. This one does not. It is the on-chain, post-quantum answer to "prove an independent +validator actually signed off on this agent's output". + +## x402 / AP2 post-quantum mandate + +`AereAP2MandateVerifier` is a minimal verifier for AP2 style payment MANDATES whose authorizing signature is +POST-QUANTUM (Falcon-512), verified in full on-chain by the live precompile (0x0AE1) through the deployed +AerePQCKeyRegistry. Settlement of the authorized spend routes through the EXISTING AERE402 rail +(AERE402FacilitatorPQC or AERE402FacilitatorV2), which is not redeployed or modified. + +The struct: + +```solidity +struct Mandate { + uint256 agentKeyId; // the paying agent's Falcon-512 key in AerePQCKeyRegistry + address token; // the settlement token the cap is denominated in + uint256 maxAmount; // cumulative spend cap over the window + uint64 periodStart; // unix seconds, inclusive + uint64 periodEnd; // unix seconds, inclusive + bytes32 purpose; // opaque purpose tag, e.g. keccak256("inference:anthropic") + uint256 mandateNonce; // per-agent mandate index (lets an agent hold several mandates) +} +``` + +This encodes the common AP2/x402 authorization: "agent X may spend up to N of token T per period P for +purpose Q". `mandateHash(m)` binds chainId and the verifier address, so a signed mandate cannot be replayed +against another verifier or chain. + +The verify path: + +- `verifyMandate(m, falconSig)`: a pure on-chain PQC check that the agent's Falcon key signed the mandate + (view, permissionless, free via eth_call). +- `authorizeSpend(m, amount, falconSig)`: the enforced path. Verifies the Falcon mandate signature via the + live precompile, checks the validity window and the cumulative cap, records the spend against the mandate, + and emits `MandateAuthorized`. Fail-closed on any invalid or tampered signature, an out-of-window mandate, + or a cap overflow. Rotating or revoking the agent's Falcon key halts the mandate immediately. + +Settlement routing: `authorizeSpend` records that `amount` is authorized under the mandate; the actual token +movement plus the 25 bps fee to AereSink is performed by the live AERE402 rail. To keep the cumulative cap +honest (only real settlements should consume it), `authorizeSpend` is gated to an immutable +`SETTLEMENT_EXECUTOR` when one is configured (the AERE402 facilitator, which calls it atomically with +settlement). When `SETTLEMENT_EXECUTOR` is the zero address the accounting path is open (for verification and +testing); the pure PQC check `verifyMandate` is always open. + +Why it matters: AP2 and x402 mandates today are ECDSA authorizations, quantum-forgeable. An Aere mandate is a +Falcon-512 authorization, quantum-durable, verified on-chain. + +`[VERIFY: confirm against the finalized x402 / AP2 mandate schema]` The x402 and AP2 mandate field sets are +still evolving (AP2 distinguishes Intent versus Cart mandates; x402 carries an HTTP 402 payment payload). +This struct captures the common "spend up to N per period for purpose Q" authorization; reconcile the exact +field set and encoding with the final specs before claiming wire level conformance. + +## Test result (real) + +Command, run from `aerenew/contracts`: + +``` +npx hardhat test test/erc8004-adapters.test.js +``` + +Result: 18 passing. + +- Identity: register an existing DID agent, resolve by id / domain / controller address, controller only + register and update, unknown agent and duplicate domain rejection. +- Reputation: forward feedback into the live AereAIReputation and read the score back (attest then read), + out-of-range delta and unregistered agent rejection, and the honest AdapterNotAttestor revert when the + adapter is not an authorized attestor (the immutable mainnet case), with the read path still working. +- Validation: a genuine Falcon-512 (0x0AE1) response accepted and recorded, a genuine ML-DSA-44 (0x0AE3) + response accepted, a tampered proof rejected fail-closed with nothing recorded, a proof bound to a + different response score rejected, a wiped precompile treated as invalid, and request guards + (inactive/non-PQC validator key, unknown server agent). +- Mandate: a genuine Falcon mandate verified (pure view) and spend authorized up to the cap, over-cap + rejected, expired window rejected, tampered signature rejected fail-closed, revoked Falcon key halts the + mandate, and the settlement-executor gate enforced. + +`[MEASURE]` Local Hardhat has no PQC precompile, so the test installs the repo's `MockPQCPrecompile` at +0x0AE1 and 0x0AE3 via `hardhat_setCode`, exactly as the fault-harness `AereRecoveryRegistry` test does. The +mock parses the input at the LIVE precompile's spec offsets and accepts iff commitment equals +keccak256(pk || message), so a positive result proves the adapter routed the correct input to the correct +precompile and enforces fail-closed and non-replay semantics. The REAL precompile path (that the on-chain +0x0AE1 / 0x0AE3 accept a genuine Falcon-512 / ML-DSA-44 signature) is exercised separately against live +mainnet 2800 via eth_call, the same way AerePQCKeyRegistry and AerePQCAttestation are proven, and is not +re-proven inside this unit test. The adapters stay hard-wired to the live registry and precompiles for +production. + +## Honest status summary + +- The adapters are built and tested. They wrap the live deployed contracts and do NOT redeploy or modify + them. +- The Identity resolve path and the Reputation read path adapt the currently deployed contracts as is, with + no change and no authorization. +- The Reputation write-through path requires the adapter to be an authorized attestor on the reputation + instance; the live instance's attestor set is immutable Foundation-only, so this is an external, founder + gated governance decision. +- The Validation registry and the AP2 mandate verifier verify Falcon-512 and ML-DSA-44 signatures through the + live precompiles. This is application layer post-quantum authentication. It does NOT make Aere consensus + post-quantum. +- Selector level conformance with the final ERC-8004 and x402/AP2 texts is marked `[VERIFY]` wherever the + specs are still in flux; the adapters implement the documented semantics. +- Whether the wider agent ecosystem adopts these standards is external to Aere and is not something Aere + controls. What Aere controls is being ready and being the only stack whose agent validation and payment + mandates can be quantum-durable. diff --git a/AERE-FAULT-INJECTION-HARNESS.md b/AERE-FAULT-INJECTION-HARNESS.md new file mode 100644 index 0000000..7878695 --- /dev/null +++ b/AERE-FAULT-INJECTION-HARNESS.md @@ -0,0 +1,123 @@ +# Spec 3: Deterministic fault-injection harness + on-chain attested recovery + +Built 2026-07-19. Purpose: turn "we ran some fault tests" into a reproducible adversarial evidence +suite that de-risks the biggest gated item (the post-quantum consensus flip) for zero capital. +Extends the existing measured fault-tolerance work into a repeatable chaos matrix plus an on-chain +recovery-attestation contract, honest about what runs locally vs what needs a live testnet. + +**Scope boundary (held throughout):** this DE-RISKS the consensus flip. It does NOT activate +post-quantum consensus. That flip stays founder-gated and audit-gated. + +--- + +## Part 1: `AereRecoveryRegistry.sol` (REAL, BUILT + TESTED) + +- Contract: `aerenew/contracts/contracts/AereRecoveryRegistry.sol` (solc 0.8.23, repo style). +- Test: `aerenew/contracts/test/AereRecoveryRegistry.test.js`. + +Records recovery events (validator-set drop below quorum -> halt -> subsequent resume), each +authenticated by a Falcon-512 signature verified on-chain by the LIVE precompile 0x0AE1. +- Fields per record: haltHeight, resumeHeight, faultKind (1=crash, 2=netsplit, + 3=byzantine-proposer), attesting operator key (operatorId), Falcon signature over the record + hash, plus validator-set context (nValidators, quorum, aliveDuringFault) that encodes the + "drop below quorum." +- **Fail-closed:** invalid signature, stale nonce, inconsistent heights, or bad validator set + records nothing and advances no nonce; an empty/zero/short precompile return (pre-fork / stale + chain) is treated as INVALID. Reverts with `PQCVerificationFailed`. +- **Append-only:** records live in a push-only array; recordId is an immutable index; a strictly + increasing per-operator nonce is consumed each write (no replay). There is NO owner, admin, or + overwrite/delete function anywhere (structurally verified in the test's ABI scan). +- Wired to 0x0AE1 for production; Falcon-512 encoding matches the live precompile + (pk 897/header 0x09; envelope nonce(40) || esig(0x29..)), mirroring `AerePQCAttestation.sol`. + +### REAL TEST RESULT: 10/10 PASSING +Command: `npx hardhat test test/AereRecoveryRegistry.test.js` from `aerenew/contracts`. +Compiled clean; all 10 tests green (~1s): +- registerOperator: accepts well-formed Falcon-512 key + sequential ids; rejects wrong length/header. +- valid attestation records: kill-2 (f=2 boundary) crash recovery stores every field; netsplit + + byzantine-proposer under one operator with nonce advancing. +- fail-closed: tampered signature rejected (nothing recorded); signature bound to different + heights/fault-kind rejected; empty precompile return treated invalid; unknown operator / invalid + fault kind / bad heights / bad validator set all revert. +- append-only: appends without rewriting an earlier record; replay of a consumed signature rejected; + ABI exposes no set/update/delete/overwrite/admin/owner function. + +**[MEASURE] flag on Part 1:** the Hardhat EVM has no 0x0AE1, so the test installs the repo's +faithful `MockPQCPrecompile` (scheme 1) at 0x0AE1 via `hardhat_setCode` (same pattern the existing +`AerePQCAttestation.test.js` uses). The mock parses input at the LIVE precompile's spec offsets, so +a passing record proves the contract builds the 0x0AE1 input correctly. The real-precompile path +(that on-chain 0x0AE1 accepts a genuine Falcon-512 signature) is proven separately against live +mainnet 2800 via eth_call, not inside the unit test. + +--- + +## Part 2: chaos-matrix runner (SCAFFOLD + CONFIG; multi-node runs [MEASURE]) + +Under `aerenew/chaos/`: +- `matrix.json` — single source of truth. N=7 (quorum 5, f=2) and N=9 (quorum 6, crash-tol 3) + fault matrix: C1 kill-1, C2 kill-2 (N=7 f=2 boundary), C3 kill-3 (N=7 sub-quorum halt / N=9 + crash boundary), C4 kill-4 (N=9 sub-quorum halt), P1 network partition (minority halts), B1 + byzantine-proposer. Documented tool = Pumba (toxiproxy / Chaos Mesh as alternatives), plus a + process-mode fallback that reuses the existing `audit-package-pq-consensus/harness/n7/` scripts. +- `run-chaos-matrix.sh` — reads the matrix, injects each fault, snapshots per-node heights across + the fault + recovery windows, decides halt/resume/fork, and (on a halt-then-recover) invokes the + attester. Has a hard guard that REFUSES to run on the live infra box. +- `lib/partition.sh` — network partition via pumba netem / iptables so the majority keeps quorum. +- `lib/attest-recovery.js` — ethers script that reads the record hash from the deployed registry, + signs it with the operator's offline Falcon-512 key, and submits `submitRecovery(...)`. + +Validated locally: `matrix.json` parses (6 scenarios, N7/q5 + N9/q6); `bash -n` clean on both +shell scripts; `node --check` clean on the JS. + +**[MEASURE] flag on Part 2:** the ACTUAL multi-node runs require a live isolated QBFT testnet on a +SCRATCH box, NEVER the infra box. The runner is inert without a net up (heights read 0). The +already-measured numbers are CITED from `matrix.json` `evidence`, not re-invented: +- Kill-2 soak (docs/FAULT-TOLERANCE-CHARACTERIZATION-2026-07-14.md): 100 adversarial cycles + (40 RT=4 mixed + 40 RT=1 mixed + 20 pure-Besu), **0 forks, 100/100 self-resync**, rare + temporary self-recovering f=2-boundary stall (3/40 RT=4, 1/40 RT=1, 0/20 Besu) that is inherent + QBFT-at-f=2 (FLP), not a client bug. +- Sub-quorum halt-and-recover and partition (spec 5.3/5.4): halts in place, no fork, resumes from + the exact halt height on restore, no re-genesis. +- Byzantine negatives (harness/n7/run-b-negatives.sh): 1-2 Falcon-faulty TOLERATED (<= f=2), + 3 faulty (> f) HALT post-detection, restore RESUMES with no re-genesis. + +--- + +## Part 3: watchtower design (DESIGN) + +`aerenew/chaos/WATCHTOWER-DESIGN.md`. An independent off-chain observer holding a registered +Falcon-512 key that: (1) detects a halt by combining a progress stall with quorum loss and no +fork (so it does not false-positive on the rare temporary f=2-boundary stall), classifying the +fault kind; (2) waits for quorum restoration, doing nothing that could influence consensus; (3) +submits the signed recovery attestation to Part 1, verified fail-closed by 0x0AE1. Includes the +watchtower's own failure modes and the honest single-operator caveat. + +Composition: Part 2 generates adversarial fault evidence reproducibly, Part 3 produces it live and +independently, Part 1 makes all of it un-doctorable and quantum-durable on chain. Together they +make the flip decision rest on honest, checkable evidence. The flip itself stays a founder + audit +decision; the suite does not pull the trigger. + +--- + +## All [VERIFY] / [MEASURE] flags + +- [MEASURE] Part 1: real-precompile 0x0AE1 acceptance of a genuine Falcon-512 sig is proven vs live + mainnet via eth_call, not in the Hardhat unit test (Hardhat has no 0x0AE1; mock installed there). +- [MEASURE] Part 2: multi-node chaos runs need a live isolated QBFT testnet on a scratch box; not + run here. Existing soak numbers cited, none invented. +- [VERIFY] Part 2/3: `lib/attest-recovery.js` needs the operator's offline Falcon-512 signer + key + (AERE_FALCON_SIGN / AERE_FALCON_KEY) and a chain where 0x0AE1 is live to complete the submit; on + a plain testnet without the precompile the on-chain verify fails closed (correct, safe). +- [MEASURE]/[VERIFY] Part 3: the live watchtower daemon and its detection-threshold tuning against + live inter-validator RTT are designed, not built; single-operator vantage is corroboration, not + independence, until third-party watchtowers run. + +## Files +- aerenew/contracts/contracts/AereRecoveryRegistry.sol +- aerenew/contracts/test/AereRecoveryRegistry.test.js +- aerenew/chaos/matrix.json +- aerenew/chaos/run-chaos-matrix.sh +- aerenew/chaos/lib/partition.sh +- aerenew/chaos/lib/attest-recovery.js +- aerenew/chaos/WATCHTOWER-DESIGN.md +- aerenew/chaos/README.md diff --git a/AERE-FORMAL-BROADEN-REPORT.md b/AERE-FORMAL-BROADEN-REPORT.md new file mode 100644 index 0000000..d635eb8 --- /dev/null +++ b/AERE-FORMAL-BROADEN-REPORT.md @@ -0,0 +1,115 @@ +# Formal-verification broadening: new contract SMT models + canonical runner consolidation + +Date: 2026-07-19. Tooling: Python 3.14.4, z3 4.16.0 (real z3 verdicts, no fabricated greens). +All verdicts below were produced by actually running the scripts. + +## Part 1: four new z3 SMT models (all PROVED, negative controls fired) + +Each model proves its safety property by asserting NOT-property under the real Solidity +guards (z3 returns UNSAT) and pairs every proof with a firing negative control that removes +one guard and returns SAT (non-vacuity). DESIGN-level caveats and [VERIFY]/[MEASURE] items +are stated in each model's SUMMARY block exactly as the money-contract models do. + +### a. pqfinality_smt.py -> PROVED (10 PROVED, 3 CEX-FOUND, 0 FAILED, rc=0) +Contracts: contracts/contracts/pqfinality/AereFinalityCertificateVerifier.sol + +AerePQAttestationKeyRegistry.sol +Proved: quorum threshold is exactly ceil(2N/3) = (2N+2)/3 (Q0 for all N>=1; Q0b anchors +N in {4,5,7,9} -> {3,4,5,6}); an accepted certificate meets that quorum (P1; P1b a 4-of-7 +cert is rejected); it is bound to the live registry validatorSetRoot (P2) and size (P2b); it +is bound to the chainId+registry attestation domain so a cross-chain/registry certificate is +rejected (P3 via injective domain hash; P3b direct); a key rotation that changes the root +makes an old-root certificate unaccept-able (P4 via injective root hash); an empty validator +set is rejected (P5). +Negative controls (all fired SAT): drop quorum -> sub-quorum accepted; drop root binding -> +stale/forged root accepted; drop domain binding -> cross-chain replay accepted. +Caveats stated: SP1 gateway soundness (verifyProof reverts on invalid proof) is a trusted +primitive [VERIFY]; the off-chain zkVM aggregation circuit is [MEASURE], NOT implemented +(contract tests use a MOCK gateway); keccak256 injectivity (root/domain) is [VERIFY]; +additive PQ finality, consensus stays classical ECDSA QBFT; DESIGN math not EVM bytecode. + +### b. pqaggregate_smt.py -> PROVED (7 PROVED, 2 CEX-FOUND, 0 FAILED, rc=0) +Contract: contracts/contracts/mpc/AerePQAggregateVerifier.sol +Proved: a registered committee is well-formed (R0: root!=0, 1<=t<=n, scheme!=0); an accepted +authorization is EXACTLY the registered committee's key set (P1; P1b via committee-root +injectivity, so a foreign key set is rejected); it is bound to the caller's message digest +(P2); it proves at least threshold t distinct signatures (P3); it binds size and scheme as +defense in depth (P4); and the on-chain accept reads only O(1) committee/public fields (keys +not stored), so verification cost is independent of n (P5). +Negative controls (all fired SAT): drop root binding -> a different committee's key set +authorizes; drop digest binding -> a proof for message A authorizes message B. +Caveats stated: SP1 gateway soundness [VERIFY]; off-chain zkVM aggregation circuit [MEASURE], +not implemented (MOCK gateway); keccak256 injectivity [VERIFY]; account/authorization +aggregation not consensus, no funds, no admin; DESIGN math not EVM bytecode. + +### c. credential_registry_smt.py -> PROVED (7 PROVED, 3 CEX-FOUND, 0 FAILED, rc=0) +Contracts: contracts/contracts/compliance/AereTrustRegistry.sol + AereVerifiableCredential.sol +Proved: issuance requires accreditation (A: anchor success => Active AND in-scope; A2: a +None/Suspended/Revoked or out-of-scope issuer cannot anchor) and a valid Falcon-512 issuer +signature (A3); the status history is append-only so a committed record cannot be rewritten +(B, via the standard append relation); revocation is terminal (C: from Revoked no transition +returns to Active); and both the anchored (isValid, D) and presented (verifyPresented, D2) +verification paths are fail-closed on expired / not-yet-valid / revoked / un-accredited. +Negative controls (all fired SAT): drop the accreditation check -> a revoked issuer issues; +allow a status overwrite -> a committed record is silently rewritten; drop the validity +window -> an expired credential is accepted. +Caveats stated: Falcon-512 precompile 0x0AE1 soundness modelled as the sigValid predicate +[VERIFY]; the Bitstring Status List and live issuer status are trusted external oracles; +application-layer, no funds, consensus stays classical ECDSA QBFT; legal weight of any +accreditation is external; DESIGN logic not EVM bytecode. + +### d. recovery_registry_smt.py -> PROVED (5 PROVED, 2 CEX-FOUND, 0 FAILED, rc=0) +Contract: contracts/contracts/AereRecoveryRegistry.sol +Proved: a record is written only if the Falcon-512 signature verifies (FC, fail-closed) and +is well-formed (FC2: fault kind / heights / validator set); the per-operator nonce strictly +increases on every write (NO); a nonce-k signature cannot be replayed once the nonce advances +because the record hash binds the nonce (RP, via injective nonce hash + EUF-CMA verify +predicate); and the records array is append-only so a committed record is never rewritten (AP). +Negative controls (all fired SAT): drop the nonce binding -> one signature replays to rewrite +history; drop append-only -> a committed record is silently overwritten. +Caveats stated: Falcon-512 precompile 0x0AE1 soundness (EUF-CMA, input parsing, +empty-return-is-invalid) modelled as the verify predicate [VERIFY]; keccak256 injectivity of +the nonce-bound record hash [VERIFY]; records attestations only, does not observe consensus or +activate PQ consensus (still classical ECDSA QBFT); uint64 nonce cannot realistically +overflow; DESIGN logic not EVM bytecode. + +## Part 2: canonical runner consolidation + +File changed: aerenew/formal-consensus/run_consensus_verification.py (had a hardcoded MODELS +list of 8 consensus models). Added a CONTRACT_MODELS section wiring in all 7 new contract SMT +scripts written in this loop, keeping the 8 consensus models intact: + computemarket_smt, destinationsettler_smt, migrator_smt (the 3 money models) + + pqfinality_smt, pqaggregate_smt, credential_registry_smt, recovery_registry_smt (the 4 new). +The runner now also captures each child's output and tallies the per-check verdict lines. + +### Canonical runner fresh totals (real run, exit 0) + models run: 15 passed: 15 (8 consensus + 7 contract) + verdict lines: 128 PROVED 79 CEX-FOUND 0 FAILED + RESULT: ALL MODELS PASS (proofs PROVED, negative controls fired) + +Breakdown of the 128/79 (per-check verdict lines, i.e. distinct property checks): + - 4 new models: 29 PROVED / 10 CEX-FOUND (pqfinality 10/3, pqaggregate 7/2, + credential_registry 7/3, recovery_registry 5/2) + - 3 fund-flow models: 26 PROVED / 11 CEX-FOUND (computemarket 16/3, destinationsettler 5/4, + migrator 5/4) + - 8 consensus models: 73 PROVED / 58 CEX-FOUND (remainder) + +Note on scope: the 7 wired-in contract models live in aerenew/formal-consensus/ (the same +directory as the canonical runner). The research-stage staging copy +(aerenew/research-stage/formal-consensus/) is a separate curated publish target with its own +committed expected-output.log and was left unchanged. + +### REPRODUCE.md update +Updated aerenew/REPRODUCE.md section 3b: the "canonical in-tree" subsection previously cited +"8 models" / "8 of 8 models PASS". It now reads "15 models: 8 consensus + 7 contract", "15 of +15 models PASS", with the real fresh runner tally of 128 PROVED / 79 CEX-FOUND / 0 FAILED, the +per-group breakdown above, the names of the 7 newly-added contract models, and a restatement +of the NOT-property-UNSAT + firing-negative-control discipline and the per-model DESIGN / +[VERIFY] / [MEASURE] boundaries. No fabricated numbers: every figure is from the actual run. +The staging "(10 models)" section and the older bash-loop "(9 models)" contract section were +left as-is (correct and separate). + +## Honesty posture +- All verdicts are real z3 output; no green was fabricated. +- Every model has at least one firing negative control (SAT under a removed guard). +- No contract was modified. Only SMT scripts were added, the runner was extended, and + REPRODUCE.md was updated with real fresh numbers. diff --git a/AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md b/AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md new file mode 100644 index 0000000..3c17118 --- /dev/null +++ b/AERE-FORMAL-EXTENSION-MONEY-CONTRACTS.md @@ -0,0 +1,191 @@ +# Formal-verification extension: new fund-flow contracts (z3 SMT + full regression) + +Date: 2026-07-19 +Scope: three new money contracts for Aere Network, modelled in z3 in the exact style of the +existing consensus/contract SMT corpus, plus a full regression of the new-contract test suite to +confirm the recent security fixes (M1 giveFeedback gate, L1 codeless-gateway guards, L2 VectorStore +receipt binding) broke nothing. + +Honesty posture (same caveat as the rest of the corpus): each SMT script checks the DESIGN-level +accounting/guard logic over the modelled transitions with unbounded Ints, NOT the compiled EVM +bytecode. A model counts as non-vacuous only because a NEGATIVE CONTROL (one guard removed) fires a +real counterexample. Trusted external primitives (SP1 gateway proof soundness, the Falcon-512 +precompile at 0x0AE1, SafeERC20 whole-tx revert) are marked [VERIFY] and are not re-proved here. + +All verdicts below are the REAL z3 output and the REAL mocha output, reproduced verbatim from the runs. + +--- + +## PART 1: new z3 SMT models + +All three scripts live in `aerenew/formal-consensus/` (they join the existing corpus next to +`spokepool_smt.py`, `settlementhub_smt.py`, `threshold_account_smt.py`). Run each with +`python