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

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.

Generated from soma describe on this file.

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

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

$ 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

Builtins used

get_status, map, transition

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