Nikaia
Menu
v0.0.1343pre-alpha GitHub

Nikaia Language Specification

Part III: Tooling, Ecosystem & Interoperability Version: 0.0.1343 (Draft) Date: 2026-11-03

Chapter 13: The Toolchain (CLI)

Nikaia provides one command-line interface, nikaia. It builds and runs a project, manages its dependencies, formats its source and runs its tests.

Prerequisites. A Nikaia installation requires a stable Rust toolchain and nothing else. The compiler emits stable Rust and hands it to cargo. It uses no unstable compiler feature and no -Z flag. A Nikaia installation, std and the emitted Rust require Rust 1.88 or newer. The emitted Rust is Edition 2024 (ADR-305). The compiler writes that number as rust-version into every generated Cargo.toml and compares it with rustc --version before cargo runs. An older toolchain is refused before the backend runs.

13.1. Project Structure

nikaia new my_project writes a new directory, and refuses one that exists and is not empty: nikaia.toml with name and version only, src/main.nika printing Hello, Nikaia!, tests/main.stdout holding that line, and a .gitignore naming target/. A project holds:

13.2. Core Commands

Four commands take a single .nika file:

A file inside a project is a file of that project: the nearest nikaia.toml above it decides its [build] settings and its dependencies, exactly as nikaia build reads them. A file outside any project is standalone. It has the default settings and the command-line switches, and no dependencies.

Backends. nikaia build, nikaia run and nikaia lower compile through the rust backend. It is the only code generator, and it is part of every installation. nikaia interpret runs a program instead of producing one. There is no --backend switch: each command says which job is asked.

13.2b. Where std Comes From (the Sysroot)

std is not resolved by a registry and is not a type = "rust" dependency (13.3). A generated project depends on it by path into a sysroot: a directory that travels with the compiler and holds std’s sources. NIKAIA_SYSROOT names the sysroot. By default it is the source tree the compiler was built from.

13.3. Manifest Configuration (nikaia.toml)

The manifest defines the project’s metadata and the build options of Part I 1.2.

The build options live in [build]. --target and --user-parallelism override target and user-parallelism for a single build. reentrancy-check is read from the manifest. --cpu=LEVEL on build, run and test names the least CPU the program runs on, and the build may use every instruction of that level, in the program and in std; it has no key in the manifest (ADR-002 D6). On x86-64 the levels are x86-64 (the default), x86-64-v2, x86-64-v3 and x86-64-v4; every target takes native, the CPU of the machine that builds, and a target without named levels takes only its baseline and native. A level the target does not have fails the build, naming the ones it has. Where the environment sets RUSTFLAGS or CARGO_ENCODED_RUSTFLAGS, those apply and the level comes after them, so --cpu wins over a target-cpu they name. A key [build] does not know fails the build.

optimization names optimizations that change nothing a program means, as NAME:on or NAME:off words separated by commas. --optimization=NAME:on overrides it for a single build, and may be given more than once; a later word for a name wins. remove-bounds-checks:on writes an index without its check where the compiler has proved 0 <= i < xs.len(); remove-overflow-checks:on writes a +, - or * of one whole-number type without its overflow check where it has proved the result stays inside that type, a -x where it has proved x is not the type’s least value, and a shift x << k or x >> k where it has proved 0 <= k and k below the width of x’s type (ADR-306 D18, ADR-314 D5). prove-through-loops:on asks an index’s or an overflow’s check that reads a name a loop changes, and that is left open without the loop, once more through the loop’s invariant, as an assert is asked (14.2, ADR-361 D10); it changes what is proved, so what the two above may drop, never what a program means. Under it a whole-number field of the elements of a list a loop writes through an index is one summary for all its elements: a write to one element widens the summary rather than replacing it, and the summary is related to the loop’s counters, as count <= rows and |sum| <= K * count where each turn adds at most 1 to count and at most K to sum (ADR-361 D11). skip-free-at-exit:on leaves the memory main still holds at its end to the operating system: from the end of main’s last statement until the drain, each value still dies and its Drop and cleanup run, but its memory is not freed (17.1, ADR-348). All four are off by default. remove-bounds-checks and remove-overflow-checks choose only what is written; what is proved depends only on prove-through-loops. A proof reads what every write into a local list puts in it as a bound on its values, x % n as below n, the length a loop that pushes once per turn leaves, and the length of a list, text, map or set whose elements take space as below 2^60; every length, and the number of turns a for takes, is at most 2^63 - 1 (ADR-385 D1); a list whose elements take no space has only the length it was built with. A grammar’s action is proved like a function’s body, from what its bindings matched: x:dec[T](digit{m,n}) is a T in 0..=10^n - 1, c:digit a char whose code is in '0'..='9', and x:digit{m,n} text of m to n characters, each of them a digit for for d in x.chars(). A char converted to a whole number is in 0..=0x10FFFF, and a call to a function whose ledger entry has ensures is a value of which each holds (ADR-314); the name a for binds to an element of a sequence whose ledger entry has ensures_each is a value of which each holds, b.find_all(set; from: f)’s f <= s < b.len() among them (ADR-375 D5). A fold or par_fold over a grammar’s input takes at most len / max(w, 1) steps, len the input’s length and w the least number of bytes its element rule matches; a whole-number field of the accumulator that every step, the initial value included, changes by at most k, outside any loop, and that the merge leaves the sum of the two partial results’ fields or one of them, is within -k·steps..=k·steps. Where k · 2^60 / max(w, 1) fits the field’s type the field’s check is proved; where only k · len / max(w, 1) fits below a length L, the input’s length is compared with L once before the fold, and below it the step and the merge run without the field’s checks. This holds only for an input whose length is known when the fold starts, text or Bytes, and only inside the fold: a method the step reaches keeps its checks where it is called from elsewhere (ADR-367). No check that is not proved is dropped, so a program stops at an index or an overflow where it stops with both off (A.2). A dropped check is asserted in a build that keeps debug assertions; in one that does not, a wrong proof is undefined behaviour (ADR-306 D19). With both off, the emitted code holds no unsafe but the program’s own (ADR-378). It is part of the build’s cache key; std is lowered with both off.

The manifest carries what the compiler must know. How the program behaves on the machine it runs on — the number of I/O workers, the size of the pool for user code, the I/O mechanism, the shutdown drain — is runtime configuration (13.3b), read at startup by whoever runs the program.

reentrancy-check is a build option. It changes what the compiler emits and is a cache-key dimension like target and user-parallelism. refuted-claims is one too (ADR-269 D8): at error, the default, a claim the compiler shows false with values (NK1207, 14.2) refuses the program, and so does an index or an arithmetic operation it shows fails for a value the program reaches; at warn the program builds, each such claim a warning and a check where it is reached. --refuted-claims overrides it for a single build. It is the bypass for the day a better prover refutes what an older one built, and for that emergency only: a claim newly refuted in code is fixed in that code (ADR-359 D9). unproved-claims is a cache-key dimension as well (ADR-380 D2): at error, the default, an assert the compiler does not prove refuses the program (NK1300, 14.2); at warn the program builds, each such claim a warning and a check where it is reached. --unproved-claims overrides it for a single build. cleanup-deadline is runtime configuration. It changes what a running program waits for; the compiler does not read it.

[prove] names the proposers, proposers = ["cmd arg", …]: programs that nikaia prove --propose runs, each handed every loop problem left open and answering with candidate invariants (ADR-361 D6). The command starts each proposer once as a child process and writes to its standard input one JSON line per problem, {"version": 1, "id": …, "problem": …, "source": …, "names": […]}, the problem in SMT-LIB HORN, the loop’s source and the names it reads, and closes the input after the last; the proposer writes to its standard output one JSON line per problem it answers, {"id": …, "candidates": […]}, each candidate an SMT-LIB term over those names, and ends. Its standard error is shown. A proposer that fails, ends early or writes another line is skipped; the other proposers and the built-in strategies go on. nikaia prove --propose=CMD runs CMD as the one proposer of that run. A proposer may send what it is handed to a service outside the machine; that happens only through this entry and that command. No build reads [prove].

[package]
name = "hyper-core"
version = "0.1.0"
authors = ["dev@nikaia.org"]

[build]
# The machine the program is built for. `wasm32-unknown` has no threads and
# traps rather than unwinding; the target decides the panic strategy and what
# `std` offers.
target = "x86_64-linux"

# What is made: a program (the default), or a library other languages call.
# `artifact = "c-library"` exports every `pub extern fn` with a body and
# generates the header. With `target`, it decides whether foreign code may
# call in.
# artifact = "program"
# The prefix of every exported symbol and constant. The default is the package
# name with `-` written `_`.
# symbol-prefix = "hc"

# Whether user code may run concurrently. A permission, not a count; how many
# threads serve a "yes" is the runtime's decision.
#   "no"  (default) - no two pieces of user code are ever in flight at once
#   "yes"           - user code may run concurrently
# The option bounds user code, not the compiler or the runtime.
user-parallelism = "no"

# Optimizations that change nothing a program means (ADR-306). "off" by
# default; "on" writes a proved index or arithmetic without its check.
# optimization = "remove-bounds-checks:on,remove-overflow-checks:on,prove-through-loops:on"

# `cleanup-deadline` is runtime configuration (13.3b). A manifest that carries
# the key compiles, with a note naming where it went.

# A manifest that carries `ordering` fails the build, with a message naming
# `async` (Part I 8.1.2).

# Whether the compiled program notices a lock taken while a lock is held.
#   "on" (default) - the check is emitted, and a violation panics where it happens
#   "off"          - the check is not emitted
# Taking a lock inside a lock is refused at build time (Part II 12.3). Every
# program the refusal accepts behaves the same at both values. The option
# decides only whether a violation the refusal missed is noticed.
reentrancy-check = "on"

[dependencies]
# A Nikaia package by path. The key is the name a `use` writes; the path,
# relative to this file, says where the package comes from. The package is
# built as a Rust crate of its own, and its files are read for its ledger:
# `pub` is what it offers, its own `[build]` is ignored with a note (a package
# is built with the options of the program that uses it), and the overflow
# checks of A.2 reach it.
http = { path = "../http" }
# A Nikaia package by version resolves through Cargo: on crates.io it is the
# crate `nikaia_http_server`, and the generated `Cargo.toml` writes the rename,
# so the prefix never reaches a `.nika` file. `"1.2"` is Cargo's semver; a
# `git` table with a `tag` is the same arm without an index. The key is an
# identifier, because it is the `use` name. *Decided, not built yet:* a bare
# version is refused.
http_server = "1.2"
# A native Rust crate. The entry reaches Cargo with only `type` removed and a
# relative `path` made absolute, and Cargo resolves, fetches and links it.
regex = { type = "rust", version = "1.5" }

[directories]
# A directory under src/ that holds .nika files is a package of the project
# and a module of its crate (Part I 9.1). This table treats one otherwise.
"src/fixtures" = "ignore"     # not read, whatever it holds
"src/assets"   = "resources"  # not code; published, and read by asset(…)
"src/testkit"  = "tests"      # its packages are built only under `nikaia test`
"src/ffi"      = "crate"      # a crate of its own: an `extern` symbol, or Rust
                              # beside its Nikaia. It may not be in a cycle.

# Code generation, per target. These keys decide output size and speed and
# change nothing a program means. The table of the chosen target becomes the
# generated `Cargo.toml`'s profile. The panic strategy follows from `target`,
# and a build never has debug assertions (ADR-002 D5).
[build.wasm32-unknown]
opt-level = "z"     # Optimize for binary size

[build.x86_64-linux]
opt-level = 3       # Maximize throughput
lto = true          # Link Time Optimization
codegen-units = 16  # Pieces rustc cuts each crate into; the inliner sees one
                    # piece at a time. Absent, rustc chooses (ADR-002 D6).
incremental = false # Compile as one piece: slower rebuilds, faster program.
                    # Absent, it is on (ADR-002 D5).
debug = 2           # Debug info for a debugger, as Cargo spells it (0, 1, 2,
                    # "line-tables-only"). Absent, it is 0: none.

13.3b. Runtime Configuration (nikaia-runtime.toml)

The runtime configuration is set by whoever runs the program and is read when the program starts. It has four keys:

# The number of I/O threads the runtime runs. One always runs. It runs `std`'s
# own code and never user code, so it exists at `user-parallelism = "no"` too.
# More than one lets a pair of operations overlap on a machine with no
# completion queue.
io-workers = 1

# The size of the pool for user code at `user-parallelism = "yes"`. "0" means
# as many threads as the machine has. The key is read at both values of the
# build option and used at one; a key that is present is never dropped
# silently.
user-pool = 0

# The mechanism that serves a file.
#   "auto"     (default) - the kernel completes the operation where the machine
#                          can, and the blocking path serves it where it
#                          cannot. Decided when the program starts, never when
#                          it was compiled.
#   "uring"              - pinned to completion. A machine without it refuses
#                          to start; there is no silent fallback.
#   "blocking"           - pinned to the blocking path, whatever the machine has.
io-method = "auto"

# How long the runtime waits at program end for pending resource cleanups
# (flushes, rollbacks, connection shutdowns; Part I 6.4). The default is "30s".
# On expiry the remaining cleanups are cancelled (their synchronous fallback
# runs), and the program ends with exit status 70 and a message naming every
# resource that did not finish cleanly, on stderr and through the panic hook,
# never on stdout and never as a 0. "0" disables draining. The deadline always
# ends the wait: the timer runs in the runtime, and cancelling a cleanup always
# terminates.
cleanup-deadline = "30s"

The file has these four keys and no other. No key sets how many tasks run at once: admission decides (Part II, Chapter 12). Any other key fails, as under [build]. Decided, not built yet: two keys for the http package’s file bodies (17.1), send-file (auto by default, pinnable to never or to a size) and static-cache (0 disables it) (ADR-289 D24, D29). The file is read from the working directory. NIKAIA_RUNTIME_CONFIG names a file outright. Without a file, the defaults above apply.

A build option is not runtime configuration: target and user-parallelism change what the program means and stay in nikaia.toml.

13.4. C Libraries a Package Needs

There is no build script: no program of a package runs before or during a build (ADR-324). An extern block names the system library its functions come from, and the manifest says how it is found:

extern(library: "sqlite3") {
    fn sqlite3_libversion_number() -> i32
}
[library.sqlite3]
pkg-config = "sqlite3"

Every library a block names has a [library.<name>] entry, and pkg-config is required in it; a block naming a library without an entry, or an entry no block names, is NK1226. The compiler finds the library through the machine’s pkg-config, with arguments it forms itself, and links it into every program that uses the package; the program’s author writes nothing for it. A library pkg-config does not find, or a machine without pkg-config, refuses the build with NK1224. Only -l, -L, -pthread, and on macOS -framework and -F, reach the linker from pkg-config’s output; any other flag is NK1225. A block without library links nothing of its own: its functions are the C library’s every program has.

A package brings no C sources. Nothing in a build compiles C.

13.5. The Borrow Contract Ledger (nikaia.contracts)

Nikaia source contains no lifetime annotations (Part I, 6.5). The compiler infers a borrow contract for every function whose signature involves references, such as the result of longest(a, b) borrows from a or b, by analysing all .nika sources of the package as one graph. The result is written to a generated, human-readable file in the project root, nikaia.contracts: the ledger.

File format (illustrative):

# AUTO-GENERATED by `nikaia build`. Commit this file like a lockfile.
# Do not edit by hand — it is regenerated on every build.
version = 4

[fn."text::longest"]
pub = true
sync = "inferred"
signature = "(a: String, b: String) -> String from a | b"

[fn."http::Request::header"]
pub = true
signature = "(self, name: String) -> String? from self"

[type."parser::Token"]
pub = true
fields = ["text: String", "at: i64"]
tethered = ["text"]

What a contract was derived from is a file of its own (ADR-251 D1): nikaia.derived, beside it, generated and committed with it.

# AUTO-GENERATED by `nikaia`, beside the contract it describes.
version = 3
toolchain = "nikaia 0.1.0"
inference = "stage0-signatures+sync-bodies+throws-bodies+sharing-bodies"

[sources]
"text.nika" = "9f3a…"
"main.nika" = "41c0…"

The contract says what a caller may rely on; the record says which compiler wrote it, by which inference, from which sources. A compiler upgrade or an edited comment in a source changes the record, and a diff of the contract is a contract that moved. A description written by nikaia describe has the same pair, contracts/<crate>.contracts and contracts/<crate>.derived.

Build semantics. On every build the compiler infers fresh contracts and diffs them against the ledger:

  1. Unchanged: the fast path. Callers of unchanged contracts are not re-checked; the record beside the ledger is the incremental-compilation cache key. The lock is consulted before any work and decides whether a build starts at all. The ledger is compared after inference and decides which callers are re-checked. The two are separate files: the ledger ships with a published package and a lockfile does not. --locked means regenerate-and-compare for the ledger and do-not-re-resolve for the lock.
  2. Changed, all callers still valid: the ledger is updated and the build proceeds. The change is noted in the build output.
  3. Changed, and a caller breaks: the compiler uses the diff to narrate the cause chain:
error[NK2401]: a change in `longest` broke its caller `report`
  --> text.nika:8 (the change)
   |
 8 |     return b.trim()
   |            ^^^^^^^^ the result of `longest` now borrows from `b`
   |                     (previously: only from `a`)
  --> main.nika:14 (the breakage)
   |
14 |     let best = longest(title, subtitle)
15 |     drop(subtitle)
16 |     println(best)
   |             ^^^^ `best` may point into `subtitle`, which is already gone
   |
  help: either keep `subtitle` alive until after line 16,
        or return an owned copy from `longest`: `return b.trim().clone()`
  note: contract change recorded in nikaia.contracts (line 12) — if the
        change was unintentional, this diff shows exactly what to revert.

Trait methods. Dynamic dispatch requires one contract per trait method. Its keeps is what its signature marks keep (ADR-views-3 D2), and each impl’s entry carries that column. An impl, in any package, whose body keeps more is refused with NK1264. A change to the column of a pub trait method warns with NK1265, in either direction.

What the ledger records. The ledger records what a caller must know about a body it cannot see: borrows, whether a function may pause, and whether it may fail. A parameter written as a tuple pattern appears in signature as written, "((a, b): (String, String)) -> String from a | b", and every other key names its parts by their names; a caller reads a part as the component of its argument (ADR-358 D4).

