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

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.

Generated from soma describe on this file.

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

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

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

Builtins used

get_status, idiv, len, map, sort, transition

Source file: /corpus/civic/lottery.cell · examples/corpus/civic/lottery.cell