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/invariantsINVARIANTS - 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.
~[comptime|norun] pub tor inferred { source: Source }~[comptime|norun] pub tor aspirational { source: Source }~[comptime|command] pub tor invariants {
program: *const Program,
allocator: __koru_std.mem.Allocator,
argv: []const []const u8
}