Status: Superseded by ADR-281 — its D1-D2 are D34-D35 there
Date: September 20, 2026
Target Version: Nikaia 0.0.88
Related: ADR-067 D1 (which split the sentence and left this
question), ADR-039 D2 (NK2203), ADR-027 D2
(NK2202), ADR-025 D6 (iterates, the precedent for a column on
a type), ADR-033 (the touches vocabulary),
ADR-016 (what a mapping is), ADR-010 D1 and
Part III C.4 (why silence is not a claim),
Part II 12.2
Part II 12.2 says no I/O while holding locked data, and
ADR-067 D1 split that sentence in two: what pauses inside a
door is NK2202’s, what takes a lock is NK2203’s, and a println is the
second. It then left the remainder as a question rather than a code:
What a third code would add is I/O that neither pauses nor takes a lock, and whether any exists is a question to answer before writing one.
Measured, of the nine entries in std’s ledger whose touch set names I/O:
| entries | sync |
locks |
which code |
|---|---|---|---|
print, println, eprint, eprintln |
yes | yes | NK2203 |
fs::map, fs::read, fs::read_to_string, fs::write |
— | — | NK2202 |
reading a fs::Mapped |
yes | — | neither |
A mapping is a file held as memory (ADR-016): the pages arrive as
they are touched. So mapped[i] is a page fault — a disk read that neither
suspends nor takes a lock — and inside an open door it is a disk read with the
lock held, which nothing said a word about.
And it is free today. No program in examples/, in tests/ or in
benches/ opens a door at all, which is the cheap case for a
refusal: free before programs exist, breaking afterwards.
touches.The same column std’s functions carry (ADR-033’s resource
kinds), on the type. fs::Mapped says touches = ["file read"].
On the type rather than on a function, and that is the whole reason it is a
new column: mapped[i] calls nothing a program wrote, so there is no call
site to hang a function’s touches on. That is the same shape as
iterates = "throws" on io::Lines (ADR-025 D6) — a fact about a
type that makes an analysis treat operations on it differently, recorded rather
than inferred because the body is Rust.
Written by hand and never inferred, like crosses: a struct a .nika
file declares reads nothing when it is read, because a field access is memory.
And silence is not a claim. A type with no touches is one nobody answered
for. Everywhere else in this compiler the absence of a claim is read
fail-closed (ADR-010 D1); here it may not be, because the thing
built on it is a refusal, and refusing on doubt refuses correct programs
(C.4). The polarity follows what is at stake, which
is ADR-027 D2’s own arrangement one question over.
NK2201.Both shapes of read: a method on it and an index of it. The message names the page fault, says why the other two codes are silent, and hands over the way out — read what the block needs before the door and hand the value in, so the block works on memory that is already there.
It is counted on a line of its own in the tally, beside the two NK21xx rules
and the walked sequence, and for their stated reason: the tally has to say what
it counted, and a place that can fail without saying so is not what this is.
std.contracts and nothing in the compiler.fs::Mapped outside a door, which is most of what a
mapping is for: examples/1brc.nika reads one end to end and takes no lock.Both decisions. crates/nikaia/tests/io_under_a_lock.rs holds seven: the method
and the index refused inside a door, the message’s three parts, a mapping read
outside a door untouched, a door over memory untouched, a type that says
nothing claimed nothing about, and the claim itself read out of the shipped
ledger — including that fs::Mapped is the only type that carries it, which is
the measurement this record rests on.