soma.cell

Term limits — the third term is not forbidden, it is unrepresentable

In 2008, New York's City Council — at Mayor Bloomberg's urging — voted 29-22 to extend its own term limits so the sitting mayor could run again, overriding two public referenda in which New Yorkers had twice voted for a two-term cap. It was legal precisely because the limit lived in an ordinary statute the limited officials themselves could amend. The U.S. answer to FDR's four terms was different: the 22nd Amendment put the cap somewhere no incumbent can reach. This module is the 22nd-Amendment version. The terms ledger carries `invariant terms <= 2` — certifying a third term for the same person is a WRITE THE MEMORY REFUSES, and there is no handler anywhere that can loosen an invariant at runtime. Each term also walks a machine whose `vacated` state is terminal: an ended term cannot be revived as a sneaky continuation of itself.

A Soma program from the governance part of the verified corpus: 128 lines, cells TermRegistry, TermLimitTests. It passes soma check with soma 3.2.4.

How it is built

The cell TermRegistry declares 5 signals in its face: nominate(person: String, term_id: String) -> Map, certify_win(person: String, term_id: String) -> Map, inaugurate(term_id: String) -> Map, vacate(term_id: String) -> Map and terms_served(person: String) -> Int; keeps 2 memory slots: terms (Map<String, Int>, persistent and consistent) under the invariant terms >= 0 && terms <= 2 and winners (Map<String, String>, persistent and consistent). Its state machine term starts in open_seat and allows 5 transitions: open_seat -> nominated, nominated -> won, won -> sworn_in, sworn_in -> vacated and nominated -> lost. lost and vacated are terminal. Handlers: nominate (line 50), certify_win (line 60), inaugurate (line 77), vacate (line 83) and terms_served (line 89).

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

Generated from soma describe on this file.

The source

term_limits.cell

// ============================================================================
// TERM LIMITS — the third term is not forbidden, it is unrepresentable
// ============================================================================
//
// In 2008, New York's City Council — at Mayor Bloomberg's urging —
// voted 29-22 to extend its own term limits so the sitting mayor could
// run again, overriding two public referenda in which New Yorkers had
// twice voted for a two-term cap. It was legal precisely because the
// limit lived in an ordinary statute the limited officials themselves
// could amend. The U.S. answer to FDR's four terms was different: the
// 22nd Amendment put the cap somewhere no incumbent can reach.
//
// This module is the 22nd-Amendment version. The terms ledger carries
// `invariant terms <= 2` — certifying a third term for the same person
// is a WRITE THE MEMORY REFUSES, and there is no handler anywhere that
// can loosen an invariant at runtime. Each term also walks a machine
// whose `vacated` state is terminal: an ended term cannot be revived
// as a sneaky continuation of itself.
// ============================================================================

cell TermRegistry {
    face {
        signal nominate(person: String, term_id: String) -> Map
        signal certify_win(person: String, term_id: String) -> Map
        signal inaugurate(term_id: String) -> Map
        signal vacate(term_id: String) -> Map
        signal terms_served(person: String) -> Int
    }

    memory {
        // person -> terms certified, lifetime. 3 does not exist.
        terms: Map<String, Int> [persistent, consistent]
        invariant terms >= 0 && terms <= 2

        winners: Map<String, String> [persistent, consistent]
    }

    // nominated -> won -> sworn_in -> vacated (TERMINAL).
    // The office is re-filled only through a NEW term id — a new
    // nomination, a new election, a fresh certification against the cap.
    state term {
        initial: open_seat
        open_seat -> nominated
        nominated -> won
        won -> sworn_in
        sworn_in -> vacated
        nominated -> lost
    }

    on nominate(person: String, term_id: String) {
        // the ballot gate: someone already at the cap cannot even run
        if (terms.get(person) ?? 0) >= 2 {
            return map("ok", false, "reason", "{person} has served 2 terms; the ballot is closed")
        }
        let r = try { transition(term_id, "nominated") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "candidate", person)
    }

    on certify_win(person: String, term_id: String) {
        if get_status(term_id) != "nominated" {
            let s = get_status(term_id)
            return map("ok", false, "reason", "nothing to certify from {s}")
        }
        // THE WALL: even if the ballot gate above were repealed by a
        // friendly council, the third certification is a write of 3 —
        // and the ledger refuses it.
        let w = try { terms.set(person, (terms.get(person) ?? 0) + 1) }
        if w.error != () {
            return map("ok", false, "reason", "22nd Amendment: no third term for {person}")
        }
        transition(term_id, "won")
        winners.set(term_id, person)
        return map("ok", true, "person", person, "terms", terms.get(person))
    }

    on inaugurate(term_id: String) {
        let r = try { transition(term_id, "sworn_in") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "holder", winners.get(term_id))
    }

    on vacate(term_id: String) {
        let r = try { transition(term_id, "vacated") }
        if r.error != () { return map("ok", false, "reason", "{r.error}") }
        return map("ok", true, "state", "vacated")
    }

    on terms_served(person: String) {
        return terms.get(person) ?? 0
    }
}

