Milestone 13 — The documented gaps (plan and report)

Status: complete (2026-10-28). G1–G6 and their follow-ups are done; the acceptance is the last section. The owner asked, on 2026-10-28, for Nova's remaining known gaps to be taken up while CosmoOS's CI is slow.

Why

The README and the earlier milestone reports name what Nova still lacks:

• no userland threads and no data-race guarantee for them;
• no dynamic dispatch (dyn, OD-10);
• no owning, escaping closures (OD-9b);
• no package registry or version solver: path and git dependencies only (ADR 0013);
• vector and string growth 2–3.5× slower than C (milestone-9.md 9f);
• a borrow checker that rejects some valid programs whose lifetimes cross functions.

Each gap below was reproduced against the compiler at b9fa451 (2026-10-28) before any change. The probe is quoted.

Plan

#	Gap	Probe at b9fa451	Spec	Status
G1	Vector and string growth: allocate, copy, free on every growth; an out-of-line call on every push and append; the vector's address escapes into that call, so its length lives in memory	vector-growth 1.79× C, string-building 2.72×, parsing 1.31×; peak heap 384 MiB against C's 256 (Mac, below)	c-backend.md §2 (vectors), §6 (nova_realloc)	done; measured on the Mac and the Ryzen box
G2	Dynamic dispatch: dyn Interface behind a pointer (Box<dyn Shape>, borrow dyn Shape)	expected '>', found identifier (N0100) at Box<dyn Shape>	ADR 0015 accepted 2026-10-28; type-system §21, §37	done (G2a, G2b)
G3	Owning closures: returnable and storable, owning their captures (OD-9b; ADR 0012 deferred it to come with dyn)	expected the plain function type 'fn(u64) -> u64', but this closure captures 'n', so it is a 'borrow fn' (N0299)	ADR 0015 §3.6; type-system §36.5	done
G4	Userland threads with a data-race guarantee: spawn and join, values that may cross threads, shared state only through locks or atomics	cannot find 'Thread' in this scope (N0200)	ADR 0016 accepted 2026-10-28; type-system §38	done (G4a–G4d)
G5	Checker generality: valid programs the borrow checker rejects	— (a corpus to collect first)	lifetimes.md §8, type-system §16.5, §36.2	done
G6	A package registry and a version solver	— (ADR 0013 chose path and git only, as the owner asked)	ADR 0017 accepted 2026-10-28; tooling.md §4.6–§4.8	done; index at github.com/vkuttyp/nova-index

The order is G1 (no language change), then G2–G4, which build on each other, then G5 and G6. G2, G4 and G6 change the language or the toolchain beyond their accepted designs: each gets a design and an ADR for the owner before code, as G7 and G8 did in M11.

G1: vector and string growth (done, 2026-10-28)

Three changes, none to the language:

1. Growth by realloc. nova_vec_grow allocates a first buffer and resizes a later one with the new nova_realloc (runtime/core/nova_rt_core.c), over the new platform hook nova_platform_realloc (runtime/hosted/nova_rt_hosted.c: realloc). A reallocation is one counted attempt, so the fault-injection sweep sees the same attempts as before, and on failure the old block is unchanged and still live. The old and new buffers no longer coexist, so the peak heap is C's.
2. A fast path. The generated push and append (CEmitter.EmitVectorHelpers) call nova_vec_grow only when the buffer is full, and append copies with nova_mem_copy instead of a byte loop.
3. No escaping address. They pass the capacity through a local, not &v->cap. Before, the vector's address escaped into the out-of-line call, so clang kept its length in memory and stored and reloaded it on every push.

The interpreter's VectorGrow (Interpreter/Runtime.cs) needs no change: it already counts one attempt per growth and leaves the vector unchanged on failure.

Measurements (run 2026-10-28, Mac M-series, Apple clang 21, benchmarks/suite/run.py --runs 5 --langs nova,c)

Workload	Before: Nova / C ms (ratio)	After: Nova / C ms (ratio)	Peak heap before → after (C)
vector-growth	630.0 / 351.7 (1.79)	370.1 / 390.0 (0.95)	384.0 → 256.0 MiB (256.0)
string-building	595.0 / 219.1 (2.72)	410.6 / 218.4 (1.88)	12.0 → 8.0 MiB (8.0)
parsing	181.8 / 138.9 (1.31)	156.0 / 138.7 (1.12)	48.0 → 32.1 MiB (32.0)

The C times vary between runs on this shared Mac (321.6 to 390.0 ms for vector-growth).

Measurements of record (run 2026-10-28, the Ryzen box, docs/benchmarks.md)

The trees at b9fa451 (before) and 587e38f (after) were each built and run with benchmarks/suite/run.py --runs 5 --langs nova,c three times, before and after interleaved, under nice, with a load average of about 2 (a shared server). The time is the median of the three repetitions' medians (ms), Nova / C:

Workload	clang 18 before	clang 18 after	gcc 12 before	gcc 12 after	Peak heap before → after (C)
vector-growth	1150 / 553 (2.08)	603 / 584 (1.03)	1174 / 580 (2.02)	570 / 577 (0.99)	384.0 → 256.0 MiB (256.0)
string-building	841 / 348 (2.42)	555 / 346 (1.61)	1094 / 310 (3.53)	817 / 309 (2.64)	12.0 → 8.0 MiB (8.0)
parsing	203 / 137 (1.49)	172 / 138 (1.25)	263 / 182 (1.45)	206 / 191 (1.07)	48.0 → 32.0 MiB (32.0)

Allocation counts are unchanged (vector-growth 241, string-building 661, parsing 25 under both). Raw results: /root/nova-ci/m13/out on that machine. The other thirteen workloads were not rerun: the change touches only vector, string and slot-map growth.

Steps, measured on the generated C (2026-10-28): the realloc and fast path alone moved vector-growth from 630 to 662 ms (within noise) and parsing to 151 ms. The local capacity moved vector-growth to 370 ms. In vector-growth, the overflow check on the final summing loop costs about 5% (0.63 against 0.60 s, the loop with and without nv_add_u64). That check is Nova's semantics (OD-6), not overhead to remove.

What is left in string-building

The workload appends digitText[d..d + 1]. Each append checks the index and both ends of the slice for a UTF-8 boundary: two loads from the text and their compares per byte, where C stores a byte. Two ways to close it, neither done:

• An optimisation: a slice of a constant string whose bytes are all ASCII needs no boundary check. That is a check elimination (optimisations.md), with the same equivalence tests as BCE.
• A library member: a way to append one ASCII byte ('0' + d) without a view, which the spec does not have (type-system §23.2: text enters a string only through append of a StringView or appendNumber).

Since done (2026-10-28, after M13): the optimisation (optimisations.md §2.9: no boundary check on a slice of an ASCII literal), and a cause the analysis above missed, gcc calling memcpy for every one-byte append, which the append helper now copies with a byte loop up to 16 bytes (c-backend §2). On the Ryzen box string-building went from 548.7 to 436.8 ms under clang (1.58× to 1.26× C) and from 809.7 to 434.9 ms under gcc (2.58× to 1.40×); parsing and vector-growth did not move. The library member was not needed.

G2: dynamic dispatch (done, 2026-10-28; ADR 0015)

Spec: type-system.md §37 (and §21.1, effect lists on interface methods), grammar.md, c-backend.md §2, intermediate-representation.md §3, diagnostics N0330–N0331. The guide's generics page has a checked example.

