soma.cell

All-or-nothing crowdfunding — miss the goal, every backer gets refunded

The all-or-nothing pledge model only works if "nothing" is enforced. Platforms have been burned both ways: creators paid out on campaigns that quietly missed their goal, and failed campaigns where refunds ran twice (or never). Here the payout edge exists ONLY from `succeeded`, a campaign can reach `succeeded` only via close_campaign checking pledged >= goal, and the failed branch must drain the pledge pool to zero through refunds — the pool slot refuses negative writes, so a double refund of the same backer raises in memory.

A Soma program from the escrow_finance part of the verified corpus: 120 lines, cells Crowdfund, CrowdfundTests. It passes soma check with soma 3.2.4.

How it is built

The cell Crowdfund declares 5 signals in its face: launch(id: String, goal: Int) -> Map, pledge(id: String, backer: String, amount: Int) -> Map, close_campaign(id: String) -> Map, payout_creator(id: String) -> Map and refund_backer(id: String, backer: String) -> Map; keeps 3 memory slots: pool (Map<String, Int>, persistent and consistent) under the invariant pool >= 0, goals (Map<String, Int>, persistent and consistent) and backers (Map<String, Int>, persistent and consistent) under the invariant backers >= 0. Its state machine campaign starts in drafted and allows 4 transitions: drafted -> open_for_pledges, open_for_pledges -> succeeded, open_for_pledges -> failed and succeeded -> paid_out. failed and paid_out are terminal. Handlers: launch (line 42), pledge (line 50), close_campaign (line 61), payout_creator (line 72) and refund_backer (line 79).

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

Generated from soma describe on this file.

The source

crowdfund_all_or_nothing.cell

// ============================================================================
// ALL-OR-NOTHING CROWDFUNDING — miss the goal, every backer gets refunded
// ============================================================================
//
// The all-or-nothing pledge model only works if "nothing" is enforced.
// Platforms have been burned both ways: creators paid out on campaigns
// that quietly missed their goal, and failed campaigns where refunds ran
// twice (or never). Here the payout edge exists ONLY from `succeeded`,
// a campaign can reach `succeeded` only via close_campaign checking
// pledged >= goal, and the failed branch must drain the pledge pool to
// zero through refunds — the pool slot refuses negative writes, so a
// double refund of the same backer raises in memory.
// ============================================================================

cell Crowdfund {
    face {
        signal launch(id: String, goal: Int) -> Map
        signal pledge(id: String, backer: String, amount: Int) -> Map
        signal close_campaign(id: String) -> Map
        signal payout_creator(id: String) -> Map
        signal refund_backer(id: String, backer: String) -> Map
    }

    memory {
        pool: Map<String, Int> [persistent, consistent]
        invariant pool >= 0
        goals: Map<String, Int> [persistent, consistent]
        backers: Map<String, Int> [persistent, consistent]
        invariant backers >= 0
    }

    // paid_out is terminal and reachable ONLY from succeeded;
    // open -> paid_out does not exist. failed never reaches paid_out.
    state campaign {
        initial: drafted
        drafted -> open_for_pledges
        open_for_pledges -> succeeded
        open_for_pledges -> failed
        succeeded -> paid_out
    }

    on launch(id: String, goal: Int) {
        if goal <= 0 { return map("ok", false, "reason", "bad goal") }
        transition(id, "open_for_pledges")
        goals.set(id, goal)
        pool.set(id, 0)
        return map("ok", true, "goal", goal)
    }

    on pledge(id: String, backer: String, amount: Int) {
        if get_status(id) != "open_for_pledges" {
            return map("ok", false, "reason", "campaign is not open")
        }
        if amount <= 0 { return map("ok", false, "reason", "bad amount") }
        let k = "{id}:{backer}"
        backers.set(k, (backers.get(k) ?? 0) + amount)
        pool.set(id, (pool.get(id) ?? 0) + amount)
        return map("ok", true, "pool", pool.get(id))
    }

    on close_campaign(id: String) {
        let raised = pool.get(id) ?? 0
        let goal = goals.get(id) ?? 0
        if raised >= goal {
            transition(id, "succeeded")
        } else {
            transition(id, "failed")
        }
        return map("ok", true, "state", get_status(id), "raised", raised)
    }

    on payout_creator(id: String) {
        transition(id, "paid_out")       // raises unless goal was met
        let amt = pool.get(id) ?? 0
        pool.set(id, 0)
        return map("ok", true, "paid", amt)
    }

    on refund_backer(id: String, backer: String) {
        if get_status(id) != "failed" {
            return map("ok", false, "reason", "refunds only on failed campaigns")
        }
        let k = "{id}:{backer}"
        let owed = backers.get(k) ?? 0
        if owed == 0 { return map("ok", false, "reason", "nothing owed to {backer}") }
        pool.set(id, (pool.get(id) ?? 0) - owed)   // double refund raises here
        backers.set(k, 0)
        return map("ok", true, "refunded", owed)
    }
}

