Fief.Transfer (Fief v0.1.0)

Copy Markdown View Source

The lazy-pull key-migration protocol of design.md §6.3 as two pure state machines — Fief.Transfer.Donor and Fief.Transfer.Recipient — the one place the ⊨ rules are implemented (implementation.md §1 Decision, §7). Every rule here has a TLC counterexample behind it (specs/FiefTransfer.tla); a third-party vnode impl that wants incremental migration embeds these machines rather than re-deriving them.

Key-generic transfer substrate: built purely on the public Fief.Vnode behaviour, with no dependency on Fief.Key — the machines see only opaque keys and blobs, never a key module — so any stateful vnode impl can embed this protocol (see guides/extending/migration-embedding.md). The module name mirrors the TLA+ spec that model-checks it, specs/FiefTransfer.tla. Fief.Key.VnodeImpl is the sanctioned embedder: it wires these machines to Fief.Key's key→pid map, limbo interplay, and cold-start origin discipline (init/3 with ctx.origin).

The layer split

The machines implement the decision half of the protocol. The framework's agent envelope (implementation.md §6.2, built at M4) owns the transport half and guarantees, before any machine event fires:

  • peer messages are delivered only when they match the current session — a stale-session grant/push is dropped without ack before the impl sees it (the transport half of ⊨ rule "session-scoped handover");
  • handoff_out/handoff_in arrive in authoritative-observation order, and impl state persists across them (what makes taint implementable from the donor's own memory).

So the machines assume every input is in-session, but must survive loss (a grant/push/ack may never arrive), reordering, and in-session duplicates (a re-served pull grant may race a sweep push for the same key). The machines are per-session by construction: created at the handoff observation, discarded when the session ends — they carry no session tuple (Decision: the embedder owns the session; {:peer, _} effects go to the session counterpart via Fief.Vnode.send_peer/2).

Purity

Structs plus event functions returning {effects, machine}. No processes, no clock reads, no sends, no timers, no randomness. Time arrives as explicit tick/1 events (the M6 embedder drives them from seam timers: sweep cadence on the donor, pull-retry cadence on the recipient). Key liveness is an input, not machine state (Decision): the embedder owns the key→pid map, calls first_touch only for keys with no live process, and passes live? to the delivery events — the machines track migration-protocol status, never pids.

Peer-message vocabulary (the payloads of Fief.Wire.peer/2 envelopes)

  • {:pull, key} — recipient → donor: first-touch handover request
  • {:grant, key, blob} — donor → recipient: pull answer, state attached
  • {:not_here, key} — donor → recipient: key not in the residual ledger; authorizes escheat for this key, this session (⊨ rule 1)
  • {:push, key, blob} — donor → recipient: background sweep
  • {:ack, key} — recipient → donor: blob delivered; the donor may drop the retained residual

Blobs are fully opaque (whatever the user's extract_state/1 returned).

Effect vocabulary

Effects are plain data, interpreted by the embedder in list order:

  • {:peer, payload} — send payload (vocabulary above) to the session counterpart (Fief.Vnode.send_peer/2)
  • :report_drained — donor only, emitted exactly once, when the residual ledger empties (⊨ rule "settle is donor-reported"): Fief.Vnode.report_drained/1
  • {:inject, key, blob} — start a key process from transferred state (the key's init/3 with a {:residual, blob} source)
  • {:escheat, key} — rebuild the key from durable truth (the key's init/3 with a :fresh source and :escheat origin); only ever emitted when authorized (⊨ rule 1)
  • {:resume, key, blob} — donor regained ownership: restart this never-shipped residual as a live process
  • {:discard, key} — donor regained ownership: this residual was shipped and is tainted — do not resume; the key escheats on next touch
  • {:release, key, messages} — deliver pended messages, in arrival order, to the key process the preceding inject/escheat effect started
  • {:overflow, key, message} — the pend bound was hit; the message is dropped and the caller times out (design §6.3's stated semantics)

⊨ rules, mapped (design §6.3 / specs/FiefTransfer.tla)

RuleWhere
Escheat gated: :not_here or session-over, never a pull timeoutRecipient (handle_not_here/3, session_over/1; tick/1 only re-pulls)
Settle on donor report, only when emptyDonor (:report_drained exactly when the ledger empties)
Session-scoped handover, stale inject dropped without acktransport half: agent envelope (M4); duplicate-ack half: Recipient (handle_grant/4, handle_push/4 — ack-without-inject when live or ever injected this session, spec InjectGuard extended to inject-at-most-once; see the Recipient moduledoc)
Taint on reacquisition: shipped (acked or not) discarded, never-shipped resumedDonor.regained/1
Residuals retained until acked; in-session re-serve/re-push safeDonor (handle_pull/2, tick/1, handle_ack/2)
Exactly-one-live-process-per-keyledger holds only retired state (freeze precedes the machine); grants/pushes come only from the ledger; recipient injects at most once per key, and only when not live

Decision: Fief.Transfer.Channel — the blob-transport behaviour with the 64 KB max_blob_size cap (implementation.md §7) — is deliberately deferred to M6, where the embedder that would call it exists. The machines never see blob sizes; blobs are opaque here.

Summary

Types

blob()

The opaque per-key state term produced by extract_state and handed back to init/3.

effect()

What the embedder interprets, in list order (moduledoc).

key()

A user key. Opaque to the machines.

peer_msg()

The peer-payload vocabulary carried inside Fief.Wire.peer/2.

pended()

A message pended for a key mid-pull. Opaque to the machines.

Types

blob()

@type blob() :: term()

The opaque per-key state term produced by extract_state and handed back to init/3.

effect()

@type effect() ::
  {:peer, peer_msg()}
  | :report_drained
  | {:inject, key(), blob()}
  | {:escheat, key()}
  | {:resume, key(), blob()}
  | {:discard, key()}
  | {:release, key(), [pended()]}
  | {:overflow, key(), pended()}

What the embedder interprets, in list order (moduledoc).

key()

@type key() :: term()

A user key. Opaque to the machines.

peer_msg()

@type peer_msg() ::
  {:pull, key()}
  | {:grant, key(), blob()}
  | {:not_here, key()}
  | {:push, key(), blob()}
  | {:ack, key()}

The peer-payload vocabulary carried inside Fief.Wire.peer/2.

pended()

@type pended() :: term()

A message pended for a key mid-pull. Opaque to the machines.