Skip to main content

Report.from_substrait()

Read a plan to_substrait exported, and prove its contract again

Usage

Source

Report.from_substrait(data)

with the checker (#664).

The plan goes to the checker as it was exported, pinned options, shims and all, with the preconditions and postconditions it carries; the report says what the checker proves of it now. For an export of a verified plan, proved is true again, with the same postconditions.

Parameters

data: str | bytes | Mapping[str, Any]
The export: protobuf JSON (a string or its dict) or bytes.

Returns

Report

A Report of the plan: its postconditions with their status,

the runtime errors the checker cannot rule out, the facts on

each output column and the options the proof depends on. Facts

are in Lean’s notation, and nothing is known of the Ibis types.

the runtime errors the checker cannot rule out, the facts on

each output column and the options the proof depends on. Facts

are in Lean’s notation, and nothing is known of the Ibis types.

Raises

ValueError
The plan carries no sverify contract, or the checker rejects the plan.