ADR-369: A Type’s Invariant — Written as an `assert` in the Struct, and Found Where None Is Written

Status: Accepted Date: October 19, 2026 Answers: #384’s second question, is a field’s bound an invariant of the type or a fact within one method?, asked after ADR-306 D17 decided the second half Related: ADR-269 (an assert is a contract: proved where the compiler can, checked where it cannot; no new words for contracts), ADR-306 D17 (a field is a fact of the walk while nothing can change it), ADR-361 (the compiler finds a loop’s invariant itself), ADR-270 D19-D23 (nikaia.proofs), Part I 4.1-4.2 (private fields; the anonymous constructor), Part I 6.5 (a lent value does not change while it is lent)

1. Question

struct Piece {
    start: i64,
    end: i64,
    assert(0 <= start && start <= end; message: "a piece ends after it starts")
}

Many types hold a rule every value of them keeps: a piece starts before it ends, a cursor stays inside its buffer, a ring’s mask is its length less one. Today the rule lives in the package’s code - private fields, a constructor that checks - and the compiler does not know it: every function that uses p.start as an index checks again, or proves nothing.

2. How others do it

Eiffel, D: an invariant clause on the class, holding at every public method’s entry and exit, checked when the program runs.
Ada 2012: Type_Invariant (at the package’s boundary) and Dynamic_Predicate (at every assignment).
Dafny, Spec#: written invariants, proved statically.
Kotlin, Java records, Rust, Go, C#, Swift: the common practice - the constructor checks (init { require(lo <= hi) }, a record’s compact constructor, a new that returns an error), and encapsulation keeps the rule afterwards. The compiler never uses it.

3. Decision

D1 — A struct states its rule with an `assert` after its fields.

An assert(claim; message: …) in a struct’s body, after its fields, is the type’s invariant. Its claim reads the struct’s fields by name and paths from them (c.len()), comptime values and literals, and is pure (ADR-269 D3). A struct may write several; each is a rule of its own, with its own message. No word is added: as ADR-269 decided for functions, a written assert is the contract, and where it stands says what it is a contract of.

D2 — The rule holds wherever a value of the type can be seen.

It is established:

by every construction - a struct literal, a with copy, the anonymous constructor’s result;
at the end of every method that changes the value (mut self), at each return and each throw;
after every write to a field from outside a method of the type: a pub field written anywhere, a private one written by the package’s code.

Inside a method that changes the value the rule may be broken for a while; it must hold again when the method ends. Each of these points is an ADR-269 D4 claim: proved where the compiler can, checked where it cannot, so a type pays for a check only where its own rule is not proved, and a type that writes no rule pays nothing. A failure names the rule’s message, the point that broke it and the type.

D3 — Where the rule holds, it is a fact.

Wherever a value of the type is read - a parameter at entry, a binding after its construction, a field of another value, an element taken from a list, self at a method’s entry - each of its rules is a fact of the walk (ADR-306 D17) and of the prover (ADR-269 D9) over that value’s field paths, for as long as D17 keeps a fact about them.

D4 — Where no rule is written, the compiler may find one.

For a struct whose fields are private, the compiler searches for claims over those fields that every construction in the package makes and every method of the package keeps, with the strategies ADR-361 uses for a loop, under the build’s counted budget. A rule it finds is used as a fact as D3 says, only once it is proved with its certificates, and is kept in nikaia.proofs with what found it. A found rule is never checked when the program runs, never published in the ledger as a promise to other packages, and never a refusal: where it cannot be found, nothing is lost but the proofs it would have given. Only a written rule is part of the type’s contract (ADR-269 D18).

D5 — `--asserts` shows both.

nikaia --asserts lists each written rule with the points that are checked and why, and each found rule with what found it, so a rule that stopped being found after an edit is visible where its proofs went.

4. Rejected alternatives

Only found rules (option B): no annotation, but a rule nobody wrote can disappear after an edit in one method, and the checks it removed come back elsewhere without a word in the source. Kept as D4, beside a written rule.
No rule at all (option D): encapsulation, D17 and preconditions reach one function at a time; a rule every function of a type relies on is restated in each, or the check stays.
invariant as a reserved word (Eiffel, D): a word taken from every program’s names for a contract assert already writes.
The assert after the struct’s closing brace: a line that reads as a statement standing loose among items.

5. What this does not decide

A rule in an impl block, beside or instead of the struct’s own - not excluded; asked if a type needs a rule its fields alone cannot state.
Rules of an enum and of its variants.
A rule relating two values (p.end <= b.len()): a precondition’s (ADR-269 D5), not a type’s.
Found rules over pub fields, which code outside the package changes.

</content> </invoke>

This site is open source. Improve this page.

ADR-369: A Type’s Invariant — Written as an assert in the Struct, and Found Where None Is Written