std/refine: Constraints That Meet, Boundaries That Enforce

A declaration gives a field a shape — port: i64 — and stops there. Nothing in the shape says a port lives above 1024 and below 65536, so the knowledge that “port” means something narrower than “integer” stays in the author’s head, or in a comment, or in a runtime check somebody remembered to write.

std/refine is the second half of the sentence:

std/proto(Server) {
    port: i64
    retries: i64
    host: string
}

std/refine(Server) {
    port: i64 & >1024
    port: i64 & <=65535
    retries: i64 & >=0 & <10
    host: string
}

The & position is the vocabulary this module owns. Terms come in three kinds: bounds — >, >=, <, <=, == over integer literals — which test a value; sets — 1 | 2 | 3, one member optionally marked * — which say a value is one of a list; and clamp(lo, hi), which rewrites one. Bounds on the same field meet: they merge into one interval, order-independently. port is declared on two lines above; the compiler reads it as one field whose constraint set is >1024 and <=65535 together, and reports the canonical meet while it works:

refine input:Server: port: i64 & >1024 & <=65535, retries: i64 & >=0 & <10, host: string

Five bound kinds share that grammar — >, >=, <, <=, == — and an equality is a bound like any other: it tests a value, it is met onto the field, and it is enforced wherever the interval is.

A meet that lands empty is a refusal, not an override

The other half of “meet” is what happens when the constraints disagree:

std/refine(Server) {
    port: i64 & >20000 & <=1000
}

That does not pick a winner. The compile refuses, naming the two bounds that cannot both hold:

error[KORU205]: std/refine(Server): field 'port' refines to nothing — '>20000' and '<=1000' cannot both hold

Never last-wins. A constraint system that silently prefers the later bound is a config-override chain wearing a lattice’s clothes — the refusal is the feature, because it is what makes “merge these two declarations” a safe operation instead of a precedence argument.

That has to hold across blocks and scopes too, not just within one: a contradiction split over two std/refine blocks is the same empty meet, and it refuses in either declaration order. Equality is the term that shows this is work rather than a slogan. Bounds meet by keeping the strongest of each side, so a disagreement survives the fold and the emptiness judge rules on it. An equality has no strongest term — it cannot fold by strength, so the fold records the disagreement rather than resolving it. Keeping the first value is how a meet quietly becomes a race between transforms, decided by the order the blocks happen to be written in.

Enforcement lives at the consumer’s boundary

Here is the part where refine differs from the language it stole the idea from. In CUE, a constraint is ambient — the unifier enforces it everywhere, always. In Koru a facet is a declaration, and a declaration does nothing until a consumer decides to honor it. std/refine itself emits no runtime code; it leaves a typed facet in the program tree and dissolves. Enforcement is a choice each consumer makes at its own boundary.

std/list made that choice for push. A list of a proto is a list of the record — push spells the whole value by field name, the same convention std/store:insert uses:

std/list:new(Server)
| list xs |> std/list:push(xs, port: 8080, host: "web-01") |> std/list:len(xs): n |> std/io:print.ln("len={{ n:d }}") |> std/list:free(xs)
| err e |> std/io:print.ln("ERR {{ e:s }}")

When the element’s proto carries a facet, the synthesized push-Server returns a union that says everything that can happen at the boundary — the generated Zig, de-indented from the emitter’s nesting:

pub const Output = union(enum) {
    ok: struct {
    },
    violated: []const u8,
    oom: struct {
    },
};
pub fn handler(__koru_event_input: @This().Input) @This().Output {
    if (!(port > 1024 and port <= 65535)) {
        return .{ .violated = "port" };
    }
    xs.items.append(xs.allocator, .{ .port = port, .host = host,  }) catch {
        return .{ .oom = .{} };
    };
    return .{ .ok = .{} };
}

In Koru that union is spelled as branches on the event: push declares | ?ok, | ?!violated string, | ?!oom. The ?! is a panic branch — the third kind alongside required | and optional | ? — and its price is decided at the call site, not in the library. Leave it unhandled and the compiler synthesizes the trap you would have written by hand: push port: 80 and the process dies printing panic branch 'violated' fired — payload: port, naming the field. Handle it, and the rejection arrives as an ordinary branch — this is the whole program, nothing elided:

import std/proto
import std/refine
import std/list
import std/io

std/proto(Server) {
    port: i64
    host: string
}

std/refine(Server) {
    port: i64 & >1024 & <=65535
    host: string
}

