Process Blocks

ProcessSection ::= 'Process' ':' ProcessDecl+

ProcessDecl    ::= ident '(' (Param (',' Param)*)? ')' '=' ProcessBody ';'
Param          ::= ident ':' Type

ProcessBody    ::= ProcessExpr (';' ProcessExpr)*
ProcessExpr    ::= 'Skip'
                |  'Div'
                |  Event '->' ProcessExpr
                |  '[' Guard ']' ProcessExpr
                |  ProcessExpr ('[]' ProcessExpr)+ ('default' ProcessExpr)?
                |  ProcessRef
                |  '(' ProcessBody ')'
ProcessRef     ::= ident ('(' (ident (',' ident)*)? ')')?
Guard          ::= ident | '!' ident

A process block is the orchestration layer of a Fiducia protection domain — a CSP-style algebraic expression composed from events, guards, choices, and sequential composition. Each Process: section declares one or more named processes; multiple sections in the same .fi merge into a single process list.

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

Naming convention

Process names start with an UpperCamelCase first letter — this both signals intent and lets the parser detect the start of a new declaration while consuming a body. The convention also disambiguates:

• Reply(pkt) — sub-process call (UpperCamelCase, parses as a process expression).
• send_frame(pkt) — computation-event reference (snake_case, parses as an event).

The disambiguation happens at parse time on the leading character of the identifier; do not lowercase a process name or capitalise an event name.

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. default and otherwise are both currently accepted as the keyword for the default branch; default is the canonical form (paper choice).

Examples

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

// Two branches with a fallback.
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 (process bodies cannot declare their own state). The guard binds tighter than [] — [b] e -> P [] e2 -> Q guards the first branch only.

🚧 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 body is not a list of declarations — it is a single process expression with ;-composed sub-expressions:

Notified() = irq?159 -> Handle_eth() ; irq!159 -> Notified();

The trailing ; after Notified() is the declaration terminator, not the sequential operator. Inside the body, ; separates expressions.

Sub-process calls

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

A sub-process call references another process declared in the same section. The argument list is currently restricted to identifiers (the expression grammar will widen this). Argument-less calls may also drop the parentheses entirely:

Process:
    Notified() = irq?159 -> Handle_eth() ; irq!159 -> Notified();
    Handle_eth() = handle_irq -> Dispatch ;        // empty arg list, no parens
    Dispatch() = [rx] receive -> Skip [] [!rx] cleanup -> Skip ;
    Reply(pkt: int) = o2d!pkt -> Skip ;

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

Empty processes

Skip and Div are atomic and self-contained: Skip is successful termination, Div is non-termination (Ω). Both stand alone as a body:

Process:
    NoOp() = Skip;
    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.
• No variable declarations inside a process body — promote to a global.
• Recursion is modeled as a sub-process call by name, e.g. the trailing Notified() in Notified() = ... -> Notified();.