ADR 0029 — M14: exported structs that hold C state

Inherited from Nova. This is Nova's ADR 0029, which CeeSafe inherited at the fork (Nova v0.6.0; CeeSafe's Decision 0006). Its text is Nova's record and is not changed: read Nova and novac as the language and compiler CeeSafe forked from, .nova as .cee, and Nova's C names as CeeSafe's (spec/c-backend.md). Links to documents CeeSafe did not fork go to Nova's repository.

• Status: Accepted (project owner, 2026-10-30), both questions as recommended (§5): option A, with arrays in this ADR. The wording is the agent's.
• Scope: a struct defined in Nova and used by C by value, whose fields include C state (a spinlock_t) and fixed arrays. CosmoOS's roadmap 2.0 SA2 needs it for the handle table; the owner chose Nova-owned types for SA2 (2026-10-30), and SA3 and later conversions need it for every C struct that embeds a lock.

1. Context

1.1 The handle table

• The C. struct handle_table (CosmoOS kernel/include/kernel/handle.h:86) is a spinlock_t, an array of 64 struct handle_entry { struct kobject *obj; unsigned rights; unsigned flags; }, two counts and a bool. handle.c (266 lines) is its only code apart from three writes of limit in process.c (:965, :1211, :2415).
• C makes the values. The table is embedded by value in struct process (process.h:180), and self-tests put it in statics and on the stack (epolltest.c:112, :447, :530, :627, :660; memtest.c:994). It is initialised in place by handle_table_init(t) and torn down by handle_table_destroy(t). Nova code would only ever see it through a *mut handle_table from C.
• SA2 so far. The kobject layer is Nova over C's struct kobject (CosmoOS #493): an imported struct, which works today. The owner's choice for SA2 was that the types themselves become Nova's, so the definition struct handle_table { … } must come from Nova's generated header, not from handle.h.

1.2 What Nova allows today

• @repr(C) structs (type-system §28.5) cross to C and are defined in nova_exports.h, but their fields may only be integers, bool, raw pointers and other @repr(C) structs. A spinlock_t field is N0291 (checked with novac 0.4.0, 2026-10-30: "a @repr(C) struct cannot hold a 'spinlock_t'"), and so is an array field (§28.3: arrays do not cross).
• C state by value (§33, C7b) is allowed in a Nova struct, which then becomes C-laid-out (§33.1): the C compiler lays it out, it is never moved (§33.2), and it is made only by Box.create with a @placed initialiser (§33.3). Such a struct is struct nvT_S in main.c only: C code cannot name it.
• Arrays in imported structs are allowed (ADR 0014, §31): f: [E; N] is seen as Nova's array struct over the C member, with no copy.

So each half exists: C-laid-out structs inside Nova, and C-visible structs without C state. Nothing joins them.

2. Options

	A. @repr(C) may hold C state and arrays	B. A new @cstruct kind	C. Keep the type C's
Language	lift two N0291 cases of §28.5; §33's rules apply as they stand	a third struct kind with its own rules	none
Who defines struct handle_table	Nova (nova_exports.h)	Nova	C (handle.h), imported by Nova
SA2's "Nova-owned types"	yes	yes	no: the code is Nova, the type C's
New rules to learn	none: a @repr(C) struct with C state is C-laid-out, as any struct with C state is	a kind that is both	none
Later conversions (SA3: struct mutex, wait queues, struct process)	the same rule	the same	each type stays C's

3. Decision: A

3.1 Fields

A @repr(C) struct's fields may also be:

• an imported C type by value (§31), such as spinlock_t. The struct is then C-laid-out (§33.1);
• an array [E; N] whose element is an integer, bool, a raw pointer as in §28.3, a @repr(C) struct, or an imported type. Inside Nova the field is Nova's array; in C it is the member CE f[N].

Every other N0291 case stays: references, slices, boxes, vectors, optionals, results, non-@repr structs and enums, and @repr enums as fields. None of the allowed field types needs drop; in addition, a @repr(C) struct with C state may not declare a drop method (N0291, new): C makes, embeds and discards these values without calling Nova, so a drop would silently not run.

3.2 A @repr(C) struct with C state

It is C-laid-out (§33.1), with every rule of §33 unchanged:

• it is never moved, copied or assigned in Nova (N0294), and crosses to C only behind a pointer (*T, *mut T; §28.3's by-value crossing is for @repr(C) structs without C state);
• Nova makes one only through Box.create with its @placed initialiser (§33.2–§33.3), or in a static (§39.4);
• C makes one wherever C makes a struct (embedded, static, on the stack). Nova code that receives a pointer to one from C relies on C having initialised it, as with any pointer from C: the exported function that takes it says so in its /// Safety: comment (§27.4).

3.3 C

• nova_exports.h defines the struct as struct S { … } with members named as in Nova, after the @header includes that declare its imported member types (it includes them already, c-backend §2.3), and after the @repr(C) structs it contains. There is no layout assertion, as for every C-laid-out type: the C compiler lays it out, and layoutOf<T>() gives C's sizeof/_Alignof (ADR 0027).
• Array members are CE f[N]; with N written as a number. A C header that also names the length (CosmoOS's HANDLE_TABLE_SIZE) checks it with a _Static_assert beside its #include. In main.c a field place is the member seen as Nova's array struct, (*(nvA<N>_<E> *)(uintptr_t)&p->f), as for ADR 0014's imported arrays, after an assertion that the member and the array struct have one size and alignment (the member's type needs no _Generic check: main.c defines it).
• main.c uses struct S for it, as for every @repr(C) struct, so both translation units name one type (C11 6.2.7).

3.4 The interpreter

C-laid-out types are already outside the interpreter (§33.4), and a @repr(C) struct with C state is one of them. Arrays of @repr(C) elements in a @repr(C) struct without C state run in the interpreter as Nova arrays.

3.5 For the handle table (CosmoOS, after a release)

@header("kernel/spinlock.h", "kernel/object.h")
extern "C" {
    @ctype("spinlock_t")
    struct spinlock_t;
    struct kobject;
}

const HANDLE_TABLE_SIZE: usize = 64;

@repr(C)
struct handle_entry {
    obj: *mut kobject; // null: free
    rights: u32;
    flags: u32;
}

@repr(C)
struct handle_table {
    lock: spinlock_t;
    entries: [handle_entry; 64];
    count: u32;
    limit: u32;
    exiting: bool;
}

/// Safety: `t` points to storage for a table that nothing uses yet.
@export("handle_table_init")
fn tableInit(t: *mut handle_table) { … }

make nova writes the generated header (kernel/include/kernel/handle_types.h, say), and handle.h includes it in place of its own definitions, with _Static_assert(HANDLE_TABLE_SIZE == 64). process.c and the self-tests are unchanged: unsigned and uint32_t are the same type on both of CosmoOS's targets, and the C sees the same members. The entries hold *mut kobject and count their references by hand, in unsafe code, as the C does: a KRef<kobject> field would need drop glue, which C-made values never run (§3.1).

4. Consequences

• SA2's handle table, and later SA3's locks and wait queues and struct process itself, can be Nova's types without changing how C embeds them.
• C code may write a Nova-owned struct's fields (process.c writes limit). Such a struct is plain data with C state: Nova keeps no invariant in it that C could break without unsafe on the Nova side noticing, which is already the rule for anything behind a pointer from C (unsafe.md U2).
• No layout is checked for these structs in Nova; the C compiler is the authority, as for every C-laid-out type. The member types are checked in both translation units by the shared definition.
• Tests.
  • The run corpus gets a C file that embeds a C-state @repr(C) struct by value in a C struct, initialises it through an export, and uses its array.
  • Compile-fail tests cover a move of one (N0294), a by-value parameter (N0294), a drop method on one (N0291), and an array of a non-FFI type (N0291).
  • k3.py compiles CosmoOS's header against the generated one.
• Release. It needs a novac release (0.5.0) and a CosmoOS pin move before SA2's third PR.

5. Questions for the owner

1. Which option? A (recommended), B or C (§2).
2. Arrays in the same ADR? Recommended: yes, since the handle table needs both. The alternative is a separate ADR for array fields of @repr(C) structs.

6. Implementation (2026-10-30)

• Checker (TypeChecker.IsFfiSafe, the @repr(C) field loop): a field may be an imported type or an array of an allowed element; a drop on a C-laid-out @repr(C) struct is N0291.
• C (CEmitter): a @repr(C) struct's array field is the C array member in main.c and nova_exports.h, with an assertion that it has the layout of Nova's array struct; places use it through the cast that ADR 0014's imported arrays use (IsCArrayMember); a struct literal assigns its arrays after the compound literal (EmitConstruction); a static's initialiser writes them as plain braces (CArrayInitializer). The header names an imported member by its C spelling and defines no imported struct.
• Tests.
  • ffi/exported-c-state.nova with .c and .types.h, under every C configuration: C embeds xs_table (a lock, a self-pointing list head, an array of @repr(C) entries) in its own struct, a static and a stack frame, writes a field, and uses it through Nova's exports. Grid, a plain @repr(C) struct with nested arrays, is a value and a static in Nova. The reviewed header is ffi/exported-c-state.h.
  • check-fail/c-state-types.nova: a drop (N0291) and a by-value parameter (N0294). check-fail/ffi-declarations.nova: array fields are allowed, and arrays of a non-@repr struct or a @repr enum are N0291.