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