# sverify

> Contracts and incremental views, proven in Lean, on DuckDB, Polars, DataFusion, Snowflake and Spark

## Docs

### API Reference

#### Contracts
> State what a transformation assumes and promises, and have it proved before any data runs.


- [transform](https://alexandernenninger.github.io/substrait-lean/reference/transform.html): Decorate a function from Ibis tables to an Ibis table with a contract
- [verify](https://alexandernenninger.github.io/substrait-lean/reference/verify.html): Try to prove `ensures` about `query` (an Ibis table expression or a
- [unique](https://alexandernenninger.github.io/substrait-lean/reference/unique.html): A key: at most one row per combination of `cols`
- [key](https://alexandernenninger.github.io/substrait-lean/reference/key.html): A primary key: at most one row per combination of `cols`, and no NULL
- [references](https://alexandernenninger.github.io/substrait-lean/reference/references.html): A foreign key: every non-NULL value of `col` occurs in the column `to`
- [Report](https://alexandernenninger.github.io/substrait-lean/reference/Report.html): What the checker proved about a transformation, returned by `verify` and kept
- [Report.from_substrait](https://alexandernenninger.github.io/substrait-lean/reference/Report.from_substrait.html)

#### Report Methods
> Methods for the Report class

- [Report.to_json](https://alexandernenninger.github.io/substrait-lean/reference/Report.to_json.html)
- [Report.from_json](https://alexandernenninger.github.io/substrait-lean/reference/Report.from_json.html)
- [Report.from_substrait](https://alexandernenninger.github.io/substrait-lean/reference/Report.from_substrait.html)
- [Report.to_substrait](https://alexandernenninger.github.io/substrait-lean/reference/Report.to_substrait.html)
- [Report.substrait_contract](https://alexandernenninger.github.io/substrait-lean/reference/Report.substrait_contract.html)
- [Report.to_sql](https://alexandernenninger.github.io/substrait-lean/reference/Report.to_sql.html)
- [Report.check_inputs](https://alexandernenninger.github.io/substrait-lean/reference/Report.check_inputs.html)
- [Report.run](https://alexandernenninger.github.io/substrait-lean/reference/Report.run.html)
- [Report.proved](https://alexandernenninger.github.io/substrait-lean/reference/Report.proved.html)
- [Report.floats_unmet](https://alexandernenninger.github.io/substrait-lean/reference/Report.floats_unmet.html)
- [Report.needed](https://alexandernenninger.github.io/substrait-lean/reference/Report.needed.html)
- [Report.needed_text](https://alexandernenninger.github.io/substrait-lean/reference/Report.needed_text.html)
- [Report.equivalence](https://alexandernenninger.github.io/substrait-lean/reference/Report.equivalence.html)
- [Report.needs](https://alexandernenninger.github.io/substrait-lean/reference/Report.needs.html)
- [Report.needed_conditions](https://alexandernenninger.github.io/substrait-lean/reference/Report.needed_conditions.html)
- [Report.needs_text](https://alexandernenninger.github.io/substrait-lean/reference/Report.needs_text.html)
- [Report.needs_lines](https://alexandernenninger.github.io/substrait-lean/reference/Report.needs_lines.html)
- [Report.errors](https://alexandernenninger.github.io/substrait-lean/reference/Report.errors.html)
- [Report.warnings](https://alexandernenninger.github.io/substrait-lean/reference/Report.warnings.html)
- [Report.suggestions](https://alexandernenninger.github.io/substrait-lean/reference/Report.suggestions.html)
- [Report.unproved](https://alexandernenninger.github.io/substrait-lean/reference/Report.unproved.html)
- [Report.notes](https://alexandernenninger.github.io/substrait-lean/reference/Report.notes.html)
- [Report.route](https://alexandernenninger.github.io/substrait-lean/reference/Report.route.html)
- [Report.verdict](https://alexandernenninger.github.io/substrait-lean/reference/Report.verdict.html)
- [Report.__str__](https://alexandernenninger.github.io/substrait-lean/reference/Report.__str__.html)

#### Transforms, nodes and refresh
> A source piped into a contracted transform, `orders.pipe(paid)`, builds a node. Nodes compose left to right with `.pipe`, are stored with `.write(sink)`, and are kept up to date by `.refresh()`, with update plans proved equal to a full recompute.


- [Node](https://alexandernenninger.github.io/substrait-lean/reference/Node.html): The result of a contracted transform over sources or other nodes
- [sql.Unsupported](https://alexandernenninger.github.io/substrait-lean/reference/sql.Unsupported.html)
- [sql.Dialect](https://alexandernenninger.github.io/substrait-lean/reference/sql.Dialect.html)
- [sql.parse_plan](https://alexandernenninger.github.io/substrait-lean/reference/sql.parse_plan.html)
- [sql.to_sql](https://alexandernenninger.github.io/substrait-lean/reference/sql.to_sql.html)
- [sql.dialect_of](https://alexandernenninger.github.io/substrait-lean/reference/sql.dialect_of.html)
- [sql.Kind](https://alexandernenninger.github.io/substrait-lean/reference/sql.Kind.html)
- [sql.DIALECTS](https://alexandernenninger.github.io/substrait-lean/reference/sql.DIALECTS.html)
- [group](https://alexandernenninger.github.io/substrait-lean/reference/group.html): Several nodes to refresh together, against the same source versions:
- [io.Changes](https://alexandernenninger.github.io/substrait-lean/reference/io.Changes.html)
- [nodes.Group](https://alexandernenninger.github.io/substrait-lean/reference/nodes.Group.html)
- [nodes.Refresh](https://alexandernenninger.github.io/substrait-lean/reference/nodes.Refresh.html)
- [nodes.Status](https://alexandernenninger.github.io/substrait-lean/reference/nodes.Status.html)
- [nodes.NodeStatus](https://alexandernenninger.github.io/substrait-lean/reference/nodes.NodeStatus.html)
- [nodes.StageRefresh](https://alexandernenninger.github.io/substrait-lean/reference/nodes.StageRefresh.html)

#### Node Methods
> Methods for the Node class

- [Node.__repr__](https://alexandernenninger.github.io/substrait-lean/reference/Node.__repr__.html)
- [Node.schema](https://alexandernenninger.github.io/substrait-lean/reference/Node.schema.html)
- [Node.internal_plan](https://alexandernenninger.github.io/substrait-lean/reference/Node.internal_plan.html)
- [Node.plan](https://alexandernenninger.github.io/substrait-lean/reference/Node.plan.html)
- [Node.report](https://alexandernenninger.github.io/substrait-lean/reference/Node.report.html)
- [Node.to_substrait](https://alexandernenninger.github.io/substrait-lean/reference/Node.to_substrait.html)
- [Node.to_sql](https://alexandernenninger.github.io/substrait-lean/reference/Node.to_sql.html)
- [Node.pipe](https://alexandernenninger.github.io/substrait-lean/reference/Node.pipe.html)
- [Node.write](https://alexandernenninger.github.io/substrait-lean/reference/Node.write.html)
- [Node.refresh](https://alexandernenninger.github.io/substrait-lean/reference/Node.refresh.html)
- [Node.status](https://alexandernenninger.github.io/substrait-lean/reference/Node.status.html)
- [Node.table](https://alexandernenninger.github.io/substrait-lean/reference/Node.table.html)
- [Node.versions](https://alexandernenninger.github.io/substrait-lean/reference/Node.versions.html)
- [Node.to_arrow](https://alexandernenninger.github.io/substrait-lean/reference/Node.to_arrow.html)
- [Node.quarantined](https://alexandernenninger.github.io/substrait-lean/reference/Node.quarantined.html)
- [Node.to_polars](https://alexandernenninger.github.io/substrait-lean/reference/Node.to_polars.html)
- [Node.to_pandas](https://alexandernenninger.github.io/substrait-lean/reference/Node.to_pandas.html)

#### Sources and sinks
> Delta Lake and Iceberg tables as versioned sources, sources of preconditions, and sinks that carry the contract (`sverify.io`).


- [io.DeltaSource](https://alexandernenninger.github.io/substrait-lean/reference/io.DeltaSource.html)
- [io.DeltaSink](https://alexandernenninger.github.io/substrait-lean/reference/io.DeltaSink.html)
- [io.IcebergSource](https://alexandernenninger.github.io/substrait-lean/reference/io.IcebergSource.html)
- [io.IcebergSink](https://alexandernenninger.github.io/substrait-lean/reference/io.IcebergSink.html)
- [io.StaticSource](https://alexandernenninger.github.io/substrait-lean/reference/io.StaticSource.html)
- [io.SinkWrite](https://alexandernenninger.github.io/substrait-lean/reference/io.SinkWrite.html)
- [io.Contract](https://alexandernenninger.github.io/substrait-lean/reference/io.Contract.html)
- [io.Storage](https://alexandernenninger.github.io/substrait-lean/reference/io.Storage.html)

#### Your own sources and sinks
> Read from an API, a database or a folder of files with one `read` method, and write anywhere with one `write` method; sverify keeps the versions, the changes, the contract and the exactly-once writes. Table formats with metadata implement the full `VersionedSource` protocol.


- [io.Source](https://alexandernenninger.github.io/substrait-lean/reference/io.Source.html)
- [io.Batch](https://alexandernenninger.github.io/substrait-lean/reference/io.Batch.html)
- [io.from_query](https://alexandernenninger.github.io/substrait-lean/reference/io.from_query.html)
- [io.from_frame](https://alexandernenninger.github.io/substrait-lean/reference/io.from_frame.html)
- [io.from_files](https://alexandernenninger.github.io/substrait-lean/reference/io.from_files.html)
- [io.Sink](https://alexandernenninger.github.io/substrait-lean/reference/io.Sink.html)
- [io.SinkChange](https://alexandernenninger.github.io/substrait-lean/reference/io.SinkChange.html)
- [io.sink_from](https://alexandernenninger.github.io/substrait-lean/reference/io.sink_from.html)
- [io.VersionedSource](https://alexandernenninger.github.io/substrait-lean/reference/io.VersionedSource.html)
- [io.Snapshot](https://alexandernenninger.github.io/substrait-lean/reference/io.Snapshot.html)
- [io.SourceBatch](https://alexandernenninger.github.io/substrait-lean/reference/io.SourceBatch.html)

#### Engines and SQL
> Run a checked plan on DuckDB, Polars, DataFusion or Spark, or write it as DuckDB, Snowflake or Spark SQL (`Node.to_sql`, `Report.to_sql`; `sverify.engines`). `Dialect`'s SQL-writing methods change as functions land, so they are left out; subclassing it is outside the 1.x promise.


- [connect](https://alexandernenninger.github.io/substrait-lean/reference/connect.html): A new, empty connection whose plans run on `engine`
- [engines.run](https://alexandernenninger.github.io/substrait-lean/reference/engines.run.html)
- [engines.ENGINES](https://alexandernenninger.github.io/substrait-lean/reference/engines.ENGINES.html)
- [engines.Connection](https://alexandernenninger.github.io/substrait-lean/reference/engines.Connection.html)
- [engines.Dialect](https://alexandernenninger.github.io/substrait-lean/reference/engines.Dialect.html)
- [engines.DUCKDB](https://alexandernenninger.github.io/substrait-lean/reference/engines.DUCKDB.html)
- [engines.SNOWFLAKE](https://alexandernenninger.github.io/substrait-lean/reference/engines.SNOWFLAKE.html)
- [engines.SPARK](https://alexandernenninger.github.io/substrait-lean/reference/engines.SPARK.html)
- [engines.Unsupported](https://alexandernenninger.github.io/substrait-lean/reference/engines.Unsupported.html)
- [engines.SPARK_CONF](https://alexandernenninger.github.io/substrait-lean/reference/engines.SPARK_CONF.html)
- [engines.run_sharded](https://alexandernenninger.github.io/substrait-lean/reference/engines.run_sharded.html)

#### ASOF joins
> Align two time series, each row with the latest earlier row of the other.

- [asof_join](https://alexandernenninger.github.io/substrait-lean/reference/asof_join.html): Match each left row with the latest right row at or before it

#### Plans
> The low-level layer: Substrait plans, Lean's written form of them, the SQL of a plan, and the update plans of incremental maintenance (`sverify.engines`). They take sverify's internal plan, so they are outside the 1.x promise and may change in a minor release; `Node.to_sql`, `Report.to_sql` and `Report.to_substrait` are the stable way to a plan.


- [engines.to_sql](https://alexandernenninger.github.io/substrait-lean/reference/engines.to_sql.html)
- [engines.substrait_json](https://alexandernenninger.github.io/substrait-lean/reference/engines.substrait_json.html)
- [engines.written_plan](https://alexandernenninger.github.io/substrait-lean/reference/engines.written_plan.html)
- [engines.run_substrait_json](https://alexandernenninger.github.io/substrait-lean/reference/engines.run_substrait_json.html)
- [engines.delta_plans](https://alexandernenninger.github.io/substrait-lean/reference/engines.delta_plans.html)

#### Testing
> Test transforms and their contracts with pytest (`sverify.testing`). Installing sverify registers a pytest plugin with the fixtures `sv_source` (in-memory sources) and `sv_engine` (a test per installed engine).


- [testing.assert_contract](https://alexandernenninger.github.io/substrait-lean/reference/testing.assert_contract.html)
- [testing.assert_engines_agree](https://alexandernenninger.github.io/substrait-lean/reference/testing.assert_engines_agree.html)
- [testing.cases](https://alexandernenninger.github.io/substrait-lean/reference/testing.cases.html)
- [testing.source](https://alexandernenninger.github.io/substrait-lean/reference/testing.source.html)
- [testing.installed_engines](https://alexandernenninger.github.io/substrait-lean/reference/testing.installed_engines.html)

#### Command line
> The `sverify` command (`sverify.cli`): `check`, `suggest`, `refresh` and `explain` a pipeline's file from a shell, a CI job or an agent.


- [cli.main](https://alexandernenninger.github.io/substrait-lean/reference/cli.main.html)
- [cli.discover](https://alexandernenninger.github.io/substrait-lean/reference/cli.discover.html)
- [cli.summary](https://alexandernenninger.github.io/substrait-lean/reference/cli.summary.html)
- [cli.Discovery](https://alexandernenninger.github.io/substrait-lean/reference/cli.Discovery.html)
- [cli.Checked](https://alexandernenninger.github.io/substrait-lean/reference/cli.Checked.html)

#### Standards
> Contracts in the Open Data Contract Standard (`sverify.odcs`, #791): a node's contract written as ODCS, and ODCS contracts read as conditions.


- [odcs.export](https://alexandernenninger.github.io/substrait-lean/reference/odcs.export.html)
- [odcs.write](https://alexandernenninger.github.io/substrait-lean/reference/odcs.write.html)
- [odcs.read](https://alexandernenninger.github.io/substrait-lean/reference/odcs.read.html)
- [odcs.OdcsContract](https://alexandernenninger.github.io/substrait-lean/reference/odcs.OdcsContract.html)
- [odcs.Unread](https://alexandernenninger.github.io/substrait-lean/reference/odcs.Unread.html)
- [odcs.UnreadRuleWarning](https://alexandernenninger.github.io/substrait-lean/reference/odcs.UnreadRuleWarning.html)

#### Errors
> What sverify raises, and when (`sverify.errors`).

- [errors.SverifyError](https://alexandernenninger.github.io/substrait-lean/reference/errors.SverifyError.html)
- [errors.VerificationError](https://alexandernenninger.github.io/substrait-lean/reference/errors.VerificationError.html)
- [errors.PreconditionError](https://alexandernenninger.github.io/substrait-lean/reference/errors.PreconditionError.html)
- [errors.PostconditionError](https://alexandernenninger.github.io/substrait-lean/reference/errors.PostconditionError.html)
- [errors.CompositionError](https://alexandernenninger.github.io/substrait-lean/reference/errors.CompositionError.html)
- [errors.NotIncremental](https://alexandernenninger.github.io/substrait-lean/reference/errors.NotIncremental.html)
- [errors.AuditError](https://alexandernenninger.github.io/substrait-lean/reference/errors.AuditError.html)
- [errors.SchemaError](https://alexandernenninger.github.io/substrait-lean/reference/errors.SchemaError.html)
- [errors.SqlError](https://alexandernenninger.github.io/substrait-lean/reference/errors.SqlError.html)
- [errors.ExportError](https://alexandernenninger.github.io/substrait-lean/reference/errors.ExportError.html)
- [errors.Unsupported](https://alexandernenninger.github.io/substrait-lean/reference/errors.Unsupported.html)