soma.cell

Emergency sunset — extraordinary powers that cannot become ordinary

Egypt declared a state of emergency in 1981 after Sadat's assassination. It was "temporarily" renewed, again and again, for THIRTY-ONE YEARS — a whole generation governed under exception. The pattern is universal enough that modern emergency statutes (and the post-2020 reform wave in U.S. states) all converge on the same two teeth: an emergency expires BY ITSELF unless the legislature acts, and the executive cannot renew it indefinitely on its own signature. Both teeth are structural here. A declaration must be confirmed by the legislature before any power is exercised; `expired` is terminal — soma verify proves a lapsed emergency has no path back to life (you must declare a NEW one, in public, with a new confirmation). And the renewal counter carries `invariant <= 2`: the third renewal of the same declaration is a write the statute book refuses.

A Soma program from the governance part of the verified corpus: 136 lines, cells EmergencyAct, SunsetTests. It passes soma check with soma 3.2.4.

How it is built

The cell EmergencyAct declares 6 signals in its face: declare(em: String) -> Map, confirm(em: String, ayes: Int, nays: Int) -> Map, exercise_power(em: String, order: String) -> Map, renew(em: String) -> Map, expire(em: String) -> Map and renewals_of(em: String) -> Int; keeps 2 memory slots: renewals (Map<String, Int>, persistent and consistent) under the invariant renewals >= 0 && renewals <= 2 and orders (Map<String, String>, persistent and consistent). Its state machine emergency starts in declared and allows 4 transitions: declared -> confirmed, confirmed -> active, active -> expired and declared -> expired. expired is terminal. Handlers: declare (line 51), confirm (line 56), exercise_power (line 68), renew (line 77), expire (line 91) and renewals_of (line 97).

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

Generated from soma describe on this file.

The source

emergency_sunset.cell

// ============================================================================
// EMERGENCY SUNSET — extraordinary powers that cannot become ordinary
// ============================================================================
//
// Egypt declared a state of emergency in 1981 after Sadat's
// assassination. It was "temporarily" renewed, again and again, for
// THIRTY-ONE YEARS — a whole generation governed under exception. The
// pattern is universal enough that modern emergency statutes (and the
// post-2020 reform wave in U.S. states) all converge on the same two
// teeth: an emergency expires BY ITSELF unless the legislature acts,
// and the executive cannot renew it indefinitely on its own signature.
//
// Both teeth are structural here. A declaration must be confirmed by
// the legislature before any power is exercised; `expired` is terminal
// — soma verify proves a lapsed emergency has no path back to life
// (you must declare a NEW one, in public, with a new confirmation).
// And the renewal counter carries `invariant <= 2`: the third renewal
// of the same declaration is a write the statute book refuses.
// ============================================================================

