Auction house — escrowed bids, gold that cannot be printed
In 2013 Blizzard took the Diablo III auction house offline after patch 1.0.8: cancelling a bid refunded the gold WITHOUT releasing the escrow, and billions of duplicated gold crashed the economy within hours. The bug was an accounting gap — wallet and escrow updated by paths that disagreed. Here the accounting is structural: a bid MOVES gold wallet->escrow in one handler, an outbid refunds exactly the escrowed amount, and total_gold() is conserved by construction. Balances cannot go negative (the memory refuses the write), and `sold` is a TERMINAL state soma verify proves: a settled auction can never reopen for a second refund.
A Soma program from the games_economy part of the verified corpus: 124 lines, cells AuctionHouse, AuctionTests. It passes soma check with soma 3.2.4.
How it is built
The cell AuctionHouse declares 6 signals in its face: fund(player: String, gold: Int) -> Int, place_bid(auction: String, player: String, amount: Int) -> Map, settle(auction: String, seller: String) -> Map, balance_of(player: String) -> Int, escrow_of(player: String) -> Int and total_gold() -> Int; keeps 4 memory slots: wallet (Map<String, Int>, persistent and consistent) under the invariant wallet >= 0, escrow (Map<String, Int>, persistent and consistent) under the invariant escrow >= 0, high_bid (Map<String, Int>, persistent and consistent) and high_bidder (Map<String, String>, persistent and consistent). Its state machine auction starts in listed and allows 3 transitions: listed -> bidding, listed -> withdrawn and bidding -> sold. sold and withdrawn are terminal. Handlers: fund (line 43), place_bid (line 48), settle (line 71), balance_of (line 81), escrow_of (line 82) and total_gold (line 84).
The file also holds 1 test cell (AuctionTests) with 20 assertions, run by soma test.
The source
auction_house.cell
// ============================================================================
// AUCTION HOUSE — escrowed bids, gold that cannot be printed
// ============================================================================
// In 2013 Blizzard took the Diablo III auction house offline after patch
// 1.0.8: cancelling a bid refunded the gold WITHOUT releasing the escrow,
// and billions of duplicated gold crashed the economy within hours. The bug
// was an accounting gap — wallet and escrow updated by paths that disagreed.
// Here the accounting is structural: a bid MOVES gold wallet->escrow in one
// handler, an outbid refunds exactly the escrowed amount, and total_gold()
// is conserved by construction. Balances cannot go negative (the memory
// refuses the write), and `sold` is a TERMINAL state soma verify proves:
// a settled auction can never reopen for a second refund.
// ============================================================================
cell AuctionHouse {
face {
signal fund(player: String, gold: Int) -> Int
signal place_bid(auction: String, player: String, amount: Int) -> Map
signal settle(auction: String, seller: String) -> Map
signal balance_of(player: String) -> Int
signal escrow_of(player: String) -> Int
signal total_gold() -> Int
}
memory {
wallet: Map<String, Int> [persistent, consistent]
invariant wallet >= 0
escrow: Map<String, Int> [persistent, consistent]
invariant escrow >= 0
high_bid: Map<String, Int> [persistent, consistent]
high_bidder: Map<String, String> [persistent, consistent]
}
// sold and withdrawn are terminal: no post-sale cancel, no double refund.
// An auction with a live bid (bidding) can no longer be withdrawn.
state auction {
initial: listed
listed -> bidding
listed -> withdrawn
bidding -> sold
}
on fund(player: String, gold: Int) {
wallet.set(player, (wallet.get(player) ?? 0) + gold)
return wallet.get(player)
}
on place_bid(auction: String, player: String, amount: Int) {
let phase = get_status(auction)
if phase != "listed" && phase != "bidding" {
return map("ok", false, "reason", "auction is {phase}")
}
let lead = high_bid.get(auction) ?? 0
if amount <= lead { return map("ok", false, "reason", "{amount} does not beat {lead}") }
// the wall: an over-wallet bid drives the balance negative — REFUSED
let w = try { wallet.set(player, (wallet.get(player) ?? 0) - amount) }
if w.error != () { return map("ok", false, "reason", "insufficient gold") }
escrow.set(player, (escrow.get(player) ?? 0) + amount)
let prev = high_bidder.get(auction)
if prev != () {
// refund the old leader EXACTLY the escrowed amount — conservation
escrow.set(prev, (escrow.get(prev) ?? 0) - lead)
wallet.set(prev, (wallet.get(prev) ?? 0) + lead)
}
high_bid.set(auction, amount)
high_bidder.set(auction, player)
if phase == "listed" { transition(auction, "bidding") }
return map("ok", true, "lead", amount)
}
on settle(auction: String, seller: String) {
let r = try { transition(auction, "sold") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let winner = high_bidder.get(auction)
let amount = high_bid.get(auction)
escrow.set(winner, (escrow.get(winner) ?? 0) - amount)
wallet.set(seller, (wallet.get(seller) ?? 0) + amount)
return map("ok", true, "winner", winner, "paid", amount)
}
on balance_of(player: String) { return wallet.get(player) ?? 0 }
on escrow_of(player: String) { return escrow.get(player) ?? 0 }
on total_gold() {
let t = 0
let ws = wallet.keys()
for p in ws { t = t + (wallet.get(p) ?? 0) }
let es = escrow.keys()
for p in es { t = t + (escrow.get(p) ?? 0) }
return t
}
}
cell test AuctionTests {
rules {
assert fund("alice", 100) == 100
assert fund("bob", 100) == 100
// a bid escrows gold: it leaves the wallet, the total is conserved
assert place_bid("ax", "alice", 60).ok == true
assert balance_of("alice") == 40
assert escrow_of("alice") == 60
assert total_gold() == 200
// an outbid refunds the old leader exactly what was escrowed
assert place_bid("ax", "bob", 80).ok == true
assert balance_of("alice") == 100
assert escrow_of("alice") == 0
assert total_gold() == 200
// you cannot bid gold you do not have — the wallet refuses negatives
assert place_bid("ax", "alice", 999).ok == false
assert_fails wallet.set("alice", -1)
// settlement pays the seller from escrow; still conserved
assert settle("ax", "seller").ok == true
assert balance_of("seller") == 80
assert total_gold() == 200
// SOLD IS TERMINAL — the Diablo III double-refund has no state to reach
assert_fails transition("ax", "bidding")
assert_fails transition("ax", "listed")
assert place_bid("ax", "alice", 90).ok == false
// an auction with a live bid cannot be quietly withdrawn
assert place_bid("ay", "bob", 10).ok == true
assert_fails transition("ay", "withdrawn")
}
}What the toolchain says
$ soma check auction_house.cell
✓ All checks passed.$ soma test auction_house.cell
test AuctionTests ...
✓ assert fund("alice", 100) == 100
✓ assert fund("bob", 100) == 100
✓ assert place_bid("ax", "alice", 60).ok == true
✓ assert balance_of("alice") == 40
✓ assert escrow_of("alice") == 60
✓ assert total_gold() == 200
✓ assert place_bid("ax", "bob", 80).ok == true
✓ assert balance_of("alice") == 100
✓ assert escrow_of("alice") == 0
✓ assert total_gold() == 200
✓ assert place_bid("ax", "alice", 999).ok == false
✓ assert_fails wallet.set("alice", -1) — raised memory invariant violated on 'wallet': wallet >= 0 — rejected write of -1 (key "alice"); the slot is unchanged
✓ assert settle("ax", "seller").ok == true
✓ assert balance_of("seller") == 80
✓ assert total_gold() == 200
✓ assert_fails transition("ax", "bidding") — raised invalid transition: sold → bidding. Current state: 'sold'. Valid targets: []
✓ assert_fails transition("ax", "listed") — raised invalid transition: sold → listed. Current state: 'sold'. Valid targets: []
✓ assert place_bid("ax", "alice", 90).ok == false
✓ assert place_bid("ay", "bob", 10).ok == true
✓ assert_fails transition("ay", "withdrawn") — raised invalid transition: bidding → withdrawn. Current state: 'bidding'. Valid targets: [sold]
20 tests: 20 passed, 0 failed$ soma verify auction_house.cell
Verifying auction_house.cell...
State machine 'auction': 4 states, initial 'listed'
States: [bidding, listed, sold, withdrawn]
✓ 4 states, 3 transitions
✓ all states reachable from 'listed'
✓ terminal states: [withdrawn, sold]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 2 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
⚠ refinement: declared transition `listed → withdrawn` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `place_bid` ⟶ {listed → bidding [if phase == "listed"]}
✓ refinement: handler `settle` ⟶ {sold}
· transition sources: `settle` calls transition(id, target) without declaring the source — the runtime refuses a move the graph forbids, but the proof does not see where the handler starts; `transition(id, from, to)` names the edge (checked by `soma check`, refused at run time from any other state)
AuctionHouse/invariants:
⚠ invariant wallet >= 0 — runtime-checked (computed values): fund → wallet because `gold` is a parameter (narrow it: `require ((wallet.get(player) ?? 0) + gold) >= 0 else …`); `wallet` has no known range, place_bid → wallet because `amount` is a parameter (narrow it: `require ((wallet.get(player) ?? 0) - amount) >= 0 else …`); `wallet` has no known range, place_bid → wallet because `lead` = (high_bid.get(auction) ?? 0) — not bounded (give both sides of `??` a bound); `prev` reads a slot with no interval invariant; `wallet` has no known range, settle → wallet because `amount` reads a slot with no interval invariant; `wallet` has no known range
⚠ invariant escrow >= 0 — runtime-checked (computed values): place_bid → escrow because `amount` is a parameter (narrow it: `require ((escrow.get(player) ?? 0) + amount) >= 0 else …`); `escrow` has no known range, place_bid → escrow because `escrow` has no known range; `lead` = (high_bid.get(auction) ?? 0) — not bounded (give both sides of `??` a bound); `prev` reads a slot with no interval invariant, settle → escrow because `amount` reads a slot with no interval invariant; `escrow` has no known range; `winner` reads a slot with no interval invariant
9 passed, 3 warnings, 0 failures
Temporal properties for 'auction':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK