Event Blocks

EventsSection   ::= 'Events' ':' EventDecl*

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

An event block is the block of computation events declared at the top level of a .fi file under an Events: section header. Each declaration binds one named atom of computation that processes can reference by name. A .fi file may have zero or more Events: sections; multiple sections merge into a single event list at parse time.

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. They are documented at the end of this chapter.

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).

Carriers

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

Carriers are read-only inputs 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.

Carriers are read-only inside the body. 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 and initialise it from the carrier (int x = carrier; once initialisers land).

Body and termination

Between : and end, the body is a sequence of statements: local variable declarations, assignments, and external function calls. There is no return value — events emit side effects (memory writes, external calls, channel sends are implicit when the event participates in a process’s ->).

The end keyword is the explicit terminator. Implicit termination on the next top-level keyword would give weak error messages on a missing ; inside the body; the explicit end keeps diagnostics local. The same keyword terminates process sub-bodies for symmetry.

Examples

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

    // Single carrier, single-statement body.
    Event read_frame.|idx: int|: eth.handle_rx(); end

    // Multi-statement body with a local.
    Event handle_packet.|size: int|:
        int local_buf;
        local_buf = eth.alloc();
        counter = counter + 1;
    end

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

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

A .fi file may carry multiple Events: sections (for grouping by concern); they merge into a single event list:

Events:
    Event setup_eth: eth.eth_setup(); end

import "more.c" as more;

Events:
    Event handle_irq: more.handle(); end

Both events become part of Program.events.

Empty-body events

Event noop: end is accepted; the body is just zero statements. This is 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 restriction

The RHS of ! is restricted to value-producing, side-effect-free expressions: literals, variable references, arithmetic, and logical expressions. Call expressions (eth.get_pkt()) are deliberately rejected as a send payload — external calls must happen inside a computation event, which preserves the rule that channel events stay pure-communication atoms in the LTS. To send the result of a call, bind it in a computation event first:

// Rejected
// c!eth.get_packet()

// Accepted: bind, then send.
Event get_pkt: pkt = eth.get_packet(); end
Process 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:

Notified() = irq?159 -> Handle_eth() ; irq!159 -> Notified();

The IRQ number here parses as an integer literal — channel events do not yet accept integer payloads on either side. This asymmetry exists because IRQ numbers are constants from the system topology, while general channel payloads will become full expressions once the expression grammar lands.