Status: Accepted
Date: September 16, 2026
Related: ADR-284 D1 (what a program may run on is a
target, never a third value of user_parallelism), ADR-055
(a pausing function is a state machine; the executor is ours),
ADR-037 and ADR-005 Group B (every verdict is the
same at both settings), ADR-303 D3, D5 (the runtime and its
configuration), ADR-281 and ADR-288 D21 (a door’s
block is sync and touches no lock), ADR-297 and
ADR-297 (cleanup and its deadline), ADR-288 D27
(the emitted Rust and its floor), ADR-290 (a foreign crate is
described before it is called), ADR-310 (paths at build time),
Part III 13.3, 13.3b, 16, 17.2, Appendix A
Nikaia runs a program on one thread by default. A function that can pause is
lowered to a state machine (Rust’s async fn), an executor drives those
machines, and I/O reports back through a reactor. That structure is the one
embedded Rust has used for years without an operating system: the Embassy
project runs it on microcontrollers, single-threaded, with interrupts as
wakers and tasks laid out statically. “A function may pause, and the
compiler knows which” fits a device without a scheduler better than it fits
threads.
What a device does not have is the other half of std: files over
io_uring, sockets, threads, memory mapping, a filesystem to read a
configuration from, a process to exit. The language already separates the two
halves along one axis — the target — and says per function on which
target it exists (fs::map is a compile-time error on wasm32-*; threads do
not exist at user_parallelism = no). A target without an operating system
is one more column in that table, not a second language.
This record is written to be read by people who build control units. It says what carries over unchanged, what is unavailable, what the compiler promises about interrupts, memory and timing, and — with the same care — what it does not.
target, and user_parallelism is no on it.target = "thumbv7em-none-eabihf" (or another *-none-* triple the toolchain
has) in nikaia.toml selects it. user_parallelism may not be yes: there
is one core the program owns, and a multi-core device is a later target with a
decision of its own (§4). Every verdict the compiler gives is the same as on
any other target (ADR-005 Group B); what changes is which
std entries exist.
The availability table (Part III 17.2) gains the column: unavailable are
fs, net, io over a pipe, process, std::thread, memory mapping and
http; available are everything the language itself is — overlap,
spawn as a coroutine on the one executor, the four doors, Cleanup,
Seen, grammars, comptime, the trust lattice, and the DSL-based assembly of
Chapter 16 for the target’s instruction set.
no_std: core and alloc, a target prelude, and no unwinding.The generated crate declares #![no_std], depends on core and alloc
only, and takes its prelude from the target’s half of std instead of
nikaia_std::prelude. Panic is abort — which is what the language already
does at user_parallelism = no (Appendix A) — and on this target abort is
what the device does with a fault: a breakpoint or a reset, chosen by the
target’s std half; the panic hook runs first, as everywhere. There is no
unwinding and therefore no poisoning; a panic ends the program.
rust-version (ADR-288 D27) and the stable channel apply
unchanged. Nothing the emitter writes is target-specific except the prelude
and the abort.
The target’s std half provides the executor: a loop that runs ready tasks
and sleeps (wfi) until an interrupt wakes one. That is ADR-055
D3’s “the executor is ours” with a different sleep; the state machines the
emitter writes do not change.
An interrupt handler is a function the program hands to the target’s std:
irq::on(Vector::Uart0, handler). The entry’s ledger declares the parameter’s
type as fn() sync, and that one word does the work a whole embedded
discipline usually does by convention:
sync function never pauses, so a handler cannot await inside an
interrupt;touches column names no lock, so a handler cannot take one and cannot
deadlock against the code it interrupted;std provides, or read a register through the target’s DSL.A body that does not satisfy the type is refused in this language’s words
(ADR-277 D7’s NK2206), not by the device at run time.
By default the target’s std half installs a global allocator over a region
the build names, and Vec, String and HashMap behave as they do
elsewhere. That is the ordinary embedded case.
A build may say allocation = "startup" in [build]. The ledger then carries
a derived column, allocates, inferred over the call graph as touches
is, fail-closed (an entry nobody described allocates), and the compiler
refuses any allocating call outside two places: a comptime initialiser, and
main before its first call that can pause — which is the moment the
executor starts. After that moment the program’s memory is what it has.
spawn under this profile takes its task from a pool sized in [build]
(tasks = N), as Embassy’s static task pools do, and a spawn past the pool is
refused where the count is decidable and a build-time table where it is not.
What this does not claim: fragmentation-freedom or a bound on peak use. Those are properties of the program and are measured, not proved.
A door’s block is sync and touches no lock (ADR-288 D21), so
on this target a lock is a critical section: interrupts are masked for the
duration of the block and nothing else. The bound on the masked time is the
block’s own code, which a WCET tool can read. Shared counts are plain
(ADR-037 D7); nothing crosses a thread because there is none.
update on a word-sized value is a compare-and-swap where the core has one
and a masked read-modify-write where it does not (ADR-281 D13).
Promised, and checkable in the emitted code:
sync function returns without pausing, and the compiler knows which
functions are sync;overlap are in written order, and tasks are run in the
order they became ready.Not promised: a worst-case execution time, a scheduling latency, or that two runs with different interrupt timing interleave the same way. Those are properties of the program and the device, established by analysis over the emitted Rust, which is plain state machines without a runtime the analyser cannot see through. The language gives the analyser more static facts than C or Rust do — which functions pause, which touch what, which allocate — and claims nothing on top of them.
There is no file to read at start, so nikaia-runtime.toml’s settings for
this target are read at build time and baked in; io-method and
user-pool have no meaning here and are refused if written. cleanup-deadline
keeps its meaning — pending cleanups are drained at program end, bounded — on
the target’s timer, and an expired deadline ends the program as
ADR-297 says, with the status delivered the way the target’s
std half ends a program.
std half is described crates, and the qualification path is stated rather than claimed.The executor, the allocator, the interrupt table and the peripherals come
from the embedded Rust ecosystem (Embassy, the HAL crates), described
before they are called (ADR-290) so that every analysis reads
an entry at the boundary and touches, locks and allocates are
fail-closed there. Nothing is written twice.
On certification: the code that reaches the device is Rust, and a qualified
Rust toolchain exists for it. What would need qualifying as a tool is this
compiler, and two of its properties help that case — the ledger is
deterministic (ADR-005 D8) and a --locked build is
reproducible from committed files. This record claims no certification and
schedules none; it says where the line is.
std half for one board family, no_std
emission with a target prelude, the allocates column and the startup
profile, build-time baking of the runtime settings, and the target row in
every availability table. The allocator and the baked settings are the C
library’s (ADR-284), reused.user_parallelism = yes on bare metal — which is
a second executor and a Send question the single-core target does not
have.allocates beyond derived like touches,
fail-closed.