Lottery — committed entries, a published seed, and a draw that closes forever
Public lotteries get rigged in two ways: officials slip entries in after seeing the pool (charter-school placement scandals), or they quietly "re-draw" until a favored name comes up — the 2017 HUD housing-voucher re-draws drew exactly this complaint. Both attacks die structurally here: an applicant's entry count cannot exceed 1 (memory wall), entries lock BEFORE the draw, the winner is a pure function of the locked pool and a pre-published seed, and `drawn` is a terminal state soma verify proves has no exit — there is no second draw.
A Soma program from the civic part of the verified corpus: 96 lines, cells HousingLottery, LotteryTests. It passes soma check with soma 3.2.4.
How it is built
The cell HousingLottery declares 6 signals in its face: enter_pool(applicant: String) -> Map, lock_entries() -> Map, draw(seed: Int) -> Map, pool_size() -> Int, winner_name() -> String and phase() -> String; keeps 2 memory slots: entries (Map<String, Int>, persistent and consistent) under the invariant entries >= 0 && entries <= 1 and result (Map<String, String>, persistent and consistent). Its state machine lottery starts in accepting and allows 2 transitions: accepting -> entries_locked and entries_locked -> drawn. drawn is terminal. Handlers: phase (line 39), enter_pool (line 41), pool_size (line 53), lock_entries (line 58), draw (line 66) and winner_name (line 75).
The file also holds 1 test cell (LotteryTests) with 14 assertions, run by soma test.
The source
lottery.cell
// ============================================================================
// LOTTERY — committed entries, a published seed, and a draw that closes forever
// ============================================================================
// Public lotteries get rigged in two ways: officials slip entries in after
// seeing the pool (charter-school placement scandals), or they quietly
// "re-draw" until a favored name comes up — the 2017 HUD housing-voucher
// re-draws drew exactly this complaint. Both attacks die structurally here:
// an applicant's entry count cannot exceed 1 (memory wall), entries lock
// BEFORE the draw, the winner is a pure function of the locked pool and a
// pre-published seed, and `drawn` is a terminal state soma verify proves
// has no exit — there is no second draw.
// ============================================================================
cell HousingLottery {
face {
signal enter_pool(applicant: String) -> Map
signal lock_entries() -> Map
signal draw(seed: Int) -> Map
signal pool_size() -> Int
signal winner_name() -> String
signal phase() -> String
}
memory {
// applicant -> entries. A second entry is unrepresentable.
entries: Map<String, Int> [persistent, consistent]
invariant entries >= 0 && entries <= 1
result: Map<String, String> [persistent, consistent]
}
// drawn has no outgoing edges: there is no re-draw.
state lottery {
initial: accepting
accepting -> entries_locked
entries_locked -> drawn
}
on phase() { return get_status("lottery") }
on enter_pool(applicant: String) {
if phase() != "accepting" {
return map("ok", false, "reason", "pool is {phase()}")
}
let prior = entries.get(applicant) ?? 0
let w = try { entries.set(applicant, prior + 1) }
if w.error != () {
return map("ok", false, "reason", "{applicant} already entered")
}
return map("ok", true, "pool", pool_size())
}
on pool_size() {
let names = entries.keys()
return len(names)
}
on lock_entries() {
let r = try { transition("lottery", "entries_locked") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "pool", pool_size())
}
// Deterministic: anyone can recompute the winner from the locked pool
// and the seed the commission published before entries opened.
on draw(seed: Int) {
let r = try { transition("lottery", "drawn") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
let pool = sort(entries.keys())
let idx = seed - idiv(seed, len(pool)) * len(pool)
result.set("winner", pool[idx])
return map("ok", true, "winner", pool[idx], "pool", len(pool))
}
on winner_name() { return result.get("winner") ?? "none" }
}
cell test LotteryTests {
rules {
assert enter_pool("ada").ok == true
assert enter_pool("bob").ok == true
assert enter_pool("eve").ok == true
assert enter_pool("bob").ok == false // double entry bounces
assert_fails entries.set("bob", 2) // unrepresentable
assert draw(7).ok == false // no draw before lock
assert lock_entries().ok == true
assert enter_pool("late").ok == false // pool locked
assert pool_size() == 3
assert draw(7).ok == true // 7 mod 3 = 1 -> "bob"
assert winner_name() == "bob"
assert draw(8).ok == false // NO re-draw, ever
assert_fails transition("lottery", "entries_locked")
assert_fails transition("lottery", "accepting")
}
}What the toolchain says
$ soma check lottery.cell
✓ All checks passed.$ soma test lottery.cell
test LotteryTests ...
✓ assert enter_pool("ada").ok == true
✓ assert enter_pool("bob").ok == true
✓ assert enter_pool("eve").ok == true
✓ assert enter_pool("bob").ok == false
✓ assert_fails entries.set("bob", 2) — raised memory invariant violated on 'entries': entries >= 0 && entries <= 1 — rejected write of 2 (key "bob"); the slot is unchanged
✓ assert draw(7).ok == false
✓ assert lock_entries().ok == true
✓ assert enter_pool("late").ok == false
✓ assert pool_size() == 3
✓ assert draw(7).ok == true
✓ assert winner_name() == "bob"
✓ assert draw(8).ok == false
✓ assert_fails transition("lottery", "entries_locked") — raised invalid transition: drawn → entries_locked. Current state: 'drawn'. Valid targets: []
✓ assert_fails transition("lottery", "accepting") — raised invalid transition: drawn → accepting. Current state: 'drawn'. Valid targets: []
14 tests: 14 passed, 0 failed$ soma verify lottery.cell
Verifying lottery.cell...
State machine 'lottery': 3 states, initial 'accepting'
States: [accepting, drawn, entries_locked]
✓ 3 states, 2 transitions
✓ all states reachable from 'accepting'
✓ terminal states: [drawn]
✓ 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 6 handlers structurally terminate
✓ refinement: handler `lock_entries` ⟶ {entries_locked}
✓ refinement: handler `draw` ⟶ {drawn}
· transition sources: `lock_entries`, `draw` 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)
HousingLottery/invariants:
✓ invariant entries >= 0 — writer 'enter_pool' proven by induction (writes prior + 1)
⚠ invariant entries >= 0 && entries <= 1 — runtime-checked (computed values): enter_pool → entries [entries <= 1] because `prior + 1` is only known to lie in [1, 2] — narrow it: `require (prior + 1) <= 1 else …`
10 passed, 1 warnings, 0 failures
Temporal properties for 'lottery':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OKBuiltins used
get_status, idiv, len, map, sort, transition