Value contracts

Attach Refine(lambda ...) to a type with Annotated. The first binder receives the constrained value. Multiple predicates are conjoined.

from refinepy import Refine
from typing import Annotated

Nat = Annotated[int, Refine(lambda v: v >= 0)]

def increment(x: Nat) -> Annotated[int, Refine(lambda result, x: result == x + 1)]:
    return x + 1

from collections.abc import Sequence

def at(
    xs: Sequence[int],
    i: Annotated[int, Refine(lambda v, xs: 0 <= v < len(xs))],
) -> int:
    return xs[i]

Additional binders name entry inputs: parameter contracts can refer to earlier parameters; return contracts can refer to any parameter. Reassigning an input in the body does not change its entry value in the contract.

Aliases and local declaration contracts use unary predicates. A local contract such as count: Nat = 0 applies to later assignments; a parameter contract applies only at entry. All parameters and returns require types; local types can be inferred.

Literal contracts and fixed tuples

Literal restricts a value to a nonempty set of same-base int, bool, str or None literals. Signed integers, static type aliases and quoted annotations are supported.

from refinepy import Refine
from typing import Literal

Mode = Literal["read", "write"]

def switch(mode: Mode) -> Mode:
    return "write" if mode == "read" else "read"

def reverse_pair(pair: tuple[Literal[0, 1], Mode]) -> tuple[Mode, Literal[0, 1]]:
    return pair[::-1]

Mixed bases, computed/named values, enums and nested Literal are unsupported. True satisfies Literal[1]; integer 1 does not satisfy Literal[True]. Defaults are base-checked at definition and refinement-checked when used.

Fixed tuples support construction, literal indexing, concatenation, equality and static slicing with a nonzero step. Slice bounds must be static or omitted/None. Every field is evaluated and checked, even for an empty slice or a comparison whose result is already known. Equality compares fields recursively; list fields need matching comparable element sorts. Mapping and abstract-sequence field equality are unsupported. Different arities or unrelated scalar types are unequal.

Ordering is lexicographic over compatible integer/bool, string, nested-tuple or matching None fields, then arity. Optional and container common fields are rejected. Tuples can contain nested supported values, but preserve aliases: storing a written list in a tuple or extracting a list field does not establish writable ownership.

Function preconditions

@requires(lambda ...) constrains entry inputs, including later parameters. Multiple preconditions are conjoined.

from refinepy import requires

@requires(lambda xs, i: 0 <= i < len(xs))
def read_at(xs: Sequence[int], i: int) -> int:
    return xs[i]

requires, ensures and decreases each take one positional literal lambda with ordinary required positional binders. Imports, aliases and re-exports work; same-named user functions do not. @reflect takes no parentheses. Duplicate reflect or decreases markers are errors; decorator order has no effect. Imports must be available before the definition, outside TYPE_CHECKING. Other decorators and old function-comment directives are unsupported.

Calls must satisfy parameter contracts and preconditions. Source callees are checked before their return contracts can be used. The companion decorators do not execute predicates or enforce contracts at runtime; the verifier does not import the checked code.

Function postconditions

@ensures adds a return predicate while retaining the required base return type. The first binder receives the result; others name immutable entry inputs. For -> None, omit the result binder; lambda: proposition is also allowed.

from refinepy import ensures

@ensures(lambda result, n: result == n + 1)
def increment(n: int) -> int:
    return n + 1

@ensures(lambda n: n + 0 == n)
def identity_lemma(n: int) -> None:
    return None

Multiple ensures decorators and return Refine metadata are conjoined. Each predicate must independently be safe to evaluate; it cannot justify its own or another predicate’s definedness. Reflected definitions require plain return contracts and cannot use ensures.

Termination measures

Use one @decreases(lambda ...) on a directly recursive function. Binders name entry inputs; the measure is an integer or a literal nonempty flat tuple of plain integers. Each self-call must establish definedness and strict descent, with all current/next components nonnegative. For a scalar: 0 <= next < entry. Tuple descent is lexicographic; later components may reset after an earlier decrease. Base cases need not have nonnegative measures. Boolean components are rejected.

A decreases(lambda ...) call immediately before a loop uses current bound header locals. Every normal or continue back edge must establish a defined, nonnegative, strictly smaller measure, including the final iteration. break, return and zero iterations need no decrease. Every nested loop needs a measure; an unbound for target or hidden iterator counter cannot be a binder.

All callees must independently terminate. Descent is checked without call-result contracts, so result-dependent descent may remain unproved. Trusted external models and mutual recursion cannot establish termination. A requested proof requires measures on every loop, including unreachable loops.

verified alone establishes normal-return contracts. Termination needs evidence for the selected function and its checked calls. It does not guarantee Python recursion-depth safety or available resources.

Static assertions

Assert checks a proposition at a source position without imposing a contract on later assignments. The target must be a definitely bound function local; the unquoted annotation has no initializer and exactly one Assert item.

from typing import Annotated
from refinepy import Assert

def absolute(n: int) -> int:
    x = abs(n)
    x: Annotated[int, Assert(lambda value: value >= 0)]
    return x

The base type must match the current value; existing refinements are checked too. The first lambda binder receives that value; additional binders name current bound locals. Free local captures, defaults and variadic binders are unsupported. Later rebinding does not update the established fact.

Assert(lambda v: P(v), using=lambda arg: lemma(arg)) uses one direct refined-None source lemma call. Arguments and preconditions are checked first; the complete lemma closure must independently terminate. External models, loops, mutual recursion and circular assertion evidence cannot supply this static proof. Without using, the proposition must follow from current facts and admitted reflected equations. Python does not evaluate these local annotations. Assert cannot appear in parameters, returns, aliases, nested types or module annotations.

