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.
330 lines
18 KiB
Python
330 lines
18 KiB
Python
#!/usr/bin/env python3
|
|
# -----------------------------------------------------------------------------
|
|
# computemarket_smt.py
|
|
#
|
|
# SMT proof (z3) of the ESCROW-SOLVENCY invariant for AereComputeMarketV3, the
|
|
# proof-carrying DePIN compute marketplace. Plus a load-bearing NEGATIVE CONTROL
|
|
# for the per-asset accounting (fee-on-transfer under-funding) and one for the
|
|
# ZK_VERIFIED pay-only-on-proof gate.
|
|
#
|
|
# Contract: contracts/contracts/depin/AereComputeMarketV3.sol
|
|
#
|
|
# We model the per-asset accounting as an inductive transition system and prove
|
|
# the safety invariant is INDUCTIVE (base case + every fund-moving op preserves
|
|
# it). Each Solidity `require`/revert is a guard; Solidity 0.8 checked arithmetic
|
|
# is modelled as "underflow reverts (no state change)".
|
|
#
|
|
# Per asset T (T = address(0) is native AERE, else an allowlisted ERC-20):
|
|
# bal[T] = balance the contract actually holds in T
|
|
# (address(this).balance for native, balanceOf(this) for ERC-20)
|
|
# liab[T] = totalLiabilities[T] -- the sum of every OPEN job reward in T
|
|
# PLUS every posted provider/challenger bond in T
|
|
#
|
|
# Note the asset routing that the model must respect (from the contract):
|
|
# - a job reward is escrowed in its own `token` and added to liab[token];
|
|
# - EVERY bond (provider + challenger) is native AERE, added to liab[0].
|
|
# So native liabilities carry (native-token rewards) + (ALL bonds), while an
|
|
# ERC-20 asset carries only its own rewards. There is no cross-asset mixing:
|
|
# each reward is added to exactly one asset once, each bond to native once.
|
|
#
|
|
# ESCROW-SOLVENCY INVARIANT (the task target, contract's isSolvent()):
|
|
# INV(T) := bal[T] >= liab[T] AND liab[T] >= 0
|
|
#
|
|
# INV(T) for every asset => every open job's reward and every posted bond is
|
|
# always fully backed by the contract's balance in that asset, so every payout
|
|
# path (settle / cancel / reclaim / resolveDispute) can always pay out, and a
|
|
# permissionless observer can never drive the balance below what is owed.
|
|
#
|
|
# Method: for each op OP, check INV(pre) AND guards AND post=OP(pre) AND
|
|
# NOT INV(post) is UNSAT. UNSAT => OP cannot break the invariant.
|
|
# Unbounded Ints = the accounting/design abstraction (matches solc SMTChecker's
|
|
# default int model). This checks the DESIGN math, NOT the EVM bytecode.
|
|
#
|
|
# ASSUMPTIONS (bound every PROVED below):
|
|
# A1. Standard ERC20: safeTransferFrom credits exactly `amount`, safeTransfer
|
|
# debits exactly `amount`. postJob explicitly REJECTS fee-on-transfer /
|
|
# rebasing tokens (received != reward reverts BadReward), so this holds by
|
|
# construction for the escrow; the NEG-CTRL below shows why that check is
|
|
# load-bearing.
|
|
# A2. There is NO protocol fee and NO owner/sweep in this contract: a reward is
|
|
# escrowed in full and paid in full; the only actors that touch a job's
|
|
# escrow are the requester (cancel/reclaim), the provider (settle), the
|
|
# challenger (dispute) and the arbiter (resolveDispute, route-only). So each
|
|
# op's balance delta equals its liability delta on the same asset.
|
|
# A3. A job's reward/bond, once added to liab at post/claim/dispute, remains a
|
|
# summand of liab until its single terminal op removes it; the per-op guards
|
|
# (amt <= liab portions) are exactly the Solidity checked-sub guards, which
|
|
# hold because the item removed is itself a summand of liab.
|
|
# -----------------------------------------------------------------------------
|
|
from z3 import Int, Solver, And, Or, Not, If, sat, unsat
|
|
|
|
def INV(bal, liab):
|
|
return And(bal >= liab, liab >= 0)
|
|
|
|
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].as_long() for d in m.decls()})
|
|
return ok
|
|
|
|
print("### AereComputeMarketV3 -- ESCROW SOLVENCY INV(T): bal[T] >= totalLiabilities[T]\n")
|
|
|
|
# ---- BASE CASE: fresh contract, every asset empty ----------------------------
|
|
s = Solver(); s.add(Not(INV(0, 0)))
|
|
check("base case (empty contract) satisfies INV", s)
|
|
|
|
# ---- postJob NATIVE reward: msg.value == reward, liab[0] += reward ------------
|
|
# Native reward asset (T = 0). bal[0] += reward, liab[0] += reward.
|
|
s = Solver()
|
|
bal, liab, reward = Int('bal'), Int('liab'), Int('reward')
|
|
s.add(INV(bal, liab), reward >= 1)
|
|
s.add(Not(INV(bal + reward, liab + reward)))
|
|
check("postJob(native) preserves INV[native] (bal+=reward, liab+=reward)", s)
|
|
|
|
# ---- postJob ERC-20 reward: safeTransferFrom exactly `reward` (received==reward
|
|
# guard rejects fee-on-transfer), liab[token] += reward -------------------
|
|
s = Solver()
|
|
balE, liabE, reward, received = Int('balE'), Int('liabE'), Int('reward'), Int('received')
|
|
# received == reward is ENFORCED by postJob (else revert BadReward). Model that.
|
|
s.add(INV(balE, liabE), reward >= 1, received == reward)
|
|
s.add(Not(INV(balE + received, liabE + reward)))
|
|
check("postJob(ERC20) preserves INV[token] (received==reward guard)", s)
|
|
|
|
# ---- claimJob: provider posts native bond == requiredBond; liab[0] += bond ----
|
|
s = Solver()
|
|
bal, liab, bond = Int('bal'), Int('liab'), Int('bond')
|
|
s.add(INV(bal, liab), bond >= 0) # bond may be 0 for ZK jobs (no state change)
|
|
s.add(Not(INV(bal + bond, liab + bond)))
|
|
check("claimJob() preserves INV[native] (bond escrowed to native)", s)
|
|
|
|
# ---- cancelJob (Open->Refunded): liab[token]-=reward; payout reward ----------
|
|
s = Solver()
|
|
bal, liab, reward = Int('bal'), Int('liab'), Int('reward')
|
|
s.add(INV(bal, liab), reward >= 1, reward <= liab) # reward is a summand of liab
|
|
s.add(Not(INV(bal - reward, liab - reward)))
|
|
check("cancelJob() preserves INV (refund requester, uncommit reward)", s)
|
|
|
|
# ---- submitResult (REPLAY/OPTIMISTIC) and submitResult ... : NO fund/liab move
|
|
# submitResult only flips status + records resultHash. bal and liab unchanged.
|
|
s = Solver()
|
|
bal, liab = Int('bal'), Int('liab')
|
|
s.add(INV(bal, liab))
|
|
s.add(Not(INV(bal, liab))) # identity transition
|
|
check("submitResult() preserves INV (status-only, no fund move)", s)
|
|
|
|
# ---- settle (acceptResult / finalize / submitResultZK) : pay reward (token) and
|
|
# return provider bond (native). Two DISTINCT assets unless token==native.
|
|
# Case token != native: reward leg on asset E, bond leg on asset N, independent.
|
|
s = Solver()
|
|
balE, liabE, reward = Int('balE'), Int('liabE'), Int('reward')
|
|
s.add(INV(balE, liabE), reward >= 1, reward <= liabE)
|
|
s.add(Not(INV(balE - reward, liabE - reward)))
|
|
check("settle() reward leg preserves INV[token!=native]", s)
|
|
|
|
s = Solver()
|
|
balN, liabN, bond = Int('balN'), Int('liabN'), Int('bond')
|
|
s.add(INV(balN, liabN), bond >= 0, bond <= liabN)
|
|
s.add(Not(INV(balN - bond, liabN - bond)))
|
|
check("settle() bond-return leg preserves INV[native]", s)
|
|
|
|
# Case token == native: BOTH reward and bond come out of the native asset at once.
|
|
s = Solver()
|
|
balN, liabN, reward, bond = Int('balN'), Int('liabN'), Int('reward'), Int('bond')
|
|
s.add(INV(balN, liabN), reward >= 1, bond >= 0, reward + bond <= liabN)
|
|
s.add(Not(INV(balN - (reward + bond), liabN - (reward + bond))))
|
|
check("settle() combined leg preserves INV[native] when token==native", s)
|
|
|
|
# ---- reclaimExpired (Claimed->Refunded): reward->requester (asset token),
|
|
# provider bond slashed to requester (native). Same deltas as settle. -----
|
|
s = Solver()
|
|
balN, liabN, reward, bond = Int('balN'), Int('liabN'), Int('reward'), Int('bond')
|
|
s.add(INV(balN, liabN), reward >= 1, bond >= 0, reward + bond <= liabN)
|
|
s.add(Not(INV(balN - (reward + bond), liabN - (reward + bond))))
|
|
check("reclaimExpired() preserves INV (reward+bond leave together, native job)", s)
|
|
|
|
# ---- dispute (Submitted->Disputed): challenger posts native bond == providerBond
|
|
s = Solver()
|
|
balN, liabN, chBond = Int('balN'), Int('liabN'), Int('chBond')
|
|
s.add(INV(balN, liabN), chBond >= 1)
|
|
s.add(Not(INV(balN + chBond, liabN + chBond)))
|
|
check("dispute() preserves INV[native] (challenger bond escrowed)", s)
|
|
|
|
# ---- resolveDispute: BOTH branches remove reward (token) + pBond+chBond (native)
|
|
# providerWon: reward->provider, pBond->provider, chBond->provider.
|
|
# !providerWon: reward->requester, chBond->challenger, pBond->challenger.
|
|
# Net asset delta is identical in both branches: token -=reward, native -=(pBond+chBond).
|
|
s = Solver()
|
|
balE, liabE, reward = Int('balE'), Int('liabE'), Int('reward')
|
|
s.add(INV(balE, liabE), reward >= 1, reward <= liabE)
|
|
s.add(Not(INV(balE - reward, liabE - reward)))
|
|
check("resolveDispute() reward leg preserves INV[token] (both branches)", s)
|
|
|
|
s = Solver()
|
|
balN, liabN, pBond, chBond = Int('balN'), Int('liabN'), Int('pBond'), Int('chBond')
|
|
s.add(INV(balN, liabN), pBond >= 0, chBond >= 0, pBond + chBond <= liabN)
|
|
s.add(Not(INV(balN - (pBond + chBond), liabN - (pBond + chBond))))
|
|
check("resolveDispute() bond leg preserves INV[native] (pBond+chBond routed)", s)
|
|
|
|
# ---- resolveByTimeout (Disputed->Refunded): PERMISSIONLESS liveness backstop for an
|
|
# arbiter that never resolves. Neutral unwind: reward -> requester, pBond -> provider,
|
|
# chBond -> challenger. Same NET asset delta as resolveDispute (token -= reward,
|
|
# native -= pBond+chBond), so solvency is preserved by the same argument, and no
|
|
# party is enriched by the arbiter's absence.
|
|
s = Solver()
|
|
balE, liabE, reward = Int('balE'), Int('liabE'), Int('reward')
|
|
s.add(INV(balE, liabE), reward >= 1, reward <= liabE)
|
|
s.add(Not(INV(balE - reward, liabE - reward)))
|
|
check("resolveByTimeout() reward leg preserves INV[token] (neutral unwind)", s)
|
|
|
|
s = Solver()
|
|
balN, liabN, pBond, chBond = Int('balN'), Int('liabN'), Int('pBond'), Int('chBond')
|
|
s.add(INV(balN, liabN), pBond >= 0, chBond >= 0, pBond + chBond <= liabN)
|
|
s.add(Not(INV(balN - (pBond + chBond), liabN - (pBond + chBond))))
|
|
check("resolveByTimeout() bond leg preserves INV[native] (both bonds returned home)", s)
|
|
|
|
# ---- LIVENESS: a DISPUTED job always has an exit. Either the arbiter resolves, or
|
|
# after ARBITRATION_TIMEOUT any caller can unwind. Model the guard disjunction:
|
|
# there is NO reachable time at which both exits are blocked.
|
|
s = Solver()
|
|
now, disputedAt, TIMEOUT = Int('now'), Int('disputedAt'), Int('TIMEOUT')
|
|
s.add(TIMEOUT >= 0, disputedAt >= 0, now >= disputedAt)
|
|
# resolveByTimeout is blocked iff now < disputedAt + TIMEOUT. Ask for a state that is
|
|
# blocked FOREVER, i.e. blocked even as now grows without bound: unsat by construction.
|
|
s.add(now >= disputedAt + TIMEOUT) # the timeout HAS elapsed
|
|
s.add(now < disputedAt + TIMEOUT) # ...yet the guard still blocks
|
|
check("DISPUTED always has an exit: timeout guard cannot block after the timeout", s)
|
|
|
|
# ---- reclaimUnsettled (Submitted->Refunded): pqc-gated job whose provider never signs.
|
|
# reward -> requester, bond -> provider (RETURNED, not slashed). Net: token -= reward,
|
|
# native -= bond. Solvency preserved; and because the bond is returned rather than
|
|
# slashed, an unsigned job cannot be used by the requester to profit.
|
|
s = Solver()
|
|
balE, liabE, balN, liabN = Int('balE'), Int('liabE'), Int('balN'), Int('liabN')
|
|
reward, bond = Int('reward'), Int('bond')
|
|
s.add(INV(balE, liabE), INV(balN, liabN),
|
|
reward >= 1, reward <= liabE, bond >= 1, bond <= liabN)
|
|
s.add(Not(And(INV(balE - reward, liabE - reward), INV(balN - bond, liabN - bond))))
|
|
check("reclaimUnsettled() preserves INV on both assets (reward out, bond returned)", s)
|
|
|
|
# ---- reclaimUnsettled is NOT a requester escape hatch on a non-pqc job: the guard
|
|
# requires pqcSettlement == true. A non-pqc job is finalizable by anyone, so a
|
|
# requester who could call this would be able to dodge paying for correct work.
|
|
s = Solver()
|
|
pqc = Int('pqc') # 1 = job is pqc-gated, 0 = not
|
|
s.add(pqc == 0) # non-pqc job
|
|
s.add(pqc == 1) # ...yet the guard admits it
|
|
check("reclaimUnsettled() is guard-infeasible on a non-pqc job (no requester escape)", s)
|
|
|
|
# ---- NEG-CTRL: a BUGGY resolveByTimeout that SLASHES on timeout, paying the provider
|
|
# bond to the challenger while ALSO returning it to the provider, sends the same
|
|
# pBond out twice and under-backs native escrow. This is why the timeout unwind is
|
|
# neutral: the absent-arbiter path must not try to pick a winner.
|
|
s = Solver()
|
|
balN, liabN, pBond, chBond = Int('balN'), Int('liabN'), Int('pBond'), Int('chBond')
|
|
s.add(INV(balN, liabN), pBond >= 1, chBond >= 1, pBond + chBond <= liabN)
|
|
s.add(Not(INV(balN - (pBond + pBond + chBond), liabN - (pBond + chBond))))
|
|
check("BUGGY resolveByTimeout (pBond paid twice) CAN under-back native escrow",
|
|
s, expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NO NATIVE/ERC-20 DOUBLE COUNT: a single ERC-20-reward + native-bond settle
|
|
# keeps BOTH assets solvent AND touches each asset's counter exactly once
|
|
# (reward only on token E, bond only on native N). Prove the joint post-state.
|
|
s = Solver()
|
|
balE, liabE, balN, liabN = Int('balE'), Int('liabE'), Int('balN'), Int('liabN')
|
|
reward, bond = Int('reward'), Int('bond')
|
|
s.add(INV(balE, liabE), INV(balN, liabN),
|
|
reward >= 1, reward <= liabE, bond >= 1, bond <= liabN)
|
|
# token=E job: E asset -= reward ; native asset -= bond ; NO cross-posting.
|
|
postE_bal, postE_liab = balE - reward, liabE - reward
|
|
postN_bal, postN_liab = balN - bond, liabN - bond
|
|
s.add(Not(And(INV(postE_bal, postE_liab), INV(postN_bal, postN_liab))))
|
|
check("no double-count: ERC20-reward + native-bond settle keeps BOTH assets solvent", s)
|
|
|
|
# ---- NO DOUBLE-PAY: a job reaches a terminal status exactly once. Any payout op
|
|
# requires a NON-terminal status (< Paid=5) and sets a terminal one; a second
|
|
# payout needs a non-terminal status again -> guard-infeasible. ------------
|
|
s = Solver()
|
|
st, TERMINAL = Int('st'), 5
|
|
# After op1 the job is terminal (st >= 5). A second payout guard needs st < 5.
|
|
s.add(st >= TERMINAL, st < TERMINAL) # status-flag guard for the 2nd payout
|
|
check("double-pay: second payout after terminal status is guard-infeasible", s)
|
|
|
|
# ---- ZK pay-only-on-proof: in ZK_VERIFIED mode, settlement is INSIDE
|
|
# submitResultZK, strictly AFTER ZK_VERIFIER.verifyProof (which reverts on an
|
|
# invalid proof). Model the verify as a guard: pay_zk => proofValid. ------
|
|
s = Solver()
|
|
proofValid, pay_zk = Int('proofValid'), Int('pay_zk')
|
|
s.add(Or(proofValid == 0, proofValid == 1))
|
|
# The ONLY ZK payout path requires verifyProof to have returned (no revert):
|
|
s.add(pay_zk == If(proofValid == 1, 1, 0)) # pay iff proof verified
|
|
s.add(pay_zk == 1, proofValid == 0) # NEGATION: paid without a valid proof
|
|
check("ZK_VERIFIED: paying without a valid proof is impossible (verify gate)", s)
|
|
|
|
# ============================ NEGATIVE CONTROLS ==============================
|
|
|
|
# ---- NEG-CTRL 1: a BUGGY postJob that commits `reward` to liab but accepts a
|
|
# fee-on-transfer token (received < reward), i.e. WITHOUT the received==reward
|
|
# check. liab grows by reward, balance only by received -> under-backed. ---
|
|
s = Solver()
|
|
balE, liabE, reward, received = Int('balE'), Int('liabE'), Int('reward'), Int('received')
|
|
s.add(INV(balE, liabE), reward >= 1, received >= 0, received < reward) # fee-on-transfer
|
|
s.add(Not(INV(balE + received, liabE + reward))) # BUG: commit full reward
|
|
check("BUGGY postJob (commit reward, receive less) CAN under-back escrow", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 2: a BUGGY claimJob that posts the native bond to the balance but
|
|
# credits liab on the WRONG asset (the ERC-20 reward token E). E's liab grows
|
|
# with no matching E balance -> E under-backed (the per-asset separation is
|
|
# load-bearing). z3 finds the under-backing on asset E. --------------------
|
|
s = Solver()
|
|
balE, liabE, bond = Int('balE'), Int('liabE'), Int('bond')
|
|
s.add(INV(balE, liabE), bond >= 1) # native bond arrives, but mis-posted to E
|
|
s.add(Not(INV(balE, liabE + bond))) # BUG: liab[E] += bond, bal[E] unchanged
|
|
check("BUGGY claim (bond mis-posted to ERC20 asset) CAN under-back that asset", s,
|
|
expect_unsat=False, kind="NEG-CTRL")
|
|
|
|
# ---- NEG-CTRL 3: a BUGGY ZK path that settles WITHOUT the verifyProof gate can
|
|
# pay a provider with no valid proof. Removing the gate makes it satisfiable.
|
|
s = Solver()
|
|
proofValid, pay_zk = Int('proofValid'), Int('pay_zk')
|
|
s.add(Or(proofValid == 0, proofValid == 1))
|
|
s.add(pay_zk == 1) # BUG: pay unconditionally, no verify gate
|
|
s.add(proofValid == 0) # ... even though the proof is invalid
|
|
check("BUGGY ZK settle (no verify gate) CAN pay without a valid proof", 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("ESCROW SOLVENCY (INV(T): bal[T] >= totalLiabilities[T]) for AereComputeMarketV3:")
|
|
print(" PROVED inductive -- base case + postJob(native/ERC20) / claimJob / cancelJob /")
|
|
print(" submitResult / settle(accept,finalize,ZK) / reclaimExpired / dispute /")
|
|
print(" resolveDispute(both branches) all preserve it, per asset, with reward on its own")
|
|
print(" asset and every bond on native, NO cross-asset double-count. Double-pay is guard-")
|
|
print(" infeasible (terminal status set once) and a ZK_VERIFIED job cannot be paid without")
|
|
print(" a valid proof (settlement sits behind the verifyProof gate).")
|
|
print(" Three NEG-CTRLs fire: fee-on-transfer commit, bond mis-posted to the wrong asset,")
|
|
print(" and a ZK settle without the verify gate each reproduce a real under-backing / pay-")
|
|
print(" without-proof counterexample, so the checks are load-bearing.")
|
|
print(" [VERIFY] The SP1 gateway's internal proof soundness and the Falcon-512 precompile")
|
|
print(" at 0x0AE1 are trusted primitives here, not re-proved by this SMT model.")
|
|
print(" BOUNDARY: this checks the DESIGN accounting over the modelled transitions, not the")
|
|
print(" compiled EVM bytecode (same caveat as the rest of the corpus).")
|
|
else:
|
|
print(" NOT fully established (see FAILED / unexpected CEX above).")
|
|
import sys
|
|
sys.exit(0 if allok else 1)
|