Process Definitions

ProcessDecl ::= Bind? 'proc' UIdent '(' (Param (',' Param)*)? ')' '{' ProcessBody '}'
Bind        ::= '@bind' '(' ident '.' ident (',' ident '.' ident)* ')'
Param       ::= ident ':' Type

ProcessBody ::= BodyItem (';' BodyItem)* ';'?
BodyItem    ::= VarDecl | ProcessExpr
VarDecl     ::= ident ':' Type ';'
ProcessExpr ::= 'Skip'
             |  'Div'
             |  Event '->' ProcessExpr
             |  '[' Guard ']' ProcessExpr
             |  ProcessExpr ('[]' ProcessExpr)+ ('default' ProcessExpr)?
             |  ProcessRef
             |  '(' ProcessExpr (';' ProcessExpr)* ';'? ')'
ProcessRef  ::= UIdent '(' (ident (',' ident)*)? ')'
Guard       ::= Expr   -- boolean-shaped: comparison, &&/||/!, boolean
                        -- variable/call/field access; not arithmetic

A process definition is the orchestration layer of a Fiducia protection domain — a CSP-style algebraic expression composed from events, guards, choices, and sequential composition. Each proc declaration introduces one named process; all proc declarations in the same .fi file are mutually visible and may reference each other by name.

proc definitions must appear after all evt declarations in the same file; the compiler rejects a proc that is followed by an evt.

Following CoreFi paper §4.2, a process expression is one of:

Naming convention

Process names use UpperCamelCase. This both signals intent and disambiguates process references from computation event references at parse time:

• Reply(pkt) — sub-process call (UpperCamelCase, parentheses required).
• send_frame.pkt — computation-event reference (snake_case, dot carrier syntax).

The disambiguation happens on the leading character of the identifier. The boot process is the one bound with @bind(microkit.init); Init is a conventional name but carries no special meaning (see Boot Initialisation).

Annotations (@bind)

A process may carry a single @bind(...) annotation mapping it to one or more platform entry points, without hardcoding kernel terminology into process names. Group the targets — one platform.entry pair per platform — on one line:

@bind(microkit.notified, cheri.interrupt_handler)
proc Notified() { o2d?pkt -> d2i!pkt -> Notified(); }

• A process with no @bind is internal — not directly callable by the kernel.
• @bind is authoritative for entry-point selection. The C backend and the UPPAAL lowering pick kernel entry points by binding, not by process name: the microkit.init-bound process becomes init() (the boot body) and the microkit.notified-bound process becomes the notified() event loop.
• Both a @bind(microkit.init) and a @bind(microkit.notified) process are mandatory for every PD with a program when targeting Microkit (--emit=c or image generation) — Microkit invokes both on every PD. See Boot Initialisation. --emit=xta (verification only) does not require them. Other platform entry points are optional.
• Each entry point binds at most one process. Two processes both @bind(microkit.notified) is an error — resolution rejects the second rather than silently keeping the first.

The target platform is chosen with --platform (e.g. --platform=microkit); omit it to compile whatever the annotations bind. A platform fic does not support is rejected.

Resolving bindings to a platform’s concrete kernel symbols — and rejecting unknown or conflicting targets across platforms — remains the project layer’s job (fire, configured in fire.toml); see #190.

Operator precedence

From loosest to tightest:

Concrete consequences:

e -> P() [] e2 -> Q()            ≡ Choice([Prefix(e, P()), Prefix(e2, Q())])
e -> P() ; Q()                   ≡ (e -> P()) ; Q()
[b] e -> P() [] e2 -> Q()        ≡ Choice([Guard(b, Prefix(e, P())), Prefix(e2, Q())])
p1() ; p2() [] p3()              ≡ p1() ; (p2() [] p3())
[b] (e -> P() [] e2 -> Q())      ≡ Guard(b, Choice(...))   // outer-guard the choice

Parenthesisation cuts through: (...) re-enters at the top of the precedence chain.

Choice and discriminators

Every branch of a [] choice must carry a discriminator — a distinguishing prefix that the surrounding environment can pattern-match on. The parser checks structurally and recurses into a branch’s first sequential item and into nested choices; deferred resolution is required only for ProcessRef (the validator follows the name).

Common discriminator shapes:

e -> P()                // event prefix
[b] P()                 // guard
c?x -> ...              // channel-event prefix

The optional default arm is taken when no branch’s guard succeeds.

Examples

// Two branches, no default.
proc Dispatch() {
    [rx] receive -> Skip [] [!rx] cleanup -> Skip;
}

// Two branches with a fallback.
proc Reply(pkt: int) {
    [pass]  o2d!pkt -> Skip
 [] [!pass] handle_ping -> Skip
    default Skip;
}

Guards

Guard ::= ident | '!' ident

A guard gates the next process expression on a boolean variable. Today the parser accepts only [var] (variable read) and [!var] (negation); the variable must be a global declared in the same .fi file. The guard binds tighter than []:

[b] e -> P [] e2 -> Q   ≡   ([b] (e -> P)) [] (e2 -> Q)

The guard applies only to the first branch.

🚧 Full boolean / relational guard expressions ([x == 3], [x && y], etc.) land with the expression grammar — see #105. Until then, decompose with intermediate globals if a guard needs richer logic.

Sequential composition

Inside a {} body, ; separates items. The last item may carry a trailing ; before }:

proc Notified() {
    irq?159 -> Handle_eth();
    irq!159 -> Notified();
}

Sub-process calls

ProcessRef ::= UIdent '(' (ident (',' ident)*)? ')'

A sub-process call references another process declared in the same file. The argument list is currently restricted to identifiers. Parentheses are always required — even for empty argument lists (Skip and Div are the only bare uppercase atoms):

proc Notified()   { irq?159 -> Handle_eth(); irq!159 -> Notified(); }
proc Handle_eth() { handle_irq -> Dispatch(); }
proc Dispatch()   { [rx] receive -> Skip [] [!rx] cleanup -> Skip; }
proc Reply(pkt: int) { o2d!pkt -> Skip; }

The validator confirms each ProcessRef resolves to a declared process and that the argument count matches.

Empty processes

Skip and Div are atomic and self-contained: Skip is successful termination, Div is divergence (a self-loop):

proc NoOp()  { Skip; }
proc Stuck() { Div; }

Limitations

• Argument lists for ProcessRef and computation-event references are restricted to identifiers. Channel-receive RHS accepts identifiers or integer literals (so irq?159 parses).
• Guards accept [var] / [!var] only.
• Currently only variable declarations (x: int;) are permitted as inline body items alongside process expressions. Assignment statements and external calls must live in evt declarations. This restriction is planned to be lifted: future versions will allow statements directly in proc bodies, with flexible interleaving of statements and process expressions.
• Recursion is modeled as a sub-process call by name.