Milestone 14 — Nova for a kernel written in Nova (plan)

Status: in progress (started 2026-10-29 at the owner's word). K1, K2a and K3 are done and accepted (booted in CosmoOS), K4 decided, K5's inline atomics and K7's generator work done (novac 0.3.1). Open: K2's separate compilation, which waits for converted subsystems' build times; K5's check eliminations, which wait for PF1; K6, the outside audit, which the owner engages. Each item that changes the language or the toolchain gets a design and an ADR for the owner before code, as in M11 and M13.

Why

CosmoOS's roadmap 2.0 (proposed, CosmoOS docs/roadmap-2.0.md, merged as #483) makes "the kernel in Nova" its goal. All new kernel code would be Nova, all existing C would be converted, and only a named floor of assembly and C wrappers would remain. Its SA track assumes Nova can write whole subsystems: allocation and object lifetimes (SA2), locks, waits and quiescence (SA3), drivers (SA4), then the network stack, storage and the core. Today's four ports (gpt, cputime, nice, fair; 982 lines) are leaf functions whose state lives in C. Reviewing the roadmap against the compiler (below) found what Nova still lacks for the rest. This milestone is that list, ordered by what the roadmap needs first.

The roadmap names these Nova gates (its "Nova prerequisites" section, proposed with this plan):

CosmoOS milestone	Needs from Nova
SA1 (gate, build from Nova)	K4 decided (how a self-hosted CosmoOS builds its kernel), K2a (C split into translation units)
SA2 (allocation, objects), SA3 (locks, waits)	K1 (global and per-CPU state), K3 (the kernel library)
SA6 onward (whole subsystems)	K2 (Nova-to-Nova across compilation units, or a measured whole-program build), K6 (an outside audit)
PF1, PF2 (performance)	K5 as measured
SA5 (parsers)	nothing new: parsers are leaf code, as GPT was

Plan

#	Gap	Probe (2026-10-29, a032dc6)	Needs	Status
K1	Global state: a kernel has lock-protected tables, singletons and per-CPU data; Nova has only compile-time const (type-system §10)	static var count: u64 = 0; and var count: u64 = 0; at top level: N0101 "expected 'fn', 'const', 'struct' or 'enum'"	ADR (OD-28)	done (2026-10-29, ADR 0024, type-system §39): static, static mut, @constant, C constant macros. Accepted: CosmoOS's nova-kcore keeps a table under a static spin lock and a per-CPU counter in every debug boot (CosmoOS #489, #490); the negative cases are check-fail kernel-static-writes.nova, kernel-percpu.nova, kernel-percpu-guard.nova and kernel-library.nova
K2	Nova-to-Nova calls with Nova's types across compilation units. Today each kernel .nova file compiles alone and they meet only through @export C functions, so references, regions, effects and Send/Share stop at every file boundary. ADR 0013 D4 keeps builds whole-program, with separate compilation deferred until build times were measured	Measured below: a whole-program build of 202,000 lines is 13.1 s in novac and 33.8 s in clang for one 1,076,000-line C file, on every change	ADR (OD-29); K2a first	K2a done (2026-10-29, ADR 0022): --split builds it in 14.0 s on 10 cores, 2.4 s after a one-file change; separate compilation open
K3	A kernel library: KernelHeap (C5), KRef<T>, SpinLock<T>, IrqSpinLock<T>, Mutex<T> and Quiesce (C7) exist as demonstrations in integrations/cosmoos/c5 and c7, not as a package a kernel depends on; ObjectCache<T>, which roadmap 2.0 lists as built, does not exist	grep -r ObjectCache in Nova's repository: no match	ADR (OD-30): where it lives and who owns it	in Nova (2026-10-29, ADR 0025): lib/kernel, checked against CosmoOS's headers by k3.py; ObjectCache<T> and a static Mutex since ADR 0027. Done and accepted (2026-10-29): CosmoOS's self-test nova-kcore passes in debug boots on both architectures (CosmoOS #489; #490 with novac 0.3.1 adds the static mutex, checked against mutex_init, and the object cache)
K4	novac where CosmoOS builds itself: roadmap 2.0's rule 7 stops committing generated C, so every kernel build runs novac, a .NET NativeAOT binary for macOS, Linux and Windows that does not run on CosmoOS (SW0, self-hosting)	—	a decision (OD-31), recorded in both roadmaps	decided (ADR 0023, 2026-10-29): source releases carry the generated C; CosmoOS's make dist is its side
K5	Kernel hot paths within roadmap 2.0's 5%: inline atomics (OD-27; ADR 0021 measured a further 1.8×), and the check elimination that converted code needs	per workload, with PF1's benchmarks	OD-27's ADR; others as measured	inline atomics done (2026-10-29, ADR 0026): static inline in rt.h, the atomic types in lib/core for kernel code; the ordered ring within 1.24–1.34× of inline C (was 2.3–2.8×); check eliminations wait for PF1
K6	An outside audit of the checker before the compiler carries whole subsystems	safety-audit.md §4: the 2026-10-29 review, by the same model that wrote the compiler, found two holes, one in a release (0.1.1)	the owner engages a reviewer; Nova provides the pack	proposed
K7	The compiler as part of a kernel's trusted base: kernel-style code in the random program generator (statics, guards, the freestanding profile), and a pin-bump checklist (the nightly campaign green, the corpus under the interpreter)	—	none (tests)	started (2026-10-29): the generator writes statics (testing.md §5), which found an unused static's library type left out of the C (fixed, run-pass/statics-unused.nova); the checklist is in release.md; since 2026-10-29 kernel-style programs built freestanding and checked against their hosted twin (--freestanding, testing.md §5), in the nightly campaign. Guards need CosmoOS's C, so k3.py covers them

Measurements for K2 (run 2026-10-29, Mac M-series, Apple clang 21, novac 0.2.0-dev Release)

A synthetic program of structs and functions with loops, vectors, matches and ?: 400 structs and 2,000 functions make 46,404 lines. Four renamed copies, with a main that calls every function so the C compiler cannot drop them, make 202,004 lines. Indicative only: real kernel code has more generics and fewer, larger functions (inferred).

Nova lines	novac check	novac build --emit c	generated C	clang -O2 -c of it
46,404	1.79 s, 152 MB	4.25 s, 213 MB	220,934 lines	—
185,604 (functions unreachable)	4.79 s, 409 MB	11.65 s, 607 MB	883,334 lines	— (clang dropped the unused functions)
202,004 (all reachable)	—	13.10 s, 721 MB	1,076,433 lines	33.84 s, 1.25 GB, one core

novac scales about linearly. The cost is the rebuild: every change recompiles everything, and the C is one translation unit that a parallel build cannot spread over cores. CosmoOS's C kernel compiles each file in parallel.

K1: global and per-CPU state (design sketch for the ADR)

• static NAME: T = e; at package level, with e a constant expression or a constant constructor of T. A static is never written directly. Its mutable state is reached only through a type that is Share (§38.1): a spin lock or mutex guard type, an atomic, or a library type declared @threadSafe. That makes static the global counterpart of Arc<T>, needing no new borrow rule: borrow STATIC is a borrow T with the static region.
• Constant construction. A kernel lock is C state that may point to itself once initialised (R-11). It needs an initialiser that C can evaluate statically (CosmoOS's SPINLOCK_INIT(name)), so the ADR must say how an imported C type's static initialiser is named (@cinit("SPINLOCK_INIT"), or a constant constructor in the binding).
• Per-CPU data. @percpu static NAME: T, accessed only where the CPU cannot change: in @context(atomic) or under a guard that disables preemption. The effect checker already proves contexts (§32), so this is a new obligation on a checked fact, not a new analysis.
• Interrupts. Data shared with an interrupt handler needs an irq-saving lock. That is a property of the lock type (C7's IrqSpinLock<T>), so the static needs nothing of its own.
• Hosted programs get the same static for Mutex<T> and atomics (lib/std): a Mutex initialised statically (PTHREAD_MUTEX_INITIALIZER, SRWLOCK_INIT).
• C. A static is a C object with internal linkage, or external with @export, and its initialiser is a C constant expression. No constructor runs at startup.

K2: typed calls across compilation units (options for the ADR)

1. K2a, cheap and first: the C in several translation units. novac stays whole-program but emits one .c per source file, or per N functions, plus a shared header. The C compiles in parallel and only changed files recompile. novac's own time stays about 13 s at 200,000 lines.
2. Separate compilation per package. Each package is checked against its dependencies' interface files: their public signatures with regions, effects, Send/Share and @effectsOf, and the bodies of their generic code, because generics are monomorphised (ADR 0013's stated precondition). A kernel would be a few dozen packages, so a change rebuilds one package and those whose interface it changes.
3. Stay whole-program, accepting K2a's numbers.

The recommendation will come from measuring K2a on the converted subsystems first. Option 2 is a large change, and it is the one that makes a ~200,000-line kernel practical to develop. In both cases, calls between Nova packages keep Nova's types, which @export-only boundaries do not.

K3: the kernel library

C5 and C7 built most of the kernel abstractions roadmap 2.0's rule 4 names: KernelHeap (c5/kernel.nova), KRef<T> (c7/kobject.nova), SpinLock<T>, IrqSpinLock<T> and Mutex<T> with their guards (c7/sync.nova), and Quiesce (c7/quiesce.nova). They live as demonstrations with their own C glue. ObjectCache<T>, a typed slab cache over CosmoOS's kmem_cache, is not built: the roadmap's list is ahead of the code there, and K3 writes it. The ADR decides:

• Where they live. The proposal is a Nova package in CosmoOS's tree (kernel/nova-core/, a nova.toml package the kernel's Nova packages depend on by path). The abstractions bind CosmoOS's own C API, so CosmoOS owns them. Nova keeps the language features they need and the tests that pin them (integrations/cosmoos/c7).
• Its API, written once in Nova with /// Safety: contracts at the floor.
• Its tests, the C5 and C7 self-tests and stress tests, moved with it.

K4: novac and a self-hosted CosmoOS

roadmap 2.0's rule 7 (generated C not committed) and SW0 (CosmoOS builds itself) conflict, because novac does not run on CosmoOS. Options:

1. Ship the generated C in source releases. The repository holds only .nova; a release tarball, or a make dist tree, holds the generated C. A build from the tarball needs no novac, so a self-hosted build works, but changing a .nova file needs a host with novac. Recommended.
2. novac on CosmoOS. NativeAOT has no CosmoOS target, and porting the .NET runtime is far larger than this milestone.
3. A Nova compiler written in Nova. A long-term direction, not a 2.0 one.

K5–K7

• K5 starts with OD-27 (inline atomics: atomics as built-in operations emitted as __atomic_*), whose ADR is the first item. Then PF1's numbers on converted code decide which check eliminations to add, each with optimisations.md's written preconditions.
• K6 is outside Nova's repository to perform. Nova keeps safety-audit.md current and turns each finding into a test.
• K7 adds generator features as the language gains them (K1's statics first). The pin-bump checklist goes in docs/release.md and CosmoOS's docs/build/nova.md.

Order and release

K4's decision and K2a come first, because SA1 needs them. Then K1 and K3, which gate SA2 and SA3; then K2's ADR, informed by K2a; K5, K6 and K7 run alongside. K1 and K2a change the language and the compiler's output, so they ship in Nova 0.2.0, with the work since 0.1.2 (M13, ADR 0018–0021), and CosmoOS moves its pin to it in one PR. 0.2.0 was released on 2026-10-29 with K1, K2a and K3. 0.3.0, the same day, adds K5's inline atomics, ADR 0027 and K7's freestanding programs. Point releases stay for fixes (release.md).

Acceptance (proposed)

• K1: a CosmoOS kernel object table written in Nova with a static spin-lock-guarded table and a per-CPU counter; negative tests for a static written outside a guard, a per-CPU access that may migrate, and a sleep under a static's spin lock.
• K2a: novac build --emit c of a multi-file package writes one translation unit per file, byte-identical between runs; a one-file change recompiles one .c.
• K3: the kernel library builds in CosmoOS's tree, and its self-tests pass in a debug boot on both architectures.
• K4: the decision recorded in both roadmaps; for option 1, a source release built without novac.
• K5, K6, K7: as their items say, each with a dated result.