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, the constructor block, global variable declarations, and the Events: and Process: sections 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’s Events: section.

Scope of this revision

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

• Event Blocks — the Events: section that declares computation events, plus the inline channel and IRQ events used on the left of a process prefix.
• Process Blocks — the Process: section that declares CSP-style processes composed from events, guards, choices, and sequential composition.
• Expressions — the expression language available to carriers, guards, send payloads, and (eventually) constructor RHS.

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

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 ::= 'Event' ident carriers? ':' stmt* 'end'
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:

Event handle_irq:
    eth.handle_irq();
end

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.

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). See Page sizes.
• 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
irq                  ::= integer_literal       // 0 ≤ irq ≤ 159
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, constructor block, 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, range 0..=159. 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>. 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.

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: false

A mapping declaration installs a MemoryRegion into the PD’s address space. The mapping’s name becomes a globally-visible symbol inside the PD; the Constructor block can then reference its .vaddr, .paddr, or .size.

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 false) — whether the mapping is cached in the CPU MMU. Device MMIO regions are typically false.

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

Constructor Block

ConstructorBlock ::= '(' ')' ':' '{' Assign* '}'
Assign           ::= ident '=' RHS ';'
RHS              ::= ident '.' MappingField
                   | <anything up to the terminating ';'>
MappingField     ::= 'vaddr' | 'paddr' | 'size'

The constructor block is the per-PD initialiser that runs before the PD’s first event. It binds globals declared in the imported .c / .rs file to either:

• a mapping field — mapping.vaddr, mapping.paddr, or .size — in which case the value is patched into the binary by the seL4 Microkit loader before the PD starts (via the setvar mechanism); or
• an opaque expression — anything up to the terminating ; — in which case the assignment runs at PD-init time inside the imported source’s init() function.

There is at most one constructor block per .fi file. Its leading (): borrows the empty-parameter-list shape; the parens are required even though there are no parameters yet.

Mapping-field RHS

The compiler classifies the RHS as a mapping field only when it is exactly mapping.field, with nothing between the field name and the terminating ; (whitespace excepted). The matched fields are:

Each matched assignment becomes one SDF setvar entry in the lowered output. The Microkit loader patches the named symbol in the PD’s ELF before launch.

(): {
    rbd = ring_buffer.vaddr;            // setvar "rbd" → vaddr
    tbd = ring_buffer.size;             // setvar "tbd" → size in bytes
    pa  = packet_buffer.paddr;          // setvar "pa"  → physical address
}

Opaque RHS

Any RHS that is not exactly mapping.field is recorded as an opaque blob and emitted into the PD’s runtime init code rather than as setvar. The parser consumes verbatim up to the next ;.

(): {
    tbd = ring_buffer.vaddr + (sizeof(struct rbd) * RBD_COUNT);  // opaque
    irq_ack_index = 0;                                            // opaque
}

This split exists because setvar only supports literal-substitution patching: it cannot evaluate arithmetic. Anything more elaborate than a direct field read is deferred to runtime initialisation in the imported source file.

🚧 Constructor block is being unified with the broader statement grammar and the expression grammar — see #128. Once that lands, the mapping-field / opaque distinction moves out of the AST and the constructor body becomes a plain sequence of statements.

Example

import "eth.c" as eth;

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

(): {
    ring_buffer_vaddr  = ring_buffer.vaddr;       // setvar
    packet_buffer_vaddr = packet_buffer.vaddr;    // setvar
    ring_buffer_paddr  = ring_buffer.paddr;       // setvar
    packet_buffer_paddr = packet_buffer.paddr;    // setvar

    rbd_count = RBD_COUNT;                         // opaque (runtime init)
}

Validation

• The mapping referenced on the left of .vaddr / .paddr / .size must exist in the same .fi file.
• .paddr is rejected if the underlying MemoryRegion was declared without an explicit physical address.
• Only one constructor block per .fi; a second (): block is a parse error.

Variable Declarations

VarDecl ::= Type ident ';'
Type    ::= PrimitiveType | 'ptr' '<' Type '>' | StructName

