Todo service backed by a typed state machine (sum type TodoStatus)

Each todo transitions Pending -> InProgress -> Done, or * -> Cancelled.

A Soma program from the web part of the verified corpus: 82 lines, cells TodoStatus, TodoService, TodoServiceTest. It passes soma check with soma 3.2.4.

How it is built

The cell TodoService declares 6 signals in its face: request(method: String, path: String, body: String) -> Map, add(text: String) -> Map, start(id: String) -> Map, finish(id: String) -> Map, cancel(id: String) -> Map and show(id: String) -> Map; keeps 1 memory slot: todos (Map<String, Map>, persistent and consistent). Its state machine todo starts in Pending and allows 3 transitions: Pending -> InProgress, InProgress -> Done and * -> Cancelled. Cancelled and Done are terminal. Handlers: add (line 30), start (line 36), finish (line 42), cancel (line 48), show (line 54) and request (line 60).

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

Generated from soma describe on this file.

The source

soma.toml

[package]
name = "web-corpus"
version = "0.1.0"
entry = "todo_state.cell"

[verify]
cells = ["TodoService"]
deadlock_free = true
eventually = ["Done", "Cancelled"]

todo_state.cell

// Todo service backed by a typed state machine (sum type TodoStatus).
// Each todo transitions Pending -> InProgress -> Done, or * -> Cancelled.

cell type TodoStatus {
    variants { Pending  InProgress  Done  Cancelled }
}

cell TodoService {
    face {
        signal request(method: String, path: String, body: String) -> Map
        signal add(text: String) -> Map
        signal start(id: String) -> Map
        signal finish(id: String) -> Map
        signal cancel(id: String) -> Map
        signal show(id: String) -> Map
        promise all_persistent
    }

    memory {
        todos: Map<String, Map> [persistent, consistent]
    }

    state todo: TodoStatus {
        initial: Pending
        Pending    -> InProgress
        InProgress -> Done
        *          -> Cancelled
    }

    on add(text: String) {
        let id = to_string(next_id())
        todos.set(id, map("id", id, "text", text))
        return map("id", id, "status", get_status(id))
    }

    on start(id: String) {
        if todos.get(id) == () { return response(404, map("error", "not found")) }
        transition(id, InProgress)
        return map("id", id, "status", get_status(id))
    }

    on finish(id: String) {
        if todos.get(id) == () { return response(404, map("error", "not found")) }
        transition(id, Done)
        return map("id", id, "status", get_status(id))
    }

    on cancel(id: String) {
        if todos.get(id) == () { return response(404, map("error", "not found")) }
        transition(id, Cancelled)
        return map("id", id, "status", get_status(id))
    }

    on show(id: String) {
        let t = todos.get(id)
        if t == () { return response(404, map("error", "not found")) }
        return map("id", id, "text", t.text, "status", get_status(id))
    }

    on request(method: String, path: String, body: String) {
        let req = map("method", method, "path", path)
        match req {
            {method: "POST", path: "/todos"}            -> add(from_json(body).text)
            {method: "POST", path: "/start/" + id}      -> start(id)
            {method: "POST", path: "/finish/" + id}     -> finish(id)
            {method: "POST", path: "/cancel/" + id}     -> cancel(id)
            {method: "GET",  path: "/todos/" + id}      -> show(id)
            _                                           -> response(404, map("error", "no route"))
        }
    }
}

cell test TodoServiceTest {
    rules {
        assert add("write tests").status == "Pending"
        assert start("1").status == "InProgress"
        assert finish("1").status == "Done"
        assert show("1").text == "write tests"
        assert cancel(add("scrap").id).status == "Cancelled"
    }
}

What the toolchain says

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

$ soma check todo_state.cell
✓ All checks passed.

$ soma test todo_state.cell
test TodoServiceTest ...
  ✓ assert add("write tests").status == "Pending"
  ✓ assert start("1").status == "InProgress"
  ✓ assert finish("1").status == "Done"
  ✓ assert show("1").text == "write tests"
  ✓ assert cancel(add("scrap").id).status == "Cancelled"

5 tests: 5 passed, 0 failed

$ soma verify todo_state.cell
Verifying todo_state.cell...

State machine 'todo': 4 states, initial 'Pending'
  States: [Cancelled, Done, InProgress, Pending]

  ✓ 4 states, 5 transitions
  ✓ all states reachable from 'Pending'
  ✓ terminal states: [Cancelled]
  ✓ no deadlocks
  ✓ liveness: every state can eventually reach a terminal state
  ✓ wildcard transitions: * -> [Cancelled]
  ⚠ `* -> Cancelled` also adds Done -> Cancelled — so Done is not final. If it should stay final, write `* -> Cancelled except [Done]`
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (3 handlers, 3 literal transitions, 0 dynamic)
  ✓ termination: all 6 handlers structurally terminate
  ✓ refinement: handler `start` ⟶ {InProgress}
  ✓ refinement: handler `finish` ⟶ {Done}
  ✓ refinement: handler `cancel` ⟶ {Cancelled}
  · transition sources: `start`, `finish`, `cancel` 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)

11 passed, 1 warnings, 0 failures

  Temporal properties for 'todo':
  ✓ deadlock_free — no deadlocks in any reachable state
  ✓ eventually(state in [Done, Cancelled]) — all paths eventually satisfy the predicate
soma.toml: 1 user-defined properties loaded
Temporal: 2 passed, 0 failed
VERIFY OK

Builtins used

from_json, get_status, map, next_id, response, to_string, transition

Source file: /corpus/web/todo_state.cell · examples/corpus/web/todo_state.cell