This library is in flux. APIs may change without notice. Generated from source with koruc 0.1.7 on 8/19/2026.

Invariants

~import std/invariants

INVARIANTS - rules that only inference can check

invariants.kz · 3 tors · ~[comptime]

INVARIANTS - rules that only inference can check · 58 more lines
INVARIANTS - rules that only inference can check Every checker this compiler ships decides a fixed question: does the obligation discharge, does the shape match, is the proc pure. A rule outside that set has no subject to hang on — "comments are written in English", "this diff adds a fallback where the charter wants an assertion", "a record whose subtractions are zero while its subject moved has stopped tracking anything". No algorithm decides those. A reader does, and increasingly that reader is an agent. So they are declared, not enforced. The declaration lives in the source, next to the code it constrains, and is machine-enumerable — which is the entire difference between an invariant and a comment. `koruc <file> invariants` lists them; anything that wants to act on them (a git gate, a review pass, a session brief) reads that list and needs no change here. Weak links are the FEATURE. The rule is natural language on purpose: a consumer that reads prose finds things a formal target vocabulary would have excluded before it ever looked. Demanding a subject destroys the point. TWO DISPOSITIONS, OPPOSITE GRADIENTS. They differ by exactly one undecidable bit — does the author intend this to become code — and the NAME carries it. That is why they are two tors and not one with a field: you cannot tell them apart afterwards by re-reading, so the distinction has to be made at the moment of writing or it is lost. inferred — permanent by nature. Nothing will ever make "comments are in English" a compiler check. Zero pressure; GROWTH IS GOOD. A large `inferred` set is a well-described project. aspirational — debt by construction. The author means this to become a real check and has not built it yet. GROWTH IS A SMELL, and a gate is entitled to say so. Usage — a JSON block, exactly as `flag.declare` takes one: std/invariants:inferred { "name": "comment-language", "tags": ["git-gate"], "rule": "Comments are written in English, not Norwegian." } std/invariants:aspirational { "name": "no-silent-truncation", "tags": ["git-gate", "review"], "rule": "No emitter drops elements without a diagnostic. Today three sites slice and stay quiet; this should become a wall." } `name` is the identity — nothing else is. `tags` route it to consumers. `rule` is the claim, in prose, addressed to whoever reads it. In pure `.k` there is no tilde — this is a Koru feature, not a host-embedding one. A host-embedding file writes the same block with ``. [norun] for the same reason as flag.declare: the declaration never executes. It is data in the AST, harvested after the parse by whoever asks. That is what makes the surface metacircular — a consumer discovers invariants by parsing the program, never from a hardcoded list.

inferred

comptimenorun koru_std/invariants.kz:62

aspirational

comptimenorun koru_std/invariants.kz:64

invariants

comptimecommand koru_std/invariants.kz:87