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 theEvents:andProcess: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
textblocks; Fiducia is not Rust, andtextkeeps 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).