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.
257 lines
15 KiB
Python
257 lines
15 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# ap2_mandate_smt.py
|
|
#
|
|
# SMT proof (z3) of the SPEND-AUTHORIZATION invariant of AereAP2MandateVerifier,
|
|
# the post-quantum x402 / AP2 payment-mandate verifier. A mandate is a standing
|
|
# authorization "agent may spend up to maxAmount of token over [periodStart,
|
|
# periodEnd] for purpose Q"; authorizeSpend records a draw against the mandate's
|
|
# cumulative cap. Plus load-bearing NEGATIVE CONTROLS for the cap check, the
|
|
# expiry check, and the post-fix L3 executor gate.
|
|
#
|
|
# Contract: contracts/contracts/erc8004/AereAP2MandateVerifier.sol
|
|
#
|
|
# spentUnder[mh] is the cumulative amount already authorized under mandate hash mh.
|
|
# authorizeSpend(m, amount, sig) fail-closes on each of these guards (else revert,
|
|
# no state change):
|
|
# E0 executor gate (L3 fix): SETTLEMENT_EXECUTOR != 0 => msg.sender == executor
|
|
# (NotSettlementExecutor)
|
|
# E1 amount != 0 (ZeroAmount)
|
|
# E2 window well-formed: periodEnd >= periodStart (InvalidMandateWindow)
|
|
# E3 not-yet-valid: now >= periodStart (MandateNotYetValid)
|
|
# E4 expired: now <= periodEnd (MandateExpired)
|
|
# E5 key ACTIVE + Falcon-512 (AgentKeyNotActiveFalcon)
|
|
# E6 signature verifies on-chain via 0x0AE1 (MandateSignatureInvalid)
|
|
# E7 cap (overflow-safe): next = already + amount; next >= already AND
|
|
# next <= maxAmount (MandateCapExceeded)
|
|
# then spentUnder[mh] = next.
|
|
#
|
|
# CAP-SOLVENCY INVARIANT (the task target):
|
|
# INV(mh) := 0 <= spentUnder[mh] <= maxAmount
|
|
#
|
|
# INV means the total authorized spend under a mandate NEVER exceeds its cap over
|
|
# the whole window, no matter how many times authorizeSpend is called; an expired
|
|
# (or not-yet-valid) mandate authorizes NOTHING; and once SETTLEMENT_EXECUTOR is
|
|
# configured (production, per the L3 fix) only that executor can consume the cap,
|
|
# so the open replay path is closed.
|
|
#
|
|
# Method: for each op, check INV(pre) AND guards AND post = op(pre) AND NOT INV(post)
|
|
# is UNSAT. UNSAT => the op cannot break the invariant. Amounts / times are unbounded
|
|
# Ints (the accounting/design abstraction, matching solc SMTChecker's default int
|
|
# model); the uint256 checked-add overflow guard E7 (next >= already) is stated as a
|
|
# guard but is belt-and-suspenders under unbounded positive amounts. This checks the
|
|
# DESIGN math, NOT the compiled EVM bytecode.
|
|
#
|
|
# ASSUMPTIONS (bound every PROVED below):
|
|
# A1. Falcon-512 signature validity (E6) is produced by the LIVE native precompile
|
|
# at 0x0AE1 through AerePQCKeyRegistry.verifyWithKey; its soundness (EUF-CMA of
|
|
# Falcon-512, correct precompile parsing, empty-return-is-invalid on a pre-fork
|
|
# node) is a trusted primitive [VERIFY], modelled as the sigValid predicate,
|
|
# not re-proved here.
|
|
# A2. mandateHash binds MANDATE_DOMAIN + chainId + this contract + the mandate
|
|
# fields, so a signed mandate cannot be replayed against another verifier or
|
|
# chain; keccak256 injectivity is [VERIFY], modelled as equality of the hash.
|
|
# A3. This contract holds NO funds: the cap is accounting, the AERE402 rail moves
|
|
# value. The vector the L3 gate closes is cap-exhaustion griefing, not theft.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import Int, Bool, Solver, And, Or, Not, Implies, sat, unsat
|
|
|
|
def INV(spent, cap):
|
|
return And(spent >= 0, spent <= cap)
|
|
|
|
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 enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap):
|
|
"""authorizeSpend's fail-closed guards E0..E7 (the enforced path). A write happens
|
|
iff all hold."""
|
|
return And(
|
|
Or(executor == 0, sender == executor), # E0 executor gate (L3 fix)
|
|
amount >= 1, # E1 ZeroAmount
|
|
pEnd >= pStart, # E2 InvalidMandateWindow
|
|
now >= pStart, # E3 MandateNotYetValid
|
|
now <= pEnd, # E4 MandateExpired
|
|
keyActive, falcon, # E5 AgentKeyNotActiveFalcon
|
|
sigValid, # E6 MandateSignatureInvalid
|
|
nxt == already + amt, amt == amount, # record: next = already + amount
|
|
nxt >= already, nxt <= cap, # E7 MandateCapExceeded (overflow-safe cap)
|
|
)
|
|
|
|
print("### AereAP2MandateVerifier -- SPEND AUTHORIZATION INV(mh): 0 <= spentUnder <= maxAmount\n")
|
|
|
|
# ---- BASE CASE: a fresh mandate has authorized nothing -----------------------
|
|
s = Solver(); cap = Int('cap'); s.add(cap >= 0, Not(INV(0, cap)))
|
|
check("base case (fresh mandate: spentUnder == 0) satisfies INV", s)
|
|
|
|
# ---- CAP preserved by one authorizeSpend (inductive step) --------------------
|
|
# INV(pre) AND all guards AND spent_post = next => INV(post). Negation UNSAT.
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(INV(already, cap))
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(Not(INV(nxt, cap))) # NEGATION: post-state breaks the cap
|
|
check("authorizeSpend preserves INV (cumulative spend stays within cap)", s)
|
|
|
|
# ---- WINDOWED CUMULATIVE never exceeds the cap: two sequential draws ----------
|
|
# spent0 = 0; draw a1 (cap-checked) -> s1; draw a2 (cap-checked) -> s2. The per-op
|
|
# cap guard forces s2 <= cap, so no pair of authorized draws can exceed the cap.
|
|
s = Solver()
|
|
a1, a2, s1, s2, cap = Int('a1'), Int('a2'), Int('s1'), Int('s2'), Int('cap')
|
|
s.add(cap >= 0, a1 >= 1, a2 >= 1)
|
|
s.add(s1 == 0 + a1, s1 <= cap) # draw 1 with its cap guard
|
|
s.add(s2 == s1 + a2, s2 <= cap) # draw 2 with its cap guard
|
|
s.add(s2 > cap) # NEGATION: cumulative exceeds cap
|
|
check("windowed cumulative: two guarded draws can never exceed the cap", s)
|
|
|
|
# ---- MONOTONE spend: authorizeSpend never REDUCES the recorded cumulative -----
|
|
# next = already + amount with amount >= 1, so spend strictly increases; there is no
|
|
# refund / decrement path, so a replay can never free previously-consumed cap.
|
|
s = Solver()
|
|
already, amount, nxt = Int('already'), Int('amount'), Int('nxt')
|
|
s.add(already >= 0, amount >= 1, nxt == already + amount)
|
|
s.add(Not(nxt > already)) # NEGATION: cumulative did not increase
|
|
check("authorizeSpend is monotone (consumed cap is never reduced / refunded)", s)
|
|
|
|
# ---- EXPIRED mandate authorizes NOTHING: a write requires now <= periodEnd -----
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(now > pEnd) # NEGATION: mandate is EXPIRED yet authorized
|
|
check("an expired mandate authorizes nothing (write requires now <= periodEnd)", s)
|
|
|
|
# ---- NOT-YET-VALID mandate authorizes NOTHING: a write requires now >= periodStart
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(now < pStart) # NEGATION: before the window yet authorized
|
|
check("a not-yet-valid mandate authorizes nothing (write requires now >= periodStart)", s)
|
|
|
|
# ---- WINDOW well-formed: an accepted mandate always has periodEnd >= periodStart -
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(pEnd < pStart) # NEGATION: inverted window yet authorized
|
|
check("an accepted authorization has a well-formed window (periodEnd >= periodStart)", s)
|
|
|
|
# ---- L3 EXECUTOR GATE (post-fix): when configured, only the executor consumes cap
|
|
# executor != 0 AND write => sender == executor. Negation UNSAT: the gate blocks a
|
|
# non-executor from the accounting path in production.
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(executor != 0) # SETTLEMENT_EXECUTOR configured (production)
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(sender != executor) # NEGATION: a non-executor consumed the cap
|
|
check("L3 executor gate: with SETTLEMENT_EXECUTOR set, only it can consume the cap", s)
|
|
|
|
# ---- ZERO-AMOUNT rejected: an accepted authorization always draws amount >= 1 -----
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
keyActive, falcon, sigValid = Bool('keyActive'), Bool('falcon'), Bool('sigValid')
|
|
already, amt, nxt, cap = Int('already'), Int('amt'), Int('nxt'), Int('cap')
|
|
s.add(enforced_guards(executor, sender, amount, pStart, pEnd, now, keyActive, falcon, sigValid,
|
|
already, amt, nxt, cap))
|
|
s.add(amount <= 0) # NEGATION: a zero/negative draw was authorized
|
|
check("a zero-amount draw is rejected (ZeroAmount guard)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1 (drop the cap check): a BUGGY authorizeSpend that records
|
|
# next = already + amount WITHOUT the `next <= maxAmount` guard lets the
|
|
# cumulative spend exceed the mandate cap. z3 finds the over-cap draw. -------
|
|
s = Solver()
|
|
already, amount, nxt, cap = Int('already'), Int('amount'), Int('nxt'), Int('cap')
|
|
s.add(INV(already, cap), amount >= 1, nxt == already + amount) # BUG: no `nxt <= cap` guard
|
|
s.add(nxt > cap) # cumulative now exceeds the cap
|
|
check("no-cap-check verifier CAN authorize spend beyond the mandate cap", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2 (drop the expiry check): a BUGGY path without `now <= periodEnd`
|
|
# authorizes a spend on an EXPIRED mandate. z3 finds the expired authorization.
|
|
s = Solver()
|
|
amount, pStart, pEnd, now = Int('amount'), Int('pStart'), Int('pEnd'), Int('now')
|
|
# BUG: window guard drops E4; only not-yet-valid + well-formed remain.
|
|
buggy_ok = And(amount >= 1, pEnd >= pStart, now >= pStart)
|
|
s.add(buggy_ok)
|
|
s.add(pEnd >= 0, now > pEnd) # the mandate is EXPIRED
|
|
check("no-expiry-check verifier CAN authorize spend on an expired mandate", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 3 (drop the L3 executor gate): a BUGGY open path (no executor gate)
|
|
# lets ANY address that observes the public standing signature consume a
|
|
# configured mandate's cap without being the settlement executor (the exact
|
|
# cap-exhaustion vector the L3 fix's gate closes). ------------------------------
|
|
s = Solver()
|
|
executor, sender = Int('executor'), Int('sender')
|
|
s.add(executor != 0) # a real executor IS configured
|
|
# BUG: the E0 gate is removed, so a caller that is not the executor still reaches the write.
|
|
buggy_write_reached = True
|
|
s.add(buggy_write_reached, sender != executor) # a non-executor consumes the cap
|
|
check("no-executor-gate verifier CAN let a non-executor consume a configured mandate", 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("AereAP2MandateVerifier spend-authorization safety:")
|
|
print(" PROVED -- the cumulative spend under a mandate stays within its cap inductively (base")
|
|
print(" case + every authorizeSpend preserves 0 <= spentUnder <= maxAmount), two sequential")
|
|
print(" guarded draws can never exceed the cap (windowed cumulative), the recorded cumulative")
|
|
print(" is monotone (consumed cap is never refunded), an expired or not-yet-valid mandate")
|
|
print(" authorizes nothing, an accepted authorization has a well-formed window and a non-zero")
|
|
print(" amount, and (post-fix L3) with SETTLEMENT_EXECUTOR configured only that executor can")
|
|
print(" consume the cap. Three NEG-CTRLs fire: dropping the cap check authorizes over-cap,")
|
|
print(" dropping the expiry check authorizes an expired mandate, and dropping the executor gate")
|
|
print(" lets a non-executor drain a configured mandate's cap.")
|
|
print(" [VERIFY] FALCON-512 PRECOMPILE (0x0AE1): the mandate-signature validity bit (E6) is")
|
|
print(" produced by the live native precompile through AerePQCKeyRegistry.verifyWithKey; its")
|
|
print(" soundness (EUF-CMA of Falcon-512, correct precompile parsing) is a trusted primitive,")
|
|
print(" modelled as the sigValid predicate, not re-proved. mandateHash chain/contract binding")
|
|
print(" and keccak256 injectivity are [VERIFY], modelled as hash equality.")
|
|
print(" DESIGN: application-layer payment authorization, holds NO funds (the cap is accounting,")
|
|
print(" the AERE402 rail moves value); consensus stays classical ECDSA QBFT. The open path")
|
|
print(" (SETTLEMENT_EXECUTOR == 0) is verification/test only per the contract's documented L3;")
|
|
print(" production MUST set the executor, which this model proves closes the vector. This checks")
|
|
print(" the guard logic under unbounded-Int arithmetic, not the compiled EVM bytecode.")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|