Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

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