soma.cell

Tournament bracket — eliminated means eliminated

Online tournament platforms keep having bracket-integrity incidents: an admin "fixes" a reported result and a knocked-out player reappears in the semifinals, or a player skips a round entirely. Fighting-game brackets on early smash.gg/Challonge saw enough of this that audit logs were added. The integrity rule is structural here: ELIMINATION IS PERMANENT, CHAMPION IS FINAL, and the only way into a round is winning the previous one. and no edge skips a round.

A Soma program from the games_economy part of the verified corpus: 73 lines, cells Bracket, BracketTests. It passes soma check with soma 3.2.4.

How it is built

The cell Bracket declares 3 signals in its face: record_win(player: String) -> Map, record_loss(player: String) -> Map and standing(player: String) -> String. Its state machine progress starts in quarterfinal and allows 6 transitions: quarterfinal -> semifinal, semifinal -> final, final -> champion, quarterfinal -> eliminated, semifinal -> eliminated and final -> eliminated. champion and eliminated are terminal. Handlers: record_win (line 31), record_loss (line 42) and standing (line 48).

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

Generated from soma describe on this file.

The source

tournament_bracket.cell

// ============================================================================
// TOURNAMENT BRACKET — eliminated means eliminated
// ============================================================================
// Online tournament platforms keep having bracket-integrity incidents: an
// admin "fixes" a reported result and a knocked-out player reappears in the
// semifinals, or a player skips a round entirely. Fighting-game brackets on
// early smash.gg/Challonge saw enough of this that audit logs were added.
// The integrity rule is structural here: ELIMINATION IS PERMANENT, CHAMPION
// IS FINAL, and the only way into a round is winning the previous one.
// soma verify proves it: `eliminated` and `champion` have no outgoing edges,
// and no edge skips a round.
// ============================================================================

cell Bracket {
    face {
        signal record_win(player: String) -> Map
        signal record_loss(player: String) -> Map
        signal standing(player: String) -> String
    }

    state progress {
        initial: quarterfinal
        quarterfinal -> semifinal
        semifinal -> final
        final -> champion
        quarterfinal -> eliminated
        semifinal -> eliminated
        final -> eliminated
    }

    on record_win(player: String) {
        let here = get_status(player)
        let next = ""
        if here == "quarterfinal" { next = "semifinal" }
        if here == "semifinal" { next = "final" }
        if here == "final" { next = "champion" }
        if next == "" { return map("ok", false, "reason", "{player} is {here}: no match to win") }
        transition(player, next)
        return map("ok", true, "advanced_to", next)
    }

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

    on standing(player: String) { return get_status(player) }
}

cell test BracketTests {
    rules {
        // ada wins through every round to the title
        assert record_win("ada").ok == true
        assert standing("ada") == "semifinal"
        assert record_win("ada").ok == true
        assert record_win("ada").ok == true
        assert standing("ada") == "champion"
        // CHAMPION IS TERMINAL — no further matches, no retroactive demotion
        assert record_win("ada").ok == false
        assert record_loss("ada").ok == false
        assert_fails transition("ada", "eliminated")
        // bob loses in the quarters — elimination is permanent
        assert record_loss("bob").ok == true
        assert standing("bob") == "eliminated"
        assert_fails transition("bob", "semifinal")
        assert record_win("bob").ok == false
        // rounds cannot be skipped, even by an admin "fixing" the bracket
        assert_fails transition("cleo", "final")
        assert_fails transition("cleo", "champion")
    }
}

What the toolchain says

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

$ soma check tournament_bracket.cell
✓ All checks passed.
$ soma test tournament_bracket.cell
test BracketTests ...
  ✓ assert record_win("ada").ok == true
  ✓ assert standing("ada") == "semifinal"
  ✓ assert record_win("ada").ok == true
  ✓ assert record_win("ada").ok == true
  ✓ assert standing("ada") == "champion"
  ✓ assert record_win("ada").ok == false
  ✓ assert record_loss("ada").ok == false
  ✓ assert_fails transition("ada", "eliminated") — raised invalid transition: champion → eliminated. Current state: 'champion'. Valid targets: []
  ✓ assert record_loss("bob").ok == true
  ✓ assert standing("bob") == "eliminated"
  ✓ assert_fails transition("bob", "semifinal") — raised invalid transition: eliminated → semifinal. Current state: 'eliminated'. Valid targets: []
  ✓ assert record_win("bob").ok == false
  ✓ assert_fails transition("cleo", "final") — raised invalid transition: quarterfinal → final. Current state: 'quarterfinal'. Valid targets: [semifinal, eliminated]
  ✓ assert_fails transition("cleo", "champion") — raised invalid transition: quarterfinal → champion. Current state: 'quarterfinal'. Valid targets: [semifinal, eliminated]

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

State machine 'progress': 5 states, initial 'quarterfinal'
  States: [champion, eliminated, final, quarterfinal, semifinal]

  ✓ 5 states, 6 transitions
  ✓ all states reachable from 'quarterfinal'
  ✓ terminal states: [champion, eliminated]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ⚠ dynamic transition targets: handler `record_win` uses a dynamic (computed) transition target — the state these handlers move to is computed at run time (from input or an LLM answer), so the machine's safety is checked at run time for them, not proven
  ✓ termination: all 3 handlers structurally terminate
  ⚠ refinement (partial — dynamic targets fall back to runtime check): handler `record_win` calls transition() with a computed target — which edge it takes is checked at run time (invalid_transition), not proven; write the target as a literal state to have it verified
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `record_win` ⟶ <dynamic>
  ✓ refinement (partial — dynamic targets fall back to runtime check): handler `record_loss` ⟶ {eliminated}
  · transition sources: `record_loss` calls 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)

8 passed, 2 warnings, 0 failures

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