verify()

Try to prove ensures about query (an Ibis table expression or a

Usage

Source

verify(
    query,
    /,
    *,
    requires=None,
    ensures=(),
    tables=None,
    counterexamples=None,
    params=None,
    semantics=None,
    on_inferred="error",
    infer=None
)

SQL query) from requires, a mapping from table name to conditions.

tables gives the input schemas; it is only needed for SQL transforms. For each unproved postcondition, up to counterexamples small inputs are tried for one that breaks it (sverify.counterexample); 0 skips that.

A proof is about the plan transform compiles to, under Rel.eval. An Ibis expression compiles with sverify’s own producer, so it means what docs/ibis-semantics.md says, whichever Ibis backend it came from; where Ibis backends disagree (% on Polars, -0.0 == 0.0 on DataFusion, …), no backend’s execute is guaranteed to match. sverify.engines.run runs the verified plan with that meaning (or fails) on DataFusion, DuckDB and Polars. A SQL string, and a SQL condition, is DuckDB’s SQL, lifted by sverify.sql_lift with semantics: the reference semantics by default, or what DuckDB computes with semantics="duckdb" (#411). The report says which (Report.semantics).

Unlike transform, verify checks nothing on data and raises nothing when a postcondition is unproved: it returns the report.

Parameters

transform

The transformation, as an Ibis table expression or a SQL query.

requires: Mapping[str, Sequence[Condition]] | Sequence[Condition] | None = None

Preconditions, as a mapping from input table name to its conditions (Ibis expressions, SQL snippets, unique or references), or, for a transformation with one input, a list of its conditions. They are assumed, not checked. Default: none.

ensures: Sequence[Condition] = ()

Postconditions on the output to prove, including unique keys. Default: none, which still reports the facts and possible runtime errors.

tables: Mapping[str, ibis.Schema | ir.Table] | None = None

Input schemas by table name, as Ibis schemas, anything ibis.schema accepts, Ibis tables, or mappings of column names to DuckDB’s type names ({"id": "BIGINT", "name": "VARCHAR NOT NULL"}, input_schema). Needed for SQL transforms; an Ibis expression’s own tables are found from it.

counterexamples: int | None = None

How many small inputs to try per unproved postcondition when searching for one that breaks it; 0 skips the search. Default: the SVERIFY_COUNTEREXAMPLES environment variable, else 200 (default_counterexamples).

params: Mapping[ir.Scalar, Any] | None = None

Values for the ibis.params of an Ibis transform, as Ibis’s execute(params=...) takes them. The report is about the transform with these values (bind_params); an unbound parameter is refused.

semantics: Semantics | None = None

What the SQL verify lifts means, the transformation if it is a SQL string and every SQL condition: "reference" (the default), sverify’s reference semantics, where an operation that would create a NaN raises; or "duckdb", what DuckDB computes, NaN and ±inf included. An sv.sql expression inside an Ibis transformation keeps its own semantics. Unstated (None), it is "duckdb" for a transformation whose SQL is all sv.sql(..., semantics="duckdb"), else "reference". "polars" checks an Ibis transformation under Polars’s profile (#444); the checker refuses it until it has one. "substrait" checks an Ibis transformation under Substrait’s own semantics (Profile.substrait, #444): the proof under the reference holds there where Substrait allows nothing more at the options the plan meets, and Report.transfer names the options where it allows more.

on_inferred: OnInferred = "error"

What a precondition sverify infers does. sverify infers the bounds on input columns that rule out integer overflow (infer_bounds: amount * 2 on BIGINT needs _.amount < 2**62) and the IS NOT NULLs a postcondition needs (Report.inferred). "error" (the default): the plan is not proved without it, and the report says where it came from and how to state it (Report.needed). "warn": it is assumed, checked on the data before each run, and a warning names it (InferredPreconditionWarning). "ignore": it is assumed and checked without a warning. "off": nothing is inferred or assumed, so an integer SUM that may leave 64 bits, or a double operation that may overflow to ±inf, is an error too, which the other values check on the data while the job runs (Report.assumed); each Issue.hint suggests a bound. "silent" is a deprecated spelling of "ignore".

infer: bool | None = None

Deprecated: infer=False is on_inferred="off".

Returns

Report

A Report with the status of each postcondition, the possible

runtime errors, and what is known about each output column.

Raises

ValueError

requires names an unknown table, unique or references names an unknown column or table, or the checker fails on the request (for example on a plan outside the Lean model).

Examples

A SQL query (DuckDB’s SQL), with its input schema:

import ibis
import sverify as sv
from ibis import _

orders = ibis.table({"id": "int64", "amount": "int64"}, name="orders")

report = sv.verify(
    "select id, amount from orders where amount > 0",
    tables={"orders": orders},
    ensures=["amount > 0"],
)
report.proved  # True

An Ibis expression, with preconditions:

report = sv.verify(
    orders.select(orders.id, total=orders.amount + 1),
    requires={"orders": [_.amount >= 0]},
    ensures=[_.total >= 1],
)
report.facts["total"]  # 'an integer ≥ 1'