Report

What the checker proved about a transformation, returned by verify and kept

Usage

Source

Report(
    requires,
    ensures,
    facts=dict(),
    not_null=list(),
    deterministic=True,
    windows_total=True,
    tie_places=list(),
    issues=list(),
    guard_free=False,
    unchecked=None,
    optimized=None,
    rewrites=list(),
    inferred=dict(),
    implied=dict(),
    assumed=list(),
    params=list(),
    hints=list(),
    bounds=dict(),
    rows=None,
    relations=list(),
    semantics="reference",
    plan=None,
    observation=(lambda: _observation.PLAN_BOUND)(),
    stated=False,
    floats_on=dict(),
    depends=None,
    routes=dict(),
    contract=None,
    transfer=None,
    output=dict(),
    epsilon=None,
    rows_exact=None,
    conditions=dict(),
    dialect="ibis",
    ties=dict(),
    on_inferred="ignore",
    inferred_from=dict(),
    postconditions=list(),
    inputs=dict()
)

in ContractedTransform.report.

str(report) lists each postcondition with its status, the possible runtime errors and warnings, and what is known about each output column; in a notebook the report renders as tables.

Parameter Attributes

requires: dict[str, list[str]]

The preconditions that were assumed, as labels, per input table.

ensures: list[CheckedCondition]

Each postcondition, in the order given: its label, whether it was proved, what the checker established about it, and a counterexample if one was found.

facts: dict[str, str] = dict()

What the checker established about each output column.

not_null: list[str] = list()

The output columns the checker proved never NULL, from what it established about them (facts), in the output’s order. A stored node of a proved report writes them as NOT NULL columns.

deterministic: bool = True

False when rows may tie in the ORDER BY of a window or of an ordered aggregate (first, last, group_concat; without an order_by every row ties), or when a LIMIT takes rows that tie in its ORDER BY, or has none. The engine then picks an order, and a rerun may pick another (D10). The postconditions are proved for every order (D24); the deterministic profile (routes.choose(deterministic=True), a sink’s reproducible=) refuses such a plan and names tie_places.

windows_total: bool = True

False only for the window and ordered-aggregate ties of deterministic.

tie_places: list[TiePlace] = list()

Where the plan leaves the order of ties open (D24), one entry per window, ordered aggregate or LIMIT; empty when deterministic.

issues: list[Issue] = list()

Runtime errors, SUM overflows among them, the checker could not rule out; when empty, the transformation provably runs without them.

guard_free: bool = False

The only issues are assumed ones (SUMs that may overflow, double operations that may give ±∞, which keep their checks): on data that meets the preconditions, the transformation’s SQL (sverify.engines.to_sql) and Polars plan give the same result with guards=False, without per-row checks (Rel.guardFree_sound).

unchecked: dict | None = None

The expressions that run correctly without their checks, on data that meets the preconditions (Rel.evalG_marks), as a tree parallel to the plan; pass it to sverify.engines.to_sql(..., unchecked=...) with the same plan, and only the other expressions keep their checks. None when Lean found none (a left join with a filter on its right side, for one).

optimized: dict | None = None

The transformation as a Substrait JSON plan, rewritten with the facts and keys of the preconditions (Rel.optimize in SubstraitLean/Semantic.lean): for example a DISTINCT over a key is gone. On data that meets the preconditions it gives the same rows (Rel.optimize_sound); pass it to sverify.engines.to_sql, or as JSON to sverify.engines.run, instead of the transformation. None if Lean did not return one.

rewrites: list[str] = list()

The rewrites in optimized, such as “DISTINCT on a key”.

inferred: dict[str, list[Condition]] = dict()

The bounds inferred to rule out overflow (infer_bounds), per input table: also in requires, and assumed like the rest of it.

implied: dict[str, str] = dict()

