soma.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.

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.

Generated from soma describe on this file.

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

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/games_economy/auction_house.cell · examples/corpus/games_economy/auction_house.cell