Wager duel — staked gold that exactly one fighter can win
Wager duels and "death-match stakes" servers keep reproducing the same scam: both fighters stake gold, the loser disconnects before the result commits, and a support ticket gets the stake refunded — while the winner was ALSO paid. The pot pays out twice. Here the duel is a machine where `paid_out` and `refunded` are both TERMINAL and mutually exclusive: the pot leaves through exactly one door, once. Stakes move wallet -> pot in one handler, gold is conserved across every path, and no wallet can go negative — you cannot stake gold you do not have.
A Soma program from the games_economy part of the verified corpus: 122 lines, cells WagerDuel, DuelTests. It passes soma check with soma 3.2.4.
How it is built
The cell WagerDuel declares 6 signals in its face: fund_fighter(player: String, gold: Int) -> Int, stake(duel: String, a: String, b: String, amount: Int) -> Map, declare_winner(duel: String, winner: String) -> Map, refund_draw(duel: String) -> Map, purse_of(player: String) -> Int and house_total() -> Int; keeps 4 memory slots: purse (Map<String, Int>, persistent and consistent) under the invariant purse >= 0, pot (Map<String, Int>, persistent and consistent) under the invariant pot >= 0, side_a (Map<String, String>, persistent and consistent) and side_b (Map<String, String>, persistent and consistent). Its state machine duel_flow starts in open and allows 3 transitions: open -> staked, staked -> paid_out and staked -> refunded. paid_out and refunded are terminal. Handlers: fund_fighter (line 41), stake (line 46), declare_winner (line 63), refund_draw (line 74), purse_of (line 84) and house_total (line 86).
The file also holds 1 test cell (DuelTests) with 18 assertions, run by soma test.
The source
wager_duel.cell
// ============================================================================
// WAGER DUEL — staked gold that exactly one fighter can win
// ============================================================================
// Wager duels and "death-match stakes" servers keep reproducing the same
// scam: both fighters stake gold, the loser disconnects before the result
// commits, and a support ticket gets the stake refunded — while the winner
// was ALSO paid. The pot pays out twice. Here the duel is a machine where
// `paid_out` and `refunded` are both TERMINAL and mutually exclusive: the
// pot leaves through exactly one door, once. Stakes move wallet -> pot in
// one handler, gold is conserved across every path, and no wallet can go
// negative — you cannot stake gold you do not have.
// ============================================================================
cell WagerDuel {
face {
signal fund_fighter(player: String, gold: Int) -> Int
signal stake(duel: String, a: String, b: String, amount: Int) -> Map
signal declare_winner(duel: String, winner: String) -> Map
signal refund_draw(duel: String) -> Map
signal purse_of(player: String) -> Int
signal house_total() -> Int
}
memory {
purse: Map<String, Int> [persistent, consistent]
invariant purse >= 0
pot: Map<String, Int> [persistent, consistent]
invariant pot >= 0
side_a: Map<String, String> [persistent, consistent]
side_b: Map<String, String> [persistent, consistent]
}
// the pot leaves through exactly one terminal door
state duel_flow {
initial: open
open -> staked
staked -> paid_out
staked -> refunded
}
on fund_fighter(player: String, gold: Int) {
purse.set(player, (purse.get(player) ?? 0) + gold)
return purse.get(player)
}
on stake(duel: String, a: String, b: String, amount: Int) {
if amount <= 0 { return map("ok", false, "reason", "stake must be positive") }
if get_status(duel) != "open" { return map("ok", false, "reason", "duel already staked or settled") }
let wa = try { purse.set(a, (purse.get(a) ?? 0) - amount) }
if wa.error != () { return map("ok", false, "reason", "{a} cannot cover the stake") }
let wb = try { purse.set(b, (purse.get(b) ?? 0) - amount) }
if wb.error != () {
purse.set(a, (purse.get(a) ?? 0) + amount) // give a's stake back
return map("ok", false, "reason", "{b} cannot cover the stake")
}
transition(duel, "staked")
pot.set(duel, amount * 2)
side_a.set(duel, a)
side_b.set(duel, b)
return map("ok", true, "pot", amount * 2)
}
on declare_winner(duel: String, winner: String) {
if winner != side_a.get(duel) && winner != side_b.get(duel) {
return map("ok", false, "reason", "{winner} is not in this duel")
}
let r = try { transition(duel, "paid_out") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
purse.set(winner, (purse.get(winner) ?? 0) + (pot.get(duel) ?? 0))
pot.set(duel, 0)
return map("ok", true, "winner", winner)
}
on refund_draw(duel: String) {
let r = try { transition(duel, "refunded") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let half = idiv(pot.get(duel) ?? 0, 2)
purse.set(side_a.get(duel), (purse.get(side_a.get(duel)) ?? 0) + half)
purse.set(side_b.get(duel), (purse.get(side_b.get(duel)) ?? 0) + half)
pot.set(duel, 0)
return map("ok", true, "refunded_each", half)
}
on purse_of(player: String) { return purse.get(player) ?? 0 }
on house_total() {
let t = 0
let ps = purse.keys()
for p in ps { t = t + (purse.get(p) ?? 0) }
let ds = pot.keys()
for d in ds { t = t + (pot.get(d) ?? 0) }
return t
}
}
cell test DuelTests {
rules {
assert fund_fighter("rok", 100) == 100
assert fund_fighter("ysa", 100) == 100
assert stake("d1", "rok", "ysa", 60).ok == true
assert purse_of("rok") == 40
assert purse_of("ysa") == 40
assert house_total() == 200
// ysa wins the pot — through the ONE pay-out door
assert declare_winner("d1", "ysa").ok == true
assert purse_of("ysa") == 160
assert house_total() == 200
// THE SCAM: refund after pay-out — the door does not exist
assert refund_draw("d1").ok == false
assert_fails transition("d1", "refunded")
assert declare_winner("d1", "rok").ok == false
assert house_total() == 200
// you cannot stake gold you do not have; nobody goes negative
assert stake("d2", "rok", "ysa", 9999).ok == false
assert_fails purse.set("rok", -1)
// an outsider cannot be declared winner of someone else's duel
assert fund_fighter("eve", 50) == 50
assert stake("d3", "rok", "ysa", 10).ok == true
assert declare_winner("d3", "eve").ok == false
}
}What the toolchain says
$ soma check wager_duel.cell
✓ All checks passed.$ soma test wager_duel.cell
test DuelTests ...
✓ assert fund_fighter("rok", 100) == 100
✓ assert fund_fighter("ysa", 100) == 100
✓ assert stake("d1", "rok", "ysa", 60).ok == true
✓ assert purse_of("rok") == 40
✓ assert purse_of("ysa") == 40
✓ assert house_total() == 200
✓ assert declare_winner("d1", "ysa").ok == true
✓ assert purse_of("ysa") == 160
✓ assert house_total() == 200
✓ assert refund_draw("d1").ok == false
✓ assert_fails transition("d1", "refunded") — raised invalid transition: paid_out → refunded. Current state: 'paid_out'. Valid targets: []
✓ assert declare_winner("d1", "rok").ok == false
✓ assert house_total() == 200
✓ assert stake("d2", "rok", "ysa", 9999).ok == false
✓ assert_fails purse.set("rok", -1) — raised memory invariant violated on 'purse': purse >= 0 — rejected write of -1 (key "rok"); the slot is unchanged
✓ assert fund_fighter("eve", 50) == 50
✓ assert stake("d3", "rok", "ysa", 10).ok == true
✓ assert declare_winner("d3", "eve").ok == false
18 tests: 18 passed, 0 failed$ soma verify wager_duel.cell
Verifying wager_duel.cell...
State machine 'duel_flow': 4 states, initial 'open'
States: [open, paid_out, refunded, staked]
✓ 4 states, 3 transitions
✓ all states reachable from 'open'
✓ terminal states: [paid_out, refunded]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `stake` ⟶ {open → staked}
✓ refinement: handler `declare_winner` ⟶ {paid_out}
✓ refinement: handler `refund_draw` ⟶ {refunded}
· transition sources: `declare_winner`, `refund_draw` 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)
WagerDuel/invariants:
✓ invariant purse >= 0 — writer 'declare_winner' proven by induction (writes (purse.get(winner) ?? 0) + (pot.get(duel) ?? 0))
✓ invariant purse >= 0 — writer 'refund_draw' proven by induction (writes (purse.get(side_a.get(duel)) ?? 0) + half)
✓ invariant purse >= 0 — writer 'refund_draw' proven by induction (writes (purse.get(side_b.get(duel)) ?? 0) + half)
✓ invariant purse >= 0 — writer 'stake' proven by induction (writes (purse.get(a) ?? 0) + amount)
⚠ invariant purse >= 0 — runtime-checked (computed values): fund_fighter → purse because `gold` is a parameter (narrow it: `require ((purse.get(player) ?? 0) + gold) >= 0 else …`); `purse` has no known range, stake → purse because `purse` has no known range
✓ invariant pot >= 0 — writer 'declare_winner' proven (writes 0)
✓ invariant pot >= 0 — writer 'refund_draw' proven (writes 0)
✓ invariant pot >= 0 — writer 'stake' proven by induction (writes amount * 2)
17 passed, 1 warnings, 0 failures
Temporal properties for 'duel_flow':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK