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

The Project Manifest (fire.toml)

fire reads a fire.toml manifest from the project directory. It names the project, locates the sources, and configures how fire build / fire run build and execute the image and how fire verify invokes the model checker.

🚧 This page documents the manifest schema introduced with the fire build / fire run / fire verify subcommands (PR #174). Until that lands on a release, the previous [target] / [qemu] layout applies — see the CHEATSHEET.md of your installed version.

Complete example

[project]
name = "datadiode"     # output filename stem: build/datadiode.img / .xml
src  = "."             # directory with the .fis/.fi files, relative to this file

[run]
mode = "qemu"          # qemu | hardware (hardware is not yet implemented)
# Arguments for qemu-system-aarch64; {img} is substituted with the
# absolute path to the built image at runtime.
args = [
    "-machine", "virt,virtualization=on",
    "-cpu",     "cortex-a53",
    "-serial",  "mon:stdio",
    "-device",  "loader,file={img},addr=0x70000000,cpu-num=0",
    "-m",       "size=2G",
    "-nographic",
]

[run.target]
board   = "qemu_virt_aarch64"   # Microkit board identifier
profile = "debug"               # debug | release
# sdk / gcc / ld — optional, fall back to $MICROKIT_SDK / $GCC / $LD
# allow_wf2_cycles = true       # skip WF2 when `fire verify` covers deadlock-freedom

[verify]
mode = "verifyta"               # verification engine
# path / args — optional; path falls back to $VERIFYTA / PATH

[project] — identity and sources

FieldRequiredDescription
nameyesShort name used as the output filename stem: fire build / fire run write build/<name>.img, fire verify writes build/<name>.xml and reads the hand-written <src>/<name>.q.
srcyesDirectory containing the .fis / .fi files, relative to fire.toml. Build artifacts go to <src>/build/.

[run] — execution mode and arguments

FieldRequiredDescription
modeyesqemu or hardware. Hardware deployment is not yet implemented.
argsyesArguments passed verbatim to the executor (qemu-system-aarch64 in QEMU mode). The placeholder {img} is substituted with the absolute path to the built .img.

[run.target] — board and toolchain

FieldRequiredDescription
boardyesMicrokit board identifier, e.g. qemu_virt_aarch64, kria_k26. Must exist in the SDK’s board/ directory.
profileyesMicrokit build profile: debug or release.
sdknoPath to the Microkit SDK root. Falls back to $MICROKIT_SDK.
gccnoAArch64 cross-compiler binary. Falls back to $GCC.
ldnoAArch64 cross-linker binary. Falls back to $LD.
allow_wf2_cyclesnoPass --allow-wf2-cycles to fic: skip the structural WF2 acyclicity check. Use when deadlock-freedom is established by fire verify instead — WF2 rejects cyclic topologies even when they are deadlock-free under a fair scheduler. Default false.

When sdk / gcc / ld are set they are passed to the fic child process as environment variables, overriding any values already in your environment — useful for pinning a toolchain per project.

[verify] — formal verification

Optional section; configures fire verify.

FieldRequiredDescription
modeyesVerification engine. Currently verifyta (UPPAAL); spin, prism, … may follow.
pathnoPath to the verifier binary. Falls back to $VERIFYTA, then to verifyta on PATH.
argsnoExtra flags appended after the model and query arguments.

Worked example

The repository’s demo/datadiode/fire.toml is a complete, runnable manifest for the data-diode demo — three protection domains (eth_outer, dd, eth_inner) built into one image and launched on qemu_virt_aarch64 with two virtio-net devices, driven from the host (demo/datadiode/inject.py) since a foreign-MAC diode needs raw frames a NAT can’t deliver.