Seen[T], and Nothing Stamped Goes Back In BlindStatus: Superseded by ADR-281 — its D1-D6 are D22-D27 there
Date: September 16, 2026
Target Version: Nikaia 0.0.8
Related: ADR-110 (update fn(mut v), the door that decides
inside the lock), ADR-099 D3 (NK2205, which this widens),
ADR-039 D10 (the four doors), ADR-059 (access
reads), ADR-065 (update_all), ADR-067 D1 and
ADR-033 (touches, the column the pass-through rule reads),
ADR-108 (the same shape of answer: no analysis, a type),
ADR-005 Group B (the same verdict at both settings), Part I 6.3,
Part II 12.2, Part III 13.5
The lost update is written in two lines, and the specification’s own refusal saw one:
let stand = kasse.get() // lock open, read, lock closed
// … a pause, another task, another core …
kasse.set(stand + 100) // lock open, store, lock closedBetween the lines the lock is open. At yes another thread writes in the
gap; at no another task does, as soon as anything between the lines pauses.
The value stored was computed from a state that no longer holds, and nothing
says so — not at build time, not at run time, not in a log. NK2205 refused
kasse.set(kasse.get() + 100) and, being syntactic, taught the two-line
form. The second shape of the same mistake, check then act —
if stand > 100 { kasse.set(0) } — was never refused at all, and it is the
one that breaks rarely and late, which is where a language loses the trust
its doors promised.
Four ways to close it were weighed. A dataflow pass over one body catches the
two lines and stops at the function boundary, which is half a helmet. A pass
across calls needs ledger columns and a fixpoint, and still stops at time: a
value read in one request, kept in a struct, and written in the next is not a
shape any analysis sees. A witness at run time — a version carried with
the value and compared at set — sees through time, but reports the collision
when it happens and costs a counter per lock and sixteen bytes per value. And
a stamp in the type: what leaves a lock carries a mark, the mark travels
with the value through calls, fields and time because types do, and the only
thing the mark forbids is going back into a lock blind.
The stamp is the answer, for the reason the bank gives: you may open the box, look, take a copy out, and do your business anywhere — but what you carried out does not go back into a box unnoticed. It costs nothing at run time, it is complete where the analyses were partial, and it has no way off, because a mark that can be removed with one word is Perl’s taint again: somebody removes it early, to make the types fit, and three functions later nobody remembers.
Seen[T], and the emitter erases it.kasse.get() is a Seen[i64]. The result of kasse.access fn(v) { … } is
a Seen of what the block computed, and so is access_all’s. Seen[T] is a
type in the checker and in the ledger’s type language (Part III 13.5), and it
is not a type in the language below: a Seen[i64] is lowered as an
i64, a field declared Seen[i64] is an i64 field, a signature with Seen
in it is one without. No counter, no marker, no check at run time, no bytes.
stand + 100 is a Seen[i64]; stand > 100 is a Seen[bool]; stand.abs()
and max(stand, limit) are Seen. A call whose argument is stamped is
allowed where the callee’s touches column names no lock — it cannot put the
value into one — and its result is stamped. That covers every sink: f"…",
println, fs::write’s data, a response body, a serialiser. A Seen reaches
the world without a word written for it.
A callee whose touches names a lock, or whose touches is absent (which the
column reads as touches everything, ADR-033), takes a Seen
only where its signature says Seen — because it could write the value into
the lock it touches, and that is D3’s second place.
Seen is written at two places and inferred everywhere else.A struct field that keeps a value read from a lock is declared Seen[T],
because a field is where the value outlives the moment it was read. A
parameter of a function that touches a lock is declared Seen[T] where a
stamped value is to be passed in. A local, an expression, an argument to a
lock-free function and a return value are inferred as every other type is.
NK2205, first shape: a set given a stamped value.
kasse.set(stand + 100), whether stand was read on the line above, in
another function, or in another request.NK2205, second shape: a set under a stamped condition.
if stand > 100 { kasse.set(0) } — the value stored is plain, the decision
is not. A while, a match and a nested if are conditions alike.NK2207: an update or update_all block that assigns to its mut v
without reading it. update fn(mut v) { v = n } is a set through the
back door and is refused as one; a block that reads v — v += n,
v.push(e), if v > 100 { v = 0 } — decides inside the lock and is the
door for that.set therefore takes an unstamped value and stands under no stamped
condition: a starting value, a configuration that arrived from outside, a
reset an operator asked for. There is no .value, no overwrite, and no
word that turns a Seen[T] into a T. The one place a human judges is a
foreign crate’s touches line, which ADR-104 already has
reviewed by hand.
set(neu; after: seen) is the one door for a stamped value, and it is a definition.kasse.set(neu; after: stand)
// is, by definition,
kasse.update fn(mut v) { if v == stand { v = neu } else { throw Overtaken } }The witness is the value itself: store neu if the lock still holds what I
saw. With after: the stored value may be stamped and the call may stand
under a stamped condition, because the witness covers both — if the value is
still the one seen, every decision taken on it still holds. T must be
comparable, the witness is a Seen[T], and Overtaken is an error like any
other: caught or declared, retried in a loop with catch { continue } — the
one catch this language has takes everything, and where the only failure
that can reach it is Overtaken that is exact — or handed to the caller,
which in a server is the honest 409.
On a word-sized value this is ADR-110 D2’s compare-and-swap
without the retry. On a large value it is a comparison of the whole value,
and the message says so: for a ten-thousand-entry list the hand-written
update block with a version field of the program’s own is the form.
yes and at no.A two-line update at no with no pause between the lines would in fact be
safe, and it is refused all the same, because the refusal is about the
shape and not about the clock (ADR-005 Group B: no switch
reaches a verdict). Read-modify-write through two doors is what update is
for, at every setting.
update, or after:.Overtaken exists only where a program wrote
after:.b.set(a.get()), copying one lock into another, is refused — the
value is stamped — and the form for it is update_all(a, b) fn(mut x, mut y)
{ y = x }, which is also the one that reads a consistent pair.Seen[…] at a field that keeps a read value over
time, and at a parameter of a function that touches a lock. Nowhere else.NK2205 keeps its number and grows: the inline get inside a set is
the first shape’s smallest case.touches; three refusals; one option on
set with one error type; the emitter erasing the attribute.a.set(x; after: b_seen) compares a’s
value with what was seen in b; the stamp does not say which lock it came
from. It is a logic error, loud in practice — it almost always throws — and
a type that names its lock is a later decision if it is ever needed.; on some later day and changes nothing here.Seen means to a foreign crate. At the boundary a Seen[T] is a
T, and whether the crate writes it into a lock is what its reviewed
touches line says.D1, D2, D3 and D4. Seen[T] is a type in the checker and in the ledger’s
type language and not one below — the emitter erases it, so a Seen[i64]
is an i64, a field declared Seen[i64] is an i64 field, and a signature
with Seen in it is one without. get is -> Seen[$T] in std.contracts,
and what access and access_all hand back is stamped too.
The stamp sticks through an operator, through a comparison, and through a
call whose callee’s touches names no lock — with its result stamped in turn,
which is what makes kasse.set(bumped(stand)) the same answer as
kasse.set(stand + 1) without an analysis following the value. A callee
whose touches is absent reads as touches everything
(ADR-033) and hands back a plain value: the wrong answer that way
costs a refusal that is not raised, and the wrong answer the other way refuses
a program.
All three refusals. NK2205 in both shapes — the value and the condition —
and NK2207 for an update block that replaces its mut v without reading
it.
What the old NK2205 was. It asked whether the argument contained a get
on the same container, which caught one line and nothing else. Two things
it let through are refused now: the same pair spread over two lines, which
it called a question about what happened between two statements; and a value
read from another lock, because set’s own touches names one, so by D2
it takes a Seen only where its signature says Seen — and it does not. The
stamp does not record which lock, and that is the design rather than a limit.
Two things the record had not said, each found by a test:
v = v + 1
mentions v and decides inside the lock exactly as v += 1 does; a first
build of NK2207 looked only at whether the statement was a whole-name
assignment and refused it.if under a
stamped one is still under it, and a plain condition inside does not clear
the outer one.D5. kasse.set(neu; after: stand) is a different entry and not an
option on set: the ledger carries Locked::set(after) and
SharedMut::set(after), keyed by the way the call is written. Two things
follow from it being an entry. The witness is checked, lent and stamped through
the one path every argument goes through, because it is an argument of that
entry. And the door carries throws = ["Overtaken"], so the failure propagates
the way every other one does — NK2605 where the caller has not declared
throws, a ? in the lowering, and a catch that takes the Result instead.
The relaxation is the witness’s and nothing else’s. NK2205 asks of set,
and set(after) is not set — the ledger’s own name is what decides, because
the name is what already says which operation this is. So the stored value may
be stamped and the call may stand under a stamped condition, and the same two
programs without the witness are refused exactly as they were.
It lowers to one acquisition: set_after(neu, stand), a std door that
compares and stores while the lock is open once, in both shapes
(ADR-057 D4). Overtaken is a Rust error type that carries
nothing, for a reason worth writing down — the value in the lock now is not
in it, because reading it would be a second acquisition, and a caller that
wants it takes the door again and gets a fresh stamp.
Two things the record had not said, each found by reading the lowering back.
The witness is a view and the value is not, which is the difference between
what is stored and what is only read. A witness taken by value is moved out
of the caller, and reading what was seen after asking whether it still holds is
an ordinary thing to write — a witness larger than a word did exactly that and
met rustc about a file nobody wrote (Part III C.1). So the ledger says
seen: &$T, and the & is the compiler’s to write as it is everywhere else
(ADR-094 D1). It is written by the emitter rather than looked up,
because lends withholds its claim on every method argument — the emitter
cannot resolve a receiver (ADR-028) — and this one position needs
no resolving: the checker has already said the call is the door. A & somebody
wrote is NK1137, for the same reason it is one anywhere else.
The lowering is reachable by name. The
Rust name is reachable from above: kasse.set_after(a, b) would have been a
method that exists, takes two arguments, hands back a Result nothing in the
ledger describes — so the failure would be dropped and rustc would warn
about a file nobody wrote (Part III C.1). NK2208 is what that meets, and it
is the cheap half of one door: there is no second entrance to the compare,
and therefore none around the stamp.
What D5 also says and is not built is ADR-110 D2’s compare-and-swap for a word-sized value, which is that record’s speed row and is named there. The door is correct without it and pays a lock acquisition for what a word could do with one instruction.
A catch that names the error it takes — so that a program could retry
Overtaken and let a disk error past — does not exist, and no program in the
corpus needs it; D5’s retry is the untyped catch, which is exact where
Overtaken is the only failure. The day a program wants to retry one failure
and not another, a typed handler is a record of its own.