R6.1 transfer-authority model — written before the mechanism

R6's first pass (receipts/R6-EXECUTED.md) earned one sentence: a Locus's state is the complete transferable token of its currentness, and a token that is bytes cannot refuse its own copy. S2/S9 showed the composed two-floor system installing one duplicated 317-byte record on both floors and both floors becoming current. The floor's half held everywhere it was attacked; the missing invariant lies outside either floor.

This document fixes two things the first pass said badly, then states the mechanism R6.1 builds to close F87 — as a mapping onto the frozen R0.8 durable layer, executed, not cited — and names every intermediate state a move can be caught in.

0. Taxonomy, corrected before anything is built

R6-OPEN §2 wrote "a core is a carrier". That welds a semantic identity to a physical placement, and S3b is the evidence against it: a Suspended Locus moved to another floor still RECOVERed against carrier C17, because nothing anywhere says C17 lives on core 2 — Carrier identity was never defined as CPU placement. The correct picture keeps three things apart:

physical core          an execution location                      (R6 pins one floor per core)
   └─ floor instance   one kernellet image: private TABLE/ROWS/stack, run-to-completion,
                       no shared mutable state with any other floor.  Named by a FLOOR ID.
        └─ may host    a Carrier  C17   the replaceable execution embodiment a Locus attaches to
                          └─ Locus L    the semantic unit: possession, generation, fence, authority set

• core ≠ Carrier. floor ≠ Carrier. A Carrier may be placed, migrated or

restarted on another floor/core without becoming a new semantic Carrier.

• Relocating a Locus between floors is not Carrier succession and does

not advance the lifecycle generation. ATTACH does not advance the generation either; DETACH and FINALIZE do (+1). Physical placement is not semantic succession.

• S3b is therefore not fixed by making `CarrierId` a `(floor, id)` pair,

and this round does not. A Suspended Locus keeps custody for the same CarrierId across relocation. What a later placement layer must supply is evidence that the named Carrier is runnable at the destination before RECOVER is operationally meaningful. That evidence is not built here.

• The first-pass rule stands: **an Attached Locus is not relocated

directly.** It becomes Vacant (DETACH), Suspended (SUSPEND) or is finalized (FINALIZE) through the existing lifecycle first.

MOVE_OUT / MOVE_IN stay measurement-profile mechanisms (feature move, gated like bench), not canonical lifecycle verbs. The canonical sentence is relocate a non-attached Locus between execution domains while preserving its lifecycle state.

1. Currentness, restated

R6-EXECUTED §1 said "currentness across cores is the fabric's linearity". That was the wrong abstraction: the fabric is the adversary (it delays, drops, duplicates, reorders, corrupts — R6-OPEN §1), and a correctness argument that needs the adversary to behave has weakened the design. The statement this round is built on:

The transport may duplicate the bytes. The transfer authority must be linear. Delivery of a record is not entitlement to install it.

Which continues a family of separations already in the tree:

reachability  ≠ authentication        (R0.9)
authentication ≠ authority            (R0.4)
evidence      ≠ currentness           (R3)
transport delivery ≠ transfer authority   (this round)

And the first-pass claim "no shared global semantic state" is narrowed to what the battery actually supported: no shared mutable semantic state is needed inside the per-core floor instances. The composed multicore system does need one globally coherent fact — which of many byte-identical copies of a transfer may be installed — and that fact is load-bearing. It is not hidden under the word "fabric". It cannot live in the copied bytes: a consumed flag inside the record is defeated by copying the record before it is set, and a destination id inside the record is defeated by duplicating it to that destination. It must live where a copy cannot take it: a durable revision store with fork refusal, an OS lock, a hardware queue, or an unforgeable capability. R0.8 already built the first of those.

2. The mapping: a Locus's placement is an R0.8 lineage

R0.8 (frozen at e42cc88) holds, per Locus, one durable lineage: a copyable descriptive store, a root that commits to the exact canonical history by SHA-256 and carries the pending transition, an anchor outside every movable copy that pins revision/head and the one successor it authorized, and an incarnation lock a copy cannot carry. Its refusals are the ones a transfer needs:

So the placement of Locus L is modelled as an R0.8 lineage whose carrier column holds a floor id — the holder of L's state — and whose transitions are the existing ones:

genesis        attach(F0)      req=genesis          placement = resident(F0)
relinquish     detach          req=take:<move>      placement = in-transfer(<move>)   (Vacant, placement generation +1)
redeem         attach(F1)      req=redeem:<move>    placement = resident(F1)

