Order records with nested line-items, computed totals, and a state machine over the order lifecycle

Demonstrates records carrying lists of records, with() copy-update, and records that drive transitions.

A Soma program from the records part of the verified corpus: 58 lines, cells OrderStatus, Orders, OrdersTest. It passes soma check with soma 3.2.4.

How it is built

The cell Orders declares 4 signals in its face: new_order(customer: String) -> Map, subtotal(o: Map) -> Int, with_discount(o: Map, pct: Int) -> Map and pay(id: String) -> String. Its state machine order starts in Pending and allows 4 transitions: Pending -> Paid, Paid -> Shipped, Shipped -> Delivered and * -> Cancelled. Cancelled and Delivered are terminal. Handlers: new_order (line 25), subtotal (line 32), with_discount (line 37) and pay (line 43).

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

Generated from soma describe on this file.

The source

orders.cell

// Order records with nested line-items, computed totals, and a state
// machine over the order lifecycle. Demonstrates records carrying lists
// of records, with() copy-update, and records that drive transitions.

cell type OrderStatus {
    variants { Pending  Paid  Shipped  Delivered  Cancelled }
}

cell Orders {
    face {
        signal new_order(customer: String) -> Map
        signal subtotal(o: Map) -> Int
        signal with_discount(o: Map, pct: Int) -> Map
        signal pay(id: String) -> String
    }

    state order: OrderStatus {
        initial: Pending
        Pending  -> Paid
        Paid     -> Shipped
        Shipped  -> Delivered
        *        -> Cancelled
    }

    on new_order(customer: String) {
        return Order { customer: customer, lines: list(
            Line { name: "Keyboard", qty: 1, price: 80 },
            Line { name: "Mouse",    qty: 2, price: 25 }
        )}
    }

    on subtotal(o: Map) {
        return sum(o.lines |> map(l => l.qty * l.price))
    }

    // Functional copy-update: return a new record with a `total` field added.
    on with_discount(o: Map, pct: Int) {
        let base = subtotal(o)
        let total = base - floor(base * pct / 100)
        return o |> with("total", total)
    }

    on pay(id: String) {
        transition(id, Paid)
        return get_status(id)
    }
}

cell test OrdersTest {
    rules {
        assert subtotal(new_order("Ada")) == 130
        assert new_order("Ada").customer == "Ada"
        assert with_discount(new_order("Ada"), 10).total == 117
        assert pay("ord-1") == "Paid"
        assert new_order("Ada").lines[1].name == "Mouse"
    }
}

What the toolchain says

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

$ soma check orders.cell
✓ All checks passed.

$ soma test orders.cell
test OrdersTest ...
  ✓ assert subtotal(new_order("Ada")) == 130
  ✓ assert new_order("Ada").customer == "Ada"
  ✓ assert with_discount(new_order("Ada"), 10).total == 117
  ✓ assert pay("ord-1") == "Paid"
  ✓ assert new_order("Ada").lines[1].name == "Mouse"

5 tests: 5 passed, 0 failed

$ soma verify orders.cell
Verifying orders.cell...

State machine 'order': 5 states, initial 'Pending'
  States: [Cancelled, Delivered, Paid, Pending, Shipped]

  ✓ 5 states, 7 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 Delivered -> Cancelled — so Delivered is not final. If it should stay final, write `* -> Cancelled except [Delivered]`
  ✓ think-isolated: CTL safety properties hold regardless of LLM output (1 handlers, 1 literal transitions, 0 dynamic)
  ✓ termination: all 4 handlers structurally terminate
  ⚠ refinement: declared transition `Paid → Shipped` is never reached by any handler — spec may be aspirational or stale
  ⚠ refinement: declared transition `Shipped → Delivered` is never reached by any handler — spec may be aspirational or stale
  ⚠ refinement: declared transition `* → Cancelled` is never reached by any handler — spec may be aspirational or stale
  ✓ refinement: handler `pay` ⟶ {Paid}
  · transition sources: `pay` calls 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)

9 passed, 4 warnings, 0 failures

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

Builtins used

floor, get_status, list, map, sum, transition, with

Source file: /corpus/records/orders.cell · examples/corpus/records/orders.cell