Resonate Specification

The Resonate protocol, specified as an executable abstract machine in Lean 4: a state, a set of effects (atomic operations on the state) and a set of request handlers (transitions composed from effects).

The Machine

State

state.lean

• objects — promises, tasks, and schedules
• deferred — resume obligations the server records at settlement and invokes on itself later
• timeouts — obligations the environment fires later, as internal transitions
• outbox — messages awaiting delivery: execute dispatches a task to a worker, unblock notifies a listener of a settled promise

Wire-level records and request/response types are in types.lean.

Effects

The atomic operations of the machine (state.lean) — lookups, keyed upserts, and deletes per state component:

Component	Effects
promises	getPromise / setPromise
tasks	getTask / setTask
schedules	getSchedule / setSchedule / delSchedule
deferred	defer / undefer
timeouts	setPromiseTimeout / setTaskTimeout / setScheduleTimeout / del…Timeout
outbox	setMessage

Handlers touch state only through effects. Together they are the contract a concrete implementation must realize. Settlement's write set, restricted to promises and tasks, is {p.id}: settle neither reads nor writes any promise but its own — resumes are recorded as deferred work, discharged by the drain.

Handlers

Every handler is a pure function

Req → (now : Nat) → M Res    -- M = StateM ServerState

composed from effects. Deterministic and total; there is no hidden clock — time enters only through now.

Conventions the whole model leans on:

• Projection — a pending promise past timeoutAt is observed as already settled (resolved for timers, rejectedTimedout otherwise) even before its timeout transition persists that fact.
• Validation — anything rejectable by inspecting the request alone is 400, with highest precedence: before existence, state, or version are consulted. Examples: settling to a non-settable state, self-await, duplicate or empty awaited lists, an untargeted task.create action, an undeliverable listener address.

Protocol Handlers

Promises

	Handler	Transition
P-01	promise.get	Read a promise (with timeout projection).
P-02	promise.create	Create a pending promise; a resonate:target tag also spawns a task and an execute message, optionally delayed.
P-03	promise.settle	Settle a pending promise: fulfill its task, notify listeners, resume awaiters.
P-04	promise.register_callback	Subscribe an awaiter promise for resume when the awaited promise settles.
P-05	promise.register_listener	Subscribe an address for an unblock message when the promise settles.
P-06	promise.search	Not yet specified (501).

Tasks

	Handler	Transition
T-01	task.get	Read a task (projected fulfilled once its promise is no longer pending).
T-02	task.create	Create a promise with an immediately-acquired task, or re-acquire an existing pending task.
T-03	task.acquire	Worker claims a pending task: bump version, arm the lease.
T-04	task.fence	Run a promise.create/promise.settle guarded by the task's fencing token.
T-05	task.heartbeat	Extend the leases of a worker's acquired tasks.
T-06	task.suspend	Park an acquired task on awaited promises; 300 if any is already settled.
T-07	task.fulfill	Settle the task's promise and fulfill the task in one transition.
T-08	task.release	Return an acquired task to pending and re-enqueue its execute.
T-09	task.halt	Take a task out of circulation.
T-10	task.continue	Return a halted task to pending and re-enqueue its execute.
T-11	task.search	Not yet specified (501).

Schedules

	Handler	Transition
S-01	schedule.get	Read a schedule.
S-02	schedule.create	Create a schedule and arm its first fire.
S-03	schedule.delete	Delete a schedule and disarm its timeout.
S-04	schedule.search	Not yet specified (501).

Internal Transitions

Handler	Transition
resume	Drain a deferred resume: wake a suspended awaiter (re-pending + execute) or record the trigger on an active one; the deadline guard re-checks at drain time (timeout always wins).
timeouts	Environment-fired transitions: promise timeout, task retry, lease expiry, schedule fire (with catch-up).

Build

cd spec && lake build