## verify()


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


Usage

``` python
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](transform.md#sverify.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](engines.run.md#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](transform.md#sverify.transform), [verify](verify.md#sverify.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](unique.md#sverify.unique) or [references](references.md#sverify.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](unique.md#sverify.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.param`s 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](verify.md#sverify.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 NULL`s 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](Report.needed.md#sverify.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](Report.md#sverify.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](unique.md#sverify.unique) or [references](references.md#sverify.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:

``` python
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:

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