Module spec/refine
EXPERIMENTAL — not covered by the std stability promise (audit spec/ verdict: FREEZE AS DOC). These are Phase 0 identity stubs from plans/backlog/FORMAL_VERIFICATION.md; refinement predicates arrive with the Phase 2+ verifier. Expect ANY change here, including removal.
Stability
unstable — Phase 0 identity stubs, outside the std stability promise
entirely. Expect ANY change, including removal, when the Phase 2 verifier
lands. The section exists so yo doc reports it: the warning above is
prose, and a consumer keyed on the machine-readable stability channel read
these two modules as frozen std surface.
Types
The base refinement constructor the other three are written in terms
of — Refine(T) is intended to read as "a T that satisfies a
compile-time predicate".
In Phase 0 it IS T, exactly. The body is T, so
Refine(i32), NonZero(i32), Bounded(i32, 0, 9) and i32 are one
and the same type: nothing is checked, nothing is rejected, and a
plain i32(0) passes wherever a NonZero(i32) is asked for. The
annotation is a signature that documents a precondition to a human or
an LLM reader, not one the compiler enforces — pair it with a
requires(...) clause if you want the precondition checked before the
Phase 2 verifier lands.
The predicate is not a parameter yet: Phase 2 widens the surface to
Refine(T, predicate) and enforces it at construction sites, so code
written against today's one-parameter spelling will have to name its
predicate then.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
NonZero(T) — values of T that are not zero. Phase 0 is a
type alias for T; future phases will enforce via verification.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Bounded(T, lo, hi) — values of T in the closed range
[lo, hi]. Phase 0 is a type alias for T. T must be Comptime
so the bounds can be compile-time-known.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
_lo | T : (Comptime) | comptime |
_hi | T : (Comptime) | comptime |
NonEmpty(T) — collection types with at least one element.
Phase 0 is a type alias for T.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |