# Realizability

<style>
main table, main .gd-table-scroll > table {
  table-layout: fixed; width: 100% !important; min-width: 0; font-size: 0.85rem;
}
main table th, main table td {
  overflow-wrap: anywhere; white-space: normal; vertical-align: top;
}
main table code { white-space: normal; }
main :not(pre) > code { font-size: 0.875em !important; line-height: inherit; }
main section.level2 {
  border-top: 1px solid var(--bs-border-color, #dee2e6);
  margin-top: 2.25rem; padding-top: 0.75rem;
}
main .ledger-meta {
  font-style: italic; font-size: 0.9em; color: var(--bs-secondary-color, #6c757d);
}
main .ledger-meta p { margin-bottom: 0.75rem; }
</style>

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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md#obligations-option-by-option), 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.

- native: the engine's behaviour is one the reference allows.
- shim: the translation writes the shim first, at its cost: a written argument, an expression per row or group, or a sort.
- observed: the same as a result the reference allows up to an observation (D18), such as rows as a multiset; a postcondition that observes more needs the row's shim, or the plan is refused there.
- observed (tolerance): within the plan's float bound (#85) of a result the reference allows, a tolerance being an observation of doubles.
- precondition: the engine differs only where the reference raises, so a plan verified never to raise never reaches the difference; where the precondition is checked on the data, its guard stays.
- not characterized: outside the prototype slice; the engine's profile allows every behaviour of the core there.

"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](../reference/io.Sink.md#sverify.io.Sink.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](../reference/sql.Dialect.md#sverify.sql.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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R1.json), [duckdb-R15-int-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-int-arith.json) |
| int.arith | `overflow` | raise | `ERROR` | `ERROR` | native; stated `SILENT`, `SATURATE`: not native | fuzz | tested: [duckdb-R1](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R1.json), [duckdb-R15-int-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-int-arith.json) |
| agg.isum | `overflow` | raise | `ERROR` | `ERROR` | native | probe | tested: [duckdb-R6](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R6.json) |
| every | `on_division_by_zero` | raise | `ERROR` | `ERROR` | native; stated `NULL`: not native | fuzz | tested: [duckdb-R2](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R2.json) |
| fp.div | `on_division_by_zero` | raise | `ERROR` | `IEEE` | precondition: no divisor is 0; stated `NULL`, `LIMIT`: not native | fuzz | tested: [duckdb-R5](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R5.json) |
| every | `division_type` | choose | `TRUNCATE` | `TRUNCATE` | native | fuzz | tested: [duckdb-R3](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R3.json) |
| int.div | `division_type` | choose | `TRUNCATE` | `TRUNCATE` | native; stated `FLOOR`: not native | fuzz | tested: [duckdb-R3](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R3.json) |
| int.mod | `division_type` | choose | `TRUNCATE` | `TRUNCATE` | native; stated `FLOOR`: not native | fuzz | tested: [duckdb-R3](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R3.json) |
| every | `min_mod_neg_one` | choose | `ZERO` | `ERROR` | shim `MIN % -1 written out` (expression) | probe | tested: [duckdb-R15-int-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-int-modulus.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-round.json) |
| every | `on_domain_error` | raise | `ERROR` | `NAN` | precondition: every argument is in its function's domain | fuzz | tested: [duckdb-R15-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-double-arith.json) |
| int.div | `on_domain_error` | raise | `NAN`, `NULL`, `ERROR` | `NAN`, `NULL`, `ERROR` | native | fuzz | tested: [duckdb-R15-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-double-arith.json) |
| int.pow | `on_domain_error` | raise | `NAN`, `NULL`, `ERROR` | `NAN`, `NULL`, `ERROR` | native | fuzz | tested: [duckdb-R15-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-double-arith.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-double-arith.json) |
| every | `zero_sign` | choose | `ONE_ZERO` | `IEEE` | shim [Dialect.canon](../reference/sql.Dialect.md#sverify.sql.Dialect.canon) (expression) | probe | tested: [duckdb-R14](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R14.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-arg-min-nulls.json) |
| every | `nan_kind` | choose | `ONE_NAN` | `IEEE` | observed: up to zeros canon | probe | tested: [duckdb-signbit](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-signbit.json) |
| every | `negative_start` | choose | `WRAP_FROM_END` | `WRAP_FROM_END` | native; stated `LEFT_OF_BEGINNING`: not native | engine_test | tested: [duckdb-R13](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R13.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-sum-double.json), [duckdb-avg-double](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-avg-double.json) |
| every | `stat_algo` | open | `GENERIC` | `WELFORD_CHAN` | native | proof | proved `FloatBounds.StdModel.core_var_chan`; [duckdb-var-stddev](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-var-stddev.json), [duckdb-covar](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-covar.json), [duckdb-corr](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-corr.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R6.json) |
| every | `quantile_interp` | open | `BETWEEN` | `LINEAR` | native | probe | tested: [duckdb-quantile-cont-interpolation](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-quantile-cont-interpolation.json) |
| every | `tie_pick` | open | `ANY_ROW` | `FIRST_READ` | native | probe | tested: [duckdb-mode-ties](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-mode-ties.json), [duckdb-arg-min-nulls](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-arg-min-nulls.json) |
| every | `tie_order` | open | `ANY` | `ANY` | native | probe | tested: [duckdb-sort-ties](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-sort-ties.json), [duckdb-mode-ties](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-mode-ties.json) |
| every | `null_order` | choose | `NULLS_LAST` | `NULLS_LAST` | native | engine_test | tested: [duckdb-F2](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-F2.json) |
| 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](../reference/sql.Dialect.md#sverify.sql.Dialect.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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/facts/duckdb-R15-double-arith.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-arith.json), [polars-int-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-divide.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-arith.json), [polars-int-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-divide.json) |
| dec.arith | `overflow` | raise | `ERROR` | `ERROR` | native | probe | tested: [polars-decimal-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-decimal-arith.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-sum-int.json) |
| every | `on_division_by_zero` | raise | `ERROR` | `NULL` | precondition: no divisor is 0 | proof | proved `Rel.polars_sound`; [polars-int-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-divide.json), [polars-int-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-modulus.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-divide.json) |
| every | `division_type` | choose | `TRUNCATE` | `FLOOR` | shim `int_mod_trunc` (expression) | proof | proved `Polars.int_mod_trunc`; [polars-int-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-modulus.json) |
| int.div | `division_type` | choose | `TRUNCATE` | `FLOOR` | shim `int_div_trunc` (expression) | proof | proved `Polars.int_div_trunc`; [polars-int-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-divide.json) |
| int.mod | `division_type` | choose | `TRUNCATE` | `FLOOR` | shim `int_mod_trunc` (expression) | proof | proved `Polars.int_mod_trunc`; [polars-int-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-modulus.json) |
| fp.mod | `division_type` | choose | `TRUNCATE` | `FLOOR` | shim `column_divisor` (expression) | probe | tested: [polars-double-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-modulus.json), [polars-scalar-divisor](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-scalar-divisor.json) |
| every | `min_mod_neg_one` | choose | `ZERO` | `ZERO` | native | proof | proved `Rel.polars_sound`; [polars-int-modulus](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-int-modulus.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-decimal-arith.json), [polars-decimal-casts](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-decimal-casts.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-decimal-arith.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-round.json) |
| fp.div | `rounding` | choose | `TIE_TO_EVEN` | `TIE_TO_EVEN`, `RECIPROCAL` | observed: within the plan's bound | probe | tested: [polars-scalar-divisor](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-scalar-divisor.json) |
| every | `on_domain_error` | raise | `ERROR` | `NAN` | precondition: every argument is in its function's domain | proof | proved `Rel.polars_sound`; [polars-double-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-divide.json) |
| int.div | `on_domain_error` | raise | `NAN`, `NULL`, `ERROR` | `NAN`, `NULL`, `ERROR` | native | proof | proved `Rel.polars_sound`; [polars-double-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-divide.json) |
| int.pow | `on_domain_error` | raise | `NAN`, `NULL`, `ERROR` | `NAN`, `NULL`, `ERROR` | native | proof | proved `Rel.polars_sound`; [polars-double-divide](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-divide.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-arith.json) |
| every | `zero_sign` | choose | `ONE_ZERO` | `IEEE` | shim `one_zero` (expression) | proof | proved `Polars.one_zero`; [polars-zero-sign](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-zero-sign.json), [polars-zero-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-zero-order.json) |
| agg.order | `zero_sign` | choose | `ONE_ZERO` | `IEEE` | shim `one_zero` (expression) | proof | proved `Polars.one_zero`; [polars-zero-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-zero-order.json), [polars-min-max-zero](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-min-max-zero.json) |
| fp.arith | `zero_sign` | choose | `ONE_ZERO` | `IEEE` | shim `one_zero` (expression) | proof | proved `Polars.one_zero`; [polars-zero-sign](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-zero-sign.json), [polars-zero-add](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-zero-add.json) |
| every | `nan_equality` | choose | `NAN_IS_NAN` | `NAN_IS_NAN` | native | probe | tested: [polars-nan-equality](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-nan-equality.json) |
| every | `nan_order` | choose | `GREATEST` | `GREATEST` | native | probe | tested: [polars-nan-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-nan-order.json) |
| agg.order | `nan_order` | choose | `GREATEST` | `IGNORED` | shim `max_nan_greatest` (expression) | proof | proved `Polars.max_nan_greatest`; [polars-min-max-nan](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-min-max-nan.json) |
| every | `nan_kind` | choose | `ONE_NAN` | `IEEE` | observed: up to zeros canon | probe | tested: [polars-nan-sign](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-nan-sign.json) |
| every | `negative_start` | choose | `WRAP_FROM_END` | `WRAP_FROM_END` | native; stated `LEFT_OF_BEGINNING`: not native | probe | tested: [polars-substring](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-substring.json) |
| every | `substring_range` | raise | `ERROR` | `ERROR`, `COMPUTE` | not characterized | missing |  |
| every | `case_sensitivity` | choose | `CASE_SENSITIVE` | `CASE_SENSITIVE` | native | probe | tested: [polars-match-functions](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-match-functions.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-sum-float.json), [polars-mean-float](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-mean-float.json) |
| every | `stat_algo` | open | `GENERIC` | `WELFORD_CHAN` | native | probe | tested: [polars-var-std](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-var-std.json), [polars-cov](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-cov.json), [polars-corr](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-corr.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-avg-int.json) |
| every | `quantile_interp` | open | `BETWEEN` | `LINEAR` | native | probe | tested: [polars-quantile](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-quantile.json) |
| every | `tie_pick` | open | `ANY_ROW` | `FIRST_READ` | native | probe | tested: [polars-first-last](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-first-last.json) |
| every | `tie_order` | open | `ANY` | `ANY` | native | proof | proved `Polars.tie_order`; [polars-sort-stability](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-sort-stability.json), [polars-first-last](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-first-last.json) |
| every | `null_order` | choose | `NULLS_LAST` | `NULLS_FIRST` | shim `null_order` (argument) | proof | proved `Polars.null_order`; [polars-null-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-null-order.json) |
| every | `clustered` | open | `ADJACENT` | `ADJACENT` | shim `sort on the keys` (sort) | probe | tested: [polars-clustered](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-clustered.json) |
| every | `ntile_spread` | choose | `STANDARD` | `STANDARD` | not characterized | missing |  |
| every | [float_to_int](../reference/sql.Dialect.md#sverify.sql.Dialect.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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-sum-int.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-double-arith.json) |
| every | `null_join_keys` | choose | `NO_MATCH` | `NO_MATCH` | native | probe | tested: [polars-null-keys](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-null-keys.json) |
| 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](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-substring.json) |
| str.match | `string_positions` | choose | `ONE_BASED_CHARS` | `ZERO_BASED_BYTES` | shim `strpos_chars` (expression) | proof | proved `Polars.strpos_chars`; [polars-strpos](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-strpos.json) |

Refused on Polars, with no expression there:

- `md5` ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- `sha256` ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- `levenshtein` ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- [repeat](../reference/sql.Dialect.md#sverify.sql.Dialect.repeat) ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- `ascii` ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- [like](../reference/sql.Dialect.md#sverify.sql.Dialect.like) ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))
- [ilike](../reference/sql.Dialect.md#sverify.sql.Dialect.ilike) ([polars-string-functions-missing](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/facts/polars-string-functions-missing.json))