soma.cell

Battle turns — nobody acts twice, and the dead stay dead

The oldest cheat in networked turn-based games is the double-move: send two action packets before the server flips the turn flag (Pokemon battle simulators and play-by-mail chess servers both had it). Its cousin: keep acting after the battle ended to farm rewards from a corpse. Here the turn IS the machine — your attack is the transition that hands the turn over, so a second attack has no state to fire from. `victory` and `defeat` are terminal (soma verify proves it), and HP lives behind a 0..100 invariant: damage can never make HP negative, healing can never pass full.

A Soma program from the games_economy part of the verified corpus: 89 lines, cells Battle, BattleTests. It passes soma check with soma 3.2.4.

How it is built

The cell Battle declares 4 signals in its face: hero_attack(b: String, dmg: Int) -> Map, foe_attack(b: String, dmg: Int) -> Map, hp_of(who: String) -> Int and phase(b: String) -> String; keeps 1 memory slot: hp (Map<String, Int>, persistent and consistent) under the invariant hp >= 0 && hp <= 100. Its state machine turn starts in hero_turn and allows 4 transitions: hero_turn -> foe_turn, foe_turn -> hero_turn, hero_turn -> victory and foe_turn -> defeat. defeat and victory are terminal. Handlers: hp_of (line 35), hero_attack (line 41), foe_attack (line 53) and phase (line 65).

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

Generated from soma describe on this file.

The source

battle_turns.cell

// ============================================================================
// BATTLE TURNS — nobody acts twice, and the dead stay dead
// ============================================================================
// The oldest cheat in networked turn-based games is the double-move: send
// two action packets before the server flips the turn flag (Pokemon battle
// simulators and play-by-mail chess servers both had it). Its cousin: keep
// acting after the battle ended to farm rewards from a corpse. Here the turn
// IS the machine — your attack is the transition that hands the turn over,
// so a second attack has no state to fire from. `victory` and `defeat` are
// terminal (soma verify proves it), and HP lives behind a 0..100 invariant:
// damage can never make HP negative, healing can never pass full.
// ============================================================================

cell Battle {
    face {
        signal hero_attack(b: String, dmg: Int) -> Map
        signal foe_attack(b: String, dmg: Int) -> Map
        signal hp_of(who: String) -> Int
        signal phase(b: String) -> String
    }

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

    state turn {
        initial: hero_turn
        hero_turn -> foe_turn
        foe_turn -> hero_turn
        hero_turn -> victory
        foe_turn -> defeat
    }

    on hp_of(who: String) {
        let h = hp.get(who)
        if h == () { return 100 }
        return h
    }

    on hero_attack(b: String, dmg: Int) {
        if get_status(b) != "hero_turn" { return map("ok", false, "reason", "not the hero's turn") }
        let left = max(0, hp_of("foe") - dmg)
        hp.set("foe", left)
        if left == 0 {
            transition(b, "victory")
            return map("ok", true, "result", "victory")
        }
        transition(b, "foe_turn")
        return map("ok", true, "foe_hp", left)
    }

    on foe_attack(b: String, dmg: Int) {
        if get_status(b) != "foe_turn" { return map("ok", false, "reason", "not the foe's turn") }
        let left = max(0, hp_of("hero") - dmg)
        hp.set("hero", left)
        if left == 0 {
            transition(b, "defeat")
            return map("ok", true, "result", "defeat")
        }
        transition(b, "hero_turn")
        return map("ok", true, "hero_hp", left)
    }

    on phase(b: String) { return get_status(b) }
}

cell test BattleTests {
    rules {
        assert hero_attack("b1", 60).ok == true
        assert hp_of("foe") == 40
        // THE DOUBLE-MOVE: a second hero action has no state to fire from
        assert hero_attack("b1", 60).ok == false
        assert hp_of("foe") == 40
        assert_fails transition("b1", "victory")    // victory is the hero's exit, not the foe's
        assert foe_attack("b1", 30).ok == true
        assert hp_of("hero") == 70
        // the finishing blow: HP floors at 0 — never negative — and ends it
        assert hero_attack("b1", 999).ok == true
        assert hp_of("foe") == 0
        assert phase("b1") == "victory"
        assert_fails hp.set("foe", -1)
        // VICTORY IS TERMINAL — no post-battle actions, no reward farming
        assert hero_attack("b1", 10).ok == false
        assert foe_attack("b1", 10).ok == false
        assert_fails transition("b1", "hero_turn")
    }
}

What the toolchain says

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

$ soma check battle_turns.cell
✓ All checks passed.
$ soma test battle_turns.cell
test BattleTests ...
  ✓ assert hero_attack("b1", 60).ok == true
  ✓ assert hp_of("foe") == 40
  ✓ assert hero_attack("b1", 60).ok == false
  ✓ assert hp_of("foe") == 40
  ✓ assert_fails transition("b1", "victory") — raised invalid transition: foe_turn → victory. Current state: 'foe_turn'. Valid targets: [hero_turn, defeat]
  ✓ assert foe_attack("b1", 30).ok == true
  ✓ assert hp_of("hero") == 70
  ✓ assert hero_attack("b1", 999).ok == true
  ✓ assert hp_of("foe") == 0
  ✓ assert phase("b1") == "victory"
  ✓ assert_fails hp.set("foe", -1) — raised memory invariant violated on 'hp': hp >= 0 && hp <= 100 — rejected write of -1 (key "foe"); the slot is unchanged
  ✓ assert hero_attack("b1", 10).ok == false
  ✓ assert foe_attack("b1", 10).ok == false
  ✓ assert_fails transition("b1", "hero_turn") — raised invalid transition: victory → hero_turn. Current state: 'victory'. Valid targets: []

14 tests: 14 passed, 0 failed
$ soma verify battle_turns.cell
Verifying battle_turns.cell...

State machine 'turn': 4 states, initial 'hero_turn'
  States: [defeat, foe_turn, hero_turn, victory]

  ✓ 4 states, 4 transitions
  ✓ all states reachable from 'hero_turn'
  ✓ terminal states: [victory, defeat]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 4 literal transitions, 0 dynamic)
  ✓ termination: all 4 handlers structurally terminate
  ✓ refinement: handler `hero_attack` ⟶ {victory [if left == 0], foe_turn}
  ✓ refinement: handler `foe_attack` ⟶ {defeat [if left == 0], hero_turn}
  · transition sources: `hero_attack`, `foe_attack` 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)

Battle/invariants:

  ✓ invariant hp >= 0 — writer 'foe_attack' proven by induction (writes left)
  ✓ invariant hp >= 0 — writer 'hero_attack' proven by induction (writes left)
  ⚠ invariant hp >= 0 && hp <= 100 — runtime-checked (computed values): foe_attack → hp [hp <= 100] because `left` is only known to lie in [0, ∞) — narrow it: `require left <= 100 else …`, hero_attack → hp [hp <= 100] because `left` is only known to lie in [0, ∞) — narrow it: `require left <= 100 else …`

11 passed, 1 warnings, 0 failures

  Temporal properties for 'turn':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, max, transition

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