Refinement Types

Refinement types let you constrain values at the type level. A refined type is a base type plus a predicate — the compiler verifies the predicate holds, and erases the refinement in the emitted C#.

Quick Reference

Named Refinement Types (§RTYPE)

Define a refinement type at module level. The predicate uses # to refer to the value being constrained.

Syntax

§RTYPE{id:Name:baseType} (predicate)

• id — unique identifier (e.g., r1)
• Name — the refinement type name, used in parameter declarations
• baseType — the underlying type (i32, str, etc.)
• predicate — a boolean expression using # for the value

Examples

§RTYPE{r1:NatInt:i32} (>= # INT:0)
§RTYPE{r2:Port:i32} (&& (>= # INT:1) (<= # INT:65535))
§RTYPE{r3:NonEmpty:str} (> (len #) INT:0)

These read as:

• NatInt: an i32 that is non-negative
• Port: an i32 between 1 and 65535
• NonEmpty: a str with length greater than 0

Using Named Refinement Types

Once defined, use the name as a parameter type:

§RTYPE{r1:NatInt:i32} (>= # INT:0)

  §F{f001:Process:pub}
    §I{NatInt:count}
    §O{void}
  // count is guaranteed non-negative

The obligation engine creates a verification obligation for count — proving the refinement predicate holds given the function's preconditions.

Inline Refinements (|)

For one-off constraints, attach a predicate directly to a parameter with |:

Syntax

§I{baseType:paramName} | (predicate)

Examples

§F{f001:Divide:pub}
  §I{i32:a}
  §I{i32:b} | (!= # INT:0)         // b must be non-zero
  §O{i32}
  §R (/ a b)

§F{f002:SetPort:pub}
  §I{i32:port} | (&& (>= # INT:1) (<= # INT:65535))
  §O{void}
  // ...

Inline Refinements with Default Values

Inline refinements can coexist with default parameter values:

§I{i32:age} | (>= # INT:0) = INT:18

Self-Reference (#)

The # symbol refers to the value being constrained. It is only valid inside refinement predicates:

§RTYPE{r1:Positive:i32} (> # INT:0)     // # = the i32 value
§I{i32:x} | (>= # INT:0)                // # = x

Using # outside a refinement predicate is a compile error (SelfRefOutsidePredicate).

Proof Obligations (§PROOF)

A proof obligation asserts that a condition holds at a specific point in the function body. The obligation engine attempts to prove it using Z3.

Syntax

§PROOF{id:description} (boolean-expression)
§PROOF{id} (boolean-expression)

• id — unique identifier
• description — optional human-readable label

Examples

§F{f001:Transfer:pub}
  §I{i32:balance}
  §I{i32:amount} | (> # INT:0)
  §O{i32}
  §Q (>= balance amount)

  §B{newBalance:i32} (- balance amount)
  §PROOF{p1:non-negative} (>= newBalance INT:0)

  §R newBalance

Z3 proves this: given balance >= amount and amount > 0, then balance - amount >= 0.

Proof Obligation Statuses

Erasure

Refinement types are a compile-time construct. In the emitted C#, they are erased:

The refinement constrains what values are valid. Since 0.15, a Discharged obligation's guard is replaced with a proof comment by default; pass --keep-proven-guards to keep the runtime guard and treat the verdict as a diagnostic only.

Obligation Engine

The obligation engine is the verification pipeline for refinement types:

1. Generation — Walk the AST and create obligations for every refined parameter and §PROOF statement
2. Solving — For each obligation, use Z3's assume-negate-check pattern:
   • Assume all preconditions (§Q)
   • Negate the obligation condition
   • If UNSAT → Discharged (proven)
   • If SAT → Failed (counterexample found)
   • If UNKNOWN → Timeout
3. Guard Discovery — For failed obligations, discover the simplest guard that would discharge them
4. Code Generation — Emit runtime guards based on obligation status and policy

Obligation Kinds

Public vs Private Functions

For public functions, caller constraints can't be verified — parameter refinement obligations are marked Boundary and always emit runtime guards. For private functions, the solver attempts full verification.

Obligation Policy

The obligation policy controls what happens for each obligation status. Three built-in policies:

Default

Strict

All non-discharged obligations are compilation errors. Use in CI for maximum safety.

Permissive

Failed obligations emit warnings and guards instead of errors. Use during development or migration.

Complete Example

§M{m001:Banking}

// Named refinement types
  §RTYPE{r1:PositiveAmount:i32} (> # INT:0)
    §RTYPE{r2:NonNegBalance:i32} (>= # INT:0)

      §F{f001:Transfer:pub}
        §I{NonNegBalance:balance}
        §I{PositiveAmount:amount}
        §O{i32}
        §Q (>= balance amount)                  // sufficient funds

        §B{result:i32} (- balance amount)
        §PROOF{p1:balance-safe} (>= result INT:0)

        §R result

The obligation engine:

1. Creates Boundary obligations for balance and amount (public function)
2. Creates a ProofObligation for p1
3. Z3 proves p1: given balance >= 0, amount > 0, and balance >= amount, then balance - amount >= 0
4. Emitted C#: runtime guards for the public boundary parameters, and // PROVEN: proof obligation [p1: balance-safe] in place of the p1 guard (the default since 0.15; --keep-proven-guards emits the p1 guard too)

See Also

• Dependent Types Tutorial — Progressive walkthrough with MCP agent guidance
• Contracts — Preconditions and postconditions
• Static Verification — Z3-based contract verification
• MCP Tools — Agent guidance tools for refinement types