soma.cell

Crafting forge — ingredients consumed exactly once

The classic MMO "craft-cancel dupe": start a craft, let the server consume the ingredients, then cancel at the exact tick that refunds them — keeping both the refund and (on a desynced shard) the output. Ultima Online and early WoW economies were both warped by variants of this bug. Here the craft job is a machine soma verify proves: `cancelled` is reachable ONLY from `pending` — before anything was consumed. Once the ingredients are gone the only path is `finished`, which is terminal (no re-finishing for a second free sword). And the pantry refuses to go negative, so a craft can never consume ingredients that are not there.

A Soma program from the games_economy part of the verified corpus: 98 lines, cells Forge, ForgeTests. It passes soma check with soma 3.2.4.

How it is built

The cell Forge declares 6 signals in its face: stock(item: String, n: Int) -> Int, begin_craft(job: String) -> Map, cancel_craft(job: String) -> Map, finish_craft(job: String) -> Map, pantry_count(item: String) -> Int and owned(item: String) -> Int; keeps 2 memory slots: pantry (Map<String, Int>, persistent and consistent) under the invariant pantry >= 0 and items (Map<String, Int>, persistent and consistent) under the invariant items >= 0. Its state machine craft_job starts in pending and allows 3 transitions: pending -> consumed, pending -> cancelled and consumed -> finished. cancelled and finished are terminal. Handlers: stock (line 40), begin_craft (line 46), cancel_craft (line 61), finish_craft (line 67), pantry_count (line 74) and owned (line 75).

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

Generated from soma describe on this file.

The source

crafting_forge.cell

// ============================================================================
// CRAFTING FORGE — ingredients consumed exactly once
// ============================================================================
// The classic MMO "craft-cancel dupe": start a craft, let the server consume
// the ingredients, then cancel at the exact tick that refunds them — keeping
// both the refund and (on a desynced shard) the output. Ultima Online and
// early WoW economies were both warped by variants of this bug.
// Here the craft job is a machine soma verify proves: `cancelled` is
// reachable ONLY from `pending` — before anything was consumed. Once the
// ingredients are gone the only path is `finished`, which is terminal (no
// re-finishing for a second free sword). And the pantry refuses to go
// negative, so a craft can never consume ingredients that are not there.
// ============================================================================

cell Forge {
    face {
        signal stock(item: String, n: Int) -> Int
        signal begin_craft(job: String) -> Map
        signal cancel_craft(job: String) -> Map
        signal finish_craft(job: String) -> Map
        signal pantry_count(item: String) -> Int
        signal owned(item: String) -> Int
    }

    memory {
        pantry: Map<String, Int> [persistent, consistent]
        invariant pantry >= 0
        items: Map<String, Int> [persistent, consistent]
        invariant items >= 0
    }

    // the refund path exists only BEFORE the consume; both ends are terminal
    state craft_job {
        initial: pending
        pending -> consumed
        pending -> cancelled
        consumed -> finished
    }

    on stock(item: String, n: Int) {
        pantry.set(item, (pantry.get(item) ?? 0) + n)
        return pantry.get(item)
    }

    // recipe: 1 sword = 2 iron + 1 wood, consumed atomically before output
    on begin_craft(job: String) {
        if get_status(job) != "pending" { return map("ok", false, "reason", "job already started") }
        let iron = pantry.get("iron") ?? 0
        let wood = pantry.get("wood") ?? 0
        let a = try { pantry.set("iron", iron - 2) }
        if a.error != () { return map("ok", false, "reason", "not enough iron") }
        let b = try { pantry.set("wood", wood - 1) }
        if b.error != () {
            pantry.set("iron", iron)        // undo before anything escaped
            return map("ok", false, "reason", "not enough wood")
        }
        transition(job, "consumed")
        return map("ok", true, "job", job)
    }

    on cancel_craft(job: String) {
        let r = try { transition(job, "cancelled") }
        if r.error != () { return map("ok", false, "reason", "too late: ingredients consumed") }
        return map("ok", true)
    }

    on finish_craft(job: String) {
        let r = try { transition(job, "finished") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        items.set("sword", (items.get("sword") ?? 0) + 1)
        return map("ok", true, "made", "sword")
    }

    on pantry_count(item: String) { return pantry.get(item) ?? 0 }
    on owned(item: String) { return items.get(item) ?? 0 }
}

cell test ForgeTests {
    rules {
        assert stock("iron", 2) == 2
        assert stock("wood", 1) == 1
        assert begin_craft("j1").ok == true
        assert pantry_count("iron") == 0
        // THE DUPE: cancel after consume — the refund path does not exist
        assert cancel_craft("j1").ok == false
        assert_fails transition("j1", "cancelled")
        assert finish_craft("j1").ok == true
        assert owned("sword") == 1
        // finished is terminal: no re-finish for a second free sword
        assert finish_craft("j1").ok == false
        assert_fails transition("j1", "consumed")
        // a craft cannot consume ingredients that are not there
        assert begin_craft("j2").ok == false
        assert_fails pantry.set("iron", -2)
        assert owned("sword") == 1
    }
}

What the toolchain says

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

$ soma check crafting_forge.cell
✓ All checks passed.
$ soma test crafting_forge.cell
test ForgeTests ...
  ✓ assert stock("iron", 2) == 2
  ✓ assert stock("wood", 1) == 1
  ✓ assert begin_craft("j1").ok == true
  ✓ assert pantry_count("iron") == 0
  ✓ assert cancel_craft("j1").ok == false
  ✓ assert_fails transition("j1", "cancelled") — raised invalid transition: consumed → cancelled. Current state: 'consumed'. Valid targets: [finished]
  ✓ assert finish_craft("j1").ok == true
  ✓ assert owned("sword") == 1
  ✓ assert finish_craft("j1").ok == false
  ✓ assert_fails transition("j1", "consumed") — raised invalid transition: finished → consumed. Current state: 'finished'. Valid targets: []
  ✓ assert begin_craft("j2").ok == false
  ✓ assert_fails pantry.set("iron", -2) — raised memory invariant violated on 'pantry': pantry >= 0 — rejected write of -2 (key "iron"); the slot is unchanged
  ✓ assert owned("sword") == 1

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

State machine 'craft_job': 4 states, initial 'pending'
  States: [cancelled, consumed, finished, pending]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'pending'
  ✓ terminal states: [cancelled, finished]
  ✓ 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 `begin_craft` ⟶ {pending → consumed}
  ✓ refinement: handler `cancel_craft` ⟶ {cancelled}
  ✓ refinement: handler `finish_craft` ⟶ {finished}
  · transition sources: `cancel_craft`, `finish_craft` 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)

Forge/invariants:

  ✓ invariant pantry >= 0 — writer 'begin_craft' proven by induction (writes iron)
  ⚠ invariant pantry >= 0 — runtime-checked (computed values): begin_craft → pantry because `iron - 2` is only known to lie in [-2, ∞) — narrow it: `require (iron - 2) >= 0 else …`, begin_craft → pantry because `wood - 1` is only known to lie in [-1, ∞) — narrow it: `require (wood - 1) >= 0 else …`, stock → pantry because `n` is a parameter (narrow it: `require ((pantry.get(item) ?? 0) + n) >= 0 else …`); `pantry` has no known range
  ✓ invariant items >= 0 — writer 'finish_craft' proven by induction (writes (items.get("sword") ?? 0) + 1)

12 passed, 1 warnings, 0 failures

  Temporal properties for 'craft_job':
  ✓ 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/crafting_forge.cell · examples/corpus/games_economy/crafting_forge.cell