Battle pass — every tier reward claimed exactly once
Battle-pass duplication exploits reduce to two writes: a claim counter going past 1 (claim, crash the client mid-grant, claim again — the "crash-and-reclaim" farmed in several seasons of big battle royales), or tier progress jumping the track via a modified client. Here each (player, tier) claim is walled at <= 1 BY THE MEMORY, tier progress is capped at 50 by an invariant, and the season itself is a machine whose `closed` state is terminal — soma verify proves that when a season ends, the books are shut for good.
A Soma program from the games_economy part of the verified corpus: 92 lines, cells BattlePass, PassTests. It passes soma check with soma 3.2.4.
How it is built
The cell BattlePass declares 5 signals in its face: open_pass() -> Map, close_pass() -> Map, advance_tier(player: String) -> Map, claim_tier(player: String, tier_n: Int) -> Map and tier_of(player: String) -> Int; keeps 2 memory slots: tier (Map<String, Int>, persistent and consistent) under the invariant tier >= 0 && tier <= 50 and claims (Map<String, Int>, persistent and consistent) under the invariant claims >= 0 && claims <= 1. Its state machine pass starts in dormant and allows 2 transitions: dormant -> live and live -> closed. closed is terminal. Handlers: open_pass (line 36), close_pass (line 42), advance_tier (line 48), claim_tier (line 55) and tier_of (line 65).
The file also holds 1 test cell (PassTests) with 15 assertions, run by soma test.
The source
battle_pass.cell
// ============================================================================
// BATTLE PASS — every tier reward claimed exactly once
// ============================================================================
// Battle-pass duplication exploits reduce to two writes: a claim counter
// going past 1 (claim, crash the client mid-grant, claim again — the
// "crash-and-reclaim" farmed in several seasons of big battle royales), or
// tier progress jumping the track via a modified client. Here each
// (player, tier) claim is walled at <= 1 BY THE MEMORY, tier progress is
// capped at 50 by an invariant, and the season itself is a machine whose
// `closed` state is terminal — soma verify proves that when a season ends,
// the books are shut for good.
// ============================================================================
cell BattlePass {
face {
signal open_pass() -> Map
signal close_pass() -> Map
signal advance_tier(player: String) -> Map
signal claim_tier(player: String, tier_n: Int) -> Map
signal tier_of(player: String) -> Int
}
memory {
tier: Map<String, Int> [persistent, consistent]
invariant tier >= 0 && tier <= 50
claims: Map<String, Int> [persistent, consistent]
invariant claims >= 0 && claims <= 1
}
state pass {
initial: dormant
dormant -> live
live -> closed
}
on open_pass() {
let r = try { transition("pass", "live") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true)
}
on close_pass() {
let r = try { transition("pass", "closed") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true)
}
on advance_tier(player: String) {
if get_status("pass") != "live" { return map("ok", false, "reason", "pass is not live") }
let w = try { tier.set(player, (tier.get(player) ?? 0) + 1) }
if w.error != () { return map("ok", false, "reason", "already at tier 50") }
return map("ok", true, "tier", tier.get(player))
}
on claim_tier(player: String, tier_n: Int) {
if get_status("pass") != "live" { return map("ok", false, "reason", "pass is not live") }
if (tier.get(player) ?? 0) < tier_n { return map("ok", false, "reason", "tier {tier_n} not reached") }
let key = "{player}#{tier_n}"
// THE WALL: a second claim writes 2 into a <= 1 slot — refused
let w = try { claims.set(key, (claims.get(key) ?? 0) + 1) }
if w.error != () { return map("ok", false, "reason", "tier {tier_n} already claimed") }
return map("ok", true, "claimed", tier_n)
}
on tier_of(player: String) { return tier.get(player) ?? 0 }
}
cell test PassTests {
rules {
// nothing moves before the season opens
assert advance_tier("vic").ok == false
assert open_pass().ok == true
assert advance_tier("vic").ok == true
assert advance_tier("vic").ok == true
assert tier_of("vic") == 2
// cannot claim a tier you have not reached
assert claim_tier("vic", 3).ok == false
assert claim_tier("vic", 2).ok == true
// THE CRASH-AND-RECLAIM: the second claim is an unstorable write
assert claim_tier("vic", 2).ok == false
assert_fails claims.set("vic#2", 2)
// tier progress cannot be injected past the cap
assert_fails tier.set("vic", 51)
// a closed season is closed forever
assert close_pass().ok == true
assert claim_tier("vic", 1).ok == false
assert advance_tier("vic").ok == false
assert_fails transition("pass", "live")
assert_fails transition("pass", "dormant")
}
}What the toolchain says
$ soma check battle_pass.cell
✓ All checks passed.$ soma test battle_pass.cell
test PassTests ...
✓ assert advance_tier("vic").ok == false
✓ assert open_pass().ok == true
✓ assert advance_tier("vic").ok == true
✓ assert advance_tier("vic").ok == true
✓ assert tier_of("vic") == 2
✓ assert claim_tier("vic", 3).ok == false
✓ assert claim_tier("vic", 2).ok == true
✓ assert claim_tier("vic", 2).ok == false
✓ assert_fails claims.set("vic#2", 2) — raised memory invariant violated on 'claims': claims >= 0 && claims <= 1 — rejected write of 2 (key "vic#2"); the slot is unchanged
✓ assert_fails tier.set("vic", 51) — raised memory invariant violated on 'tier': tier >= 0 && tier <= 50 — rejected write of 51 (key "vic"); the slot is unchanged
✓ assert close_pass().ok == true
✓ assert claim_tier("vic", 1).ok == false
✓ assert advance_tier("vic").ok == false
✓ assert_fails transition("pass", "live") — raised invalid transition: closed → live. Current state: 'closed'. Valid targets: []
✓ assert_fails transition("pass", "dormant") — raised invalid transition: closed → dormant. Current state: 'closed'. Valid targets: []
15 tests: 15 passed, 0 failed$ soma verify battle_pass.cell
Verifying battle_pass.cell...
State machine 'pass': 3 states, initial 'dormant'
States: [closed, dormant, live]
✓ 3 states, 2 transitions
✓ all states reachable from 'dormant'
✓ terminal states: [closed]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 2 literal transitions, 0 dynamic)
✓ termination: all 5 handlers structurally terminate
✓ refinement: handler `open_pass` ⟶ {live}
✓ refinement: handler `close_pass` ⟶ {closed}
· transition sources: `open_pass`, `close_pass` 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)
BattlePass/invariants:
✓ invariant tier >= 0 — writer 'advance_tier' proven by induction (writes (tier.get(player) ?? 0) + 1)
⚠ invariant tier >= 0 && tier <= 50 — runtime-checked (computed values): advance_tier → tier [tier <= 50] because `tier` has no known range
✓ invariant claims >= 0 — writer 'claim_tier' proven by induction (writes (claims.get(key) ?? 0) + 1)
⚠ invariant claims >= 0 && claims <= 1 — runtime-checked (computed values): claim_tier → claims [claims <= 1] because `claims` has no known range; `key` = "{player}#{tier_n}" — not bounded
11 passed, 2 warnings, 0 failures
Temporal properties for 'pass':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK