Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-269: An assert Is a Contract — Proved Where the Compiler Can, Checked Where It Cannot, Published Across Packages, and a Test Is a Block

Status: Accepted Date: October 2, 2026 History: the records this one replaces are archived in docs/history/adr; read them only for how the decision was reached Answers: #190 (assert is on the prelude’s list and is not in std; whatever it is, it is decided with the testing chapter), the owner’s question what happens to a claim the compiler cannot prove, and 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 Related: ADR-313 D1 (the prelude’s list), ADR-298 and ADR-302 (a reserved word needs a construct), Part I 2.2 and Part III A.2 (an overflow is unrecoverable at every build), ADR-010 D2 (data from outside the program), ADR-276 (a jump that carries its condition — the guard the prover reads most), ADR-288 (a promise is what the source wrote), ADR-258 (the four weights this is weighed by), ADR-270 (the logic layer and the solver that decide the implications here), 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-290 (a Nikaia piece is called from Rust)

1. Question

When the compiler can neither prove nor refute an assert, does the program build — with the claim checked when it runs — or is it refused?

Everything else about assert and tests follows from the answer, which is why this record holds all of it: what a test is, what an assert is, what its condition may do, which claims the compiler proves, and what it reports.

The answer cannot default, for three reasons:

The second question follows from the first: 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?

A precondition placed by its line would exist inside one package only, and nowhere 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:

2. How others do it

Language / tool Its answer What it costs there Source
Ada / SPARK Pre, Post and pragma Assert are contracts; GNATprove proves what it can, and what it does not prove stays a run-time check under the assertion policy. A project may require all checks proved as a goal it reaches step by step the proof is opt-in per unit, which is how large Ada code bases adopt it gradually from memory, not checked
Dafny every assertion is proved, or the program is not compiled specification effort is the price of every line; loops need invariants by hand from memory, not checked
Eiffel require / ensure / check are checked at run time; which levels are on is a build setting a contract can be switched off, so it is a test and not a promise from memory, not checked
Rust assert! is on in every profile, debug_assert! only in debug; nothing is proved the check is always paid; the optimiser removes what it can see through the reference, std::assert!
Zig assert is checked in Debug and ReleaseSafe, and is undefined behaviour in ReleaseFast the release build trades the claim for speed 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
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

What does not transfer: Dafny’s model needs a specification language and a solver the project does not have, and makes the solver’s reach the language’s reach. Eiffel’s and Zig’s build switch is what Part I 2.2 rules out for overflow, and would make an assert the one check a build removes. SPARK’s model is the one that fits — the claim means the same thing whether or not it is proved, and the proof only removes its cost.

For contracts across packages, the clause syntax does not transfer, by the owner’s decision. What does is 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 — proved, or the program is refused

fn first(xs: Vec[i64]) -> i64 {
    assert(xs.len() > 0)       // refused: the caller's list is not readable
    return xs[0]
}

Option B — proved where the compiler can, checked where it cannot

fn first(xs: Vec[i64]) -> i64 {
    assert(xs.len() > 0)       // a precondition: proved at each call, or checked there
    return xs[0]
}

Option C — always checked at run time, nothing proved

The same source as B; a check is emitted for every claim, and a proof would never remove one.

Option D — B, and a build option removes the unproved checks

The same source as B; --release-fast leaves out what is not proved.

Weighed

  D1 the special case pays, not the common one D2 the compiler works, not the developer D3 no cost for the common case D4 consistent with itself If it is wrong
A the common claim pays: an invariant outside the theory cannot be written the developer works for the prover — reshapes code until it is readable, or writes panic() nothing at run time consistent, and narrow: a claim exists only where a theory does programs written around the prover; undoing it accepts more, breaks nothing
B the unproved claim pays one comparison, where it is reached the compiler proves what it can and says which it could not (D7) a proved claim costs nothing; the others cost what the program would have written as a panic one meaning for every claim; Part I 2.2’s the check does not depend on a build option a program can stop in production on a claim nobody proved — visible in D7, and a project can refuse it (§6)
C every claim pays nothing proved, nothing reported every claim costs consistent with overflow today fixes the meaning at today’s implementation; a prover could never remove a check
D as B as B the release build pays nothing the one check a build removes, against Part I 2.2 a release build runs a program whose claim is false, silently

