Regime-Based Capability Semantics (RCS)

This post is part of The Eter programming Language series.

This is the fourth post in the series dedicated to the Eter programming language, a side project that allows me to take my mind off the research I have to conduct. The previous posts are (from the most recent to the oldest):

If you are interested in the project, you can find more information in the Eter compiler monorepo. The Eter language reference and the Eter Doxygen documentation, although not yet complete, are also good starting points.

The first post, in its prelude, introduces what we are currently researching for the Eter language. Then, it discusses the mutable value semantics (MVS) and how the popular programming languages (e.g., Swift, Hylo) implement it. The second post covers the trade-offs between MVS and ownership & borrowing, examining friction points in Rust, Hylo, and Swift while searching for common ground between the two memory models. The third post proposes a friendly tour of the type-theoretic landscape behind memory safety. Starting from the logical roots of substructural logic, it walks through linear, affine, and uniqueness types, then visits regions, effects, capabilities, typestate, and the latest work on reachability and separation types.

Premises

I'm really excited to share this post with all of you. When this path started (2 month ago), I had no idea that I would end up here. However, fundamental properties such as type soundness (or safety), via progress and preservation, require formalization of both typing rules, to define what is considered valid, and operational semantics, to describe how programs evolve. However, I will not delve into this level of formalization here. While we are currently starting the implementation of the Eter compiler, I'm interested formalizing the ideas as well—if someone wants to collaborate in this direction, please get in touch. I'm familiar with Rocq theorem prover, but I'm open to using other tools or paper-and-pencil proofs as well. Additionally, while writing this post, I came across a very interesting discussion on a programming languages subreddit, pointed out by knue82 in the comments of the previous post. Even if you're not already familiar with the regimes, they share similarities with the "universes" model that WittyStick proposed three years ago in that discussion.

Regime-Based Capability Semantics

The Regime-Based Capability Semantics (RCS) is a substructural graph-based capability semantics framework, where the right to read, mutate, or alias a value is not a property of the value itself but a label (the regime) carried by the edges through which the value is reached. Conceptually, a program state is a directed graph whose nodes are storage locations and whose edges are access paths; each edge is annotated with a regime—one of imm, mut, or proj—that fixes what may legitimately happen along that path. Safety is then a statically-enforced invariant on how these regime-labelled edges may be created, relabelled, forwarded, and discarded.

Wait, what the hell is this? It's actually quite simple, and the name is just a technical description of the system. I'll break it down, but I'd rather start by explaining what RCS is not, to give you a clearer idea of what it is. It is tempting to file RCS under one of the familiar headings, but it brushes against many at once—broad categories of formal artifact and the specific disciplines from the previous post alike—and the cleanest way to characterize it is to say, why it is precisely none of them.

RCS is not merely...

