soma.cell

Multi-step expense-approval workflow with guarded transitions

A submitted expense needs manager sign-off; anything over a threshold also needs finance. Rejection at either gate sends it back to draft. Guards on the state machine encode the business rule: the manager_ok -> finance_review arrow is only taken for large amounts.

A Soma program from the state_machines part of the verified corpus: 81 lines, cells ExpenseApproval, ExpenseTests. It passes soma check with soma 3.2.4.

How it is built

The cell ExpenseApproval declares 6 signals in its face: submit(id: String, amount: Int) -> Map, manager_sign(id: String) -> String, finance_sign(id: String) -> String, reject(id: String) -> String, pay_out(id: String) -> String and status(id: String) -> String; keeps 1 memory slot: amounts (Map<String, Int>, persistent and consistent) under the invariant amounts >= 0. Its state machine claim starts in draft and allows 7 transitions: draft -> pending_manager, pending_manager -> pending_finance, pending_manager -> approved, pending_finance -> approved, pending_manager -> draft, pending_finance -> draft and approved -> paid. paid is terminal. Handlers: submit (line 33), manager_sign (line 40), finance_sign (line 51), reject (line 52), pay_out (line 53) and status (line 54).

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

Generated from soma describe on this file.

The source

expense_approval.cell

// Multi-step expense-approval workflow with guarded transitions.
// A submitted expense needs manager sign-off; anything over a threshold
// also needs finance. Rejection at either gate sends it back to draft.
// Guards on the state machine encode the business rule: the manager_ok ->
// finance_review arrow is only taken for large amounts.

cell ExpenseApproval {
    face {
        signal submit(id: String, amount: Int) -> Map
        signal manager_sign(id: String) -> String
        signal finance_sign(id: String) -> String
        signal reject(id: String) -> String
        signal pay_out(id: String) -> String
        signal status(id: String) -> String
    }

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

    state claim {
        initial: draft
        draft          -> pending_manager
        pending_manager -> pending_finance
        pending_manager -> approved
        pending_finance -> approved
        pending_manager -> draft
        pending_finance -> draft
        approved        -> paid
    }

    on submit(id: String, amount: Int) {
        require amount > 0 else bad_amount
        amounts.set(id, amount)
        transition(id, "pending_manager")
        return map("state", get_status(id), "amount", amount)
    }

    on manager_sign(id: String) {
        let amt = amounts.get(id) ?? 0
        // large claims escalate to finance; small ones are approved outright
        if amt > 1000 {
            transition(id, "pending_finance")
        } else {
            transition(id, "approved")
        }
        return get_status(id)
    }

    on finance_sign(id: String) { transition(id, "approved") return get_status(id) }
    on reject(id: String)       { transition(id, "draft")    return get_status(id) }
    on pay_out(id: String)      { transition(id, "paid")     return get_status(id) }
    on status(id: String)       { return get_status(id) }
}

cell test ExpenseTests {
    rules {
        // small claim: manager approves outright, then paid
        assert submit("e1", 200).state == "pending_manager"
        assert manager_sign("e1") == "approved"
        assert pay_out("e1") == "paid"

        // large claim: escalates to finance before approval
        assert submit("e2", 5000).state == "pending_manager"
        assert manager_sign("e2") == "pending_finance"
        assert finance_sign("e2") == "approved"
        assert pay_out("e2") == "paid"

        // rejection bounces back to draft, then can be resubmitted
        assert submit("e3", 300).state == "pending_manager"
        assert reject("e3") == "draft"
        assert submit("e3", 300).state == "pending_manager"

        // a zero/negative amount is refused before any state change
        assert_fails submit("e4", 0)
        // illegal: cannot pay an expense that isn't approved yet
        assert_fails pay_out("e5")
    }
}

What the toolchain says

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

$ soma check expense_approval.cell
✓ All checks passed.
$ soma test expense_approval.cell
test ExpenseTests ...
  ✓ assert submit("e1", 200).state == "pending_manager"
  ✓ assert manager_sign("e1") == "approved"
  ✓ assert pay_out("e1") == "paid"
  ✓ assert submit("e2", 5000).state == "pending_manager"
  ✓ assert manager_sign("e2") == "pending_finance"
  ✓ assert finance_sign("e2") == "approved"
  ✓ assert pay_out("e2") == "paid"
  ✓ assert submit("e3", 300).state == "pending_manager"
  ✓ assert reject("e3") == "draft"
  ✓ assert submit("e3", 300).state == "pending_manager"
  ✓ assert_fails submit("e4", 0) — raised require failed: bad_amount: constraint violated
  ✓ assert_fails pay_out("e5") — raised invalid transition: draft → paid. Current state: 'draft'. Valid targets: [pending_manager]

12 tests: 12 passed, 0 failed
$ soma verify expense_approval.cell
Verifying expense_approval.cell...

State machine 'claim': 5 states, initial 'draft'
  States: [approved, draft, paid, pending_finance, pending_manager]

  ✓ 5 states, 7 transitions
  ✓ all states reachable from 'draft'
  ✓ terminal states: [paid]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (5 handlers, 6 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `submit` ⟶ {pending_manager}
  ✓ refinement: handler `manager_sign` ⟶ {pending_finance [if amt > 1000], approved [if not (amt > 1000)]}
  ✓ refinement: handler `finance_sign` ⟶ {approved}
  ✓ refinement: handler `reject` ⟶ {draft}
  ✓ refinement: handler `pay_out` ⟶ {paid}
  · transition sources: `submit`, `manager_sign`, `finance_sign`, `reject`, `pay_out` 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)

ExpenseApproval/invariants:

  ✓ invariant amounts >= 0 — writer 'submit' proven by induction (writes amount)

13 passed, 0 warnings, 0 failures

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

Builtins used

get_status, map, transition

Source file: /corpus/state_machines/expense_approval.cell · examples/corpus/state_machines/expense_approval.cell