The holder id the lineage records is what the presenting floor says it is: the adapter does not authenticate floors, and under a bearer capsule whereis names a holder on the presenter's word. Reachability ≠ authentication applies to the carrier column as it does everywhere else; a placement-domain authentication of floors is not built in this round.

This is a second lineage, kept in its own anchor namespace and under its own placement-domain mark. It is not L's lifecycle lineage: L's generation, fence, possession and Carrier travel inside the payload, untouched. The placement lineage's generation counts relocations; L's counts successions. Using the lifecycle algebra one rung up is a proposal for adjudication, not an assertion: the property needed — exactly one holder, replaceable only through Vacant — is the possession algebra, and the frozen semantics supply it unmodified. R0.8 is not changed; the adapter drives the frozen `cd-durable` binary.

2.1 The move id binds the authority to one payload

move = SHA-256("cd-transfer/1" ‖ locus ‖ from_floor ‖ to_floor ‖ placement_revision_before ‖ payload)[..16]

The take's request id is take:<move>; the placement head after the take commits (through R0.8's canonical material) to that request id; the capsule carries (revision, head) after the take. Hence: head ⇒ this take ⇒ this move id ⇒ these payload bytes, this source, this destination. A capsule whose payload was altered fails the digest before the placement is opened; a capsule re-digested by an attacker carries a move id the head does not commit to and fails the head check; a capsule from an earlier move carries a revision the placement has passed.

What R0.8 does not do, and the adapter must. The root CAS binds a successor to the current head, not to a take's identity: an attach under any request id the ledger has never seen commits on a vacant placement. So the binding of a redemption to its take is adapter code and is load-bearing: the digest check (payload ⇒ move id) and the ledger probe — detach req=take:<move> must answer already-applied (R0.8E: recognised, never re-executed; a new id on a vacant placement is refused by cd-core and moves nothing durable). The probe is only ever sent after the placement has been read as vacant under the lock, because on an attached placement a never-seen id would execute a real detach. Found by probing a capsule that copied the true (revision, head) from whereis over a garbage payload with a self-digested move id: a head-equality check alone let it claim. The battery's unchecked-claim control disables the adapter's pre-check and probe to show which refusals are R0.8's own (already-applied, request-id-conflict, locus is attached, not vacant) and which are the adapter's.

Which mapping rows the battery executes: the fork and superseded rows are exercised only as they arise in the crash and race cases (T2, T3); the ledger, lock and possession rows are fired directly (T1b's control, T2's held lock, T3); the CAS row is what makes the crash windows behave as T3 gates.

to_floor may name a floor or be ANY (a bearer capsule). The battery runs F87 in both modes, because a refusal that depends on the destination id alone is not the refusal this round is after: with ANY, a duplicate at a third floor must be refused by consumption (NotVacant / request-id conflict), not by address.

2.2 The capsule is not a wire format

"CDTA" ver=1 pad[3] | locus 16 | move 16 | from 16 | to 16 | revision u64 | head 64 (hex) | len u16 | payload (317 B kernellet record)

The payload is the R6 record, which carries the World mark; the transport in this round is the trusted harness on one host, as in R6, and the capsule is a trusted measurement representation. It is not sealed, because nothing untrusted sees it; the moment bytes cross an untrusted boundary, the payload must become a capability-bearing sealed capsule with the mark structurally inaccessible — the opposite class from the deliberately public R3 LifecycleEgressV1, which must not be reused here.

3. The protocol, and why the order is load-bearing

SOURCE floor F0                      TRANSFER AUTHORITY (R0.8 placement lineage)          DESTINATION floor F1
 1  MOVE_OUT(slot)   -> record       │                                                    │
    (F0 now has nothing: S1)         │                                                    │
 2  relinquish(record) ─────────────►│ detach req=take:<move>      in-transfer            │
 3  capsule leaves ── adversarial transport: delay / drop / copy / reorder / corrupt ────►│ 4  redeem(capsule):
                                     │                                                    │    parse, digest, destination,
                                     │◄──────────────────────────────────────────────────┤    state == (vacant, revision, head)
                                     │ attach(F1) req=redeem:<move>   resident(F1)        │    -> ok
                                     │                                                    │ 5  MOVE_IN(slot, record)

• MOVE_OUT before relinquish. If the order were reversed there would be

a window where the placement says in-transfer while F0 still holds L and can act on it; after F1 redeems, two floors act. NC2 keeps that defect reproducible.

• Claim before install. If a floor installed first and claimed

second, a slow floor could act on L in memory while another floor redeemed a duplicate and committed. Possession follows the commit: a floor may not act on L until its own redemption committed.

• **The authority is consulted once per redemption, by the floor that

installs.** No floor reasons about another floor; the placement lineage is the only thing that knows more than one floor exists.

4. Every intermediate state, named

whereis(L) answers from the placement lineage alone — through a controller open, which when it takes the lock may complete a pending claim (R0.8 rolls forward during open), so a read may finish a write — and has exactly two values: RESIDENT(floor, revision) or IN_TRANSFER(revision, head). "Resident nowhere" is not a reachable answer in this model. The states a move can be interrupted in, and what each means:

A sub-case is named and deferred rather than built: a claimant that is alive, in the same incarnation, and provably holds nothing could re-install from the capsule soundly, because an installed L can only leave a floor through the placement. That needs a floor incarnation identity, which does not exist yet.

5. Refusal codes of the adapter (tools/r61_transfer.py)

MALFORMED (frame, or revision 0) · PAYLOAD_MISMATCH (digest) · WRONG_LOCUS (the payload's carried Locus ≠ the capsule's) · WRONG_DESTINATION (addressed capsule at another floor) · NOT_IN_TRANSFER (placement is resident) · ALREADY_CONSUMED (this transfer was redeemed: revision+1, attached) · STALE_TRANSFER (the placement has moved past this transfer) · AUTHORITY_MISMATCH (same revision, different head — a fork or a re-digested capsule) · CONTENDED (another redeemer holds the incarnation lock) · NOT_HOLDER (relinquish by a floor that is not the holder) · INSTALL_REFUSED_AFTER_CLAIM (the floor refused a record the checks passed — must never fire; if it does, the placement is RESIDENT_HOLDER_UNINSTALLED).

Refusals before the placement is opened (MALFORMED, PAYLOAD_MISMATCH, WRONG_LOCUS, WRONG_DESTINATION) leave the lineage untouched by construction — the adapter has not spawned the controller yet.

A refusal R0.8 gives at open — superseded, fork, one-ahead, in-flight, or store is not the canonical history the root commits to — is never relabelled. A read-only open reads the store, the root and the anchor as three files with no lock, so it can read one of them before, and the next after, another incarnation's commit and be refused with the very string a genuinely stale or doctored history produces. Both torn pairs were measured in the race battery: the store already at the winner's revision while the root still named the prior one (the more frequent), and the root before and the anchor after a finalize. The adapter re-opens a bounded number of times and lets R0.8 answer again; a persisting refusal is reported as given. That a read-only open is not linearizable against R0.8's three-file commit is a finding about using open as a read, recorded, not repaired here.

6. Falsifiers

• F87 a duplicated capsule installs twice — at the source, at the same

destination again, or at a third floor — in either capsule mode, or a refusal depends on the transport having dropped the duplicate.

• F88 two concurrent redemptions of the same transfer both succeed.

• F89 a crashed redeemer's claim is erased, or a crashed redeemer's

claim lets a second floor install (split brain through the crash window).

• F90 a relinquished, undelivered transfer reads as resident or as

nowhere, or a capsule for it can be minted without the payload.

• F91 a delayed original redeems after a copy has.

• F92 a corrupted payload, or a re-digested capsule, or a capsule whose

authority is L-A's and whose payload is L-B's, reaches the placement lineage or the floor.

• F93 a consumed transfer redeems after the Locus has moved again.

• F94 relocation advances L's lifecycle generation or transition count,

or the 176 + 133 bytes arrive changed.

• F96 a lineage refusal at open is relabelled as contention, or the

race battery goes green without ever observing the lock.

• F95 the negative controls stop reproducing their defect: the

first-pass record path (S2/S9), relinquish-before-MOVE_OUT, and a consumed flag inside the capsule.

• F86 (kept) the move profile leaks into the production image.

7. Predictions, before the battery

• F87 holds in both modes; the third-floor refusal under ANY is

ALREADY_CONSUMED by NotVacant or request-id conflict, never by address.

• Concurrency: exactly one REDEEMED; the loser sees CONTENDED on the

race and ALREADY_CONSUMED on retry, and contention is observed in at least one round and forced in one. R0.8's flock is the serializer.

• Under the unchecked-claim control, a never-seen request id on a consumed

placement is refused by possession (not vacant) at every floor.

• Crash windows follow R0.8's eight points exactly: before-commit and

after-anchor-pending leave the transfer open; every later point leaves resident(F1) with an uninstalled holder and a consumed capsule, and the second floor's open reports what it did by R0.8's own label (unused-reservation-cancelled, pending-transition-rolled-forward, pending-transition-committed-and-finalized, lineage-advanced-to-authorized-successor, or clean).

• Relocation does not move L's generation or transitions; 100 relocations

of a Vacant L leave both unchanged while the placement generation is +100.

• The three negative controls reproduce their defects.

• The cost of a redemption through a spawned cd-durable over SQLite is

milliseconds, three to four orders above the 2,285-instruction move; it is a baseline for an adapter, not a floor for the mechanism.

8. Precedent — the same separation, elsewhere

Every system found that faced this problem put the single-consumption fact in a ledger the copier cannot fork, keyed by an identity plus a monotonic generation or a compare-and-swap on the ledger's own prior value; none put it in the payload.

• Barrelfish serialises a capability as bytes for cross-core transfer

("copying the bytes … is sufficient for serialization") and makes an owning core the synchronisation point; transfer is a monitor-only operation under two-phase commit so all cores agree on one ordering (Baumann et al., The Multikernel, SOSP 2009 §4.7; Nevill, An Evaluation of Capabilities for a Multikernel, ETH 2012 §2.1–3.1). Its documented failure is the shape R6 exhibited: a revoke completes while a copy is still in flight to a third core (Barrelfish TN-013 §6.1.3).

• SemperOS allows one kernel to own a resource and delegates by a

two-way handshake so the child capability exists only after the owner recorded it — exactly claim before install (Hille et al., USENIX ATC 2019 §3.3, §4.3.2, and its table of orphaned/invalid windows).

• Zircon moves a handle by closing it in the sender inside

zx_channel_write; the kernel handle table is the authority and a handle value is meaningless in another process.

• Chubby sequencers and fencing tokens (Burrows, OSDI 2006 §2.4;

Kleppmann 2016): the resource checks a lock generation and rejects a request whose token has gone backwards; Kafka fences a zombie producer by a persisted producer epoch (ProducerFenced). The R0.8 revision plus the request ledger play the same role for a placement.

• QUIC (RFC 9000 §9.3.3) states the residual window plainly: a

forwarded copy that arrives first looks like a genuine migration and "this defense is imperfect"; what confers nothing durable is that the highest-numbered genuine packet moves the endpoint back. R6.1's equivalent is T5: which floor wins is the transport's order; that exactly one wins is the authority's.

• Orleans documents occasional duplicate activations under its default

directory and moved to versioned range locks; Akka cluster sharding hands off through a singleton coordinator with a time margin; Erlang `global` resolves a healed partition by killing one registrant. All three are the cost of not having the fact durable and checked at install.

9. Adjudicated (2026-09-05) — what stands, what was amended

R6.1 was accepted as the closure of F87. Standing after the ruling:

• §0 taxonomy and §1 statement: accepted, with one narrowing — the

globally coherent fact is coherent per Locus / per placement lineage, never one system-wide serialization point. Disjoint Loci remain independently movable. Standing sentence: per-core floors share no mutable semantic state; cross-floor exclusivity is supplied by a coherent per-Locus transfer authority whose payload may traverse an adversarial, duplicating transport.

• §2 mapping: accepted **as the R6.1 mechanism and as proof that R0.8 is

the sufficient durable substrate**. "Placement is lifecycle one rung up" is not canonized: the crash windows (§4) showed two histories — claimant dead before install, holder dead after acting — sharing one stored state while needing different futures. That is the evidence for a placement phase beyond possession, taken up in docs/placement-activation-model.md (R6.2).

• §4 vocabulary: RESIDENT is retired — it named the holder and

implied presence. The authority-side answer is a phase (ACTIVE, CLAIMED, IN_TRANSFER) and materialization is reported separately. RESIDENT_HOLDER_UNINSTALLED was the observed predecessor of CLAIMED_UNINSTALLED.

• §2.1 attribution stands as the standing description: R0.8 supplies

durable linear history, fork refusal, request-id semantics, crash reconciliation and incarnation serialization; the adapter supplies move/payload binding, Locus binding, destination policy and transfer interpretation. Do not write that R0.8 understands a move.

• §5 torn reads: the discipline stands — re-open, never reinterpret the

frozen refusal string; the durable layer is not changed for it.