ADR-067: sync Means One Thing — Never Pauses — and touches Gets the Inference It Was Written For

Status: Superseded by ADR-288 — its D1-D3 are D21-D23 there Corrects: Part II 12.1 and 12.2’s prose, which promised that sync also forbids I/O Completes: ADR-033 D2 and D4 — the column and its polarity were specified and never inferred Related: ADR-027 (sync is earned from the body), ADR-006 D6 (the panic hook must be sync and may block), ADR-039 D3 (the lock-touching property this makes possible), D4 (why it says a lock and never which)

1. Context

A program was run, not argued:

let k = SharedMut(0)
k.update fn(alt) {
    println(f"ich laufe: {alt}")     // prints
    return alt + 1
}

It compiles and prints. Two things follow, and the second is worse than the first.

sync does not forbid an effect. std.contracts has println as sync = true with touches = ["stdout write"], and that entry is right for what sync is used for: the column decides whether the emitted Rust is an async fn or a plain one (ADR-055), and println writes and returns — it never suspends.

And println takes a lock. Standard output is behind a global one. So a print inside a door is a lock taken while a lock is held — exactly the nesting ADR-039 D2 refuses, and the refusal is not built. (Rust’s stdout lock is re-entrant, which is why nothing has hung: a print inside a print does not deadlock itself. It does not make the nesting sound.)

But Part II says sync means more. 12.1: “sync guarantees: I will never pause, I will never do I/O”, and “it cannot call standard functions (which might perform I/O)”. 12.2: “a sync lambda can never perform I/O and can never pause”.

The records disagree with the page, and they agree with each other. Three of them use the word and every reason given is about pausing — ADR-005 D6, ADR-027, and ADR-006 D6, whose panic hook “must be sync” because “mid-panic there is no runtime to pause on” and which may block. A property that permits blocking is not “a pure CPU task”.

And the column that should have answered the second question has no inference. sync, throws and sharing are each read off a body over the call graph. touches was specified with the same fail-closed polarity (ADR-033 D4) and was only ever hand-written in std’s ledger — so every function a .nika file declared answered “nobody said”, which means “it touches everything”. Safe, and useless: the walk stopped at the first call out of std.

2. Decisions

D1 — sync promises one thing: it never pauses.

Part II 12.1 and 12.2 are corrected. What a function reaches is a different question with a different column, and conflating them is what let a print into a door with the page saying it could not be there.

The alternative was to take println out of sync, which is where the page’s promise points. It costs the panic hook, which must be sync and must be able to write a crash report; and it makes every function that prints async, for a suspension that does not happen. That is a large price for a word.

One word, one promise. This session is the second time a word carrying two of them cost a day — ADR-064 D1 is the first — and the rule is worth stating once: a name in this language answers one question, and a second question gets a second name.

D2 — touches is inferred from the body, like the three columns beside it.

The fourth derived column gets the pass it was written for. A greatest fixpoint over the call graph, for ADR-027’s reason: start from “it touches nothing” and take the claim away from anything that reaches a function without one. Mutual recursion between two functions that touch nothing keeps the claim.

The polarity is the column’s own (ADR-033 D4): a call nothing describes, a construct that runs something, or a described callee whose own touch set is “nobody said” leaves the caller unknown, and no fixpoint brings the claim back. An empty set is an answer; an absent one is not.

A resource named by a parameter does not travel yet. fs::read touches file(path) and path is its parameter: a caller’s argument may be a literal, or a parameter of its own under another name. Mapping one onto the other is a piece of work of its own, and until it is done such a callee leaves the caller unknown — conservative in the direction this column is conservative in, and the one thing that keeps overlap from getting sharper across user code today.

D3 — A lock is a resource, and lock joins the vocabulary.

ADR-033 D2’s own table named it; touch.rs kept it out under the rule that a word waits until a program asks for it, “neither function exists”. Both exist now (ADR-064, ADR-065), and a program asks.

It names no parameter, which is ADR-039 D4’s decision and not a limit here: the property says a lock and never which, because telling two handles apart would make whether a program compiles depend on whether that proof happened to succeed. get, access and access_all are reads and do not conflict with each other; set, update and update_all are writes and do.

3. Consequences

One missing pass, three consumers. The lock-touching property (ADR-039 D3) that refuses a lock inside a lock now has the fact it needs — measured: a function whose body prints inside an update reports ["lock write", "stdout write"], which is the nesting written down. overlap can prove disjointness past a call into user code. And “touches nothing, and it is known” is very nearly “repeating it is unobservable”, which is the property ADR-039 §3’s retry route was waiting on (lock-free.md).

No new promise was added to do it. Neither pure nor repeatable is a word this language now has. pure is more than any of the three consumers need — a retry recomputes, so it wants no effect rather than the same answer — and a third promise beside sync and touches is how this went wrong the first time.

std’s own ledger says touches = [] for its one .nika function, because the shipped entry is checked against the source that produces it and the inference now reads that source. An empty list there is a claim and reads as one.

4. What this does not decide

• Whether a lock inside a lock is refused. The fact is available now; the refusal (ADR-039 D2, D3, NK2203) is still catalogued and not emitted. So is NK2201, which is what would refuse the print.
• Whether a block may be repeated, and therefore the lock-free shape. The question is on open-decisions.md with the measurement beside it; what this changes is that its missing half is now a derivation away rather than a vocabulary away.
• Mapping a callee’s parameter onto a caller’s argument, which D2 names and leaves.
• The clock. Nothing in std reads one yet, so it is not a gap — but a repetition would see a different time, and “touches nothing” must not quietly cover that when one arrives.

5. What is built

All three. contracts::touch::infer runs in Ledger::infer beside sync, throws and sharing, reusing the one call walk the checker and sync already share (ADR-028’s rule that there is one answer to what a call goes to). lock is in KINDS and on all ten doors in std.contracts. Part II 12.1 and 12.2 say never pauses and point at the second column for the rest.

crates/nikaia/tests/touches.rs is seven programs: a body that reaches nothing says so, what a callee reaches travels up, a door reaches a lock, a print inside a door reaches both, a call nothing describes takes the claim away, a parameter-named resource does not travel, and mutual recursion that reaches nothing keeps the claim.

This site is open source. Improve this page.