Issue #714: Build ADR-369: a type’s invariant, written as an assert after a struct’s fields, and found where none is written

Open and answer this issue on GitHub.

language, ready · opened 2026-10-19 · updated 2026-10-20 · 1 comment

History

#384 asked whether a field’s bound is “an invariant of the type, or a fact within one method”. ADR-306 D17 (#711) decided the second half: a field is a fact while nothing can change it.

For type invariants, the owner rejected “no case needs it” as an argument. The question was weighed by what is common:

• written invariants: Eiffel, D, Ada, Dafny;
• “check in the constructor, then rely on encapsulation”: Kotlin, Java records, Rust, Go, C#;
• Nikaia’s own pattern: contracts are written asserts (ADR-269) and loop invariants are found by the compiler (ADR-361).

The owner chose C: written and found. The assert goes inside the struct’s body after its fields. A rule in an impl block is not excluded for later.

Decision

ADR-369; Part I 4.1; Part III 14.2.

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

Where a rule must hold. It holds after every construction (a literal, with, or the constructor’s result). It holds at the end of every method that changes the value, at each return and throw. It holds after every write to a field from outside such a method. Each such point is an ADR-269 D4 claim: proved where the compiler can, checked where it cannot.

Where a rule is a fact. Wherever a value of the type is read, the rule is a fact over its field paths, for as long as ADR-306 D17 keeps one.

Found rules. For a struct with private fields that writes no rule, the compiler searches for one with ADR-361’s strategies under the counted budget. A found rule is used only once it is proved. It is recorded in nikaia.proofs. It is never checked at runtime and never published in the ledger.

--asserts lists both kinds.

To build

Depends on #711 (field paths in the walk).

1. Parser and AST: an assert(...) in a struct body after the fields; several allowed, each with message:. Struct-body grammar in the parser crate, which is a winnow-grammar DSL.
2. Checker:
   • The claim reads the struct’s fields, paths from them, comptime values and literals, and is pure (ADR-269 D3).
   • Anything else is refused. Ask the supervisor for an NK code if a new refusal is needed.
3. The points of D2:
   • Generate the claim at each construction, each exit of a mut self method, and each outside field write.
   • Prove it, or emit the check with the rule’s message, naming the point and the type.
4. Facts of D3: every value of the type read in a body brings its rules as facts over its paths. This covers parameters at entry, bindings after construction, fields, elements, and self at a method’s entry.
5. Ledger: a written rule of a pub struct is published as part of the type’s contract (ADR-269 D18). Changing it in the breaking direction warns (D19).
6. Found rules (D4), may be a second issue: the search over private fields, certificates in nikaia.proofs, used only as facts.
7. --asserts (D5).
8. Tests:
   • a literal that breaks the rule is refuted at build time (ADR-269 D8);
   • one that may break it is checked and fails with the message;
   • a mut self method that breaks it in the middle and restores it passes; one that leaves it broken is caught at its exit;
   • a pub field write from another package is proved or checked;
   • the rule proves an index in a function that only receives a Piece;
   • a found rule for a private cursor struct (0 <= at <= c.len()) removes a check, and after an edit that breaks it, the check returns and --asserts says why.
9. Measure: proved sites over the corpus; cmp/phase3/fast/fast.nika with Piece carrying its rule.

Comments

keywan-ghadami, 2026-10-20

Built so far (0.0.1155–0.0.1158): D1–D3, and three holes closed. Each hole was shown with a probe that read past the end under remove-bounds-checks:on.

Commits:

• f7b1900 and e664819: the type’s rule is checked at each literal, at each exit of a method that changes the value, and before self is handed on. It is a fact at each entry. NK1288 refuses a rule that is not a pure claim over the fields.
• 98a8e39: a type with a method that changes self and throws gets no entry fact. A failing call left the method with the rule broken, and the caller could catch the error and go on.
• b9c5cef: a type whose fields or literals another file of the package touches gets no entry fact.
• 5b7643a:
  • an open type gets no entry fact: one whose rule reads a pub field, or a pub type whose fields are all pub or defaulted. A dependency is lowered without its consumers in view, and the consumer had popped a slot;
  • a literal of the type built in another file of the package is checked against the rule.
• 531a940 and 425502a: a generic struct’s rule is refused as generic, and a failure now names the type (“the rule of T: …”).

Still to build:

1. Consumer-side checks of a dependency type’s rule (D2): the rules go into the dependency’s ledger, and a consumer checks them where it writes a pub field or builds a literal. With that, open types could keep their facts.
2. Throwing methods: they could keep their facts if the rule were checked at each call that may fail. That needs the pass to know which calls fail.
3. D4 (rules the compiler finds) and D5 (--asserts). #772 builds --asserts for assert and assume if it is not here first.
4. A method’s exit check (self.slots.len() == N) is not proved yet. Writes to an element should leave .len() unchanged; together with #767 that gives fast.nika’s table index.

---

Generated by Claude Code

Back to Open Issues