Loot roll — one roll per raider, one award per drop
Raid loot drama is as old as raids: a player spam-clicks "Need" and gets two entries in the roll, or a master looter awards the same drop to two friends ("it bugged, I swear"). Both killed guilds; the second was a real duping vector when award and mail-out raced. Here each (raider, drop) roll is walled at <= 1 entry by the memory, and the drop itself is a machine: rolling -> awarded is the ONLY award edge and `awarded` is terminal — soma verify proves a drop cannot be handed out twice.
A Soma program from the games_economy part of the verified corpus: 84 lines, cells LootRoll, RollTests. It passes soma check with soma 3.2.4.
How it is built
The cell LootRoll declares 4 signals in its face: enter_roll(drop: String, raider: String, roll_value: Int) -> Map, award(drop: String) -> Map, holder_of(drop: String) -> String and best_roll(drop: String) -> Int; keeps 4 memory slots: entries (Map<String, Int>, persistent and consistent) under the invariant entries >= 0 && entries <= 1, lead_roll (Map<String, Int>, persistent and consistent), lead_raider (Map<String, String>, persistent and consistent) and holder (Map<String, String>, persistent and consistent). Its state machine drop_flow starts in rolling and allows 2 transitions: rolling -> awarded and rolling -> disenchanted. awarded and disenchanted are terminal. Handlers: enter_roll (line 35), award (line 49), holder_of (line 58) and best_roll (line 59).
The file also holds 1 test cell (RollTests) with 14 assertions, run by soma test.
The source
loot_roll.cell
// ============================================================================
// LOOT ROLL — one roll per raider, one award per drop
// ============================================================================
// Raid loot drama is as old as raids: a player spam-clicks "Need" and gets
// two entries in the roll, or a master looter awards the same drop to two
// friends ("it bugged, I swear"). Both killed guilds; the second was a real
// duping vector when award and mail-out raced. Here each (raider, drop)
// roll is walled at <= 1 entry by the memory, and the drop itself is a
// machine: rolling -> awarded is the ONLY award edge and `awarded` is
// terminal — soma verify proves a drop cannot be handed out twice.
// ============================================================================
cell LootRoll {
face {
signal enter_roll(drop: String, raider: String, roll_value: Int) -> Map
signal award(drop: String) -> Map
signal holder_of(drop: String) -> String
signal best_roll(drop: String) -> Int
}
memory {
entries: Map<String, Int> [persistent, consistent]
invariant entries >= 0 && entries <= 1
lead_roll: Map<String, Int> [persistent, consistent]
lead_raider: Map<String, String> [persistent, consistent]
holder: Map<String, String> [persistent, consistent]
}
state drop_flow {
initial: rolling
rolling -> awarded
rolling -> disenchanted
}
on enter_roll(drop: String, raider: String, roll_value: Int) {
if get_status(drop) != "rolling" { return map("ok", false, "reason", "rolls are closed") }
if roll_value < 1 || roll_value > 100 { return map("ok", false, "reason", "roll must be 1..100") }
let key = "{drop}/{raider}"
// THE WALL: a second entry from the same raider cannot be stored
let w = try { entries.set(key, (entries.get(key) ?? 0) + 1) }
if w.error != () { return map("ok", false, "reason", "{raider} already rolled") }
if roll_value > (lead_roll.get(drop) ?? 0) {
lead_roll.set(drop, roll_value)
lead_raider.set(drop, raider)
}
return map("ok", true, "rolled", roll_value)
}
on award(drop: String) {
if lead_raider.get(drop) == () { return map("ok", false, "reason", "nobody rolled") }
// the ONLY award edge — and awarded is terminal
let r = try { transition(drop, "awarded") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
holder.set(drop, lead_raider.get(drop))
return map("ok", true, "winner", holder.get(drop))
}
on holder_of(drop: String) { return holder.get(drop) ?? "" }
on best_roll(drop: String) { return lead_roll.get(drop) ?? 0 }
}
cell test RollTests {
rules {
assert enter_roll("axe", "thorin", 42).ok == true
// THE SPAM-CLICK: a second entry is an unstorable write
assert enter_roll("axe", "thorin", 99).ok == false
assert best_roll("axe") == 42
assert_fails entries.set("axe/thorin", 2)
assert enter_roll("axe", "gimli", 77).ok == true
assert best_roll("axe") == 77
// out-of-range rolls from modified clients bounce
assert enter_roll("axe", "loki", 999).ok == false
assert award("axe").ok == true
assert holder_of("axe") == "gimli"
// AWARDED IS TERMINAL: no second hand-out, no late entries
assert award("axe").ok == false
assert_fails transition("axe", "rolling")
assert_fails transition("axe", "disenchanted")
assert enter_roll("axe", "loki", 50).ok == false
// a drop nobody rolled on cannot be "awarded" to a friend
assert award("shield").ok == false
}
}What the toolchain says
$ soma check loot_roll.cell
✓ All checks passed.$ soma test loot_roll.cell
test RollTests ...
✓ assert enter_roll("axe", "thorin", 42).ok == true
✓ assert enter_roll("axe", "thorin", 99).ok == false
✓ assert best_roll("axe") == 42
✓ assert_fails entries.set("axe/thorin", 2) — raised memory invariant violated on 'entries': entries >= 0 && entries <= 1 — rejected write of 2 (key "axe/thorin"); the slot is unchanged
✓ assert enter_roll("axe", "gimli", 77).ok == true
✓ assert best_roll("axe") == 77
✓ assert enter_roll("axe", "loki", 999).ok == false
✓ assert award("axe").ok == true
✓ assert holder_of("axe") == "gimli"
✓ assert award("axe").ok == false
✓ assert_fails transition("axe", "rolling") — raised invalid transition: awarded → rolling. Current state: 'awarded'. Valid targets: []
✓ assert_fails transition("axe", "disenchanted") — raised invalid transition: awarded → disenchanted. Current state: 'awarded'. Valid targets: []
✓ assert enter_roll("axe", "loki", 50).ok == false
✓ assert award("shield").ok == false
14 tests: 14 passed, 0 failed$ soma verify loot_roll.cell
Verifying loot_roll.cell...
State machine 'drop_flow': 3 states, initial 'rolling'
States: [awarded, disenchanted, rolling]
✓ 3 states, 2 transitions
✓ all states reachable from 'rolling'
✓ terminal states: [awarded, disenchanted]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (1 handlers, 1 literal transitions, 0 dynamic)
✓ termination: all 4 handlers structurally terminate
⚠ refinement: declared transition `rolling → disenchanted` is never reached by any handler — spec may be aspirational or stale
✓ refinement: handler `award` ⟶ {awarded}
· transition sources: `award` 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)
LootRoll/invariants:
✓ invariant entries >= 0 — writer 'enter_roll' proven by induction (writes (entries.get(key) ?? 0) + 1)
⚠ invariant entries >= 0 && entries <= 1 — runtime-checked (computed values): enter_roll → entries [entries <= 1] because `entries` has no known range; `key` = "{drop}/{raider}" — not bounded
9 passed, 2 warnings, 0 failures
Temporal properties for 'drop_flow':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK