Event Declarations

EventDecl   ::= 'evt' ident Carriers? ':' Statement*
Carriers    ::= ('.' '|' Param (',' Param)* '|')+
Param       ::= ident ':' Type

An event declaration introduces one named atom of computation at the top level of a .fi file using the evt keyword. Processes reference it by name on the left of a prefix (my_event -> ...).

evt declarations must appear before any proc definition in the same file; the compiler rejects an evt that follows a proc with a diagnostic. (Single-pass files are scannable top-to-bottom: all events visible before the processes that use them.)

Computation events are one of three event kinds in CoreFi (paper §4.2); the other two — channel events (c?x / c!e) and hardware-interrupt events (irq?N / irq!N) — are inline atoms that appear in process bodies and have no top-level declaration.

Computation events

A computation event is a named, atomic block of statements: assignments and external calls, plus optional carrier parameters. The block executes as a single transition in the labelled-transition system — processes can prefix on it (my_event -> ...) but cannot observe it mid-flight.

Names follow snake_case and start with a lowercase letter. This both signals intent and lets the parser disambiguate between a computation event reference and a sub-process reference (which uses UpperCamelCase).

Body and termination

After the :, the body is a sequence of statements: local variable declarations, assignments, and external function calls. There is no explicit terminator — the body ends implicitly when the next top-level keyword (evt, proc, import, Mapping, etc.) is reached or when the file ends. Single-statement bodies terminate at ;.

// Single-statement body — ends at ;
evt setup_eth: eth.eth_setup();

// Multi-statement body — ends at the next top-level item; size carrier used in alloc.
evt handle_packet.|size: int|:
    local_buf: int;
    local_buf = eth.alloc(size);
    counter = counter + 1;

evt next_event: ...   // body above ends here

Carriers

evt handle_packet.|size: int|:                  // single carrier
evt ack.|chan: int, slot: int|:                 // grouped carriers
evt ack.|chan: int|.|slot: int|:                // chained carriers (equivalent)

Carriers are parameters supplied by the invoking process. The syntax uses pipes (.|...|) — chosen over parentheses so the visual boundary is distinct from sub-process parameter lists. Multiple carriers may be grouped in a single .|x: int, y: int| clause or chained across multiple .|x: int|.|y: int| clauses; both forms parse to the same Vec<(Type, String)> and behave identically.

Inside the body, carriers are used like any other variable — passed to external calls (eth.handle_rx(idx)), read in expressions (local_buf = eth.alloc(size)), or updated by assignment. Three kinds of variable names can appear in an event body:

Name resolution searches in order: local → carrier → global. To carry mutable state across event invocations, use a global; to carry mutable scratch within one invocation, declare a local variable.

Examples

// No carriers — the event is a fixed call.
evt setup_eth: eth.eth_setup();

// Single carrier, single-statement body — idx is the carrier.
evt read_frame.|idx: int|: eth.handle_rx(idx);

// Multi-statement body — size carrier passed to alloc.
evt handle_packet.|size: int|:
    local_buf: int;
    local_buf = eth.alloc(size);
    counter = counter + 1;

// Multiple carriers, grouped form.
evt ack.|chan: int, slot: int|: eth.ack_slot(chan, slot);

// Same event, chained carrier form (equivalent).
evt ack.|chan: int|.|slot: int|: eth.ack_slot(chan, slot);

Empty-body events

evt noop: (no statements before the next item) is accepted; the body is zero statements. Useful as a placeholder while a process expression is being prototyped.

Channel events

ChannelEvent ::= ident '?' ident             // c?x — receive
              |  ident '!' ident             // c!e — send

A channel event is an atomic communication action between two protection domains. The channel name on the LHS is resolved against the Chan declarations in the surrounding .fis.

Channel events appear inline inside process expressions — they have no top-level declaration. The receive form c?x binds the incoming value to a local x; the send form c!e transmits the expression e.

No selective receive

The RHS of ? is always a single identifier (a binder), never a value pattern. Traditional CSP / CSP# accepts c?ACK as “wait only for the message ACK”, but Fiducia rejects this: it can deadlock when no sender ever produces the matching value, conflicting with CoreFi’s deadlock- freedom story (paper §4.1 Wf1). The same expressiveness is recovered by binding then guarding:

// Recommended.
c?msg -> [msg == ACK] handle_ack -> Skip [] [msg == NACK] handle_nack -> Skip

Send-payload style

The RHS of ! accepts any Expr — the parser does not reject a call expression there today. The recommended style is still to keep channel events as pure-communication atoms: bind a call’s result in a computation event first, then send the bound variable, rather than calling directly in send position. This keeps side-effecting work legible as its own step in the process algebra, even though the grammar itself doesn’t enforce it:

// Discouraged (parses, but buries a side-effecting call in a
// communication event):
// c!eth.get_packet()

// Recommended: bind, then send (pkt is a global variable).
evt get_pkt: pkt = eth.get_packet();
proc P() { get_pkt -> c!pkt -> ... }

Hardware-interrupt events

IRQEvent ::= 'irq' '?' integer_literal       // irq?N — await
          |  'irq' '!' integer_literal       // irq!N — acknowledge

A hardware-interrupt event is a special-cased channel event on the reserved channel name irq. The integer is the IRQ number declared on the protection domain. irq?N blocks until the IRQ fires; irq!N acknowledges the IRQ back to the kernel.

Like channel events, IRQ events appear only inside process expressions and have no top-level declaration:

proc Notified() { irq?159 -> Handle_eth(); irq!159 -> Notified(); }

🚧 self.IRQ syntax is planned (#164) — irq?self.IRQ / irq!self.IRQ will resolve the protection domain’s IRQ number without a magic literal.