Petition — one signature per citizen, a wall in memory, not a clerk's eye
In 2022 five Michigan governor candidates were struck from the ballot after an estimated 68,000 forged or duplicate petition lines; in 2004 the Nader petition in Pennsylvania collapsed the same way. Paid circulators duplicate names because the dedup is a spreadsheet applied weeks later. Here it is structural: a citizen's line count CANNOT exceed 1 — the memory refuses the write — and the clerk's certify/reject ruling is a terminal state that
A Soma program from the civic part of the verified corpus: 100 lines, cells Petition, PetitionTests. It passes soma check with soma 3.2.4.
How it is built
The cell Petition declares 6 signals in its face: start_collection() -> Map, sign(citizen: String) -> Map, submit_to_clerk() -> Map, clerk_ruling(threshold: Int) -> Map, signature_total() -> Int and phase() -> String; keeps 1 memory slot: signed (Map<String, Int>, persistent and consistent) under the invariant signed >= 0 && signed <= 1. Its state machine drive starts in drafting and allows 4 transitions: drafting -> collecting, collecting -> submitted, submitted -> certified and submitted -> rejected. certified and rejected are terminal. Handlers: phase (line 38), start_collection (line 40), sign (line 46), signature_total (line 58), submit_to_clerk (line 65) and clerk_ruling (line 71).
The file also holds 1 test cell (PetitionTests) with 15 assertions, run by soma test.
The source
petition.cell
// ============================================================================
// PETITION — one signature per citizen, a wall in memory, not a clerk's eye
// ============================================================================
// In 2022 five Michigan governor candidates were struck from the ballot after
// an estimated 68,000 forged or duplicate petition lines; in 2004 the Nader
// petition in Pennsylvania collapsed the same way. Paid circulators duplicate
// names because the dedup is a spreadsheet applied weeks later. Here it is
// structural: a citizen's line count CANNOT exceed 1 — the memory refuses the
// write — and the clerk's certify/reject ruling is a terminal state that
// soma verify proves has no exit.
// ============================================================================
cell Petition {
face {
signal start_collection() -> Map
signal sign(citizen: String) -> Map
signal submit_to_clerk() -> Map
signal clerk_ruling(threshold: Int) -> Map
signal signature_total() -> Int
signal phase() -> String
}
memory {
// citizen -> petition lines. Two lines is unrepresentable.
signed: Map<String, Int> [persistent, consistent]
invariant signed >= 0 && signed <= 1
}
// certified and rejected have no outgoing edges: the ruling is forever.
state drive {
initial: drafting
drafting -> collecting
collecting -> submitted
submitted -> certified
submitted -> rejected
}
on phase() { return get_status("drive") }
on start_collection() {
let r = try { transition("drive", "collecting") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true)
}
on sign(citizen: String) {
if phase() != "collecting" {
return map("ok", false, "reason", "window is {phase()}, not collecting")
}
let prior = signed.get(citizen) ?? 0
let w = try { signed.set(citizen, prior + 1) }
if w.error != () {
return map("ok", false, "reason", "{citizen} already signed")
}
return map("ok", true, "total", signature_total())
}
on signature_total() {
let names = signed.keys()
let n = 0
for c in names { n = n + (signed.get(c) ?? 0) }
return n
}
on submit_to_clerk() {
let r = try { transition("drive", "submitted") }
if r.error != () { return map("ok", false, "reason", "{r.error}") }
return map("ok", true, "signatures", signature_total())
}
on clerk_ruling(threshold: Int) {
if phase() != "submitted" {
return map("ok", false, "reason", "nothing submitted to rule on")
}
if signature_total() >= threshold { transition("drive", "certified") }
if phase() == "submitted" { transition("drive", "rejected") }
return map("ok", true, "ruling", phase())
}
}
cell test PetitionTests {
rules {
assert sign("ada").ok == false // window not open yet
assert start_collection().ok == true
assert sign("ada").ok == true
assert sign("bob").ok == true
assert sign("ada").ok == false // duplicate bounces
assert_fails signed.set("ada", 2) // 2 lines: unrepresentable
assert_fails signed.set("bob", -1)
assert signature_total() == 2
assert sign("eve").ok == true
assert submit_to_clerk().ok == true
assert sign("late").ok == false // window closed
assert clerk_ruling(3).ok == true
assert phase() == "certified"
assert_fails transition("drive", "collecting") // ruling is forever
assert_fails transition("drive", "rejected")
}
}What the toolchain says
$ soma check petition.cell
✓ All checks passed.$ soma test petition.cell
test PetitionTests ...
✓ assert sign("ada").ok == false
✓ assert start_collection().ok == true
✓ assert sign("ada").ok == true
✓ assert sign("bob").ok == true
✓ assert sign("ada").ok == false
✓ assert_fails signed.set("ada", 2) — raised memory invariant violated on 'signed': signed >= 0 && signed <= 1 — rejected write of 2 (key "ada"); the slot is unchanged
✓ assert_fails signed.set("bob", -1) — raised memory invariant violated on 'signed': signed >= 0 && signed <= 1 — rejected write of -1 (key "bob"); the slot is unchanged
✓ assert signature_total() == 2
✓ assert sign("eve").ok == true
✓ assert submit_to_clerk().ok == true
✓ assert sign("late").ok == false
✓ assert clerk_ruling(3).ok == true
✓ assert phase() == "certified"
✓ assert_fails transition("drive", "collecting") — raised invalid transition: certified → collecting. Current state: 'certified'. Valid targets: []
✓ assert_fails transition("drive", "rejected") — raised invalid transition: certified → rejected. Current state: 'certified'. Valid targets: []
15 tests: 15 passed, 0 failed$ soma verify petition.cell
Verifying petition.cell...
State machine 'drive': 5 states, initial 'drafting'
States: [certified, collecting, drafting, rejected, submitted]
✓ 5 states, 4 transitions
✓ all states reachable from 'drafting'
✓ terminal states: [certified, rejected]
✓ no deadlocks
✓ liveness: every state can eventually reach a terminal state
✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 4 literal transitions, 0 dynamic)
✓ termination: all 6 handlers structurally terminate
✓ refinement: handler `start_collection` ⟶ {collecting}
✓ refinement: handler `submit_to_clerk` ⟶ {submitted}
✓ refinement: handler `clerk_ruling` ⟶ {certified [if signature_total() >= threshold], rejected [if phase() == "submitted"]}
· transition sources: `start_collection`, `submit_to_clerk`, `clerk_ruling` 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)
Petition/invariants:
✓ invariant signed >= 0 — writer 'sign' proven by induction (writes prior + 1)
⚠ invariant signed >= 0 && signed <= 1 — runtime-checked (computed values): sign → signed [signed <= 1] because `prior + 1` is only known to lie in [1, 2] — narrow it: `require (prior + 1) <= 1 else …`
11 passed, 1 warnings, 0 failures
Temporal properties for 'drive':
✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK