soma.cell

Gem store — a purchase receipt credits exactly once

The "receipt replay" exploit: capture one valid in-app-purchase receipt and submit it to the game server again and again — each replay credits the gems again. Several mobile studios shipped this exact validation gap before Apple and Google hardened server-side receipt checks; it is real money printed from a single purchase. Here a receipt is a state machine: created -> paid -> credited, and `credited` is TERMINAL — the replayed submit has no transition to take. Conservation rides on top: every gem in circulation traces to exactly one credited receipt (minted == circulating + sunk), and no balance can ever go negative.

A Soma program from the games_economy part of the verified corpus: 101 lines, cells GemStore, GemTests. It passes soma check with soma 3.2.4.

How it is built

The cell GemStore declares 5 signals in its face: mark_paid(receipt: String, player: String, gems: Int) -> Map, redeem(receipt: String) -> Map, spend_gems(player: String, n: Int) -> Map, gems_of(player: String) -> Int and conserved() -> Bool; keeps 5 memory slots: balance (Map<String, Int>, persistent and consistent) under the invariant balance >= 0, minted (Map<String, Int>, persistent and consistent) under the invariant minted >= 0, sunk (Map<String, Int>, persistent and consistent) under the invariant sunk >= 0, rcpt_player (Map<String, String>, persistent and consistent) and rcpt_gems (Map<String, Int>, persistent and consistent). Its state machine receipt starts in created and allows 3 transitions: created -> paid, created -> voided and paid -> credited. credited and voided are terminal. Handlers: mark_paid (line 42), redeem (line 51), spend_gems (line 62), gems_of (line 70) and conserved (line 72).

The file also holds 1 test cell (GemTests) with 13 assertions, run by soma test.

Generated from soma describe on this file.

The source

gem_store.cell

// ============================================================================
// GEM STORE — a purchase receipt credits exactly once
// ============================================================================
// The "receipt replay" exploit: capture one valid in-app-purchase receipt
// and submit it to the game server again and again — each replay credits
// the gems again. Several mobile studios shipped this exact validation gap
// before Apple and Google hardened server-side receipt checks; it is real
// money printed from a single purchase. Here a receipt is a state machine:
// created -> paid -> credited, and `credited` is TERMINAL — the replayed
// submit has no transition to take. Conservation rides on top: every gem in
// circulation traces to exactly one credited receipt (minted == circulating
// + sunk), and no balance can ever go negative.
// ============================================================================

