6cb0140fae
The public history carried kat/__pycache__/mlkem768_reference.cpython-314.pyc, a compiled Python artifact embedding the operator's absolute local path. Text secret scanners do not read compiled binaries, which is exactly how it slipped through, and removing it from the tip would have left it reachable through the old root commits. So this repository is republished from a single clean root. This root also carries, from the previously unpublished line of work: - corrected LICENSE year, LICENSING.md, VERIFY-POLICY.md, and CITATIONS-UNRESOLVED.md remeasured 2026-08-11 (101 paths, README aligned) - O-018: run_consensus_verification.py ran 19 of 29 models and reported PASS; it now runs all 29, and computemarket_smt.py gains resolveByTimeout / reclaimUnsettled cases plus a negative control - O-006: the word 'audited' removed from next to Bouncy Castle, twice, after a concurrent edit resurrected it - O-014: prior art named and dated - Algorand's native falcon_verify shipped about ten months before AERE's precompiles; the primacy claim is withdrawn where it was implied - bench/ scripts parametrized so they actually run for an outsider (the earlier textual sanitization left $STAGING unexpanded inside Python strings) - AIP-2/AIP-3 errata with measured figures, spec remeasurements at 2026-08-01, and the spec-zk-stack retractions (owner is an operational key, not the Foundation; 'maximally sound' withdrawn; aggregator V1 deprecated) The redacted bench-host environment files from the sanitized line are kept exactly as published; the unredacted local variants are not carried.
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)
|