Status: Accepted
Related: ADR-297 (cleanup, which depends on D6), ADR-283
(works out D4), ADR-300 (where D7 is met),
ADR-020 (the ledger as its own file),
ADR-037 D2/D3 (the switch Group B’s Send check may not consult),
ADR-303 D7 (which relies on that check for a foreign runtime),
ADR-312 (a handle on a shared value; the crossing verdict per destination)
Nikaia promises ownership without the pain while compiling through a toolchain whose whole vocabulary for ownership is lifetime annotations and borrow-checker errors. Every borrow situation a program can produce falls in exactly one group, and the group decides who solves it.
Group A — rustc already solves it, silently. Transient borrows ending at
last use (NLL); list.push(list.len()) (two-phase borrows); borrows held across
an I/O suspension point, which implicit async inherits free from async fn’s
self-referential state machines; single-input-reference signatures (elision);
2024-edition capture defaults. These are written into the spec as guarantees
(Part I 6.5), not left to chance — the code generator must preserve them.
Group B — the compiler solves it, with no user-visible syntax. Cross-function
contract inference (D3); conditional return of a borrow (D2); Send-ness checked
structurally in the frontend at every setting of user_parallelism, so a
library written at no cannot turn out un-compilable at yes; Box::pin for
recursive functions under implicit async.
“At every setting” is a claim about the verdict, not about the severity. The check may not consult the switch, because a check that did would answer
yesfor a value whose expansion is safe at one setting and not at the other — which is the asymmetry this member exists to prevent. What the switch may decide is whether this build performs the crossing at all: atuser_parallelism = nonothing the user wrote runs concurrently, so a crossing into a task does not happen and is reported as a lint rather than refused, which is what Part III C.3 asked for. A crossing into a foreign runtime’s thread happens at both settings (ADR-303 D7) and is refused at both. The verdict is asked of a value and a destination, one answer per destination at both settings (ADR-312 D6); this is whereNK2501andNK2502come from (§5).
Group C — inexpressible in safe Rust, so the language gets a construct. Stored slices (D4); scoped tasks borrowing from the parent (D5); lock guards across suspension points (D6).
Group D — a real bug, where only diagnostics help. Mutating a collection
while iterating it is not a lifetime problem; it is undefined behaviour in C++
and a runtime surprise in Python. The answer is a named safe API for every known
anti-pattern (retain, drain, entry, swap) plus D7.
There is no lifetime syntax in the grammar and none will be added. All lifetime knowledge lives in the compiler and in the generated ledger (D3). This is a headline language guarantee, not a v0.x restriction.
Every reference-related feature is classified A/B/C/D during specification, before it is designed.
Group B’s second member is worth naming: conditional return of a borrow (the
get_or_insert shape) is rejected by the stable borrow checker, and what solves
it here is desugaring the known patterns onto entry-style APIs in the
frontend — a Group B answer, with no user-visible syntax and no lifetime the
user writes.
The desugaring is affordable because the corpus already writes it.
examples/1brc.nika and examples/access-log/src/main.nika both want exactly this
situation — look a key up, add it if it is absent, keep using it — and both write
.entry(k).and_modify fn { … }.or_insert_with fn { … }, unprompted, because that
is the natural way to write it against Nikaia’s own HashMap surface. So Group
B.2 is answered with the language’s own idiom.
The situation is reachable from Nikaia, which is what keeps it on the list
rather than in Rust’s issue tracker: thirteen lines — let found =
self.entries.get(0), if found.is_some() { return found.unwrap() }, then push
and look again — lower to Rust the borrow checker rejects with E0502.
One region variable per reference position, constraints collected from bodies, solved over the call graph SCC-wise with a fixpoint for recursion. This is rustc’s own intra-function region inference lifted across function boundaries.
Rust refuses to infer signatures from bodies for a good reason: it creates action at a distance, where editing a callee surfaces an error three modules away. Nikaia answers that with a generated, committed file rather than in-source annotations. Each build diffs fresh contracts against it:
That last line is the ledger’s purpose: turning spooky action at a distance into a narrated cause chain. A trait method stores one contract, the join of all implementations, so dynamic dispatch has something to check against. The ledger ships with published packages, so downstream builds get the same errors.
Transient = borrow, stored = tether. A slice used within a call tree stays a real
&str/&[u8]at zero cost. A slice that escapes — into a struct field, a@detachedlambda, or a return past its buffer’s frame — is lowered to a buffer handle plus aRange<u32>.
Safe Rust cannot express a struct holding a buffer and a slice into it, and no
foreseeable feature changes that. The precedent decides it: async Rust abandoned
reference slices for stored data and standardised on bytes::Bytes. Nikaia
promotes that from library convention to language semantics.
One refcount per buffer, not per token, riding the existing Shared
mechanism (a plain count at user_parallelism = no, an atomic one at yes,
ADR-312 D10). The guarantee inverts from “you may
not use this token after the buffer is gone” to “the buffer cannot die while a
token lives”, which is why the user never sees a lifetime error.
This closes the question of user-visible struct Foo<'a> permanently: no, the
tether covers the case. The lattice and the escape analysis are
ADR-283.
user_parallelism, and the spec says which.Changed by ADR-328 D10: a pausing task in a scope is polled by
the scope’s own future at every setting, so it may borrow at yes too; the
setting no longer decides what a scope accepts.
task::scope with implicit borrowing in an async context is unsound in Rust —
a cancelled scope cannot synchronously stop children on other threads whose
borrows point into the dying frame. Hence no safe async scope in tokio.
user_parallelism = no: sound. Nothing the user wrote runs
concurrently, so no child runs simultaneously with
cancellation, and teardown collects children before the parent frame dies.
This rests on two spec requirements: no mem::forget equivalent, and task
futures are runtime-owned, never user-owned values.0: sound only for sync children. A blocking compute scope (the
rayon join model) covers the real use case, data parallelism, and matches
what par_iter already demands. Async children with borrows are removed
from the spec above 0; they use @detached and return via the handle.A user will hit this without any Rust background, so the diagnostic says “a background task may outlive the things it looks at” and states the fix.
sync.access and access_all require a sync lambda at every setting.
Part II 12.2’s “no I/O while holding a lock” is Rust’s “a MutexGuard must not
live across .await” in Nikaia words. Making it static rather than a runtime
reentrancy panic removes an error class from the happy path and shrinks the
divergence of Locked[T] between settings. The runtime check and lock poisoning
stay as backstops — sync does not rule out reentrant access on the same lock
through a chain of sync calls.
What a function must do to earn sync is ADR-288.
Nikaia intercepts every backend diagnostic and re-reports it against the .nika
line that caused it.
NK code (Part III,
Appendix C). E0277, a trait bound that is not satisfied, is in the list
too, because a trait bound is how Send, sync and every future marker
rule surfaces from the backend. So is E0621, a missing explicit
lifetime (for example on a HashMap[&str, …] whose key is stored): it is a
lifetime error like the others.The mechanism is ADR-300: rustc --error-format=json is read back
and every message is placed against the .nika line that produced it, through
the source map the emitter writes.
The position and the text are two different promises, and only the first is
kept for every class. ADR-300’s translator deliberately does not rewrite a
message, because the lowering is name for name (ADR-296 D17) and
“xs does not live long enough” is already a sentence about the Nikaia source
with only its place wrong. That argument holds for the seven borrow classes and
fails for E0277, whose every noun is a Rust type the author did not write.
So for a trait bound the place is translated and the text is not, and the gap is
closed from the other end: what the frontend can decide about a crossing it
refuses itself, in Nikaia words, with NK2501/NK2502 (§5). Rewriting a
trait-bound message into Nikaia vocabulary is a second question and is open.
E0621 is the same open half, and worse. Its text is
help: add explicit lifetime 'a to the type of key — a lifetime, a region name
and a type annotation, and ADR-283 D1 says the author writes none
of the three. So here too the place is translated and the text is not, and this
one cannot be closed from the other end the way the crossing was: what the
frontend would have to decide instead is which lifetime a stored view has,
which is ADR-283 D2’s tether lattice. A partial fix is worse than none, so this
stays open.
Same tree, same toolchain, any thread count, any machine → a
byte-identical nikaia.contracts. The Cargo.lock standard, deliberately not
mere semantic equivalence.
This is cheap because the mathematics cooperates: the inference solves a
monotone constraint system over a lattice, so by Kleene/Tarski the least
fixpoint is unique and solving order cannot change the result. Nondeterminism
can only enter through implementation slips, and canonical serialisation costs a
sort. Byte equality also makes verification git diff --exit-code instead of a
custom comparer that can itself be wrong.
Every item below is a documented real-world nondeterminism source, and is banned in any ledger-emitting path:
| Banned | Why |
|---|---|
| iterating an unordered hash map to produce output | randomised SipHash seeds per process; rustc’s nondeterminism source #1, banned by its dev guide |
| consuming directory listings in filesystem order | readdir order differs across ext4/APFS/NTFS — sort every source-tree walk |
| internal counter IDs as ledger keys | not stable across runs; keys are source-derived (module path + name + signature hash) |
| absolute paths, timestamps, hostnames, environment values | standard reproducibility leaks; paths are project-relative |
| locale-dependent sorting | sort by code point, never by collation |
| thread arrival order influencing names or numbering | parallel solving is allowed; derived names come from source identity, never scheduling |
Sub-decisions: parallel solving is allowed (the requirement is purity, not single-threadedness); stability across toolchain versions is explicitly not required, or inference could never improve — the ledger records the toolchain hash and the compiler says when a diff came from a bump rather than from your code; one ledger serves every combination of the two switches (ADR-037 D4), because borrow structure is identical whatever the machine and whatever runs at once. A check that depended on a switch would put a build-time choice into a file that ships with a package.
Enforced by building twice with different thread counts and comparing bytes, and by doing that on two operating systems. A mismatch is a red build, never a flake: the risk here is not the mathematics but multi-year discipline, since any new emit path can smuggle in a hash-map iteration.
The two builds are two processes, and that is the load-bearing half. A hash
map’s iteration order is stable within one process and randomised between them,
because the seed is per-process — so a same-process comparison passes over the
one banned item that is easiest to write by accident. The second operating
system is what catches the readdir-order and locale rows.
-> &str @from(a, b)) — the contract is
derived truth and belongs in a generated artifact. A persisted, diffable
contract explains a break better than a hand-written annotation, which can
only mismatch.Shared[…] and trait impl inherits the constraints, producing
exactly the errors Nikaia exists to prevent.The frontend gains a region-inference engine and a diagnostic-translation layer. Both are substantial and both are the direct price of the headline promise.
Ledger merge conflicts resolve like lockfile conflicts: regenerate.
Send checkGroup B’s third member, the check NK2501 and NK2502 come from.
A value may cross a thread only if it may cross any thread.
Changed by ADR-312 D6: the verdict is asked of a value and a destination, not of a type alone — one answer per destination, the same at both settings.
That is ADR-303 D7’s first rule read as a property of the type
rather than of the crossing, and reading it that way is what makes it one answer
at both settings of user_parallelism. contracts::send walks a type
structurally and transitively — through a container’s arguments, through a
struct’s fields as the ledger records them (ADR-024), through a
type that holds itself — and gives one of three answers, not two:
| answer | what it means |
|---|---|
| may | every part of it may cross, and the compiler can see every part |
| may not | a part of it may not go there. Which values a destination refuses is ADR-312 D7–D9 |
| undecided | nothing written down says. A Rust type whose parts this compiler cannot walk, a ?, a lambda’s captures |
The third answer is the design, and undecided is not may.
ADR-010 D1 — an analysis that fails open is a vulnerability
generator — forbids reading the absence of an answer as permission. But
undecided cannot be a refusal either, because Stage 0 knows the type of rather
less than half of what a program writes and Part III C.4’s property is that the
compiler never rejects a program that is correct. So what the two non-may
answers cost depends on who chose the crossing:
task::both that statement
overlapping emits (ADR-292) — is a step it was never obliged to
take, so anything but may means it does not take it and the statements keep
their written order. Fail-closed costs speed here and never a refusal, which is
ADR-292 D3’s own polarity applied to the crossing question;may not and handed on on
undecided. Handed on, not accepted: rustc still type-checks the emitted
crate (ADR-002 §3), and D7’s E0277 translation reports that
refusal against the .nika line.A type whose parts are Rust can say so, in one line of the ledger: crosses
on a [type."…"] entry is a promise about a body this compiler does not read,
written in the file that ships and reviewed like code — the same kind of line as
sync = true on a Rust function. Its absence is “nobody said”, never “it may
not”.
| crossing | checked | how |
|---|---|---|
task::both — statement overlapping’s vehicle |
yes | the result of each overlapped operation crosses back to the thread that started it, so it must be able to; anything else keeps the written order. The captures are empty by construction (Accounted::NonLiteralArgument); were that limit lifted, each would be asked this |
spawn |
yes, NK2501 |
every name the task’s body mentions, looked up in the scope outside it |
| a scope’s tasks | no | task::scope has no syntax; D5 and Part II 12.7 are what it answers to |
| a value handed to a call this compiler cannot see the end of | yes, NK2502 |
ADR-303 D7’s foreign runtime. A call no ledger describes may do anything with what it is given, and a thread of its own is among them |
It is enforceable only as far as a foreign crate is honest. A Rust API that
writes unsafe impl Send about a type that is not puts a value on another thread
with nothing complaining, and a structural check in the frontend would not catch
it: the value is crossable by declaration where Nikaia can see it.
ADR-303 D7’s first rule says so.