cell test TermLimitTests {
    rules {
        // term one: nominate, win, swear in, and eventually vacate
        assert nominate("bloomberg", "t2002").ok == true
        assert certify_win("bloomberg", "t2002").terms == 1
        assert inaugurate("t2002").holder == "bloomberg"
        assert vacate("t2002").ok == true

        // a vacated term is dead — no continuation-in-place
        assert_fails transition("t2002", "sworn_in")
        assert_fails transition("t2002", "won")

        // term two, through a brand-new term id
        assert nominate("bloomberg", "t2005").ok == true
        assert certify_win("bloomberg", "t2005").terms == 2
        assert inaugurate("t2005").ok == true
        assert vacate("t2005").ok == true

        // THE 2008 MOVE: the third run. The ballot gate refuses —
        // and even a "council override" of that gate hits the memory.
        assert nominate("bloomberg", "t2009").ok == false
        assert_fails terms.set("bloomberg", 3)
        assert terms_served("bloomberg") == 2

        // a rigged certification with no election behind it also dies:
        // t2009 was never nominated, so there is nothing to certify
        assert certify_win("bloomberg", "t2009").ok == false
        assert_fails transition("t2009", "won")

        // the office itself stays alive — for somebody else
        assert nominate("thompson", "t2009").ok == true
        assert certify_win("thompson", "t2009").terms == 1
    }
}

What the toolchain says

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

$ soma check term_limits.cell
✓ All checks passed.
$ soma test term_limits.cell
test TermLimitTests ...
  ✓ assert nominate("bloomberg", "t2002").ok == true
  ✓ assert certify_win("bloomberg", "t2002").terms == 1
  ✓ assert inaugurate("t2002").holder == "bloomberg"
  ✓ assert vacate("t2002").ok == true
  ✓ assert_fails transition("t2002", "sworn_in") — raised invalid transition: vacated → sworn_in. Current state: 'vacated'. Valid targets: []
  ✓ assert_fails transition("t2002", "won") — raised invalid transition: vacated → won. Current state: 'vacated'. Valid targets: []
  ✓ assert nominate("bloomberg", "t2005").ok == true
  ✓ assert certify_win("bloomberg", "t2005").terms == 2
  ✓ assert inaugurate("t2005").ok == true
  ✓ assert vacate("t2005").ok == true
  ✓ assert nominate("bloomberg", "t2009").ok == false
  ✓ assert_fails terms.set("bloomberg", 3) — raised memory invariant violated on 'terms': terms >= 0 && terms <= 2 — rejected write of 3 (key "bloomberg"); the slot is unchanged
  ✓ assert terms_served("bloomberg") == 2
  ✓ assert certify_win("bloomberg", "t2009").ok == false
  ✓ assert_fails transition("t2009", "won") — raised invalid transition: open_seat → won. Current state: 'open_seat'. Valid targets: [nominated]
  ✓ assert nominate("thompson", "t2009").ok == true
  ✓ assert certify_win("thompson", "t2009").terms == 1

17 tests: 17 passed, 0 failed
$ soma verify term_limits.cell
Verifying term_limits.cell...

State machine 'term': 6 states, initial 'open_seat'
  States: [lost, nominated, open_seat, sworn_in, vacated, won]

  ✓ 6 states, 5 transitions
  ✓ all states reachable from 'open_seat'
  ✓ terminal states: [vacated, lost]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (4 handlers, 4 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ⚠ refinement: declared transition `nominated → lost` is never reached by any handler — spec may be aspirational or stale
  ✓ refinement: handler `nominate` ⟶ {nominated}
  ✓ refinement: handler `certify_win` ⟶ {nominated → won}
  ✓ refinement: handler `inaugurate` ⟶ {sworn_in}
  ✓ refinement: handler `vacate` ⟶ {vacated}
  · transition sources: `nominate`, `inaugurate`, `vacate` 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)

TermRegistry/invariants:

  ✓ invariant terms >= 0 — writer 'certify_win' proven by induction (writes (terms.get(person) ?? 0) + 1)
  ⚠ invariant terms >= 0 && terms <= 2 — runtime-checked (computed values): certify_win → terms [terms <= 2] because `terms` has no known range

12 passed, 2 warnings, 0 failures

  Temporal properties for 'term':
  ✓ 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/term_limits.cell · examples/corpus/governance/term_limits.cell