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