Distributed Invariants as Obligations: How Far the Type System Gets

celld runs Cloudflare Durable Objects on your own machines. A cell’s owner is one object in an S3 bucket, claimed by a conditional PUT, and the epoch that comes with the claim is baked into the object prefix — so a node that loses the race writes into a prefix nobody will ever read.

It is a good fence, and it is a fence made of consequence. The losing node still runs. It still calls its write path. It is merely writing somewhere that does not matter, and it never finds out. Correctness is established after the fact, as a property of where the bytes landed.

An obligation is a fence made of admission.

The lease

cas.claim is the only event that mints <lease!>.

pub tor cas.claim { node: string, guard: i64 }
| applied string<lease!>
| rejected

cas.claim = if(guard == own.etag)
| then |> std/store:stored { own.etag: own.etag + 1, own.epoch: own.epoch + 1 } => applied node
| else => rejected

The data path borrows it. An input typed <lease> reads the token without discharging it, so one lease admits many writes — and no lease admits none.

pub tor cell.write { lease: string<lease>, cell: string, data: string }
cell.write = std/io:print.ln("  {{ lease:s }}  write e{{ own.epoch:d }} {{ cell:s }} <- {{ data:s }}")

Giving it back consumes it.

pub tor cas.release { lease: string<!lease> }
cas.release = std/io:print.ln("  {{ lease:s }}  release")

Two nodes race for one cell. The second reads the record before the first writes, so its guard is stale and its claim is refused; it re-reads and takes over at the next epoch.

node-a  cas guard=0
  node-a  write e1 room-42 <- hello from a
  node-a  release
node-b  cas guard=0 (stale)
  node-b  rejected — etag moved
node-b  cas guard=1 (takeover)
  node-b  write e2 room-42 <- hello from b
  node-b  release

The last line is the interesting one, because nobody wrote it. <!lease> has exactly one consumer, so the compiler inserts the release at scope exit and a lease cannot be leaked by forgetting. celld buys the same property with a ten-second TTL, a renewal timer at a third of it, a fence timer just past it, and a self-fence that halts the process.

The gate

celld’s Durable Objects claim RPO=0, and the mechanism is that a handler which commits does not get to answer. The response waits until the replicator proves a position in the bucket, and it is acknowledged only if the proof covers the write; a shorter proof from a lagging replicator fails it rather than acknowledging something the node could not restore.

That is a rule about a value’s lifetime, so it is an obligation. A commit mints <pending!> — an unanswered response — and there are exactly two ways to discharge it.

pub tor gate.ack { r: string<!pending>, proof: i64<!durable> }
gate.ack = std/io:print.ln("  ack  {{ r:s }} — durable through {{ proof:d }}")

pub tor gate.fail { r: string<!pending>, why: string }
gate.fail = std/io:print.ln("  fail {{ r:s }} — {{ why:s }}")

Acknowledging consumes the response and a <durable!> proof, which only the replicator mints. One proof covers one gated write.

node-a claims the cell
  held msg-1 at pos 1 — response gated
  ack  msg-1 — durable through 1
  held msg-2 at pos 2 — response gated
  fail msg-2 — durability unproven
  release node-a

msg-2 committed perfectly well. It was failed rather than acknowledged because no proof could reach its position.

Now compare the two resources. A lease has one way back, so the compiler inserts it for you. A response has two, so the compiler refuses to choose and every request’s fate has to be written down. Neither behaviour was designed in; both fall out of counting the consumers. And both are right: silently dropping a request and silently acking one are the same lie in different directions, which is why celld’s fence walks its pending writes and completes each one as explicitly failed.

Authority

A node holds its authority as a lease too, and it can end two ways. Renewal borrows it. Fencing consumes it. Nothing in the names carries that difference.

pub tor node.renew { lease: string<lease> }
node.renew = std/io:print.ln("  renew {{ lease:s }}")

pub tor node.fence { lease: string<!lease> }
node.fence = std/io:print.ln("  SELF-FENCE {{ lease:s }} — lease not renewed within TTL")

Then acknowledging asks for the lease as well:

pub tor gate.ack { r: string<!pending>, proof: i64<!durable>, lease: string<lease> }
gate.ack = std/io:print.ln("  ack  {{ r:s }} — durable through {{ proof:d }}")

Surrender the lease and gate.ack is simply unreachable, so a pending response has one way out left.

  renew node-a
  ack  msg-1 — durable through 1
  SELF-FENCE node-a — lease not renewed within TTL
  fail msg-2 — node fenced

celld states this invariant in a comment — the fence and the fail are atomic — and it holds because a loop walks every gated write and fails it, and because nothing else in the codebase builds a success. Here it holds because no other shape of program exists. The sharp case is a genuine durability proof, minted by the replicator, covering the position exactly: the acknowledgement is still refused, because authority went first.

The part that did not survive

Three ports from one system is one witness, and celld is the worst possible one: it is the only system in this survey that advertises a pure decision core, in a Cargo.toml comment. A project that advertises a property has selected itself for that property.

So: three more, read at source rather than from their documentation.

The architectural claim does not survive that. ZooKeeper is mature, correct, and in production everywhere, and it never needed a decision core to be right.

What does survive, four for four, is narrower and more useful: the correctness-bearing computation is pure in every one of them. ZooKeeper’s majority test is return (ackSet.size() > half);. Raft’s commit index is a median over an array with no I/O anywhere near it. TigerBeetle’s state machine imports no clock; its timestamps arrive as data in the replicated record. Whether a codebase separates that computation is house style. That it is pure appears not to be.

Where it stops

All three of the other systems nominated the same invariant as the one a linear type should not reach: the quorum.

An ack is a resource. It is minted once per peer and consumed by counting it, which means counting the same one twice does not compile — and that is not a small thing, since double-counting an agreement is the classic quorum bug. Raft keys its match indexes by server id; ZooKeeper holds a Set<Long> and types its majority test to take one; TigerBeetle, which uses a plain counter, needs a dedicated flag and a helper with the words exactly once in its name.

pub tor peer.matched { id: i64, index: i64 } -> i64<ack!>
peer.matched -> index

pub tor tally.count { ack: i64<!ack>, from: i64 }
tally.count = std/store:stored { raft.counted: raft.counted + 1, raft.best: ack }
    |> std/io:print.ln("  counted ack from peer {{ from:d }} at index {{ ack:d }}")

The threshold stays where every one of those systems puts it — at runtime, in arithmetic.

pub tor quorum.check {}
| reached i64
| short
quorum.check = if(raft.counted > raft.half)
| then => reached raft.best
| else => short

And here is the test that passes while printing the wrong answer.

  counted ack from peer 1 at index 7
  counted ack from peer 2 at index 7
  counted ack from peer 2 at index 7
commit -> 7 on 3 acks of 5

Peer 2 agreed twice. Two acks minted for one peer are two genuinely distinct resources, each consumed exactly once, entirely legally — and a majority is declared on the word of two voters out of five.

The peer id is passed straight into tally.count. The compiler is holding the identity at the call site and can do nothing with it, because an obligation is a statement about a value’s lifetime and never about its equality to another value. Linearity counts tokens; a quorum counts identities. Every real implementation defends that with a set, and a set is not a thing a linear type stands in for.

The ancestor, and the port I did not write

Orleans is where virtual actors come from — Durable Objects are its idea, reimplemented. So the obvious move is to port its single-activation guarantee, and that port would be a lie.

Orleans’ exclusivity is best-effort, and its own source says so plainly. The directory handoff path records “the applications which lost the registration race (duplicate activations)” and then goes and destroys them. Another comment reads “Grain is supposed to be in single activation mode, but we have two activations!!”. A silo wrongly marked dead lets a second activation replace one that is still serving. celld makes duplicate ownership logically impossible with a compare-and-swap and an epoch in the object prefix; Orleans carries an advisory view stamp and a lease heuristic.

A compile-time guarantee on top of a best-effort runtime property is a lie with a checkmark on it. So the lease does not transfer.

What does transfer is the thing Orleans leaves entirely to you. Its turn model is single-threaded per activation, and whether another turn may run while yours is suspended is decided by MayInvokeRequest — the one genuinely pure predicate in that runtime, no I/O and no timers, driven by the [Reentrant] and [AlwaysInterleave] markers. That is within-silo and within-activation: a scope a type system actually reaches.

Borrow versus consume turns out to be the spelling of does this suspension keep the turn?

pub tor call.blocking { turn: string<exclusive>, target: string }
call.blocking = std/io:print.ln("  await {{ target:s }} — non-reentrant, turn held")

