Report.run()

Run the plan this report checked (plan) over the tables of

Usage

Source

Report.run(
    con,
    engine=None,
    *,
    route="auto",
    unverified=False,
    deterministic=False,
    reproducible=None,
    check_requires=True,
    streaming="allow",
    check_inputs=None
)

con, so the result is the one the report is about (#461).

The plan reads the tables by the names it was verified with, and runs on engine as sverify.engines.run runs a plan, with the meaning Rel.eval gives it.

A plan that is not proved (proved is False) is refused (UnverifiedRunError), with what was not proved in the message; unverified=True runs it anyway, and says so: a warning (UnverifiedRunWarning), the route "unverified" in routes, and sverify.verified: false in the result’s schema metadata.

The run first chooses how the proof reaches the engine (sverify.routes.choose, #444): "auto" takes the plan natively where it was verified under the engine’s profile, through the reference’s translation where it was verified under the reference, by the option-wise transfer check, or by a re-check under the engine’s profile, and refuses it otherwise. The route goes into routes. Where ensures names no observation (sv.equivalent), the engine’s doubles may differ from the reference’s within the plan’s bound (epsilon), except in the columns a postcondition reads.

Parameters

con: Connection

The connection whose tables the plan reads (sv.connect()).

engine: Engine | Any = None

"duckdb", "polars", "datafusion", "spark", or a Spark session. Default: the connection’s engine.

route: RouteKind | Literal["auto"] = "auto"

"auto" (the default) chooses a route; "native", "translated", "transfer" or "recheck" takes that one or refuses ("reference" is a deprecated alias of "translated").

unverified: bool = False

Run a plan that is not proved, without a route. Default False: such a plan is refused.

deterministic: bool = False

Require a rerun to reproduce the result exactly (reproducible=sv.equivalent(), D10).

reproducible: Observation | None = None

What a rerun must reproduce (D20): the engine’s run-to-run variation must refine it. Default None: determinism is only reported.

check_requires: bool = True

Check the preconditions (requires, the inferred bounds among them) and the assumed SUMs on the tables of con before the run, and refuse a batch that breaks one (check_inputs, #444 goal 1, #604), as transform(check_requires=) does on bound inputs. Default True. False skips the check, for a caller that has made it already: the report’s guarantee then holds only on data that meets them, and a batch that does not may raise on the engine.

streaming: Literal["allow", "require"] = "allow"

On Polars, "require" refuses a plan any of whose nodes runs on the in-memory engine (polars_engine.fallback_nodes); "allow" (the default) runs it. Either way a chosen route records the nodes in Route.fallbacks.

check_inputs: bool | None = None

Deprecated alias of check_requires.

Returns

pa.Table

The result as an Arrow table, with the transformation’s output

names.

Raises

ValueError

The report has no plan (it was not made by verify), or engine is unknown.

sverify.errors.UnverifiedRunError

The plan is not proved, and unverified is False. It is a VerificationError and a RouteError.

sverify.errors.RouteError

No route takes the plan to engine, or, with streaming="require", a node of its Polars plan runs on the in-memory engine.

sverify.routes.EngineVersionError

The engine’s major version is not the one its profile’s facts were probed at.

sverify.errors.PreconditionError

With check_inputs, a precondition does not hold on the data: nothing ran.

Examples

Verify a query, then run what was verified:

con = sv.connect()
con.put("t", pa.table({"host": ["a", "a", "b"], "cpu": [1, 5, 7]}))
report = sv.verify(
    "SELECT host, max(cpu) AS m FROM t WHERE cpu > 3 GROUP BY host",
    tables={"t": con.table("t")},
    ensures=[sv.unique("host")],
)
result = report.run(con)  # refused if report.proved is False