cell EmergencyAct {
    face {
        signal declare(em: String) -> Map
        signal confirm(em: String, ayes: Int, nays: Int) -> Map
        signal exercise_power(em: String, order: String) -> Map
        signal renew(em: String) -> Map
        signal expire(em: String) -> Map
        signal renewals_of(em: String) -> Int
    }

    memory {
        // declaration -> times renewed. Two renewals, then the machine
        // forces a fresh public declaration. Egypt-1981 is a 31 the
        // statute book cannot hold.
        renewals: Map<String, Int> [persistent, consistent]
        invariant renewals >= 0 && renewals <= 2

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

    // declared -> confirmed -> active; expired is TERMINAL.
    // No edge runs from expired anywhere: resurrection is impossible.
    state emergency {
        initial: declared
        declared -> confirmed
        confirmed -> active
        active -> expired
        declared -> expired
    }

    on declare(em: String) {
        return map("ok", true, "em", em, "state", get_status(em))
    }

    // the legislature, not the palace, turns the key — simple majority
    on confirm(em: String, ayes: Int, nays: Int) {
        if ayes <= nays {
            let r = try { transition(em, "expired") }
            if r.error != () { return map("ok", false, "reason", "{r.error}") }
            return map("ok", false, "reason", "legislature refused: {ayes}-{nays}; declaration dies")
        }
        let c = try { transition(em, "confirmed") }
        if c.error != () { return map("ok", false, "reason", "{c.error}") }
        transition(em, "active")
        return map("ok", true, "state", "active")
    }

    on exercise_power(em: String, order: String) {
        if get_status(em) != "active" {
            let s = get_status(em)
            return map("ok", false, "reason", "no emergency power without an ACTIVE emergency ({s})")
        }
        orders.set("{em}:{order}", order)
        return map("ok", true, "order", order)
    }

    on renew(em: String) {
        if get_status(em) != "active" {
            let s = get_status(em)
            return map("ok", false, "reason", "only an active emergency renews ({s})")
        }
        // THE WALL: renewal number three does not exist
        let w = try { renewals.set(em, (renewals.get(em) ?? 0) + 1) }
        if w.error != () {
            return map("ok", false, "reason",
                "{em} has been renewed twice; declare a NEW emergency or stand down")
        }
        return map("ok", true, "renewals", renewals.get(em))
    }

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

    on renewals_of(em: String) {
        return renewals.get(em) ?? 0
    }
}

cell test SunsetTests {
    rules {
        // a bare declaration confers NOTHING — the legislature must act
        assert declare("em-1981").ok == true
        assert exercise_power("em-1981", "curfew").ok == false
        assert renew("em-1981").ok == false
        assert_fails transition("em-1981", "active")       // no skipping confirmation

        // confirmed by the chamber: powers flow
        assert confirm("em-1981", 310, 90).ok == true
        assert exercise_power("em-1981", "curfew").ok == true

        // two renewals pass; the third is a value the book cannot hold
        assert renew("em-1981").renewals == 1
        assert renew("em-1981").renewals == 2
        assert renew("em-1981").ok == false
        assert_fails renewals.set("em-1981", 3)
        assert renewals_of("em-1981") == 2

        // sunset: expired is terminal — no path back, powers go dark
        assert expire("em-1981").ok == true
        assert exercise_power("em-1981", "censorship").ok == false
        assert renew("em-1981").ok == false
        assert_fails transition("em-1981", "active")
        assert_fails transition("em-1981", "confirmed")
        assert_fails transition("em-1981", "declared")

        // a declaration the chamber votes DOWN dies on the spot
        assert declare("em-2").ok == true
        assert confirm("em-2", 100, 200).ok == false
        assert get_status("em-2") == "expired"
        assert exercise_power("em-2", "anything").ok == false
    }
}

What the toolchain says

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

$ soma check emergency_sunset.cell
✓ All checks passed.
$ soma test emergency_sunset.cell
test SunsetTests ...
  ✓ assert declare("em-1981").ok == true
  ✓ assert exercise_power("em-1981", "curfew").ok == false
  ✓ assert renew("em-1981").ok == false
  ✓ assert_fails transition("em-1981", "active") — raised invalid transition: declared → active. Current state: 'declared'. Valid targets: [confirmed, expired]
  ✓ assert confirm("em-1981", 310, 90).ok == true
  ✓ assert exercise_power("em-1981", "curfew").ok == true
  ✓ assert renew("em-1981").renewals == 1
  ✓ assert renew("em-1981").renewals == 2
  ✓ assert renew("em-1981").ok == false
  ✓ assert_fails renewals.set("em-1981", 3) — raised memory invariant violated on 'renewals': renewals >= 0 && renewals <= 2 — rejected write of 3 (key "em-1981"); the slot is unchanged
  ✓ assert renewals_of("em-1981") == 2
  ✓ assert expire("em-1981").ok == true
  ✓ assert exercise_power("em-1981", "censorship").ok == false
  ✓ assert renew("em-1981").ok == false
  ✓ assert_fails transition("em-1981", "active") — raised invalid transition: expired → active. Current state: 'expired'. Valid targets: []
  ✓ assert_fails transition("em-1981", "confirmed") — raised invalid transition: expired → confirmed. Current state: 'expired'. Valid targets: []
  ✓ assert_fails transition("em-1981", "declared") — raised invalid transition: expired → declared. Current state: 'expired'. Valid targets: []
  ✓ assert declare("em-2").ok == true
  ✓ assert confirm("em-2", 100, 200).ok == false
  ✓ assert get_status("em-2") == "expired"
  ✓ assert exercise_power("em-2", "anything").ok == false

21 tests: 21 passed, 0 failed
$ soma verify emergency_sunset.cell
Verifying emergency_sunset.cell...

State machine 'emergency': 4 states, initial 'declared'
  States: [active, confirmed, declared, expired]

  ✓ 4 states, 4 transitions
  ✓ all states reachable from 'declared'
  ✓ terminal states: [expired]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (2 handlers, 4 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `confirm` ⟶ {expired [if ayes <= nays], confirmed, active}
  ✓ refinement: handler `expire` ⟶ {expired}
  · transition sources: `confirm`, `expire` 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)

EmergencyAct/invariants:

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

10 passed, 1 warnings, 0 failures

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