The recipient half of the lazy-pull migration (design.md §6.3, steps 3/4/6;
specs/FiefTransfer.tla actions SendPull / RecvPullResp / RecvPush /
Escheat). Pure: see Fief.Transfer for the purity contract, the
effect vocabulary, and the layer split.
Created at handoff_in(session). Tracks per-key migration status and
bounded pend queues; key liveness is an input (the embedder owns the
key→pid map — moduledoc of Fief.Transfer).
Behavior:
first_touch/3— a message arrived for a key with no live process: emit{:pull, key}and pend the message. The pend queue is bounded (max_pending:); overflow drops the new message with an{:overflow, key, msg}effect, so the caller times out (design §6.3's stated semantics).tick/1— pull retry: re-pull every still-pulling key. A pull timeout never authorizes escheat (⊨ rule 1): the donor may be alive and unfenced on the far side of a recipient↔donor partition, still holding the live process — retry forever, until the session ends or:not_herearrives. Downtime over inconsistency.handle_grant/4,handle_push/4— the inject/ack half of the spec'sInjectGuard(the transport half — stale sessions dropped without ack — is the agent envelope, M4). Key never injected this session and not live →{:inject, key, blob}+{:ack, key}+ release pends. Otherwise → ack without inject: an in-session duplicate ack is safe because the session pins the custody period, and the donor retains the residual until some ack lands. Inject at most once per key per session (Decision): after the first inject the frozen blob is stale by construction — the injected process may have written and persisted newer state before dying, and blobs are not version-comparable, so re-injecting resurrects pre-persist state (the intra-session form of ⊨ rule 6's hazard; the spec never models per-key death on a healthy node —procgoes live→NoValonly via node crash, fence, or donor freeze — so itsproc = NoValinject guard is necessarily extended here). A dead injected key recovers via re-pull, which converges to the donor's post-ack:not_here→ escheat from durable truth.handle_not_here/3— escheat is now authorized for this key, this session (⊨ rule 1's other gate). Authorization is sticky for the session (Decision): the donor's ledger only ever shrinks, so its:not_hereanswer can never become wrong — a later re-touch of the key (its process died) escheats immediately, without another round trip.session_over/1— the embedder observed settle or abort (handoff_in(nil)semantics:prev_owner = NULL, the other gate of ⊨ rule 1): every still-pulling key becomes escheat-authorized and escheats, releasing its pends. Terminal — the embedder discards the machine.
Injecting only when the key is not live is the recipient's half of exactly-one-live-process-per-key (the donor's half: the ledger holds only retired state).
Summary
Functions
Was key injected at least once this session?
Is escheat authorized for key this session?
A message arrived for a key with no live process (the embedder checks liveness first; live keys are delivered directly and never reach the machine). Escheat-authorized keys escheat immediately (sticky authorization); keys already pulling pend the message (bounded); anything else starts a pull and pends the message.
A {:grant, key, blob} arrived (in-session — the envelope guarantees it).
live? is the embedder's answer to "does this key have a live process".
Never injected this session and not live → inject + ack + release pends;
otherwise → ack without inject (the in-session duplicate-ack
discipline, spec InjectGuard, extended to inject-at-most-once — see the
moduledoc).
A {:not_here, key} arrived: escheat is authorized for this key, this
session — recorded sticky. If the key has an outstanding pull (waiters),
escheat now and release the pends; if it is live (a duplicate grant won the
race) or nothing is waiting, just record — the next first_touch/3
escheats without a round trip.
A {:push, key, blob} arrived (background sweep). Identical discipline to
handle_grant/4 — the spec's RecvPullResp and RecvPush are the same
action over different message types, and a sweep push may race a pull grant
for the same key.
Create the recipient machine at handoff_in(session).
Messages pended for key, in arrival order.
Is a pull outstanding for key?
The session is over (the embedder observed settle or abort — the
handoff_in(nil) transition: prev_owner = NULL). Every still-pulling key
becomes escheat-authorized and escheats, releasing its pends. Terminal.
Pull-retry tick (the embedder's retry-cadence seam timer): re-emit
{:pull, key} for every key still pulling. Never escheats, never gives up
(⊨ rule 1: retry forever until :not_here or session-over).
Types
@type event_result() :: {[Fief.Transfer.effect()], t()}
@type t() :: %Fief.Transfer.Recipient{ arrived: MapSet.t(Fief.Transfer.key()), authorized: MapSet.t(Fief.Transfer.key()), max_pending: pos_integer(), pulling: %{required(Fief.Transfer.key()) => [Fief.Transfer.pended()]} }
pulling— key → pended messages (reversed arrival order), for keys with an outstanding pullarrived— keys injected at least once this session (the inject-at-most-once guard: a frozen blob is stale once its process has run)authorized— keys whose escheat is authorized for this session (:not_herereceived; sticky)
Functions
@spec arrived?(t(), Fief.Transfer.key()) :: boolean()
Was key injected at least once this session?
@spec escheat_authorized?(t(), Fief.Transfer.key()) :: boolean()
Is escheat authorized for key this session?
@spec first_touch(t(), Fief.Transfer.key(), Fief.Transfer.pended()) :: event_result()
A message arrived for a key with no live process (the embedder checks liveness first; live keys are delivered directly and never reach the machine). Escheat-authorized keys escheat immediately (sticky authorization); keys already pulling pend the message (bounded); anything else starts a pull and pends the message.
@spec handle_grant(t(), Fief.Transfer.key(), Fief.Transfer.blob(), boolean()) :: event_result()
A {:grant, key, blob} arrived (in-session — the envelope guarantees it).
live? is the embedder's answer to "does this key have a live process".
Never injected this session and not live → inject + ack + release pends;
otherwise → ack without inject (the in-session duplicate-ack
discipline, spec InjectGuard, extended to inject-at-most-once — see the
moduledoc).
@spec handle_not_here(t(), Fief.Transfer.key(), boolean()) :: event_result()
A {:not_here, key} arrived: escheat is authorized for this key, this
session — recorded sticky. If the key has an outstanding pull (waiters),
escheat now and release the pends; if it is live (a duplicate grant won the
race) or nothing is waiting, just record — the next first_touch/3
escheats without a round trip.
@spec handle_push(t(), Fief.Transfer.key(), Fief.Transfer.blob(), boolean()) :: event_result()
A {:push, key, blob} arrived (background sweep). Identical discipline to
handle_grant/4 — the spec's RecvPullResp and RecvPush are the same
action over different message types, and a sweep push may race a pull grant
for the same key.
Create the recipient machine at handoff_in(session).
Options: max_pending: — pend-queue bound per key (default 128, the
max_pending_per_key of implementation.md §9).
@spec pending(t(), Fief.Transfer.key()) :: [Fief.Transfer.pended()]
Messages pended for key, in arrival order.
@spec pulling?(t(), Fief.Transfer.key()) :: boolean()
Is a pull outstanding for key?
@spec session_over(t()) :: event_result()
The session is over (the embedder observed settle or abort — the
handoff_in(nil) transition: prev_owner = NULL). Every still-pulling key
becomes escheat-authorized and escheats, releasing its pends. Terminal.
@spec tick(t()) :: event_result()
Pull-retry tick (the embedder's retry-cadence seam timer): re-emit
{:pull, key} for every key still pulling. Never escheats, never gives up
(⊨ rule 1: retry forever until :not_here or session-over).