• Types. dyn is contextual in types (Parser.ParseTypeCore, DynType). TypeKind.Dyn (TypeTable.DynOf) names an interface instantiation. The checker allows it only as a reference's pointee or a box's contents (ResolvePointee, N0330), and only for interfaces whose methods all take a reference receiver (N0331).
• Coercions (TypeChecker.CoerceToDyn) are casts, so moves and loans flow through them as through any cast. Each records its (T, dyn I) table. An argument for a borrow dyn I parameter may be a T, a box, or a temporary box: a temporary Box<dyn I> is lent, never copied out. Box.create takes no hint from an expected Box<dyn I>.
• Calls. Each interface method is a bodiless HirFunction of the dyn type (IsDynMethod, DynSlot), so a call is an ordinary NirCall. The borrow checker summarises it by its signature, and the effect checker uses its declared effects, or sleep and alloc (§37.3). An interface method's @effects is inherited by impl methods without their own list, and bounds those with one (InheritEffects).
• C and the interpreter dispatch through the table (c-backend.md §2). The interpreter gives tables addresses from 0xFFFE…, below its function addresses.
• Not done (when G3 was written; both done the same day, "The remaining items" below): the random program generator (tests/Nova.Fuzz) does not generate dyn values or owning closures yet (ADR 0015 §6 planned it with G3). No dyn benchmark yet: ADR 0015 §4 asks for one before any performance claim.

Tests (run 2026-10-28):

• run-pass/dyn.nova:
  • a vector of boxes of three types;
  • mutation through borrow mut dyn and through a vector of boxes;
  • a generic interface;
  • a box in a field and in an optional, a function returning a box, and a Result of one;
  • a temporary box as an argument;
  • drop through the table;
  • an @effects() interface method called from an @effects() function.
• run-pass/dyn-allocators.nova: a Box<dyn I, A> with a user allocator, freed with the implementation's layout (16 bytes, not the pair's).
• Both are compiled under every C configuration with -Werror, and interpreted; the outputs agree.
• check-fail/dyn.nova:
  • N0330 four ways;
  • N0331;
  • N0268, a type that does not implement the interface;
  • N0248, a mutating method through a shared reference;
  • N0234, a method the interface lacks;
  • N0295, an impl list wider than its interface's.
• check-fail/dyn-effects.nova: N0295 for a dyn call without a list in an atomic context, and for an inheriting impl that sleeps. A call with @effects() in that context is accepted.

G3: owning closures (done, 2026-10-28; ADR 0015 §3.6)

Spec: type-system.md §36.5, grammar.md (move literals, dyn fn types), c-backend.md §2, diagnostics N0332–N0333. The guide's closures page has a checked example.

• Types. dyn fn(…) -> R and dyn mut fn(…) -> R (TypeTable.DynFunctionOf) are dyn types without an interface. Their one method, call, is a synthetic bodiless dyn method (DynFunctionMethod) with the type's effect list.
• Literals. move (…) => … (ClosureExpr.IsMove) is checked as a closure literal. Its expected type is a Box<dyn fn…>, reaching Box.create through ! and ?. Its captures become CaptureMode.Move, and its environment (IsMoveEnvironment, not scoped) holds the captured values. NirBuilder.LowerMoveLiteral moves (or copies) each captured local in.
• Boxes and calls. Box.create boxes the environment. Coercing it to Box<dyn fn…> records the table, whose only entry is the body. f(args) on a place that reaches a dyn fn borrows it, mutably for dyn mut fn, and calls call, so it is an ordinary dyn call. N0248 is reported when that access is not mutable.
• Drop. The environment's drop glue destroys the captured values, through the table.
• Parser. A type argument list in an expression (Vector<Box<dyn fn(u64) -> u64>>.create()) may now contain parentheses and -> after fn.

Tests (run 2026-10-28):

• run-pass/move-closures.nova:
  • a returned adder;
  • a counter (dyn mut fn), called directly and through borrow mut Box<…>;
  • a closure owning a vector;
  • a vector of closures;
  • a closure in a struct field;
  • @effects() on a dyn fn type, called from an @effects() function;
  • a closure owning a value with a drop, destroyed with the box.
• It is compiled under every C configuration and interpreted.
• check-fail/move-closures.nova: N0330, N0333, N0332, N0299 and N0248.
• check-fail/move-closures-moves.nova: use after the capture's move (N0250), and a capture moved out of the body (N0251).

G4: threads (G4a–G4c done, 2026-10-28; ADR 0016)

Spec: type-system.md §38, ownership.md T1–T3, c-backend.md §6, N0334. The guide has a new page, Threads, whose examples are checked.

