4a0b48588c
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.
263 lines
15 KiB
Python
263 lines
15 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# pqfinality_smt.py
|
|
#
|
|
# SMT proof (z3) of the FAIL-CLOSED acceptance guards of Aere Network's ADDITIVE
|
|
# Post-Quantum Finality Certificate: AereFinalityCertificateVerifier bound to the
|
|
# live AerePQAttestationKeyRegistry. Plus load-bearing NEGATIVE CONTROLS for the
|
|
# quorum, the validator-set-root binding, and the attestation-domain binding.
|
|
#
|
|
# Contracts: contracts/contracts/pqfinality/AereFinalityCertificateVerifier.sol
|
|
# contracts/contracts/pqfinality/AerePQAttestationKeyRegistry.sol
|
|
#
|
|
# A certificate is ONE SP1 proof that a quorum of validators produced a valid
|
|
# hash-based (post-quantum) attestation over a finalized block. verifyCertificate()
|
|
# ACCEPTS a certificate ONLY when every fail-closed guard holds (else it reverts):
|
|
# G0 registry validator set non-empty: n >= 1 (EmptyValidatorSet)
|
|
# G1 root binding: pvRoot == REGISTRY.validatorSetRoot() (ValidatorSetRootMismatch)
|
|
# G2 size binding: pvSize == n (SizeMismatch)
|
|
# G3 domain binding: pvDomain == attestationDomain (DomainMismatch)
|
|
# attestationDomain = keccak(DOMAIN_PREFIX, chainId, registry)
|
|
# G4 quorum: pvQuorum >= ceil(2N/3) = (2N+2)/3 (BelowQuorum)
|
|
# G5 non-zero block: pvBlockHash != 0 (ZeroBlockHash)
|
|
# G6 SP1 proof verifies through the pinned vkey + gateway (verifyProof reverts on bad proof)
|
|
#
|
|
# We model the guards as first-order constraints over the decoded public-values
|
|
# fields and prove each safety property by asserting its NEGATION under the guards
|
|
# and showing z3 returns UNSAT (no counterexample). Each NEG-CTRL removes exactly
|
|
# one guard and shows the corresponding bypass becomes satisfiable (SAT).
|
|
#
|
|
# Roots / domains / block hashes are modelled as Int identities (the proof needs
|
|
# equality / disequality, not byte layout). keccak256 is modelled as an INJECTIVE
|
|
# uninterpreted function (collision-resistance, marked [VERIFY]) exactly where the
|
|
# binding argument rests on "a different pre-image gives a different commitment".
|
|
# This checks the DESIGN-level guard logic, NOT the compiled EVM bytecode.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Function, IntSort, BoolSort, Solver, And, Or, Not,
|
|
Implies, Distinct, ForAll, sat, unsat)
|
|
|
|
results = []
|
|
def check(name, s, expect_unsat=True, kind="PROOF"):
|
|
r = s.check()
|
|
if expect_unsat:
|
|
ok = (r == unsat); tag = "PROVED" if ok else "FAILED"
|
|
else:
|
|
ok = (r == sat); tag = "CEX-FOUND" if ok else "FAILED"
|
|
results.append((name, tag, ok, kind))
|
|
print(f"[{tag:9}] ({kind}) {name}: z3={r} (expected {'unsat' if expect_unsat else 'sat'})")
|
|
if r == sat:
|
|
m = s.model()
|
|
print(" witness:", {str(d): m[d] for d in m.decls()})
|
|
return ok
|
|
|
|
def required_quorum(n):
|
|
# _quorumThreshold(n) = (2*n + 2) / 3, Solidity floor division for n >= 0.
|
|
return (2 * n + 2) / 3
|
|
|
|
def add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain,
|
|
pvQuorum, pvBlockHash,
|
|
g_quorum=True, g_root=True, g_domain=True):
|
|
"""Assert verifyCertificate()'s fail-closed guards. Flags let a NEG-CTRL drop one."""
|
|
s.add(n >= 1) # G0 EmptyValidatorSet
|
|
if g_root:
|
|
s.add(pvRoot == regRoot) # G1
|
|
s.add(pvSize == n) # G2
|
|
if g_domain:
|
|
s.add(pvDomain == expDomain) # G3
|
|
if g_quorum:
|
|
s.add(pvQuorum >= required_quorum(n)) # G4
|
|
s.add(pvBlockHash != 0) # G5
|
|
|
|
print("### AereFinalityCertificateVerifier -- FAIL-CLOSED certificate acceptance\n")
|
|
|
|
# ---- Q0 The threshold formula IS ceil(2N/3): required=(2N+2)/3 satisfies the
|
|
# ceiling characterization 3*required >= 2N AND 3*(required-1) < 2N, for all
|
|
# N >= 1. Negation UNSAT => the on-chain quorum is exactly ceil(2N/3). --------
|
|
s = Solver()
|
|
n = Int('n')
|
|
req = required_quorum(n)
|
|
s.add(n >= 1)
|
|
s.add(Not(And(3 * req >= 2 * n, 3 * (req - 1) < 2 * n))) # NEGATION of the ceil law
|
|
check("Q0 quorum threshold (2N+2)/3 == ceil(2N/3) for all N>=1", s)
|
|
|
|
# ---- Q0b Concrete anchor values: N=7 -> 5, N=9 -> 6, N=4 -> 3 (matches doc). The
|
|
# Solidity floor division (2N+2)/3 is asserted equal to the doc's quorum for each
|
|
# anchor N; the negation (any anchor wrong) is UNSAT. -----------------------
|
|
s = Solver()
|
|
bad = Bool('bad')
|
|
s.add(bad == Or((2*4+2)//3 != 3, (2*5+2)//3 != 4, (2*7+2)//3 != 5, (2*9+2)//3 != 6))
|
|
s.add(bad)
|
|
check("Q0b concrete quorum anchors N in {4,5,7,9} -> {3,4,5,6}", s)
|
|
|
|
# ---- P1 QUORUM: an accepted certificate has pvQuorum >= ceil(2N/3). Negation:
|
|
# all guards hold yet pvQuorum < required. UNSAT under G4. -------------------
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(pvQuorum < required_quorum(n)) # NEGATION: sub-quorum accepted
|
|
check("P1 accepted certificate meets the ceil(2N/3) quorum (no sub-quorum accept)", s)
|
|
|
|
# ---- P1b Concrete N=7: a 4-of-7 certificate (below the 5 quorum) is rejected. ---
|
|
s = Solver()
|
|
pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
s.add(pvSize == 7, pvRoot == regRoot, pvDomain == expDomain, pvBlockHash != 0)
|
|
s.add(pvQuorum >= (2*7+2)//3) # G4 with N=7 => >= 5
|
|
s.add(pvQuorum == 4) # NEGATION: a 4-of-7 cert
|
|
check("P1b N=7: a 4-of-7 (sub-quorum) certificate cannot be accepted", s)
|
|
|
|
# ---- P2 ROOT BINDING: an accepted certificate's validatorSetRoot equals the LIVE
|
|
# registry root. Negation: accepted yet pvRoot != registeredRoot. UNSAT (G1). -
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(pvRoot != regRoot) # NEGATION: stale / forged root accepted
|
|
check("P2 accepted certificate is bound to the live registry validatorSetRoot", s)
|
|
|
|
# ---- P2b SIZE BINDING: pvSize == N. Negation UNSAT (G2). ---------------------
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(pvSize != n) # NEGATION
|
|
check("P2b accepted certificate's validatorSetSize equals the registry N", s)
|
|
|
|
# ---- P3 DOMAIN BINDING (anti cross-context replay): attestationDomain is
|
|
# keccak(DOMAIN_PREFIX, chainId, registry), modelled as an INJECTIVE function
|
|
# D(chainId, registry). A certificate produced for a DIFFERENT chain or
|
|
# registry has pvDomain = D(chainId2, registry2) with (chainId2,registry2) !=
|
|
# (chainId,registry), so by injectivity pvDomain != expDomain and G3 rejects.
|
|
# Negation: such a cross-context certificate is accepted. UNSAT. ------------
|
|
D = Function('D', IntSort(), IntSort(), IntSort()) # keccak(prefix, chainId, registry)
|
|
s = Solver()
|
|
chainId, registry = Int('chainId'), Int('registry')
|
|
chainId2, registry2 = Int('chainId2'), Int('registry2')
|
|
# collision-resistance / injectivity of the domain hash [VERIFY: keccak256]:
|
|
s.add(ForAll([chainId, registry, chainId2, registry2],
|
|
Implies(D(chainId, registry) == D(chainId2, registry2),
|
|
And(chainId == chainId2, registry == registry2))))
|
|
cid, reg = Int('cid'), Int('reg')
|
|
cid2, reg2 = Int('cid2'), Int('reg2')
|
|
expDomain = D(cid, reg) # this verifier's bound domain
|
|
pvDomain = D(cid2, reg2) # domain baked into the foreign cert
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(Or(cid2 != cid, reg2 != reg)) # a DIFFERENT chain or registry
|
|
check("P3 a certificate from another chain/registry is rejected (domain binding)", s)
|
|
|
|
# ---- P3b DOMAIN BINDING, direct form: accepted yet pvDomain != expected. UNSAT.
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(pvDomain != expDomain) # NEGATION
|
|
check("P3b accepted certificate's attestationDomain equals the bound domain", s)
|
|
|
|
# ---- P4 KEY ROTATION invalidates an old-root certificate. The registry root
|
|
# commits to each validator's (address, keyEpoch, keyHash); a rotation bumps
|
|
# the epoch and changes the key hash, so the recomputed root changes. Model the
|
|
# root as an INJECTIVE function R(epochVec) [VERIFY: keccak256]. After a rotation
|
|
# the live root is newRoot = R(afterEpochs) != R(beforeEpochs) = oldRoot. A
|
|
# certificate carrying pvRoot == oldRoot then fails the (now-newRoot) G1 binding.
|
|
# Negation: an old-root certificate is still accepted after the rotation. UNSAT.
|
|
R = Function('R', IntSort(), IntSort()) # root as a function of the epoch commitment
|
|
s = Solver()
|
|
beforeEpochs, afterEpochs = Int('beforeEpochs'), Int('afterEpochs')
|
|
s.add(ForAll([beforeEpochs, afterEpochs],
|
|
Implies(R(beforeEpochs) == R(afterEpochs), beforeEpochs == afterEpochs)))
|
|
be, ae = Int('be'), Int('ae')
|
|
s.add(be != ae) # rotation changed the epoch commitment
|
|
oldRoot = R(be) # root the old cert was proven against
|
|
newRoot = R(ae) # live root after rotation
|
|
n = Int('n'); pvSize = Int('pvSize')
|
|
pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
# The live registry now returns newRoot; the old certificate carries pvRoot = oldRoot.
|
|
add_guards(s, n, oldRoot, newRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
check("P4 a key rotation (root changes) makes an old-root certificate unaccept-able", s)
|
|
|
|
# ---- P5 EMPTY SET fail-closed: with n == 0 no certificate is accepted (G0). ----
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
# reuse the guards but force the empty set; G0 (n>=1) then contradicts n==0.
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash)
|
|
s.add(n == 0) # NEGATION of the non-empty guard
|
|
check("P5 empty validator set is rejected (EmptyValidatorSet, fail-closed)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1 (drop the quorum guard G4): without pvQuorum >= ceil(2N/3), a
|
|
# sub-quorum certificate (e.g. 1 attestation of 7) is accepted. z3 finds it. --
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash,
|
|
g_quorum=False) # DROP G4
|
|
s.add(n == 7, pvQuorum == 1) # a 1-of-7 certificate
|
|
check("no-quorum-check verifier CAN accept a sub-quorum certificate", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2 (drop the root binding G1): without pvRoot == registeredRoot, a
|
|
# certificate proven against a STALE or FORGED validator set is accepted. -----
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash,
|
|
g_root=False) # DROP G1
|
|
s.add(pvRoot != regRoot) # forged / stale root accepted
|
|
check("no-root-binding verifier CAN accept a stale/forged validator-set root", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 3 (drop the domain binding G3): without pvDomain == attestationDomain,
|
|
# a certificate from a DIFFERENT chain or registry replays here. z3 finds it. --
|
|
s = Solver()
|
|
n = Int('n'); pvRoot, regRoot = Int('pvRoot'), Int('regRoot')
|
|
pvSize = Int('pvSize'); pvDomain, expDomain = Int('pvDomain'), Int('expDomain')
|
|
pvQuorum, pvBlockHash = Int('pvQuorum'), Int('pvBlockHash')
|
|
add_guards(s, n, pvRoot, regRoot, pvSize, pvDomain, expDomain, pvQuorum, pvBlockHash,
|
|
g_domain=False) # DROP G3
|
|
s.add(pvDomain != expDomain) # cross-context certificate replays
|
|
check("no-domain-binding verifier CAN accept a cross-chain/registry certificate", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ------------------------------------------------------------------------------
|
|
print("\n=== SUMMARY ===")
|
|
allok = True
|
|
for name, tag, ok, kind in results:
|
|
print(f" {tag:9} [{kind}] {name}")
|
|
allok = allok and ok
|
|
print()
|
|
if allok:
|
|
print("AereFinalityCertificateVerifier acceptance safety:")
|
|
print(" PROVED -- the on-chain quorum threshold is EXACTLY ceil(2N/3) (Q0/Q0b), and an")
|
|
print(" accepted certificate necessarily meets that quorum (P1/P1b), is bound to the live")
|
|
print(" registry root and size (P2/P2b), is bound to the chainId+registry attestation domain")
|
|
print(" so cross-context replay is rejected (P3/P3b), stops matching once a key rotation")
|
|
print(" changes the root (P4), and is rejected on an empty validator set (P5). Three NEG-CTRLs")
|
|
print(" fire: dropping the quorum, the root binding, or the domain binding each opens a real")
|
|
print(" bypass (sub-quorum accept / forged-root accept / cross-chain replay).")
|
|
print(" [VERIFY] SP1 GATEWAY SOUNDNESS: acceptance also requires SP1_GATEWAY.verifyProof to")
|
|
print(" succeed against the pinned PROGRAM_VKEY; verifyProof reverting on an invalid proof is a")
|
|
print(" trusted primitive, not re-proved here. The OFF-CHAIN zkVM aggregation circuit (that N")
|
|
print(" distinct hash-based attestations over the domain-bound block exist under the root) is")
|
|
print(" [MEASURE], NOT implemented, proven only against a MOCK gateway in the contract tests.")
|
|
print(" keccak256 injectivity (root / domain collision-resistance) is [VERIFY], modelled here.")
|
|
print(" DESIGN: additive PQ finality, Aere consensus stays classical ECDSA QBFT; this checks")
|
|
print(" the guard logic, not the compiled EVM bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|