120 lines
10 KiB
Markdown
120 lines
10 KiB
Markdown
# Formal-verification broadening: new contract SMT models + canonical runner consolidation
|
|
|
|
> **Note added 2026-09-24 (consensus).** Where this document says that consensus is classical secp256k1 ECDSA and not post-quantum, read it as the per-block finality statement it was until block 24,300,000 (AIP-22 stage 4, 2026-10-25). Since that block every validator attributes a consensus vote only through its verified post-quantum seal, and a block is post-quantum final once the next anchor, at most 32 blocks later, carries the certificate that covers it; headers still carry classical ECDSA commit seals until AIP-22 stage 5 (this sentence corrected on 2026-10-25). It no longer describes all of consensus on chain 2800: since 2026-08-14 every anchor block must carry a certificate of validator post-quantum seals under its hash (Falcon-512, with SLH-DSA as well since 2026-09-04), and since 2026-09-05 (block 17,250,000) the nine AERE-client validators (nine of the ten) refuse a commit message without a valid Falcon-512 seal of its author, and since 2026-09-08 (block 17,700,000) any QBFT consensus message without one, while the tenth, the second client, enforced that seal only on commit messages until block 24,300,000 and attributes every consensus message only through it since (this clause corrected on 2026-10-12, 2026-10-25 and 2026-10-28; until 2026-10-28 it dated the refusal of every message type to 2026-09-05, the date of the commit layer alone). (Note applied to this document on 2026-09-27.)
|
|
|
|
> **Note added 2026-08-19.** Statements in this document that consensus on chain 2800 is (or remains) classical secp256k1 ECDSA QBFT were written before the post-quantum header anchor went live, and remain true for block-by-block finality. Since block 13,014,000 anchor blocks (every 32nd block, on every one since block 13,889,296) also carry, under the block hash, a certificate of validator Falcon-512 seals, and since 2026-08-14 a node rejects an anchor block with fewer than three valid seals (f+1 of nine; eight or nine are carried in practice). That is a post-quantum checkpoint about every 16 seconds, not a per-block quorum: the claim published on 2026-08-15 that from block 14,050,000 no block finalizes without a post-quantum quorum was wrong (the per-block rule armed at that height is retired in the shipped code in favour of the anchor rules) and was withdrawn on 2026-08-19. Details: https://aere.network/quantum.html and the aere-node repository, anchor/README.md.
|
|
|
|
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.
|