Introduction

This is the reference for Fiducia, the source language consumed by the fic compiler. A Fiducia source tree describes a seL4 Microkit system: its memory regions, protection domains, channels, the per-PD program logic, and the communication / computation events those programs orchestrate.

The reference is organised after the Rust Reference: each chapter pairs a formal grammar production with the prose semantics that surround it, then expands per syntactic feature with focused subsections and short examples. Where the surface syntax is still in flight, the chapter calls out the incomplete forms with a 🚧 marker so the reference stays honest about what the parser actually accepts today.

Source surfaces

A Fiducia project is two parallel surfaces that the compiler reads together:

• System description (.fis) — the static topology: memory regions, protection domains, channels, the system composition. One per project.
• Program implementations (.fi) — per-PD logic: imports of external C / Rust files, memory mappings, global variable declarations, flat evt declarations, and flat proc definitions covered by this reference. One per protection domain.

The two are linked by name: a Mapping in a .fi file refers to a MemoryRegion declared in the .fis; a channel reference in a process expression resolves against the .fis channel declarations; a computation event referenced by name from a process is declared in the same .fi with evt.

Scope of this revision

This revision covers the three constructs that participate in the Fiducia process algebra:

• Event Declarations — evt declarations for computation events, plus the inline channel and IRQ events used on the left of a process prefix.
• Process Definitions — proc definitions for CSP-style processes composed from events, guards, choices, and sequential composition.
• Expressions — the expression language available to carriers, guards, and send payloads.

Other surfaces (lexical structure, system items, types, validation, the type system) belong in chapters that have not yet been ported into this revision; they remain in the inline /// doc comments in src/parser/ and on their tracking issues until the corresponding chapters land.

Conventions

• Production blocks use the BNF dialect documented in Notation — the same conventions as the Rust Reference.
• Examples render in text blocks; Fiducia is not Rust, and text keeps mdBook’s syntax-highlight neutral.
• Keywords and identifiers are written with backticks in prose (Event, eth.send_frame) and as bare tokens inside grammar productions.
• An em-dash (—) separates parenthetical asides, matching the existing module-doc style.
• Cross-references to the parser source use repository-relative paths (src/parser/event.rs); cross-references to other chapters use plain Markdown links (e.g. Event Declarations).

Notation

This reference uses a BNF dialect for grammar productions. The notation is intentionally close to the Rust Reference so readers familiar with Rust documentation can read it without a separate primer.

Grammar productions

A production has the form LHS ::= RHS, where the right-hand side is a sequence of terminals, non-terminals, and meta-operators. Productions are written in text-tagged code blocks:

EventDecl ::= 'evt' ident carriers? ':' stmt*
carriers  ::= carrier_group+
carrier_group ::= '.' '|' param (',' param)* '|'
param     ::= ident ':' type

Meta-operators

Whitespace between symbols in a production is significant only when called out — most productions allow inter-token whitespace and comments, exactly as the lexer does.

Inline references

• A non-terminal in prose is written in italics (e.g. event, process).
• A literal token in prose is written in backticks (e.g. Event, ->).
• A type-level reference into the AST uses backticks plus the Rust path fragment when it disambiguates (Event::CPEvent, Process::Choice { branches, default }).

Examples

Examples render in text-tagged code blocks, not rust-tagged: the Fiducia source language is not Rust, and text keeps mdBook’s syntax-highlighter neutral. Example:

evt handle_irq:
    eth.handle_irq();

Where an example references symbols declared elsewhere (a channel from the .fis file, a function from an imported .c file, a process declared in the same section), the surrounding prose names the dependency.

Stability markers

A construct flagged with the 🚧 marker is not yet implemented by the parser. The form appears in the reference because it is part of the designed grammar, but the parser will reject it today. The marker links to the tracking issue:

🚧 Not yet implemented — see #105.

Data Layer: Structs and Constants

StructDecl ::= 'struct' UIdent '{' Field* '}'
Field      ::= ident ':' Type ';'
Type       ::= ScalarType | Type '[' ArrayLen ']'
ArrayLen   ::= integer-literal | CONST_NAME
ConstDecl  ::= 'const' UPPER_IDENT ':' Type '=' Expr ';'

The data layer is the system-wide vocabulary of payload struct types and layout constants. It is shared by every protection domain — and, through generated type headers, by the external low-level implementations (C, Rust, Pancake) too, so the model and the code agree on one definition. It lives as flat, top-level items in the .fis file: like the rest of the system description, declarations are visible to every .fi program with no import ceremony.

const PACKET_BUFFER_SIZE: int = 2 * 1024;

struct Packet {
    length:  uint16;                    // valid bytes in payload (≤ capacity)
    payload: byte[PACKET_BUFFER_SIZE];  // fixed-capacity buffer
}

const RING_BYTES: int = 64 * sizeof(Packet);

Structs

• Names use UpperCamelCase by convention.
• Fields are flat — primitives, other declared structs, or fixed-size arrays of those; no pointers.
• Fixed-size arrays T[N]: the length N is an integer literal or a declared integer const (e.g. byte[PACKET_BUFFER_SIZE]), so the size stays statically known: sizeof(T[N]) = N * sizeof(T).
• No recursion: a struct may not contain itself, directly or indirectly. This guarantees sizeof is computable at compile time by recursive field traversal.
• Fields must have fixed-width types (uint32, not int; arrays of fixed-width elements) so the layout is well-defined.
• Struct names are usable wherever a type is expected — variable declarations, typed channel buffers (via buf<Packet>), and sizeof.

Constants

• Names use SCREAMING_SNAKE_CASE by convention; a declared type is required.
• The right-hand side is a full expression, folded at compile time (rustc-style, before any lowering). The const subset covers: literals, references to previously declared constants, sizeof(T), and unary/binary arithmetic, bitwise, shift, comparison, and logical operators.
• Function calls, runtime variables, and field access are rejected in const position. Forward references between constants are errors — declare in dependency order.
• The folded value must match the declared type (bool constants take boolean values; integer-family types take integers).

Program-local structs

A .fi program may declare structs of its own, with the same grammar and rules as system structs. These are PD-internal types — device-ring descriptors, driver bookkeeping — that never cross a channel:

// eth_outer.fi
struct Rbd {
    data_length: uint16;
    flags:       uint16;
    addr:        uint32;
}

ring: Rbd;

Scoping:

• A local struct is visible only within its own program — other PDs and the .fis cannot reference it. Channel buffer payload types must be system structs: system structs are the project’s communication types (what may cross a channel), local structs are program types (PD-internal state) — the two tiers of the data model.
• A local struct may contain system structs in its fields; the reverse is impossible.
• A local struct may not reuse the name of a system struct (shadowing is an error), so every type name means one thing across the project.
• Array lengths in local fields may reference system constants.

The C backend emits system structs and constants into a shared header named after the .fis file — <project>_types.h (e.g. datadiode_types.h) — and each PD’s local structs into a per-PD header, <pd>_types.h (e.g. eth_outer_types.h), included by the PD’s generated unit and importable by that PD’s hand-written driver code. A PD may not share the project’s name if it declares local structs (the two headers would collide).

Global state

The data layer declares types and constants, not mutable state. In CoreFi, shared global state is exactly the channel-buffer view: mutable data lives in declared memory regions, mapped explicitly into the PDs that may touch it and labelled for information flow. A shared scalar is a typed slot of a declared region — never an ambient global.

Memory Region Declarations

MemoryRegionDecl ::= SecurityLabel? 'MemoryRegion' ident '(' size (',' page_size)? (',' phys_addr)? ')' ';'
size             ::= hex
page_size        ::= hex      // '0x1000' (4 KiB) | '0x200000' (2 MiB)
phys_addr        ::= hex
SecurityLabel    ::= 'High' | 'Low'

A memory region declaration introduces one named region of physical or virtual memory that protection domains can later map into their address space. MemoryRegion declarations live in .fis system files; they are pure topology and carry no per-PD program logic.

Fields

• Security label (optional, defaults to Low). Tags information-flow level. High regions can be mapped only into PDs that themselves carry flow restrictions consistent with the flows_to lattice — see Information-flow labels.
• Name — snake_case identifier; the same name is referenced from Mapping declarations in .fi files.
• Size — required, hex literal, in bytes. Must be a multiple of the region’s page size (validation runs post-parse and reports a size not aligned error if not).
• Page size — optional, defaults to 0x1000 (4 KiB). The other accepted value is 0x200000 (2 MiB / Large).
• Physical address — optional. When present, must be aligned to the region’s page size. Used for device MMIO regions (clock controller, ethernet registers) where the seL4 loader maps a fixed physical frame rather than allocating one.

Security label and ordering

The label, if present, comes before the MemoryRegion keyword. Omitting it is equivalent to writing Low:

MemoryRegion ring_buffer_outer(0x1000, 0x1000);          // Low (default)
Low MemoryRegion eth0(0x10000, 0x10000, 0x5b040000);     // explicit Low
High MemoryRegion ring_buffer_inner(0x1000, 0x1000);     // High
High MemoryRegion eth_clk(0x1000, 0x1000, 0x5b200000);   // High MMIO

Validation

The following checks run after parsing:

1. size is a positive multiple of page_size.
2. phys_addr (if present) is aligned to page_size.
3. The region name is unique within the system file.

A region is referenced from .fi files by its name; the validator confirms each Mapping’s mem_region points at a declared MemoryRegion.

Examples

// Anonymous shared buffer, default 4 KiB page, allocator-assigned phys_addr.
MemoryRegion ring_buffer_outer(0x1000, 0x1000);

// 2 MiB region — large pages, allocator-assigned phys_addr.
MemoryRegion packet_buffer_outer(0x200000, 0x200000);

// Memory-mapped device (4 KiB MMIO, fixed physical address).
Low MemoryRegion eth_outer_register(0x1000, 0x1000, 0xf000000);

// 64 KiB device register window.
Low MemoryRegion eth0(0x10000, 0x10000, 0x5b040000);

// High-side region (any access from a Low PD will be rejected by the
// information-flow check).
High MemoryRegion eth_clk(0x1000, 0x1000, 0x5b200000);

Protection Domain Declarations

ProtectionDomainDecl ::= 'ProtectionDomain' ident '(' priority (',' irq)? (',' budget)? (',' period)? ')' ';'
priority             ::= integer_literal       // 0 ≤ p ≤ 254, enforced
irq                  ::= integer_literal       // fits u16; range not enforced
budget               ::= integer_literal       // microseconds, default 1000
period               ::= integer_literal       // microseconds, default = budget

A protection-domain declaration introduces one named seL4 Microkit protection domain (PD): an isolated thread of execution with its own address space, scheduling parameters, and (optionally) one IRQ binding. Each ProtectionDomain listed in a .fis system file pairs with one .fi program file by name.

Fields

• Name — snake_case identifier. The matching <name>.fi file holds the PD’s mappings, events, and processes.
• Priority — required, range 0..=254. Out-of-range values are rejected with a parse-time error. Higher numbers run first under the Microkit fixed-priority scheduler.
• IRQ — optional; any value fitting a u16 parses (no range check is enforced by the compiler — pick a number the target board’s IRQ controller actually has). When present, the PD is wired to receive that hardware interrupt on the reserved irq channel and can observe it via irq?N / irq!N events.
• Budget — optional, microseconds; defaults to 1000. Microkit schedules the PD for at most budget microseconds out of every period.
• Period — optional, microseconds; defaults to whatever budget was set to. Setting period > budget produces a sub-rate scheduling policy.

The trailing fields are positional: to pin only the period, both irq and budget must precede it.

Validation

• priority must be in 0..=254.
• A PD name is unique within the system file.
• A PD that is referenced from a Channel or from the System = composition must be declared.
• A PD without a corresponding <name>.fi is rejected at link time (not at parse time).

Examples

// Three PDs with distinct priorities; IRQ on the outer driver only.
ProtectionDomain eth_outer(99, 159);
ProtectionDomain dd(150);
ProtectionDomain eth_inner(199, 155);

// A simulator with a low priority and no IRQ binding.
ProtectionDomain simulate(50);

// Explicit budget / period pair (sub-rate scheduling).
ProtectionDomain monitor(120, 0, 200, 1000);  // priority 120, IRQ 0, 200 µs / 1 ms

System composition

A .fis file ends with a System = ... clause that names the PDs to include and their composition operator (currently always |||, interleave). Every PD referenced in System must be declared above:

System = eth_outer ||| dd ||| eth_inner ||| simulate;

PDs declared but omitted from System are dead code and currently produce no error; this may tighten in a future revision.

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

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> or a declared data-layer struct (via eth_outer_output<Slot>). Without via, the channel is treated as a pure synchronisation point with no shared payload buffer. A struct payload is the channel’s communication type: it must be a system (.fis) struct — never a program-local struct — and the C backend types receive binders from it (o2d?pkt declares static struct Slot pkt;).

  A buffer region is implicitly mapped into both endpoint PDs (rw, cached) at compiler-allocated vaddrs — it must not also appear in an explicit Mapping, and it may back only one channel. Each endpoint’s generated unit declares the loader-patched symbols <region>_vaddr / <region>_size (and driver code may declare <region>_paddr on demand), named after the region, not a mapping.

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 Declarations → Channel events for the inline event grammar and Process Definitions for how channel events sit in a process expression.

Limitations

• A struct payload types the receive binder in the generated C, but the payload transport (the ring copy through the backing region) is not generated yet — it is an explicit follow-up under the data-diode case study (#201). The generated code marks the pending copy with a comment.
• Send-site type checking (c!e against the declared payload) needs expression typing and is tracked under the type-system work (#117).
• The Sync modifier rejects bidirectional <-> syntactically; sync bidirectional channels would require a richer call/reply protocol than the current implementation supports.

Imports and Mappings

Two declarations sit at the top of every .fi file: import brings an external C or Rust source file into scope under a chosen alias, and Mapping puts a memory region declared in the .fis into the protection domain’s address space.

Imports

ImportDecl ::= 'import' '"' FilePath '"' 'as' ident ';'
FilePath   ::= ident '.' ('c' | 'rs')

An import declaration names the external implementation that backs the PD’s computation events. The path is a single bare file name (no directories) ending in .c or .rs; the parser dispatches on the extension to record it as a C or Rust source. The alias becomes the prefix on every external call inside the PD.

import "eth.c" as eth;             // call: eth.send_frame(...)
import "dd.c" as dd;               // call: dd.forward_packet(...)
import "driver.rs" as driver;      // Rust source — same call shape

Multiple imports are allowed, and they may interleave with mappings — order does not matter for parsing. Each alias must be unique within the file.

Mappings

MappingDecl ::= SecurityLabel? 'Mapping' ident '(' region (',' vaddr)? ',' perms (',' cached)? ')' ';'

region      ::= ident                      // a MemoryRegion declared in .fis
vaddr       ::= hex                        // explicit virtual address (optional)
perms       ::= string_literal             // 'r', 'rw', 'rx', 'rwx', 'x', 'wx'
cached      ::= bool_literal               // default: true

A mapping declaration installs a MemoryRegion into the PD’s address space. The mapping’s name derives the auto-emitted setvar symbols (<mapping>_vaddr, _paddr, _size) patched into the PD’s ELF — see Boot Initialisation.

Fields

• Security label — High or Low prefix, default Low. The mapping inherits the region’s confidentiality; the type-checker rejects a Low mapping over a High region. See Information-flow labels below.
• Name — the mapping’s own identifier. Distinct from the region’s name; one region can have multiple mappings under different names.
• Region — the MemoryRegion declared in the .fis file.
• Vaddr (optional) — pin the mapping at a specific virtual address. If omitted, the loader allocates one. Hex literal.
• Permissions — a quoted string of r/w/x characters. Order and case are insensitive: "rw" and "WR" are equivalent. Write-only is rejected; at least r or x must be present. The accepted set is r, rw, rx, rwx, x, wx.
• Cached (optional, default true) — whether the mapping is cached in the CPU MMU. Device MMIO regions should be set false explicitly.

Examples

// Anonymous shared buffer at allocator-chosen vaddr, read-write, uncached.
Low Mapping ring_buffer(ring_buffer_outer, "rw", false);

// Same region, default cached flag (true).
Mapping packet_buffer(packet_buffer_outer, "rw");

// Pinned vaddr — useful for debugging or for binding two PDs to a
// shared layout that pre-allocates virtual addresses.
Low Mapping eth0(eth0, 0x2_000_000, "rw");

// High-side mapping. Backed by a High MemoryRegion; rejected if the PD
// or the region's label disagrees.
High Mapping eth_clk(eth_clk, 0x2_200_000, "rw");

// Read-only mapping (data-diode input).
Low Mapping input_buf(eth_outer_output, "r");

Information-flow labels

Both MemoryRegion and Mapping declarations may carry a High or Low prefix. The two-level lattice is:

flows_to(Low,  Low)  = true
flows_to(Low,  High) = true       // upgrade is fine
flows_to(High, Low)  = false      // downgrade is rejected
flows_to(High, High) = true

In source: Low is the default — omitting the prefix is equivalent to writing Low. Place the prefix before the MemoryRegion / Mapping keyword; placing it elsewhere is a parse error.

The validator runs after parsing and rejects any mapping that violates flows_to(region.label, mapping.label). The data-diode demo uses this to enforce one-way information flow at the type-checker.

Validation

• Each Mapping’s region must reference a declared MemoryRegion.
• Permission strings must contain at least one of r or x. "w" alone is rejected.
• A pinned vaddr must be aligned to the region’s page size.
• Mapping names are unique within the same .fi file.

Boot Initialisation: the microkit.init Process and Auto-Setvars

Boot-time behaviour of a protection domain is expressed in two ways:

1. Address binding is automatic: every Mapping exports its addresses to the imported C / Rust implementation through a naming convention (the setvar mechanism below). No syntax is required.
2. Boot-time logic is modelled by an ordinary process bound to the platform’s boot entry point with @bind(microkit.init) — the model-level counterpart of Microkit’s void init(void) entrypoint, which the imported source file implements.

ℹ️ Earlier versions of Fiducia used a special (): { ... } constructor block for both purposes. It was removed in #168; (): { is now a parse error.

The boot process

The boot process is the one annotated @bind(microkit.init). Its name carries no meaning — Init is a common choice, but the binding, not the name, is what makes it the boot entry point:

@bind(microkit.init)
proc Init() {
    setup_eth -> Skip;
}

Microkit calls the PD’s entrypoint exactly once, before any event is delivered, so the bound process must not contain channel receives or IRQ awaits. When it terminates (Skip), control falls through to the @bind(microkit.notified) event loop — exactly as the generated C init() runs the boot body and then arms notified().

A @bind(microkit.init) process is mandatory for every PD that has a .fi program when targeting Microkit (--emit=c or image generation): the kernel calls init() on every PD at startup. It is mandatory in tandem with @bind(microkit.notified) — Microkit invokes both, so a conforming PD binds both (any other platform entry points are optional). A PD with no boot work still declares a no-op:

@bind(microkit.init)
proc Init() { Skip; }

The requirement is enforced on the C / image path only. Pure verification models (--emit=xta) do not require kernel entry points.

Auto-emitted setvars

For every mapping named m, the compiler emits setvar candidates for three ELF symbols:

Before image generation (--emit=img), candidates whose symbol is not declared in the PD’s compiled ELF are dropped — the implementation only receives the symbols it declares. The Microkit loader patches the surviving symbols before the PD starts.

import "eth.c" as eth;

Low Mapping ring_buffer(ring_buffer_outer, "rw");
Low Mapping packet_buffer(packet_buffer_outer, "rw");

/* eth.c — declared symbols are patched by the loader */
uintptr_t ring_buffer_vaddr;    /* ← ring_buffer.vaddr  */
uintptr_t ring_buffer_paddr;    /* ← ring_buffer.paddr  */
uintptr_t packet_buffer_vaddr;  /* ← packet_buffer.vaddr */
/* packet_buffer_size not declared → no setvar emitted   */

Pick mapping names so that <mapping>_vaddr matches the symbol your implementation uses.

Derived values

setvar only supports literal-substitution patching: it cannot evaluate arithmetic. Values derived from a mapping address (for example, an offset into a ring buffer) are computed at runtime inside the implementation’s init function — or, in future, in proc Init once compile-time expression evaluation (#111) lands.

Validation

• Mapping names must be unique within a PD (checked by name resolution); this also guarantees the derived setvar symbols are unique.
• m_paddr is always linked: when the underlying MemoryRegion has an explicit physical address that value is patched in, otherwise the kernel assigns one at boot.

Variable Declarations

VarDecl ::= ident ':' Type ';'
Type    ::= BaseType ('[' ArrayLen ']')?
BaseType ::= PrimitiveType | StructName

A variable declaration introduces one named value at PD-global scope or inside an event body. The ident: Type; form is the only shape supported today; an initialiser (ident: Type = expr;) is reserved but not yet parsed.

🚧 Initialiser syntax (= expr) is reserved but unparsed — see #105. For now, initialise locals from inside the body, and globals from the imported source’s init() function (see Boot Initialisation).

Scopes

Variables can appear in two positions inside a .fi file:

• Global — at the top level of the file, alongside Mapping and import declarations. Globals are visible everywhere in the PD, read/write inside event bodies.
• Local — inside a computation event body. Locals shadow globals of the same name. Their scope ends where the enclosing event’s body ends — implicitly, at the next top-level item (evt, proc, import, Mapping), since there is no explicit terminator keyword.

Process bodies cannot declare variables; any state needed by guards or process expressions must be promoted to a global.

The full scope-resolution order inside an event body is:

local → carrier → global

Carriers are the read-only inputs declared in the event header — see Event Declarations.

Primitive types

The primitive types accepted in declarations are:

int and uint without a width default to 32-bit. byte is an alias for uint8. There is no void type — every declared variable has a concrete, storable type.

Struct types and arrays

pkt: Slot           // user-defined struct — declared in the .fis data layer
buf: uint8[16]       // fixed-size array — length is a literal or const name

Any identifier that isn’t a recognised primitive keyword is treated as a struct type name, resolved against the .fis struct declarations during name resolution (unknown names are rejected there, not at parse time). Fiducia has no pointer types — there is no ptr<T> syntax.

Examples

// Global declarations, top of a .fi file.
counter: int;
ready: bool;
last_irq_ts: uint64;

// Local declarations inside an event body.
evt handle_packet.|size: int|:
    local_buf: uint8[64];     // local
    ok: bool;                 // local
    local_buf = eth.alloc();  // assignment uses globals/locals/carriers

Validation

• A variable name is unique within its enclosing scope (multiple globals with the same name are rejected; a local may legally shadow a global).
• The type must be a recognised primitive, Address, a fixed-size array of one, or a struct name that resolves to a real .fis struct declaration.

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.

Process Definitions

ProcessDecl ::= Bind? 'proc' UIdent '(' (Param (',' Param)*)? ')' '{' ProcessBody '}'
Bind        ::= '@bind' '(' ident '.' ident (',' ident '.' ident)* ')'
Param       ::= ident ':' Type

ProcessBody ::= BodyItem (';' BodyItem)* ';'?
BodyItem    ::= VarDecl | ProcessExpr
VarDecl     ::= ident ':' Type ';'
ProcessExpr ::= 'Skip'
             |  'Div'
             |  Event '->' ProcessExpr
             |  '[' Guard ']' ProcessExpr
             |  ProcessExpr ('[]' ProcessExpr)+ ('default' ProcessExpr)?
             |  ProcessRef
             |  '(' ProcessExpr (';' ProcessExpr)* ';'? ')'
ProcessRef  ::= UIdent '(' (ident (',' ident)*)? ')'
Guard       ::= Expr   -- boolean-shaped: comparison, &&/||/!, boolean
                        -- variable/call/field access; not arithmetic

A process definition is the orchestration layer of a Fiducia protection domain — a CSP-style algebraic expression composed from events, guards, choices, and sequential composition. Each proc declaration introduces one named process; all proc declarations in the same .fi file are mutually visible and may reference each other by name.

proc definitions must appear after all evt declarations in the same file; the compiler rejects a proc that is followed by an evt.

Following CoreFi paper §4.2, a process expression is one of:

Naming convention

Process names use UpperCamelCase. This both signals intent and disambiguates process references from computation event references at parse time:

• Reply(pkt) — sub-process call (UpperCamelCase, parentheses required).
• send_frame.pkt — computation-event reference (snake_case, dot carrier syntax).

The disambiguation happens on the leading character of the identifier. The boot process is the one bound with @bind(microkit.init); Init is a conventional name but carries no special meaning (see Boot Initialisation).

Annotations (@bind)

A process may carry a single @bind(...) annotation mapping it to one or more platform entry points, without hardcoding kernel terminology into process names. Group the targets — one platform.entry pair per platform — on one line:

@bind(microkit.notified, cheri.interrupt_handler)
proc Notified() { o2d?pkt -> d2i!pkt -> Notified(); }

• A process with no @bind is internal — not directly callable by the kernel.
• @bind is authoritative for entry-point selection. The C backend and the UPPAAL lowering pick kernel entry points by binding, not by process name: the microkit.init-bound process becomes init() (the boot body) and the microkit.notified-bound process becomes the notified() event loop.
• Both a @bind(microkit.init) and a @bind(microkit.notified) process are mandatory for every PD with a program when targeting Microkit (--emit=c or image generation) — Microkit invokes both on every PD. See Boot Initialisation. --emit=xta (verification only) does not require them. Other platform entry points are optional.
• Each entry point binds at most one process. Two processes both @bind(microkit.notified) is an error — resolution rejects the second rather than silently keeping the first.

The target platform is chosen with --platform (e.g. --platform=microkit); omit it to compile whatever the annotations bind. A platform fic does not support is rejected.

Resolving bindings to a platform’s concrete kernel symbols — and rejecting unknown or conflicting targets across platforms — remains the project layer’s job (fire, configured in fire.toml); see #190.

Operator precedence

From loosest to tightest:

Concrete consequences:

e -> P() [] e2 -> Q()            ≡ Choice([Prefix(e, P()), Prefix(e2, Q())])
e -> P() ; Q()                   ≡ (e -> P()) ; Q()
[b] e -> P() [] e2 -> Q()        ≡ Choice([Guard(b, Prefix(e, P())), Prefix(e2, Q())])
p1() ; p2() [] p3()              ≡ p1() ; (p2() [] p3())
[b] (e -> P() [] e2 -> Q())      ≡ Guard(b, Choice(...))   // outer-guard the choice

Parenthesisation cuts through: (...) re-enters at the top of the precedence chain.

Choice and discriminators

Every branch of a [] choice must carry a discriminator — a distinguishing prefix that the surrounding environment can pattern-match on. The parser checks structurally and recurses into a branch’s first sequential item and into nested choices; deferred resolution is required only for ProcessRef (the validator follows the name).

Common discriminator shapes:

e -> P()                // event prefix
[b] P()                 // guard
c?x -> ...              // channel-event prefix

The optional default arm is taken when no branch’s guard succeeds.

Examples

// Two branches, no default.
proc Dispatch() {
    [rx] receive -> Skip [] [!rx] cleanup -> Skip;
}

// Two branches with a fallback.
proc Reply(pkt: int) {
    [pass]  o2d!pkt -> Skip
 [] [!pass] handle_ping -> Skip
    default Skip;
}

Guards

Guard ::= ident | '!' ident

A guard gates the next process expression on a boolean variable. Today the parser accepts only [var] (variable read) and [!var] (negation); the variable must be a global declared in the same .fi file. The guard binds tighter than []:

[b] e -> P [] e2 -> Q   ≡   ([b] (e -> P)) [] (e2 -> Q)

The guard applies only to the first branch.

🚧 Full boolean / relational guard expressions ([x == 3], [x && y], etc.) land with the expression grammar — see #105. Until then, decompose with intermediate globals if a guard needs richer logic.

Sequential composition

Inside a {} body, ; separates items. The last item may carry a trailing ; before }:

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

Sub-process calls

ProcessRef ::= UIdent '(' (ident (',' ident)*)? ')'

A sub-process call references another process declared in the same file. The argument list is currently restricted to identifiers. Parentheses are always required — even for empty argument lists (Skip and Div are the only bare uppercase atoms):

proc Notified()   { irq?159 -> Handle_eth(); irq!159 -> Notified(); }
proc Handle_eth() { handle_irq -> Dispatch(); }
proc Dispatch()   { [rx] receive -> Skip [] [!rx] cleanup -> Skip; }
proc Reply(pkt: int) { o2d!pkt -> Skip; }

The validator confirms each ProcessRef resolves to a declared process and that the argument count matches.

Empty processes

Skip and Div are atomic and self-contained: Skip is successful termination, Div is divergence (a self-loop):

proc NoOp()  { Skip; }
proc Stuck() { Div; }

Limitations

• Argument lists for ProcessRef and computation-event references are restricted to identifiers. Channel-receive RHS accepts identifiers or integer literals (so irq?159 parses).
• Guards accept [var] / [!var] only.
• Currently only variable declarations (x: int;) are permitted as inline body items alongside process expressions. Assignment statements and external calls must live in evt declarations. This restriction is planned to be lifted: future versions will allow statements directly in proc bodies, with flexible interleaving of statements and process expressions.
• Recursion is modeled as a sub-process call by name.

Expressions

This chapter describes the expression grammar fic actually parses. Expressions appear as:

• the right-hand side of assignments inside event bodies;
• the payload of a channel send (c!e);
• the body of a guard ([b]);
• arguments to calls, sub-process calls, and computation-event carriers.

One grammar (Expr) covers literals, variables, calls, sizeof, unary and binary operators, and field access. There’s no separate arithmetic vs. logical vs. boolean sub-grammar — a boolean-shaped subset of Expr is what’s required in guard position (see below), not a different grammar.

Expr    ::= Lit | ident | CExpr | 'sizeof' '(' Type ')'
          | UnOp Expr | Expr BinOp Expr
          | FieldBase '.' ident           -- field access
FieldBase ::= ident | CExpr | FieldBase '.' ident  -- var, call, or field chain

Lit     ::= int_lit | hex_lit | bool_lit
UnOp    ::= '-' | '!' | '~'
BinOp   ::= '+' | '-' | '*' | '/' | '%'
          | '==' | '!=' | '<' | '<=' | '>' | '>='
          | '&&' | '||'
          | '&' | '|' | '^' | '<<' | '>>'

Operator precedence

Loosest to tightest:

Call expressions (CExpr)

CExpr ::= ident '.' ident '(' (Expr (',' Expr)*)? ')'

A call expression invokes a function defined in an imported .c file, prefixed with the import alias chosen at the import declaration. The alias is required — there are no local callables in Fiducia, only externally-implemented functions reached through an alias.

The first ident is the alias; the second is the function name. No whitespace is permitted around the . or before the (:

eth.send_frame()                  // OK
eth.send_frame(pkt, len)          // OK — arguments are full Expr, comma-separated
drv .start()                      // rejected — whitespace before '.'
drv. start()                      // rejected — whitespace after '.'
drv.start ()                      // rejected — whitespace before '('

Guard expressions

A guard ([b] P) requires a boolean-shaped Expr — arithmetic like [a + b] is rejected at parse time, since a guard must denote a yes/no decision, not a value. Boolean-shaped means: a boolean literal, a variable, a call, a field access, a !-negated boolean-shaped expression, or a comparison/&&/|| combination of boolean-shaped expressions.

[a + b == c]              // OK — comparison of arithmetic is boolean-shaped
[eth.is_forward()]         // OK — call
[!flag && ready]           // OK — negation + conjunction
[true]                     // OK
[a + b]                    // rejected — arithmetic isn't boolean-shaped