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

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.

Generated from soma describe on this file.

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

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

$ 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

Builtins used

get_status, map, transition

Source file: /corpus/civic/petition.cell · examples/corpus/civic/petition.cell