Module spec/refine
Refinement types — the real refine(T, p) surface (V6 task 3,
plans/backlog/FORMAL_VERIFICATION.md §7; breaking-change ledger entry 3).
A refinement type is a T whose values additionally satisfy a
compile-time-known predicate. Refinements are DISTINCT at the type level
and erased at codegen — zero runtime cost. The verifier (pragma(Pragma.Verify)
files) discharges them modularly: a callee ASSUMES p(param) at entry, a
call site PROVES refine#N for each refined argument.
{ NonZero, check_non_zero } :: import("std/spec/refine");
safe_div :: (fn(num : i32, denom : NonZero(i32)) -> i32)(num / denom);
// Construction paths — a plain `T` does not coerce silently:
match(check_non_zero(i32(2)), // runtime gate: Option(NonZero(i32))
.Some(d) => safe_div(i32(10), d),
.None => i32(0)
);
Stability
unstable — outside the std stability promise entirely; the verification
campaign is still shaping this surface (expect the .check/.unchecked
spellings and the family set to move).
The module is unsafe-capable because the trusted casts name a *(T)
witness parameter — a privilege token a safe file cannot produce
(issues/fixed/safe-code-forges-refinement-proofs-through-unchecked-casts.md).
Types
The general refinement constructor — Refine(T, p) is "a T that
satisfies the one-parameter ghost predicate p". The predicate is a
COMPTIME value parameter (a one-parameter ghost_fn over T — plain
functions are rejected: a type-level predicate must not carry runtime
semantics).
Most call sites use the named families below (NonZero(T), …), which
keep their historical signatures; Refine(T, p) is the escape hatch for
custom predicates.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
p | fn(v : T) -> bool | comptime |
NonZero(T) — values of T that are not zero. The predicate is a
ghost spelled INSIDE this alias body: each NonZero(i32) evaluation
binds T := i32 there, creating a fully concrete predicate.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Bounded(T, lo, hi) — values of T in the closed range [lo, hi].
The predicate captures this alias's comptime value parameters, so the
bounds are compile-time-known at every use site. 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) — a value of T that carries at least one element.
A generic .len() > 0 predicate is not expressible for every T (an
i32 has no length), so this alias is the BARE refinement: attach your
collection's predicate where the element check belongs —
Refine(ArrayList(T), your_pred). The Phase-0 spelling NonEmpty(T) is
preserved as a signature; what changed (breaking, ledger entry 3) is
that it now creates a distinct refinement type instead of aliasing T.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Functions
unchecked(p, x, &(x)) — the TRUSTED cast: returns x as Refine(T, p)
without any check and without any proof obligation. Callers take
responsibility for p(x) holding. The witness parameter is how that
responsibility is enforced: it is a raw pointer, which only an
unsafe-capable file can produce (&(x) at the call site), so a safe file
cannot forge a refinement the verifier never discharged
(issues/fixed/safe-code-forges-refinement-proofs-through-unchecked-casts.md).
The witness is not inspected.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Parameters
| Name | Type | Notes |
|---|---|---|
p | (fn(v : T) -> bool) | comptime |
x | T | |
witness | *T |
Returns: Refine(T, p)
check_non_zero(x) — the NonZero family's runtime gate, spelled with
the family's own predicate inline (the alias-created ghost is anonymous,
so the family check restates it — the verifier proves x != 0 on the
Some arm's path either way).
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Parameters
| Name | Type | Notes |
|---|---|---|
x | T |
unchecked_bounded(x, lo, hi, &(x)) — the Bounded family's trusted
cast. The witness pointer is the privilege token; see unchecked.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Parameters
| Name | Type | Notes |
|---|---|---|
x | T | |
lo | T | comptime |
hi | T | comptime |
witness | *T |
Returns: Bounded(T, lo, hi)