B wins on D2 and D4. A wins only D3, and only by refusing the programs whose claims it cannot read — the cost moves from the run to the developer, which is what D2 says the language does not do. C is B without the proof, and D is B with Part I 2.2 broken.

Where a contract is placed, and how it crosses a package

Option E — clauses in the signature

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

Option F — 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 G — 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
E 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-276)
F 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
G 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; F is its special case a refactoring changes a contract without touching an assert — D19 warns

G 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 D19 exists for.

4. Decision

D1 — A test is a test "name" { … } block in the package it tests.

test "a blank line is counted" {
    let (lines, blank) = count("a\n\nb\n")
    assert(lines == 3)
    assert(blank == 1; message: "an empty line is blank")
}

test is a reserved word, for this construct.

D2 — assert is a prelude function, and the compiler knows it.

assert(cond)
assert(cond; message: "what should have held")

It is a function in the sense of the language — the subject before the ;, an option after it — so it costs no reserved word, and it is on the prelude’s list (ADR-313 D1). The compiler recognises the call, for D3 to D11, and for its message: a false assert names its line, its condition as written, and the value of each operand of the comparison, because only the compiler knows what they were called:

assertion failed at src/tally.nika:4
    assert(blank == 1; message: "an empty line is blank")
    blank is 2

A false assert is unrecoverable, as a panic is (Part III A.2).

D3 — The condition of an assert is pure.

The condition may not pause, may not fail, and may not change anything: it is sync, it does not throw, and it touches no place and calls nothing that does. A condition that does is refused where it is written.

This is what makes D4 one meaning rather than two. A condition with an effect would make the program behave differently depending on whether the check is performed — and whether it is performed is exactly what a proof changes.

D4 — An assert is a contract: proved where the compiler can, checked where it cannot.

An assert claims that its condition holds whenever it is reached. For each one the compiler does one of two things:

the compiler then
proves the claim (D9, D10) no check is emitted; the claim costs nothing when the program runs
does not the condition is checked where it is reached, and a false one is D2’s failure

The claim means the same in both rows. A proof only removes its cost, so a compiler that proves more removes checks and changes nothing a correct program does. No build option chooses between the rows: debug and release programs hold the same claims, as they hold the same overflow checks (Part I 2.2). Changed by ADR-380 D1, D2: the second row refuses the program (NK1300) unless the build says unproved-claims = "warn", where it is as above.

An assert and a guard say different things. A guard — throw … if c, return … if c (ADR-276) — handles a case the program expects to meet. An assert says the case cannot occur, and that if it does, the program is wrong. The first is behaviour; the second is a contract, whose breach is a defect and stops the program.

D5 — A claim about a parameter is the caller’s to establish.

An assert whose claim, carried back to the entry (D15), names only the function’s parameters, and that the body cannot prove on its own, is the function’s precondition - an assert at the top of the body is the simplest case. The body assumes it. Each call proves it with the arguments in place of the parameters, and a call that does is free; a call that does not carries D4’s check at the call, so that a failure names the caller that broke the contract rather than the function that stated it:

fn percent(part: i64, whole: i64) -> i64 {
    assert(whole > 0)              // a precondition: `whole > 0` at every call
    return part * 100 / whole
}

fn report(done: i64, total: i64) -> i64 {
    return 0 if total <= 0         // the guard proves `percent`'s precondition
    return percent(done, total)
}

Which claims are preconditions is computed, not read off the line (D15): a claim carried back to the entry that names only the parameters is one. Where the calls cannot all be seen - a pub fn, a method, a function handed on as a value - the precondition is published in the ledger (D18) and the function has two entries (D20), so none of them is an exception.

D6 — A claim about data from outside the program is a guard’s job, and is refused.

A value whose bytes someone else chose (ADR-010 D2: a socket, a request, a database row) has no property the program can claim: its being wrong is a case the program has to handle, not a defect. An assert about it is refused with NK1202, saying where the value came from and naming the way that works — a guard where it arrives, throw BadInput(n) if n > 100 — after which the claim is proved from the guard and costs nothing.

This is the one place D4’s second row is not offered, and it is what keeps D4’s line between a guard and an assert from blurring: a check the program needs in order to be correct is written by the program and handled; a check that only catches a defect is an assert.

D7 — nikaia --asserts answers which claims are not proved, and why.

Beside --sharing, --tethers and --overlaps: every assert of the program by line, and for each one how it is held —

and a count of the claims checked at run time, so that a project can watch it fall and gate on it. The report is how a reader finds the claims that cost something, and how the prover’s progress is seen.

