Protocols and Streams

The Protocol judgment: how components may interact over time, and how stream combinators transform both payloads and protocols. Principles in force: P-2 (arbitration/buffering never silent), P-4 (unified surface).

Committed design

1. Protocols are trace languages, delivered as a catalog (D-015)

A protocol is a language of legal interaction traces, not a metadata enum (ReadyValid, InOrder). But full user-defined refinement session types have undecidable equality/subtyping even over decidable arithmetic (Das & Pfenning, CONCUR 2020), and no inference story. So committed scope is a catalog of built-in protocol schemas with checkable parameters:

• ready_valid { payload_stable_while_blocked }
• credit<N> — credits as linear tokens returned through the protocol (03 §6)
• burst<N> — header then exactly N beats then completion
• request_response { matched_by: Id, faults: allowed }
• Process<During, Success, Failure> — the async-transition protocol used by typestate

Each schema ships with: its dual, its parametric compatibility rules (decidable), its generated verification artifacts (08), and its combinator transformation laws (§5).

Probe-driven catalog additions (2026-07-17, probes/protocol-catalog/ — the OP-3 coverage probe, SUPPORTS-SETTLED). Expressing AXI4-Lite, a credit NoC, WRAP bursts, and out-of-order same-ID matching produced a precise requirements list, all catalog-level, none requiring phase-3 user protocols:

• bundle operator — product of schema instances with shared conservation counters: AXI4-Lite is five ready_valid instances whose write-response ordering is plain linear inequalities over acceptance counters — but the counters span instances, which single schemas can't state. (Implemented executably in the probe.)
• layer operator — one physical stream governed by two schemas at different granularities (credit at flit level under packets at burst level).
• burst_dyn { max_len } schema — variable-length bursts via a benign existential over length, still decidable; static burst<N> stays for fixed-length uses.
• Monomorphization rule — schema parameters that multiply (WRAP's container = len · 2^size) are Presburger per instance but not parametrically; such schemas monomorphize at comptime over their finite legality sets, keeping compatibility decidable. This is now a stated D-015 rule.

Two confirmations worth recording: per-key FIFO ordering is inexpressible as a refinement predicate — validating §4's choice to keep ordering relations a separate judgment rather than schema sugar; and keyed counters sit exactly where refinement-session undecidability lives, validating the fence around trace-level refinement between keyed schemas.

The CHI-lite re-probe (2026-07-17, probes/protocol-catalog-chi/, SUPPORTS-SETTLED) fixed phase 3's scope with teeth on both sides. CHI's entire link layer — four channel classes with per-channel credits — fits bundle + layer(credit<K>) with zero new machinery, and the wave-1 refinement language needed zero additions (snoop fan-out counting, #resp = #snoop, is plain Presburger over one keyed counter family). What the catalog provably cannot do (shown executably: the best bundle-level aggregate invariants accept a per-ID-confused trace that sessions reject) is the four-channel per-transaction lifecycle. Phase 3 must deliver exactly:

1. a session<key> operator over bundles — spawn-per-key, cross-channel projection, retirement-as-acceptance; small and decidable per instance (~60 lines in the probe);
2. session bodies as D-027 user protocols, unchanged — the body is irreducibly user-defined content, D-027's first real customer;
3. roles and projection replacing duality for multiparty flows: binary dual() computes but is no participant's view of a three-role body (shown by test) — with the wave-1 monomorphization rule generalizing to role cardinality (comptime-concrete N keeps per-role projection finite-state and decidable);
4. the existing fences kept: parametric-N multiparty session types and refinement between keyed bodies stay out.

G12 closed (2026-07-17, probes/protocol-hazards/, SUPPORTS-SETTLED): same-address hazard ordering fits the committed machinery. Two generalizations, neither enlarging phase-3 scope: (a) session<key>'s key is a computed unary projection — any restricted-Presburger expression over one message's payload (line address = addr div LINE_BYTES; the field case is key = v(f)) — plus per-message key bindings, where a retiring message inherits its key from the binding latched at open (txn → line); (b) one catalog-schema candidate, hazard_lock — a generic two-state per-key mutex (acquire at open, owner latched, release at retirement). session<addr div 64> hazard_lock is CHI's HN same-line serialization (WAW/RAW) verbatim, and is exactly PDL's per-address lock (Zagieboylo et al., PLDI 2022). Genuinely binary address-overlap ordering is §4's, not this section's — see the §4 related_by generalization. One composition note held from the probe: the lock and the per-transaction session are conjoined monitors — the lock serializes lifecycles; message-alphabet duties stay with the session. With G12 closed, the phase-3 protocol requirements list is confirmed complete and the scope freeze is unblocked. (Residual flag: snoop/request races under DMT/DCT direct paths — re-probe only if phase 3 adopts them.)

2. User-defined protocols: Rast-lineage, check-only (D-027)

Beyond the catalog (phase 3), user protocol declarations follow the proven-practical slice of refinement session types — Rast's recipe: binary session types + Presburger-only refinements, assert/assume on messages, ∃/∀ over naturals. Three imported engineering rules:

1. Check, don't infer: invariants are user-written; the checker verifies.
2. Sound, incomplete, terminate-with-hints: type-equality uses Rast's bisimulation semi-algorithm; when it fails needing a stronger coinductive invariant, the error asks the user for an explicit type declaration — a stable, actionable outcome, not a flaky one.
3. Refinement discharge goes through the shared Tier-1/Tier-2 machinery with its stable proved/refuted/obligation outcomes.

Example (a committed-catalog schema, shown with its refinement content):

A consumer of Burst<N, T> provably handles exactly N beats.

3. Duality, compatibility, refinement

Connections require Producer<P> / Consumer<Dual<P>> with compatibility checked per-schema (catalog: decidable; user-defined: semi-algorithm + hints). Substitution is protocol refinement, not equality — a producer with stronger ordering or lower latency bound may satisfy a weaker consumer contract — with variance handled per parameter, never nominal inheritance. Liveness caution from 06 §4 applies.

4. Ordering as named relations

InOrder is replaced by relations over events: PreservesOrder<Input.Accept, Output.Transfer, key = TxnId>, CommitsIn<ProgramOrder>. A reorder buffer accepts out of order, completes out of order, commits in program order — three relations, directly stated, each generating its own relational check.

related_by generalization (2026-07-17, probes/protocol-hazards/). PreservesOrder<A.Accept, B.Transfer, key = f> orders events agreeing on a unary projection; some memory-protocol ordering (AXI: same-ID transactions to overlapping bytes complete in issue order) is keyed on a binary Presburger relation between two payloads: PreservesOrder<AW.Accept, B.Transfer, group = Id, related_by = overlaps(a, b)> with overlaps(a,b) := a.addr ≤ b.addr + W·b.len − 1 ∧ b.addr ≤ a.addr + W·a.len − 1 (beat width W = 2^size monomorphized per the D-015 rule). Key-equality is the special case related_by := (f(a) = f(b)). The relation stays in this judgment: it is checked by the same relational monitor, and is inexpressible as a session key (a key is a function of one message) or as a refinement predicate (per-pair obligations exceed even per-key queues). Conservative coarsening to line granularity is sound only as a key set (every line the burst touches — one event may join several keyed orders); keying by the start line alone is unsound for line-crossing bursts (executable counterexample in the probe). The judgment requires related_by symmetry (or checks both orientations) — an asymmetric relation silently halves the property.

5. Combinators transform protocols, by law

Every stream combinator has a declared effect on payload and on protocol/temporal guarantees, derived from a small stream calculus, not library docs:

fork is refused as a bare operation (P-2): the caller picks broadcast(completion = AllSinksAccept), tap(loss = Allowed), or partition(route) — semantically distinct operations with distinct protocol effects.

6. Arbitration is first-class

The Bluespec lesson (03 §4): compiler-chosen urgency plus stringly pragmas, module-local and blind to other contenders' readiness, is the documented failure mode. Strata's arbitrate is an architectural node (P-5) with real identifiers, cross-module scope, and a full contract:

Safety checks are static/Tier-2; liveness is a Tier-3 obligation with its assumptions explicit; the policy generates fairness assertions, starvation coverpoints, adversarial tests, and counters (08). The optimizer may change comparator topology or pipeline the selection under the latency contract, but may not change policy without a refinement proof (07 §4).

7. Clock crossing is a protocol transformation with a contract

cross_clock::<B>(bridge) changes the domain and the temporal contract. The bridge (e.g. AsyncFifo) is an unsafe clock_crossing component carrying a CDC contract — ordering preserved, capacity D, asynchronous latency, progress assuming both clocks fair, reset-release protocol required — with evidence attached (06 §3): vendor-assumed, formally verified once, or imported as a reviewed artifact. Composition then uses the contract without reopening the gray-pointer logic. In committed scope this is also the only way feedback or data crosses domains (03 §5).

The bridge is additionally a squash-contract carrier (probe-resolved, wave 3, probes/squash-cdc/) — carrier, not owner: the bridge stays epoch-oblivious (the 05 §4 CDC-below-epochs containment holds), and its ordinary contract clauses are exactly the premises of the cross-domain squash story. Epoch control (Open/Resolve/Kill) crosses in-band, ordered with data; the consumer side maintains a mirrored epoch chain and runs the ordinary 05 §3 squash contract against it (bind epoch is the enforcement point). Ordering gives two properties for free: recovery epochs cannot be confused with victims (the Open follows the Kill), and per-epoch Resolve/Kill exclusivity delivers no-stale-commit across domains — a value whose epoch died at the source can cross, be speculatively consumed, but never retire. The drain bound for crossing capacity is keyed on the death event and denominated in far-side response events plus a fixed synchronizer tail (not source cycles). Two sharpened clauses: (1) "progress assuming both clocks fair" is strengthened to the consumer's acceptance must not be conditioned on subsequent channel content — a Tier-3 liveness obligation on the consuming component, without which no drain bound of any denomination exists (deadlock witness in the probe); (2) a bridge MAY declare exit-side early annulment as a performance refinement only with the death-event fence (kill boundary + push-sequence watermark) — the unfenced kill_from comparator is machine-refuted (297/300 traces drop live recovery-epoch entries).

8. The surface declaration

One declaration, elaborated into orthogonal judgments (P-4):

flow.outstanding is where dynamic latency lives in committed scope (D-034): an occupancy refinement plus conservation tokens, not a symbolic interval.

North star

• Full user-defined refinement session types with arithmetic-refined subtyping, if/when inference research matures.
• Multiparty/coherence protocols (cache-coherence message families as one typed protocol object with per-role projections).
• HazardFlow-style hazard interfaces as composed protocol transformers (stall/bypass/restart as protocol structure rather than ad-hoc wiring).
• Protocol-level cancellation as a first-class dual channel tied to speculation epochs.
• Fault/recovery schemas separating occurrence, detection, correction, containment, escalation, and optional health invalidation; corrected transients need not kill a health generation (D-081, probes/fault-health/).
• Finite progress summaries over held resources, release events, protocol phase, VCs, fairness class, and assumption ownership; rank/escape certificates prove a restricted cyclic fragment while unresolved cases become Tier-3 obligations (D-083, probes/progress-waitfor/).
• Mapping lease/borrow lifecycles for DMA/IOMMU/interrupt boundaries, with owner-validated opaque generations and drain-aware invalidation (D-082, probes/dma-iommu/).
• Memory consistency as a separate composition check over partial event relations with explicit completeness, never inferred from message-trace legality (D-084, probes/memory-consistency/).

Open problems touching this doc

OP-3 — the catalog-coverage probe (express AXI4, a CHI-lite subset, and a credit NoC in the catalog + refinements; wherever it fails, that's the phase-3 requirements list).