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.
205 lines
12 KiB
Python
205 lines
12 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# vectorstore_smt.py
|
|
#
|
|
# SMT proof (z3) of the VERSION-MONOTONICITY + APPEND-ONLY + committed-version and
|
|
# one-shot-receipt state invariants of AereVectorStore, verifiable semantic memory
|
|
# for AI agents. Plus load-bearing NEGATIVE CONTROLS for the attest version-bound,
|
|
# the append-only history, and the one-shot paid-query receipt.
|
|
#
|
|
# Contract: contracts/contracts/agentic/AereVectorStore.sol
|
|
#
|
|
# A store owner appends VERSIONED commitment roots; a retrieval provider attests
|
|
# "for this query against committed version V, resultRoot", backed on a priced store
|
|
# by a one-shot AERE402 payment receipt. The safety-critical state invariants:
|
|
# VM. VERSION MONOTONICITY. commit() sets version = s.version + 1 and s.version =
|
|
# version, so a store's version strictly increases by exactly one per commit;
|
|
# commitCount is likewise monotone.
|
|
# AO. APPEND-ONLY HISTORY. _versions[storeId] is push-only; a committed version
|
|
# entry is never rewritten or deleted (no admin, no owner override, no upgrade).
|
|
# CV. RETRIEVAL AGAINST A COMMITTED VERSION. attestRetrieval reverts unless
|
|
# 1 <= version <= s.version (UnknownVersion), so an attestation always references
|
|
# a real committed store state.
|
|
# R1. ONE-SHOT RECEIPT. On a priced store the payment receipt is consumed at most
|
|
# once (r.consumed guard, then r.consumed = true) and only by its bound provider
|
|
# (r.provider == msg.sender, the L2 fix), so a paid retrieval cannot be double-
|
|
# spent or front-run.
|
|
#
|
|
# Method: model version updates and the append relation as first-order constraints
|
|
# and prove each property by asserting its NEGATION under the real guards (UNSAT).
|
|
# The append-only history uses the standard "writes only push" relation over an
|
|
# uninterpreted index->value function (as in recovery_registry_smt / credential_
|
|
# registry_smt). Each NEG-CTRL removes exactly one guard and shows the attack becomes
|
|
# SAT. This checks the DESIGN-level state logic, NOT the compiled EVM bytecode.
|
|
#
|
|
# ASSUMPTIONS (bound every PROVED below):
|
|
# A1. Post-quantum store commit AUTHENTICITY is the Falcon-512 precompile (0x0AE1)
|
|
# verifying commitChallenge; that fail-closed PQC auth is a precompile-return
|
|
# property [VERIFY], a trusted primitive here, not re-proved (see spokepool /
|
|
# cryptoregistry models for the precompile-return checks).
|
|
# A2. paidQuery settles on the LIVE AERE402 facilitator and forwards the delta-
|
|
# measured receipt; that fund-flow is external and trusted here. This model
|
|
# covers the receipt STATE machine (one-shot + provider-bound), not the rail.
|
|
# A3. Merkle inclusion (verifyVectorInclusion / verifyResultInclusion) rests on
|
|
# keccak256 / OpenZeppelin MerkleProof soundness [VERIFY], not modelled.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import (Int, Bool, Function, IntSort, Solver, And, Or, Not, Implies,
|
|
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
|
|
|
|
print("### AereVectorStore -- VERSION MONOTONICITY + APPEND-ONLY + one-shot receipt\n")
|
|
|
|
# ---- VM VERSION strictly increases by exactly one per commit. commit() computes
|
|
# version = pre + 1 and sets s.version = version. Negation: post != pre + 1. UNSAT.
|
|
s = Solver()
|
|
pre, post = Int('pre'), Int('post')
|
|
s.add(pre >= 0)
|
|
s.add(post == pre + 1) # commit(): version = s.version + 1
|
|
s.add(post != pre + 1) # NEGATION (paired with the update)
|
|
check("VM commit increments version by exactly one (version = s.version + 1)", s)
|
|
|
|
# ---- VM2 VERSION strictly increases (monotone). Negation: post <= pre. UNSAT. -----
|
|
s = Solver()
|
|
pre, post = Int('pre'), Int('post')
|
|
s.add(pre >= 0, post == pre + 1)
|
|
s.add(Not(post > pre)) # NEGATION: version did not strictly increase
|
|
check("VM2 the store version strictly increases on every commit", s)
|
|
|
|
# ---- VM3 commitCount is monotone (a global commit counter that never decreases). --
|
|
s = Solver()
|
|
cpre, cpost = Int('cpre'), Int('cpost')
|
|
s.add(cpre >= 0, cpost == cpre + 1)
|
|
s.add(Not(cpost > cpre)) # NEGATION
|
|
check("VM3 the global commitCount strictly increases on every commit", s)
|
|
|
|
# ---- AO APPEND-ONLY version history: a committed version entry is never rewritten.
|
|
# Model the history as index->value with the append relation: a commit only
|
|
# pushes at index == len (0-based; version number = index + 1), leaving every
|
|
# existing index untouched. Negation: an already-committed index changes. UNSAT.
|
|
vB = Function('vB', IntSort(), IntSort()) # version array BEFORE the commit
|
|
vA = Function('vA', IntSort(), IntSort()) # version array AFTER the commit
|
|
s = Solver()
|
|
L = Int('L'); newRoot = Int('newRoot'); i = Int('i')
|
|
s.add(L >= 0)
|
|
s.add(ForAll([i], Implies(And(i >= 0, i < L), vA(i) == vB(i)))) # existing entries preserved
|
|
s.add(vA(L) == newRoot) # the new version only at index L (== old count)
|
|
j = Int('j')
|
|
s.add(j >= 0, j < L, vA(j) != vB(j)) # NEGATION: a committed version mutated
|
|
check("AO the version history is append-only (a committed root cannot be rewritten)", s)
|
|
|
|
# ---- CV RETRIEVAL AGAINST A COMMITTED VERSION: attestRetrieval requires
|
|
# 1 <= version <= s.version. Negation: an attestation is accepted with version == 0
|
|
# OR version > current. UNSAT (UnknownVersion guard, fail-closed).
|
|
s = Solver()
|
|
version, current = Int('version'), Int('current')
|
|
attest_ok = And(version >= 1, version <= current) # the UnknownVersion guard (else revert)
|
|
s.add(current >= 0)
|
|
s.add(attest_ok)
|
|
s.add(Or(version == 0, version > current)) # NEGATION: references an uncommitted version
|
|
check("CV an attestation always names a committed version (1 <= version <= current)", s)
|
|
|
|
# ---- CV2 the same version bound protects verifyVectorInclusion (a proof is only ever
|
|
# checked against a committed root). Negation: inclusion checked at an out-of-range
|
|
# version. UNSAT.
|
|
s = Solver()
|
|
version, current = Int('version'), Int('current')
|
|
s.add(current >= 0, version >= 1, version <= current) # the guard in verifyVectorInclusion
|
|
s.add(Or(version == 0, version > current)) # NEGATION
|
|
check("CV2 vector-inclusion is only checked against a committed version", s)
|
|
|
|
# ---- R1 ONE-SHOT RECEIPT: a priced retrieval consumes the receipt at most once. The
|
|
# guard requires consumed == false and sets consumed = true; a second consume needs
|
|
# consumed == false again -> infeasible. Model the flag before/after. UNSAT.
|
|
s = Solver()
|
|
consumedPre, consumedPost = Bool('consumedPre'), Bool('consumedPost')
|
|
# first consume: guard requires not consumedPre, effect consumedPost = true
|
|
s.add(Not(consumedPre), consumedPost == True)
|
|
# a SECOND consume would again require the (now true) flag to be false:
|
|
s.add(consumedPost == False) # NEGATION: receipt consumed twice
|
|
check("R1 a paid-query receipt is consumed at most once (ReceiptConsumed guard)", s)
|
|
|
|
# ---- R2 RECEIPT PROVIDER BINDING (L2 fix): only the bound provider may consume a
|
|
# receipt. Negation: a consume by a caller who is not the receipt's provider. UNSAT.
|
|
s = Solver()
|
|
provider, caller = Int('provider'), Int('caller')
|
|
consume_ok = (caller == provider) # the NotReceiptProvider guard (else revert)
|
|
s.add(consume_ok)
|
|
s.add(caller != provider) # NEGATION: a third party consumes the receipt
|
|
check("R2 only the bound provider may consume a paid receipt (L2 front-run guard)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1 (drop the version bound): a BUGGY attestRetrieval without the
|
|
# `1 <= version <= current` guard records an attestation against a version that
|
|
# was never committed. z3 finds the out-of-range attestation. -------------------
|
|
s = Solver()
|
|
version, current = Int('version'), Int('current')
|
|
s.add(current >= 0)
|
|
# BUG: no version-bound check; any version is accepted.
|
|
s.add(version > current) # references a store state never committed
|
|
check("no-version-bound store CAN attest a retrieval against an uncommitted version", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2 (drop append-only): a BUGGY mutable version array that overwrites an
|
|
# EXISTING version index. A committed root is silently rewritten. ---------------
|
|
s = Solver()
|
|
L = Int('L'); j = Int('j'); newRoot = Int('newRoot')
|
|
s.add(L >= 1, j >= 0, j < L)
|
|
# BUG: the write targets an existing index j (overwrite), so vA(j) != vB(j) is allowed.
|
|
s.add(vA(j) == newRoot, vB(j) != newRoot) # committed version rewritten
|
|
check("mutable-history store CAN silently overwrite a committed version root", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 3 (drop the one-shot guard): a BUGGY attestRetrieval that does NOT
|
|
# require consumed == false lets one paid receipt back two retrievals (double
|
|
# spend of a single payment). z3 finds the second consume of an already-used receipt.
|
|
s = Solver()
|
|
consumedPre, consumedPost = Bool('consumedPre'), Bool('consumedPost')
|
|
# BUG: the ReceiptConsumed guard is removed; a consume proceeds even if already consumed.
|
|
s.add(consumedPre == True) # the receipt is ALREADY consumed
|
|
s.add(consumedPost == True) # ...yet a second consume still proceeds
|
|
check("no-one-shot store CAN consume one paid receipt twice (double-spend a payment)", 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("AereVectorStore memory-provenance safety:")
|
|
print(" PROVED -- a commit increments the store version by exactly one and strictly increases")
|
|
print(" it (VM/VM2), the global commitCount is monotone (VM3), the version history is append-")
|
|
print(" only so a committed root can never be rewritten (AO), every retrieval attestation and")
|
|
print(" inclusion check names a committed version 1..current (CV/CV2), and a priced receipt is")
|
|
print(" consumed at most once (R1) and only by its bound provider (R2, the L2 fix). Three NEG-")
|
|
print(" CTRLs fire: dropping the version bound attests against an uncommitted version, a mutable")
|
|
print(" history overwrites a committed root, and dropping the one-shot guard double-spends one")
|
|
print(" paid receipt.")
|
|
print(" [VERIFY] FALCON-512 PRECOMPILE (0x0AE1): a post-quantum store's commit AUTHENTICITY is")
|
|
print(" the live precompile verifying commitChallenge (fail-closed); that precompile-return")
|
|
print(" soundness is a trusted primitive, not re-proved here. The AERE402 facilitator settlement")
|
|
print(" in paidQuery is an external trusted rail; this model covers the receipt STATE machine,")
|
|
print(" not the token movement. Merkle inclusion rests on keccak256 / OZ MerkleProof soundness")
|
|
print(" [VERIFY]. R2 provider-binding is also covered by the Hardhat L2 test; the z3 adds the")
|
|
print(" at-most-once state invariant. DESIGN-level state 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)
|