soma.cell

Harvest node — one vein, one yield per respawn cycle

"Node duping" in MMO gathering: hit the same ore vein twice inside the lag window before the server marks it empty. Classic WoW's launch had mining nodes yielding to two players at once, and every gathering economy since has fought the same race. Here the race has nowhere to live: the yield IS the transition `ripe -> harvested`, so the second strike in the lag window has no edge to take. Nodes also wear out — `depleted` is terminal (soma verify proves it), killing infinite-respawn farm spots — and the ore ledger can never go negative.

A Soma program from the games_economy part of the verified corpus: 79 lines, cells Mine, MineTests. It passes soma check with soma 3.2.4.

How it is built

The cell Mine declares 5 signals in its face: harvest(node: String, player: String) -> Map, respawn_node(node: String) -> Map, retire_node(node: String) -> Map, ore_of(player: String) -> Int and node_phase(node: String) -> String; keeps 1 memory slot: ore (Map<String, Int>, persistent and consistent) under the invariant ore >= 0. Its state machine node_cycle starts in ripe and allows 3 transitions: ripe -> harvested, harvested -> ripe and harvested -> depleted. depleted is terminal. Handlers: harvest (line 35), respawn_node (line 43), retire_node (line 49), ore_of (line 55) and node_phase (line 56).

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

Generated from soma describe on this file.

The source

harvest_node.cell

// ============================================================================
// HARVEST NODE — one vein, one yield per respawn cycle
// ============================================================================
// "Node duping" in MMO gathering: hit the same ore vein twice inside the
// lag window before the server marks it empty. Classic WoW's launch had
// mining nodes yielding to two players at once, and every gathering economy
// since has fought the same race. Here the race has nowhere to live: the
// yield IS the transition `ripe -> harvested`, so the second strike in the
// lag window has no edge to take. Nodes also wear out — `depleted` is
// terminal (soma verify proves it), killing infinite-respawn farm spots —
// and the ore ledger can never go negative.
// ============================================================================

cell Mine {
    face {
        signal harvest(node: String, player: String) -> Map
        signal respawn_node(node: String) -> Map
        signal retire_node(node: String) -> Map
        signal ore_of(player: String) -> Int
        signal node_phase(node: String) -> String
    }

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

    state node_cycle {
        initial: ripe
        ripe -> harvested
        harvested -> ripe
        harvested -> depleted
    }

    on harvest(node: String, player: String) {
        // the yield is the transition — two harvests need two ripenings
        let r = try { transition(node, "harvested") }
        if r.error != () { return map("ok", false, "reason", "node is not ripe") }
        ore.set(player, (ore.get(player) ?? 0) + 3)
        return map("ok", true, "ore", ore.get(player))
    }

    on respawn_node(node: String) {
        let r = try { transition(node, "ripe") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true)
    }

    on retire_node(node: String) {
        let r = try { transition(node, "depleted") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true)
    }

    on ore_of(player: String) { return ore.get(player) ?? 0 }
    on node_phase(node: String) { return get_status(node) }
}

cell test MineTests {
    rules {
        assert harvest("vein-1", "jo").ok == true
        assert ore_of("jo") == 3
        // THE LAG-WINDOW DOUBLE-TAP: the second strike has no edge to take
        assert harvest("vein-1", "kim").ok == false
        assert ore_of("kim") == 0
        assert_fails transition("vein-1", "harvested")
        // after a respawn the vein yields again — exactly once
        assert respawn_node("vein-1").ok == true
        assert harvest("vein-1", "kim").ok == true
        assert ore_of("kim") == 3
        // a depleted vein is gone forever — no infinite farm spot
        assert retire_node("vein-1").ok == true
        assert_fails transition("vein-1", "ripe")
        assert harvest("vein-1", "jo").ok == false
        assert respawn_node("vein-1").ok == false
        assert_fails ore.set("jo", -1)
    }
}

What the toolchain says

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

$ soma check harvest_node.cell
✓ All checks passed.
$ soma test harvest_node.cell
test MineTests ...
  ✓ assert harvest("vein-1", "jo").ok == true
  ✓ assert ore_of("jo") == 3
  ✓ assert harvest("vein-1", "kim").ok == false
  ✓ assert ore_of("kim") == 0
  ✓ assert_fails transition("vein-1", "harvested") — raised invalid transition: harvested → harvested. Current state: 'harvested'. Valid targets: [ripe, depleted]
  ✓ assert respawn_node("vein-1").ok == true
  ✓ assert harvest("vein-1", "kim").ok == true
  ✓ assert ore_of("kim") == 3
  ✓ assert retire_node("vein-1").ok == true
  ✓ assert_fails transition("vein-1", "ripe") — raised invalid transition: depleted → ripe. Current state: 'depleted'. Valid targets: []
  ✓ assert harvest("vein-1", "jo").ok == false
  ✓ assert respawn_node("vein-1").ok == false
  ✓ assert_fails ore.set("jo", -1) — raised memory invariant violated on 'ore': ore >= 0 — rejected write of -1 (key "jo"); the slot is unchanged

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

State machine 'node_cycle': 3 states, initial 'ripe'
  States: [depleted, harvested, ripe]

  ✓ 3 states, 3 transitions
  ✓ all states reachable from 'ripe'
  ✓ terminal states: [depleted]
  ✓ 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 5 handlers structurally terminate
  ✓ refinement: handler `harvest` ⟶ {harvested}
  ✓ refinement: handler `respawn_node` ⟶ {ripe}
  ✓ refinement: handler `retire_node` ⟶ {depleted}
  · transition sources: `harvest`, `respawn_node`, `retire_node` 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)

Mine/invariants:

  ✓ invariant ore >= 0 — writer 'harvest' proven by induction (writes (ore.get(player) ?? 0) + 3)

11 passed, 0 warnings, 0 failures

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