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