sync Is Earned, Not EnteredStatus: Superseded by ADR-288 — its D1-D6 are D1-D6 there
Related: ADR-020 (the ledger the inference writes to),
ADR-010 D1 (the same polarity question, answered the same way),
ADR-008 D6 (@borrowed: an assertion you write where you want a
property held), ADR-005 D6 and D8,
ADR-029 (answers §7’s second item)
Part II 12.1 gives sync one rule — a sync function may only call sync functions — and
crates/nikaia/src/contracts/sync.rs has checked it since ADR-020 gave it a ledger to ask.
The rule is right. The default was backwards, and it took building the check to see it.
Every construct in Chapter 12 that makes concurrency safe does it by demanding a sync lambda:
| construct | why it demands sync |
|---|---|
access, access_all (12.2) |
you must not pause while holding locked data |
par_iter (12.6) |
the body runs on a CPU core, not an event loop |
task::scope where its children run in parallel (12.7) |
the scope can only wait out tasks that finish on their own |
| the panic hook (Part I, 7.2) | mid-panic there is nothing to pause on |
So sync is not a niche annotation for hot loops. It is the gate on every safe concurrency
primitive the language has. And it was opt-in.
A function got sync in the ledger if and only if someone typed the word. So:
fn bonus(score: i32) -> i32 { score * 2 + 1 }
fn tally(p: &Player) -> i32 sync {
return p.score + bonus(p.score) // error[NK2202] before this ADR
}bonus adds two integers. It cannot pause. The compiler had read its body, had an entry for it
in the ledger, and still recorded “not sync” — because the ledger was recording what the
declaration said rather than what was true.
The consequence compounds. To put anything inside access, you annotated it; to annotate it,
you annotated everything it called; and anything you did not own you could not annotate at all.
The restrictive side of the language was the unusable one, and the reflex it trained is the
wrong one: put less inside the lock, not because the work should be outside it, but because the
annotation chain was too long.
This is not a hypothetical. The check’s first run reported two examples for
exactly this: a sync method building a value through a constructor that never
said sync either. The constructor builds a struct literal and calls nothing —
it could never pause. What the check found was a missing annotation, and a test
froze that confusion in place with the violation as the expected outcome.
sync-ness is a property of the call graph, and the check already walks it. check starts at
a sync function, resolves each call against this unit’s ledger or a library’s, and reports
what can pause. Turning that into an answer for every function is the same walk without the
if !is_sync { return } at the top.
Nothing new has to be computed. The ledger (ADR-020) already holds what a call promises across
the std boundary, which is the part a compiler cannot work out for itself.
One thing does have to be decided, and it is the substance of this ADR: an analysis that claims a property must be careful in the opposite direction from one that checks a claim.
The check is conservative in the permissive direction, and says so in its own header: with
no receiver types, a.method() cannot be looked up, so it is not an error. That is right for a
check. It never rejects a correct program, and an unchecked promise catches nothing at all.
Reuse that polarity for inference and it becomes a defect. “I cannot see what this calls,
therefore sync” writes a promise into a file that is shipped (13.5), read by a consumer’s
compiler, and used to admit a body into access. A wrong sync there is a pausing body inside
somebody else’s lock — a deadlock on one thread, a stalled core on several, and no diagnostic
anywhere, because every compiler involved was told the thing was pure.
The ledger has already answered this question once, for provenance (ADR-010 D1):
Where provenance cannot be established the answer is
Untrusted, neverTrusted— an analysis that fails open is a vulnerability generator.
The same sentence with the nouns changed is this decision.
sync is inferred from the body, for every function.A function is sync when every call it makes resolves, and every callee is sync. The
inference runs after the ledger’s entries exist, over the call graph of the compilation unit,
resolving into a library’s ledger exactly as the check does.
The fixpoint is a greatest one: start from “every candidate is sync” and take the claim
away from anything that reaches a function without it, until nothing changes. That is not an
implementation detail — it is what makes mutual recursion between two pure functions come out
sync, which is the true answer and the one a least fixpoint gets wrong.
A call the compiler cannot resolve costs the function its claim. That covers a method call
(no receiver type yet — ADR-024), a name no ledger knows, spawn (its body runs later and
elsewhere, so the function around it is not a pure CPU task), and a dsl (whose action blocks
are arbitrary Nikaia).
The check keeps the permissive polarity it already had. The two live in one file and
share one resolution rule (reached), and they disagree only about what to do with a call
that rule cannot name: the check shrugs, the inference refuses. Having them disagree about
what a call resolves to would be a bug; having them disagree about what an unresolvable one
means is the design.
And the check is conservative in the same direction, which it was not. A
source that asserts sync and calls something no ledger knows kept its
assertion, because D4 says an assertion is never overwritten by the inference
and the check returned nothing for an unresolvable call. So a ledger that
ships (ADR-020) could carry sync = true for a function that may
pause, and a consumer’s par_iter body would believe it.
The permissiveness was bought with a diagnostic: NK2202 wants a caret on the
call. It was buying nothing — Part III C.2 reports this checker at statement
granularity already, which is a position. A method call stays permissive here
and is a different case: the type checker resolves one
(ADR-028) and the inference merges that answer in per function,
so the claim is still taken away where it must be.
sync = true where the source asserted it, sync = "inferred" where the body implies it.
Absent still means not sync, so nothing about how the file is read changes.
A caller must not distinguish them, and does not: both mean “cannot pause”, and everything that asks the caller’s question asks it through one predicate.
A diff must distinguish them, which is why a bool is not enough. Withdrawing an asserted
sync is a decision somebody made and has to have meant. Losing an inferred one is a
consequence of an edit somewhere else, usually further down the call graph. 13.5 asks this
file’s diffs to narrate causes; two different events that print the same line cannot be
narrated apart.
Where the source says sync, the ledger records Asserted and the inference leaves it alone —
including where the inference could not have derived it. That is deliberate: the keyword’s
remaining job is to hold a property the compiler cannot yet prove, and NK2202 reports what it
can see contradicting it. An inference that quietly downgraded an assertion would remove the
only tool a person has for the cases D2 refuses.
So the keyword changes meaning without changing syntax. It was a mode you entered; it is an
assertion you make — the same move @borrowed makes in Part I 6.6, checked the same way,
and with the same effect on the generated program, which is none.
inference goes from stage0-signatures to stage0-signatures+sync-bodies, because a ledger
whose sync was read off a declaration is not one whose sync was read off a body. 13.5 built
this header for exactly this event; a regenerated ledger shows the header moving, and the
narration says the toolchain did it rather than the code.
--locked names the entry a changed line belongs to.Not strictly part of the inference, and caused by it. sync is now the commonest line in a
ledger, and the --locked diff reported bare lines with no owner:
What the build inferred and the ledger does not have:
sync = true
sync = true
sync = trueThat says something moved and leaves the reader to find out what. It now says whose contract moved, which is the least a diff meant to narrate a cause can do.
examples/1brc.nika carries seven sync declarations. Stripping all seven and rebuilding:
| function | recovered | why |
|---|---|---|
Stats::new, Stats::add, Stats::merge, Stats::mean |
✅ sync = "inferred" |
arithmetic on fields; no calls to resolve |
Summary::new, Summary::record, Summary::merge |
❌ | reach HashMap::new() and .entry(…) — a path and a method no ledger names |
Four of seven, and the boundary is exactly D2’s: what the resolver can name. The remaining three are not a limit of this decision but of ADR-024’s open work — a method call becomes resolvable the day its receiver has a signature written down, and neither analysis here has to change for that to help. The number is expected to rise on its own.
The stripped file compiles clean either way, which is the other half of the result: the check did not merely stop reporting, it had nothing to report.
Infer, and treat an unresolvable call as harmless. More functions get the promise, and some of them cannot keep it. Rejected under §2: the entry ships.
Infer, and report a warning where the inference could not decide. Every method call in every program, for a question most callers never ask. It would train people to ignore the warning, and the thing to fix is not in their code.
Drop the keyword now that bodies are read. It is the only override for D2’s refusals, and the only way to say “hold this function to being pure” about a body that would otherwise lose the property silently on the next edit. Removing it would make the compiler’s inability to see a receiver type into a permanent ceiling instead of a temporary one.
Record one sync = true for both origins. Simpler file, and it makes an assertion being
withdrawn indistinguishable from an inference lapsing. D3.
Infer throws the same way. Tempting, and out of scope: throws is part of a function’s
published shape (a caller writes catch, or declares it in turn), so deriving it silently
changes what callers must write rather than what they may assume. sync is a permission, and
throws is an obligation; they do not take the same treatment. See also the semver question
in §7.
sync line. That is the file recording
something true it previously omitted, and --locked diffs stay readable because of D6.a_constructor_makes_the_same_promise_or_does_not) and keeps its other
half: a constructor that really can pause still takes its caller’s promise down with it. The
guarantee did not move; the ledger’s answer to “can this pause” got better.sync in existing source keeps working, keeps being checked, and now means something slightly
stronger than it did: not “I am entering the sync world” but “hold me to this”.A pub function that loses an inferred sync is a breaking change for its consumers, and
nothing says so yet. The machinery is in place — --locked compares byte for byte and D6 names
the entry — but nothing classifies the change. The same question applies to a pub function
gaining throws, which today can be triggered by an implementation detail (Part I 6.4: a
resource whose cleanup can fail). Both want the same answer: a ledger diff on a pub entry is
a semver event and should be reported as one, by name.
Effect polymorphism was the larger version of this problem: a higher-order
function had to commit to one answer for all of its callers, so no map was
sync, whatever the lambda did. Answered by ADR-029, and in
the shape predicted here — the ledger already said “depends on a parameter” for
borrows, and the same shape serves a different question.