A variable declaration introduces one named value at PD-global scope or inside an event body. The bare Type ident; form is the only shape supported today; an initialiser (Type ident = 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 Constructor block or the imported source’s init() function.

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 and the constructor.
• Local — inside a computation event body, between the : and end. Locals shadow globals of the same name. Their scope ends with the end of the enclosing event.

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

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.

Pointer and struct types

ptr<int>            // pointer to int
ptr<ptr<int>>       // pointer to pointer
struct rbd          // user-defined struct (parser support pending)

Pointer parsing exists in the grammar as 'ptr' '<' Type '>'; struct type parsing is reserved for a later revision and is gated on the struct-declaration grammar.

Examples

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

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

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, a pointer to a recognised type, or a declared struct (struct support pending).

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.

Process Blocks

ProcessSection ::= 'Process' ':' ProcessDecl+

ProcessDecl    ::= ident '(' (Param (',' Param)*)? ')' '=' ProcessBody ';'
Param          ::= ident ':' Type

ProcessBody    ::= ProcessExpr (';' ProcessExpr)*
ProcessExpr    ::= 'Skip'
                |  'Div'
                |  Event '->' ProcessExpr
                |  '[' Guard ']' ProcessExpr
                |  ProcessExpr ('[]' ProcessExpr)+ ('default' ProcessExpr)?
                |  ProcessRef
                |  '(' ProcessBody ')'
ProcessRef     ::= ident ('(' (ident (',' ident)*)? ')')?
Guard          ::= ident | '!' ident

A process block is the orchestration layer of a Fiducia protection domain — a CSP-style algebraic expression composed from events, guards, choices, and sequential composition. Each Process: section declares one or more named processes; multiple sections in the same .fi merge into a single process list.

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

Naming convention

Process names start with an UpperCamelCase first letter — this both signals intent and lets the parser detect the start of a new declaration while consuming a body. The convention also disambiguates:

• Reply(pkt) — sub-process call (UpperCamelCase, parses as a process expression).
• send_frame(pkt) — computation-event reference (snake_case, parses as an event).

The disambiguation happens at parse time on the leading character of the identifier; do not lowercase a process name or capitalise an event name.

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. default and otherwise are both currently accepted as the keyword for the default branch; default is the canonical form (paper choice).

Examples

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

// Two branches with a fallback.
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 (process bodies cannot declare their own state). The guard binds tighter than [] — [b] e -> P [] e2 -> Q guards the first branch only.

🚧 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 body is not a list of declarations — it is a single process expression with ;-composed sub-expressions:

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

The trailing ; after Notified() is the declaration terminator, not the sequential operator. Inside the body, ; separates expressions.

Sub-process calls

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

A sub-process call references another process declared in the same section. The argument list is currently restricted to identifiers (the expression grammar will widen this). Argument-less calls may also drop the parentheses entirely:

Process:
    Notified() = irq?159 -> Handle_eth() ; irq!159 -> Notified();
    Handle_eth() = handle_irq -> Dispatch ;        // empty arg list, no parens
    Dispatch() = [rx] receive -> Skip [] [!rx] cleanup -> Skip ;
    Reply(pkt: int) = o2d!pkt -> Skip ;

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

Empty processes

Skip and Div are atomic and self-contained: Skip is successful termination, Div is non-termination (Ω). Both stand alone as a body:

Process:
    NoOp() = Skip;
    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.
• No variable declarations inside a process body — promote to a global.
• Recursion is modeled as a sub-process call by name, e.g. the trailing Notified() in Notified() = ... -> Notified();.

Expressions

This chapter describes the expression grammar designed for Fiducia and the subset that today’s parser actually accepts. Expressions appear as:

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

The grammar is divided into four sub-languages: arithmetic (integer- valued), logical (boolean / relational), boolean (lifted), and call expressions. Only call expressions are fully implemented today. The others are flagged 🚧 below.

Expr  ::= AExpr | LExpr | BExpr | CExpr

Call expressions (CExpr)

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

A call expression invokes a function defined in an imported .c / .rs 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
drv.start()                       // OK
drv .start()                      // rejected — whitespace before '.'
drv. start()                      // rejected — whitespace after '.'
drv.start ()                      // rejected — whitespace before '('

Argument lists

Argument parsing is currently a stub: the parser accepts an empty (...) argument list and stores Vec::new() for the args. Once the rest of the expression grammar lands, arguments will be Vec<Expr> and the call site shape (eth.send_frame(pkt)) will parse as expected.

🚧 Argument parsing for call expressions is gated on the broader expression grammar — see #105. Today, only () is accepted; calls with arguments parse only inside places that do their own identifier-list handling (sub-process calls, computation-event carriers).

Arithmetic expressions (AExpr)

🚧 Not yet implemented — see #105.

The designed grammar covers integer literals, variables, unary negation, and the standard binary arithmetic operators (+, -, *, /, %). Until the grammar lands, integer values appear in source only as literals at fixed positions (IRQ numbers, page sizes, sizes / phys-addrs in MemoryRegion).

Logical expressions (LExpr)

🚧 Not yet implemented — see #105.

The designed grammar covers comparison (==, !=, <, <=, >, >=) and boolean composition (&&, ||, !). Until the grammar lands, guards accept only [var] and [!var].

Boolean expressions (BExpr)

🚧 Not yet implemented — see #105.

A lifted boolean form for use as a payload type, distinct from LExpr which composes other relations. Likely to merge into LExpr in the final grammar — tracked under #105.

Stand-ins for unimplemented forms

Where the grammar currently lacks a construct, the surrounding parser accepts a narrow stand-in so existing fixtures continue to parse:

These accept-narrow / reject-everything-else windows keep the parser honest: every position where an expression should go either has a fully-typed Expr (via CExpr) today, or accepts a clearly-restricted shape that surfaces an error if you reach for an un-implemented form.