The `fic` Compiler

fic is the Fiducia compiler. fire drives it for the common build-and-run / verify workflows; invoke it directly to check a project, build an image with explicit flags, or inspect any intermediate representation.

fic <PROJECT_DIR> --board <BOARD> --build-profile <PROFILE> [-o <IMG>]   # image (default)
fic <PROJECT_DIR> --check                                               # front-end only
fic <PROJECT_DIR> --emit=<FORMAT> [-o <PATH>]                           # inspection emits

PROJECT_DIR is a directory containing exactly one .fis file and one .fi file per protection domain (bound by filename: eth_outer.fi implements PD eth_outer).

By default — like rustc, whose default output is a binary — fic compiles the project to a bootable Microkit image: it runs the full front-end, lowers to SDF, cross-compiles each PD’s C file, patches the setvars, and packs the loader, seL4 kernel, and PD ELFs into <project>.img. This requires --board / --build-profile and the MICROKIT_SDK / GCC / LD environment.

With --check, fic stops after the front-end — parse, data-layer resolution, name resolution, vaddr materialization, information-flow typecheck, WF2 acyclicity — and reports diagnostics without writing any output (the cargo check of Fiducia):

$ fic demo/datadiode/ --check
  ✓ Parsed 1 system + 3 program files
  ✓ Resolved data layer (2 structs, 1 consts)
  ✓ Resolved names
  ✓ Resolved mapping vaddrs
  ✓ Type-checked information flow
  ✓ Checked channel dependency acyclicity (WF2)

`--emit` formats

--emit replaces the default image output with an intermediate representation:

Format	Output (default path)	Description
`rawast`	stdout / `-o`	Parsed AST as JSON, before validation.
`ast`	stdout / `-o`	Validated AST as JSON (vaddrs allocated, names resolved).
`c`	`<project>/build/gen/`	Generated per-PD C state machines plus `<project>_types.h`/`<pd>_types.h`. No image is built.
`sdf`	`<project>.system`	SDF IR as XML — debug bridge for Microkit developers.
`dot`	`<project>.dot`	Graphviz topology graph. Render with `dot -Tpng <project>.dot -o topology.png`.
`xta`	`<project>.xml`	UPPAAL XTA model. Queries are user-authored — see `fire verify`.

The inspection formats (rawast, ast, c, dot) skip the WF2 check — they have no deployment target. xta exists precisely to analyse cyclic systems, so it also skips WF2; image generation (the default) and sdf enforce it.

Options

`--check`

Run the front-end only; produce no artifact. Conflicts with --emit.

`-o, --output <PATH>`

Override the default output path for the image or the chosen emit mode.

`--board <BOARD>`, `--build-profile <PROFILE>`

Required for image generation (the default mode): the Microkit board identifier (e.g. qemu_virt_aarch64, kria_k26) and build profile (debug / release). Must match a directory under $MICROKIT_SDK/board/.

`--allow-wf2-cycles`

Skip the WF2 acyclic-channel-dependency check.

WF2 is a structural over-approximation: it rejects any cyclic channel dependency graph, including programs that are deadlock-free under a fair scheduler (e.g. the asymmetric dining philosophers, Hoare CSP §2.5.4). Use this flag when deadlock-freedom is established by an external authority — typically fire verify on the emitted UPPAAL model.

Language server

The Language Server Protocol server is a separate binary, fic-lsp (analogous to rust-analyzer vs rustc), built from the fic-lsp workspace crate and used by the editor integrations under editors/. Install it with cargo install --path fic-lsp; it speaks LSP on stdio.

Environment variables

Variable	Needed by	Description
`MICROKIT_SDK`	image generation	Path to the extracted Microkit SDK.
`GCC`	image generation	AArch64 cross-compiler binary.
`LD`	image generation	AArch64 cross-linker binary.
`RUST_LOG`	debugging	Log verbosity (`debug`, `info`, `warn`).
`RUST_BACKTRACE`	debugging	Show backtraces on panic (`1` or `full`).

Diagnostics

Errors are rendered as annotated source snippets with the offending span highlighted — parse errors, duplicate names, undeclared references, vaddr misalignment / overlaps, information-flow violations, and WF2 cycles all point back to the .fis / .fi source location.

Exit status

fic exits 0 on success and non-zero when any pipeline stage reports diagnostics, making it safe to use in scripts and CI.

Keyboard shortcuts

The Fiducia User Manual