#!/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) # ---- 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)