cell GemStore {
    face {
        signal mark_paid(receipt: String, player: String, gems: Int) -> Map
        signal redeem(receipt: String) -> Map
        signal spend_gems(player: String, n: Int) -> Map
        signal gems_of(player: String) -> Int
        signal conserved() -> Bool
    }

    memory {
        balance: Map<String, Int> [persistent, consistent]
        invariant balance >= 0
        minted: Map<String, Int> [persistent, consistent]
        invariant minted >= 0
        sunk: Map<String, Int> [persistent, consistent]
        invariant sunk >= 0
        rcpt_player: Map<String, String> [persistent, consistent]
        rcpt_gems: Map<String, Int> [persistent, consistent]
    }

    state receipt {
        initial: created
        created -> paid
        created -> voided
        paid -> credited
    }

    on mark_paid(receipt: String, player: String, gems: Int) {
        if gems <= 0 { return map("ok", false, "reason", "gems must be positive") }
        let r = try { transition(receipt, "paid") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        rcpt_player.set(receipt, player)
        rcpt_gems.set(receipt, gems)
        return map("ok", true)
    }

    on redeem(receipt: String) {
        // THE REPLAY WALL: paid -> credited fires once; credited is terminal
        let r = try { transition(receipt, "credited") }
        if r.error != () { return map("ok", false, "reason", "not redeemable: {r.error}") }
        let p = rcpt_player.get(receipt)
        let g = rcpt_gems.get(receipt)
        balance.set(p, (balance.get(p) ?? 0) + g)
        minted.set("total", (minted.get("total") ?? 0) + g)
        return map("ok", true, "credited", g)
    }

    on spend_gems(player: String, n: Int) {
        if n <= 0 { return map("ok", false, "reason", "spend must be positive") }
        let w = try { balance.set(player, (balance.get(player) ?? 0) - n) }
        if w.error != () { return map("ok", false, "reason", "insufficient gems") }
        sunk.set("total", (sunk.get("total") ?? 0) + n)
        return map("ok", true)
    }

    on gems_of(player: String) { return balance.get(player) ?? 0 }

    on conserved() {
        let circ = 0
        let players = balance.keys()
        for p in players { circ = circ + (balance.get(p) ?? 0) }
        return (minted.get("total") ?? 0) == circ + (sunk.get("total") ?? 0)
    }
}

cell test GemTests {
    rules {
        assert mark_paid("rc-9", "mia", 500).ok == true
        assert redeem("rc-9").ok == true
        assert gems_of("mia") == 500
        // THE REPLAY: submitting the same receipt again has no transition
        assert redeem("rc-9").ok == false
        assert gems_of("mia") == 500
        assert_fails transition("rc-9", "credited")
        assert_fails transition("rc-9", "paid")
        // a receipt that was never paid cannot be redeemed
        assert redeem("rc-ghost").ok == false
        // spending flows into the sink; overdraft is refused by the memory
        assert spend_gems("mia", 200).ok == true
        assert spend_gems("mia", 999).ok == false
        assert_fails balance.set("mia", -1)
        assert gems_of("mia") == 300
        // the books balance: minted == circulating + sunk
        assert conserved() == true
    }
}

What the toolchain says

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

$ soma check gem_store.cell
✓ All checks passed.
$ soma test gem_store.cell
test GemTests ...
  ✓ assert mark_paid("rc-9", "mia", 500).ok == true
  ✓ assert redeem("rc-9").ok == true
  ✓ assert gems_of("mia") == 500
  ✓ assert redeem("rc-9").ok == false
  ✓ assert gems_of("mia") == 500
  ✓ assert_fails transition("rc-9", "credited") — raised invalid transition: credited → credited. Current state: 'credited'. Valid targets: []
  ✓ assert_fails transition("rc-9", "paid") — raised invalid transition: credited → paid. Current state: 'credited'. Valid targets: []
  ✓ assert redeem("rc-ghost").ok == false
  ✓ assert spend_gems("mia", 200).ok == true
  ✓ assert spend_gems("mia", 999).ok == false
  ✓ assert_fails balance.set("mia", -1) — raised memory invariant violated on 'balance': balance >= 0 — rejected write of -1 (key "mia"); the slot is unchanged
  ✓ assert gems_of("mia") == 300
  ✓ assert conserved() == true

13 tests: 13 passed, 0 failed
$ soma verify gem_store.cell
Verifying gem_store.cell...

State machine 'receipt': 4 states, initial 'created'
  States: [created, credited, paid, voided]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'created'
  ✓ terminal states: [voided, credited]
  ✓ 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 5 handlers structurally terminate
  ⚠ refinement: declared transition `created → voided` is never reached by any handler — spec may be aspirational or stale
  ✓ refinement: handler `mark_paid` ⟶ {paid}
  ✓ refinement: handler `redeem` ⟶ {credited}
  · transition sources: `mark_paid`, `redeem` call 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)

GemStore/invariants:

  ⚠ invariant balance >= 0 — runtime-checked (computed values): redeem → balance because `balance` has no known range; `g` reads a slot with no interval invariant; `p` reads a slot with no interval invariant, spend_gems → balance because `balance` has no known range
  ⚠ invariant minted >= 0 — runtime-checked (computed values): redeem → minted because `g` reads a slot with no interval invariant; `minted` has no known range
  ✓ invariant sunk >= 0 — writer 'spend_gems' proven by induction (writes (sunk.get("total") ?? 0) + n)

10 passed, 3 warnings, 0 failures

  Temporal properties for 'receipt':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

map, transition

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