key on meaning
pub fn, type reachable from outside the unit that declares it
sync fn Part II 12.1: it never pauses; what it reaches is answered by touches. true where the source asserted it, "inferred" where the body implies it, "sync(f)" where the lambda it is given decides - the source’s own sync(f) (ADR-288 D31)
throws fn Part I 7.1: it may fail, and with what: throws = ["ConfigError", "IoError"], the set inferred over the call graph. The set names error types and never one of their variants. A member written "?" is something this compiler cannot name — an unresolved call, or a call into code no ledger describes. A member written "from(p)" is what the function value given as p throws, where p is a parameter or a field path of one ("from(handler)", "from(job.run)"); a caller replaces it with the set of what it passed, and a function value is never a reason for "?" (ADR-351 D4). std’s own entries all name what they throw: io::IoError for the seven that read, write or check text, Overtaken for the lock’s two doors. Where the set has exactly one member and the member is a type any ledger describes — the unit’s own, or std’s — the failure channel is that type; where it has two or more, the channel is a generated sum over them. Either way a catch matches on the members’ variants. A set with a "?" in it travels in one opaque error
returns fn for a result whose parts hold views, each part’s sources by its path: returns = "left: from a, right: from b". A whole result’s sources are in the signature, -> String from a \| b, a written from as written (ADR-views-3 D10)
keeps fn the parameters the body keeps past the call - stores, hands to a task or to a callee that keeps it - each written keep in the source (ADR-views-3 D2): keeps = ["value"]. A caller hands such an argument over; every other one is lent. Absent on a present entry means it keeps nothing
once fn the lambda parameters the entry runs at most once, once = ["f"]: a lambda handed to one may give away what it captures (Part I 5.4 D, ADR-lambdas-1). Inferred for user code, written by hand in std.contracts (Entry::or_insert_with, Entry::and_modify, Locked::access, SharedMut::access). Absent means the entry may run it more than once
mutates fn the call changes the value it is made on. Written in the signature, as the receiver mut self; the key stands only on an entry with no receiver to write it on
signature fn its parameters, its options and its result, as the source writes them: "(path: ?, data: ?; append: bool = false, create: bool = true)". An option carries its default (Part I, 5.1) as its value, never as the expression that computed it: a literal, a struct literal of literals, or a std type’s constant constructor over literal parts (time::Duration::new(30, 0)). It is spelled as Nikaia spells a declaration (ADR-251 D4). A method’s receiver is the first parameter, written self, mut self or keep self, and self: T (or mut self: T) where its type is not the entry’s own or carries arguments. A kept parameter carries keep. Where the result points is written after it, -> String from self, -> Seq[T] from self. A type variable is declared in brackets before the parameters, as fn hand[T](x: T) declares one, and a caller binds it from what it passes and reads the result off the same signature: hand records "[T](x: T) -> T", and a call that passes an i64 gets one back. Self is ?. A bound stands where the declaration writes it, "[H: Handler](h: H) -> String", and the trait is spelled the way the declaring package writes it. Shared mutable state is written SharedMut[T]
fields type every field of a struct with its type, pub where another package may read it: ["pub name: String", "temp: i32"]
variants type every case of an enum and what it holds: ["Quit", "Write(String)", "Move { x: i32, y: i32 }"], so a match in another package is checked for completeness
tethered type the fields that hold a view, directly or through another type that does, in the order written. Each is a place of its own for what its views point into, pub or not; a field whose type holds several views is one place. An enum and a type the program throws are one place whatever this lists (ADR-views-3 D10)
compares type two values of it can be compared with == (true), for a type whose parts are the library’s; a Nikaia type compares where its fields or variants do. Absent means it does not (NK1188)
equates type its equality is an equivalence, the Eq a bound [T: Eq] asks of a library type (true). Absent means it is not taken for one (ADR-341 D4)
orders type its values have an order, the one an ordered map (BTreeMap, BTreeSet) asks of its key (true), for a type whose parts are the library’s. Absent means it has none (NK1247)
hashes type its values have a hash that agrees with its equality, the one a hash map (HashMap, HashSet) asks of its key (true), for a type whose parts are the library’s. Absent means it has none (NK1260, ADR-010 D11)
iterates type a for over a value of it can fail, so the function holding the loop declares throws (ADR-025 D6)
ends_by_length fn a sequence entry’s result can be walked from the back only where every input’s length is known (below)
pieces fn a grammar entry whose body is a par_fold: a caller in another package drives it in pieces (Part II 10.7)
threads fn a described foreign call may start threads of its own (true), may not (false), or nobody said (absent); NK2502 fires on the claim, never on its absence (ADR-290 D6)
provenance fn the function is a source: its result is bytes that entered the program from outside, and this names who chose them (ADR-010 D2). Absent means not a source, which is what almost every function is
trait."…" table a trait, with its methods as ordinary fn entries (signature, sync, throws) and no fields; a bound and an impl … for must name one. The table carries the name and nothing else. The methods are the fn entries beside it, under Handler::handle, the key shape NK1130 compares against.
impl."A for T" table an impl, in the ledger of the package that wrote it. Whether T implements A is the union over every ledger a program reads plus its own; no ledger claims completeness. A consumer reads it under both spellings, the package’s and the qualified one. An extra spelling can only make the check fail open (C.4); it never removes NK1164.
crosses type a value of this type may cross a thread (true), may not (false, which the crossing refusals NK25xx fire on), or nothing was recorded (absent). Written by nikaia describe from a foreign type’s fields — false for an Rc or a raw pointer, true where every field is plainly sendable, nothing where it cannot tell — or by hand, and never inferred. It answers only for a type whose parts this compiler cannot walk; a Nikaia struct records its fields and the check walks those. Absence means nobody said, which is not permission: the compiler does not put such a value on a thread of its own choosing
constant type how a value of a std type whose parts this compiler cannot walk is written while the program is built: a constructor and the parts it takes, constant = "time::Duration::new(secs: u64, nanos: u32)". The constructor is a std entry that is not pub. A build-time value of the type is held as its parts and crosses as the constructor over them (Part II 10.2). Absent means a value of the type does not cross (NK1167)
touches fn, type which resources it reaches and whether it reads or writes them: ["file(path) write", "stdout write"]. Absent means it touches everything, so a function nobody has described orders against everything and stays where it was written
locks fn whether the body may acquire a lock anywhere it reaches; this decides whether a call may appear inside an open lock. Propagated over the same call graph as sync. locks = "?" is this compiler could not tell, which reads as true. An absent entry means it touches a lock, the one inverted key in this file (below). The key says a lock, never which lock, so it never answers an ordering question; that is touches’s
sharing fn which of its Shared positions are one allocation, and which reference count each of those classes gets: ["counts \| <result>: plain", "hits: atomic"]. counts and the result are the same allocation, so they have the same count whichever side of the call decides it. The count is atomic unless the compiler proved that nothing crosses a thread with the class; word is the atomic count where the class is a SharedMut of a word-sized value whose crossing was proved and no access_all/update_all holds it, and its lock is a compare-and-swap (ADR-281). Absent means the function has no Shared position
maps fn for a function with a map in its signature: one line for each group of map positions its body makes one map, and what the body puts into it: ["t.counts: from(word)", "m \| <result>: from()", "seen: keyed"]. A position is a parameter, or a map field of one (t.counts), or <result>; \| joins the positions of a group. from(word, ...) adds keys as trusted as the arguments named, from() adds none, and keyed adds keys the body does not trust, or hands the map where the keyed hash is fixed. A caller hashes its map with the keyed hash where the line says keyed or names an argument it does not trust (17.1, ADR-010 D9). A map no line covers is keyed
code fn for a function that puts code (a function value) into a place reached from a parameter or its result: one line for each such place and what the body puts there, ["self.tasks.run: from(t)", "<result>.run: Bad"]. A path is one field long below the parameter, through the elements of a list or a map. A caller adds the set, from(p) replaced by what it passed, to the value it holds at that path; handles to one storage (sharing) share it. Absent means it keeps no code (ADR-351 D8)
views fn which of Part I 6.6’s states each view in its signature solved to: ["data: borrowed", "<result>: tethered"]. A view in a parameter borrows. A result borrows where a receiver or a parameter carries a view, and tethers where the buffer is one the body made. Owned never appears. Absent means the signature holds no view. --tethers (on nikaia build and nikaia lower) prints what it solved

sharing and views are the function keys whose content cannot make a program wrong. The other function keys are read as permissions: a caller that trusts a wrong sync puts a pausing body inside a lock, and one that trusts a wrong locks puts a second lock inside the first. sharing records an optimisation on a floor that is already safe: the worst a class can be given is the atomic count. A ledger that says nothing, or says atomic about everything, still describes a correct program. The classes compose across a call: a build that can read a dependency’s sources continues the analysis through its published functions, and the two reference counts never become two types.

signature and fields make a type check possible across a boundary whose bodies are not visible; the NK1xxx diagnostics of C.3 are answered from them. A ? in either is the absence of a claim. A checker reports a mismatch only where both sides are written down, so a contract that says less makes the compiler quieter and never wronger.

Only what is true is written. An absent sync on an entry means not sync. An absent entry means nothing is known, and a caller may not assume.

locks is the one key whose absence is the restrictive answer written the other way round. An absent locks means the function touches a lock. A function that reaches no lock says locks = false.

The contract carries no prose (ADR-251 D2). A /// in front of a declaration is the source’s (Part I), and the compiler does not copy it into the ledger. std.contracts, which is written by hand, keeps its sentences as # comments above the entries they are about.

sync is written in two forms. sync = true is a promise the source made; a body that contradicts it is refused with NK2202. sync = "inferred" is an observation about the body: nothing the function calls can pause, so today the function cannot pause.

Inside a package a caller does not distinguish the two forms. Both mean this cannot pause, and both satisfy the sync half of what access and par_iter require.

A caller in another package reads only the promise (ADR-288 D28). Across a package boundary, "inferred" means may pause: a change inside the body may withdraw it, and nobody promised it. A sync function, a lock’s update or access, a par_iter lambda or a grammar’s action that calls such a function is refused, and the message names the word to write in the other package (sync, or sync(f)). Only the check reads it so. The call is lowered by what the body is, and a function that cannot pause is not awaited (D3). A caller whose only pausing call is such a function may pause itself, to its own consumers.

A build names what its author could promise (ADR-288 D29). nikaia build, run, test and lower end with a note listing the package’s own pub functions that never pause and do not say sync, and those that pause only where the lambdas they are given do and do not say sync(f), each with the word to write:

note: 2 pub functions never pause and do not promise it: `parse`, `total`
  help: write `sync` after the result, and callers in other packages can rely on it

A dependency’s functions are not named in its consumer’s build.

A build warns where a pub function lost what it had (ADR-288 D32). Where the committed ledger says a pub function’s sync is "inferred" and the build finds that it can now pause, the build warns (NK2211) at the statement that made it, naming the calls that lead there. Committing the new ledger acknowledges it, and the warning is not repeated.

A diff distinguishes the two forms: the narration of a withdrawn asserted sync differs from that of a lost inferred one.

sync is one of two conditions for a body inside a lock. A body goes inside a lock only if it cannot pause and reaches no lock of its own; the first condition is sync, the second is locks.

throws is a set. The diff says which error appeared and which catch stopped covering it. The narration is NK24xx (Appendix C), the same machinery a changed borrow contract uses.

A function that runs a caller’s lambda says so. xs.map fn(n) { n + 1 } cannot pause and xs.map fn(n) { io::read()… } can, and both call the same map.

sync = "sync(f)" names the parameter that decides, as the source’s sync(f) does (ADR-288 D31). A caller reads it as this call adds no pausing of its own. The lambda’s body counts as part of the function that writes the lambda.

sync(f) is for an immediate lambda only. A parameter the callee stores or starts as a free task (@detached, Part I 5.4) may not be named by it. The rule is held by a check over std’s own entries.

locks has no sync(f) form. The check reads a lambda passed in a call directly from the caller’s body. The premise is the same immediate lambda.

A signature may name its receiver’s type arguments. HashMap::entry is written [K, V](mut self: collections::HashMap[K, V], key: ?) -> Entry[V] from self: the result holds whatever the map holds. At a call site the receiver’s actual type binds the variables, and they are substituted away: HashMap[String, Stats] makes the result an Entry[Stats] and and_modify’s fn(mut V) a fn(mut Stats), which gives the s in fn(s) { s.add(t) } its type.

A sequence has a name in the ledger, and a container keeps its own. Seq[T] is elements of T produced step by step; keys(), scalars, io::lines() and xs.iter().map fn … hand one back, and cloned() is map fn(x) { x.clone() }, a copy of each element (ADR-384 D2), and sync, pauses or throws after it say what one step may do, as after a function type. The first two are three states and not two: sync promises the step does not pause, pauses warns that it does, and neither is nobody said. A for over a sequence that says pauses gives its thread up instead of holding it; one that says nothing keeps the blocking step. The eager consumers collect, count, nth and join also read pauses. collect builds a list, or the map, set or String that the let, field or result it goes into declares, where its items fit; into a declared C[T]? from items of T? it is null at the first null item (ADR-293 D25). A Seq is consumed by walking it, so a second walk is refused with NK2702, wherever the first one took it: a let that names it again, an argument, a loop or a lambda that would take it on its next turn. Three more words say what a sequence is as a whole: ends — it can be walked from the back; sized — its length is known before it is walked; replays — walking it does not use it up, which is true of a range and of nothing produced. On a receiver they are a demand (rev writes Seq[T] ends, and a sequence without the word is NK2703); on a result they pass through, and ends_by_length = true says the result has a back end only where every input’s length is known. A walk of one whose step pauses is a for or one of the eager consumers; map, cloned, filter, take, skip, step_by and zip over one make another such sequence; rev is NK2703. A list’s windows and chunks hand out Array[T] views (Part I 2.2). A sequence never loses its producer: a consumer written right after a sequence std produces is the one the ledger names for that producer where it names one, never the general walk (find_all(set).count() counts per block and makes no position, ADR-375 D4); a step between them makes another producer. A Vec[T] or a HashMap[K, V] is a container, walked by view and as often as a program likes. Par[T] is what par_iter() hands back, and a lambda handed to it must be sync (Part II 12.6). Neither Seq nor Par is in a program’s type grammar. Seen[T] is what a lock hands out: get is -> Seen[T], the result of access is a Seen, the stamp sticks through arithmetic and through calls to entries whose touches names no lock, and a set given one is refused. A Seen[i64] is emitted as an i64. Seen is in a program’s type grammar at two places: a struct field, and a parameter of a function that touches a lock.

An unbound variable becomes ?, never a name. A variable is bound and replaced, or it is the absence of a claim. A map built by HashMap() says nothing about what it holds and binds nothing, and the chain stops there.

A variable says what flows out; ? stays for what flows in. A variable may appear in a result and in a lambda’s parameter type, and never in an argument of a std entry. Binding is narrow: from the receiver, by position, one pattern; a free function’s arguments bind its own written type parameters (ADR-288 D19-D20).

The type a lambda parameter names is a function type, fn(mut Stats). It says what the lambda is handed, so that the s in fn(s) { s.add(t) } has a type and the call on it resolves. A program writes the same type in its source, fn(i64) -> i64 sync (Part I 5.4 C).

The check on an asserted sync and the inference of sync share one resolution rule and differ in what an unresolvable call means (ADR-288 D2):

What counts as resolvable is the type checker’s answer. A call by name, such as helper(x) or io::read_to_string(), is looked up directly. A method call needs the receiver’s type. The type checker records where each method call went, and the sync inference reads that record.

Where the inference does not earn sync, a program writes sync by hand, and the body is checked against it.

A method with no entry is an unknown, and an unknown costs every function that calls it its inferred promise. A library that ships thin contracts makes its consumers’ code unusable inside access and par_iter, however pure that code is.

Writing a signature down is what lets a library’s callers be sync.

Which inference wrote it. The record beside the ledger, nikaia.derived, carries inference, naming what the ledger was derived from. The borrow contract is the widest one the signature supports: a result that is a view may point into any view it was given. sync, the errors a throws names and sharing are read off the body. A ledger regenerated by a compiler that reads one more body shows a change in the record, and a change in the contract only where an answer moved; the change is narrated. The toolchain recorded is Nikaia’s version, not rustc’s.

Distribution. A published package ships its ledger, so a downstream project builds against stable contracts and receives the same diff-based explanation when a dependency upgrade changes one. std ships std.contracts; it is the file a program’s compiler reads when the program calls io::… or fs::…. A library whose implementation is partly in another language cannot have all of its contracts inferred. Those contracts are written in the ledger, marked as such, and reviewed like code. The ones that can be inferred are regenerated and checked against the sources by the library’s own tests.

A consumer reads a dependency’s ledger; it never derives a dependency’s contracts itself. A package’s ledger is written by the package’s own build and read by every consumer, as for std. The inference runs over the package as one graph, so a call from one file of a package to another resolves. A call into a dependency is answered from that dependency’s ledger. Only a call into code no ledger describes is unresolved, and it fails closed.

A ledger is believed only while the sources it came from are unchanged. The record beside it, nikaia.derived, holds per unit the SHA-256 of the file the entries were derived from, the digest nikaia.lock uses. A ledger with no record beside it is not believed. At a consumer’s build a dependency whose sources hash as recorded is believed, and nothing is inferred. A dependency whose sources changed has its ledger derived again and written, and the difference is narrated. A dependency with a ledger and no sources is believed. A dependency is never believed against its own sources. The build is ordered by the dependency graph, so a ledger exists before its consumer is checked. A mismatch the backend reports at a package boundary is reported as the ledger of that package does not match its sources.

Version control. nikaia.contracts and nikaia.derived are committed. A merge conflict resolves like a lockfile conflict: accept either side and run nikaia build to regenerate. Where a toolchain upgrade, and not user code, changed the inference results, the build output states that the contract changes were caused by the toolchain update.

Determinism guarantee. The ledger and its record are a pure function of (source tree, toolchain), where the source tree includes the committed nikaia.proofs (ADR-270 D4): the solver’s search may differ between machines, and a build uses only the answers that file records; the same sources and the same pinned toolchain produce a byte-identical nikaia.contracts on every machine, every run, with any thread count. A violation is a compiler bug. Two consequences:

Verification mode (--locked). nikaia build --locked verifies instead of updating: the compiler regenerates the contracts in memory, the program’s and those of every path dependency it has sources for, and compares each byte for byte against its committed nikaia.contracts and nikaia.derived. Any difference fails the build with the narrated contract diff (NK2401 above). This is the one place contracts are compared rather than hashes; a development build compares hashes and derives only what changed. A CI build with --locked is equivalent to git diff --exit-code nikaia.contracts after a regular build. --locked also searches no proof: every query the build asks must have a checking entry in nikaia.proofs, and every entry must be asked; a difference fails the build with the query’s position and run nikaia build and commit nikaia.proofs (ADR-270 D22).

Chapter 14: Testing and Quality Assurance

Testing and verification are part of the language.

14.1. Unit Tests (test)

A test "name" { … } block checks specific inputs. It stands where a fn may, in any file of the package, and sees what the package sees, private names included. Only nikaia test compiles it: nikaia build and nikaia run leave it out, unchecked.

test "a blank line is counted" {
    let (lines, blank) = count("a\n\nb")
    assert(lines == 3)
    assert(blank == 1; message: "an empty line is blank")
}

A test’s body may pause and may fail. A test fails on an error that leaves its body, which is printed in its long form (the site and the chain), on a false assert (14.2), or on a panic. nikaia test builds the package once with its tests compiled in and runs each test in a process of its own, so a test that stops the program does not stop the others. It prints a line per test, the output of each failing one, and a summary, and it exits unsuccessfully where any test failed.

Each test runs under the user_parallelism the project names. nikaia test --both-settings runs each at no and at yes, and a test whose outcome differs between the two fails with both outcomes shown: a program means the same at both settings (Part I 1.2), so a difference is a fault of the compiler.

An output test is a few files and no code (ADR-269 D13, ADR-247). In a package’s tests/ directory, NAME.stdout or NAME.out/ makes NAME a test of the package’s program. nikaia test builds the program as nikaia build does and runs it in a fresh, empty directory of the test’s own, removed afterwards, so nothing it writes reaches the package. NAME.in/, where there is one, is copied into that directory first; the arguments are the lines of NAME.args and the input is NAME.stdin, each empty where the file is absent. The test passes where the program ends successfully, prints exactly NAME.stdout (where there is one) and leaves every file NAME.out/ names with exactly its bytes; a file it writes that NAME.out/ does not name is not compared. A failing one is reported as a line difference, - expected and + produced. Output tests run beside a package’s test blocks, and at both settings under --both-settings. A package’s output tests run side by side, as many at once as the machine has cores, or as NIKAIA_TEST_JOBS says (1 runs them one after another); what is printed comes in the tests’ order whatever finishes first.

A test program is tests/NAME.nika (ADR-269 D22): a program of its own that may use the package. NAME.stdout is what it must print and NAME.stderr what it must write to standard error, or, where it must be refused, the compiler’s whole message, its path written tests/NAME.nika. The test passes where what happened is what is written: a program refused where no NAME.stderr holds that refusal fails, and so does one that builds where NAME.stderr holds a refusal. The package’s own output tests take a NAME.stderr the same way. A passing program’s standard error is compared only where a NAME.stderr exists, and --bless writes one only for a refusal or where the file already exists, so warnings are never blessed. A refusal is the Nikaia compiler’s error[NKxxxx]: a program that fails in rustc fails the test as not compiling and is not blessed. A refused program is only checked, never compiled; the ones that build are compiled together.

A test program’s --bounds report is an expectation too (#1069): NAME.bounds holds the check --bounds report of NAME.nika at prove-through-loops:off, NAME.loops.bounds the same at prove-through-loops:on, each computed as check --bounds computes it for the program, whatever the build’s remove-* levels (ADR-306 D14: what is proved does not depend on them). Each that exists is compared byte for byte after two normalisations: the first line names the program tests/NAME.nika, and its tail ` - written without their check: … is cut, so the file depends neither on –both-settings nor on the machine. A difference fails the test and is printed as a difference; –bless writes the files that exist (a new one starts empty). A .bounds or .loops.bounds` with no test program beside it is an error.

nikaia test --bless writes the expectations from what the program did: its standard output into NAME.stdout where the test has one, its standard error or its refusal into NAME.stderr where the test has one, and each file it wrote into the NAME.out/ entry of that name. Only a run that ended successfully is blessed, and at --both-settings only one whose two runs agree. A new output test starts as an empty NAME.stdout, or the empty NAME.out/ entries it should compare, and is blessed; the change is reviewed in version control.

A test block runs in the package’s directory, so it reads what the package holds, and writes under fs::scratch(): a fresh, empty directory handed back as an fs::Root::Dir, inside the test’s own directory and removed with it.

--asserts (ADR-269 D7), beside --overlaps (every task an async form starts, its window, its wait point and its group, and per par_iter call the execution chosen - pieces or one task per element - and the call that made a lambda pause, Part I 8.1.2, Part II 12.6), --sharing, --tethers, --trust and --comptime on nikaia build and nikaia lower, prints every assert of the program by line and how it is held (14.2): proved while the program was built, a precondition its callers prove, checked at run time - with the reason the prover gave up -, or checked by a test when it runs; and how many are checked at run time. Where the build refuses a claim it did not prove (NK1300, unproved-claims = "error", ADR-380 D1), that claim is listed as refused, with the reason, and not as checked at run time. It is how a reader asks where the unproved claims are, so those come first: refused, checked at run time, checked by a test; then the claims checked where outside data arrives (main’s preconditions); and last what the build proved, the claims proved and the preconditions proved at every call it sees. On a terminal the first group is red, the second light blue and the last green; NO_COLOR or output that is not a terminal prints no colour.

--bounds (#389) is the same report for the checks the compiler writes itself: every index into a list and every +, - and * that --optimization may drop the check of (ADR-306), by line, proved or checked, and for a checked one the shape that stopped the walk - a field, a list of lists, a product of two unknowns, a call’s result, or no fact on what it reads - with the issue that would supply it. It reports what the build proves, whatever optimization says. It names where the next fact pays off; it does not prove the fact would be enough.

14.2. Assertions: a contract the compiler proves where it can

assert(cond) and assert(cond; message: "…") claim that cond holds whenever the line is reached. assert is a prelude function the compiler knows, not a statement: it needs no use and costs no reserved word, and a program that declares its own fn assert calls its own.

The condition changes nothing. It may not pause, may not fail, and may not touch or change anything: every call in it has to be sync, throw nothing, touch nothing (touches = []) and change nothing, and a call nothing describes is not known to. A condition that could is refused where it is written (NK1194), because a condition with an effect would make the program depend on whether the check is performed, and a condition that reads the world has no value a compiler could prove. assert takes one bool and one option, message:, which is text (NK1195).

An assert is a contract the compiler proves (ADR-269 D4, ADR-380). A claim the compiler proves while the program is built has no check emitted, so it costs nothing when the program runs. A claim it does not prove refuses the program, NK1300, and the message says why and that not proved is not false; so does a function’s precondition that a call the build sees does not prove. With unproved-claims = "warn" (13.3) the program builds, each such claim a warning and checked where it is reached, and a false one stops the program as panic does (A.2). A precondition of main, a claim in a test and an assume are not refused for being unproved. The claim means the same either way - a proof only removes its cost.

An assert is not a guard. A guard - throw … if c, return … if c - handles a case the program expects to meet. An assert says the case cannot occur, and that if it does, the program is wrong.

What the prover reads (ADR-269 D9). Comparisons of whole numbers built with +, -, a * by a constant and a / or % by a positive constant or by a divisor that what is known pins to one value (ADR-359 D5, D6), joined with &&, || and !, over bindings that do not change - a comptime binding among them, as its value (D7) - a path of fields from such a binding (p.end, t.slots.len()) for as long as nothing can change it - through a parameter the function only borrows, the whole body (ADR-306 D17) - a path of fields through one element of such a path, indexed by a name (t.slots[at].sum), until the name changes or a write may reach the same fields of any element of the list (D20) - a type’s invariant over such a value, written or found (ADR-369), and a let mut binding no call is handed and no lambda changes, followed through each assignment: after x = x + 1 the name is the old value plus 1, after a branch that changes it on one side it is either side’s value, and a name a loop changes is read through the loop’s invariant (ADR-361 D2, D9), and the len() of a list or text that does not change - and a property (ADR-381): a call of a sync function that returns bool, throws, touches and changes nothing, over such names or over bindings and paths of fields nothing can change, is a name of its own, the same name for the same function and arguments; it holds after an assert of it is reached, after a guard that leaves when it is false, from a precondition, a callee’s postcondition, a type’s rule and an assume, until an argument may change, and as a precondition it is carried to the caller and published as written; its body is not read, so a proof of it removes its own check and nothing else; it knows the branch an if is in, what a jump with its condition after it has ruled out (return 0 if b == 0 leaves b != 0), a for over a range, a let’s value and every claim proved before. It may fail to prove a true claim and never proves a false one (D10); a claim it cannot prove is NK1300, or at unproved-claims = "warn" checked when the program runs. A claim that what is known before it rules out - false every time it is reached, proved so - is an error, NK1207, with values for its names from a model of what is known (D8): a program the compiler has shown wrong does not build. refuted-claims = "warn" (13.3) builds it, the claim a warning and a check. So is a call that breaks its callee’s precondition every time it is reached. So is a claim false for some of the values that reach it, where what is known is exactly what reaches - no parameter, no call’s result, no condition the prover cannot read, no loop that may end early stands between the values and the claim - so that a value what is known allows is one the program reaches: for i in 0..<10 { percent(1, i) } is told when i is 0. A claim that is only not proved is not NK1207: elsewhere a value what is known allows need not be one the program reaches; it is NK1300.

A claim a loop stands before is asked through the loop (ADR-361). A claim that reads a name a loop changes, after the loop or inside it, and that is left open without it, is asked once more as the loop’s problem in Horn clauses: its state, its entry, its condition, a turn, and each way out - a break, a continue and a return each one of its own. Nobody has to write an invariant: the compiler searches for one with the strategies it has, cheapest first, under the build’s counted budget. An assert that reads names the loop changes is a claim where the flow reaches it, wherever it stands in the body, and once proved a fact the search may use. An invariant is used only when three queries are proved with their certificates - it holds at entry, a turn keeps it, and with each way out it gives the claim - and it is kept in nikaia.proofs with what found it, a strategy or a proposer (13.3); where it came from never decides whether it is believed. --asserts names, for a claim proved through a loop, the invariant and its origin, and for one left open, the loop and the names it changes.

A loop of a constant number of turns, at most 16, is also followed turn by turn (ADR-361 D12). Where the number of turns is a constant the prover reads - a for over a range with literal bounds, a counter a constant step takes from a known start to a literal limit - and at most 16, each whole-number name the loop changes gets one candidate per turn: at the start of turn k it lies in the interval that k turns of the body give from its start. Each candidate is checked as any other, and one that does not hold is dropped; --asserts names these as turn-indexed intervals. Beyond 16 turns, or with a number of turns the prover does not read, nothing is proposed. A whole-number let in the body whose value the prover does not read - its type written, or a cast - is a name of its own, so a guard that tests it constrains it, and a throw in the body is a way out of the loop, as a return is, not a turn. So four turns of n = n * 16 + d, after return 0 if d < 0 || d > 15, prove n <= 0xFFFF.

A loop counts its turns, and a counter is bounded by them (ADR-361 D13). A for over a collection with a length has a turn count t, which the program cannot name: at the start of each turn 0 <= t < len, len the length where the loop is reached, since a for cannot change what it walks (NK2305); over a..b it has t < b - a and its binding is a + t. A while counts its turns by a name it grows by exactly 1 on every path of a turn, t being i - i@, what the name has gained since the loop was reached. A whole-number name n the loop changes only by adding constants of one sign - at least l and at most k along any path from the start of a turn to its end or a continue - lies within l * t <= n - n@ <= k * t at the start of each turn, n@ its value where the loop was reached; these sums are a turn’s step and the start the base, so the bound is checked as any candidate is. A name changed any other way - reset, multiplied, by a call, in an inner loop or a lambda - gets none. Both settings of prove-through-loops read these bounds. So at += 1 in for x in xs, from at = 0, is proved, at < xs.len() and every length below 2^60 (ADR-306 D12), and n += 1 in a while i < xs.len() that ends each turn with i += 1.

The prover’s logic is a package a program may ask too (ADR-270 D24-D26). Its terms, queries, answers and verify are public; its solvers are not. It is not part of std: a package depends on it at a version, and may call it while it is built, as any Nikaia dependency that only computes. A question asked while a program is built is not an entry of nikaia.proofs: it gets the reference solver’s answer under a budget counted in work, the same on every machine, and unknown proves nothing.

A claim about parameters is the caller’s (ADR-269 D5). An assert at the top of a function that names only its parameters - its options among them (Part I 5.1) - and that the body cannot prove, is the function’s precondition: the body assumes it, a call that proves it - with an option’s default where it leaves the option out - costs nothing, and a call that does not carries the check, so that a failure names the caller. divide below asks each caller to show b != 0. ADR-269 D14-D21 generalise this, within a package and across packages, and it is built: a claim is carried back to the entry - a let is substituted, a parameter changed before the claim included, a branch becomes an implication, a guard weakens it - and where it then reads only the parameters it is a precondition, path → claim: let y = x - 1 and if mode == 1 { assert(y > 0) } make mode == 1 → x - 1 > 0. A call is carried back too: a callee’s precondition the body cannot show, with the arguments in place of the parameters, is the function’s own, as an assert of it at the call would be - so the caller that passes the value is the one told, and the calls in between need no check. A call that can come back to the function, directly or through others, is not carried back. A loop, a lambda, a match arm or a call’s result stops it, and the claim stays a check. A computed precondition is proved at each call or checked in the body, and a call that breaks it is told the condition and the assert it came from. A claim about the value returned, shown at every exit, is a postcondition, and a caller knows it of the result: after let c = clamp(n), clamp’s result >= 0 holds of c. So does a call inside a let’s value: let e = 10 + clamp(n) knows clamp’s postconditions of its result. A sync function whose body is one return e, with e a whole number the prover reads, ensures result == e, published with from = ["return"] (ADR-314 D3): text::digit_value ensures result == c - 48, a char standing for its code. Inside its package, a call’s result is also known by what its callee’s body returns, where a claim needs it (ADR-359 D1-D3): a body without a loop that changes a name it reads, a match or a call that can come back to it, whose every exit returns a whole number the prover reads, gives for each exit the path to it and the value returned, and a claim that what is known leaves open is asked once more with it. It is observed, not promised: the ledger writes it as inferred, a caller in another package does not see it, and a change to it is not warned of. So example(2) over fn example(a: i64) -> i64 { let whole = 10 + a; return positive(whole) } is 12, and assert(4 / example(2) > 10) is refused, the note naming the value of each call it read. Where only the body of a function in another package the build reads from a path would decide a claim, the claim stays as it is and a hint, NK1263, names the fact and the assert on the result that would promise it. A call whose arguments are all values the build knows is run while the program is built, where a claim that what is known leaves open reads its result (ADR-359 D11-D13): compiled and run as a comptime is (Part II 10.2), its body sync with an empty touch set, under the same budget; its value is a fact, so assert(fib(10) == 54) is refused. A call that cannot be run - not sync, touching anything, outside this build or over the budget - leaves the claim a check; one that stops is told as a check that fails every time it is reached (NK1207). The ledger publishes both - requires, ensures, and the assert each came from - so a caller in another package proves the one and relies on the other; a guard is only observed and is not published. A function with a precondition has two entries: f checks it and calls the body, f__unchecked; a call that proves it or checks it where it stands calls the second, and every other caller - a function value, a method call, another package, the language below - reaches the first. A method of a trait’s implementation has no precondition. A contract changed in the breaking direction - a precondition stronger, a postcondition weaker than the committed ledger’s, decided by the solver - warns its author (NK1208) until the ledger is committed.

A claim about data from outside the program is refused (NK1202, ADR-269 D6; standard input and files are such data unless marked trusted: true, ADR-365): it is not a defect when such data is wrong, so it is checked where it arrives, with a guard the program handles (ADR-010); after the guard, the claim is proved. main’s parameters are such data, and the check is made for them (Part I 5.5, ADR-360 D3, D4): main’s preconditions are derived as any function’s are, carried back to its entry, and are checked after the words the program was started with are read and before the body runs; a breach ends the program with exit status 2 (A.2). --asserts reports each as a precondition of main checked where the words arrive.

A claim the program vouches for is unsafe { assume(claim) } (ADR-376). Written only inside unsafe (NK1294) and never in std (NK1295), it is read as an assert’s claim is, may speak of data from outside the program, and is a fact from where it stands. In a build with remove-bounds-checks:off and remove-overflow-checks:off it is checked as an assert is; in a build with either on it is not checked, and a false claim is undefined behaviour. nikaia check --asserts lists every assume, and --bounds and --asserts name a check or claim proved only with an assume’s fact as proved from an assume, with its line (ADR-381 D6).

In a test, a claim is the test’s verdict and is checked when the test runs. A false one stops the test, as panic does (A.2), and says what only the compiler knew: the line, the message, the claim as written, and the value of each operand of its comparison - a literal’s value is already on the line, and an operand whose type has no printed form is left out.

fn divide(a: i64, b: i64) -> i64 sync {
    assert(b != 0; message: "division by zero")
    return a / b
}
src/math.nika:2: the program stopped: assertion failed: division by zero
    assert(b != 0; message: "division by zero")
    b is 0

14.3. Property-Based Testing (Fuzzing)

Fuzzing generates random data to find crashes. The test runner does this for a test that declares parameters.

Automatic data generation A test that declares parameters is given generated inputs.

struct User { name: String, age: i32 }

// Nikaia automatically creates random 'User' structs here
test "User Validation" (u: User) {
    assert(u.age >= 0) // Might fail if fuzzer generates -1
}

Custom generators (impl Generator) Where random data does not fit the type, such as a field that must hold a valid email address, the type implements the Generator trait.

impl Generator for User {
    // 1. How to generate standard random samples
    fn arbitrary() -> User {
        User { 
            name: String::random_alphanumeric(10), 
            age: i32::random_range(0, 100) 
        }
    }

    // 2. Defining "Edge Cases" (Values likely to break things)
    // The fuzzer will ALWAYS try these values first.
    fn edge_cases() -> Vec[User] {
        [
            User { name: "", age: 0 },         // Empty/Zero
            User { name: "A".repeat(1000), age: -1 } // Overflow/Negative
        ]
    }
}

14.4. Benchmarking (bench)

A bench block measures the speed of user code.

Regression detection nikaia bench:

  1. executes the block thousands of times;
  2. calculates the average time and the standard deviation;
  3. compares the result against the last recorded run.

Where the new version is more than 5% slower, the CLI prints a warning:

Performance regression: ‘Sorting’ is 12% slower than commit 8f3a2c.

Result storage Results are stored in .nikaia/benchmarks.json. The file records:

bench "Sorting" {
    let mut list = [5, 2, 9, 1, 6]
    list.sort()
}

Viewing history nikaia bench --history shows the recorded history.

Chapter 15: Interoperability (FFI)

A Nikaia program calls C and Rust, and a Nikaia library is called from C and from every language that speaks C.

15.1. C Interoperability

A call into C is written inside an unsafe block, and so is an assume (14.2, ADR-376).

extern {
    fn strlen(s: ref Array[u8]) -> usize
}

fn main() {
    let text = "hello\0"
    let n = unsafe { strlen(text) }
    println(f"{n}")
}

A C string ends at a zero byte, and the caller puts it there.

extern and unsafe are reserved words with constructs. extern is the C calling convention, the only one on every target, and is written without naming it: extern "C" is NK1227. extern(library: "name") names the system library a block’s functions come from (13.4). An extern block lowers to Rust’s own, and the call lowers to Rust’s own unsafe. A call to an extern name outside an unsafe block is refused with NK1143. A declaration in an extern block is sync and carries no throws without writing either. Its touches and locks are fail-closed, as a described crate’s are.

What the boundary lends is a view. ref T, ref mut T, ref Array[T] and ref mut Array[T] in an extern declaration are the pointer C wants, and each lives for the call. Nothing is stored and nothing escapes. A ref Array[T] takes whatever lends a run of elements — a Vec[T], an Array[T, N], and text where the element is u8 — and the call makes the address.

A length beside a view is checked at the call. A ref Array[T] followed by a usize is one fact: the pointer says where and the count says how far. A call whose count cannot be shown to fit the buffer is refused with NK1159. Two shapes are accepted: the buffer’s own len(), and a constant a known length covers, which is an Array[T, N]. The type usize, not the parameter’s name, marks the length. A usize in a declaration names C’s size_t; a caller passes an i64, and the conversion is emitted.

ref mut is the boundary’s and nowhere else’s. Away from it, a parameter the callee may change is written mut name: T, and a ref mut outside an extern declaration is refused with NK1158. A ref Array[T] is a view of a run everywhere; only in a declaration does it lower to an address beside a count.

A handle a library hands out is opaque:

extern {
    opaque type FILE released by fclose
    fn fopen(path: ref Array[u8], mode: ref Array[u8]) -> FILE
    fn fclose(f: FILE) -> i32
}

An opaque type is an address the language never dereferences. It is moved and stored like any value. It has no fields, no indexing and no constructor; a field access, an index or a call of it is refused with NK1160. Its release is a cleanup the compiler runs at the end of its scope (Part I 6.4), so a handle cannot be forgotten. A C function that keeps the address past its own call is not checked.

A handle is lent to every declaration but its release: fileno(f) reads it and f is still the caller’s to close, while fclose(f) takes it and is the cleanup. None of opaque, type, released and by is a reserved word; each means something only in this position and is a name everywhere else.

A handle that may be absent is a T?, as in Part I 2.3: ?? and ?. get past it. A handle holds a non-null address and T? is the absence of one, so a nullable handle is one machine word, and ref mut sqlite3? is sqlite3 ** as C writes it. This makes an out-parameter work:

extern {
    opaque type Block released by free
    fn posix_memalign(out: ref mut Block?, alignment: usize, size: usize) -> i32
    fn free(b: Block)
}

fn main() {
    let mut room: Block? = null
    let rc = unsafe { posix_memalign(room, 64, 128) }
    println(f"{rc}")
}

At this boundary a ? on a ref mut T or a ref Array[T] belongs to what it points at and not to the view: ref mut sqlite3? is a slot that holds a handle or nothing. A plain ref T? is 2.3’s own nullable view.

A declaration that does not say ? is a claim. Where C hands back nothing, the program aborts with a message naming the declaration (Appendix A.2). A T? reaches the T a parameter wants through ?? throw: slot ?? throw Refused::NoDatabase is a sqlite3.

Text a C library hands back is a CStr, and std copies it:

use std::foreign

extern {
    fn getenv(name: ref Array[u8]) -> foreign::CStr?
}

fn main() throws {
    let home = unsafe { getenv("HOME\0") }
    println(home?.to_string() ?? "none")
}

A CStr is an address the caller does not own, whose lifetime is the library’s, and which ends at a zero byte. It is an opaque handle with no cleanup. to_string copies it into a String; the walk to the zero byte is written once, in std. to_string fails where the bytes are not UTF-8. A declaration says -> CStr? where the library may hand back no text, and the program writes ??.

There is no raw pointer, and Pointer[u8] is not a type. Pointer[u8] is refused with NK1135. Memory the language indexes arrives with a length it knows. A program that needs a buffer makes one in Nikaia and lends it.

A build that lets C call in is a target. An exported entry point may be called twice at once from threads the caller owns; user_parallelism does not bound those. Such a build is one artifact, safe at its boundary: the entry points and everything they reach take the safe shape, and the rest of the library keeps the per-value answer.

Providing a library to C, and to everything that speaks it. A pub extern fn greet(name: ref String) -> String { … } with a body is an entry point. A build with artifact = "c-library" in [build] makes a shared and a static library of the package and generates <package>.h from the ledger. The caller owns the memory, and a call never surprises.

15.2. Rust Integration (Deep Integration)

The compiler verifies safety properties at the boundary with a Rust crate.

A value handed to a Rust function may reach a thread that function owns. A call whose body the compiler cannot see may put what it is given on a thread of its own. A value may cross into a foreign thread only if it may cross any thread. The crossing the compiler can decide about is refused with NK2502 (C.5), at both values of user_parallelism.

The rule reaches as far as the Rust signature is true. Where the compiler reads the signature, a value is crossable by declaration. A narrowing shim is reviewed like the boundary it is.

A call into foreign code is judged by what its arguments can reach. Where no lock is reachable from the arguments, transitively and through the fields of a struct, the call is allowed. Otherwise the call is refused with NK2503 (C.3, worked through in C.6); the way out is to keep the lock out of the call’s reach and hand over a copy of what it needs. A lambda among the arguments is its captures, so whether it touches a lock is read off its body (Part II, 12.3). A foreign function a ledger describes is not subject to this rule.

“No lock reachable” is an answer, not the absence of one. Where nothing written down says what a value contains, the question is undecided: C.5’s third answer, which is not permission and is handed on. A ledger entry with an empty field list, which is what a type whose fields are Rust has, means nothing recorded and not nothing inside (13.5).

Mapping Types

A crate is described before it is called. A call into a crate the manifest declares with type = "rust" that no contracts/<crate>.contracts describes is refused with NK2504, once per crate, with the command in the message. A written type from such a crate counts as a call; a name the build did not declare is left alone (C.4). nikaia describe <crate> reads the crate’s pub signatures, from rustdoc-JSON where the toolchain offers it and from the sources where it does not, and writes a draft entry for every function the program calls and the types those signatures name, translated by the table above. The draft names what it could not answer. A version dependency is refused with its reason. The draft is committed as contracts/<crate>.contracts and reviewed like code. It is believed while the crate’s version and source hash hold. A file that hashes differently is NK2505, and the way out is the same command and another review. What a signature cannot say (touches, locks) is written fail-closed, and what neither reader can read is written ?. The description’s entries are read: the signature types the call and what it hands back, throws makes it a place that can fail, and sync makes it one a sync function may not make. A described crate is a package, and nothing about it is imported. Where the backend disagrees at a call into a described crate (not a future, a ? on what is not a Result, a Result where none was expected), the build says the description of X does not match the crate, keeps the backend’s words as a note, and the way out is the same command and another review (ADR-290 D21).

A crate may ship its reviewed description. A crate that keeps a nikaia.contracts beside its Cargo.toml, with the [sources] it was reviewed against in a nikaia.derived beside it, ships its description. For a path dependency on such a crate, nikaia describe <crate> adopts that description instead of drafting one: it checks that the file’s # crate: <crate> <version> line names the crate’s version and that every source file hashes as recorded, and copies both files to contracts/<crate>.contracts and contracts/<crate>.derived, saying so. A shipped description that names another version, or whose sources hash differently, is refused, and the way out is another review in the crate. The project’s copy is the one the build believes, under the rule above (ADR-290 D22).

Thread Safety (Send/Sync) Whether a value may cross into foreign code is decided from the Nikaia type of the argument. No crate metadata is read.

# nikaia.toml: a Rust crate
[dependencies]
image = { type = "rust", version = "0.24" }
// In code
use image                    // a Rust crate: nikaia.toml declares it with type = "rust"

fn process() {
    // Allowed because the argument is text, and text may be passed to another thread.
    let img = image::open("test.png")
}

15.3. WebAssembly (WASM) Synergy

WebAssembly runs in a single-threaded host with a linear memory. user_parallelism = no matches that host.

Zero overhead. nikaia build --target=wasm32-unknown produces compact binaries. The runtime a no build starts is the I/O worker and nothing else, and no OS-level mutex is generated. At user_parallelism = no every Shared[T]’s owner count is the cheap count. The verdict on a crossing does not move with the build option: a call whose body the compiler cannot see is refused a lock and a Shared at both values.

A library for the web is the same build with artifact = "c-library" (15.1): the pub extern fn declarations become the module’s exports, a generated .js and .d.ts stand where the header would, the host obtains its buffers from <package>_alloc, and a function that may pause is a Promise driven from the host’s event loop. There is no extern "wasm".

JavaScript Interoperability (dsl js) Nikaia does not map the DOM to Nikaia structs. A program embeds JavaScript with the dsl keyword (Part II, 10.5).

// main.nika
fn main() {
    let message = "Hello from Nikaia!"

    // The 'js' grammar parses the code. ':msg' is a parameter hole -
    // a deferred parameter, not string interpolation, so the value cannot
    // be spliced into the source text and change its meaning.
    let script = dsl js {
        document.querySelector("#submit").addEventListener("click", () => {
            window.alert(:msg);
        });
    } eod

    // Subject: none ; Config: msg
    script.exec(msg: message)
}

Chapter 16: Hardware Instructions (via DSL)

Hardware instructions are not part of the Nikaia core language. They are provided by library-defined DSLs, dsl backend::x86, dsl backend::arm64 and dsl backend::wasm, each of which validates its own operands.

Before assembly: lanes and instructions as functions (ADR-371). std offers a portable vector of lanes - loaded from a Bytes at a position, checked as that cut and proved as it is, compared into a mask whose first set lane is a position - with crc32c and a prefetch hint beside it; each has a meaning on every target, an instruction where there is one. An instruction of one architecture is a safe function of its module, std::backend::x86::pext(x, mask), callable only in a build for a CPU level that has it and refused elsewhere at compile time. No unsafe is written for any of it; the assembly below is for what neither offers.

hash::crc32c(crc: u32, word: u64) -> u32 is the CRC-32C (polynomial 0x1EDC6F41, reflected) of word’s eight bytes, lowest first, continued from crc, with no inversion before or after (ADR-371 D5). Its value is the same on every target.

hash::sha256_hex(data: Vec[u8]) -> String is the SHA-256 digest of data (FIPS 180-4) as 64 lowercase hex characters, the same text on every target.

target::has(i: target::Instruction) -> bool answers whether the CPU level the program is built for (--cpu, 13.3; without it the target’s baseline, never the machine that builds) has the instruction i: Crc32c (x86-64 from x86-64-v2, AArch64 with crc), Bmi2 and Avx2 (x86-64 from x86-64-v3). In a comptime (Part II 10.2) it answers for that level, not for the machine that builds; at run time it answers the same. A comptime result that reads it is kept per CPU level (ADR-371 D6).

16.1. Why not a core construct

The core language has no asm block and no register constraints. Each backend DSL defines the operand model its hardware has and the grammar that validates it.

16.2. Usage

Assembly uses the standard dsl syntax. The assembly DSL uses immediate capture (meta::capture, Part II 10.5): it binds variables from the current scope and injects machine code at the call site. In an assembly block, val is the val in the enclosing scope.

use std::backend::x86

fn fast_add(val: i64, ptr: Array[i64]) -> i64 {
    let mut result: i64 = 0

    // The grammar parses the bindings and resolves 'val', 'ptr' and 'result'
    // from the enclosing scope.
    dsl x86::Asm {
        // 1. Binding header - syntax defined by the x86 grammar
        $v = in(reg) val
        $p = in(mem) ptr
        $r = out(reg) result

        // 2. Instructions
        mov $r, $v
        add $r, $p
    } eod

    return result
}

The constraint vocabulary (reg, freg, mem, imm, clobber declarations) belongs to the x86 grammar and is documented with it. A stack-machine backend declares a different vocabulary: dsl wasm has locals and a value stack, not registers.

16.3. Consequences

Chapter 17: The Standard Library and the Official Packages

The standard library is the core the language stands on: input and output, files, text, collections, tasks, locks, processes, time, the command line and numbers. It consists of universal modules, with the same API on every target, and target-specific capabilities. A format or a protocol is an official package (17.3).

17.1. Universal Modules

These modules rely on the unified types and behave identically at every value of every build option. Their implementation differs to match the runtime model.

std::io — standard input

A stream is not a file: the surface has no map, no seek, no length, and no second read of the same bytes. Standard input’s bytes do not exist until they are read, so a program that wants views into its input owns the buffer first.

pub fn read_to_string() -> String throws   // all of it, UTF-8 validated
pub fn read() -> Bytes throws              // all of it, as bytes
pub fn lines() -> Lines throws             // one line at a time
pub fn bytes() -> ByteStream throws        // chunks as they arrive

A step of lines can fail, and the failure leaves the function. Nothing marks the loop. The compiler requires the enclosing function to declare throws:

use std::io

fn tally() -> i64 throws {          // NK2701 without the `throws`
    let mut n = 0
    for line in io::lines() { n += 1 }
    return n
}

A failed read is never indistinguishable from the end of the input. Part I 6.4 refuses that at the closing brace of a block; this is the same refusal at the top of a loop.

The surface is std::fs’s shape minus what a stream cannot keep. A read looks blocking and is not: no async on the signature, no await at the call. A for over lines() is the same: each step may pause, nothing in the loop says so, and the thread is given up between lines. On a single-threaded runtime the event loop runs another task while the pipe is empty; with threads the read may resume on a different one. A sync function cannot call it (Part II, 12.1), so a par_iter body cannot wait on a pipe.

lines() yields owned text, where a file’s lines are views into the mapping they came from (fs::map(path, root) and .lines(), below). An iterator may hand out views into a buffer it does not own, and never into one it does.

There is one standard input, so these are functions rather than a handle. Reading it a second time yields nothing.

Provenance follows the rule files follow: standard input is Untrusted. A program that knows who writes it reads it with io::read_to_string(; trusted: true) (ADR-365).

Writing output

println(text) writes a line to standard output, print(text) writes without the newline, and eprintln / eprint are the same two on standard error. They are in the prelude rather than in a module.

The argument is an ordinary interpolated string (Part I, 2.5), so a hole is written where the value goes and {{ is a literal brace:

print(f"{name}: ")
println(f"{count} rows")

print is for output composed piece by piece, where a newline after every fragment would be wrong.

std::time — a span of time

A span is made by a method on an integer and read back by its mirror on the span (ADR-150 D2, D5):

use std::time

fn main() {
    let timeout = 90.seconds()          // also millis, micros, minutes, hours
    time::sleep(timeout)
    println(f"{timeout.in_minutes()}")  // 1: whole units, cut off
}

in_hours, in_minutes, in_seconds, in_millis, in_micros and in_nanos answer an i64; a span longer than an i64 counts reads as i64::MAX, as a count too large to make a span saturates. time::sleep pauses, and gives the thread up while it does.

http — a package, not a module of std An HTTP/1.1 server: GET and POST, bodies by Content-Length, connections kept alive between requests. Chunked bodies, TLS, HTTP/2 and a client are not built. http is not part of std: it is a package reached by path, http = { path = "../http" }.

http::listen stands on net::serve: each connection is a task, on one thread at user_parallelism = no and on the pool at yes. A panic in a handler ends its connection with 500 where the response has not begun, and the server goes on.

use http

fn main() throws {
    // Starts a server on 127.0.0.1:8080.
    // The code looks the same, but the runtime behavior follows `user_parallelism`.
    // The handler is a trailing lambda, outside the parentheses. There is one,
    // and it looks at the path and decides.
    http::listen("127.0.0.1:8080") fn(request) {
        if request.path() == "/" {
            return http::Response::text("Hello World")
        }
        let who = request.query("name") ?? "world"
        return http::Response::text(f"Hello, {who}")
    }
}

The handler and the request. A handler is a lambda, so its arguments follow Part I 5.3: the first and only one is the request. It returns an http::Response, a value with named fields built where it is returned: http::Response { status: 400, content_type: "text/plain", body: "id is required" }. http::Response::text(body) is a 200 in plain text, and http::Response::not_found() a 404. The limits are options after the ; with defaults, and a program names only what it changes: body_cap, head_cap, head_timeout, body_bytes_per_second, idle_timeout and connections (ADR-289 D13, ADR-326 D6-D9).

Timers. The whole head of a request arrives within head_timeout (10 s), counted from the accept for a connection’s first request and from the first byte for a later one. A body keeps body_bytes_per_second (500) on average since its first byte, after a start-up period. Past either the server answers 408 and closes. Between requests a connection waits idle_timeout (75 s) and then closes; under load the server may end a connection early, only by saying Connection: close on its next response. A connection handed to another protocol, a WebSocket after its upgrade, is that protocol’s. examples/hello-http/ is a server built this way.

Decided, not built yet (ADR-289 D14, D17-D19, D22-D29): what follows, to the end of this module’s description, except the last paragraph on the request’s views. A server is http::Server over a tree of routes, a handler per method and path, and a handler that needs nothing names nothing:

comptime ROUTES = http::Routes()
    .get("/")            fn { "Hello World" }                   // names none, takes none
    .get("/hello?name")  fn(name: String = "world") { "Hello, " + name }
    .get("/fortunes")    fn(request: http::Request) { render(request) }

fn main() throws {
    http::Server(ROUTES).listen("127.0.0.1:8080")
}

What a handler returns is what answers the request:

returns becomes
String 200, text/plain; charset=utf-8
html::Raw 200, text/html; charset=utf-8
Bytes 200, application/octet-stream
Response itself
T throws the value on success; on failure 500 with a generic body, the error logged

A handler gets only what its signature declares (ADR-332). The method is the call - .get, .post, .put, .patch, .delete, and .route(methods, path) for several - and the path, a comptime parameter (fn get[F: Fn](self, comptime path: String, handler: F), Part I 4.6), names the values it carries; a path that does not read is refused at the string in the call:

In the path Means
{id} a whole segment
{year}.pdf part of a segment
{path...} the rest of the path, last; its value without the leading /; /files/ matches with ""
?expand a query value named as the parameter
?page-size={page_size} a query value whose name on the wire differs

A parameter of that name gives the type and, with a default, makes the value optional; a value that does not convert answers 400. A name the path gives no parameter, and a plain parameter the path does not name, are refused while the program is built. The raw path is split at / before each segment is decoded; a . or .. segment or a %2F in a rest answers 400, and nothing is normalised. A literal segment wins over a partial one, a partial one over {name}, {name} over {name...}; two routes as specific as each other are refused while the program is built, whatever their parameters’ types. There are no optional segments.

Every other input is a type implementing http::Extract, whose extract declares its own inputs as typed parameters:

impl http::Extract for Session {
    fn extract(cookie: Cookie["session"]) -> Session throws http::Reject {
        return sessions::load(cookie.value) ?? throw http::Reject(401)
    }
}

comptime ORDERS = http::Routes()
    .get("/orders/{id}?expand") fn(id: i64, expand: bool = false, session: Session) -> Order { … }
    .post("/orders")            fn(data: Body[NewOrder], key: Header["X-Api-Key"]) -> Order { … data.value … }
    .get("/files/{path...}")    fn(path: fs::Path, agent: Header[http::USER_AGENT]?) -> http::File { … }

Header[name] and Cookie[name] take the name on the wire as a value parameter (Part I 4.6); http declares the standard names as constants, and a name not of a header’s form is refused while the program is built. Only http’s own extractors read the raw request; a failed one answers its Reject’s status and the handler does not run. Body[T] names no format: Content-Type chooses the one a body is read in and Accept the one a result is written in, among the server’s formats, and another answers 415. A format that cannot express T is refused while the program is built. A wrapper is read with .value. An input no parameter declares is not reachable; a handler that needs the raw request declares request: http::Request. The path, every parameter and every extractor’s inputs are read while the program is built, through F::params (Part II 10.3), and an API description is made from them.

A tree of routes is a comptime value (ADR-334). Handlers capture nothing; shared state is the extractor State[T], filled from what the server is given:

pub comptime ROUTES = http::Routes()
    .get("/{id}") fn(id: i64, db: State[Db]) -> Order { … }

comptime APP = http::Routes()
    .mount("/api/v1/orders", orders::ROUTES)
    .mount("/admin", admin::ROUTES; formats: [json::Format])

http::Server(APP; formats: [json::Format, form::Format], state: [db]).listen(":8080")

Trees are built from others across files and packages, under conditions the build decides; a group’s formats replace the server’s below it. state holds one value per type; a State[T] nothing is given for, and two values of one type, are refused while the program is built. The whole tree is checked then - conflicts, formats, state - its API description is a constant, and its matcher is built from it.

Work around routes is a layer (ADR-335): a value declared on a tree, .layer(http::Compress()), whose kind implements http::Layer with any of three phases. before(…typed inputs…) -> R throws Reject runs before the handler and may refuse or answer itself; after(r: R, response) -> Response changes the response; observe(exchange) reads method, path, status, time and sizes after the response is sent. The handler runs at most once, and only the runtime starts or cancels it: no layer calls, skips or repeats it. befores run in written order, at once only where neither depends on the other’s result and their effects stand whichever refuses. afters run one by one, innermost first, and an error response passes through them too; a failing after either lets the response pass or turns it into a 500, as its layer declares, and after a stream’s first byte a failure ends the connection. observe cannot change a response; what waits for it is bounded, and past the bound an observation is dropped and counted. A timeout, a body’s size limit and a panic’s 500 are std’s layers. An outer tree’s layers wrap an inner one’s. Two afters writing one header, and a layer whose inputs a route cannot give, are refused while the program is built.

A status code, a header or a body of the handler’s own is a Response, built where it is returned: http::Response { status: 400, body: "id is required" }, with headers a field like the others.

A body need not be bytes the program allocated. Bytes is the shared buffer of Part I 6.6 and Mapped derefs to it, so a page mapped once, outside the handler and handed to the server as state, is a body that costs a reference count per request. The handler answering with it duplicates the handle rather than moving it:

use std::fs
use http

fn main() throws {
    let page = fs::map("index.html", fs::Root::Dir("site"))
    http::Server(ROUTES; state: [page]).listen("127.0.0.1:8080")
}

comptime ROUTES = http::Routes()
    .get("/") fn(page: State[fs::Mapped]) { page.value }

A response may be a file the program never read: http::File("index.html", fs::Root::Dir("site")) is a body whose bytes go from the page cache to the socket without entering the process. Its Content-Type follows the extension. Its length, and any failure to open it, are settled before the status line. Whether the transfer is sendfile(2), a mapping or an ordinary read is the library’s choice at run time. http::File is unavailable under TLS and under HTTP/2.

When the request names the file, the name and its root arrive together. A download route:

// The request chose this name; the call says which directory it may not leave.
http::File(request.query("file") ?? "", fs::Root::Dir(store))

Every std function that takes a path takes its root right after it, with no default: http::File like fs::map, fs::read and fs::write. The root is an fs::Root: Dir(store), under which the joined name is resolved and compared component by component, or Anywhere, which performs no check and is listed per site by --trust (on nikaia build and nikaia lower). A name that leaves its Dir is io::IoError::Outside, and the handler answers 404. The call refuses; it does not rewrite. Nothing is inferred about where the name came from; a ../../etc/shadow is stopped at the call, before the headers are written. Whether fs::map trusts the file’s content is a different question.

What the library keeps between requests is bounded, dropped when the file’s identity or modification time changes, and sized by the operator rather than the program. A page that must be held for certain is mapped by the program itself, outside the handler, as in the mapped-page example above.

The request’s strings are views into the bytes the connection read: path(), header(name) and query(name) yield a String that is a view, so a parameter used inside the request’s scope costs nothing and one kept past it has to be owned (Part I, 6.6). query and header return the nullable type of Part I 3.5 rather than an empty string, and method() returns an enum rather than a string.

A handler does I/O, so it is not sync. It carries no async marker and no await; the build option chooses the executor and nothing else.

html (an official package, 17.3)

HTML escaping, on which a template’s contract rests.

pub fn escape(text: String) -> String            // for a text node or a quoted attribute
pub struct Raw                             // "this is already markup"
impl Raw { pub fn(markup: String) -> Raw } // html::Raw(markup): the audit point, and the only constructor

A template grammar escapes every hole, unconditionally. No flag at a hole turns it off, and trusted provenance exempts nothing. The one way to say a value is already markup is to give it the type Raw, so the decision is made where the value is built rather than where it is used.

escape handles the five characters that change what HTML means in a text node or a quoted attribute value, &, <, >, " and ', and returns its input unchanged when none of them is present. It does not make text safe inside <script>, inside CSS, in an unquoted attribute or in a URL. A hole in one of those positions is a compile error naming the position.

The template, and where it is compiled. dsl html { … } eod is compiled where it is written: the body is split into literal markup and holes at compile time, and the output is plain string building. The escaping is a compile-time property.

fn row(name: String, shade: String) -> String {
    return dsl html {
        <tr class="{shade}"><td>{name}</td></tr>
    } eod
}

{{ is a literal brace, the same rule an interpolated string follows. The framing whitespace — the newline after { and the indentation before } eod — is not markup and is removed; whitespace inside the body is kept exactly.

What may go in a hole is decided by the type, through the Render trait: a Raw renders itself, text renders escaped, and a type with no impl cannot be placed in a template. The compiler emits the same call for every hole; the type chooses. The rule holds on every hole, including one whose type the checker does not know.

Control flow is written as an element:

<table>
<for row in :rows><tr><td>{row.id}</td><td>{row.message}</td></tr></for>
</table>

:rows carries the colon because it is captured from the enclosing scope: the colon is where the template’s names end and the program’s begin. The loop runs over the captured collection and borrows rather than copies. The position check runs through a loop’s body; a hole in a <script> is refused inside a loop too.

std::fs (Compiler Magic) File system access looks blocking. The compiler transforms each call into a non-blocking state machine backed by the runtime’s reactor. User code never blocks the thread and never writes a callback.

Every function below may fail for environmental reasons, so every one of them throws (Appendix A.1). What they throw is io::IoError, with NotFound, PermissionDenied, NotText, Outside — where a name would leave the fs::Root it was given — and Other. A handler that only passes the failure on names nothing; one that takes it apart writes use std::io and io::IoError::NotFound(p). None of them takes an async marker, and none is awaited.

Whole-file access

// Subject: the path, and the root it may not leave ; Config: options
pub fn read(path: Path, root: Root) -> Bytes throws                  // whole file, as bytes
pub fn read_to_string(path: Path, root: Root) -> String throws       // whole file, UTF-8 validated
pub fn walk(path: Path, root: Root) -> Vec[Path] throws             // every file under a directory
pub fn canonical(path: Path, root: Root) -> Path throws         // the absolute name, links and . and .. resolved
pub fn write(path: Path, root: Root, data: Array[u8]; append: bool = false, create: bool = true) throws

A path is an fs::Path (ADR-319): a file name in the platform’s own encoding — the bytes as they are on Unix, WTF-8 on Windows, UTF-8 where names are Unicode. Text stands wherever a Path is asked, as a view without a copy, so a literal or a String is a path. A Path is made from text, by the operating system (walk, read_dir, a program’s arguments, the environment) or by the operations on one: == against a path or text, starts_with, ends_with, file_name, extension, with_extension, parent, join, strip_prefix and parts, each handing back a Path. Paths have an order, so a Path is a key of an ordered map or set (BTreeSet[fs::Path], BTreeMap[(fs::Path?, i64), T]) and of a hash map: whole parts are compared one after the other, each by its bytes, which is the order == agrees with (ADR-319 D9). p.strip_prefix(base) is the rest of p after the whole parts of base, or null where they do not lead it; it reads no file system. p.parts() is the Vec[Path] of the whole parts in order, the root first where there is one, .. as written and . only where it leads; joined again they make a name == to p, and it reads no file system either (ADR-319 D10). fs::canonical(path, root) is the absolute name with every link, . and .. resolved; it throws NotFound for a name that does not exist and, under Dir(store), Outside where the resolved name leaves the store. There is no constructor from arbitrary bytes, so no call fails for a name’s encoding. An f"…" builds a Path where its use asks for one (Part I 2.5). p.to_text() gives the String; it throws io::IoError::NotText for a path whose source is the operating system, on every target, and never for one made from text. p.display() gives text for showing, with � for what is not text, and never fails. NotFound, PermissionDenied and Outside carry the name as a Path, Other carries a message, and Root::Dir holds a Path.

Every path names its root. root is an fs::Root. Dir(store) resolves the name under that directory and throws io::IoError::Outside where it would leave it; Outside is a case of io::IoError, not an error type of its own. Anywhere performs no check. --trust (on nikaia build and nikaia lower) lists every site that writes Anywhere or Dir("/"). There is no default and no exception for a literal: a relative name is resolved against the working directory. A call that leaves the root out is refused with NK1101, whose help names both forms. fs::map(path, fs::Root::Anywhere) is the form for a command-line program whose path the operator typed.

A directory of one’s own. pub fn scratch() -> Root throws makes a fresh, empty directory and hands it back as Dir, so what is written under it is checked to stay there (ADR-247 D5). Under nikaia test it is inside the test’s own directory and is removed with it (14.1); elsewhere it is a new directory under the system’s temporary directory.

A directory walk. walk(path, root) hands back every file under the directory path, as names relative to it with / between the parts, sorted, so two runs over one tree agree (ADR-290 D14). Directories are not listed, and each is visited once, so a link back up the tree ends the walk. Under Dir(store) the root holds for every name the walk finds: an entry that leads out of it, a symlink pointing away, is left out rather than failing the walk. It throws where the directory itself cannot be read; a name that is not text is handed back like any other. A name it hands back opens under the same root: fs::read_to_string(name, root) after fs::walk(".", root).

The reactor. read, read_to_string and write go through the runtime’s reactor. Where the machine has a completion queue, the kernel performs the operation and reports when it is done; otherwise the runtime’s own I/O thread performs it. Which one serves is decided when the program starts, never when it is compiled, and an operator may pin it (13.3b). The reactor runs before the program’s first statement, so an operation costs no thread start and no thread wake-up. map is not on the reactor: it hands back pages the operating system owns. A read is a slot the caller polls rather than a call that blocks its thread, and the executor runs something else while it is in flight. Two reads are put in flight together by async (Part I 8.1.2), never by the compiler.

read returns Bytes, not a Vec[u8]: one shared buffer, and slices that outlive its scope are tethered to it (Part I 6.6). A parser can therefore hand back thousands of names that all point into a single allocation.

Bytes is a language type, written bare, and is one reference-counted buffer over memory it allocated, a Vec[u8] handed over (Bytes(v), no copy), or a mapping. A tethered slice keeps its buffer alive in whatever keeps the slice; nothing is written for it.

Reading a large file: map, and the grammar

There is no fs::lines and no fs::bytes. A program maps the file and walks the lines of its text. fs::map(path, root) owns the pages, .text() checks them once, and .lines() borrows views of them: tethered String views, no allocation per line, constant memory.

let data = fs::map(path, fs::Root::Anywhere)
for line in data.text().lines() { … }

A file that is a record per line is read with the grammar protocol: @frame(boundary: "\n") says so, and the grammar drives itself over the pages, in parallel where user_parallelism allows (Part II, 10.7).

map is a compile error on wasm32-*.

Handles

pub fn open(path: Path, root: Root; write: bool = false, append: bool = false,
            create: bool = false, truncate: bool = false) -> File throws

File implements Cleanup (Part I, 6.4): the compiler flushes and closes it at the end of the scope, on the normal path and while an error is bubbling up, and a flush that fails surfaces as an error. A program calls close() explicitly where it handles that error at a precise point.

impl File {
    pub fn read(mut self, mut into: Array[u8]) -> i64 throws
    pub fn write(mut self, data: Array[u8]) -> i64 throws
    pub fn flush(mut self) throws
    pub fn seek(mut self, to: Seek) -> i64 throws   // Seek::Start(n) | Current(n) | End(n)
    pub fn len(self) -> i64 throws
    pub fn close(self) throws                        // explicit opt-in; otherwise Cleanup does it
}

Memory mapping

pub fn map(path: Path, root: Root) -> Mapped throws     // read-only memory map

Mapped derefs to Bytes, so a mapped file is a tethered buffer like any other: it may be given wherever a Bytes is taken, read or kept, at a count, and the file stays mapped while any holder lives. The pages are the buffer, nothing is copied, and fs::map checks nothing. m.text() is the mapping as text: the first call checks UTF-8 over the whole of it and throws io::IoError::NotText with the earliest bad byte; later calls hand back the same view without checking again. A cut, m[a..<b].text(), checks only that cut. A grammar run over a mapping checks the text it reads, and a byte that is not UTF-8 is an error at its position (ADR-016 D5).

Retention. A slice that escapes the mapping’s scope tethers to it, and a tether keeps the whole map alive. The compiler warns where a small extract outlives a large buffer and suggests .clone() (ADR-283 D6). The mapping is released once the last tether is gone, which may be later than the end of the block that created it. Slices that never leave that scope cost nothing and hold nothing. At process exit a read-only mapping with nothing observable attached to it is left to the operating system rather than unmapped page by page.

Availability is a property of the target, and of nothing else. fs::map is available at every value of every build option on any target whose platform provides memory mapping: a single-threaded program compiled for Linux, macOS or Windows maps files exactly like a parallel one. On wasm32-* fs::map is a compile-time error. What std::fs offers on wasm32-* in place of fs::map is decided with that target (17.2).

Metadata and directories

pub fn exists(path: Path, root: Root) -> bool throws
pub fn metadata(path: Path, root: Root) -> Metadata throws   // len, is_dir, is_file, modified, links, file_id
pub fn read_dir(path: Path, root: Root) -> DirEntries throws
pub fn create_dir(path: Path, root: Root; recursive: bool = false) throws
pub fn remove(path: Path, root: Root; recursive: bool = false) throws
pub fn rename(from: Path, to: Path, root: Root) throws       // both names under one root
pub fn copy(from: Path, to: Path, root: Root) -> u64 throws

m.modified() is the last modification as a time::Duration since the Unix epoch, on the wall clock time::since_epoch() reads, and zero where the platform does not say; m.links() is the number of hard links, 1 off Unix; m.file_id() is the device and inode as (u64, u64)?, the same for two names of one file, and null off Unix (ADR-319, #922).

Availability by target

Every value of every build option has the same std::fs surface; only the target changes it.

API Native wasm32-*
read, read_to_string, write yes yes — backed by OPFS
open yes yes — backed by OPFS
map yes compile error — the platform has no memory mapping
metadata, read_dir, create_dir, remove, rename, copy yes yes — OPFS, within the origin’s sandbox

std::thread (17.2) is barred by user_parallelism = no, so manual threading is a compile error even on a native target that has threads. fs::map is barred only by the target.

std::collections — and where keys come from

The ordered and the hashed collections offer the same entries (ADR-collections-1). BTreeMap has what HashMap has apart from hashing, and BTreeSet what HashSet has: m.entry(k) with or_insert, or_insert_with, or_default and and_modify on both maps, and s.extend(items) on both sets, as on Vec. or_default() is or_insert_with(fn { V() }), for a V made with no arguments: a collection, String, a number, bool, or a struct every field of which has a default; another V is NK1102 (ADR-384 D1). extend takes a list, a set or a sequence of owned elements, and keeps them; s.extend(xs.clone()) copies the elements, never a list in between. Only what depends on order (first, last) is the ordered kind’s alone.

A set is walked as a list is (ADR-collections-2 D3): s.iter() lends the elements one at a time, the sequence Vec::iter() is, so any, all, filter, map, count and collect follow. A BTreeSet hands them back smallest first and from either end (rev); a HashSet in no order, as HashMap::keys does, so a program that prints them says which order it means.

Every input carries a provenance, because the compiler knows where a buffer came from (Part I 6.6):

A value inherits the provenance of the buffer it comes from, and a collection takes the most cautious provenance of everything put into it. Where the compiler cannot tell, across a dynamic call or from a foreign library, the answer is Untrusted.

The hasher follows from the provenance: untrusted keys get a keyed hash with a per-process random seed, and trusted keys get a fast one. Within that, the keys’ shape picks the function: a fixed-width type, text of a known length, or text of unknown length. A program may name its own with hasher: where it makes the map, and --trust lists the choice for every map (ADR-316). Nothing else about the map changes: same table, same API, and keys are always compared in full.

One map, one hasher, decided for the whole package (ADR-010 D9). Maps that a value passes between - a field and the map it is initialised from, a parameter and its argument, a result and what receives it, two maps compared with ==, the arms of one if or match - are hashed the same way, and get the keyed hash if any key that reaches any of them is untrusted. The compiler decides it after reading every file of the package: which file builds or fills a map, and the order the files are read in, change nothing. A map whose declaration is not part of a pub item’s signature or type has one hasher at every use of that declaration.

At the package’s boundary, each use chooses, as with a generic. A map in the signature of a pub function or method, or in a pub type, takes the hasher of the map handed in or taken out at each use, in the package and in its callers; a function has one hasher for each group of its positions that its body makes one map, so two maps it only reads from one another may be hashed differently. The package’s ledger says what each such function puts into those maps (13.5, maps), and a caller counts it with its own keys. A map in a trait method’s signature, in a described crate’s signature or in a binding for another language always gets the keyed hash. So does a map a pub function or method hands on to one of those, or to a private function with a map of its own, and the maps of a pub type one of whose methods hands a map of self on to one. Rust code that names a pub Nikaia type holding maps gives one type argument per map, in the order its fields declare them, nikaia_std::hash::Fast or nikaia_std::hash::Keyed; one it leaves out is Keyed.

Two maps that must be hashed the same way but are made with two different hasher: choices are refused with NK1246.

User code has the last word, at the place the data enters:

// A benchmark reading a file it generated itself.
let data = fs::map(path, fs::Root::Anywhere; trusted: true)

trusted: true says the program knows who wrote the bytes; trusted: false makes a source that is trusted by default untrusted. Both are recorded in the ledger. A grammar for a wire format can pin the floor for everyone who uses it, @untrusted grammar HttpHeaders, so that no application can lower it (ADR-010 D3-D4).

--trust (on nikaia build and nikaia lower) prints where the program’s bytes came from, which source said so, and which hasher its maps got:

$ nikaia lower 1brc.nika --trust
input provenance: trusted
    cli::args is trusted
    fs::map is trusted: `trusted: true` at 1brc.nika:7
hash for a map keyed by the input: fast, fixed seed - no adversary chooses these keys

An untrusted map is seeded randomly, so its iteration order is not stable between runs. A program that needs an order asks for it explicitly.

Other key modules:

17.2. Availability by Target and by user_parallelism

Some modules are available, or behave restrictively, depending on the target and on whether user code may run concurrently.

A target without an operating system is one more column of this section. user_parallelism is no on it. fs, net, process, threads and memory mapping do not exist on it, and neither does the http package, which is built on net. Everything the language itself is carries over: async, a free task as a coroutine, the four doors, Cleanup, Seen, grammars, comptime and Chapter 16’s assembly. The emitted Rust is no_std, the executor is the target’s with interrupts as wakers, an interrupt handler is a fn() sync that touches no lock, a lock is a critical section the length of its block, and a build may forbid allocation after start.

At no the runtime starts its I/O workers and nothing else, so no thread carries user code; at yes a pool for user code starts with it, sized by user-pool (13.3b). At no a task interleaves in the executor, and no user code runs concurrently; at yes a task runs on a thread of the user-pool pool.

Interleaved is not concurrent.

db (an official package, 17.3: the protocol, and nothing else) db holds what two database drivers must agree on without depending on one another: the Connection and Transaction traits, the Statement protocol a dsl block’s prepared statement speaks, and the values a row may carry: the language’s numbers, bool, String, Bytes, and T? for NULL. No SQL, no grammar, no dialect: the compiler knows none. A dialect is a grammar in a driver package (sqlite, postgres, a vendor’s own), which also brings the DDL grammar for the schema, the connection and the target adapter.

use sqlite                                    // a driver package, not `std`

comptime APP = asset("schema.sql")            // the schema, read while building

fn query_data() {
    // Transparently starts the required sidecar (thread or worker). The
    // connection is typed by the schema it was opened for (ADR-299), so a
    // statement checked against another schema is refused at `execute`.
    let db = sqlite::open("app.db"; schema: APP)

    // The driver's grammar checks the statement against the schema while
    // the program is built, and declares the columns; the row has fields.
    let active_users = dsl sqlite::Sql(schema: APP) {
        SELECT name, last_login FROM users WHERE last_login > :since
    } eod

    for u in active_users.execute(db; since: 0) {
        println(u.name)
    }
}

17.3. Official Packages

json, toml, csv, html, http1 and db are official packages: maintained with the toolchain and shipped with it, each with a version of its own, and published as every package is (nikaia_json, 13.3). std lists them with the version this toolchain ships. A use of one that neither [dependencies] nor a directory of the project names takes it in at that version and records it in nikaia.lock; a [dependencies] entry names another version. json, toml and csv each read a text into values and write values into a text. A program carries only what it calls, whether it is in std or in a package.

An official package’s source is packages/<name>/ in the toolchain’s repository, with a version of its own.

json. json::read[T](text) reads a text into a T and throws json::Error where it fails; json::write[T](value) writes a T as text, fields in declared order. json::Error has the form of a grammar’s ParseError (Appendix C): the line and the column, and the stack of what was being read there, its object members and list elements written as a path ($.contacts[3].email). json::read[T] forwards to the entry Json::read[T] of the package’s pub grammar Json, which the compiler emits once per T and which fills each struct with members[S] (Part II 10.8, ADR-grammar-2); json::write[T] is generated from T::fields while the program is built (Part II 10.3). A member matches the field of its name, or the name @json::Name gives; never by position. A member given twice is an error where the text is read; a member T has no field for is skipped. A field with no member takes its default if it has one (Part I), is null if its type is a T?, and is otherwise an error where the text is read. A member that is null goes into a T?; for any other field it takes the field’s default if it has one, and is otherwise an error. A field’s type is bool, an integer or float type, String, a declared struct, an enum whose variants carry nothing (written as the variant’s name), or a T?, Vec[T] or Map[String, T] of one; any other is NK1250, a type with a text form of its own (json::Value, time::Instant) and a variant that carries a payload among them.

For JSON whose shape no struct declares, json::parse(text) reads into a json::Value and throws json::Error as read[T] does. A number in a Value is kept as its text and converted when it is asked for as a type (as_i64, as_u64, as_f64); the members of an object keep their order.

comptime SCHEMA = asset("contact.schema.json")
struct Contact { name: String, email: String? }
let c = json::read[Contact](text; schema: SCHEMA)

A schema: is a JSON Schema read while the program is built; T is checked against it by the same rules and a mismatch is NK1251.

Appendix A: Error Hierarchy

Nikaia distinguishes between errors caused by the environment, which are recoverable, and bugs in the program logic, which are not.

A.1. Recoverable Errors (throws)

Errors arising from external circumstances, such as a missing file or a network timeout.

A.2. Unrecoverable Errors (panic)

Errors indicating an inconsistent program state: an index out of bounds on a list (a map read through the brackets is a T? and never panics); division by zero; arithmetic overflow; a handle a C declaration claimed and C did not hand back (15.1); and an explicit panic().

An overflow is in this list at every build. In a chain whose lambdas touch nothing, it may stop the chain after its last element instead of at its own, and still names its own line (Part I 4.5). Where a program means to wrap or to stop at the limit, it says so by name (Part I, 2.2). A conversion is not in the list: one that can lose a value is written as only where it is shown to fit (NK1241 otherwise), and checked_i32 and truncating_i32 are how a program asks for the rest (Part I, 2.2).

A constant that cannot fit the type it is given is refused with NK1116, and a division whose divisor is a constant zero is refused with NK1118. Neither takes a case out of the list: a divisor the compiler cannot evaluate is divided by at run time, and a zero there is unrecoverable. The compile-time refusal replaces the run-time message only where no program had to run to know it (C.1).

A panic depends on where it happens and on the target:

Where Panic Behavior Consequence
a task The task ends At both values of user_parallelism (ADR-326 D4). Its cleanups run, and the program goes on. A value a lock held for it is poisoned and never read (Part I 6.3).
main The program ends The stack unwinds and the cleanups run.

How the program ends. main ends by returning, by an error that leaves it, or by a panic. An error that leaves it is process::Exit(code) (17.1) or another error, which is exit status 1 (Part I 7.1). Returning and an error take one path: the values main and every frame below it hold die in order and their cleanups run (Part I 6.4); the tasks nobody joined run to their end and the parked cleanups run, both bounded by cleanup-deadline; then the process ends, with 0 after a return, code after Exit and 1 after another error. Before main runs, a word that does not fit its parameters or breaks one of main’s preconditions ends the program with exit status 2, one line on standard error and the short usage; nothing of the body has run and no cleanup is owed (Part I 5.5). Built with skip-free-at-exit:on (13.3), the values that die after main’s last statement are not freed; they still die in order and their cleanups run, and nothing else on this path changes (ADR-348). The panic hook does not run for an error. A task does not end the program: an Exit that arrives in one ends the task and goes to whoever joins it (Part I 8.2). A detached task’s error is printed on standard error in the long form; if it is fatal, its code replaces the status main ends with, after main has ended and before the drain, the first such error counting. The drain and cleanup-deadline are unchanged (ADR-346 D6).

One end that is not a panic and is not success either. A cleanup-deadline that expires ends the program with exit status 70 (EX_SOFTWARE) and a message naming every resource whose cleanup was cut off, delivered on the panic path: standard error and the panic hook. No build option and no runtime configuration turns that into a 0. cleanup-deadline = "0" does not drain and therefore never expires.

The target decides independently: on wasm32-unknown a panic is a trap and the module is done, whatever user_parallelism says. A build with artifact = "c-library" unwinds instead (15.1): every entry point catches the panic and returns E_PANICKED, and the library is poisoned until shutdown and init have run.

The third build option changes nothing on this page. reentrancy-check (13.3) decides whether a compiled program notices a lock taken while a lock is held. Taking one is refused at build time, so in a program the compiler accepted the check cannot fire; if it fires, the refusal has a hole. The re-entrancy panic Part II 12.2 describes at user_parallelism = no is that check, so the table above has no row for it.

On every panic path, including the abort and the WASM trap, the application’s panic hook runs first (Part I, 7.2): one global sync handler receiving message, location and stack trace, for crash dumps and reports. It runs before aborting even under panic = abort.

The abort names the .nika line. Every program carries a table of generated line to Nikaia file and line, and the hook looks the site up before it prints anything. An overflow, an index out of bounds and a written panic() all read src/main.nika:2: the program stopped: attempt to multiply with overflow, and never name a generated file. In a task the sentence is a task stopped:, because the program goes on (ADR-326 D4). A location the table does not know, such as a panic inside std’s own Rust or a foreign crate’s, is left in the words of whoever wrote it.

Appendix B: Compiler Internals & Annotations

To enforce the contextual capture rules (Part I 5.4) without hard-coding function names into the compiler, Nikaia uses internal attributes. They belong to the standard library.

@detached is a ledger fact and not a word a program writes: whether a function-typed parameter is run or kept is inferred from the body (Part I, 5.4 C).

B.1. Capture Attributes

Attribute Internal Name Default Description
None capture_mode = "immediate" Yes The lambda executes within the caller’s stack frame. Captured variables are Borrowed (views, Part I 6.5). Used by map, filter, lock.access.
@detached capture_mode = "detached" No The lambda escapes the current stack frame (stored, spawned, or deferred). Captured variables are Moved (Owned). Used by async(detached), defer.

B.2. Standard Library Signatures

Common standard library functions are annotated internally as follows:

// std::collections::List
// Standard immediate execution
pub fn map[U](self, op: fn(T) -> U) -> Vec[U]

// std::task (tasks, Part I 8.1.2, 8.2; ADR-async-5)
// `async e`, `async(handle)`, `async(deferred)`, `async(detached)` are the language's;
// A child handle borrows from its group: no `Send`, no heap; it cannot leave the group (NK2122)
pub fn ChildHandle[T].join(self) -> T throws E | Crashed | OverBudget
// `join(within:)` limits this wait: on `TimedOut` the task runs on and the handle is still live (Part I 8.2);
// `on_timeout: task::OnTimeout::Cancel` cancels the task then and takes the handle
pub fn ChildHandle[T].join(self; within: time::Duration, on_timeout: OnTimeout = OnTimeout::Keep) -> T throws E | Crashed | OverBudget | TimedOut
pub fn ChildHandle[T].cancel(self)      // the one way to cancel a task; no fallback runs
pub fn ChildHandle[T].start(mut self) // a deferred handle only; exactly once on every path (NK2121)
// A free task's handle, `async(detached)`: takes its captures, may outlive the group
pub fn TaskHandle[T].join(self) -> T throws E | Crashed | OverBudget
pub fn TaskHandle[T].join(self; within: time::Duration, on_timeout: OnTimeout = OnTimeout::Keep) -> T throws E | Crashed | OverBudget | TimedOut
pub fn TaskHandle[T].detach(self)      // nobody waits; errors go to the fallback, else the log (Part I 8.2)
pub fn TaskHandle[T].cancel(self)
pub fn TaskHandle[T].start(mut self) // `async(detached, deferred)` only
// `spawn(task: @detached fn() -> T throws E) -> TaskHandle[T]` stays until the move is built
// What a `join(within:)` does with the task when its limit runs out
pub enum OnTimeout { Keep, Cancel }
// A supervisor does not restart a fatal error; it ends and hands it on.
// A full memory block ends a task with this error (Part II, Chapter 12)
pub struct OverBudget
// Who decides when the next task starts; `std` provides the default
pub trait Admission { fn decide(mut self, load: Load) -> Decision sync }

Appendix C: The Diagnostics Contract

Nikaia compiles through the Rust toolchain. The backend’s error messages, about lifetimes, borrow traits and generated code, never reach a Nikaia program’s author. Diagnostic quality is a testable requirement.

C.1. The Iron Rule

An untranslated backend (rustc) error reaching the user is a Nikaia compiler bug.

The compiler reads every backend diagnostic from rustc --error-format=json and places it on the .nika span that produced it (ADR-300 D1, D7). Each borrow, ownership and lifetime error class is mapped to a Nikaia diagnostic with Nikaia vocabulary, .nika spans and a concrete fix-it. An unmapped error is reported as an internal error, never as normal output. The error catalogue below is also a test suite: every entry has a minimal .nika reproduction that must produce the documented message.

C.2. Requirements for Every Diagnostic

  1. No prior knowledge assumed. The message is understandable without Rust or systems-programming background. The terms “lifetime” and “borrow checker” and Rust error codes never appear.
  2. Always say what to do next. Every error names at least one concrete way out (clone, use Shared, use retain, mark a function sync, move the I/O out of the lock, …), as paste-ready code where possible.
  3. Narrate cause chains. An error caused by a change (through the ledger, 13.5) shows both sides: the edit that changed the contract and the caller that broke.
  4. Positive guarantees over prohibitions. Where the language removes a danger structurally (tethered slices, scope waiting), the documentation and the messages state the guarantee, such as the buffer cannot die while a token lives, not the forbidden thing.

  5. Spoken to the reader, in plain sentences, at the places it is about. A message says what you wrote, why it cannot work, and what to write instead, in the words a colleague would use: You’re changing count, but it wasn’t declared as mutable. Not count is changed, and a let that is changed says mut, which is correct and reads like a rule being recited. The source is shown at every place the explanation needs, each underlined whole and named: ^ under the place the error is, - under a place that explains it (declared here without mut). References to the specification and the decision records stay in the documentation, not in the message. Every message has one layout, whichever part of the compiler says it — a parse error, a checker finding, a refusal of the lowering, a relayed rustc message: the headline as a sentence, --> and the place, the source line with the place underlined, then = note: and = help:. A message with no code of its own (a parse error) is headed error: alone. A message that names no word of its own underlines its statement’s first line:

    error[NK1139]: You're changing `count`, but it wasn't declared as mutable.
  --> app.nika:4:9
   |
 2 |     let count = 0
   |         ----- declared here without `mut`
  ...
 4 |         count += n
   |         ^^^^^ changed here
   |
   = help: Add `mut` where it's declared: `let mut count`.

C.3. Error Code Catalogue (NK codes)

Range Domain Examples defined so far
NK1xxx Syntax & types NK1101 a call passes the wrong number of arguments. The same code refuses a lambda with a parameter for each part of the one tuple it is handed, filter(fn(name, ty) { … }) over (String, Ty) items; the help writes fn((name, ty)) { … } (ADR-358). NK1102 an argument is not what the parameter takes. The same code refuses a bound of comptime(steps: …, ram: …) that is not a number the build knows, and one that is not above 0, each in its own sentence (Part II, 10.2). NK1103 a let says one type and is given another. The same code refuses a ?? whose left side holds a type of the program’s own, a number, text, bool or char, and whose fallback is of another type, a number written out among them (Part I, 3.5); beside a number, an integer written out is not a float, a float written out is not an integer, and a number of another type goes in only where a let takes it (Part I, 2.4), and a catch whose block hands back a value of another type than the one it guards; the block’s type is the type it guards, or null, which widens that type to T? (Part I, 7.1). It also refuses a match arm whose pattern is of another type than the value, where both are certain: a literal of another kind than a value that is a number, text, a bool, a char or one of the program’s structs or enums, match 5 { "a" => … }, or a variant of another of the program’s enums (Part I, 3.4). A number against a char is not asked. NK1104 a return, or a body’s last expression, is not what was declared; an empty body hands back nothing. So does a body whose last expression is an if without else. A body whose last statement is a while true that no break leaves is not asked (ADR-276 D6). NK1105 an assignment is not what the target holds. NK1106 a struct literal gives a field the wrong type. NK1107 a field that is not there. On a row a dsl block’s grammar declared, a column two fields would share is no flat field, and the help names the qualified paths and AS (Part II, 10.5). NK1108 a condition that is not a bool. NK1109 a call names an option the callee does not have (Part I, 5.1), or a comptime(…) names a bound other than steps or ram (Part II, 10.2). The same code carries a dsl statement’s parameters handed to a callee that is not a driver, one declared with ...args: Self::dsl: nothing else has a place for them to arrive (Part II, 10.5). NK1110 a call reaches an item, or a field, another package keeps private (Part I, 9.2): secret is private to http, and http::Request.method is private to http for reading such a field and for giving one a value in a struct literal. A field’s pub is in the ledger. NK1101–NK1110 are answered from the ledger (13.5), so a call into a library is checked against the contracts the library ships. NK1111 (warning) a plain string holds what looks like a hole, or a doubled brace; the fix is f"…". NK1112 a call does not pass a parameter the DSL statement it is given declares; NK1113 a call names one that statement does not have (Part II, 10.5). Both are answered from the statement’s body, where a :name is written. NK1114 is retired and not reused; a body that reaches for a, b or c meets NK1117. NK1115 a call wants a shared value and is given a plain one (Part I, 6.2). The way out is an explicit wrap at the call, Shared(db), never an implicit one. NK1116 a constant does not fit the type it is given (Part I, 2.2): at an annotated let, a return against a declared result, an argument whose parameter says what it takes, a bare let where an operand’s declaration pins the type, a constant no type holds, a constant reached through a name, an operation over names whose type is pinned, wherever it stands - an f"…" hole, a condition, a list, a receiver - once, at the innermost operation that overflows, and a number its uses typed (Part I, 2.4) that is given one the type does not hold, with a note naming the use. The same code refuses a shift whose count is a constant below 0, or as large as the left side’s type is wide or larger (Part I, 2.2). A comptime whose value a use cannot hold is reported at the use, with a note at the comptime that computed it. A literal standing with nothing beside it keeps its type-less reading (Part I, 2.4), and an expression between those cases is widened rather than refused. The refusal replaces the backend’s message (C.1). NK1117 a statement is one name and nothing declares it. A word the scannerless grammar has no rule for is read as a name, and a name on its own is a legal statement; assert c and a leading _000 are refused here. 1_000 is the number 1000. The help explains a word that is not reserved: loop { … } is answered with write while true, const X = … with write comptime, and macro and quote with Nikaia has no macros. Four things declare a name: a local or parameter in scope, a function either ledger describes, a type declared here, and a module of this program. A name this compiler cannot see is not refused (C.4). The same code carries a call by a bare name nothing declares — nothing declares a function dobled, with did you mean doubled? where a function of this program or a bare std name is near. A bare name has nowhere else to come from: a use of a module brings none in, so a package’s function is written with the package’s name in front (Part I, 9.1). A name a use item ends in, or renames to, counts as declared. The same code carries the prelude’s two rules: a std name that lives in a module written without its prefix — std has text::digit_value — and a module used before it is introduced — fs is used here and introduced nowhere. Both hand over the line to add. Both are asked only where std’s ledger has exactly one entry for the name, and never about a module of this program or a package. What needs no use is the list in Part I 1.3: the entries std’s ledger keys bare. NK1118 a division, or a remainder, whose divisor is a constant zero. A division by zero at run time stays where A.2 puts it. NK1116 and NK1118 read the same constant fold: a literal, an immutable let whose value folded, + - * / % and a negation, in a magnitude and a sign (65 bits), each step held to the type a declared operand gives it; nothing is claimed about a divisor the fold cannot evaluate. NK1119 a let, a for binding, a lambda’s argument or a struct field called self. self is the one reserved word that is a name; every other reserved word does not parse in a name position. A parameter named self is refused by the grammar, because the receiver takes the word. NK1120 is unused and the number is not reused. NK1121 a ?. through a list’s index whose element is not a T?; the help names the length check. Through any other value that cannot be absent it is NK1217. Asked only where the receiver’s type is known (C.4). NK1122 an as names a type Part I 2.2 does not offer - n as usize, n as u128 (ADR-285 D14). NK1123 a hull written a second way, or a hull of a hull: Shared[Locked[T]] is SharedMut[T], and the message carries the replacement; Shared(x) where x is already a handle adds a second count around one value. NK1125 a member reached off a T? with a plain ., NK1121’s mirror. a?.b.c guards a and nothing else, so the unguarded .c reaches into a T?; a T? is a type of its own (Part I, 2.3), and a member of T is not a member of it. The way out is the guarded form, or ?? and then the plain .. NK1124 a door over several locks written wrong: handed something that is not a lock, handed one where several are wanted, or given a block that does not name one value per lock. A number is refused there although a literal carries no type (Part I, 2.4). NK1126 a field or a method reached on a type parameter that no bound of it declares. A T with no bound can be moved and passed and nothing else. The message says no bound rather than no such method. NK1127 a comptime binding, or an option’s default (Part I, 5.1), this compiler cannot evaluate while it builds. A let may fold; a comptime must. What may be evaluated is Part II 10.2’s: values of the shapes that cross, and a call to a function or method the ledger lets run at build time. The message names the way out: let. A check made with no place to compile build-time code in, such as a library call without one, refuses a comptime that calls a function with this code too, and the note says why; it never leaves the value open. NK1128 a name the language below reserves and cannot escape: crate, super and Self. Every other such name is written escaped and stays a name, so a field called type is accepted. Asked at every position that declares a name, including an item’s own name. NK1129 a trait’s method that an implementation pauses in where the declaration says sync. Without the word a method may pause. NK1140 the same comparison for throws: a body that fails under a declaration without the word. NK1130 an impl and the trait it names disagree about which methods exist: one the trait does not declare, or one it declares that the impl leaves out; two messages under one code. An impl of a trait this unit does not declare is not checked. NK1131 a mut parameter whose type is a view, handed back: the caller’s view is changed in place, and what would come back is a view of that view; the help takes the parameter without mut and walks a local. NK1131 also: a field of a borrowed subject (self, a lent parameter, a for binding over a list, a let over a place) or an element a list or a map keeps (first(), last(), get(i), m[k], m.get(k)) bound by value where a view is not what the line can mean: handed whole to a mut parameter or changed through a let mut. The compiler writes no .clone(); the help writes .clone(), for a field s.inner.clone(), for an element …?.clone(), and the message names the whole path (l.ty, x.inner.ty). Asked only where the type is known and does not copy: a number, a bool, a scalar and a view take nothing away, and nothing is claimed about a value this compiler cannot type (C.4). Handed back, at a return or as the body’s last expression, such a field or element is a view of its subject and is not asked (ADR-views-3 D7, D8). The same field bound or handed to something that keeps it is NK2106. NK1132 a break or a continue with no loop to act on (Part I 3.3): there is no loop, or a function boundary stands between (a lambda, a task an async form starts, or a DSL fold’s step), and a jump does not leave a function. A catch handler is not such a boundary and is not refused. NK1133 a statement after a break or a continue, in the same block. break carries no value, so a value written after it parses as a statement of its own. NK1134 a catch over an expression that cannot fail. An expression whose failure could not be looked up is not refused. NK1135 a type nothing declares, a type the backend has and the language does not offer (usize, i16, u128, str, outside an extern "C" declaration, with i64 or String as the help), or one written without its module: HashMap is written without its module, with use std::collections and collections::HashMap handed over. A type that lives in a module is reached through it, as a package’s is; what needs no prefix is the list in Part I 1.3, the names std’s ledger keys bare. Only std’s modules say use std::…; a package’s prefix is the package’s name. The known set is Part I 2.2’s own types, the ledger’s types map and the declaration’s own type parameters; a qualified name is left alone. A bound naming a trait neither this unit nor a ledger declares is the same refusal, with the message saying trait. char is the same refusal, and its help names scalar and u8 (ADR-320). NK1136 a let that binds several names and is given a type: the names are taken apart by position, and one written type cannot say which of them it is about. NK1137 a ref written in an expression outside an extern "C" declaration: at a call, in a for, at a return (Part I, 6.5). The caller writes nothing; whether the argument is lent, changed or kept is read off the callee’s parameter (ADR-views-3 D1, D4). The help removes the word. NK1138 a parameter a body changes where the declaration does not say mut. fn fill(mut out: Vec[i64]) is where in-place change is written, and the caller’s value is what changes. Raised only where the change is certain: an assignment into the parameter or into a place rooted at it, or a method every candidate entry marks mutates. A name a let has bound is no longer the parameter, so let mut v = x is a way out, and a method no ledger describes is not refused on (C.4). Said once per parameter, with the caret on the declaration. For a fold’s accumulator it is asked at a door and nowhere else: par_fold(…, fn(acc, m) { acc.record(m) }) compiles. NK1139 a let whose value is changed, and no mut on it (Part I 2.1). A name handed to a mut parameter is changed, so a let without mut handed to one, or a field of it, is refused too, and a parameter without mut is NK1138 (Part I, 6.5). The same code refuses a change to a for binding without mut (Part I, 3.3); over a list or an array the help writes for mut x in xs and says the change reaches xs, and for a change meant for the turn only let mut y = x.clone() (ADR-views-2 D8). It also refuses for mut over a list the function may not change, labelled at the list. A match arm’s binding is the arm’s own and may be changed (Part I, 3.4). It is separate from NK1138 because a parameter’s mut also decides what the caller sees, where a let’s is only about this body. Both read the binding in scope, so an inner block’s xs stops being it when the block closes and an outer mut xs is it again. NK1141 an update block that hands a value back. The block takes mut v and changes it, and the change is the result. Asked of the shape only: a last statement that can only be a value, or a return carrying one. A last statement that is a call is left alone (C.4). NK1143 a call to a name an extern block declares, outside an unsafe block (15.1). NK1228 a dsl block names a package where a grammar stands, dsl sqlite { … }; the help names the package’s pub grammars, dsl sqlite::Sql (Part II, 10.5). NK1229 a supervisor’s child captures a mut binding, or a value an attempt would keep, hand on or use up; the next attempt would not start fresh, and the help names building the value inside the child’s function, or .clone() there (Part II, 12.8). NK1230 a value where a parameter list holds a type, or a type where it holds a value: schema(user) for fn schema[T](T) (the help writes schema(User)), or hand(User) for fn hand[T](x: T) (Part II, 10.3). The same code refuses a struct or enum of the program named as a value where it has no constructor (let c = Conn). NK1231 a meta::Type that would reach the running program: kept in a value of it, or handed to code that runs then; it carries types, which exist only while the program is built. NK1232 is retired and not reused: a function type’s kind is Fn(F) (ADR-332 D1). NK1233 (warning) a call names a function’s type arguments in brackets, id[i64](3), where a value argument’s type could have said the type (not where the brackets alone say it, json::read[Contact](bytes), ADR-grammar-2 D11); the form is allowed while its uses are collected, and the help asks for the use case at #514. NK1234 a struct literal leaves out a field that has no default (Part I, 4.1). The same code refuses a struct pattern that leaves out a field and does not end with .., Point { x: px } over a Point with a y, at any depth of the pattern (Part I, 3.4). NK1235 an attribute names a struct that @meta::Attribute does not mark, or stands before a declaration the mark does not name; also .attribute(X) where X is no attribute (Part II, 10.3), and @inline before anything but a function or a method with a body: a trait’s method declares none (Part I, 5.6). NK1236 an attribute stands twice before one declaration, and its mark does not say repeatable: true; @inline stands once. NK1295 an assume in std’s Nikaia (ADR-376 D3). NK1296 +, -, *, / or % on a vector; the help names wrapping_add and saturating_add (ADR-377 D4). NK1297 a simd::Fixed whose lane count is not a literal power of two from 2 to 64, or a lane type other than an integer of 8 to 64 bits (D1, D2). NK1298 a shuffle index that is not a constant or not below the lane count (D3). NK1299 a lane shift, << or >> on a vector, whose count is not a literal below the lane’s width in bits (D3). NK1300 an assert the compiler does not prove, or a precondition a call does not prove; the message says why and that not proved is not false, and unproved-claims = "warn" makes it a warning and a check where the claim is reached (14.2, ADR-380). NK1294 an assume outside an unsafe block (ADR-376 D1). NK1293 @inline given anything but nothing, always or never (Part I, 5.6). NK1237 an entry point, extern fn with a body, that is not pub (15.1). NK1238 an entry point in a build that makes no library: only artifact = "c-library" exports one. NK1239 an entry point that is generic, or a trait’s method: C calls one signature, without dispatch. NK1240 an entry point’s parameter or result that does not cross to C, and the help names the shape that does: ref String for text in, String out, ref Array[T] of a number, a pub struct held as a handle, a callback that is sync (15.1). Only a name this file declared extern. NK1144 a let _ = expr: _ is the ignore pattern and stands where a name would be bound (a tuple position, a parameter, a part of a match pattern), never as a whole binding. The message says to write the expression as a statement or bind it to a name. NK1145 a field of an extern struct, or of a variant of an extern enum, that is not a C value: text, a list, an optional, a lock, a Shared, a function or a struct without the word. The message names the handle as the shape to use. NK1152 a build-time body the rule forbids: a callee that can pause, or whose touch set is anything but the build’s own parameters. Distinct from NK1127, which says this compiler cannot evaluate it, and from NK1244, a run the rule let start that stopped by itself. The rule is two ledger columns and not a list of allowed functions. It also refuses a Nikaia dependency whose ledger disagrees with what this build derives from its sources, naming the package and both answers; a call into a dependency without sources; and a call that reaches a Rust crate’s function, other than std’s, directly or through the functions it calls. The same code carries the step budget, the memory bound and the call depth: a build-time run that takes more turns of a loop and calls than its budget, holds more bytes than its bound, or recurses past the depth, is refused, naming the comptime, the bound and the call path (Part II 10.2). NK1245 an expression whose type the compiler cannot tell (C.4). NK1153 an empty list whose element type nothing ever says: [] carries none, so it takes one from the first use that needs one. Asked once the whole body has been walked, and only where nothing at all uses the name; a use this checker cannot read a type out of is left to the language below (C.4). The same code refuses a map made without an annotation that nothing writes into or types (ADR-285 D43). NK1154 two elements of one list literal that do not agree: two types with no common type (Part I, 2.2), or a number beside something that is not one. The message names the two types, or the kind (a number beside text) where an element has no type yet. Once per literal, and the only code said about it: the place the list goes into, let v: Vec[f64] = [1.0, 2], is not refused again. NK1155 the alternatives of an | pattern bind different names. Every alternative binds the same set. Recursive, so an | inside a tuple’s part is the same refusal one level down. NK1156 a use std::… whose last segment is a type: a use names a module and brings no name in, for std as for a package. Where the type lives in a module the help names that module — use std::fs and fs::Mapped — and a type keyed without one needs no line at all (Part I, 1.3). A ledger key is a type’s when its entries are called on a value (self), and a module’s when they are not. A module nothing describes is NK1186’s question. NK1186 a use std::… whose module std does not have. The accepted modules are what std’s ledger declares, joined with the modules this specification names without a ledger entry — db, json, process, thread, panic, build, task, backend. The prefixes the ledger keys that are not modules are subtracted: str::len and list::ListExt::map sit beside fs::read, and a primitive and a trait need no line (Part I, 1.3, 2.2). Only the second segment is asked, so use std::db::postgres is answered by the module it starts at. A module nikaia-std’s crate has and std does not offer gets its own message: tools holds the Rust-signature grammar, which the compiler calls and a program cannot reach. NK1187 a grammar element the page names and this engine does not have: tag and digit1, each answered with the spelling to use — a string literal and digit+. NK1188 == or != on a type two values of which cannot be compared. A type compares when every part of it does, walked structurally: the language’s own types from a list, a container exactly when what it holds does, a declared struct or enum from its parts, and a type whose parts are Rust from the ledger’s compares column - std’s or a described crate’s - whose absence is no; a lock, a mapping, a socket, a task’s handle and a channel’s ends do not compare. A name nothing knows - no declaration, no ledger entry, a module no ledger knows - is not asked: it is already NK1135’s, NK2504’s or rustc’s (ADR-204 D1). The help is one the source can take (C.2). Asked of one side and only where its type is known (C.4); the two sides disagreeing stays NK1102. NK1158 a ref mut written outside an extern declaration. It exists for the C boundary only: a parameter this language may change is written mut name: T, a receiver mut self (ADR-views-3 D3, D4). NK1159 a length handed to an extern declaration beside a buffer it cannot be shown to fit. A ref Array[T] and a usize right after it are one fact in C. Two shapes are accepted: the buffer’s own len(), and a constant a known length covers — an Array[T, N] carries its length and a Vec[T] does not; a zero is covered by every buffer. Nothing is claimed where the callee is not a foreign declaration, or where the buffer’s type is unknown (C.4). NK1161 a throw of something that is not an error (Part I 7.1). What is thrown implements Error, and the impl line says so; a number, a bool, a character and text are Part I 2.2’s own types and never do. Only those are refused: a type this file declares may have its impl in another file of the same package, a package’s type is not this compiler’s to answer for, and a caught error re-thrown is a ? (C.4). A struct or enum the package declares is refused too where no file of the package writes its impl Error; the help writes the impl. The kind is asked and not the type, because a bare 3 fits every numeric type and arrives as ? (Part I, 2.4). NK1160 a field, an index or a call reaching past an opaque handle. A handle is an address this language never dereferences, and nothing here constructs one. NK1157 a list literal standing where an Array[T, N] is wanted, with a different number of elements, or a [v; n] whose n is not N or not known while the program is built. The message names both numbers. The literal takes the array type from its use; an element that is not what the array holds is refused under the code of the let, the argument or the field. NK1151 a match that does not cover every case. An enum is complete when every variant is named; anything else needs else, and bool is complete with true and false. A match over a catch’s error is complete when every non-fatal type in its set is covered; where the set holds "?" or an unreplaced from(p) it needs else. Where a callee’s set grew, the message names the new type and the call that brings it in, from the ledger diff (ADR-357). A bare name catches and covers, and so does a pattern of the scrutinee’s struct whose every field is a binding, _ or left to .. (Point { x, .. }). Where the scrutinee’s type is not known, nothing is claimed (C.4). NK1150 a match arm written _: the catch-all arm is else, and _ is the ignore pattern, for a value that arrived. Raised by the parser. NK1149 a type’s constructor written Type::new: a type is constructed the way a .nika file declares one, Vec(), String(), HashMap(), Stats(first) (Part I 4.2). Asked of the name and not of the position, so a constructor handed over as a value goes with it: par_fold(M, Summary, …). A qualified name is left alone, as for NK1135. NK1148 a name declared twice in one file: a fn, a struct, an enum, a trait and a grammar declare a name; a method belongs to its type and a rule to its grammar, and neither declares one. Across files the same rule is the module layer’s message; nikaia lower outside a project skips the module layer. The caret is on the second declaration, and the message names both kinds. NK1147 a grammar’s rule reached through a dot: a rule of a grammar is a qualified name, Json::value(input), and the dot is for a value’s members. Asked only where the receiver is a grammar of this file and the name is one of its rules; the message carries the whole rewrite. NK1146 a struct literal written like a call: Name { field: value } is the literal, and Name(first) calls the constructor, so an options-only call is unambiguous. Asked where the name is known to denote a type, before the call resolves (C.1). A name nothing declares is not this: Widgit(size: 3) is NK1117’s call to a function nothing declares, and the brace form keeps NK1135’s claim. NK1142 is retired and not reused: a function type stands in a field, a result and a let (Part I 5.4). NK1162 a compound assignment on a map slot: m[k] += 1 reads the slot as well as writing it, and a map read is a T?, so the line has to say what an absent key counts as — the message hands over m[k] = (m[k] ?? 0) + 1. A sequence is untouched, because xs[i] is a T. Asked only where the read is nullable, so nothing is claimed about a container this compiler cannot type (C.4). NK1163 a name that needs no use, written with a std module in front of it: io::println("x"). It is NK1117’s rule read the other way. Both halves are required: the module has no such name and the bare one is a name std keys. NK1164 a call passes a type that does not answer for the bound its parameter carries: a type with no impl of the trait (the help writes the impl), a parameter of the caller’s own whose bound lacks it (the help widens the bound), or a type the declaration does not make what a shape bound (Struct, Enum) asks for, which no impl answers; and an impl Fatal for T where T has no impl Error, which a fatal type is too (ADR-345 D1). NK1165 is retired and not reused; an index past the end at build time is NK1244, with the words the run gives. NK1166 a comptime whose value is not the type it declares; an Array[T] with no length is one, and the help writes Array[T, N] with the length the build computed. NK1167 a comptime or an option’s default whose value owns memory one level in: a field, or what a variant carries, that is a Vec or a String. The message names the field, because the struct around it is fine. The same code refuses a value of a std type whose ledger entry names no constant (13.5), and names the type. NK1168 a comptime that depends on itself; the message names the chain. NK1169 a Fixed map (Part II 10.2) with one key twice; the message names both pairs. NK1170 a Fixed map whose keys are not text. NK1171 a member a known head or receiver does not have: a Type::member that names nothing :: reaches (no such variant, a field read from a value with a dot, or a field or variant reached by a type’s name where a bound, [T: Struct] or [T: Enum], is what reaches it), and a method, associated function, module function or field that neither the program, std’s ledger, a crate’s description nor an extern block declares, also where the backend has one by that name (String::from, "x".as_str(), opt.is_some()); the help names the language’s spelling where there is one, otherwise the nearest name (C.4). NK1172 one field set twice, in a struct literal or a with. NK1173 a with on what is not a struct value it may copy: an enum, another type, a view of a struct, or a value whose type could not be worked out. NK1174 a with that changes no field, which is only a copy. NK1175 an asset this build may not read: no list of readable files is in effect (--allow-read-from-list=…), the path is not in it, the path is absolute or climbs out with .., the listed file cannot be read, or it is not UTF-8. Each reason carries its own way out. NK1176 an asset whose path is computed rather than written out, so the list cannot be checked against the line. NK1177 an asset outside a comptime; the help offers comptime or fs::read. NK1178 a grammar this compiler could not run while it built: the parser refused its input (its diagnostic is relayed whole), the result has no build-time form, the grammar would run inside another still running, there is no directory to compile the parser in, or the generated parser did not compile or its result could not be read. The last two are this compiler’s defect and say so. NK1179 a field declared as a view of a list something else keeps, given a list this body owns: a parameter lends a list on its own, a field does not. NK1180 a member of a reflected field from T::fields other than .name, .of(value), .ty, .doc, .default, .attribute(X) and .attributes(X), or of a variant from T::variants other than .name, .is(value), .attribute(X) and .attributes(X); what a variant carries is read with a match. NK1181 a path whose head is none of the five things a word in front of :: may be: a type, a package use brings in, a package nikaia.toml declares, a Rust crate a description covers, or a std module, in a call (nowhere::wobble(1)) as in a value; the help is a use (with a [dependencies] line or nikaia describe where the head is not yet declared), never a new file, and names a known head one edit away first (did you mean fs?); the refusal fails open (C.4). NK1182 an Array[T] with no length as a field, an element or a result that would have to own: no piece of a buffer flows into it, so it cannot be a view (Part I 2.2, ADR-views-3 D11). The help offers Vec[T], Array[T, N], or a named length, fn f[comptime N: i64](xs: Array[T, N]) -> Array[T, N] (Part I 4.6). NK1183 a let that declares an owned T for the element a for lends; the help removes the type, or writes .clone() for a copy. NK1184 a \ in a literal that the escape set does not name, or a \u{…} naming a surrogate (U+D800-DFFF). The set is Part I 2.5’s: \n \r \t \0 \\ \' \" \xNN \u{…}. Asked of a "…", an f"…" and a '…' alike (C.1, C.2). The refusal reads the same table the build-time decoder does, and the help is read off the escape: a malformed \x or \u{…} is told the form it should have had, and anything else is a backslash to double. NK1185 a ?? whose left side is a view and whose fallback owns. user?.name is a view of user where name does not copy, and ?? "nobody".clone() asks for one value that is both. The help is ?? "…", a text literal, which is already a view (C.2). .clone() is read by name; .to_string() of text is the text itself and stays a view (ADR-282 D8), and only of a number or a value whose type is not known is it owned. Both sides have to be known (C.4). The same code carries a map’s value that is not text: m[k] ?? [] reads a view of the list the map keeps, beside a fallback of its own, and the help hands over m[k]?.clone() ?? …, the copy written where one is wanted. m.get(k) is the same read, and so is a name a let bound to either: let found = m.get(k) is a view of what the map keeps, and found ?? [] is refused as m[k] ?? [] is. A map’s text beside a name that is a view of text is a view whichever side answers. NK1189 a copy written .to_owned(): a copy is .clone(), for text and for everything else. .to_string() is the text form of a value and stays. NK1301 .to_string() or .clone() called on a plain text literal: the literal is already text where text is wanted, so the call is dropped (ADR-282 D30). NK1190 a type called like a function with nothing to call: a std type whose ledger describes no constructor, or a struct of this program with no anonymous constructor, whose help hands over the literal. NK1194 an assert whose condition could pause, fail, touch anything or change a value (14.2): every call in it has to be sync, throw nothing, touch nothing and change nothing, and one nothing describes is not known to. NK1195 an assert of another shape: other than one bool, an option other than a text message:, or the name alone. NK1196 an impl method that takes its self another way than the trait declares, asked of a trait of the same file and of Error, Drop and Cleanup. NK1197 a bit operator written beside a comparison without parentheses: this language binds & tighter than == and C binds it looser, so the line reads two ways; the help hands over (a & mask) == 0 (ADR-285 D10). NK1198 &, |, ^ or a shift on something that is not an integer; on a bool the help names &&, || or !=. NK1199 two number types in one operation that have no common type (Part I, 2.2) - u64 + i64, or an integer and an f64 - with the conversion to write; a shift’s count is the one side that may be any integer. Each is asked only where both sides are known (C.4). NK1200 one number without an annotation, two uses that ask two types of it - handed to an i32 and to an i64 - naming both, with the annotation to write (Part I, 2.4). The same code refuses a let of a '…' whose uses ask a u8 and a scalar of it, with let c: u8 = … in the help (Part I, 2.6). An index asks for an i64 only where nothing else asks. NK1215 a computation with &, |, ^, !, <<, >> or a wrapping_, saturating_ or truncating_ name, in a narrower integer type than the place it is put states, with both conversions to choose from: (a as i64) << 3 and (a << 3) as i64 (Part I, 2.2). NK1216 (warning) a ?? whose left side cannot be absent: the answer is the left side and the fallback never runs; the help says to remove it (Part I, 3.5). NK1217 (warning) a ?. through a value that cannot be absent: it is the plain ., and the help writes .name or .name(…) (Part I, 3.5). NK1218 a dsl block’s -> T names a type that is not a struct the program declares, or a field of it whose type no column can be and that is no group: a scalar, its T? or a struct is (Part II, 10.5). NK1219 a column of a block with -> T has no field; the help names the field to add and extra_columns: true. NK1220 a field of the -> T struct has no column; the help names the column and, for a T? field, missing_fields: true. NK1221 a column that may be NULL goes into a field that is not a T?, or a column’s type is not the field’s; the help names T?, COALESCE(…) and WHERE … IS NOT NULL. NK1222 a flat field of the -> T struct names a column two tables of the query have; the help names AS, a group field and the block without -> T. NK1223 a grammar declares extra_columns or missing_fields, which belong to the compiler. NK1224 a system library a package names is not found; the message names the package, the library and the pkg-config name looked for (13.4). NK1225 pkg-config returned a linker flag outside 13.4’s list; the message names the flag and the package. NK1226 an extern(library: …) names a library the manifest has no [library.<name>] entry for, or an entry names a library no block does; the help writes the missing entry with its pkg-config line (13.4). NK1227 extern "C": the C convention is the only one, and the help writes extern (15.1). NK1202 an assert about data from outside the program, which a guard checks instead (ADR-269 D6). NK1207 an assert, a call to a function with a precondition, or an index or a +, - or * whose check would stop the program, that the compiler shows false with values - every time it is reached, or for a value it shows reaches it - and a warning only under refuted-claims = "warn" (13.3); where it read a call’s result by its callee’s body, the note gives each such value and where it came from (ADR-359 D8) (ADR-269 D8). NK1209 an impl without a trait on a type the program does not declare (Part I 4.7). NK1210 a method of a number that std does not describe, and collect() on a list, whose map and filter hand back a list already. NK1211 a ?? after a list’s index whose element is not a T?; the help names the length check. After any other value that cannot be absent it is NK1216. Asked only where the left side’s type is known (C.4). NK1212 a '…' that is not one u8 or one scalar its use can take: more than one scalar, a scalar that is not ASCII where a u8 is wanted, or '\xNN' above \x7F where a scalar is; the help hands over the text literal where it is a grapheme (Part I 2.6). NK1213 (a warning) a '…' stored as several scalars that normalise to one, which it is taken to be; the note says the editor stored it decomposed. NK1214 a text cut, moved or searched at something that is not one of its positions - a number, a position of another text, or of a text chosen at run time; the help names forward and the view (ADR-374 D5). NK1208 (a warning) a pub function’s precondition is stronger, or its postcondition weaker, than the committed ledger says (ADR-269 D19). NK1203 and NK1204 are retired: a call that does not prove its callee’s precondition checks it, and a function handed on as a value checks it in its body (ADR-269 D5). NK1205 a match over a T? with no null arm whose arm names a variant or a literal of T: the pattern says nothing about null. The help hands over ?? first, and a match of what it gives. NK1206 a for over a T?: a for walks a list and not the maybe of one, and the lowering walked the option, once, with the whole list as the binding. The help hands over ?? []; for a map read, NK1185 then hands over the copy, m[k]?.clone() ?? []. NK1191 an arithmetic operator, or its compound assignment, on something that has none: text or a bool ("a" - 1, true + 1; + joins two texts and nothing else), a list, a map or a set (Part I 4.5), or a struct or an enum this unit declares - there is no overloading and no trait that gives a type an operator. The same code refuses - on anything but a number and ! on anything but a bool, an integer, a vector or a mask. -= is asked as - is, and + or += onto text stays a concatenation. Where a struct has exactly one numeric field and the side is a name, the help names the field: Did you mean a field, like a.balance -= 30? Asked only where a side is known to be one (C.4). NK1201 a value with no text form in an f"…" hole - a list, a map, a set, a range, a tuple, a SharedMut[T] or a Locked[T], whose value is reached through a door (Part I 6.3), or a struct or enum of the program that is not an error type -, or the same value handed to print, println, eprint or eprintln (#873), or an fs::Path in a hole of an f"…" that is text. A hole is written as its value’s text, and so is a print call’s argument (Part I 2.5): text, a number, a bool, a scalar, and an error, whose text is its message, have one; a collection, a range, a tuple and any other struct or enum have none. The help joins a list’s elements first, let text = data.iter().join(", "), and names a struct’s fields as holes of their own. A path has none either where the f"…" is text; the help names {p.to_text()} and {p.display()}. Asked only where the hole’s type is known to be one (C.4), and not of a hole whose : asks for a form with a ?. NK1193 a pattern that looks inside a part that holds its own type further than the lowering reaches: one such part per arm is looked into (the arm is then taken only where the part has the shape, and covers no variant on its own for NK1151), but not a part inside that part, and not in one alternative of an | (ADR-246 D5). A guard may read a name bound in there, and a part bound whole out of a box: it reads them through the box. NK1241 a narrowing as the compiler does not show to fit - a wider integer to a narrower one, signed to unsigned or back, an f64 to an integer or to an f32: the help names checked_<T>() (a T?, null where it does not fit) and truncating_<T>() or rounding_f32() (the backend’s conversion); a constant that does not fit is NK1116. The same code refuses an integer other than a u8 as scalar, a literal too: the help names scalar::from(n) (Part I 2.2). NK1242 a dsl block over a grammar with several entries, none marked main, that names none: the help names the entries, dsl G::entry { … }, and main entry rule. NK1243 a grammar with two main entries. NK1244 a build-time run that stopped: the code a comptime or a default runs aborted as the program would abort there - an overflow, an index past the end, an unwrap of nothing, a panic() - and the message is the run time’s own, at the line where it stopped, with the comptime it was computing. An initialiser of literals the checker folds stops the same way, with the same words. NK1246 two maps that must be hashed the same way (17.1) are made with two different hasher: choices, or with one the keyed hash a trait method, a described crate or a binding fixes contradicts: the message names both places and the value that joins them, seen and names end up in Index.words, so they have to be hashed the same way, and the help says to name the same hasher at both, or to leave one out so the compiler chooses. NK1247 the key of a BTreeMap or a BTreeSet, written anywhere a type is, has no order: BTreeMap keeps its keys in order, and P has no order. The language’s own types have one, from a list (a number, String, bool, char, Bytes, and a tuple, list, option or ordered map or set of such); a float has none; a struct or an enum the program declares has one only where the program writes impl Ord for it; a type whose parts are Rust has one only where its ledger says orders = true. The help names a HashMap or HashSet, or a key by a text or a number (ADR-010 D10). NK1260 the key of a HashMap or a HashSet, written anywhere a type is, does not hash: HashMap finds its keys by their hash, and Q has none. A type hashes when every part does, walked structurally: the language’s own types from a list (a number but no float, String, bool, char, Bytes, and a tuple, list or option of such); a float, a map and a set do not; a struct or an enum the program declares hashes from its fields where every field does, and not where the program wrote impl Eq for it, unless it also wrote impl Hash; a type whose parts are Rust hashes only where its ledger says hashes = true. A value handed to a Hasher’s add that does not hash is the same refusal. The message names the part that does not hash, or the hand-written equality and the impl Hash that would answer it; the help names a BTreeMap where the key has an order, or a key by a text or a number (ADR-010 D11). NK1261 is retired and not reused: ref outside an extern "C" declaration is refused, not warned about (ADR-views-3 D4). NK1262 an int in an extern "C" signature or a described Rust contract, where the other side reads the bits; the help names i64 (ADR-285 D38). NK1263 (hint) a claim that the result summary of a function in another package, read from a path, would decide: the fact it would give and the assert on the result that would make it part of that function’s contract (ADR-359 D4). NK1264 an impl of a trait from another package keeps a parameter the trait method’s column does not: the trait method, the parameter, the statement that keeps it, and that only the trait’s package widens the column (ADR-277 D17). NK1265 (a warning) the keeps column of a pub trait method changed, in either direction: the parameter and the impl that changed it, until the ledger is committed (ADR-277 D17). NK1273 a parameter of main that no word can be: a type other than int, a fixed-width integer, f64, bool, String, one of these behind ?, or a last subject parameter of Vec[T] of one of them; a required subject after a subject of type T?; any parameter of main on a target with no command line (Part I 5.5, ADR-360 D2). NK1274 an option of main named help, which the command line keeps for the help (Part I 5.5). NK1280 a [v; n] whose v is not a value that copies, a String or a Vec: the help writes (0..<n).map(fn(_i) { v.clone() }).collect() (ADR-362 D3). NK1281 (warning) a list literal whose only element is a range, [0..181]: a list of one range; the help writes (0..181).collect() for the numbers and [0; 182] for that many equal values, and a written type such as Vec[Range[i64]] silences it (ADR-362 D5). NK1282 a grammar’s entry handed an argument that is neither a String nor a Bytes (ADR-366 D1). NK1284 a field of type text::Pos; the help names text::Cursor (ADR-374 D6). NK1285 a forward or back on a position with no unit or with more than one (ADR-374 D4). NK1288 a struct’s rule, the assert after its fields, whose claim reads anything but its fields, paths, methods that change nothing, comptime values and literals (ADR-369 D1). NK1287 a bytes::ByteSet the build proves empty (ADR-375 D2). NK1286 an environment entry written as a literal in a process::run call that no platform accepts: an empty name, = or a NUL in a name, a NUL in a value (ADR-243 D7). NK1283 a tuple pattern whose shape is not the value’s: let (a, b) = (1, 2, 3), let (a, b) = Row { … }, for (a, b) in rows over a list of structs. A value is refused where it is certainly no tuple of that width (a tuple of another, one of the program’s structs or enums, a number, a bool, a char, a String), at each level of a nested pattern; one whose type is not known is not. NK1248 an operator on a type parameter that no bound allows: < needs T: Ord, and == needs T: Eq (ADR-341 D3). NK1249 an impl Eq, impl Ord or impl Hash for a type another package declares, or an impl Ord or impl Hash for a type that is not Eq (ADR-341 D5, ADR-010 D12). NK1250 a type a grammar entry is called with, or a json::write[T]’s T, that holds a field of a kind no arm of the grammar’s match covers or that an arm refuses (Part II 10.8, 17.3); the message names the field, the path to it, the rule and the reason. NK1310 a match in a grammar rule’s pattern on a value not known while building (Part II 10.8). NK1311 two fields of a struct read by members[S] that have one name in the input. NK1312 a field members[S]’s name: leaves unread that has no default and is not a T?. NK1320 meta::Field, a reflected field’s type, standing anywhere but as a parameter’s type (Part II 10.3). NK1251 a json::read[T] whose T does not match the schema it is given (17.3): a required property with no field, a field the schema does not have, a type that does not match, or a field that is not a T? for a property that may be null; the message names the property and the field. NK1252 an enum written by its type’s name alone, Shape(r), where the enum has more than one variant (Part I 3.4, 4.4); the message names the variants and the long form (Shape::Circle(r)). NK1253 a pattern of a positional variant that names a different number of parts than the variant carries, E::A(_) against A(i64, i64) (Part I 3.4); the message names both counts and the help writes the pattern with one _ a part. NK1254 is retired and not reused: a tuple may be nullable, (A, B)? (Part I 2.3, ADR-364). NK1255 a rest .. in the brackets of a variant without values, E::V(..); the help names E::V. NK1256 a null arm in a match over a value whose type is never null (Part I, 3.4). NK1257 is retired and not reused: ref outside an extern "C" declaration is refused whatever the type (ADR-views-3 D4). NK1258 a pattern with more than one .., [a, .., b, ..]. NK1259 a variant in a let, a for head or a parameter (let Some(x) = o); the help names match. NK1304 @unroll before a for over a list that is not a build-time value, naming the list and why it is not known (Part II 10.3, ADR-specialization-1 D2). NK1305 a value that may be a run-time value - the loop variable of an @unroll(up_to: N), a comptime? parameter in the function as written - where only a build-time value is allowed (D1, D3). NK1306 mut on a for binding that cannot be changed in place: a map’s key (a mut in front of the whole head of a map, for mut (k, v) in m), a set’s element, the element a lending adapter hands (v.iter().enumerate()). The message gives the reason, each in its own sentence: the key decides where the entry stands; the adapter hands read-only views. The help: take the entry out and insert it again after the loop, change a map’s value by key (m[k]) in a loop over keys taken before it, or, for an adapter, the index loop (ADR-views-2 D4, Part I, 3.3). NK1307 (code to be reserved) mut in front of one name inside a tuple pattern, let (tx, mut rx) = …, for (k, mut v) in m, labelled at the mut. The form is not supported yet, and the message says so: refused now, possible later (ADR-views-2 D1, section 6), not refused on purpose. The help writes what works today: mut in front of the whole pattern, let mut (tx, rx) = … or for mut (a, b) in pairs, which marks every name. NK1330 a call of a grammar’s entry without words: whose result can hold a winnow_grammar::Symbol, in a field, an element, a variant, a tuple or behind ?, at any depth, where its grammar interns (reaches ident or intern(p)): the symbols would point into a table nobody can reach after the call. The label is at the call; the help writes words: table with a table made by winnow_grammar::InternerContext(). An entry that interns only on the way, its result holding no symbol, is called without it (ADR-388 D2). NK1331 an immutable binding whose value can change: its type reaches a SharedMut, a Locked, a channel end or another handle to storage changeable through another owner (the message names the path to the first such part), an item-level initializer that can throw (the help writes a catch or a T?), or a cycle among item-level immutables (the message names it) (ADR-389, Part I, 2.1). NK1332 a format after the colon of an f"…" hole outside its table, or one that does not fit the value: a base on a value that is not an integer, a precision on one that is not a float, a 0 on one that is not a number. The message names the table (Part I, 2.5). NK1333 a ref written in a declaration outside extern "C": on a parameter, a receiver, a field, an element type, a local binding or a result. The help removes it (Part I, 6.5; ADR-views-3 D4); at a call or in an expression it is NK1137, and ref mut is NK1158. NK1334 is a warning, not a refusal: a parameter marked keep that the body never keeps. The help removes the word (Part I, 6.5; ADR-views-3 D2). NK1335 a from that does not name a way out’s source: a way out of the body hands back a view of a parameter the written from leaves out (Part I, 6.6; ADR-views-3 D8). NK1336 a result that is a view, with no from, where there is no body to infer its source from: a trait’s method, a function type, a foreign or Rust function (Part I, 6.6; ADR-views-3 D8).
NK21xx Running at once, and capture NK2101 a task takes ownership of a variable still used afterwards (Part I, 8.3). Raised only where the type is known and a move takes it away: a number, a bool, a scalar and a view are copied, so the name keeps working; a handle on a Shared[T] is duplicated, the exemption Part I 8.3 states; nothing is claimed about a type nothing describes (C.4). An assignment between the task and the later use clears it. NK2102 is retired and not reused: a task may pause at every setting (Part I, 8.1.2), a par_iter() lambda of map, filter or for_each too (Part II, 12.6). NK2103 a lambda after async (or after spawn, until it is removed) names an argument, and a task is handed nothing (Part I, 8.1.2): async starts a body, it does not call it. NK2104 a task and what runs beside it meet on a resource, and the message names it: an async task and a statement of its window, the tasks of one call’s arguments or one operation’s operands and what the main line computes beside them, or two runs of a par_iter() lambda (Part I, 8.1.2; Part II, 12.6); the touch sets decide whether they are independent. The same code refuses a binding the window changes while a task names it, naming the binding. Tasks of a limit: 1 form are not checked against each other. A task this compiler cannot account for is not refused (C.4). NK2105 data used after it was handed to something that keeps it: an argument the callee keeps, a key or a value written into a container, a field or an element of a literal, a let that renames it, an assignment. Inside a loop or a lambda the hand-over itself counts; a second use in the same statement, and a use of the part handed over or of the whole it was part of, count too. NK2106 a part of a value that is only lent here — a lent parameter, a for binding over a list, a let over a place — handed to something that keeps it: the owner still has it. NK2107 a lambda handed to a par_iter() walk changes a name bound outside it — an assignment, or a method that changes what it is called on: every core would write it at once (Part II, 12.6). Asked at both settings of user_parallelism; the way out is a map and a collect, or a SharedMut changed through update. NK2108 a part of a mut parameter or of mut self taken out and not given back on a way out of the function - its end, a return, a throw - or a throw or a call that can fail standing between the taking and the giving back (Part I, 6.5): the value is the caller’s and is whole whenever the caller can see it. The way out is to assign the part or the whole first, or to build the value by value, fn f(e: E) -> E. NK2109 a bound TaskHandle - an async(detached)’s, or one a call hands back - leaves its scope on some path without being taken by join, join(within:), detach or cancel, or handed on (Part I, 8.2). A join(within:) without on_timeout: task::OnTimeout::Cancel takes it only where it does not time out: in the handler of its task::TimedOut the handle is still live and is asked for on every path; the message names join() and detach() as the ways out. A child handle (async(handle)) is not asked: its group waits for it. NK2110 a task with nothing beside it: nothing runs between its start and its wait point or its group’s end - f(async g()) with no other argument computed beside it, let x = async g() named in the very next statement, an async statement that ends its group (Part I, 8.1.2); the help removes the word. NK2111 an async { … } that starts no task: its statements run in order and it waits for nothing; the help names async fn { … } for a task of several steps. NK2112 limit: on a form that starts one task, async e or a handle form. NK2113 and NK2114 are retired and not reused: task::cancel is removed, and a task is cancelled only through its handle (ADR-async-5 D14). NK2115 async before a function’s declaration, a let or a loop: whether a function pauses is inferred (Part I, 8.1), and async is a prefix of an expression. NK2116 and NK2117 are retired and not reused: the async loop is removed (ADR-async-5 D30). NK2118 a pending binding named after a catch where its failure arrived took it, on some path, where the async expression has no fallback catch; the help writes one after it. NK2119 (warning) a par_iter() chain the committed ledger recorded as running in pieces has a lambda that can now pause, so it runs one task per element; at the call that made it pause, with the calls that lead there (Part II, 12.6); committing the ledger acknowledges it. NK2120 an async form inside a loop’s body: async starts only tasks whose number stands in the source (Part I, 8.1.2); the help writes xs.par_iter().for_each fn(x) { … }. NK2121 a deferred handle (async(deferred)) that is neither started nor cancelled on some path, or started twice (Part I, 8.1.2). NK2122 a child handle (async(handle)) that leaves its group: returned past it, or stored in a value that outlives it (Part I, 8.1.2); the help writes async(detached).
NK22xx Locks & suspension NK2201 I/O while holding locked data (Part II, 12.2). Reading a fs::Mapped is a page fault, a disk read that neither suspends nor takes a lock, so NK2202 and NK2203 say nothing about it; inside a door it is a disk read with the lock held. Both read shapes are asked — a method on it and an index of it — and the claim is the type’s own touches column, so a second such type is a line in a ledger. A type whose column says nothing is not refused (C.4). The way out is reading what the block needs before the door. NK2202 a sync function called something that can pause (Part II, 12.1), answered from the ledger (13.5); and a call that can pause, or a for over a sequence whose step does, inside a door’s block, which would hold the lock across the wait (Part II, 12.2). A free call is resolved by name, and a method call by the type checker. NK2203 a lock taken while a lock is held: written one inside the other, reached through a chain of calls, or an async form inside the block, because its children run while the lock is held. The locks column propagates touches a lock over the call graph sync uses, with a spawn’s body excluded and a trailing lambda’s counted. A println takes standard output’s own lock and counts. Asked on Holds and never on the column’s third answer, where the runtime check applies (C.4). get and set hold nothing open, so neither is asked. The way out is asking for both at once: access_all(a, b) fn(x, y) { … } (Part II, 12.3). NK2204 an assignment to a SharedMut directly; the message names the door, kasse.set(42) for kasse = 42. NK2205 a set given a value that was seen in a lock, or standing under a condition that was: what a lock hands out is a Seen[T], the stamp travels with the value, and the message names update and set(…; after:). The get written inside the set is the smallest case. set(…; after: seen) is not asked: if the lock still holds what was seen, every decision taken on it still holds. NK2207 an update or update_all block that assigns to its mut v without reading it: a set through the back door, refused as one. NK2209 a call that can pause, inside a grammar’s action, or inside a fold’s init, step or merge, which is action code too. The same demand holds for a lambda of Par::fold, par_fold and par_pieces (Part II 12.6), and on a fold lambda the help names the chain map (pausing) followed by fold; a map, filter or for_each lambda of par_iter and a task may pause (Part II 12.6, Part I 8.1.2). Asked where the free call and the method call meet, and only where the ledger answered; a callee nothing describes is not refused (C.4). The message names the rule. NK2210 sync(f) names what is not code the call runs: a name that is no parameter, a parameter that is not a function, or one the function keeps (Part II 12.1, ADR-288 D31). NK2206 a lambda that pauses, handed to a parameter whose function type says sync: NK2202’s shape one level over. A lambda that does less fits a type that allows more, never the other way round. Asked of what the body’s calls say in the ledger; a callee nothing describes leaves it unasked (C.4). NK2208 set_after written by hand on a lock: it is how set(…; after: …) is lowered, and writing it directly would drop a failure nothing in the contracts describes (C.1). Worked through in C.6. NK2211 (warning) a pub function the committed ledger says could not pause ("inferred") can now, at the statement that made it and with the calls that lead there (ADR-288 D32); committing the ledger acknowledges it.
NK23xx Aliasing NK2301 cannot change a collection while looping over it (Part I, 6.8). NK2302 a body keeps a parameter not marked keep (Part I, 6.5): it stores the parameter, or a part of it, into something that outlives the call, gives it to a task, or hands it to a callee whose parameter keeps it. Keeping is inferred over the call graph and fails closed: a use the inference cannot resolve counts as keeping. The help adds keep (ADR-views-3 D2). A result that points into several parameters is not refused (Part I, 6.6). NK2303 is not a refusal: a view of a buffer a body made, or of anything it owns, may be handed out of it, and the buffer lives in the anchor of whatever holds its views; so does an argument made in a call whose result is a view of it. NK2304 what the tether cannot lower: one buffer handed both to a task and out of the function, which has no one owner; and a container of structs holding views that drops entries inside a loop, where the container is not a list or a view in the struct is not text (a list of structs of text views is held, one handle per buffer). In that last case a call on the subject is treated as keeping what it is given, which narrows the signature rather than refusing. NK2305 data changed in place while a view that may point into it is still used (Part I, 6.6): a method that changes the value, or an assignment to a part of it, between the call that made the view and a later use of the view. Reported at the change. The list a for walks is lent to its body (Part I 3.3): any change of it inside the loop (a method that changes it, an assignment to a part of it or to the whole) is this code, its label on the for head saying v is lent to this loop; reading it stays allowed. A view is also a name bound to an element or a field read off a place, or to a ?? whose answer is a view of its left side (m[k] ?? return, f.result ?? return with f a view), and it may point into the variable the place starts from and into whatever that variable views. A change to a field the view does not read, one that neither holds the place read nor lies inside it, is not reported. The same code refuses handing that data to a callee that takes it as its own (a parameter not lowered as a view, because the body keeps or changes it; push on a list too), reported at the call; its label says take keeps y and may change or discard it, and its help adds handing over a copy, take(y.clone()) (ADR-views-3 D9). The same code refuses moving that data into a field, an element or a variant’s value that must hold text of its own, because the program changes it in place or hands it to a callee that keeps it, in any function, reported at the move (ADR-views-3 D9): a label says Cursor.input must hold text of its own and a second marks the place that makes it so (c.input.push_str(..) in advance changes it in place), and the help names handing over a copy (Cursor { input: text.clone(), .. }) and building the value first and taking the view from its field. Where no view of the moved text is still used, the move is not this code (NK1106, NK2105 keep their cases). The message speaks of data, never of how long anything lives: the headline names the variable and the view, a label marks the call that made the view and the later use, a note names the callee’s way out that may hand back that argument, and the help names the two ways out, using the view before the change and taking a copy of it with .clone() before the change. Assigning the variable a new value, leaving its scope, moving it into another variable or into a struct, variant’s value, tuple or list the function builds, or passing it to a parameter lowered as a view is not a change in place and is not reported: the old buffer moves into the anchor of what holds the view, and a variable or place it moved into is held to the same rule.
NK24xx Contract changes NK2401 a borrow contract change broke a caller, narrated from the ledger diff (13.5). NK2402 (warning) an error that newly reaches a catch with else, or one that does not match on error, narrated from the same diff: such a handler takes everything that reaches it, so nothing is refused (a match that named every type is NK1151). The warning is at the call rather than at the catch, once, and the committed ledger diff is the acknowledgement. Reserved: the same over a boolean. NK2404 (warning) a pub function whose throws set gained a type since the committed ledger, at the statement that brings it in, with the calls that lead there: callers whose catch names every type stop building; committing the ledger acknowledges it (ADR-357 D4). NK2403 (warning) a parameter whose keeps changed since the committed ledger, on a type whose teardown does something (Drop or Cleanup, on it or on a field): the call that hands it a name is told where that name’s cleanup runs now, once. A backend error at a boundary — is not a future, a ? on a value that is not a Result, a Result where none was expected — is reported as the ledger of X does not match its sources, or the description of X does not match the crate, with the backend’s words as a note (ADR-100 D6).
NK25xx Portability The Send rules that parallel code needs, decided the same way at both values of user_parallelism, so that a library built at one stays usable at the other, and asked of a value and a destination, so the two codes below may answer differently: a lock goes into a task of the program’s own and not into code nothing describes. NK2501 a value that may not cross a thread is used by a task (Part II, 11.2): an error at user_parallelism = yes and a lint at no. NK2502 a value that may not cross a thread is handed to a call this compiler cannot see the end of: an error at both values. Worked through in C.5. NK2503 a call into foreign code from which a lock is reachable through its arguments, transitively and through the fields of a struct. A call that can reach no lock is allowed without a word, and the way out of one that can is keeping the lock out of its reach (15.2). Worked through in C.6. NK2504 a call, or a written type, reaching into a Rust crate no ledger describes. Once per crate, and only where the manifest declared the crate with type = "rust" (C.4). NK2505 a described crate whose sources have moved since the description was reviewed: the description is reviewed again, not derived again. Once per crate, and only where a recorded hash disagrees; a crate declared by version, and a description that recorded no hash, answer nothing moved. NK2506 a list or text handed to a Rust function that owns it (Vec<T>, String), which the compiler cannot follow back to where it was built in the package: a pub function’s parameter, a value read out of a shared value. The help names the .clone() to write; a copy is never inserted (15.2, ADR-327 D8).
NK26xx Failure declaration, resource cleanup & crash path NK2601 an impl Cleanup that is not the one method fn cleanup(mut self): another method, another shape, or a drop, which the message points at its own impl Drop (Part I, 6.4). NK2602 is retired: a value with a pausable cleanup dying where nothing may pause is the pause rules’ own case — NK2202 in a door, NK2209 in a fold lambda, NK2206 in a lambda handed to a sync function type — named as the cleanup of f (ADR-297 D3). NK2603 is retired and not reused: an expired cleanup-deadline is exit status 70 with the message on the panic path (Appendix A, ADR-297 D7-D8). NK2604 only the application may set the panic hook, and the hook must be sync (Part I, 7.2). NK2606 a lambda that can fail, handed to a parameter whose function type does not say throws: NK2605’s shape one level over, reported alone, without NK2605 beside it. Where the type does say throws, the failure travels to the caller and NK2605 applies. NK2607 is retired and not reused: process::exit throws a fatal error, which ends a task like any error (ADR-345 D5). NK2605 a written call that can fail, in a function that does not declare throws (Part I, 7.1): answered from the ledger (13.5), so it says which contract it read. The cleanup the compiler writes where a value dies is a call too, and a failing one is NK2605’s, named as the cleanup of f (Part I, 6.4). The same rule as NK2701.
NK27xx Implicit calls and sequences NK2701 a loop whose step can fail, in a function that does not declare throws. The same rule as a cleanup’s NK2605: where the language performs a call nobody wrote, a failure of it fails the enclosing function. NK2702 a sequence used after something took it — a walk, a let, an argument, or a loop or lambda that takes it again on its next turn. NK2703 a sequence asked for what it is not: walked from the back where it has no back end, or its length asked where it is not known. NK2704 a Some(…) pattern over a T?, and NK2705 a None pattern over a T?: a T? has no constructors, its value is the T itself and its nothing is null (Some(x) => is x =>, None => is null =>, ADR-352 D5); a type of the program’s own with a variant of that name keeps it.

Every NK code the compiler emits has a reproduction test and a worked example in the relevant chapter.

A code specified ahead of its check has no reproduction test.

NK2605 is reported for a call whose callee a ledger describes: a function in this program, one in another module of it, or one of std’s, by name or as a method on a receiver whose type is known. A call nothing describes is silence rather than approval, which is C.4’s property for every check here.

C.4. What a Type Error Looks Like

Two of the NK1xxx family, on a file that says io::read_to_string("input.txt") and puts a view of text it was handed in a published String field that text of its own also flows into:

error[NK1106]: `Reading.name` holds text of its own, but `city` is only lent.
  --> app.nika:8:5
   |
 8 |     return Reading { name: city, temp: 12 }
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: `city` is a lent parameter, so the text belongs to the caller, who still has it.
   = note: `Reading` keeps its `name` after this line, so it needs text of its own.
   = note: Nikaia never copies text behind your back: a copy costs as much as the text is long, so it's written where it happens.
   = help: Declare `keep city: String` so the caller hands its text over, or write `city.clone()` to copy it here.
error[NK1101]: `io::read_to_string` takes 0 arguments, but you passed 1.
   --> app.nika:12:5
    |
 12 |     let text = io::read_to_string("input.txt")
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: It's declared as `io::read_to_string() -> String`.
    = help: Call it without arguments: `io::read_to_string()`.

The note is the contract, quoted from the ledger: the compiler shows the caller what the callee promised. The underline is on the statement, not the expression: this checker and NK2202 report at statement granularity, and a message that knows the word it is about underlines that word. Where the compiler could have written the fix and did not, it says why: the text refusal names whose text it is, what keeps it, and what a copy made on its own would cost, and leads with the answer that copies nothing. The help is paste-ready, as C.2 requires: .clone() for text, as i64 between numbers, and the nearest existing field when a name is close to one that exists.

A type is known, or the expression is refused. An expression whose type the compiler cannot tell is NK1245. Not asked of what its uses type later: a number literal, a number nothing typed (Part I 2.4), an integer comptime without a type. Not asked of an operator, a branch, a block or a jump, which are unknown only because a part of them is, and not again where a part inside was refused: one cause, one refusal. An if or a match whose arms all have a type and disagree is asked, and the message names the arms’ types; where the value goes into a position with a type, each arm is a value written there instead (NK1102, NK1103, NK1104, NK1106). Where the file holds another error, NK1245 is not said: a value another refusal left without a type is that refusal’s. A value whose type differs per unrolling, field.of(value) over T::fields, is asked where it is unrolled. A name is asked where it is bound (its let, its loop, the place its lambda stands), not where it is read, and neither is a member of one bound without a type. What a number nothing typed passes through is as open as the number: a generic call or a member that hands it back (hand(7), Holder { value: 21 }.value, a task’s join(), an element of a list nothing typed), and x ?? 0 or x ?? return over a T? whose T nothing typed. asset("…") is what its comptime declares. What a DSL driver hands back (...args: Self::dsl) and its members are a type of each call site’s own, asked where it is lowered. A call through a package whose ledger the build does not read (a dependency’s own dependency, or a crate nothing describes) is asked by the build that reads it, and a dsl block for a language no grammar is, or an entry a grammar does not have, is refused where it is lowered, in words that name what is missing.

A member is written down, or it does not exist. Where the type of a receiver or the head of a path is known, what can be called on it is what the program declares, what std’s ledger lists, what a crate’s description holds and what an extern block declares. A method, an associated function, a module’s function or a field none of them holds is refused with NK1171, also where the backend has one by that name:

error[NK1171]: `String` has no function `from`.
  --> app.nika:2:13
   |
 2 |     let t = String::from("x")
   |             ^^^^^^^^^^^^
   |
   = help: A text literal is already a `String`: write `"x"`, or `"x".clone()` for text of its own.

A hole is code, and is checked like code. The expression inside f"total is {stock::total(items)}", and inside a dsl html template’s {…}, goes through the same path as a statement, so NK1101 and the rest say the same thing about it that they would say about the same expression written on a line of its own. The sync analysis reads holes too, in both directions: a pausing call inside one costs an inferred sync and contradicts an asserted one. A hole whose text does not parse is a parse error in an f"…" (ADR-309 D8) and is reported by the emitter in a template, and the checker raises no second error for it.

C.5. What a Crossing Refused Looks Like

The NK25xx codes cover the places a value the program wrote reaches another thread. One question decides them, may a value of this type go to this destination?, asked of the value’s type and of where it is going. Each destination’s answer does not depend on which build this is.

The codes do not share one verdict. Into a task of the program’s own a lock may go, at both values. Into code nothing written down describes it may not, at both values. NK2501 therefore refuses nothing a Nikaia program can write, and NK2502 refuses the shared value — a Shared[T], whose count is chosen per value and so has no one shape a foreign signature could name, and a described type that says crosses = false. A lock is the third, and it has a code of its own: the refusal there is about the call and not the value, so it is NK2503 and C.6 (15.2). One walk answers all three, and the reason it returns picks the code: a Shared[T] handed to an undescribed call gets NK2502, and a SharedMut[T] or a Locked[T] gets NK2503. No type a program can write reaches NK2501’s shape: the Held below is a type nothing describes.

A task runs somewhere else, so everything it uses goes with it:

error[NK2501]: This task uses `counts`, which can't be passed to a task.
  --> app.nika:7:5
   |
 7 |     async(detached) fn { total(counts) }
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: A task runs on its own thread, so everything it uses has to be able to move between threads.
   = note: `Held[i64]` is described as a value that can't move to another thread.
   = note: This is checked even when the program runs on one thread, so code stays correct when `user-parallelism` is turned on.
   = help: Keep it here, and pass the call only what it needs from it.

A lock goes into a task of the program’s own, and everything else a program can write goes with it. The shape above is what a type that answers may not gets.

A call whose body the compiler cannot see may start a thread of its own (15.2):

error[NK2502]: `counter` can't move to another thread, and `hyper_shim::across_a_thread` might move it.
   --> app.nika:14:5
    |
 14 |     let crossed = hyper_shim::across_a_thread(counter)
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: The compiler knows nothing about `hyper_shim::across_a_thread`, so it has to assume it might start a thread of its own.
    = note: `Shared[i64]` is shared, and how a shared value is counted is decided per value, so code outside Nikaia can't be written to handle it.
    = note: This is checked even when the program runs on one thread, so code stays correct when `user-parallelism` is turned on.
    = help: Pass what the shared value holds, a view or a copy, instead of the shared value itself.

The way out is one line. The caller passes what is inside — a view of it or a copy — so the foreign function sees an ordinary value (Part I 6.2). The same shape is the way out of NK2503 (C.6). The message states that the refusal is deliberate.

The pair follows four rules.

The rule is structural and transitive. A struct with one field that may not cross may not cross, and the note names the field that decided it rather than the struct. The fields come from the ledger (13.5), so the rule reaches a type declared in another file.

Three answers. A type may cross, may not, or nothing written down says. The third is not permission and not a refusal (C.4). An undecided crossing is handed on: rustc still type-checks the emitted crate, and the trait-bound error it raises is reported against the .nika line by the translation C.1 requires. A library may settle one of its own types with a line in its ledger. The same third answer governs whether a call into foreign code can reach a lock (15.2): an undecided type is not a type with no lock in it, and a call is allowed silently only when its arguments reach nothing.

One verdict per destination, two severities. At user_parallelism = no no user code runs concurrently, so the task above does not run and NK2501 is a lint, with a note saying which of the two it is. NK2502 is not downgraded, because a foreign runtime’s threads run whatever the build option says. Each destination’s verdict is the same at both values; only the severity differs.

The crossing the compiler chooses for itself gets no diagnostic. A child task that never pauses runs on the pool, so what it hands back crosses a thread. Where that cannot be shown, the task runs on its group’s thread instead, and --overlaps lists it. That task is the program’s own code, the same destination a free task is: a result that holds a lock still runs beside its window.

C.6. What a Refused Lock Looks Like

Five refusals come with the rule that a lock may not be taken while a lock is held, with the doors shared mutable state is reached through, and with a foreign call that could reach a lock. Each names a way out, as C.2 requires, and each way out is one line of code. The shapes below are what the codes print (C.3).

A lock taken inside a lock, which is what access_all exists for (Part II, 12.3):

error[NK2203]: `update` takes a lock, but you're already holding one here.
  --> main.nika:9:19
   |
 9 |         account_b.update fn(mut to) { to.balance += 100 }
   |                   ^^^^^^ takes a second lock
   |
   = note: This block runs while a lock is held, so taking a second lock inside it can deadlock.
   = help: Take both locks at once with `access_all(a, b) fn(x, y) { … }`, or compute the value before the block and pass it in.

A chain reads the same, with one note more: it names the call, and the function inside it that takes the lock. A scope opened inside the block is the same refusal: the scope waits for its tasks, so a task waiting for the held lock waits for the block that is waiting for it.

The two that come with the doors:

error[NK2204]: You can't assign to `kasse` directly: it holds shared mutable state.
  --> main.nika:4:5
   |
 4 |     kasse = 42
   |     ^^^^^^^^^^
   |
   = note: Changing shared state goes through a method that takes the lock.
   = help: Write `kasse.set(42)`.
error[NK2205]: This `set` stores a value that was read from `kasse` earlier, so the lock is taken twice.
  --> main.nika:6:5
   |
 6 |     kasse.set(kasse.get() + 100)
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: A value read from a lock is out of date as soon as the lock is released: anything can change between the read and the store.
   = note: This is found wherever the value was read: on the line above, in another function, or in another request.
   = help: Write `kasse.update fn(mut v) { … }`, which reads and changes the value while holding the lock.

The second one reads the stamp a value carries out of a lock: the inline get is its smallest case, and the same pair spread over two lines, two functions or two requests is the same refusal, with the note naming where the value was seen.

The lowering of a door, written as a door. set_after is a function in the language below; written directly it would take the program’s two arguments, drop the failure nobody declared, and leave the backend to report against a generated file (C.1):

error[NK2208]: `kasse` has no `set_after`. Write `set(…; after: …)` instead.
  --> main.nika:5:5
   |
 5 |     kasse.set_after(stand + 1, stand)
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |
   = note: `set` with `after:` compares and stores while holding the lock once.
   = note: Written like this, a failure would be silently dropped.
   = help: Write `kasse.set(neu; after: seen)`, where `seen` is the value you read from the lock.

The foreign call, judged by what its arguments can reach (15.2):

error[NK2503]: `hyper_shim::render` could reach a lock through `state`.
   --> main.nika:12:5
    |
 12 |     hyper_shim::render(state)
    |     ^^^^^^^^^^^^^^^^^^^^^^^^^
    |
    = note: The compiler knows nothing about `hyper_shim::render`, so it can't see what it does with what you pass it.
    = note: `state.counts` is a `SharedMut[i64]`, and code that might keep a lock could deadlock.
    = note: This is checked even when the program runs on one thread, so code stays correct when `user-parallelism` is turned on.
    = help: Pass it a copy of what it needs instead of the container:
           hyper_shim::render(state.counts.get())

The note names the field that decided it rather than the struct, as NK2501’s does: the fields come from the ledger (13.5), so the rule reaches a type declared in another file. A call whose arguments can reach no lock gets no diagnostic and no note. It is allowed silently, which is not the same as a call whose contents nobody wrote down (C.5).

The walk is NK2502’s, asked once per argument. The way out prints the path it found — the argument’s own name with the field that decided it behind it — where the argument is a name or a chain of fields, and states the general form otherwise.

This site is open source. Improve this page.