Refinement Types

Python's built-in type hints — int, str, list[int] — tell you the shape of data. But they can't express "an integer that is non-negative" or "a list that is sorted." Refinement types close this gap: they pair a base type with a logical predicate that every value of that type must satisfy.

Deppy lets you write these predicates as ordinary Python lambdas and verifies them automatically with Z3 — without modifying the code they describe. This chapter shows you how.

Base Types as Refinements

Every Python type is already a refinement type — it just has a trivially true predicate. When Deppy sees a plain int annotation, it treats it as:

# Internally: int ≡ refined(PyIntType(), "True", "x")
def successor(n: int) -> int:
    return n + 1

The same holds for str, float, bool, and every other built-in. This means refinement types are a strict generalisation of Python's existing type system — all your existing annotations keep working.

The refined Constructor

To add a predicate, use refined. It takes a base type, a string predicate (so the kernel can both Z3-check it and emit it into the Lean certificate), and the bound-variable name:

from deppy import refined
from deppy.types import PyIntType, PyListType

# Natural numbers: integers ≥ 0
Nat = refined(PyIntType(), "x >= 0", "x")

# Positive integers: strictly greater than 0
Pos = refined(PyIntType(), "x > 0", "x")

# Even integers
Even = refined(PyIntType(), "x % 2 == 0", "x")

# Odd integers
Odd = refined(PyIntType(), "x % 2 == 1", "x")

# Non-empty lists
NonEmpty = refined(PyListType(), "len(xs) > 0", "xs")

Once defined, use them exactly like regular type annotations:

def double(n: Nat) -> Even:
    return n * 2

def factorial(n: Nat) -> Pos:
    if n == 0:
        return 1
    return n * factorial(n - 1)

Deppy reads these annotations from your source and encodes the predicates as Z3 constraints. It then proves — at verification time, not at runtime — that the function body satisfies the refinement on the return type given the refinement on the parameters.

@guarantee for Postconditions

The @guarantee decorator attaches a postcondition to a function. Inside the predicate string, the special name result refers to the return value:

from deppy import guarantee

@guarantee("result >= 0")
def absolute(x: int) -> int:
    if x >= 0:
        return x
    return -x

You can reference parameters and the result together:

@guarantee("len(result) == len(a) + len(b)")
def concat(a: list[int], b: list[int]) -> list[int]:
    return a + b

Deppy verifies each guarantee by encoding it as a Z3 assertion and checking that it holds for every execution path through the function.

@ensures(lambda x, result: result >= 0)
def absolute(x: int) -> int: ...

@assume for Preconditions

Use @assume to state what must be true when a function is called. Preconditions create proof obligations at every call site — Deppy checks that every caller satisfies the assumption.

from deppy import assume

@assume("n > 0")
def reciprocal(n: int) -> float:
    return 1.0 / n

Now any call to reciprocal must provably pass a positive integer. If you write reciprocal(0), Deppy reports a verification error — before the code ever runs.

# ✓ Deppy accepts — 42 > 0 is trivially true
x = reciprocal(42)

# ✗ Deppy rejects — cannot prove 0 > 0
try:
    y = reciprocal(0)
except (ZeroDivisionError, ValueError):
    pass  # precondition violated at runtime

# ✓ Deppy accepts — the if-guard establishes n > 0
def safe_call(n: int) -> float:
    if n > 0:
        return reciprocal(n)
    return 0.0

Refinement Subtyping

If the predicate of type A implies the predicate of type B, then A is a subtype of B. Deppy checks this via Z3 implication queries.

# Subtyping chain:  Pos  <:  Nat  <:  int
#
#   x > 0   ⟹   x >= 0   ⟹   True
#
# Every Pos is a Nat, and every Nat is an int.

This means you can pass a Pos wherever a Nat is expected, and a Nat wherever an int is expected — Deppy accepts these automatically:

def increment(n: Nat) -> Pos:
    return n + 1

# Passing Pos where Nat is expected — subtyping makes this safe
p: Pos = 5
q: Pos = increment(p)   # ✓ accepted

