ADR-266: A Written assert Is a Published Contract, Placed by Computing Back to the Entry — a Guard Is Only Observed

Status: Superseded by ADR-269 — its D1-D8 are D14-D21 there Date: October 2, 2026 Answers: the owner’s question what crosses a module boundary — pub functions and methods — and what the ledger has to carry for it, with the owner’s answer to the syntax: no new words in a signature; a written assert is the contract, and the compiler recognises whether it is a precondition or a postcondition Displaces: ADR-264 D5’s test for a precondition (an assert at the top of a function’s body that names only its parameters) and its three exclusions (a pub fn, a method, a function handed on as a value) Related: ADR-264 D4 (an assert is a contract), D6 (data from outside), D9-D10 (what the prover reads), ADR-265 (the logic layer that decides implications here), ADR-244 D1 and D5 (an inferred sync is read as absent; the author is warned when it is lost, and the committed ledger acknowledges it), ADR-251 D4 (the ledger writes Nikaia’s syntax), ADR-100 (a consumer reads a dependency’s ledger and believes it while its hashes match), ADR-196 (a Nikaia piece is called from Rust), ADR-255 (a guard is a jump with its condition after it)

1. Question

How does a function’s contract reach a caller in another package, without syntax in the signature — and which of what the compiler knows about a body is a promise, and which only an observation?

Today a precondition exists inside one package only. ADR-264 D5 makes an assert at the top of a free function that names only its parameters the callers’ to prove, and refuses the idea everywhere a caller cannot be seen: a pub fn (another package calls it), a method, a function handed on as a value. Those are exactly the places a contract is worth most.

Three things have to be settled together:

• What is promised. Languages with contracts write them in the signature — requires, ensures, Pre =>. The owner has decided against new syntax there: the assert the author already writes is the contract.
• Where an assert stands is not enough to say what it is. An assert after let y = x - 1 is a claim about x; one inside if mode == 1 is a claim about x when mode is 1. Placing a claim by its line would miss both.
• A guard is not a promise. return 0 if total <= 0 is behaviour the body has today. If another package read it as a promise, a change inside the body would break code the author never saw — the fault ADR-244 removed for sync.

2. How others do it

Language / tool	Its answer	What it costs there	Source
Eiffel	require / ensure in the routine’s header; an heir may weaken a precondition and strengthen a postcondition, never the reverse	new keywords in every signature that has a contract	from memory, not checked
Ada 2012 / SPARK	Pre => / Post => aspects on the declaration; GNATprove proves the callers	contracts are part of the spec, so a change is visible in the interface	from memory, not checked
Dafny	requires / ensures clauses; nothing about a body crosses a call except them	every function used in a proof needs its clauses written	from memory, not checked
Weakest-precondition calculus (Dijkstra; used inside Boogie and Why3)	the condition at a point, carried back to the entry: an assignment substitutes, a branch becomes an implication	loops need an invariant; the result can grow	from memory, not checked
Rust, Go, Zig	no contracts; an assert! at the top of a function is a check and nothing else	a caller learns the precondition from the documentation or the panic	the languages’ references

What does not transfer: the clause syntax, by the owner’s decision. What does: Eiffel’s direction rule for what a change may do, and the weakest-precondition calculus — the method the verification tools use internally to turn a claim in a body into a claim at the entry.

3. Options, weighed

Option A — clauses in the signature

fn percent(part: i64, whole: i64) -> i64 requires whole > 0 {
    return part * 100 / whole
}

Option B — the assert is the contract, placed by its line

An assert at the top is a precondition, one before a return a postcondition; anything else is a check in the body.

Option C — the assert is the contract, placed by computing back

pub fn f(x: i64, mode: i64) -> i64 {
    let y = x - 1
    if mode == 1 {
        assert(y > 0)          // published: mode == 1 → x > 1
    }
    return y
}

Weighed

	D1 the special case pays	D2 the compiler works	D3 no cost for the common case	D4 consistent with itself	If it is wrong
A	every contract pays a clause	the author writes what the body already says	—	a second way to state a claim beside assert	a keyword is the dearest thing to take back (ADR-084)
B	a claim after one let loses its contract	the author rewrites the claim in terms of the parameters	—	a claim means something different one line lower	the rule is easy to state and surprising to meet
C	a claim the calculus cannot carry back stays a check	the compiler computes what the author meant	the common case — an assert at the top — is computed with no work	one rule for every assert; B is its special case	a refactoring changes a contract without touching an assert — D6 warns

C wins on D2 and D4, and keeps the owner’s decision on syntax. Its one cost — a contract that moves with the code computing it — is what D6 exists for.

4. Decision

D1 — A written assert is a promise; a guard is an observation.

An assert outside a test is part of its function’s contract, whether or not the function is pub: the author wrote it, so the author promised it. A guard — a branch that leaves, return … if c, throw … if c — is behaviour, and what the compiler learns from it is an observation about today’s body.

Inside its own package the prover uses both. Across a package boundary only promises cross: a guard’s facts reach the ledger marked inferred, and a consumer reads them as absent, as it reads an inferred sync (ADR-244 D1).

D2 — A claim is placed by computing it back to the entry, or forward to the exit.

For each assert the compiler computes the weakest precondition — the condition at the function’s entry under which the claim holds where it stands:

• through a let or an assignment, the value is substituted — a parameter changed before the claim included: x = x + 1 turns x > 2 into x > 1;
• through an if, the branch becomes an implication: mode == 1 → x > 1;
• through a guard, the guard’s condition becomes the implication’s other side: after return 0 if x < 0, a claim c carries back as x >= 0 → c — weaker, so no caller pays for the guard.

An assert at the top of the body is the case where nothing is computed. If the result names only the parameters — and, for a method, the receiver’s public fields — it is a precondition. A claim about the value a return hands back, carried forward to every exit, is a postcondition (D4).

D3 — Where the calculus stops, the claim is a check in the body.

The claim stays ADR-264 D4’s check where it is, and is not published, when between the entry and the claim there is

• a loop that changes a name the claim reads — carrying a claim back through a loop needs an invariant, and the author has written none;
• a call whose result the claim reads and whose ledger has no postcondition for it;
• a value from outside the program (ADR-264 D6), or an effect;

or when the result is outside what the prover reads (ADR-264 D9), names something the caller cannot see (a private field of a pub method’s receiver), or is larger than a fixed bound counted in terms, so that whether a claim is published does not depend on the machine (ADR-265 D4). --asserts says which.

D4 — A postcondition is what holds at every exit.

An assert that names the value a return hands back — directly before return v, or computed forward to it — and otherwise only parameters, states a postcondition of that exit. The function’s published postcondition is what holds at every exit: at the others the compiler proves it or checks it there, as any claim. A guard’s early return 0 is an exit like any other, so a postcondition result >= 0 is proved there from the 0.

D5 — The ledger carries promises, observations and their origin.

A function’s ledger entry gains

key	holds
requires	the published preconditions, in Nikaia’s syntax over the parameters (ADR-251 D4)
ensures	the published postconditions, over the parameters and result
inferred	what guards showed, for the package’s own prover; a consumer reads it as absent
from	for each requires and ensures, the assert it was computed from, by line

Nothing else changes about how a ledger is believed: it carries the hash of every source it was derived from (ADR-100 D3), so a changed contract makes every caller be checked again.

D6 — A contract that changes in the breaking direction warns its author.

The build compares each published contract with the committed ledger and decides the direction with the logic layer (ADR-265): does the old condition imply the new one, or the new one the old?

change	callers	the build
a precondition added or strengthened	may now stop where they did not	warns
a precondition weakened or removed	unaffected	says nothing
a postcondition weakened or removed	their proofs can fail	warns
a postcondition added or strengthened	unaffected	says nothing

Where the implication can be neither proved nor refuted, the build warns. The warning names the function, the old and the new condition, and the assert or the line of code that moved it — which is the case D2 makes possible: a let y = x - 1 changed to x - 2 changes x > 1 to x > 2 without touching the assert. Committing the new ledger acknowledges it, and the warning is not repeated (ADR-244 D5’s mechanism).

D7 — A function with a published precondition has two entries.

• The checked entry checks the precondition and continues into the body. It is what every caller that cannot read the ledger reaches: Rust through ADR-196’s route, a function handed on as a value, a consumer holding an older ledger.
• The unchecked entry is what a Nikaia caller that read the ledger calls: free where it proved the precondition, behind ADR-264 D5’s check at the call where it did not.

This lifts ADR-264 D5’s three exclusions. A method is called through its type’s ledger entry as a free function through its own; a method called through a trait reaches the checked entry until a trait carries contracts (§6).

D8 — A failure names both ends.

A precondition computed back (D2) means little to a caller as a bare formula. A failed check at a call says the computed condition, the assert it came from and its line:

src/main.nika:12: the program stopped: assertion failed
    precondition of `f`: mode == 1 → x > 1
    from assert(y > 0) at src/lib.nika:4

The same pair is what D5’s from keeps and what --asserts prints.

5. Consequences

• A pub function’s contract crosses the package boundary with no new syntax, and its callers prove it or check it at the call.
• Writing an assert in a pub function publishes something. Most of the time that is exactly what it says — the function needs it — and where it is not, it is visible: in --asserts (precondition of f), and in the ledger’s diff in review.
• A contract can move without its assert moving (D2). D6 is what makes that safe, and its warning can suggest the explicit form: write assert(x > 1) at the top of f to state it.
• Computing a claim back is substitution, which the prover already does at a call (ADR-264 D5); the frontend grows by that walk, and the logic layer (ADR-265) is unchanged.
• std.contracts can carry requires and ensures for std’s own functions, which is where most of the facts an everyday program needs would come from.

6. What this does not decide

• Whether a computed precondition must be written explicitly. The owner keeps it open: a later record may require a claim computed back through code (D2) to be restated as an assert at the top. D6’s suggestion is the bridge.
• Contracts on traits and what an implementation may change: Eiffel’s rule — weaken the precondition, strengthen the postcondition — is the expected answer, decided with the first trait that carries one.
• Loop invariants. D3 stops at a loop; whether an assert at the head of a loop becomes its invariant is a later record.
• Claims about a receiver’s private state across a package boundary — a type invariant — are not published (D3).
• Interprocedural facts beyond contracts — what a caller’s arguments make known inside a callee — are not decided here.

This site is open source. Improve this page.