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