Skip to main content

Refinement Types

A refinement type is a type together with a predicate that every value of that type must satisfy. Predicates are written in the refinement fragment of Verum — a decidable subset that the SMT layer can reason about directly.

Syntax​

Three equivalent forms:

// 1. Inline, on a type definition
type Positive is Int { self > 0 };

// 2. On a type expression
fn sqrt(x: Float { self >= 0.0 }) -> Float { ... }

// 3. On a field
type User is {
    age: Int { 0 <= self && self <= 150 },
};

All three desugar to the same core construct: a base type B plus predicate P(x), written in the literature {x: B | P(x)}.

What can go in a predicate​

The refinement language is intentionally small and decidable:

  • Comparisons: ==, !=, <, <=, >, >=.
  • Boolean connectives: &&, ||, !.
  • Arithmetic: +, -, *, /, % (with nonlinearity routed to the backend with the stronger nonlinear core).
  • Bitwise: &, |, ^, <<, >>.
What names the value, and what happens to a typo

Three spellings bind the value under refinement, and they are interchangeable:

  • self — used throughout this page;
  • it — the implicit binder, seen in Int{ it >= 0 };
  • the name a where form introduces, e.g. T where |x| x > 0.

Every other name in a predicate must be in scope. An unknown name produces error<E100>: unbound variable in refinement predicate. For example, type P is Int { slef > 0 }; is rejected because slef does not name the value under refinement.

The check applies to a type declaration's own predicate. A refinement on a parameter may name a sibling parameter — fn combinations(n: Int{>= 0}, k: Int{>= 0, <= n}) is correct — and those names are function-local, so that position is left unjudged rather than guessed at.

  • Field access: self.field, self.field.subfield.
  • Indexing: xs[i], xs[i..j].
  • Calls to reflected functions: a pure, single-expression user function is reflected into the solver as a definition (see Refinement reflection).
  • Quantifiers (bounded): forall i in 0..n. P(i), exists i in xs. P(i).
  • Built-in predicates: self.is_sorted(), self.is_empty(), self.contains(x), etc.

General function calls, recursion, mutation, and I/O are not allowed in predicates.

Where refinements get checked​

Anywhere a value flows from an unrefined type to a refined one.

fn divide(a: Int, b: Int { self != 0 }) -> Int { a / b }

fn caller(x: Int) {
    divide(10, x);      // error: cannot prove x != 0
    if x != 0 {
        divide(10, x);  // OK: flow-sensitive refinement strengthens x
    }
}

The compiler's flow-sensitive analysis narrows x inside the if branch from Int to Int { self != 0 }, so the second call succeeds.

Which positions carry a check​

"Anywhere a value flows into a refined type" is the intent. The positions that carry it today are these:

Where the refinement is writtenChecked
A parameter's typeyes
A return typeyes
A record field's typeyes
A let annotation, including destructuringyes
A variant payload — Consistent(Int{it >= 0})yes
Behind a named type — type Positive is Int{it > 0}yes
Inside a generic argument — Result<Int{it >= 0}, E>, List<Int{it > 0}>no

The named-type row is worth stating explicitly because it is the spelling programs actually use — you name the domain type once (Positive, Port, NonEmpty) and write the name everywhere after that. It carries both halves: a value the compiler can disprove is refused at compile time (error<E500>: refinement constraint failed), and one it cannot decide is checked when the program runs.

The last row is the one to know about, because nothing at the declaration marks it: the refinement is accepted, reads as a guarantee, and no check is emitted. It comes from instantiating a generic whose own declaration (Result<T, E>) carries no refinement, so there is no declaration site holding the predicate.

If you need the guarantee there, put it where it is carried — a named type with a refined field, or a refined return type on the function that produces the value:

// Not checked: the refinement rides on a type argument.
fn stored() -> Result<Int{it >= 0}, ImportError> { ... }

// the refinement is the return type.
fn count() -> Int{it >= 0} { ... }

Common patterns​

Nonzero / positive​

type NonZero<T: Numeric>  is T { self != T.zero() };
type Positive<T: Numeric> is T { self > T.zero() };
type NonNeg<T: Numeric>   is T { self >= T.zero() };

Bounded intervals​

type Percentage   is Float { 0.0 <= self && self <= 100.0 };
type Probability  is Float { 0.0 <= self && self <= 1.0 };
type Octet        is Int   { 0 <= self && self <= 255 };

Length-refined collections​

type NonEmpty<T>          is List<T> { self.len() > 0 };
type AtLeast<T, const N: Int>  is List<T> { self.len() >= N };
type ExactLen<T, const N: Int> is List<T> { self.len() == N };

Sortedness / structure​

type Sorted<T: Ord>       is List<T> { self.is_sorted() };
type Unique<T: Eq + Hash> is List<T> { self.is_unique() };
type Palindrome           is Text   { self == self.reversed() };

Textual shape​

type Email is Text { self.matches(rx#"^[^@]+@[^@]+\.[^@]+$") };
type IPv4  is Text { self.matches(rx#"^(\d{1,3}\.){3}\d{1,3}$") };
type UUID  is Text { self.len() == 36 && self.matches(rx#"^[0-9a-f-]+$") };

Proving the refinement at construction​

When you create a refined value, the SMT solver must prove the predicate holds.

fn first<T: Copy>(xs: &NonEmpty<T>) -> T {
    xs[0]   // safe: xs.len() > 0, so xs[0] is well-defined
}

fn try_first<T: Copy>(xs: &List<T>) -> Maybe<T> {
    if xs.len() > 0 {
        // Refinement of xs promoted inside this branch.
        let nonempty: &NonEmpty<T> = xs;  // discharge: xs.len() > 0 ✓
        Maybe.Some(first(nonempty))
    } else {
        Maybe.None
    }
}

Postconditions as refinements​

where ensures P is a refinement on the return type:

fn abs(x: Int) -> Int { self >= 0 }
    where ensures result == if x >= 0 { x } else { -x }
{
    if x >= 0 { x } else { -x }
}

The self in the return type refinement refers to the return value; result can also be used in the ensures clause.

Relation to SMT​

Refinements are:

  • Written in Verum's expression syntax;
  • Translated to SMT-LIB at compile time;
  • Discharged by the SMT layer (capability router picks the adapter);
  • Erased from the final binary.

When the solver cannot prove an obligation, verum verify reports it per-function with a raw counter-example — not the source-anchored error[...] transcript shown in earlier drafts of this page, which did not match real output in either format or content.

This example's transcript has been removed, not corrected, and the underlying claim is now an open question rather than a documented fact. Tested directly: a function with requires b != 0, called with a literal 0 argument, was checked with verum verify and did not fail — both the callee and the caller reported Proved. Whether caller-side obligations like input != 0 above are actually enforced at the call site is unconfirmed on the current binary; don't rely on this page's specific claim until that's resolved.

Limitations​

  • Predicates outside the decidable fragment are reported, not rejected. The compiler accepts the predicate, warns that the constraint is unenforced, and continues — which is gradual verification working as designed, but it is not the same thing as a rejection, and this page previously said "rejected". Checked on the current binary. Each row was run at BOTH polarities — once with a field value that satisfies the predicate and once with one that violates it — because a diagnostic on the violating case alone cannot tell a decision from a blanket refusal.

    predicateviolatedsatisfied
    Int{it >= 10}error<E500>clean
    Int{it * 2 >= 10}error<E500>clean
    Int{(it, 0).0 >= 10}error<E500>clean
    Int{f"{it}" == "…"}error<E500>clean
    Int{[it][0] >= 10}warning<W0500>warning<W0500>
    Int{twice(it) >= 10}warning<W0500>warning<W0500>

    The first four are decided: they refuse a value that violates them and accept one that satisfies them. The last two are not, and they say so at both polarities rather than guessing — a predicate that reaches for a function the solver cannot unfold, or indexes a list, is parsed and left unenforced.

    The table shows both satisfying and violating values. A diagnostic on the violating case alone cannot distinguish a valid decision from a blanket refusal of the predicate.

    Two smaller gaps closed with it, both found by varying the VALUE rather than the predicate. A negative or parenthesised value used to lose the verdict entirely — Int{[it][0] >= 10} warned at 5 and said nothing at -5 or at (5), because the check asked whether the expression was a literal and -5 is a negation OF one. And a predicate that is a bare NAME rather than a call — Int{is_positive}, or the where spelling Int where is_positive — was refused at a satisfying value for the same reason the call form was. Both now warn W0500 at every value.

    The warning names the predicate and says what to do:

    refinement {… >= 10} was NOT verified against a value known at compile time (SMT solver returned unknown), so the constraint is not enforced here — express the predicate in terms the solver decides (comparisons, arithmetic, &&/||/!), or check it explicitly in code

    Two things follow for anyone relying on a refinement. A predicate that compiles clean has been checked; a predicate that compiles with W0500 has been parsed. And the warning only fires where the value is known at compile time — the solver answers unknown for any predicate over a value it has not seen yet, so a refinement on a function parameter carries no such signal at the declaration.

  • Recursive predicates do not reflect: there is no decreases-checked recursive encoding, so a self-calling function stays uninterpreted and its goals stay unconstrained.

  • Mutation is not expressible: refinement predicates are pure; self.is_sorted() talks about a snapshot, not an ongoing invariant.

For invariants that span mutation, see Contracts and loop invariants in Functions.

Worked examples​

A refined bank-account record (system boundaries)​

type Positive  is Float { self >= 0.0 };
type BankAccount is {
    balance: Positive,
    account_number: Text { self.len() == 10 },
    owner: Text { !self.is_empty() },
};

fn transfer(from: &mut BankAccount, to: &mut BankAccount, amount: Positive)
    requires from != to
    requires from.balance >= amount
    ensures  from.balance == old(from.balance) - amount
    ensures  to.balance   == old(to.balance)   + amount
{
    from.balance -= amount;
    to.balance   += amount;
}

The SMT solver discharges the postconditions — provided the caller establishes from != to and from.balance >= amount.

A verified sorted-list invariant​

public pure fn is_sorted<T: Ord>(xs: &List<T>) -> Bool {
    forall i in 0..xs.len() - 1. xs[i] <= xs[i + 1]
}

type Sorted<T: Ord> is List<T> { is_sorted(self) };

@verify(formal)
fn insert<T: Ord>(xs: Sorted<T>, x: T) -> Sorted<T>
    where ensures is_sorted(result)
{
    let mut out = xs.clone();
    let pos = out.partition_point(|y| *y < x);
    out.insert(pos, x);
    out
}

The Verified data structure tutorial walks this full example with loop invariants and merge.

Relation to the trusted kernel​

Refinement types reach the kernel as the Refine { base, binder, predicate } constructor in verum_kernel.CoreTerm. The kernel's rule is:

base inhabits some Universe(u); predicate is well-typed under the extended context ctx ∪ binder : base; the refinement lives in Universe(u) too.

When the predicate is not syntactically trivial, the SMT discharge happens outside the TCB: verum_smt produces a SmtCertificate that the kernel's replay_smt_cert re-derives into a checkable CoreTerm witness. A solver bug cannot accept a false refinement.

See Architecture → trusted kernel for the Refine rule and the surrounding trust story.

Configuration knobs​

The RefinementChecker exposes four user-facing config fields, all of which are honoured by the consumer (no inert defenses):

FieldDefaultWhat it gates
enable_smttrueMaster switch for SMT-based subsumption. When false, only the syntactic checker fires; SMT-only obligations return Unknown.
timeout_ms100Per-query SMT timeout, forwarded to the backend through the SmtBackend::set_timeout_ms(ms) trait method before every check invocation. Backends propagate the value to the underlying solver via set_params({"timeout": ms}).
enable_cachetrueVerification-condition memoization. Cache key is hash(predicate, value); identical obligations short-circuit.
max_cache_size10000Evicts the lowest-1/10th when the cache reaches this many entries (LRU-style trim).

Custom backends implement the SmtBackend trait and may override set_timeout_ms to forward the per-query budget. Backends that don't override it inherit a no-op default — the trait extension is intentionally source-compatible so external implementors compile without modification when new gates are added.

Cross-references​