The production lookup
The moves table
This is not documentation. It is the lookup the production code
uses to decide where a row goes. finished and unpaid have no
moves, so they are terminal. Any event not listed for a node must
throw.
A payment row has a state column. Somewhere there are a dozen
UPDATE … SET state = ? statements, a few if (state === …)
branches, a cron job that picks rows in some states, a pruning job
that deletes rows in others, and a plan document with a table of
transitions that was accurate on the day it was written.
Ask "can a row that might hold a customer's money ever be deleted?" and nobody can answer without reading all of it. An agent certainly cannot, and every change it makes is a chance to break the answer.
The tickets repository declares each lifecycle as data, using a
shared shape in
src/shared/schema-atlas/machine-spec.ts:
The worked example is the SumUp recovery machine. SumUp does not sign its callbacks and has no redelivery, so one lost callback means a paid checkout looks exactly like an abandoned one. The machine replaces that lost notice with scheduled checks.
The production lookup
This is not documentation. It is the lookup the production code
uses to decide where a row goes. finished and unpaid have no
moves, so they are terminal. Any event not listed for a node must
throw.
export const RECOVERY_MOVES: MachineMoves<
RecoveryNodeId,
RecoveryEventId
> = {
finished: {},
owed: {
read_paid_booked: "finished",
read_paid_contradiction: "owed",
read_paid_settled: "finished",
read_paid_unreadable: "owed",
read_paid_unsettled: "owed",
read_unavailable: "owed",
},
staged: { checkout_created: "waiting" },
unpaid: {},
waiting: {
read_expired_or_failed: "unpaid",
read_paid_booked: "finished",
read_paid_contradiction: "owed",
read_paid_settled: "finished",
read_paid_unreadable: "waiting",
read_paid_unsettled: "owed",
read_pending: "waiting",
read_unavailable: "waiting",
},
};
Each node carries the facts the safety rules talk about. Note the
three-valued answer for money. waiting is not "no money owed", it is
"unknown", and the comment says why:
/** Whether a node can be holding money nobody accounted for. `waiting`
* is unknown rather than no: until SumUp answers, a paid checkout whose
* callback was lost looks exactly like one nobody ever paid. That is the
* whole harm this machine exists to close. */
export type RecoveryOwesMoney = "no" | "unknown" | "yes";
{ id: "waiting", owesMoney: "unknown", prunable: false, ... },
{ id: "owed", owesMoney: "yes", prunable: false, ... },
{ id: "unpaid", owesMoney: "no", prunable: true, ... },
A shared test helper,
registerConformanceSweep,
runs every event against every representative row of every node,
through the real transition functions:
Registers one test per node: every event runs against every one of its shapes and must land where the table says — or throw, when the cell is absent.
So the table cannot drift from the code. If someone changes a
transition and not the table, a cell lands somewhere unexpected and
the sweep fails. If someone adds an event and forgets a node, the
missing cell is a refusal, and the sweep proves the code really
refuses. registerTableChecks also pins the size of the table (nodes,
events, shapes), so a quietly shrunk event list cannot pass as "every
cell still conforms".
Beside the sweep sit the laws, written as tests over the declaration, not as sentences in a plan. From the machine's test file:
test("a row that may hold money is never deleted on age alone", () => {
expect(unaccountedNodes.map((node) => node.id)).toEqual([
"waiting",
"owed",
]);
for (const node of unaccountedNodes) {
expect(node.prunable, `${node.id} must not be prunable`).toBe(false);
}
});
test("a row that may hold money always has something that will act on it", () => {
// every unaccounted node has at least one system event that moves it
});
And over the graph, using a shared walker:
A law stops a future node or event from quietly breaking the rule. Add a new state that can hold money and forget to make it non-prunable, and the build fails with the law's name.
Once the machine exists, nothing else gets to restate it:
check event can move. A new check event joins the queue by being
declared./admin/schema all read from the spec.The machine says what valid transitions do. It cannot say what is in
the database right now. A bounded live scan
(schema-anomaly-scan.ts)
reads the stored rows, checks the machine's rules against them (for
example, every state except staged must carry a checkout id), and
shows each fault to the operator. "A proof over valid transitions does
not detect corrupt stored records."
deno task contract:diff prints how this branch changed the declared
machines: moves, money flags and tables, against the merge base. It
is a report, not a gate. It goes in the pull request description, so a
reviewer sees "this branch adds a move from owed to unpaid" in one
line instead of finding it in a diff.