std/list:new(Server)
| list xs |> std/list:push(xs, port: 80, host: "web-01")
    | ok |> std/io:print.ln("unexpected accept") |> std/list:free(xs)
    | violated f |> std/io:print.ln("rejected {{ f:s }}") |> std/list:push(xs, port: 8080, host: "web-01") |> std/list:len(xs): n |> std/io:print.ln("len={{ n:d }}") |> std/list:free(xs)
| err e |> std/io:print.ln("ERR {{ e:s }}")

rejected port
len=1

Two lines out. 80 was refused at the boundary and never entered the list; len=1 counts only the record admitted after it. Nothing was thrown, nothing was clamped into range, and no later code has to re-check what the type already refused.

And a middle layer can refuse to decide at all: | violated f |> => violated f re-raises the panic into the enclosing event’s own declared ?!violated, payload intact, for the next caller up to supervise — the let-it-crash shape, typed at every level. A proto with no facet gets no guard: the synthesized push emits the append and nothing else, and the ?!violated arm its signature declares is simply never produced into. Enforcement is opt-in, and the opt-in belongs to the consumer, not the language.

That is the enforcement model in one sentence: the facet is a promise about a field; the consumer decides what breaking the promise costs. std/list charges a typed refusal at push — loud by default, supervisable by choice. std/store charges at insert, in the store’s own currency. A JSON decoder would get to decide at the decode boundary — where a violation is not a bug in your program but a property of the outside world, and might deserve a recoverable error instead of a trap. Same declaration, different boundary, different price. Ambient enforcement cannot make that distinction; consumer-owned enforcement is nothing but.

And the deciding is cheap because the protocol is shared. Resolving a facet — which bounds govern Server, which module it calls home, what the guard text and the ?ok/?!violated branch set look like — lives in one compiler surface (ast_functional.facets) that any transform calls at comptime: one predicate spells a field’s terms for every consumer, and one normExprFor spells its clamp, per host. A consumer contributes its judgment — “I enforce here” — and its sink: a branch expression at the store, a struct literal at the list. The rule in between is not anybody’s copy.

The second consumer charges in its own currency

std/list refuses at push. std/store refuses at insert — the same facet, read through the same fold, priced by the boundary that honors it. An insert writes named columns, so the verdict carries the column’s spelling rather than the field’s:

import std/proto
import std/refine
import std/store
import std/io

std/proto:i64(Port)

std/proto(Server) {
    port: Port
}

std/refine(Server) {
    port: Port & >1024 & <=65535
}

std/store:new(fleet, capacity: 8) { web: Server }

std/store:insert(fleet) { web.port: 8080 }
| row r |> std/io:print.ln("committed {{ r:d }}")

std/store:insert(fleet) { web.port: 80 }
| violated f |> std/io:print.ln("rejected {{ f:s }}")

std/store:query(fleet)
! query e |> std/io:print.ln("web.port {{ e.web.port:d }}")

committed 16777216
rejected web.port
web.port 8080

Three things are worth reading off that run. The refused insert never wrote — the query sees exactly one row. The payload is web.port, the column path as the store spells it, not port. And 16777216 is the row handle the store minted, printed because the sample prints it: it is opaque, and nothing in the program depends on its value.

The guard the emitter writes into both of insert’s answer arms is the same predicate the list used, aimed at the column:

if (!(@"web.port" > 1024 and @"web.port" <= 65535)) return .{ .violated = "web.port" };

The prices are the same as push’s: unhandled, the synthesized arm traps naming the column; handled, the caller supervises and the store keeps its invariant. A clamp facet normalizes before anything is written — left.health: 250 under health: Health & clamp(0, 100) & >=0 stores 100, and the bound judges what was stored. And the refusal is born per target: on the JS target the same facet yields the same three outcomes out of the emitted JavaScript, because the guard and the panic arm are written in whichever language the boundary is being compiled to.

Sometimes the answer isn’t no — it’s the nearest yes

A bound and a refusal are the right physics for a port: 80 is not a degraded server, it is a different claim, and storing it would be a lie about what was sent. But some fields are not like that. A gain knob, a joystick axis, a pixel channel — these saturate. The domain’s honest answer to 240 isn’t “refuse”; it’s “the range ends at 100, so the value is 100.” Saturating arithmetic exists because this is a real semantic, not a tolerance.

That is the second term kind:

std/refine(Mixer) {
    gain: i64 & clamp(0, 100)
}

clamp is a normalizer, not a predicate — the boundary rewrites instead of guarding. Pushing gain: 240 stores 100 and returns .ok; the ?!violated branch cannot fire because nothing was violated. The generated write, verbatim:

