soma.cell

Board motion — Robert's Rules where "no quorum, no vote" is structural

Quorum is the oldest anti-capture device in deliberative bodies: a minority that shows up early cannot bind the whole board. It matters enough that in 2011 fourteen Wisconsin state senators fled to Illinois for three weeks SOLELY to deny the chamber a quorum — denying quorum was the only brake left. Corporate law is harsher: board action taken without quorum is void, not voidable. Courts unwind the merger. Here the brake is not a clerk remembering to count the room. The motion lifecycle (Robert's Rules: moved -> seconded -> voted) is a state machine soma verify proves, `passed`/`failed` are terminal so a resolved motion can never be re-voted, and one-director-one-ballot is a MEMORY invariant — the second ballot is refused at the write.

A Soma program from the governance part of the verified corpus: 155 lines, cells Boardroom, MotionTests. It passes soma check with soma 3.2.4.

How it is built

The cell Boardroom declares 7 signals in its face: check_in(director: String) -> Map, present_count() -> Int, move_motion(id: String, mover: String) -> Map, second_motion(id: String, seconder: String) -> Map, call_vote(id: String) -> Map, cast_ballot(id: String, director: String, aye: Bool) -> Map and resolve(id: String) -> Map; keeps 5 memory slots: attendance (Map<String, Int>, persistent and consistent) under the invariant attendance >= 0 && attendance <= 1, ballots (Map<String, Int>, persistent and consistent) under the invariant ballots >= 0 && ballots <= 1, movers (Map<String, String>, persistent and consistent), ayes (Map<String, Int>, persistent and consistent) under the invariant ayes >= 0 and nays (Map<String, Int>, persistent and consistent) under the invariant nays >= 0. Its state machine motion starts in drafted and allows 5 transitions: drafted -> moved, moved -> seconded, seconded -> voting, voting -> passed and voting -> failed. failed and passed are terminal. Handlers: check_in (line 57), present_count (line 62), move_motion (line 68), second_motion (line 75), call_vote (line 85), cast_ballot (line 95) and resolve (line 112).

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

Generated from soma describe on this file.

The source

board_motion.cell

// ============================================================================
// BOARD MOTION — Robert's Rules where "no quorum, no vote" is structural
// ============================================================================
//
// Quorum is the oldest anti-capture device in deliberative bodies: a
// minority that shows up early cannot bind the whole board. It matters
// enough that in 2011 fourteen Wisconsin state senators fled to Illinois
// for three weeks SOLELY to deny the chamber a quorum — denying quorum
// was the only brake left. Corporate law is harsher: board action taken
// without quorum is void, not voidable. Courts unwind the merger.
//
// Here the brake is not a clerk remembering to count the room. The
// motion lifecycle (Robert's Rules: moved -> seconded -> voted) is a
// state machine soma verify proves, `passed`/`failed` are terminal so a
// resolved motion can never be re-voted, and one-director-one-ballot is
// a MEMORY invariant — the second ballot is refused at the write.
// ============================================================================

cell Boardroom {
    face {
        signal check_in(director: String) -> Map
        signal present_count() -> Int
        signal move_motion(id: String, mover: String) -> Map
        signal second_motion(id: String, seconder: String) -> Map
        signal call_vote(id: String) -> Map
        signal cast_ballot(id: String, director: String, aye: Bool) -> Map
        signal resolve(id: String) -> Map
    }

    memory {
        // in the room: 0 or 1 — a director cannot be "present twice"
        attendance: Map<String, Int> [persistent, consistent]
        invariant attendance >= 0 && attendance <= 1

        // one director, one ballot per motion — enforced by the MEMORY
        ballots: Map<String, Int> [persistent, consistent]
        invariant ballots >= 0 && ballots <= 1

        movers: Map<String, String> [persistent, consistent]
        ayes: Map<String, Int> [persistent, consistent]
        invariant ayes >= 0
        nays: Map<String, Int> [persistent, consistent]
        invariant nays >= 0
    }

    // Robert's Rules: nothing is debated or voted until moved AND
    // seconded. passed/failed are TERMINAL: a resolved motion is history.
    state motion {
        initial: drafted
        drafted -> moved
        moved -> seconded
        seconded -> voting
        voting -> passed
        voting -> failed
    }

    on check_in(director: String) {
        attendance.set(director, 1)
        return map("ok", true, "present", present_count())
    }

    on present_count() {
        let n = 0
        for d in attendance.keys() { n = n + (attendance.get(d) ?? 0) }
        return n
    }

    on move_motion(id: String, mover: String) {
        let r = try { transition(id, "moved") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        movers.set(id, mover)
        return map("ok", true, "state", get_status(id))
    }

    on second_motion(id: String, seconder: String) {
        if movers.get(id) == seconder {
            return map("ok", false, "reason", "a motion cannot second itself: {seconder} moved it")
        }
        let r = try { transition(id, "seconded") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", get_status(id))
    }

    // THE QUORUM GUARD: a 5-seat board needs 3 in the room to open a vote
    on call_vote(id: String) {
        if present_count() < 3 {
            let p = present_count()
            return map("ok", false, "reason", "no quorum: {p} of 5 present, need 3")
        }
        let r = try { transition(id, "voting") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "voting")
    }

    on cast_ballot(id: String, director: String, aye: Bool) {
        if get_status(id) != "voting" {
            let s = get_status(id)
            return map("ok", false, "reason", "motion {id} is not open for voting ({s})")
        }
        if (attendance.get(director) ?? 0) != 1 {
            return map("ok", false, "reason", "{director} is not in the room")
        }
        // THE WALL: a second ballot writes 2 and the memory refuses it
        let k = "{id}:{director}"
        let w = try { ballots.set(k, (ballots.get(k) ?? 0) + 1) }
        if w.error != () { return map("ok", false, "reason", "{director} already voted on {id}") }
        if aye { ayes.set(id, (ayes.get(id) ?? 0) + 1) }
        if !aye { nays.set(id, (nays.get(id) ?? 0) + 1) }
        return map("ok", true, "director", director)
    }

    on resolve(id: String) {
        if get_status(id) != "voting" { return map("ok", false, "reason", "not in voting") }
        let a = ayes.get(id) ?? 0
        let n = nays.get(id) ?? 0
        if a > n { transition(id, "passed") }
        if a <= n { transition(id, "failed") }
        return map("ok", true, "state", get_status(id), "ayes", a, "nays", n)
    }
}

cell test MotionTests {
    rules {
        // moved -> seconded, and a mover cannot second their own motion
        assert move_motion("m1", "ada").ok == true
        assert second_motion("m1", "ada").ok == false
        assert second_motion("m1", "bob").ok == true

        // the vote cannot open without quorum (0 of 5 present)
        assert call_vote("m1").ok == false
        assert check_in("ada").ok == true
        assert check_in("bob").ok == true
        assert call_vote("m1").ok == false          // 2 of 5: still short
        assert check_in("cyd").ok == true
        assert call_vote("m1").ok == true           // 3 of 5: quorum

        // a drafted motion cannot jump straight to voting — no edge exists
        assert_fails transition("m2", "voting")
        assert_fails transition("m2", "passed")

        // one director, one ballot: the memory wall
        assert cast_ballot("m1", "ada", true).ok == true
        assert cast_ballot("m1", "ada", false).ok == false
        assert_fails ballots.set("m1:ada", 2)
        assert cast_ballot("m1", "bob", true).ok == true
        assert cast_ballot("m1", "zed", true).ok == false   // not in the room

        // resolution is terminal: a passed motion can never be re-voted
        assert resolve("m1").state == "passed"
        assert_fails transition("m1", "voting")
        assert_fails transition("m1", "failed")
        assert cast_ballot("m1", "cyd", true).ok == false
    }
}

What the toolchain says

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

$ soma check board_motion.cell
✓ All checks passed.
$ soma test board_motion.cell
test MotionTests ...
  ✓ assert move_motion("m1", "ada").ok == true
  ✓ assert second_motion("m1", "ada").ok == false
  ✓ assert second_motion("m1", "bob").ok == true
  ✓ assert call_vote("m1").ok == false
  ✓ assert check_in("ada").ok == true
  ✓ assert check_in("bob").ok == true
  ✓ assert call_vote("m1").ok == false
  ✓ assert check_in("cyd").ok == true
  ✓ assert call_vote("m1").ok == true
  ✓ assert_fails transition("m2", "voting") — raised invalid transition: drafted → voting. Current state: 'drafted'. Valid targets: [moved]
  ✓ assert_fails transition("m2", "passed") — raised invalid transition: drafted → passed. Current state: 'drafted'. Valid targets: [moved]
  ✓ assert cast_ballot("m1", "ada", true).ok == true
  ✓ assert cast_ballot("m1", "ada", false).ok == false
  ✓ assert_fails ballots.set("m1:ada", 2) — raised memory invariant violated on 'ballots': ballots >= 0 && ballots <= 1 — rejected write of 2 (key "m1:ada"); the slot is unchanged
  ✓ assert cast_ballot("m1", "bob", true).ok == true
  ✓ assert cast_ballot("m1", "zed", true).ok == false
  ✓ assert resolve("m1").state == "passed"
  ✓ assert_fails transition("m1", "voting") — raised invalid transition: passed → voting. Current state: 'passed'. Valid targets: []
  ✓ assert_fails transition("m1", "failed") — raised invalid transition: passed → failed. Current state: 'passed'. Valid targets: []
  ✓ assert cast_ballot("m1", "cyd", true).ok == false

20 tests: 20 passed, 0 failed
$ soma verify board_motion.cell
Verifying board_motion.cell...

State machine 'motion': 6 states, initial 'drafted'
  States: [drafted, failed, moved, passed, seconded, voting]

  ✓ 6 states, 5 transitions
  ✓ all states reachable from 'drafted'
  ✓ terminal states: [passed, failed]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 5 literal transitions, 0 dynamic)
  ✓ termination: all 7 handlers structurally terminate
  ✓ refinement: handler `move_motion` ⟶ {moved}
  ✓ refinement: handler `second_motion` ⟶ {seconded}
  ✓ refinement: handler `call_vote` ⟶ {voting}
  ✓ refinement: handler `resolve` ⟶ {voting → passed [if a > n], voting → failed [if a <= n]}
  · transition sources: `move_motion`, `second_motion`, `call_vote` 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)

Boardroom/invariants:

  ✓ invariant attendance >= 0 && attendance <= 1 — writer 'check_in' proven (writes 1)
  ✓ invariant ballots >= 0 — writer 'cast_ballot' proven by induction (writes (ballots.get(k) ?? 0) + 1)
  ⚠ invariant ballots >= 0 && ballots <= 1 — runtime-checked (computed values): cast_ballot → ballots [ballots <= 1] because `ballots` has no known range; `k` = "{id}:{director}" — not bounded
  ✓ invariant ayes >= 0 — writer 'cast_ballot' proven by induction (writes (ayes.get(id) ?? 0) + 1)
  ✓ invariant nays >= 0 — writer 'cast_ballot' proven by induction (writes (nays.get(id) ?? 0) + 1)

15 passed, 1 warnings, 0 failures

  Temporal properties for 'motion':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, transition

Source file: /corpus/governance/board_motion.cell · examples/corpus/governance/board_motion.cell