Reflected functions and lemmas

@reflect makes a checked definition callable in predicates. Inputs and results must have plain supported types, without nested refinements, preconditions or ensures. Assignments, flat unpacking, assertions, branches and returns are supported; loops and container writes are not. The original body and every argument evaluation must be safe, even when a computation is discarded.

A lemma is a checked function whose return contract states a proposition, often Annotated[None, Refine(lambda _, x: ...)] or @ensures on -> None. Its body must prove that proposition. Calling it supplies the normal-return contract. Ordinary contracts alone do not make a function callable in logic. See the Guide example.

Recursive reflection

A reflected definition may call itself by its declaration name with plain supported input/result types, a loop-free body, no preconditions and an explicit integer decreases measure. Raw-body safety and descent must verify before its equations can be used; every other callee must also verify and terminate.

Unfolding is bounded: eight layers for scalar-only signatures, three for signatures containing containers. Remaining calls are uninterpreted. Queries that cannot resolve them may return unknown, including some false equations; expansion limits can also prevent admission or proof. Mutual recursion, aliased self-calls and recursive signatures with composite container elements are excluded. Use a checked inductive lemma for equations beyond bounded unfolding.

Inductive lemmas

A directly recursive function with a refined None result and an integer or lexicographic decreases measure can prove its return proposition by induction. Every self-call must satisfy its contracts and strictly descend; its declared return proposition is the local induction hypothesis. All base and recursive returns must prove the proposition. Descent is independently checked without call-result summaries; dependencies must verify and terminate, and loops need measures. Reflected definitions are admitted separately.

There is no automatic induction search or mutual induction. Without a measure, a lemma establishes normal-return partial correctness only.

Containers and optional values

Element contracts apply to every valid element; outer contracts constrain the container. Reads require bounds or key-presence proofs. Negative sequence indices are supported. T | None and Optional[T] support absence checks and narrowing.

NonEmptyNats = Annotated[Sequence[Nat], Refine(lambda xs: len(xs) > 0)]

def first(xs: NonEmptyNats) -> Nat:
    return xs[0]

from collections.abc import Mapping

def port_or_zero(ports: Mapping[str, Nat]) -> Nat:
    port = ports.get("http")
    if port is None:
        return 0
    return port

Fresh unshared local lists permit standalone append/extend, += and integer item assignment. Element and whole-list refinements remain checked. Input/shared lists, live iterators, pop, slice assignment and dictionary writes are unsupported.

A checked source helper returning a fresh list can transfer writable ownership under one local name. A helper returning a tuple of independently allocated, disjoint mutable containers can transfer lists through direct flat unpacking: left, right = split(xs). Borrowed or shared fields, saving the tuple before unpacking, and nested unpacking cannot establish that ownership. Equal-content contracts alone are insufficient; every dependency and return alternative must verify. Abstract Sequence and optional results do not transfer ownership.

Container elements may be supported products, optionals or nested containers. Owning an outer list does not make extracted inner lists writable. Storing another written local list as an element is rejected. List equality accepts matching recursively comparable scalar, optional, tuple and list element sorts, even with different refinements; abstract Sequence and mapping elements block it. Concatenation requires matching element contracts, and writable container types remain invariant. See the Guide.

Loops and assertions

Place invariant(lambda ...) calls directly before the loop when inference cannot establish the needed property. Binders name current header locals. Add one decreases(lambda ...) to request termination.

from refinepy import invariant, decreases

def count_to(n: Nat) -> Annotated[int, Refine(lambda result, n: result == n)]:
    i = 0
    invariant(lambda i, n: 0 <= i <= n)
    decreases(lambda i, n: n - i)
    while i < n:
        i += 1
    return i

Each marker takes one positional literal lambda with required binders. Consecutive markers attach to the next loop in the same block; comments and blank lines may intervene, other statements may not. Imports, aliases and re-exports work. Markers do not execute their predicates at runtime. Legacy invariant comments remain accepted but are deprecated.

The invariant is checked initially and after every iteration. An assert is also a proof obligation and must use the supported predicate language.

Supported forms and limits

Admission does not guarantee a proof for every property. Unsupported forms, solver uncertainty or exhausted analysis/model-reconstruction limits cannot produce a successful verification result.

Predicate expressions and built-ins

Predicates must return bool and be safe under the declared types and established facts. Short-circuit guards can justify reads: len(xs) > 0 and xs[0] >= 0.

List literals, equality, concatenation and constant-step slices are allowed; empty lists need a contextual element type. Tuple construction, concatenation and static slicing are allowed too, with every field checked for safety. Unreflected user calls, explicit quantifiers, mapping construction and comprehensions are not allowed in predicates. sum, all, any, sorted, isinstance, scalar conversions and third-party APIs have no default model.

Scope of a result

A verified contract applies to inputs satisfying entry contracts and to the modeled built-in runtime. It checks modeled runtime errors and normal returns; termination is separate evidence. Python annotations do not enforce contracts. The browser reads one module without executing Python; package resolution and external model registration use the native workflow. Page navigation supports #/playground, #/guide, #/reference and their section links. Samples use #/playground/<sample> with bounds, fibonacci, squareRoot, series, rounding or division.

Needs review groups unproved, unknown and unsupported; Failed groups counterexample and error. Individual statuses remain visible. Report-level diagnostics prevent an all-verified summary. See Guide for status meanings and termination summaries.