## Report What the checker proved about a transformation, returned by [verify](verify.md#sverify.verify) and kept Usage ``` python 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](io.Snapshot.md#sverify.io.Snapshot.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 (`SUM`s 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](engines.to_sql.md#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](engines.to_sql.md#sverify.engines.to_sql), or as JSON to [sverify.engines.run](engines.run.md#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 `SUM`s 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](verify.md#sverify.verify) compiled it and Lean checked it, with the `params` bound and the SQL lifted with `semantics`. [run](Report.run.md#sverify.Report.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](Report.equivalence.md#sverify.Report.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](verify.md#sverify.verify). Empty under `floats="plan"`, which every engine meets. Where no engine meets it, the plan is not proved ([floats_unmet](Report.floats_unmet.md#sverify.Report.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](Report.needed.md#sverify.Report.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](Node.to_substrait.md#sverify.Node.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.