Data Layer: Structs and Constants

StructDecl ::= 'struct' UIdent '{' Field* '}'
Field      ::= ident ':' Type ';'
Type       ::= ScalarType | Type '[' ArrayLen ']'
ArrayLen   ::= integer-literal | CONST_NAME
ConstDecl  ::= 'const' UPPER_IDENT ':' Type '=' Expr ';'

The data layer is the system-wide vocabulary of payload struct types and layout constants. It is shared by every protection domain — and, through generated type headers, by the external low-level implementations (C, Rust, Pancake) too, so the model and the code agree on one definition. It lives as flat, top-level items in the .fis file: like the rest of the system description, declarations are visible to every .fi program with no import ceremony.

const PACKET_BUFFER_SIZE: int = 2 * 1024;

struct Packet {
    length:  uint16;                    // valid bytes in payload (≤ capacity)
    payload: byte[PACKET_BUFFER_SIZE];  // fixed-capacity buffer
}

const RING_BYTES: int = 64 * sizeof(Packet);

Structs

• Names use UpperCamelCase by convention.
• Fields are flat — primitives, other declared structs, or fixed-size arrays of those; no pointers.
• Fixed-size arrays T[N]: the length N is an integer literal or a declared integer const (e.g. byte[PACKET_BUFFER_SIZE]), so the size stays statically known: sizeof(T[N]) = N * sizeof(T).
• No recursion: a struct may not contain itself, directly or indirectly. This guarantees sizeof is computable at compile time by recursive field traversal.
• Fields must have fixed-width types (uint32, not int; arrays of fixed-width elements) so the layout is well-defined.
• Struct names are usable wherever a type is expected — variable declarations, typed channel buffers (via buf<Packet>), and sizeof.

Constants

• Names use SCREAMING_SNAKE_CASE by convention; a declared type is required.
• The right-hand side is a full expression, folded at compile time (rustc-style, before any lowering). The const subset covers: literals, references to previously declared constants, sizeof(T), and unary/binary arithmetic, bitwise, shift, comparison, and logical operators.
• Function calls, runtime variables, and field access are rejected in const position. Forward references between constants are errors — declare in dependency order.
• The folded value must match the declared type (bool constants take boolean values; integer-family types take integers).

Program-local structs

A .fi program may declare structs of its own, with the same grammar and rules as system structs. These are PD-internal types — device-ring descriptors, driver bookkeeping — that never cross a channel:

// eth_outer.fi
struct Rbd {
    data_length: uint16;
    flags:       uint16;
    addr:        uint32;
}

ring: Rbd;

Scoping:

• A local struct is visible only within its own program — other PDs and the .fis cannot reference it. Channel buffer payload types must be system structs: system structs are the project’s communication types (what may cross a channel), local structs are program types (PD-internal state) — the two tiers of the data model.
• A local struct may contain system structs in its fields; the reverse is impossible.
• A local struct may not reuse the name of a system struct (shadowing is an error), so every type name means one thing across the project.
• Array lengths in local fields may reference system constants.

The C backend emits system structs and constants into a shared header named after the .fis file — <project>_types.h (e.g. datadiode_types.h) — and each PD’s local structs into a per-PD header, <pd>_types.h (e.g. eth_outer_types.h), included by the PD’s generated unit and importable by that PD’s hand-written driver code. A PD may not share the project’s name if it declares local structs (the two headers would collide).

Global state

The data layer declares types and constants, not mutable state. In CoreFi, shared global state is exactly the channel-buffer view: mutable data lives in declared memory regions, mapped explicitly into the PDs that may touch it and labelled for information flow. A shared scalar is a typed slot of a declared region — never an ambient global.