Boot Initialisation: the microkit.init Process and Auto-Setvars

Boot-time behaviour of a protection domain is expressed in two ways:

1. Address binding is automatic: every Mapping exports its addresses to the imported C / Rust implementation through a naming convention (the setvar mechanism below). No syntax is required.
2. Boot-time logic is modelled by an ordinary process bound to the platform’s boot entry point with @bind(microkit.init) — the model-level counterpart of Microkit’s void init(void) entrypoint, which the imported source file implements.

ℹ️ Earlier versions of Fiducia used a special (): { ... } constructor block for both purposes. It was removed in #168; (): { is now a parse error.

The boot process

The boot process is the one annotated @bind(microkit.init). Its name carries no meaning — Init is a common choice, but the binding, not the name, is what makes it the boot entry point:

@bind(microkit.init)
proc Init() {
    setup_eth -> Skip;
}

Microkit calls the PD’s entrypoint exactly once, before any event is delivered, so the bound process must not contain channel receives or IRQ awaits. When it terminates (Skip), control falls through to the @bind(microkit.notified) event loop — exactly as the generated C init() runs the boot body and then arms notified().

A @bind(microkit.init) process is mandatory for every PD that has a .fi program when targeting Microkit (--emit=c or image generation): the kernel calls init() on every PD at startup. It is mandatory in tandem with @bind(microkit.notified) — Microkit invokes both, so a conforming PD binds both (any other platform entry points are optional). A PD with no boot work still declares a no-op:

@bind(microkit.init)
proc Init() { Skip; }

The requirement is enforced on the C / image path only. Pure verification models (--emit=xta) do not require kernel entry points.

Auto-emitted setvars

For every mapping named m, the compiler emits setvar candidates for three ELF symbols:

Before image generation (--emit=img), candidates whose symbol is not declared in the PD’s compiled ELF are dropped — the implementation only receives the symbols it declares. The Microkit loader patches the surviving symbols before the PD starts.

import "eth.c" as eth;

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

/* eth.c — declared symbols are patched by the loader */
uintptr_t ring_buffer_vaddr;    /* ← ring_buffer.vaddr  */
uintptr_t ring_buffer_paddr;    /* ← ring_buffer.paddr  */
uintptr_t packet_buffer_vaddr;  /* ← packet_buffer.vaddr */
/* packet_buffer_size not declared → no setvar emitted   */

Pick mapping names so that <mapping>_vaddr matches the symbol your implementation uses.

Derived values

setvar only supports literal-substitution patching: it cannot evaluate arithmetic. Values derived from a mapping address (for example, an offset into a ring buffer) are computed at runtime inside the implementation’s init function — or, in future, in proc Init once compile-time expression evaluation (#111) lands.

Validation

• Mapping names must be unique within a PD (checked by name resolution); this also guarantees the derived setvar symbols are unique.
• m_paddr is always linked: when the underlying MemoryRegion has an explicit physical address that value is patched in, otherwise the kernel assigns one at boot.