Module link 

The link port: what a layer above the link may depend on, and the whole of what it may.

docs/conditional-guarantees.md states the seam this project is built around: layers above the link may depend on its Cmd and Ind types and nothing else, so a session-aware or logged implementation can be swapped through. This module is that sentence made checkable. A layer above bounds on Link; an implementation below satisfies it; neither names the other.

Why the vocabulary is not pinned to one pair of types

The obvious port is a bound pinning the types exactly — Protocol<Cmd = pl::Cmd<P>, Ind = pl::Ind<P>>. It works for the perfect link and fails for the session link, whose Ind has three variants rather than one, and admitting both is the entire point: the four session_* broadcast modules exist because a layer written against one pair of types cannot compose over the other.

So a link keeps its own Cmd and Ind — they are its vocabulary, not the port’s — and the port supplies the two translations a layer above actually needs: build a send, and recognise a delivery. Nothing else about the link is visible.

Scope boundaries, and why there is no second trait for them

A session link reports that a session ended or was established. A perfect link cannot: it has no means of observing either, and docs/scope-annotated-modules.md forbids a module declaring a scope it cannot observe (Definition 2a, Corollary 8.1). So Link::classify returns LinkInd::Boundary only for a link that can actually see one, and that is the whole of the mechanism.

There was a ScopedLink marker trait here, so that a layer whose liveness depends on being told about a re-establishment could bound on it, making it a compile error to compose that layer over a perfect link. It was deleted, because once the four session_* broadcast modules had collapsed into their base modules — the job it was introduced to do — nothing bounded on it. Uniform reliable broadcast, the one layer that should have, could not: its resend is reached from the arm handling the child’s indications, which lives in the Link impl, so the tighter bound would have fallen on every link including the perfect one.

What keeps that resend honest is this module’s own guarantee rather than a bound: a boundary is never classified for a link that cannot observe one, so over a perfect link the path is unreachable rather than merely unused. tests/link_port.rs pins both halves — that the perfect link’s classification never yields a boundary, and that the session link’s yields one for each variant that reports it.

Reintroduce it when a layer genuinely cannot be written without the bound. Until then it is an abstraction ahead of its consumer, which is what CLAUDE.md constraint 4 warns against and what this change’s own design.md recorded as a risk against this very trait.

Enums

Boundary

A boundary of the scope within which a link’s guarantees hold.

LinkInd

What an indication from any link amounts to, in the port’s own vocabulary.

Traits

Link

What a layer above the link may depend on, and the whole of what it may.

VolatileLink

A link that keeps nothing durable the layer above has to know about.