Skip to main content

Realizability

How a plan verified under the reference runs on each engine

For each engine and each option of the catalogue, how a plan verified under the reference runs there: obligations reference E of core-semantics.md, computed from the reference’s choices and tools and the engine’s choices and observation rows (SubstraitLean/Obligations.lean). A row is per option, or per function group where a profile chooses by group.

“Stated … not native” lists the behaviours a plan may state for a Substrait option, other than the default, that the engine does not give as it is.

Evidence is the Lean theorem a row rests on, or the facts and tests that record what the engine does. A row’s level is proof where a Lean lemma about the engine covers it (its trusted model rests on the facts it cites), else the strongest check among its facts (docs < source < engine_test < probe < fuzz), and missing where no fact records the engine’s behaviour; Choice.le_sound relates the tables only. The shim count per engine is D9’s measure of few shims.

Summary

Engine Version Translation Shims native observed observed (tolerance) precondition refused not characterized Refused functions
DuckDB 2.0.0 Rel.duckdb_refines 3 24 1 1 4 0 15 0
Polars 2.1.0 Rel.polars_sound 14 14 1 2 8 0 15 7

Rows per evidence level:

Engine proof fuzz probe engine_test source docs missing
DuckDB 3 12 10 2 0 0 21
Polars 28 0 13 0 0 0 16

Shims

Engine Shim Cost Options
DuckDB MIN % -1 written out expression min_mod_neg_one
DuckDB Dialect.canon expression zero_sign
DuckDB ORDER BY the keys sort clustered
Polars int_mod_trunc expression division_type, int.mod: division_type
Polars int_div_trunc expression int.div: division_type
Polars column_divisor expression fp.mod: division_type
Polars decimal_round_half_away expression decimal_rescale
Polars decimal_div_half_away expression dec.div: decimal_rescale
Polars round_half_away argument fp.round: rounding
Polars one_zero expression zero_sign, agg.order: zero_sign, fp.arith: zero_sign
Polars max_nan_greatest expression agg.order: nan_order
Polars avg_int_declared expression avg_int_result
Polars null_order argument null_order
Polars sort on the keys sort clustered
Polars sum_empty_null expression empty_group_aggregates
Polars substring_wrap expression str.sub: string_positions
Polars strpos_chars expression str.match: string_positions

DuckDB 2.0.0

3 shims (2 expression, 1 sort). The translation as a whole rests on Rel.duckdb_refines.

