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