State machines

state order {
    initial: pending
    pending -> validated { guard { amount > 0 } }
    validated -> sent
    sent -> filled
    sent -> rejected
    filled -> settled
    * -> cancelled           // from any state
}

// In handlers:
transition("order_id", "validated")    // move state (from wherever the instance is)
transition("order_id", "pending", "validated")  // …declaring the source: `soma check`
                                       // verifies the edge pending -> validated exists, and the
                                       // call raises invalid_transition when the instance is
                                       // anywhere else — verify then sees which edge the handler takes
let status = get_status("order_id")    // current state
let valid = valid_transitions("order_id") // available transitions

// A guard reads the locals of the handler that calls transition(). It is
// PROVEN by `soma verify` when every such handler narrows the guard's
// variables with a `require` (or an enclosing `if`) before the call and does
// not reassign them in between; otherwise it is reported ⚠ runtime-checked
// (and `verify --strict` fails on it):
//   pending -> validated { guard { amount > 0 && amount < 1000 } }
//   on validate(id: String, amount: Int) {
//       require amount > 0 && amount <= 999 else BadAmount   // proves the guard
//       transition(id, "pending", "validated")
//   }