xs.items.append(xs.allocator, .{ .gain = @min(@max(gain, 0), 100),  }) catch ...

This is the case for keeping the policy in the declaration rather than hiding it in a defensive fixup. clamp(0, 100) spelled on the field is the statement “out-of-range writes saturate” — greppable, checkable, and exactly as silent as the type says it is. A coercion you can read off the declaration is not silent corruption; a coercion you can’t is.

When a field carries both kinds, the order is forced rather than chosen: normalize first, then the bounds judge the result. clamp(0, 100) & >=10 applied to gain: 5 stores 5 — in range, so nothing was rewritten — and then >=10 refuses it: the boundary judges what was actually stored, not what was typed. You normalize a value into representability before asking whether it’s valid; checking pre-normalization would be judging a number the field can’t even hold. And normalizers meet like everything else: two clamps intersect — clamp(0, 100) met with clamp(10, 90) normalizes to [10, 90], so 5 stores 10 and 95 stores 90 — and a meet that lands empty refuses at KORU205, same as any other. clamp(0, 100) & >200 is empty by construction: the normalizer can never produce a value above 200 for the bound to admit.

A field can list its values

Bounds describe an interval, and some fields do not have one. A mode flag, a protocol version, a bank selector — the honest statement is a short list, with one member marked as the value to fall back on:

std/refine(Sample) {
    mode: i64 & *1 | 2 | 3
}

The * marks the fallback; the set is the constraint. It meets like everything else here, which means by intersection: 1 | 2 | 3 met with 2 | 3 | 4 is 2 | 3, and two blocks sharing no value refuse at KORU205 rather than quietly unioning into a wider set. The field’s other terms filter it — 1 | 2 | 3 & >1 is >1 & 2 | 3, because 1 can never arrive — and a set that lands on one value is that equality: 5 | 7 & >6 is ==7. One lattice element, two spellings, so nothing downstream has to know that a singleton set and an equality are the same thing.

The default is not a term anybody judges. It is what a boundary that supplies a value would pick when nothing else decides — and no boundary supplies one yet, so push and insert enforce membership while the catalog reports the fallback and names the reader it is waiting for:

    mode.default = 1
    the `*` marks the fallback a boundary that SUPPLIES a value would select — push and insert enforce membership, never the default

That is the declared/enforced distinction doing its job on a term that is deliberately half-built: the set is enforced, the fallback is declared, and the catalog says which is which.

The base can be a name

So far every field’s base has been a raw scalar — port: i64. But std/proto also mints terminals: named scalars whose identity is the name itself. The verb is the host scalar, spelled concretely:

std/proto:i64(Port)

std/proto(Server) {
    port: Port,
    host: string
}

Port is not a wrapper and not a newtype — it’s an alias that collides loudly and can’t be confused with any other proto’s Port. And the field refines by the name it was declared under:

std/refine(Server) {
    port: Port & >1024 & <=65535
}

Spelling port: i64 here would be a lie — the declaration says Port, so the meet says Port. Legality resolves the name to its host scalar (Port → i64, integer — bounds allowed); the emitted guard is still port > 1024 because Port is i64 in the generated code. A terminal resolving to a non-integer — std/proto:string(Email) — refuses a bound the same way a raw string field does.

The wire is the program tree, not a comment

One design note worth naming, because it took a detour to get right. For a while the refine transform folded its meet and then wrote the result as a comment — // refine input:Server: port: i64 & >1024 & <=65535 — that later passes parsed back out of the generated text. A string wire inside a compiler that has a typed AST. It worked, the way a stringly-typed protocol always works, right up until you need the consumer to do anything real with it.

The facet now rides the program tree as a typed node — name, logical home, and fields carrying structured bounds (value and inclusivity, not text). std/list reads the node off the tree and builds its guard from integers; nothing anywhere calls startsWith on a comment. The emitted Zig still shows // refine input:Server: port: i64 & >1024 & <=65535 — but that line is a rendering of the node for human debugging, and the arrow only points one way: node to comment, never comment to data.

Ordering is a stage, not an accident. std/refine runs in the pre transform stage, so every facet exists in the tree before any consumer’s main stage walks it — the guarantee the comment wire used to fake through dissolution order.

The program explains its declared self

This design scatters its truth on purpose. A facet is declared in one module — refine(Server) can sit an import-graph away from proto(Server) — laid out in a second, enforced in a third. That is the architecture’s strength and its legibility tax: nothing in any single file answers “what governs port, and who checks it?”