Visually, the subtyping lattice looks like this:

              int  (λx. True)
             /   \
          Nat     Neg
       (x ≥ 0)  (x < 0)
        /    \
     Pos    Zero
   (x > 0) (x == 0)

Combining Refinements

You can build richer types by combining predicates with logical connectives:

Intersection (conjunction)

from deppy.types import PyIntType, PyFloatType, PyStrType, PyListType

# A percentage: integer between 0 and 100 inclusive
Percentage = refined(PyIntType(), "x >= 0 and x <= 100", "x")

# A probability: float in [0.0, 1.0]
Probability = refined(PyFloatType(), "x >= 0.0 and x <= 1.0", "x")

# A non-empty string of at most 255 characters
ShortStr = refined(PyStrType(), "len(s) > 0 and len(s) <= 255", "s")

Complex list predicates

# Sorted list: every adjacent pair is in non-decreasing order
# (also available as ``Sorted()`` from deppy)
SortedList = refined(
    PyListType(element_type=PyIntType()),
    "all(xs[i] <= xs[i+1] for i in range(len(xs)-1))",
    "xs",
)

# Unique list: no duplicates
UniqueList = refined(
    list[int],
    lambda xs: len(xs) == len(set(xs))
)

Worked Examples

Safe Division

from deppy import assume, guarantee

@assume("b != 0")
@guarantee("result * b == a")
def safe_div(a: int, b: int) -> int:
    return a // b

The @assume prevents division-by-zero; the @guarantee states that integer division is exact when a is divisible by b. Deppy will flag cases where the guarantee cannot hold (e.g., safe_div(7, 2) produces 3, and 3 * 2 != 7).

Head of a Non-Empty List

@guarantee("result == xs[0]")
def head(xs: NonEmpty) -> int:
    return xs[0]

Because xs has type NonEmpty, we know len(xs) > 0, so indexing at position 0 is safe. Deppy proves the guarantee trivially.

Clamping a Value

@assume("lo <= hi")
@guarantee("lo <= result and result <= hi")
def clamp(x: int, lo: int, hi: int) -> int:
    if x < lo:
        return lo
    if x > hi:
        return hi
    return x

Deppy checks each branch independently. In the first branch, x < lo so the return is lo, which satisfies lo <= lo and lo <= hi (from the assumption). The other branches follow similarly.

Inserting into a Sorted List

@guarantee("len(result) == len(xs) + 1")
def sorted_insert(xs: SortedList, v: int) -> SortedList:
    for i in range(len(xs)):
        if v <= xs[i]:
            return xs[:i] + [v] + xs[i:]
    return xs + [v]

This function both maintains the SortedList refinement on its return type and satisfies the length guarantee. Deppy verifies both properties.

How Deppy Checks Refinements

Under the hood, Deppy translates each refinement predicate into a Z3 formula. Verification proceeds in three steps:

1. Extract — Deppy reads your Python source and collects all refined types, @assume preconditions, and @guarantee postconditions.
2. Encode — Each predicate is translated into a Z3 expression. For example, lambda x: x >= 0 becomes x >= 0 in Z3's integer theory.
3. Verify — Deppy asks Z3 to prove that, given the preconditions, the postcondition holds for every path. If Z3 returns unsat (no counterexample exists), the refinement is verified.

Your Python code is never modified or instrumented. Deppy operates as a sidecar verifier: it reads your annotations, builds proof obligations, and reports results — all without touching your runtime code.

Refinements vs. Runtime Assertions

Lambda Limitations

Naming Your Refinements

# Hard to read
def f(x: refined(PyIntType(), "x >= 0 and x <= 100", "x")) -> int: ...

# Much better
Percentage = refined(PyIntType(), "x >= 0 and x <= 100", "x")

def f(x: Percentage) -> int: ...

Exercise

from deppy import refined, guarantee

ValidEmail = refined(
    str,
    lambda s: '@' in s and '.' in s
)

@guarantee("'.' in result")
def domain(email: ValidEmail) -> str:
    return email.split('@')[1]