Status: Accepted
Related: ADR-005 D3 (the Borrow Contract Ledger this extends),
ADR-283 (views and what tethers them),
ADR-010 (provenance decides the hasher),
ADR-288 (what earns the sync D2 records)
Part III 13.5 specifies nikaia.contracts in detail — its format, its
determinism guarantee, --locked, and that a published package ships its
ledger so a consumer builds against contracts rather than guesses.
Without it, two things the specification promises cannot be checked. ADR-019 D2
says a sync function cannot call io::read_to_string, and without a ledger
the compiler has no way to know what io::read_to_string is: std is a Rust
crate to it. ADR-010 says a map’s
hasher follows the provenance of its keys, and provenance has to come from
somewhere — a call whose result is a buffer.
Both need the same thing: a place where what a caller must know about a body it cannot see is written down, for this program and for every library it uses.
Changed by ADR-288 D5: the header of the derivation lives in nikaia.derived beside the contract.
An inference that reads signatures and one that reads bodies both produce a ledger, and a reader must be able to tell them apart — so the header carries it:
version = 1
inference = "stage0-signatures+sync-bodies"A later compiler writes a different name there, and --locked fails on the
difference rather than quietly accepting the weaker answer as the stronger one.
The alternative — leaving it out and hoping the version implies it — is how a
file that is supposed to be a memory starts lying.
sync and throws go in it, not only borrows.The file is called the Borrow Contract Ledger because ADR-005 was about borrows. But the question it answers is “what must a caller know about a body it cannot see”, and may it pause and may it fail are two more answers to exactly that question, needed by exactly the same callers.
Recording only borrows would mean a second file for the second question, with
the same determinism rules, the same --locked, and the same distribution
story. One file.
sync means not sync; an absent entry means nothing is known.This is the distinction the whole thing rests on. A caller that finds an entry
without sync knows the callee may pause. A caller that finds no entry knows
nothing and may not assume.
It is also what makes the file worth shipping rather than deriving: a consumer
cannot infer io::read_to_string’s contract, so the library has to state it.
sync = false on every entry would treble the file and say nothing. A diff of
this file should show a promise being made or withdrawn, and a column of
falses buries that in noise.
std is half Rust. A compiler that does not read Rust cannot infer fs::map’s
contract, and building a second frontend to do so would be a large amount of
work to derive twelve lines.
So crates/nikaia-std/std.contracts has both, in one file, marked: the entries
for modules written in Nikaia are inferred from their sources, and
crates/nikaia/tests/contracts.rs regenerates them and fails if the file has
drifted; the entries for the modules still written in Rust are written by hand
and reviewed like code. The hand-written share is a measure of how much of
std is still Rust, and shrinks as ADR-014 proceeds.
A hand-maintained copy of a derived truth goes stale, which is why only the part that cannot be derived is hand-maintained, and the part that can is tested.
fs::map, io::read_to_string, Stats::add, fs::Mapped::deref. The
anonymous constructor of Kap 4.2 is Type::new, because that is what the
lowering names it and therefore what a caller reaches.
rustc’s.sync, throws and the borrow contract are decided by this compiler and never
by the one it emits Rust for. A ledger diff blamed on “the toolchain” must name
the toolchain that actually inferred it, or the narration of 13.5 points at the
wrong thing.
The sync check has what it needs. Part II 12.1’s rule — a sync function
may only call sync functions — is a lookup: with std’s ledger a call to
io::read_to_string from a sync function is a fact the compiler finds, and
NK2202 is what it says about it. A method call resolves through the type
checker (ADR-288 D7).
Provenance has a place to be recorded. ADR-010’s sources are contracts of
exactly this kind — fs::map yields Trusted, an HTTP body yields Untrusted —
and the ledger is where they are written.
The type checker has its signature store. Parameter and result types are two
more keys on an entry, signature and fields (ADR-024), not a
second file.
sync from the body — looking for I/O calls and marking the
function accordingly.
Changed by ADR-288 D1: sync is inferred from the body for
every function; a written sync is an assertion the inference never
overwrites (ADR-288 D4), and across a package only what is
written is promised (ADR-288 D28). That is the check, not the contract: sync is a
promise the author makes about what a function is for, and the check is what
holds them to it. Inferring it would mean a function silently stops being
sync when someone adds a call, and its callers break with no line to point
at.--locked, same distribution story, three times.std’s Rust sources to infer their contracts. A second frontend
for a language this compiler does not compile, to derive what twelve reviewed
lines say.sync = false. D4.