The qualified spelling is how a refinement reaches across that distance: std/refine(app/test_lib/defs:Server) names the home the declaration lives in, and the meet folds program-wide against it.

So the program answers it. koruc explain asks every module that owns a vocabulary to report what it sees, and gathers the reports into one catalog. A refined proto pushed into a list — 671_018’s program — reads back as:

📖 std/refine
  input:Server
    contributors = 1
    port: Port & >1024 & <=65535 → i64 — refuse
    port.meet = Port & >1024 & <=65535
    port.scalar = i64
    port.effect = refuse
    gain: i64 & clamp(0,100) — saturate
    gain.meet = i64 & clamp(0,100)
    gain.effect = saturate
    host: string — declared only
    host.meet = string
    host.effect = declared only
📖 std/list
  list(input:Server)
    element = input:Server
    new_sites = 1
    port: Port & >1024 & <=65535 — push refuse
    port.enforced = refuse
    gain: i64 & clamp(0,100) — push saturate
    gain.enforced = saturate
    host: string — push declared only
    host.enforced = declared only
    facets_enforced = 2
    push declares | ?ok | ?!violated | ?!oom — an unhandled violation panics; | violated f |> handles or forwards

And a store whose member proto carries a facet — 690_319’s program — reads back as:

📖 std/refine
  input:Limb
    contributors = 1
    health: Health & >0 & <=100 → i64 — refuse
    health.meet = Health & >0 & <=100
    health.scalar = i64
    health.effect = refuse
📖 std/store
  input:body
    capacity = 8 [vjdw]
    columns = 2 [vjdw]
    left: Limb
    right: Limb
    inserts = 1 [vjdx]
    queries = 1 [vjdp82]
    watches = 0
    facets_declared = 2
    insert enforces them — every generated insert event declares `?!violated <column>`; unhandled it panics, `| violated f |>` supervises

The bracketed tokens are site witnesses: short hashes the catalog hangs on a row so koruc at <witness> can walk back to the source site that produced it. They are derived from the source, so they move when the source does.

Two runs, four voices — and the join is the interesting part. Refine reports the meet, the field’s resolved host scalar, and what the boundary will do with it. List reports enforcement at its boundary, keyed to the element it holds (element = input:Server). Store reports its composition — capacity, columns, site counts — and then the row a compiler usually hides: facets_declared = 2, and insert enforces them, naming the ?!violated <column> contract the generated events carry.

That row is a fact about enforcement, and the catalog is expected to say it straight: 690_324 fails the build if the stale “does NOT enforce” text reappears. A consumer that reads a facet and one that doesn’t are two different facts, and the gap between declaration and enforcement is exactly what a reader needs — silence would pass for “no facets exist.”

The mechanism is the other half of the honesty: each explainer runs its transform’s own fold on the pre-transform tree — the metFields resolution that builds list’s push guard is the one that builds list’s report — so the explanation cannot drift from the enforcement, and a program that refuses to compile still explains itself in the compiler’s own words. Its post is being written; the command is already pinned in the corpus — explain-command.

Importing is the vocabulary

The block only resolves where std/refine is imported — there is no ambient & syntax in the language, and a module that never imported refine cannot spell it. The parser never sees inside the { ... }: it hands the raw block text to the module that owns it, the same door std/proto’s field grammar and std/invariants’ claim blocks already walk through. A constraint grammar is a library, not a language feature.

What made the ambient version possible at all is a property of imports this work pinned down: a transform declared inside an imported module fires at compile time merely because the import landed it in the program — no call site required. import std/refine is how the vocabulary arrives today; that same mechanism is how a future refine could reach into other modules’ blocks, touching only the scopes that imported it.

What it compiles to

The refine block itself: nothing. It validates its meets, leaves the facet in the tree, and dissolves — zero runtime cost, the same dissolution contract std/trellis’s structural laws carry. The cost lives exactly where the enforcement lives: in the consumer’s generated code, at the boundary that chose to honor it.

This is the idea CUE built a whole language around, taken as a vocabulary: constraints are declarations, merging is order-independent, conflict is loud — enforcement is somebody’s explicit decision at a boundary, not the air the program breathes — and the program itself will tell you, in the compiler’s own words, what is declared, what is enforced, and where the gap between the two lives. v0 is intentionally small: integer bounds, sets and clamp on i64 fields, two consumers that read them, three term kinds — one that refuses, one that lists, one that rewrites. Non-integer bases, enforcement at decode boundaries, a consumer for the * fallback, and the ambient reach into other modules’ blocks are the designed next rungs — and each now has its mechanism pinned rather than presumed.