A SQL condition per input table that every row reaching the result passes, given requires (#81, Rel.need_eval in SubstraitLean/Implied.lean): the transformation gives the same result on the table’s rows that pass it. sverify.io sources read only those, and skip the files whose statistics rule it out.

assumed: list[Issue] = list()

The SUMs assumed to fit their type in every group (64 bits for integers, the result’s precision for decimals), and the operations on finite doubles assumed to stay finite (#575): those the inputs’ row caps (max_rows, #219) and the values’ range do not prove to fit. The job checks each at run time, on the data, and raises where one fails. The proof holds under these assumptions (Rel.noIssue_of_assumedHold). With on_inferred="off" they are errors instead.

params: list[str] = list()

The ibis.param values the transformation was verified with (verify(..., params=...)), as param1 (int64) = 5: every proof is for these values only.

hints: list[str] = list()

What to add to the contract for the issues it names (#379): bounds on a truncated timestamp column, or on the column an integer SUM adds up, with the largest group the bound lets fit.

bounds: dict[str, tuple[int | None, int | None]] = dict()

rows: int | None = None

At most this many output rows, from the inputs’ row caps (max_rows in requires, Rel.maxRows); None if nothing bounds them.

relations: list[RelationRows] = list()

Each relation of the plan, from the result down in pre-order, with the bounds Lean proves on its rows and, for an aggregate, on the rows of a group (#219).

semantics: Semantics = "reference"

The profile the report is under (verify(semantics=...)): "reference", sverify’s reference semantics; "duckdb", what DuckDB computes (#411); "polars"; or "substrait", Substrait’s own (#444).

plan: str | None = None

The plan the report is about, as Substrait protobuf JSON: the transformation as verify compiled it and Lean checked it, with the params bound and the SQL lifted with semantics. run runs it (#461).

observation: Observation = (lambda: _observation.PLAN_BOUND)()

What the result’s consumer observes (sv.equivalent in ensures, #444). When ensures names none: rows as a multiset, doubles within the plan’s bound (floats="plan", printed with the bound, epsilon) and other values exact, the same as sv.equivalent(floats="plan"). Under the plan’s bound a run holds the double columns a postcondition reads to their exact value (sverify.routes.observed). equivalence is the same, by the concept’s name.

stated: bool = False

Whether ensures names the observation (sv.equivalent).

floats_on: dict[str, list[str]] = dict()

Where the observation asks for exact doubles or a tolerance: per engine the reference translates to, why that engine’s doubles may not meet it (empty where they do), checked against the plan’s bound (epsilon) at verify. Empty under floats="plan", which every engine meets. Where no engine meets it, the plan is not proved (floats_unmet).

depends: list[dict] | None = None

The options of the profile the proof depends on (docs/core-semantics.md, step 3c), as the checker reports them: {"group", "option", "behaviours"} rows. None when the checker does not report them; the option-wise transfer check then takes every option of every group the plan calls.

routes: dict[str, Route] = dict()

The route each engine ran the plan by (run(..., route=...), D13), by engine name.

contract: dict | None = None

The request the checker proved, for a check under another profile.

transfer: list[dict] | None = None

Under semantics="substrait", the options where Substrait allows more than the reference, so that the reference’s proof does not carry over: {"group", "option", "preferences", "substrait", "reference"} rows, each with the behaviours the profile allows. Empty when it carries over; None under every other profile.

output: dict[str, Any] = dict()

The output’s columns with their Ibis types.

epsilon: dict[str, dict[str, Any]] | None = None

How far each double output column may be from a result the reference allows on an engine whose summation order differs ({"abs", "rel"} per column, #568), as the checker computes it for this plan; None where it does not.

rows_exact: dict[str, bool] | None = None

Per engine, whether every filter, key and sort of the plan keeps the same rows and groups under the columns’ ε (#568’s threshold rule): a comparison on a double whose threshold lies within ε of its range may flip. None where the checker does not say.

conditions: dict[str, list[Condition]] = dict()

dialect: Literal["ibis", "sql"] = "ibis"

The language of the transformation: the report names functions and writes code in it.

ties: dict[str, list[str]] = dict()

For a result not determined up to row order (deterministic), the sv.unique(...) per input table that would determine it: the partition (or grouping) and order columns of its windows and ordered aggregates.

on_inferred: OnInferred = "ignore"

What the inferred preconditions (inferred) do to the proof (verify(on_inferred=...)): with "error", a plan that needs one is not proved (needed).

inferred_from: dict[str, Issue] = dict()

For each inferred precondition (by label), the runtime error it rules out: where it came from.

postconditions: list[Condition] = list()

The postconditions, as conditions, in the order of ensures (to_substrait ships them).

inputs: dict[str, ibis.Schema] = dict()

The schema of each input table the plan reads, by table name: the columns requires may name, per table, as output holds those ensures may name.