provably.types

Refinement type markers and Z3 sort utilities.

from provably.types import (
    Gt, Ge, Lt, Le, Between, NotEq,
    Positive, NonNegative, UnitInterval,
    extract_refinements, python_type_to_z3_sort, make_z3_var,
)

---

Markers

Use with typing.Annotated to embed constraints in signatures.

Marker	Constraint	Example
Gt(bound)	\(x > \text{bound}\)	Annotated[float, Gt(0)]
Ge(bound)	\(x \geq \text{bound}\)	Annotated[float, Ge(0)]
Lt(bound)	\(x < \text{bound}\)	Annotated[float, Lt(1)]
Le(bound)	\(x \leq \text{bound}\)	Annotated[float, Le(100)]
Between(lo, hi)	\(\text{lo} \leq x \leq \text{hi}\)	Annotated[float, Between(0, 1)]
NotEq(val)	\(x \neq \text{val}\)	Annotated[float, NotEq(0)]

Multiple markers on the same parameter are ANDed. Any callable m(var) -> z3.BoolRef is also accepted.

---

Convenience aliases

Alias	Definition
Positive	Annotated[float, Gt(0)]
NonNegative	Annotated[float, Ge(0)]
UnitInterval	Annotated[float, Between(0, 1)]

---

extract_refinements(typ, var)

Convert Annotated markers to Z3 constraints for a symbolic variable.

import z3
from provably.types import extract_refinements, Between

x = z3.Real('x')
extract_refinements(Annotated[float, Between(0, 1)], x)
# [x >= 0, x <= 1]

---

python_type_to_z3_sort(typ)

Python type	Z3 sort
int	z3.IntSort()
float	z3.RealSort()
bool	z3.BoolSort()

Strips Annotated wrappers. Raises TypeError for unsupported types.

---

make_z3_var(name, typ)

make_z3_var('x', float)  # z3.Real('x')
make_z3_var('n', int)    # z3.Int('n')
make_z3_var('b', bool)   # z3.Bool('b')

---

provably.types

Refinement types and Z3 sort mapping for Provably.

Maps Python type annotations to Z3 sorts, and provides refinement type markers compatible with typing.Annotated for embedding proof obligations directly in function signatures.

Convenience aliases

Positive — Annotated[float, Gt(0)] NonNegative — Annotated[float, Ge(0)] UnitInterval — Annotated[float, Between(0, 1)]

These compose with other annotations::

x: Annotated[Positive, Le(100)]  # 0 < x <= 100

Classes

Between

Between(lo: int | float, hi: int | float)

Inclusive range [lo, hi].

Example::

x: Annotated[float, Between(0, 1)]   # 0 <= x <= 1
n: Annotated[int, Between(1, 100)]   # 1 <= n <= 100

Source code in src/provably/types.py

def __init__(self, lo: int | float, hi: int | float) -> None:
    self.lo = lo
    self.hi = hi

Ge

Ge(bound: int | float)

Greater than or equal to a bound.

Example::

x: Annotated[float, Ge(0)]   # x >= 0  (non-negative)

Source code in src/provably/types.py

def __init__(self, bound: int | float) -> None:
    self.bound = bound

Gt

Gt(bound: int | float)

Strictly greater than a bound.

Example::

x: Annotated[float, Gt(0)]   # x > 0  (strictly positive)

Source code in src/provably/types.py

def __init__(self, bound: int | float) -> None:
    self.bound = bound

Le

Le(bound: int | float)

Less than or equal to a bound.

Example::

x: Annotated[float, Le(1)]   # x <= 1

Source code in src/provably/types.py

def __init__(self, bound: int | float) -> None:
    self.bound = bound

Lt

Lt(bound: int | float)

Strictly less than a bound.

Example::

x: Annotated[float, Lt(1)]   # x < 1

Source code in src/provably/types.py

def __init__(self, bound: int | float) -> None:
    self.bound = bound

NotEq

NotEq(val: int | float)

Not equal to a value.

Example::

x: Annotated[float, NotEq(0)]   # x != 0  (non-zero divisor)

Source code in src/provably/types.py

def __init__(self, val: int | float) -> None:
    self.val = val

Functions

extract_refinements

extract_refinements(typ: type, var: Any) -> list[Any]

Extract Z3 constraints from Annotated type markers.

Walks the metadata arguments of an Annotated type and converts each Gt / Ge / Lt / Le / Between / NotEq marker into a Z3 BoolRef constraint on var.

Also supports callable markers: marker(var) is called and the result is included if it is a z3.BoolRef.

Parameters:

Name	Type	Description	Default
typ	type	A Python type, typically Annotated[base, *markers].	required
var	Any	The Z3 variable to constrain.	required

Returns:

Type	Description
list[Any]	A list of z3.BoolRef constraints. Empty if typ is not Annotated.

Source code in src/provably/types.py

def extract_refinements(typ: type, var: Any) -> list[Any]:
    """Extract Z3 constraints from ``Annotated`` type markers.

    Walks the metadata arguments of an ``Annotated`` type and converts
    each ``Gt`` / ``Ge`` / ``Lt`` / ``Le`` / ``Between`` / ``NotEq``
    marker into a Z3 ``BoolRef`` constraint on *var*.

    Also supports callable markers: ``marker(var)`` is called and the
    result is included if it is a ``z3.BoolRef``.

    Args:
        typ: A Python type, typically ``Annotated[base, *markers]``.
        var: The Z3 variable to constrain.

    Returns:
        A list of ``z3.BoolRef`` constraints. Empty if *typ* is not ``Annotated``.
    """
    origin = get_origin(typ)
    if origin is not Annotated:
        return []

    args = get_args(typ)
    constraints: list[Any] = []
    for marker in args[1:]:
        if isinstance(marker, Gt):
            constraints.append(var > marker.bound)
        elif isinstance(marker, Ge):
            constraints.append(var >= marker.bound)
        elif isinstance(marker, Lt):
            constraints.append(var < marker.bound)
        elif isinstance(marker, Le):
            constraints.append(var <= marker.bound)
        elif isinstance(marker, Between):
            constraints.append(var >= marker.lo)
            constraints.append(var <= marker.hi)
        elif isinstance(marker, NotEq):
            constraints.append(var != marker.val)
        elif get_origin(marker) is Annotated:
            # Nested Annotated type (e.g., Positive = Annotated[float, Gt(0)])
            constraints.extend(extract_refinements(marker, var))
        elif callable(marker) and not isinstance(marker, type):
            # Custom predicate callable (but not a bare type like float/int)
            try:
                result = marker(var)
                if isinstance(result, z3.BoolRef):
                    constraints.append(result)
            except (TypeError, Exception):
                pass  # Not a valid constraint callable
    return constraints

make_z3_var

make_z3_var(name: str, typ: type) -> Any

Create a Z3 variable from a name and Python type annotation.

Parameters:

Name	Type	Description	Default
name	str	The variable name (used as the Z3 symbol name).	required
typ	type	The Python type annotation (int, float, bool, or Annotated wrappers of these).	required

Returns:

Type	Description
Any	A Z3 Int, Real, or Bool variable.

Raises:

Type	Description
TypeError	If the type cannot be mapped to a Z3 sort.

Source code in src/provably/types.py

def make_z3_var(name: str, typ: type) -> Any:
    """Create a Z3 variable from a name and Python type annotation.

    Args:
        name: The variable name (used as the Z3 symbol name).
        typ: The Python type annotation (``int``, ``float``, ``bool``,
             or ``Annotated`` wrappers of these).

    Returns:
        A Z3 ``Int``, ``Real``, or ``Bool`` variable.

    Raises:
        TypeError: If the type cannot be mapped to a Z3 sort.
    """
    sort = python_type_to_z3_sort(typ)
    if sort == z3.IntSort():
        return z3.Int(name)
    if sort == z3.RealSort():
        return z3.Real(name)
    if sort == z3.BoolSort():
        return z3.Bool(name)
    raise TypeError(f"Cannot create Z3 variable for sort: {sort}")

python_type_to_z3_sort

python_type_to_z3_sort(typ: type) -> Any

Map a Python type annotation to a Z3 sort.

Strips Annotated wrappers and maps int → IntSort, float → RealSort, bool → BoolSort.

Parameters:

Name	Type	Description	Default
typ	type	A Python type, optionally wrapped in Annotated.	required

Returns:

Type	Description
Any	The corresponding Z3 sort.

Raises:

Type	Description
TypeError	If no Z3 sort exists for the given type.

Source code in src/provably/types.py

def python_type_to_z3_sort(typ: type) -> Any:
    """Map a Python type annotation to a Z3 sort.

    Strips ``Annotated`` wrappers and maps ``int`` → ``IntSort``,
    ``float`` → ``RealSort``, ``bool`` → ``BoolSort``.

    Args:
        typ: A Python type, optionally wrapped in ``Annotated``.

    Returns:
        The corresponding Z3 sort.

    Raises:
        TypeError: If no Z3 sort exists for the given type.
    """
    origin = get_origin(typ)
    if origin is Annotated:
        return python_type_to_z3_sort(get_args(typ)[0])

    _MAP: dict[type, Any] = {
        int: z3.IntSort(),
        float: z3.RealSort(),
        bool: z3.BoolSort(),
    }
    sort = _MAP.get(typ)
    if sort is not None:
        return sort
    raise TypeError(f"No Z3 sort for Python type: {typ}")