cell test CrowdfundTests {
    rules {
        // a campaign that MISSES its goal
        assert launch("c1", 1000).ok == true
        assert pledge("c1", "amy", 400).ok == true
        assert pledge("c1", "ben", 300).ok == true
        // creator cannot grab the pool mid-campaign or after failure
        assert_fails transition("c1", "paid_out")
        assert close_campaign("c1").state == "failed"
        assert_fails transition("c1", "paid_out")
        assert_fails payout_creator("c1")
        // every backer made whole, exactly once
        assert refund_backer("c1", "amy").refunded == 400
        assert refund_backer("c1", "amy").ok == false
        assert refund_backer("c1", "ben").refunded == 300
        assert_fails pool.set("c1", -1)
        // a campaign that MAKES its goal
        assert launch("c2", 500).ok == true
        assert pledge("c2", "cal", 600).ok == true
        assert close_campaign("c2").state == "succeeded"
        // no refunds on a successful campaign — the money goes to the work
        assert refund_backer("c2", "cal").ok == false
        assert payout_creator("c2").paid == 600
        // paid_out is terminal: no second payout, no late refund path
        assert_fails transition("c2", "succeeded")
        assert_fails transition("c2", "failed")
    }
}

What the toolchain says

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

$ soma check crowdfund_all_or_nothing.cell
✓ All checks passed.
$ soma test crowdfund_all_or_nothing.cell
test CrowdfundTests ...
  ✓ assert launch("c1", 1000).ok == true
  ✓ assert pledge("c1", "amy", 400).ok == true
  ✓ assert pledge("c1", "ben", 300).ok == true
  ✓ assert_fails transition("c1", "paid_out") — raised invalid transition: open_for_pledges → paid_out. Current state: 'open_for_pledges'. Valid targets: [succeeded, failed]
  ✓ assert close_campaign("c1").state == "failed"
  ✓ assert_fails transition("c1", "paid_out") — raised invalid transition: failed → paid_out. Current state: 'failed'. Valid targets: []
  ✓ assert_fails payout_creator("c1") — raised invalid transition: failed → paid_out. Current state: 'failed'. Valid targets: []
  ✓ assert refund_backer("c1", "amy").refunded == 400
  ✓ assert refund_backer("c1", "amy").ok == false
  ✓ assert refund_backer("c1", "ben").refunded == 300
  ✓ assert_fails pool.set("c1", -1) — raised memory invariant violated on 'pool': pool >= 0 — rejected write of -1 (key "c1"); the slot is unchanged
  ✓ assert launch("c2", 500).ok == true
  ✓ assert pledge("c2", "cal", 600).ok == true
  ✓ assert close_campaign("c2").state == "succeeded"
  ✓ assert refund_backer("c2", "cal").ok == false
  ✓ assert payout_creator("c2").paid == 600
  ✓ assert_fails transition("c2", "succeeded") — raised invalid transition: paid_out → succeeded. Current state: 'paid_out'. Valid targets: []
  ✓ assert_fails transition("c2", "failed") — raised invalid transition: paid_out → failed. Current state: 'paid_out'. Valid targets: []

18 tests: 18 passed, 0 failed
$ soma verify crowdfund_all_or_nothing.cell
Verifying crowdfund_all_or_nothing.cell...

State machine 'campaign': 5 states, initial 'drafted'
  States: [drafted, failed, open_for_pledges, paid_out, succeeded]

  ✓ 5 states, 4 transitions
  ✓ all states reachable from 'drafted'
  ✓ terminal states: [failed, paid_out]
  ✓ 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 5 handlers structurally terminate
  ✓ refinement: handler `launch` ⟶ {open_for_pledges}
  ✓ refinement: handler `close_campaign` ⟶ {succeeded [if raised >= goal], failed [if not (raised >= goal)]}
  ✓ refinement: handler `payout_creator` ⟶ {paid_out}
  · transition sources: `launch`, `close_campaign`, `payout_creator` 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)

Crowdfund/invariants:

  ✓ invariant pool >= 0 — writer 'launch' proven (writes 0)
  ✓ invariant pool >= 0 — writer 'payout_creator' proven (writes 0)
  ✓ invariant pool >= 0 — writer 'pledge' proven by induction (writes (pool.get(id) ?? 0) + amount)
  ⚠ invariant pool >= 0 — runtime-checked (computed values): refund_backer → pool because `pool` has no known range
  ✓ invariant backers >= 0 — writer 'pledge' proven by induction (writes (backers.get(k) ?? 0) + amount)
  ✓ invariant backers >= 0 — writer 'refund_backer' proven (writes 0)

15 passed, 1 warnings, 0 failures

  Temporal properties for 'campaign':
  ✓ deadlock_free — no deadlocks in any reachable state
Temporal: 1 passed, 0 failed
VERIFY OK

Builtins used

get_status, map, transition

Source file: /corpus/escrow_finance/crowdfund_all_or_nothing.cell · examples/corpus/escrow_finance/crowdfund_all_or_nothing.cell