Group Option Reference’s tool Reference DuckDB Case Level Evidence
every overflow raise ERROR ERROR native fuzz tested: duckdb-R1, duckdb-R15-int-arith
int.arith overflow raise ERROR ERROR native; stated SILENT, SATURATE: not native fuzz tested: duckdb-R1, duckdb-R15-int-arith
agg.isum overflow raise ERROR ERROR native probe tested: duckdb-R6
every on_division_by_zero raise ERROR ERROR native; stated NULL: not native fuzz tested: duckdb-R2
fp.div on_division_by_zero raise ERROR IEEE precondition: no divisor is 0; stated NULL, LIMIT: not native fuzz tested: duckdb-R5
every division_type choose TRUNCATE TRUNCATE native fuzz tested: duckdb-R3
int.div division_type choose TRUNCATE TRUNCATE native; stated FLOOR: not native fuzz tested: duckdb-R3
int.mod division_type choose TRUNCATE TRUNCATE native; stated FLOOR: not native fuzz tested: duckdb-R3
every min_mod_neg_one choose ZERO ERROR shim MIN % -1 written out (expression) probe tested: duckdb-R15-int-modulus
every shift_range raise DROP_BITS ERROR, ZERO, DROP_BITS not characterized missing
every decimal_rescale choose TIE_AWAY_FROM_ZERO TIE_AWAY_FROM_ZERO, TIE_TO_EVEN, TRUNCATE not characterized missing
every rounding choose TIE_TO_EVEN TIE_TO_EVEN native missing proved Choice.le_sound
fp.round rounding choose TIE_AWAY_FROM_ZERO TIE_AWAY_FROM_ZERO native probe tested: duckdb-R15-round
every on_domain_error raise ERROR NAN precondition: every argument is in its function’s domain fuzz tested: duckdb-R15-double-arith
int.div on_domain_error raise NAN, NULL, ERROR NAN, NULL, ERROR native fuzz tested: duckdb-R15-double-arith
int.pow on_domain_error raise NAN, NULL, ERROR NAN, NULL, ERROR native fuzz tested: duckdb-R15-double-arith
every on_log_zero raise ERROR NAN, ERROR, MINUS_INFINITY not characterized missing
every nan_creation raise ERROR NAN precondition: no operation makes a NaN of non-NaN values (∞ − ∞, 0 · ∞, ∞ / ∞, #257) fuzz tested: duckdb-R15-double-arith
every zero_sign choose ONE_ZERO IEEE shim Dialect.canon (expression) probe tested: duckdb-R14
every nan_equality choose NAN_IS_NAN NAN_IS_NAN native missing proved Choice.le_sound
every nan_order choose GREATEST GREATEST native probe tested: duckdb-arg-min-nulls
every nan_kind choose ONE_NAN IEEE observed: up to zeros canon probe tested: duckdb-signbit
every negative_start choose WRAP_FROM_END WRAP_FROM_END native; stated LEFT_OF_BEGINNING: not native engine_test tested: duckdb-R13
every substring_range raise ERROR ERROR, COMPUTE not characterized missing
every case_sensitivity choose CASE_SENSITIVE CASE_SENSITIVE native missing proved Choice.le_sound
every char_set choose UTF8 UTF8, ASCII_ONLY not characterized missing
every null_handling choose ACCEPT_NULLS IGNORE_NULLS, ACCEPT_NULLS not characterized missing
every date_range raise ERROR ERROR, COMPUTE not characterized missing
every time_interval_months raise none DROP_MONTHS, ERROR not characterized missing
every list_null_order choose NULL NULL, GREATEST, LEAST not characterized missing
agg.order list_null_order choose GREATEST NULL, GREATEST, LEAST not characterized missing
every sum_order open ANY ANY, SCALED_CONSTANT observed: within the plan’s bound proof proved FloatBounds.StdModel.epsilon_sum; duckdb-sum-double, duckdb-avg-double
every stat_algo open GENERIC WELFORD_CHAN native proof proved FloatBounds.StdModel.core_var_chan; duckdb-var-stddev, duckdb-covar, duckdb-corr
every stat_degenerate choose NULL NULL, NAN, ERROR not characterized missing
every avg_int_result choose DECLARED_TYPE EXACT_TRUNCATE native probe tested: duckdb-R6
every quantile_interp open BETWEEN LINEAR native probe tested: duckdb-quantile-cont-interpolation
every tie_pick open ANY_ROW FIRST_READ native probe tested: duckdb-mode-ties, duckdb-arg-min-nulls
every tie_order open ANY ANY native probe tested: duckdb-sort-ties, duckdb-mode-ties
every null_order choose NULLS_LAST NULLS_LAST native engine_test tested: duckdb-F2
every clustered open ADJACENT ADJACENT shim ORDER BY the keys (sort) proof proved Rel.duckdb_refines
every ntile_spread choose STANDARD STANDARD not characterized missing
every float_to_int choose TRUNCATE TRUNCATE, TIE_AWAY_FROM_ZERO, TIE_TO_EVEN not characterized missing
every cast_failure raise THROW_EXCEPTION THROW_EXCEPTION, RETURN_NULL not characterized missing
every distribution choose SAMPLE SAMPLE, POPULATION not characterized missing
every empty_group_aggregates choose NULL NULL native missing proved Choice.le_sound
every float_overflow raise ERROR INFINITY precondition: no finite double operation overflows to ±∞: proved from the bounds, or checked on the data (#575) fuzz tested: duckdb-R15-double-arith
every null_join_keys choose NO_MATCH NO_MATCH native missing proved Choice.le_sound
every string_positions choose ONE_BASED_CHARS ONE_BASED_CHARS native missing proved Choice.le_sound

Polars 2.1.0

14 shims (2 argument, 11 expression, 1 sort). The translation as a whole rests on Rel.polars_sound.

Group Option Reference’s tool Reference Polars Case Level Evidence
every overflow raise ERROR SILENT precondition: every result fits its declared width: proved from the inferred bounds (#244), or a SUM’s checked on the data (#316) proof proved Rel.polars_sound; polars-int-arith, polars-int-divide
int.arith overflow raise ERROR SILENT precondition: every result fits its declared width: proved from the inferred bounds (#244), or a SUM’s checked on the data (#316); stated SATURATE: not native proof proved Rel.polars_sound; polars-int-arith, polars-int-divide
dec.arith overflow raise ERROR ERROR native probe tested: polars-decimal-arith
agg.isum overflow raise ERROR SILENT precondition: every result fits its declared width: proved from the inferred bounds (#244), or a SUM’s checked on the data (#316) proof proved Polars.sum_leaves_i64; polars-sum-int
every on_division_by_zero raise ERROR NULL precondition: no divisor is 0 proof proved Rel.polars_sound; polars-int-divide, polars-int-modulus
fp.div on_division_by_zero raise ERROR IEEE precondition: no divisor is 0; stated NULL, LIMIT: not native proof proved Rel.polars_sound; polars-double-divide
every division_type choose TRUNCATE FLOOR shim int_mod_trunc (expression) proof proved Polars.int_mod_trunc; polars-int-modulus
int.div division_type choose TRUNCATE FLOOR shim int_div_trunc (expression) proof proved Polars.int_div_trunc; polars-int-divide
int.mod division_type choose TRUNCATE FLOOR shim int_mod_trunc (expression) proof proved Polars.int_mod_trunc; polars-int-modulus
fp.mod division_type choose TRUNCATE FLOOR shim column_divisor (expression) probe tested: polars-double-modulus, polars-scalar-divisor
every min_mod_neg_one choose ZERO ZERO native proof proved Rel.polars_sound; polars-int-modulus
every shift_range raise DROP_BITS ERROR, ZERO, DROP_BITS not characterized missing
every decimal_rescale choose TIE_AWAY_FROM_ZERO TIE_TO_EVEN shim decimal_round_half_away (expression) proof proved Polars.decimal_round_half_away; polars-decimal-arith, polars-decimal-casts
dec.div decimal_rescale choose TIE_AWAY_FROM_ZERO TIE_TO_EVEN shim decimal_div_half_away (expression) proof proved Polars.decimal_div_half_away; polars-decimal-arith
every rounding choose TIE_TO_EVEN TIE_TO_EVEN native missing proved Choice.le_sound
fp.round rounding choose TIE_AWAY_FROM_ZERO TIE_TO_EVEN shim round_half_away (argument) proof proved Polars.round_half_away; polars-round
fp.div rounding choose TIE_TO_EVEN TIE_TO_EVEN, RECIPROCAL observed: within the plan’s bound probe tested: polars-scalar-divisor
every on_domain_error raise ERROR NAN precondition: every argument is in its function’s domain proof proved Rel.polars_sound; polars-double-divide
int.div on_domain_error raise NAN, NULL, ERROR NAN, NULL, ERROR native proof proved Rel.polars_sound; polars-double-divide
int.pow on_domain_error raise NAN, NULL, ERROR NAN, NULL, ERROR native proof proved Rel.polars_sound; polars-double-divide
every on_log_zero raise ERROR NAN, ERROR, MINUS_INFINITY not characterized missing
every nan_creation raise ERROR NAN precondition: no operation makes a NaN of non-NaN values (∞ − ∞, 0 · ∞, ∞ / ∞, #257) proof proved Rel.polars_sound; polars-double-arith
every zero_sign choose ONE_ZERO IEEE shim one_zero (expression) proof proved Polars.one_zero; polars-zero-sign, polars-zero-order
agg.order zero_sign choose ONE_ZERO IEEE shim one_zero (expression) proof proved Polars.one_zero; polars-zero-order, polars-min-max-zero
fp.arith zero_sign choose ONE_ZERO IEEE shim one_zero (expression) proof proved Polars.one_zero; polars-zero-sign, polars-zero-add
every nan_equality choose NAN_IS_NAN NAN_IS_NAN native probe tested: polars-nan-equality
every nan_order choose GREATEST GREATEST native probe tested: polars-nan-order
agg.order nan_order choose GREATEST IGNORED shim max_nan_greatest (expression) proof proved Polars.max_nan_greatest; polars-min-max-nan
every nan_kind choose ONE_NAN IEEE observed: up to zeros canon probe tested: polars-nan-sign
every negative_start choose WRAP_FROM_END WRAP_FROM_END native; stated LEFT_OF_BEGINNING: not native probe tested: polars-substring
every substring_range raise ERROR ERROR, COMPUTE not characterized missing
every case_sensitivity choose CASE_SENSITIVE CASE_SENSITIVE native probe tested: polars-match-functions
every char_set choose UTF8 UTF8, ASCII_ONLY not characterized missing
every null_handling choose ACCEPT_NULLS IGNORE_NULLS, ACCEPT_NULLS not characterized missing
every date_range raise ERROR ERROR, COMPUTE not characterized missing
every time_interval_months raise none DROP_MONTHS, ERROR not characterized missing
every list_null_order choose NULL NULL, GREATEST, LEAST not characterized missing
agg.order list_null_order choose GREATEST NULL, GREATEST, LEAST not characterized missing
every sum_order open ANY SEQUENTIAL, ANY, COMPENSATED observed: within the plan’s bound proof proved FloatBounds.StdModel.epsilon_sum; polars-sum-float, polars-mean-float
every stat_algo open GENERIC WELFORD_CHAN native probe tested: polars-var-std, polars-cov, polars-corr
every stat_degenerate choose NULL NULL, NAN, ERROR not characterized missing
every avg_int_result choose DECLARED_TYPE FP64 shim avg_int_declared (expression) proof proved Polars.avg_int_declared; polars-avg-int
every quantile_interp open BETWEEN LINEAR native probe tested: polars-quantile
every tie_pick open ANY_ROW FIRST_READ native probe tested: polars-first-last
every tie_order open ANY ANY native proof proved Polars.tie_order; polars-sort-stability, polars-first-last
every null_order choose NULLS_LAST NULLS_FIRST shim null_order (argument) proof proved Polars.null_order; polars-null-order
every clustered open ADJACENT ADJACENT shim sort on the keys (sort) probe tested: polars-clustered
every ntile_spread choose STANDARD STANDARD not characterized missing
every float_to_int choose TRUNCATE TRUNCATE, TIE_AWAY_FROM_ZERO, TIE_TO_EVEN not characterized missing
every cast_failure raise THROW_EXCEPTION THROW_EXCEPTION, RETURN_NULL not characterized missing
every distribution choose SAMPLE SAMPLE, POPULATION not characterized missing
every empty_group_aggregates choose NULL ZERO shim sum_empty_null (expression) proof proved Polars.sum_empty_null; polars-sum-int
every float_overflow raise ERROR INFINITY precondition: no finite double operation overflows to ±∞: proved from the bounds, or checked on the data (#575) proof proved Polars.makes_infinite; polars-double-arith
every null_join_keys choose NO_MATCH NO_MATCH native probe tested: polars-null-keys
every string_positions choose ONE_BASED_CHARS none not characterized missing
str.sub string_positions choose ONE_BASED_CHARS ZERO_BASED_CHARS shim substring_wrap (expression) proof proved Polars.substring_wrap; polars-substring
str.match string_positions choose ONE_BASED_CHARS ZERO_BASED_BYTES shim strpos_chars (expression) proof proved Polars.strpos_chars; polars-strpos

Refused on Polars, with no expression there: