soma.cell

Milestone escrow — a contractor is paid per accepted milestone, never ahead

Freelance platforms learned this the expensive way: pay a contractor the full project fee up front and disputes become hostage negotiations. The escrow answer is milestones — but then the bug moves: releasing milestone money TWICE, or releasing more than the client funded. Here the funded balance is a slot that releases draw down (`escrowed >= 0`: the over-release is a rejected write), each milestone is released at most once, and a cancelled or completed project is terminal — the leftover balance goes back to the client exactly once.

A Soma program from the escrow_finance part of the verified corpus: 106 lines, cells MilestoneEscrow, MilestoneTests. It passes soma check with soma 3.2.4.

How it is built

The cell MilestoneEscrow declares 5 signals in its face: fund_project(id: String, amount: Int) -> Map, accept_milestone(id: String, ms: String, fee: Int) -> Map, finish_project(id: String) -> Map, cancel_project(id: String) -> Map and escrow_left(id: String) -> Int; keeps 2 memory slots: escrowed (Map<String, Int>, persistent and consistent) under the invariant escrowed >= 0 and released (Map<String, Int>, persistent and consistent) under the invariant released >= 0. Its state machine project starts in proposed and allows 3 transitions: proposed -> funded, funded -> completed and funded -> cancelled. cancelled and completed are terminal. Handlers: fund_project (line 39), accept_milestone (line 46), finish_project (line 61), cancel_project (line 68) and escrow_left (line 75).

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

Generated from soma describe on this file.

The source

milestone_escrow.cell

// ============================================================================
// MILESTONE ESCROW — a contractor is paid per accepted milestone, never ahead
// ============================================================================
//
// Freelance platforms learned this the expensive way: pay a contractor the
// full project fee up front and disputes become hostage negotiations. The
// escrow answer is milestones — but then the bug moves: releasing milestone
// money TWICE, or releasing more than the client funded. Here the funded
// balance is a slot that releases draw down (`escrowed >= 0`: the
// over-release is a rejected write), each milestone is released at most
// once, and a cancelled or completed project is terminal — the leftover
// balance goes back to the client exactly once.
// ============================================================================

cell MilestoneEscrow {
    face {
        signal fund_project(id: String, amount: Int) -> Map
        signal accept_milestone(id: String, ms: String, fee: Int) -> Map
        signal finish_project(id: String) -> Map
        signal cancel_project(id: String) -> Map
        signal escrow_left(id: String) -> Int
    }

    memory {
        escrowed: Map<String, Int> [persistent, consistent]
        invariant escrowed >= 0
        released: Map<String, Int> [persistent, consistent]
        invariant released >= 0
    }

    // completed and cancelled are terminal: no release after either.
    state project {
        initial: proposed
        proposed -> funded
        funded -> completed
        funded -> cancelled
    }

    on fund_project(id: String, amount: Int) {
        if amount <= 0 { return map("ok", false, "reason", "bad amount") }
        transition(id, "funded")
        escrowed.set(id, amount)
        return map("ok", true, "escrowed", amount)
    }

    on accept_milestone(id: String, ms: String, fee: Int) {
        if get_status(id) != "funded" {
            return map("ok", false, "reason", "project is not active")
        }
        if fee <= 0 { return map("ok", false, "reason", "bad fee") }
        let k = "{id}:{ms}"
        if (released.get(k) ?? 0) > 0 {
            return map("ok", false, "reason", "milestone {ms} already released")
        }
        let bal = escrowed.get(id) ?? 0
        escrowed.set(id, bal - fee)        // raises past the funded amount
        released.set(k, fee)
        return map("ok", true, "milestone", ms, "left", bal - fee)
    }

    on finish_project(id: String) {
        transition(id, "completed")
        let refund = escrowed.get(id) ?? 0
        escrowed.set(id, 0)                // unspent escrow back to client
        return map("ok", true, "refund_to_client", refund)
    }

    on cancel_project(id: String) {
        transition(id, "cancelled")
        let refund = escrowed.get(id) ?? 0
        escrowed.set(id, 0)
        return map("ok", true, "refund_to_client", refund)
    }

    on escrow_left(id: String) {
        return escrowed.get(id) ?? 0
    }
}

cell test MilestoneTests {
    rules {
        assert fund_project("site", 5000).ok == true
        assert accept_milestone("site", "design", 1500).ok == true
        assert accept_milestone("site", "build", 2500).ok == true
        assert escrow_left("site") == 1000
        // THE DOUBLE RELEASE: same milestone, second payment — refused
        assert accept_milestone("site", "design", 1500).ok == false
        // THE OVER-RELEASE: 1,800 against 1,000 left — the write raises
        assert_fails accept_milestone("site", "launch", 1800)
        assert escrow_left("site") == 1000
        assert_fails escrowed.set("site", -1)
        // finishing returns the leftover to the client, once
        assert finish_project("site").refund_to_client == 1000
        assert escrow_left("site") == 0
        // completed is terminal: no milestone, no cancel-refund after
        assert accept_milestone("site", "extra", 100).ok == false
        assert_fails transition("site", "cancelled")
        assert_fails transition("site", "funded")
        // the cancel path on another project, equally final
        assert fund_project("logo", 800).ok == true
        assert accept_milestone("logo", "draft", 300).ok == true
        assert cancel_project("logo").refund_to_client == 500
        assert_fails transition("logo", "completed")
    }
}

What the toolchain says

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

$ soma check milestone_escrow.cell
✓ All checks passed.
$ soma test milestone_escrow.cell
test MilestoneTests ...
  ✓ assert fund_project("site", 5000).ok == true
  ✓ assert accept_milestone("site", "design", 1500).ok == true
  ✓ assert accept_milestone("site", "build", 2500).ok == true
  ✓ assert escrow_left("site") == 1000
  ✓ assert accept_milestone("site", "design", 1500).ok == false
  ✓ assert_fails accept_milestone("site", "launch", 1800) — raised memory invariant violated on 'escrowed': escrowed >= 0 — rejected write of -800 (key "site"); the slot is unchanged
  ✓ assert escrow_left("site") == 1000
  ✓ assert_fails escrowed.set("site", -1) — raised memory invariant violated on 'escrowed': escrowed >= 0 — rejected write of -1 (key "site"); the slot is unchanged
  ✓ assert finish_project("site").refund_to_client == 1000
  ✓ assert escrow_left("site") == 0
  ✓ assert accept_milestone("site", "extra", 100).ok == false
  ✓ assert_fails transition("site", "cancelled") — raised invalid transition: completed → cancelled. Current state: 'completed'. Valid targets: []
  ✓ assert_fails transition("site", "funded") — raised invalid transition: completed → funded. Current state: 'completed'. Valid targets: []
  ✓ assert fund_project("logo", 800).ok == true
  ✓ assert accept_milestone("logo", "draft", 300).ok == true
  ✓ assert cancel_project("logo").refund_to_client == 500
  ✓ assert_fails transition("logo", "completed") — raised invalid transition: cancelled → completed. Current state: 'cancelled'. Valid targets: []

17 tests: 17 passed, 0 failed
$ soma verify milestone_escrow.cell
Verifying milestone_escrow.cell...

State machine 'project': 4 states, initial 'proposed'
  States: [cancelled, completed, funded, proposed]

  ✓ 4 states, 3 transitions
  ✓ all states reachable from 'proposed'
  ✓ terminal states: [completed, cancelled]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 5 handlers structurally terminate
  ✓ refinement: handler `fund_project` ⟶ {funded}
  ✓ refinement: handler `finish_project` ⟶ {completed}
  ✓ refinement: handler `cancel_project` ⟶ {cancelled}
  · transition sources: `fund_project`, `finish_project`, `cancel_project` 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)

MilestoneEscrow/invariants:

  ✓ invariant escrowed >= 0 — writer 'cancel_project' proven (writes 0)
  ✓ invariant escrowed >= 0 — writer 'finish_project' proven (writes 0)
  ✓ invariant escrowed >= 0 — writer 'fund_project' proven by induction (writes amount)
  ⚠ invariant escrowed >= 0 — runtime-checked (computed values): accept_milestone → escrowed
  ✓ invariant released >= 0 — writer 'accept_milestone' proven by induction (writes fee)

14 passed, 1 warnings, 0 failures

  Temporal properties for 'project':
  ✓ 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/milestone_escrow.cell · examples/corpus/escrow_finance/milestone_escrow.cell