Hot Swap That Refuses Unsafe State Migration: Typed Hand-Off and the No-Laundering Rule

Pitch

Erlang's code_change hands state from old code to new and trusts the new module to cope; revl checks the hand-off type at admission, before teardown, so a mismatch is refused with the running composition untouched, and it refuses to carry state across a cold-start path.

Abstract

Hot code replacement is only useful if long-lived state survives it, and only safe if the new code can actually hold that state. Erlang/OTP leaves the decision to a user-written code_change callback; dynamic software updating systems such as Ginseng, Kitsune and Proteus verify state transformers against types or update points, usually for C programs. We describe the state transfer protocol of revl, a language whose components acquire resources through effects with declared inverses and are hot-swapped in a running composition. A swap drains in-flight calls, captures state, tears the old provider down in derived LIFO order, loads the successor and restores. Two channels carry state. Live instances of a spawned template migrate through a snapshot and restore protocol (__revl_state__ and __revl_restore__) gated by a same-length, same-type check on the resource vector. Composition-level providers declare a handoff type; the admission gate checks the successor's accepted type against the predecessor's exported type with the same compatibility relation used for interface drift, refuses a mismatch with a trace that names both shapes before teardown, and threads the value into the successor on success. The instance channel checks the whole cohort before writing and rolls the swap back on rejection; a defence-in-depth check on the hand-off path also rolls back. State never crosses a respawn or a rollback (the no-laundering rule), and an agent-authored successor receives operator state only through a declared and type-compatible hand-off. We document one unfixed hazard, same-typed resources reordered by a successor, pin it with a test, and list the evidence on main: 13 test functions in the hand-off grammar and gate file (8 gate, 5 grammar and parse), 4 execution tests, 7 undo-dossier tests, and 4 instance-migration tests. These are counted from the files, not run for this draft.

Problem and claim

A stateful provider (a cache, a session store, a rate limiter) loses its world when the old version is torn down. The swap then degrades to restart with extra steps and no diagnostic. The two usual cures both have a hole. Trusting the successor to accept any state, as OTP does, lets a type mismatch surface later as wrong data. Positional or structural migration, as in many live-reload tools, can silently put state in the wrong slot.

The claim: a swap can be made all-or-nothing with respect to state, for the shapes the gate can see. Either the successor is checked to accept the predecessor's exported shape (checked at admission, re-checked on the live resource vector as defence in depth), or the swap is refused and the running composition is exactly as it was. And the negative half: no path that starts the successor cold (respawn, rollback, undo) carries state, because carrying it would launder one generation's writes into the other generation's code.

What the paper does not claim: that the declared hand-off type is a full behavioural contract (it states shape, not meaning), or that instance migration is sound when a component holds two resources of one type (that case is a known, pinned wrong result).

Contributions

1. A snapshot and restore protocol for effect-acquired resources with a same-length, same-type gate and cohort-wide check-then-apply, with rollback on rejection (StateIncompatible).
2. A declared hand-off (a prelude declaration, one per component, additive IR field) whose type reads as "exports" for the predecessor and "accepts" for the successor, checked with the covariant case of the existing compatibility relation; correlation by provided key, so renamed successors still match.
3. The no-laundering rule: respawn, cold start, rollback and undo carry no state, and the undo report names the state it drops. Under the declared policy an agent-authored successor receives state only through a declared, type-compatible hand-off.
4. A named and test-pinned hazard (same-typed resource reorder under positional migration) with the narrowed fix stated.
5. A statement of what instantiation as acquisition does not give: request-scoped instances leak without sub-component teardown scopes.

Related work

Evidence on main

Numbers that exist

• Test counts by file on main: tests/test_state_handoff.py 13 test functions (8 gate: admitted, widened, narrowed, incompatible, refusal trace, renamed, no-handoff, cold-key; 5 grammar and parse: parses and lowers, absent, must target a key, must precede effects, at most one), tests/test_state_handoff_exec.py 4, tests/test_instance_migration.py 4 named (lines 113, 140, 165, 235), tests/test_mcp_undo_handoff_state_2346.py 7, tests/test_service_compat.py 16. These are counts of test functions, not run results; none were run for this draft.
• No performance or scale measurement of capture, restore or swap latency exists in the files read. No corpus of real swaps.

Paper outline

1. Introduction and the state loss problem on hot swap.
2. Background: components, effects with inverses, derived LIFO teardown, swap and admission.
3. Two channels: instance migration (snapshot protocol, same-type gate) and declared hand-off (exports and accepts, covariant check, key correlation).
4. Atomicity: capture before teardown, check the cohort before applying, rollback; defence in depth.
5. No laundering: respawn, rollback, undo; the declared policy for untrusted successors.
6. Hazards: same-typed reorder (pinned), request-scoped instance leak.
7. Evaluation (to be done), comparison with OTP code_change and DUS systems.
8. Limits and conclusion.

Threats to validity and limits

• A declared type states shape, not meaning. A successor that accepts Map[Str, Str] but reinterprets keys passes the gate. The paper must not claim semantic safety.
• The instance channel is positional and has a pinned wrong result for same-typed reorders; the design doc calls it a "Named hazard (canonical, not yet closed)".
• Everything executed is on cordis-py. The state protocol on the other five tiers was not checked for this draft.
• The widened-acceptor rule (Opt[T] accepts T) relies on the compatibility relation; its soundness here is by reuse of that relation, not a new proof.
• There is no state transformer: a change of representation cannot be expressed, so the only options are a compatible type, an opt-out cold start, or a refusal. This is a design choice that limits expressiveness relative to code_change and DUS transformers.
• The leak with request-scoped instances means "instantiation is acquisition" is only partly true today.
• No measurements exist.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 19 checked, 5 corrected.

Cite this draft

@misc{revlp24,
  author       = {Thomas Moussajee},
  title        = {Hot Swap That Refuses Unsafe State Migration: Typed Hand-Off and the No-Laundering Rule},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P24.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.