...a type system. A type system classifies expressions; here the primary object is the access graph, and the typing judgment is a projection of it. The kind presented by a binding derives from the regime of the edge that reaches its value, not vice versa.
...an operational semantics. Reduction explains how a program runs; RCS additionally imposes static invariants—on aliasing, mutation, and forwarding—that constrain which graph transformations are admissible in the first place.
...an effect system. Effects record what a computation does (the actions it performs), bottom-up. Regimes record what a path is permitted to do, structurally—authority over the heap, not a log of events.
...a capability system. Classical capabilities are primitive, token- or reference-shaped values. Here a capability is not a primitive: it is the pair of an edge and its regime, and authority is read off the topology of the graph rather than carried as a separate token.
...a substructural type system. Substructural disciplines restrict the structural rules on variables in a context. RCS lifts that restriction to the edges of the graph: it is the connectivity, not the binding, that becomes, e.g., affine, unique, or unrestricted.
...a reference capabilities system. The nearest relative—they, too, qualify access rather than the object. But the qualifier rides on a reference, a value held by a node, and is read off in isolation; an RCS regime rides on the edge and answers to graph-level invariants (at most one mut in-edge per location), not to the type of a reference taken alone.
...a reachability type system. They share the graph and the concern with separation, but hang a set of reachable variables on the type of a value and let separation fall out of qualifier disjointness. RCS hangs a regime on the edge; separation and exclusivity are constraints on edges, not a derived property of node-indexed sets.
...an object capabilities system. They equate authority with reachability: holding the reference is the permission. RCS refines exactly that equation—an edge is necessary but not sufficient, and its regime says what the edge authorizes, so two references to one object may carry different authority.
...a region and ownership type system. They partition the heap by where a value lives or which object owns it—a discipline on the nodes and their grouping. RCS imposes no such partition: authority is local to each edge, and a single location may sit at the end of edges of every regime simultaneously.
...a fractional-permission or degree-of-separation system. Here the kinship runs deepest, and it is genuine: imm's coexisting read-only aliases are a value's uniqueness split into shares, and mut is the full share \(p = 1\)—exactly the condition under which a write is sound (Granule's writeArray demands \(p = 1\)). RCS does not reject fractional uniqueness; at its core it is a fractional-uniqueness discipline. What makes it more than the usual presentation is threefold. First, the shares ride on edges, and the only question that ever matters—"am I the sole owner?"—collapses to a graph fact, the node's live in-degree. Second, there is no explicit split/join arithmetic: recombination to \(p = 1\) is implicit, discovered by liveness, so a shared value silently regains write-authority the moment its other owners die (we work this out below). Third, it is folded into a three-regime system, with proj supplying the scoped borrow that fractional permissions can only model as a temporary fraction. And where the Capture Separation Calculus enforces separation only where parallel use makes a race possible, RCS settles it structurally, by the regime on each edge.

The system therefore stratifies into three layers. A primary ontology—the reference graph with regime-labelled edges; a dynamics—the rewrite rules that move, forward, and reinitialize those edges; and a family of derived views—types, effects, capabilities, and aliasing constraints—each of which is an extrapolation of the same underlying graph discipline. Conceptually, you can think of a type taking shape depending on the regime of the edges it reaches.

Breaking Down RCS

The Reference Graph

We make the structure precise. An RCS state is a directed graph \(G = (V, E, \rho, \tau)\) where

\(V\) is a set of locations,
\(E \subseteq V \times V\) is a set of directed access edges,
\(\rho : E \to \mathcal{R} \ s.t.\ \mathcal{R} = \{\,\mathsf{imm},\ \mathsf{mut},\ \mathsf{proj}\,\}\)
\(\tau : V \to \mathsf{Type}\) assigns a type to each location

\(V\) is a set of storage locations (objects, allocations, bindings); \(E \subseteq V \times V\) is a set of directed access edges; \(\tau : V \to \mathsf{Type}\) assigns a type to each location; and \(\kappa : E \to \mathcal{R}, \qquad \mathcal{R} = \{\,\mathsf{imm},\ \mathsf{mut},\ \mathsf{proj}\,\}\) assigns a regime to each edge. The classical reference graph is the special case in which \(\kappa\) is constant—every edge carries the same, uniform "points-to" meaning. RCS makes \(\kappa\) the centre of attention: the regime, not the mere existence of the edge, is what the semantics reasons about.

Reading an edge \(u \xrightarrow{r} v\) as "from \(u\), the value at \(v\) may be accessed under regime \(r\)", the three regimes are:


x --(imm)--> y   // observe y through x
x --(mut)--> y   // mutate y through x
x --(proj)--> y  // borrow y through x

Regimes Live on the Edges

Each regime is a different substructural discipline imposed on the edge that carries it. The table summarizes the three; the rows are not permissions on an object but permissions on a path.

Regime	Read	Write	Aliasing of the edge	Structural status
`imm`	✓	✗	Unrestricted (duplicable)	Unrestricted
`mut`	✓	✓	None (unique active edge)	Affine (move)
`proj`	✓	Conditional (reinit)	Controlled, non-persistent	Linear (forward)

The behaviour of each regime is fixed by a small set of invariants on \(G\). Writing \(\mathrm{in}(v)\) for the edges pointing at a location \(v\):

Immutable sharing. An imm edge may be duplicated without restriction (contraction is permitted), but on its own it never licenses a write. A location reached only by imm edges admits arbitrary aliasing and no mutation—the graph analogue of a freely-shared, read-only value; read quantitatively, it is a uniqueness split into shares, reassembled for mutation only once all but one have been dropped (see below).
Mutable exclusivity. A mut edge is affine and write-capable, and at most one may reach a given location at a time: \[ \bigl|\{\, e \in \mathrm{in}(v) : \kappa(e) = \mathsf{mut} \,\}\bigr| \le 1 \qquad \text{for every } v \in V . \] This is the graph-level restatement of "no two writers"—Rust's shared-XOR-mutable rule, recovered as a counting constraint on incoming edges.
Projection linearity. A proj edge is a linear resource: it cannot be copied, only forwarded—relabelled onto a new source and consumed at the old one—and it may never coexist with a concurrent mut edge to the same location. A projection is access without ownership: it neither owns nor drops its target, yet while it is live the owner must hold still.

Transfer is a Graph Rewrite

Everything dynamic in the system—assigning, passing an argument, returning a result—is a rewrite of regime-labelled edges, and the rewrites are directional. The pattern echoes the asymmetry of uniqueness from the previous post: authority is forgotten freely, and regained only against a proof that the value is back in a single owner's hands.

Concretely, a transfer is a partial map on regimes, \(\mathsf{mut} \rightharpoonup \mathsf{imm}\), \(\mathsf{proj} \rightharpoonup \mathsf{proj}\), and so on, realized as one of five edge operations:

move — the source edge is consumed and re-created at the destination (the discipline of mut);
copy — a new edge is created alongside the old one (admissible only for imm);
forward — a proj edge is relabelled onto a new source and invalidated at the old one, with no aliasing introduced;
reinitialization — an edge is replaced by a fresh capability after the old one is invalidated, which is what a proj must do before it can be observed as imm or mut;
reuse — when a location's live in-edges collapse to a single imm edge, that edge may be upgraded in place to mut and moved on, with no copy and no allocation: uniqueness recovered, the node reused.

The directions that are not free are as telling as the ones that are. Weakening is always available: a mut edge may be forgotten into imm at will. Strengthening—turning an imm edge back into a mut, or lending it out as a proj—is not forbidden, but it is gated: it is sound exactly when the location has returned to a single owner, its live in-degree one, which is the graph reading of the fractional condition \(p = 1\). When the compiler proves this by liveness, the strengthening is a zero-copy reuse; when it cannot, the same syntax falls back to a copy, minting a fresh, unaliased node that is unique by construction. Authority can always be relaxed, then, and it can be regained—but only against a proof that no one else is still watching.

Recovering Uniqueness: `imm` as a Fractional Share

The cleanest way to see the gate at work is to read imm as a share of a value's uniqueness. A freshly allocated value has one owner holding all of it, \(p = 1\); every let imm that aliases it splits the share, and the shares always sum to one. Dropping an owner returns its share to those that remain. Writing demands the whole share back, \(p = 1\)—precisely the soundness condition for in-place mutation, since \(p = 1\) means no one else can observe the change.

Made explicit, a chain of immutable aliases and their drops walks the share from \(1\) down through the co-owners and back up to \(1\) as they die—and the last drop, finding itself alone, is the one that actually frees:

{
  let imm x = [1, 2, 3];   //  x ──imm──▶ ⟦[1,2,3]⟧        p(x) = 1
  let imm y = x;           //  + y                          p = 1/2, 1/2
  let imm z = y;           //  + z                          p = 1/3, 1/3, 1/3

  drop(z);   //  shares ⇒ (x: 1/2, y: 1/2)     share returns to survivors — no free
  drop(y);   //  shares ⇒ (x: 1)               share returns to survivors — no free
  drop(x);   //  x held the whole share (p = 1)  ⇒  DEALLOCATE ⟦[1,2,3]⟧
}

Now the payoff. If, instead of letting the value die, we hand it to a mut binding while its co-owners are already dead, the share has silently returned to \(p = 1\) at x—so the imm → mut upgrade is licensed, and it is a move, not a copy. The would-be drops become placebo (shares handed back, never the final one), and the terminal free is replaced by reuse of the very same node:

{
  let imm x = [1, 2, 3];
  let imm y = x;
  let imm z = y;
  // y and z are dead here  ⇒  their shares collapse onto x  ⇒  p(x) = 1
  let mut m = x;   //  p(x) = 1 licenses imm → mut:  MOVE + upgrade, no copy, no free
}
//  resulting state:   m ──mut──▶ ⟦[1,2,3]⟧

This settles the natural question—does the final drop come before or after the assignment?—with neither: it is fused into it. A real drop(x) before would zero the in-degree and free the buffer, leaving = x dangling; after, there is nothing left to drop, since the move already consumed x. The assignment is the move-and-upgrade, guarded by \(p(x) = 1\); what must happen first is only the collapse of the other shares. The same terminal operation is therefore a free when nothing rescues the node and a reuse when something does—a drop/reuse split the compiler settles statically, ahead of execution.

And because the decision rides on liveness, the very same line is a move or a copy depending on what comes after it:

let imm x = [1, 2, 3];
let imm y = x;
let mut m = x;   //  if y is dead here  ⇒  p(x) = 1    ⇒  move + upgrade (zero-copy)
print(y);        //  if y is live here  ⇒  p(x) = 1/2  ⇒  `let mut m = x` COPIES instead

This is exactly copy-on-write—mutation forces a copy unless the value is uniquely held—but here it is a wholly static discipline: liveness decides, at every use site, whether the upgrade is a zero-copy reuse or a copy, all at compile time. One practical consequence is worth stating plainly: the rational shares are a faithful model, but an implementation never needs the arithmetic. Reads do not care about the magnitude of a share, and the single place magnitude matters—the write—asks one yes/no question, "am I alone?", which the checker answers statically from the node's live in-degree. The fractions are how to think about it; a static uniqueness bit is how to compile it.

Four Projections: Ownership, Mutation, Aliasing, Transfer

Because the regime sits on the edge, the four properties one usually states about a value are not independent axioms but projections of the graph. Each reads off a different aspect of the incoming edges of a location:

Ownership strength — the strongest regime among the edges reaching a location, ordered \(\mathsf{mut} > \mathsf{proj} > \mathsf{imm}\);
Mutation rights — whether any incoming edge is mut, subject to the exclusivity invariant above;
Aliasing capacity — how many edges may simultaneously reach the location, which the regime caps (many for imm, one for mut, one live chain for proj);
Transfer semantics — not a static attribute at all, but the rewrite rule that fires when an edge is moved, copied, forwarded, reinitialized, or reused in place once uniqueness is recovered.

They are coupled through ownership strength: aliasing capacity and mutation rights are constraints derived from it, and transfer semantics is the transition system that carries one configuration of the four to the next. We unpack each of these projections in the sections that follow.

Some Examples to Materialize the Point

Before we dig into the details, let's see some examples of how the regime disciplines manifest.

¹ An unrestricted value is one that satisfies all structural rules of classical logic, allowing contraction, weakening, and exchange without restriction. ↩