Module spec/numeric
Numeric refinement families — real predicates over the
refine(T, p) surface (V6 task 3, plans/backlog/FORMAL_VERIFICATION.md
§7; breaking-change ledger entry 3). Each family is a comptime alias
whose predicate ghost is spelled INSIDE the alias body: the alias's
comptime T is in scope at ghost creation, so every Positive(i32)
evaluation creates a fully concrete predicate.
{ Positive, check_positive } :: import("std/spec/numeric");
recipl :: (fn(x : Positive(i32)) -> i32)(i32(1) / x); // p assumed at entry
match(check_positive(i32(3)), // runtime gate: Option(Positive(i32))
.Some(v) => recipl(v),
.None => i32(0)
);
Stability
unstable — outside the std stability promise entirely; the verification campaign is still shaping this surface.
Types
Positive(T) — strictly greater than zero.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Negative(T) — strictly less than zero.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
NonNegative(T) — greater than or equal to zero.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
NonPositive(T) — less than or equal to zero.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Functions
check_non_negative(x) — the NonNegative family's runtime gate.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Parameters
| Name | Type | Notes |
|---|---|---|
x | T |
Returns: Option(NonNegative(T))
check_non_positive(x) — the NonPositive family's runtime gate.
Type Parameters
| Name | Type | Notes |
|---|---|---|
T | Type | comptime |
Parameters
| Name | Type | Notes |
|---|---|---|
x | T |
Returns: Option(NonPositive(T))