• G4a, Send and Share (TypeTable.IsSend/IsShare). They are inferred structurally, used as bounds like Copy, and checked at instantiation (N0334). @threadSafe, accepted only in library files, marks Arc, Mutex and the atomics.
• G4b, spawn and join.
  • Thread.spawn(move () => …) is checked as a move literal whose result type comes from an expected Thread<T> or from the body: an expression, or the type of every return.
  • Its captures and result must be Send.
  • It becomes the ThreadSpawn builtin with the environment, and the (environment, dyn mut fn() -> T) table is recorded. t.join() is ThreadJoin. Thread<T> is TypeKind.Thread, a move type whose drop joins.
  • Effects: spawning has sleep and alloc; joining and dropping have sleep.
• G4c, shared state.
  • lib/std/sync.nova: AtomicU64, AtomicU32, AtomicUSize, AtomicBool, Mutex<T> with MutexGuard, Arc<T>, and SpawnError.
  • It is Nova code over the runtime's nova_mutex_* and nova_atomic_*, in the style of C7's locks.
  • lib/std is new: the hosted library, compiled into hosted packages only (CoreLibrary.HostedSources). The emitter now also emits library drop functions that only drop glue reaches.
• The interpreter (Interpreter/Threads.cs):
  • A host thread per Nova thread, with a baton, switching only when a thread blocks (a join, a held mutex) or ends, to the first runnable thread in spawn order.
  • Every thread waiting is a deadlock fault.
  • A panic, fault or exit in a thread ends the run from the main thread.
  • It makes the C runtime's three allocations per spawn, so fault-injection counts agree.
• Found on the way: the emitter printed any statement-position builtin it did not list as a console write. A bare t.join(); printed the handle. The thread builtins are now listed.

Tests (run 2026-10-28):

• run-pass/threads.nova:
  • u64, String and void results;
  • four threads × 1000 increments under an Arc<Mutex<…>>;
  • two threads on an Arc<AtomicU64>;
  • AtomicBool;
  • a value moved into a thread, destroyed at join;
  • an unjoined thread joined by its drop.
• It is compiled under every C configuration and interpreted. One scratch copy of its worker part was also built with -fsanitize=thread and run three times: no report.
• check-fail/threads.nova: a capture and a result that are not Send, a spawn without a move literal, a Send bound, and @threadSafe in user code.
• check-fail/threads-freestanding.nova: N0293.
• G4d, CosmoOS userland. nova_rt_thread.c has a third branch over cosmo_thread_* and cosmo_mutex_*, which integrations/cosmoos/c1.py selects with -DNV_COSMOOS. c2.py --arch aarch64 --ssh root@10.211.55.15 (run 2026-10-28, against CosmoOS v1.0.14 on the Parallels VM) passed:
  • 185 corpus programs in the guest, threads, dyn and move-closures among them;
  • the guest fault-injection sweep, 42 programs and 386 runs;
  • the CosmoOS tree left unchanged.
• To make that possible, emitted C no longer carries what lib/std alone asks for. Composites requested only while checking lib/std (TypeTable.InHostedLibrary), and built-in items only library code names (IsLibraryUse), are emitted only where emitted code uses them, and library externs only when called. Every emit-C snapshot is unchanged.
• c2.py --arch x86_64 (QEMU, run 2026-10-28) passed the same: 185 programs, the guest sweep (42 programs, 386 runs), a clean shutdown (QEMU status 33). The corpus had outgrown CosmoOS's 64 MiB boot partition (scripts/mkimage.sh: "Disk full"), so c1.make_image now puts the programs in the image without debug information (llvm-objcopy --strip-debug; nv-threads 301 → 72 KB). The built ELFs keep it.
• Not done (when G4 was written; the status of each since, in "The remaining items" below):
  • the parallel benchmark on the Ryzen box (done: benchmarks/parallel);
  • ThreadSanitizer as a standing C configuration of the corpus (still open: the acceptance below ran it once, on the worker test);
  • dyn … + Send (type-system §38.4) is specified but not implemented, so Thread.spawn takes only a move literal (done);
  • the random program generator does not generate threads (done).

