Channel Declarations

ChannelDecl       ::= SyncChannelDecl | AsyncChannelDecl

SyncChannelDecl   ::= 'Sync' 'Chan' ident '=' ident '-->' ident ';'?

AsyncChannelDecl  ::= 'Async'? 'Chan' ident '=' ident ('<->' | '-->') ident ViaClause? ';'?

ViaClause         ::= 'via' ident ('<' Type '>')?

A channel declaration introduces one named communication endpoint between two protection domains. Channels carry the events that show up inside a process expression — c?x (receive) and c!e (send). They live in .fis system files; the .fi files reference channels by name only.

Channel kinds

Kind	Direction	Notation	Notes
`SyncUni`	Unidirectional	`pd_a --> pd_b`	Synchronous call/reply; only the unidirectional shape is allowed.
`AsyncUni`	Unidirectional	`pd_a --> pd_b`	Notification-only; no payload acknowledgement.
`AsyncBi`	Bidirectional	`pd_a <-> pd_b`	Each side can send and receive on the same channel.

The Async keyword may be omitted — a Chan without a leading Sync is asynchronous by default. The default arrow is <->. Only Sync channels require the unidirectional --> form.

Fields

Name — snake_case identifier. The same name appears in process expressions on the LHS of ? / !.
Endpoints — two protection-domain names. Both must be declared in the same .fis file.
Buffer (optional, after via) — the MemoryRegion that backs the channel’s payload buffer, optionally annotated with a typed slot: via packet_buffer_outer<int>. Without via, the channel is treated as a pure synchronisation point with no shared payload buffer.

The optional trailing semicolon is accepted but not required.

Examples

// Synchronous unidirectional — outer PD calls into the diode.
Sync Chan o2d = eth_outer --> dd;

// Asynchronous bidirectional — `Async` is the default, can be omitted.
Chan d2i = dd <-> eth_inner;
Async Chan s2o = simulate <-> eth_outer;

// Buffer-backed channel, typed slot.
Chan packet = eth_outer <-> eth_inner via packet_buffer_outer<int>;

// Buffer-backed, untyped (slot type defaults later).
Chan ring = eth_outer --> eth_inner via ring_buffer_outer;

Channel events in process bodies

Inside a process, channel events are written chan_name '?' ident (receive) and chan_name '!' ident (send). The names must match exactly; the validator resolves each event back to the declared ChannelDecl to check direction and payload type.

See Event Blocks → Channel events for the inline event grammar and Process Blocks for how channel events sit in a process expression.

Limitations

Slot types in the via clause currently accept only primitive types; struct slot types parse but are gated by the type-system work tracked separately. The corresponding test is marked #[ignore].
The Sync modifier rejects bidirectional <-> syntactically; sync bidirectional channels would require a richer call/reply protocol than the current implementation supports.