D8 — A refutation needs a counterexample, and it refuses the program.

A claim is refuted only with concrete values that reach the assert with the condition false, and the message shows them. There are two ways to know that they reach it: what is known rules the claim out, so it is false every time it is reached; or what is known is exactly what reaches it - every name the claim depends on is pinned by a constant, a let, a range’s counter, a condition the prover read or a claim checked before, and nothing it cannot see narrows which values get there (a parameter, a call’s result, a condition it cannot read, a loop that may end early) - so a model of what is known and the claim’s negation is a state the program reaches, unless it stops or leaves before:

error[NK1207]: This call breaks `divide`'s precondition `b != 0` every time it is reached.
  --> src/main.nika:12:5
   = note: Here `b` is 0.

It is an error: a program the compiler has shown to break its own contract, with the values that do it, does not build. Fewer defects reach production is what the language is for, and a defect proved while the program is built is the cheapest one there is to fix.

The cost this accepts, and its bypass. A compiler that refutes more will refuse, in its next version, a program the previous one built. That is accepted: what it refuses was wrong before it was refused. For the day it lands at a bad moment, [build] refuted-claims = "warn" - or --refuted-claims warn for one build - builds the program, with each such claim a warning and D4’s check where it is reached. The default is error, and the setting is part of the build’s cache key.

D9 — What the prover reads.

D10 — The prover may fail to prove a true claim, and never proves a false one.

Fourier-Motzkin elimination over the facts and the claim’s negation, with the integer tightening of each derived bound: a claim is proved when every case of its negation contradicts the facts. It gives up past a fixed amount of work, and giving up is D4’s second row. A later prover that proves more removes checks; it never refuses a program, and never changes what one does.

D11 — An assert in a test block is the test’s verdict.

A test exists to run code and look at the result (D1); its asserts are checked when it runs, and a false one fails the test. The prover does not read a test’s body, and D6 does not apply to it: a test looks at what the program computed, from whatever input it was given.

D12 — nikaia test runs at the project’s setting; both settings on request.

Each test runs under the user_parallelism the project names. nikaia test --both-settings runs each test at no and at yes, and a test whose outcome differs between them fails with both outcomes shown. The meaning of a program is the same at both settings (Part I 1.2); a difference is a compiler fault, and this is how a project asks for it to be looked for.

D13 — An output test is files and no code.

In a package’s tests/ directory, NAME.stdout makes NAME a test of the package’s program:

file is
NAME.stdout what the program must print, compared byte for byte
NAME.stdin optional: what it is given on standard input (empty otherwise)
NAME.args optional: its arguments, one per line

The program must also end successfully. ADR-247 gives an output test a directory of its own, NAME.in/ and NAME.out/, and --bless.

D14 — 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-288 D28).

D15 — 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:

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 (D17).

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

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

or when the result is outside what the prover reads (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-270 D4). --asserts says which.

D17 — 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.

D18 — 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.

D19 — 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-270): 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 D15 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-288 D32’s mechanism).

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

So a pub fn, a method and a function handed on as a value have preconditions like any other function (D5). 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).

D21 — A failure names both ends.

A precondition computed back (D15) 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 D18’s from keeps and what --asserts prints.

D22 — A test program is tests/NAME.nika, and what it must produce is a file beside it, a refusal included.

tests/NAME.nika is a program of its own that may use the package, as an integration test does. What it must produce stands beside it: NAME.stdout for what it prints, and NAME.stderr for what it writes to standard error where it runs, or for the compiler’s whole message where it is refused - code, line and help, with the path written tests/NAME.nika. What happened is compared with what is written: a program refused where no NAME.stderr holds the refusal fails, and so does one that builds where NAME.stderr holds one. nikaia test --bless writes both files. The package’s own output tests (D13) take a NAME.stderr the same way.

Why a file and not a mark in the source. One form for every test, the one D13 already has: what a test expects is a file, written by --bless and read in review as a diff. A changed message fails until it is blessed, so no message gets worse unseen; rustc’s UI tests work this way.

What it costs to run. A refused program is refused by the checker and never reaches the backend, so it costs a parse and a check. The programs that build are compiled together, each a package of the test build (ADR-286 D38); one that the checker should have refused and the backend rejects is built again alone to name it.

Decided October 9, 2026 (#535).

6. What this does not decide

This site is open source. Improve this page.