State model: records, enums, and internal fields

The abstract machine holds all its knowledge in a single ServerState. This chapter walks every component of that state: the records, their fields, which fields cross the wire, and which are internal implementation details the spec uses but never exposes to callers.

The canonical source for everything here is spec/01-objects/types.lean (wire records and enums) and spec/01-objects/state.lean (internal objects, effects, and ServerState). Read these files directly when a detail matters for your implementation.

Two levels: internal objects and wire records#

The spec defines two shapes for each entity:

• Internal object (PromiseObject, TaskObject) — what the machine stores. Contains all fields including ones that are never serialized.
• Wire record (PromiseRecord, TaskRecord) — what appears in request/response bodies. A strict subset of the internal object.

The conversion is explicit. PromiseObject.toRecord strips callbacks and listeners. TaskObject.toRecord strips resumes (as a List String) and replaces it with resumes.length (a count). If you store more than the wire record in your database, those extra fields are implementation internals that callers will never see and must never rely on.

Promises#

PromiseState#

pending | resolved | rejected | rejectedCanceled | rejectedTimedout

Five variants. A promise starts pending and moves to exactly one terminal state. The three rejected* variants distinguish a caller-initiated rejection (rejected), an administrative cancellation (rejectedCanceled), and a timeout expiry (rejectedTimedout). resolved is the success terminal. See the durable promise specification for the semantics of each state.

PromiseRecord (wire-visible)#

Value is { headers : Tags, data : Option String }. Tags is List (String × String). Both appear on the wire as-is.

PromiseObject (internal — adds two fields)#

callbacks holds promise IDs, not task IDs. When a task suspends waiting for a promise to settle, the server adds the awaiter's promise ID (which equals the awaiter's task ID) to the awaited promise's callbacks list. listeners holds delivery addresses (strings). Both lists are deduplicated: adding an entry that already exists is a no-op.

External and timer promises#

Two predicate functions on PromiseObject matter throughout the machine:

• External promise: p.tags.has "resonate:target" || p.isTimer — a promise that triggers work outside the machine (a worker execution or a timer). External promises always have a corresponding task.
• Timer promise: p.tags.get? "resonate:timer" == some "true" — a special external promise that settles resolved (not rejectedTimedout) when its timeoutAt elapses.

See tasks for how resonate:target causes a task and an execute message to be created alongside the promise.

Tasks#

TaskState#

pending | acquired | suspended | halted | fulfilled

Five variants. fulfilled is the only terminal state; halted is an administrative state that a task enters via task.halt and leaves via task.continue (which returns it to pending). A task in halted is out of circulation: it holds no lease and no retry timeout. Your monitoring should surface halted tasks explicitly — they will not self-recover.

TaskRecord (wire-visible)#

TaskObject (internal — resumes is richer)#

The resumes divergence is the sharpest difference between the two levels. On the wire, resumes is a count — a worker can observe that multiple settlements fired while it was away but cannot see which ones without looking up the awaited promises individually. Internally, the machine stores the actual IDs so that enqueueResume can deduplicate.

Version and lease#

Version (version : Nat) is the fencing token. It increments on every pending→acquired transition — in task.acquire (see T-03-task.acquire.lean) and in the re-acquire branch of task.create (T-02-task.create.lean). No other operation changes it. A task returning to pending after a lease expiry or a task.release keeps its current version; the next task.acquire bumps it. Every mutating operation on a task (fence, suspend, fulfill, release) must present the current version and receives 409 if the version has moved on. This is how a stale worker's writes are rejected.

Lease is ttl+pid together. ttl is the Unix ms deadline after which the server considers the worker dead; pid identifies which worker holds it. Both are none when a task is not acquired. Both are set on task.acquire and cleared on task.suspend (the task parks without a lease; it is woken by settlement, not by a clock). A lease timeout fires onTaskLeaseTimeout, which returns the task to pending, clears ttl and pid, and re-enqueues an execute message — all without advancing the version.

Schedules#

A Schedule is a recurring cron rule. The machine stores it as a single record with no internal-only variant:

Each schedule carries its own timeout entry. When that timeout fires, onScheduleTimeout calls catchUp — which loops, creating promises for every missed fire since the last run, advancing nextRunAt after each one, until the schedule is current. See timeouts and projection for the full catchUp semantics.

Timeout lists#

ServerState has three timeout lists. Each entry is a (id, timeout) pair the environment is expected to fire when now ≥ timeout:

The kind field on TaskTimeout is the only place where a single list encodes two distinct behaviors. A pending task has a retry timeout (kind=0): if no worker acquires it within retryTimeout ms (default 5000), the server re-enqueues the execute message. An acquired task has a lease timeout (kind=1): if no heartbeat refreshes it in time, the server evicts the worker. The two kinds are always exclusive — a pending task carries exactly one kind=0 entry, an acquired task exactly one kind=1 entry, and other states carry none; delTaskTimeout (which removes all entries for an id regardless of kind) always runs before setTaskTimeout in every handler that transitions between these states, so both kinds are never present at once. See timeouts and projection for how projection interacts with both.

Outbox#

outbox : List OutboxEntry is the machine's pending delivery queue. Each entry is:

structure OutboxEntry where
  address : String
  message : Message   -- execute (taskId version) | unblock (promise : PromiseRecord)

Two message types exist:

• execute taskId version — dispatches a task to a worker at address. Carries the task's current version (not incremented by the enqueue; the next acquire will increment it).
• unblock promise — notifies a listener at address that a promise has settled. Carries the settled PromiseRecord.

Outbox entries are keyed: setMessage deduplicates by taskId for execute messages, and by "{promiseId}:notify:{address}" for unblock messages. A handler that enqueues the same message twice leaves only one entry. Your delivery layer reads and drains the outbox; the spec says nothing about delivery guarantees or ordering beyond the keying rule. See outbox and delivery for implementation strategies.

Cross-reference#

The objects defined here appear throughout the prose specification:

• Promise lifecycle and promise states: durable promise specification
• Task lifecycle, invariants, and version semantics: tasks
• How timeout projection makes a pending-but-expired promise read as already settled: timeouts and projection

The abstract machine chapter preceding this one covers M, effects, and handler structure: abstract machine.

Verified against resonate-specification@83d64c3.