Reference 04 State and commits

4. State and commits

Velle abstracts away the database. The system's state is a black box: the set of all shape instances and their stored properties. How that state is physically kept — tables, documents, caches, indexes — is a compiling concern (## 1. Principles); no CRUD vocabulary, storage API, or save/load call exists in the language.

The one way state ever changes is a commit: one mutation entering the state at a discrete moment — an external act submitting a new shape instance (committing an instance is persisting the record — ## Assignment (mutation in place), "No act-level sugar"), a scheduled tick, which is a commit whose changed datum is today (## Schedule triggers), or a rule firing's effects (## rule). A rule's body is exactly one commit, and a firing's effects are a new commit that may match further rules' conditions just as an act's commit would — rules react to conditions holding at commits, never to other rules; there is no call graph. A system never does anything on its own; every change to state traces to some commit.

The CRUD replacement reads off directly: "create" is committing a new instance, "update" is an assignment fired by a rule (## Assignment (mutation in place)), "read" is any predicate or derivation evaluated against current state, and "delete" is a rule effect, delete <path>, whose legality the compiler derives from everything the spec proves using the instance's existence (## Assignment (mutation in place), "Deletion"). What that derivation protects is the fact-recording stance: a produced fact records something that happened in the world, and deleting it would make the description lie (## Exit triggers) — while a current-state record is deletable exactly where nothing the spec proves depends on it. Where the business needs reversal rather than removal, that's a policy expressed as data (## Open / unresolved, Reversal).

Because a commit is a discrete moment, pre-state and post-state are both well-defined at it — which is what lets entry into and exit from a refinement mean something precise, with no hidden bookkeeping (## rule ... when ... on ...). By default, an act's commit and every commit its consequences produce stand or fall together — one all-or-nothing envelope that a rule opts out of with after commit (## rule, "Transactions and after commit"). An act's commit carries exactly one statically-shaped closure — a single instance in the common case, the act plus its declared inline parts when the act's declaration says the parts arrive with it (## Relationships, "Inline part creation"). "Several things arrive together" is not a special commit kind but an ordinary modeling call — a container shape whose single instance is the committed act, with the parts as related shapes — and closure membership is declared, never data-dependent, which is what lets "can these triggers coincide?" be answered from trigger shapes alone (## Assignment (mutation in place), one-writer). Still open: the order-independence and quiescence proofs (OQ16).

Transient acts (transient act)

By default, committing an act is persisting the record — the act is simultaneously a request and a durable business fact (Payment, EmailChange). But some incoming acts are inputs to the state, not members of it: a request whose entire meaning is decided at arrival, whose durable trace should be what the system did about it, not the request itself. Declaring the act transient declares that:

transient act ChangeDueDate {
    invoice: one Invoice
    newDue: Date
}

A transient act's instance exists only within its own commit's transaction: its refinements are evaluated exactly once — at that commit, against the state of that moment — its rules fire, its consequences persist, and at the transaction's close the instance is gone (evaluation.md, "Transient acts"). For an ordinary act, a partition like applicable/refused is re-evaluated whenever the partitioning state changes — an act applied long ago can drift into the refused side when the state later flips (the drift hazard, advisory A4; worked exhibit examples/partition-drift/). For a transient act that re-evaluation never happens, because there is no later act: the hazard is structurally impossible rather than checked.

The declaration carries two obligations (checks V17–V18):

• Isolation — nothing durable or later may depend on the act: no shape may hold a relationship to it (outcome records copy the fields they need — which is also the author declaring which slice of the request is durable business data), its name may appear in no expression, and its rules may fire only on commit — no after commit, no schedules, no when leaving. Asynchronous work hangs off a durable intent the handling rule materializes, the intent-before-effect pattern (## rule, "Transactions and after commit").
• Every request gets a response — a transient act nothing answers would be ignored with no record it ever arrived (an ordinary act at least sits visibly unprocessed). So the answers must provably cover every instance in every reachable state — a compile error otherwise, which is the compiler asking the product question "what should happen to this request in this situation?" and refusing to proceed until the spec answers. An answer is a rule's condition or a never over the act — the boundary refusal is a response, and pairing a rule with a complementary never is the pure-validation rung: the caller is told, and nothing is kept at all (membership's AssignTicket; contrast billing's ChangeDueDate, where the refusal is a business record — which to keep is a product decision, made per act). v0 proves the coarse slice: an answer on the bare act shape, or a complementary pair (P / not P); per-reason refusals live in one complement rule with a conditional reason value.

Correlating responses to requests. Because the instance is gone at the transaction's close, there is no system-assigned request id for a caller to point at later. Where a durable outcome must be matched back to the request that caused it — or the same request submitted twice must be applied once — the act carries a correlation key: a client-supplied field (requestKey: text) whose value every outcome record copies, the idempotency-key pattern real APIs already use (the caller mints one key per logical request, so a resubmission arrives carrying the same key). Everything the pattern needs already exists: the caller supplies the key, outcomes copy it like any other field, and a duplicate-detection guard reads it off the durable outcome (not exists (BidRecord where requestKey == this.requestKey)). This is deliberately a documented idiom rather than language machinery (settled OQ26): the key's uniqueness is the client's to own — the language can neither check nor supply it without storing or minting client keys, a layer below the abstraction it occupies. The per-outcome copy and the per-rule guard conjunct are the author's visible decisions about which requests must be idempotent, the same trade as ## Run-once guards' "No guard sugar"; and two copies of one request racing in flight are simply two transactions, serialized like any others (evaluation.md, "The universal transaction"), the later one meeting whatever guard the author wrote.