pub tor call.interleaving { turn: string<!exclusive>, target: string } -> string<exclusive!>
call.interleaving = std/store:stored { grain.count: grain.count + 1 }
    |> std/io:print.ln("  await {{ target:s }} — REENTRANT; another turn bumped to {{ grain.count:d }}")
    |> turn.begin(id: "resumed")

A non-reentrant call borrows <exclusive> and the turn survives it. A reentrant one consumes it and hands back a fresh turn. Nothing in the names carries that difference; in Orleans it is a class attribute whose consequences live in your memory.

The safe shape follows from the types rather than from a style rule — read, modify and write atomically inside the turn, so no value ever escapes to go stale:

pub tor state.bump { turn: string<exclusive> }
state.bump = std/store:stored { grain.count: grain.count + 1 }
    |> std/io:print.ln("  bump -> {{ grain.count:d }}")

  bump -> 1
  await other-grain — non-reentrant, turn held
  bump -> 2
  turn t1 ends
  bump -> 3
  await other-grain — REENTRANT; another turn bumped to 4
  bump -> 5
  turn resumed ends

Where it stops again

Hand a value out of the turn and the famous reentrancy bug is back:

pub tor state.read { turn: string<exclusive> } -> i64<fresh!>
state.read -> grain.count

pub tor state.write { turn: string<exclusive>, v: i64<!fresh> }
state.write = std/store:stored { grain.count: v }
    |> std/io:print.ln("  count := {{ v:d }}")

  await other-grain — REENTRANT; another turn bumped to 1
  count := 0
  turn resumed ends
the other turn's bump is gone; count is 0

Another turn bumped the count to 1; the write stored a value read before the suspension; the increment is gone. <fresh> is a claim about the binding x and <exclusive> is a claim about the binding t1, and Koru cannot say the first dies when the second is discharged.

One honest note about how that test got written, because the first version of it was wrong in an instructive way. The natural spelling is state.write(turn: t2, v: x + 1) — and that is refused. It would have made a lovely screenshot. It has nothing to do with staleness: arithmetic strips the obligation, so x + 1 carries no <fresh!> at all, and the identical refusal fires in a flow with no interleave in it. The control that caught it was the same write with the interleave removed, and it took one run. When a wrong program is refused, check that it is refused for the reason you are about to claim.

Three walls, one wall

Three ports, two unrelated families of system, and each one stopped. Stated separately they read like three different shortfalls in the type system:

They are one wall. An obligation is a claim about one binding: this value came from that minting path, and it has been consumed this many times. Every wall hit was a claim about two things — this proof ≥ that position, this token’s peer ≠ that token’s peer, this value’s validity depends on that binding’s liveness. Ordering, magnitude, equality and liveness-dependence are all relations, and a per-binding phantom state cannot express any of them.

That reframing is worth more than the three findings it replaces. As three shortfalls it invites the wrong work — bolt a comparison on here, a dedup there. As one property it is a test you can apply before writing anything: is this invariant about one value’s lifetime, or about a relationship between two values? Only the first is reachable, and knowing that in advance tells you where the next port will stop without running it.

It also says what to do instead, and all three ports agree on the answer: change the shape until the relation is gone. Orleans’ safe pattern is read-modify-write atomic inside the turn — no value escapes, so no value can go stale, so the relation never arises. That is the same advice the Orleans documentation gives about reentrant grains. Arriving at it from the type side, as the only shape that compiles cleanly, is a different kind of knowing than reading it in a best-practices list.

What is actually true

The claim this started with was that a distributed protocol is a pure decision core. Four systems say no: only celld is built that way, and celld is the one that advertised it. ZooKeeper is mature, correct, in production everywhere, and never needed one.

The claim that survives is narrower and holds four for four — the correctness-bearing computation is pure in every one of them, whatever the codebase does with it. That is why a language with no sockets, no threads and no clock can carry the interesting half of this work today.

And the type system reaches the lifetime of a value, not its arithmetic and not its relationships. Everything above that line is free and permanent: provenance cannot be forged, a consumed resource cannot be reused, an unanswered request cannot be dropped. Everything below it — is this the same peer, is this position greater, has this value gone stale — is still yours to get right.

Knowing exactly where the line falls is the result. Not the ports.