G5: checker generality (first increment, 2026-10-28)

Fifteen probes of programs that borrow checkers commonly reject, run against ee9b159 (scratch, 2026-10-28):

Probe	Result	Note
two-phase v.push(v.length)	accepted
conditional return of a borrow, then mutate (Rust's NLL problem case 3)	accepted
a loop that returns a borrow or pushes and returns another	accepted
borrow mut p.a and borrow mut p.b	accepted
a slice of an array, then a write to the array after its last use	accepted
a field of a struct while iterating another field	accepted
a move out of a local and back, in a branch	accepted
a function returning one of two views (StringView<r>)	accepted
an optional reference returned, then the vector grown	accepted
a closure reading s.b while s.a is written	rejected, now accepted	field-precise captures
borrow mut v[0] and borrow mut v[2]	rejected, now accepted	constant indices
a method returning borrow this.field, then another field written	rejected	as in Rust: a method's signature borrows all of this
borrow mut v[i] and borrow mut v[j]	rejected	as in Rust; a splitAtMut is the remedy, not yet in the library
a reference variable re-pointed (var cur = n)	rejected	by design: assigning to a reference writes through it (N0246)

Changes:

• Constant indices (BorrowChecker.Overlap). Elements at different constant indices do not overlap. Messages name a constant index (values[0], not values[_]), so three quoted messages in the README and guide changed.
• Field-precise captures (TypeChecker.FieldPrecise, HirCapture.Field, NirBuilder._fieldCaptures).
  • A captured struct local that the body reaches only through its fields is captured as one reference per field. That covers expressions, assignment targets and borrowed places, including their index expressions.
  • The closure's loans are then on those fields.
  • Nested closures and whole uses keep the whole capture.

Tests (run 2026-10-28):

• run-pass/precise-borrows.nova: reads and writes through field-precise closures, and two mutable loans of constant elements. Compiled under every C configuration, and interpreted.
• check-fail/precise-borrows.nova: a captured field written while the closure lives, a whole-local capture, one element borrowed twice, and a variable index.

Second increment (2026-10-28):

• Field-precise captures through references. A reference to a struct (this in a method) that a closure reaches only as this.x is captured as references to (*this).x, so a method's closure that reads this.width leaves this.count to the method (HirCapture.ThroughReference).
• splitAt and splitAtMut (type-system §16.5) on slices and vectors, in lib/core (SliceSplitting<T>, SliceHalves<T>, SliceHalvesMut<T>). Two disjoint mutable parts of one slice at a split known only at run time: the remedy for borrow mut v[i] and borrow mut v[j]. The halves borrow the slice while they live (N0240 for a write to it meanwhile). A split past the end panics, at lib/core's line.
• Tests: precise-borrows gains a method's closures over this, a run-time split of an array, and a vector's splitAt; its check-fail twin gains a write to this.width under a closure that reads it, and a write to an array while its halves live.

What stays rejected, as in Rust: a method returning borrow this.field borrows all of this (its signature says so), and a reference variable cannot be re-pointed (by design).

G6: a package registry (2026-10-28; ADR 0017)

Spec: tooling.md §4.6 (the registry and its index), §4.7 (version solving), §4.8 (publishing), diagnostics N0328, N0329 and N0335, and an amendment to ADR 0013 D6.

• Versions and requirements (Packages/Versions.cs): MAJOR.MINOR.PATCH. Caret requirements are the default ("1.4"), with =, >=, >, <, <=, commas and *.
• The index (Packages/Registry.cs, PackageIndex): a git repository fetched through the git cache. It holds packages/<name>.toml with [[version]] entries (version, git, commit, hash, dependencies, yanked).
• The solver (VersionSolver) chooses the newest version that fits, preferring a locked one, and backtracks. On failure it names the requirements on the package it could not choose and where each came from.
• novac fetch (Workspace):
  • resolves path and git dependencies first, collecting their registry requirements;
  • solves per index (--update [name] ignores the lock);
  • checks out each chosen commit, verifying the index's hash and the manifest's name and version;
  • writes registry+<index> entries with version and repository. Other commands read them from the lock (N0324 when a requirement no longer fits). A registry package's own dependencies come from its index.
• novac publish (Packages/Publishing.cs) checks the package: a library with a version, registry dependencies only, type-checking, a clean tree at a commit on a remote. It then prints the entry. novac index-check is the index's CI: each entry's commit, name, version, hash and dependencies, and increasing versions.
• The index repository's files are in packaging/nova-index/: a README with the publishing steps, packages/, and a check workflow that builds novac from this repository and runs index-check. The repository https://github.com/vkuttyp/nova-index was created from them on 2026-10-28, at the owner's request.

Tests (run 2026-10-28, PackageManagerTests):

• requirements, valid and invalid;
• the solver: newest, yanked, backtracking, a stale lock given up, a kept lock, explained conflicts;
• end to end with git repositories the test makes (no network):
  • a registry dependency solved, locked, read through the lock offline, and compiled;
  • a newer release taken only with --update;
  • a requirement the lock no longer meets (N0324), and a conflict (N0329);
• publish on a clean clone, and refused after an edit (N0335); index-check passing, and finding a wrong hash (N0328).

The remaining items (2026-10-28)

dyn … + Send (type-system §38.4)

dyn I + Send and dyn fn(…) -> R + Send (DynType.IsSend, NovaType.IsSendDyn) are dyn types whose boxes are Send. Only a Send value coerces to one (N0334), and one converts to its plain form, never back.

• Both forms share a C type and tables. The emitter emits each composite once by its mangled name, and a cast between equal C types is the value itself.
• Thread.spawn takes a Box<dyn mut fn() -> T + Send> too (ThreadSpawnBoxed, nvTSB_), so a closure made in one place runs on a thread started in another.
• A move literal's environment is Send when its captures are; its code pointer is an address.
• Tests: threads.nova spawns a boxed closure made by a function, and moves a Box<dyn Job + Send> into a thread. check-fail/threads.nova coerces a type that is not Send to a + Send type, and moves a plain Box<dyn Job> into a thread.
• Found on the way: deduplicating composites by C name merged a Box<T, A> of a user allocator with the system heap's, which have one C type but different drop glue. They are deduplicated by mangled name.

The random program generator

tests/Nova.Fuzz now generates three more kinds of statement:

• dynamic dispatch: a vector of boxes of two Op implementations, folded over, then changed through bump();
• owning closures: a Box<dyn fn(T) -> T> called once, and a dyn mut fn counter called twice;
• threads: a computation spawned and joined at once.

Move bodies capture only Copy values that hold no loans (InMoveClosure). All of the first 1,000 seeds type-check (--accept 1000, 2026-10-28).

The oracle on seeds 1–150 found 16 programs whose C did not compile under -Werror. These were two bugs, both fixed:

• dyn tables and thread helpers whose only use was in unreachable code were unused statics (now NV_UNUSED);
• a Result<Thread<T>, SpawnError> left by such code named lib/std's SpawnError, which was not emitted. The emitter now treats every emitted composite's parts as used.

With both fixed, seeds 1–300 run with no finding (2026-10-28). Each program is checked under five clang configurations and the interpreter. Of the 300, 66 panic and 204 exit with another status, the same in every configuration.

Benchmarks (run 2026-10-28, the Ryzen box)

benchmarks/dispatch and benchmarks/parallel (each with a README and a run.py), on the AMD Ryzen 5 PRO 3600 (6 cores, 12 threads), Debian 12, load average about 2 (a shared server), under nice. The figures are medians; every program printed the same checksum.

Dispatch (9 interleaved runs; a million boxed objects of two types, 100 passes):

Program	clang 18	gcc 12
Nova dyn (Vector<Box<dyn Shape>>)	290.2 ms (1.03 × C's table)	311.5 ms (1.05)
Nova enum and match	271.1 ms (0.96)	293.4 ms (0.99)
C function-pointer table	283.1 ms (1.00)	297.4 ms (1.00)
C tagged switch	248.6 ms (0.88)	258.0 ms (0.87)

A dyn call costs what C's hand-written table costs, within 5%. Where the set of types is closed, an enum is a little faster, as in C.

Parallel (5 interleaved runs; 40 million values over N threads). Nova's time, its speed-up over one thread, and Nova's time over C's (pthreads):

Threads	clang 18	gcc 12
1	631.7 ms (1.00×), 1.02	735.1 ms (1.00×), 0.99
2	315.0 ms (2.01×), 1.00	370.8 ms (1.98×), 1.00
4	161.8 ms (3.90×), 1.00	191.0 ms (3.85×), 1.00
6	109.8 ms (5.76×), 0.96	128.8 ms (5.71×), 1.01
12	90.9 ms (6.95×), 0.98	99.4 ms (7.39×), 1.05

Nova threads scale as pthreads do: nearly linearly to the six cores, and a little further with their second hardware threads. The spawn, the closure and join add nothing measurable.

Acceptance (2026-10-28)

The roadmap's criterion: for each gap, the probe that showed it now passes, with a spec, positive and negative tests; G2, G4 and G6 after an ADR each; performance measured on the suite.

Gap	Probe at b9fa451	Now	Spec and ADR	Tests	Measured
G1 growth	vector-growth 2.08×, string-building 2.42× C (Ryzen, clang)	1.03×, 1.61×	c-backend §2, §6	emit-c/vectors.c; the whole corpus	Ryzen, clang and gcc
G2 dyn	Box<dyn Shape> is N0100	runs, compiled and interpreted, also in CosmoOS	ADR 0015; type-system §37	run-pass/dyn, dyn-allocators; check-fail/dyn, dyn-effects	benchmarks/dispatch: within 5% of C's table
G3 owning closures	returning a capturing closure is N0299	Box<dyn fn…> returned, stored, called	ADR 0015 §3.6; type-system §36.5	run-pass/move-closures; check-fail/move-closures, move-closures-moves	— (an allocation per closure, as specified)
G4 threads	Thread is N0200	spawn, join, Arc, Mutex, atomics, + Send; deterministic in the interpreter; in CosmoOS on both arches	ADR 0016; type-system §38; ownership T1–T3	run-pass/threads; check-fail/threads, threads-freestanding	benchmarks/parallel: 5.76× on 6 cores, as pthreads
G5 checker generality	4 of 15 probes rejected that need not be	2 of the 4 accepted, and splitAtMut for a third; 2 rejected by design, as in Rust	lifetimes §8; type-system §16.5, §36.2	run-pass/precise-borrows; check-fail/precise-borrows, slice-borrows	—
G6 registry	— (path and git only)	an index, solving, the lock, publishing; github.com/vkuttyp/nova-index with its CI	ADR 0017; tooling §4.6–§4.8	PackageManagerTests (requirements, solver, end to end with local repositories)	—

Every run below was on 2026-10-28.

• The full suite (dotnet test Nova.slnx) passed at each commit. The last complete run had 3,388 tests, before the final emitter fix.
  • That fix then passed the suite's fuzz, corpus and interpreter tests (409), and every emit-C snapshot.
  • Nova CI passed on each push, the last run being 40669583703 on 3bceb32.
• CosmoOS (integrations/cosmoos/c2.py, after G4): 185 corpus programs and the guest fault-injection sweep on aarch64 (Parallels VM) and x86_64 (QEMU).
• The fuzzer, extended to dyn, owning closures and threads: seeds 1–300 under five clang configurations and the interpreter, no finding.
• ThreadSanitizer: the worker test, three runs, no report.

What M13 leaves open, as recorded open decisions or reports:

• several versions of one package in a build (OD-26);
• weaker atomic orderings (OD-24) and scoped threads (OD-25);
• scoped dyn(r) I and downcasting (OD-10a, OD-10b);
• monomorphised closures (OD-9a);
• ThreadSanitizer as a standing C configuration of the corpus.

The suite-wide performance figures in the README are from M11, rerun only for G1's three workloads.