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

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.

Generated from soma describe on this file.

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

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

$ 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

Builtins used

get_status, map, transition

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