# proposal/04-protocols-and-streams.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/a0828f65437c5a864898323290e15e77383c4a52/proposal/04-protocols-and-streams.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: a0828f65437c5a864898323290e15e77383c4a52 Requested commit: a0828f65437c5a864898323290e15e77383c4a52 Commit: a0828f65437c5a864898323290e15e77383c4a52 Blob: dd27ec3709986058b48687196e0ae6243f75f559 Size: 16035 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/a0828f65437c5a864898323290e15e77383c4a52/proposal/04-protocols-and-streams.md?format=markdown) ```` # 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` — credits as linear tokens returned through the protocol ([03 §6](03-time-and-resources.md)) - `burst` — header then exactly N beats then completion - `request_response { matched_by: Id, faults: allowed }` - `Process` — the async-transition protocol used by [typestate](02-type-system-core.md) Each schema ships with: its dual, its parametric compatibility rules (decidable), its generated verification artifacts ([08](08-verification-platform.md)), 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` 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)` 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` 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`'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 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](06-refinements-and-evidence.md) with its stable `proved/refuted/obligation` outcomes. Example (a committed-catalog schema, shown with its refinement content): ``` protocol Burst { send Header { length: N }; repeat N { send Beat; } recv Completion; } ``` A consumer of `Burst` provably handles exactly `N` beats. ### 3. Duality, compatibility, refinement Connections require `Producer

` / `Consumer>` 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](06-refinements-and-evidence.md) applies. ### 4. Ordering as named relations `InOrder` is replaced by relations over [events](03-time-and-resources.md): `PreservesOrder`, `CommitsIn`. 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` 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` 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: | Combinator | Preserves | Changes / introduces | | ------------------ | ---------------------------------------------------------- | -------------------------------------------------------- | | `map(f)` | cardinality, ordering, backpressure, cancellation identity | payload, latency, combinational depth | | `filter(p)` | ordering among survivors | cardinality, rate (no fixed output rate) | | `zip(a,b)` | — | synchronization dependency, deadlock potential (flagged) | | `buffer(d)` | payload trace, ordering | capacity +d, latency window, backpressure timing | | `batch(n)/unbatch` | order | rate, payload shape | `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](03-time-and-resources.md)): 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](01-design-principles.md)) with real identifiers, cross-module scope, and a full contract: ``` arbitrate { inputs: [loads, stores, atomics], eligibility: |r| r.ready, policy: oldest_first(key = r.age), resource: memory_port, guarantee { exclusive_grant; no_grant_to_ineligible; } liveness { weak_fairness under continuously_ready(memory_port); } } ``` 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](08-verification-platform.md)). 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](07-compiler-architecture.md)). ### 7. Clock crossing is a protocol transformation with a contract `cross_clock::(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](06-refinements-and-evidence.md)): 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](03-time-and-resources.md)). **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](05-speculation-authority-effects.md) 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): ``` stream LoadRequests { payload: LoadRequest, domain { clock: CoreClock, reset: CoreReset }, protocol ready_valid { payload_stable_while_blocked }, flow { acceptance: at_most 1/cycle, outstanding: 0..=8, latency: dynamic }, identity { transaction: LoadTxnId }, ordering { preserve request_acceptance_order }, authority { speculative: BranchEpoch, cancellation: by BranchRecovery }, } ``` `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](05-speculation-authority-effects.md). - 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](open-problems.md) — 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). ````