# Spec gaps

<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>

Behaviour Substrait's extension YAMLs leave unspecified, though Substrait could express it with an option, an option's value or a default, where engines differ ([core-semantics.md](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md)).


# Substrait


## ST-1: `shift_left` and `shift_right` (`functions_arithmetic.yaml`) do not say what a shift count below 0 or at …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`shift_left` and `shift_right` (`functions_arithmetic.yaml`) do not say what a shift count below 0 or at least the base's width gives, nor whether `shift_left` may shift bits out. They have no option for it. A negative base is allowed by the test cases (`shift_left(-3::i64, 1::i32) = -6::i64`).

Reproduction:

- `shift_left(1::i64, 64)`, `shift_right(-5::i64, 64)`, `shift_left(-1::i64, 1)`, `shift_left(2^62::i64, 2)`: the YAML's descriptions define none of them.
- DuckDB 2.0: `1 << 64` raises, `-1 << 1` raises, `(2^62) << 2` raises (a bit shifted out), `-5 >> 64` is `0`.

How sverify handles it:

- The core allows each engine's recorded behaviour (raise, `0`, drop the bits) as the option `shift_range` (docs/core-semantics.md, D3). The reference drops the bits shifted out and raises for a count outside `[0, 63]`; DuckDB's written plan guards both shifts.
- Could be expressed as: An option such as `on_shift_overflow: [ERROR, ZERO, WRAP]` for the count, and the existing `overflow` for bits shifted out of `shift_left`.

Status: Still open on main (a4d8e00342d0, = v0.108.0): [`functions_arithmetic.yaml` L982-L1046](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L982-L1046) define the shifts by description only, with no option and nothing on a count outside `[0, width)` or bits shifted out of `shift_left`. The test cases allow a negative base (`shift_left.test` L9-L12: `shift_left(-3::i64, 1::i32) = -6::i64`). No existing issue; options in general: [\#254](https://github.com/substrait-io/substrait/issues/254).

See: facts [duckdb-R15-shift-left](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R15-shift-left), [duckdb-R15-shift-right](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R15-shift-right), [polars-int-shift](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-int-shift); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/pull/799>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml shift\_\* and tests/cases/arithmetic/shift\_\*.test on main; the gap is there, except a negative base, which the test cases allow


## ST-2: `atan2` takes `on_domain_error: [NAN, ERROR]`, but the YAML does not say what its domain is, so whether …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`atan2` takes `on_domain_error: [NAN, ERROR]`, but the YAML does not say what its domain is, so whether `atan2(0, 0)` is a domain error is open. IEEE 754 and C's `atan2` give `±0` (or `±π`) there.

Reproduction:

- `atan2(0.0::fp64, 0.0::fp64)` with `on_domain_error: ERROR`: raise, or `0`?
- DuckDB 2.0: `atan2(0, 0)` is `0` under every setting.

How sverify handles it:

- The reference raises (`Issue.domain`); the core allows `0` as well. DuckDB's written plan raises at `(0, 0)`.
- Could be expressed as: State the domain of `atan2` in its description (all pairs, following IEEE 754, or all but `(0, 0)`).

Status: Still open on main (a4d8e00342d0): [`functions_arithmetic.yaml` L702-L726](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L702-L726) gives `atan2` `on_domain_error: [NAN, ERROR]` without saying what its domain is; `atan2.test` has no `(0, 0)` case. No existing issue; options undocumented in general: [\#254](https://github.com/substrait-io/substrait/issues/254).

See: facts [duckdb-R15-atan2](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R15-atan2), [polars-atan2](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-atan2); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/issues/254>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml atan2 and tests/cases/arithmetic/atan2.test on main; the gap is there


## ST-3: `corr` says what no input gives (null); `variance` and `std_dev` say nothing about it, though they return …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`corr` says what no input gives (null); `variance` and `std_dev` say nothing about it, though they return nullable types. None of them says anything about the degenerate cases: `corr` of one pair or of a side whose values are all equal, and any of them over a group with `±inf` or NaN. Engines give NULL or NaN there.

Reproduction:

- `corr(x, y)` over `(1, 2)` alone, or over `(1, 1), (1, 2)`.
- DuckDB 2.0 and Polars 2.1: NaN for both; Spark 4.3: NULL for both. DuckDB: `var_samp` over `[inf, 1]` is NaN.

How sverify handles it:

- The core allows NULL, NaN or a raise (`stat_degenerate`); the reference gives NULL for `corr`, as the SQL standard does, and raises for an infinite value. `semantics="duckdb"` gives NaN.
- Could be expressed as: An option, such as `on_degenerate: [NULL, NAN]` and the existing `on_domain_error` for non-finite input, or a sentence in each description.

Status: Still open on main (a4d8e00342d0): [`functions_arithmetic.yaml` L1492-L1516](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L1492-L1516) says only that `corr` of no input is null, and [`functions_arithmetic.yaml` L1394-L1491](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L1394-L1491) (`std_dev`, `variance`) say nothing beyond their names; no option or sentence covers one pair, a constant side, or `±inf`/NaN input. No existing issue.

See: facts [duckdb-corr](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-corr), [spark-corr](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/other-facts.md#spark-corr), [polars-corr](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-corr), [duckdb-nonfinite-aggregates](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-nonfinite-aggregates), [duckdb-var-stddev](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-var-stddev), [polars-nonfinite-aggregates](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-nonfinite-aggregates); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml corr, std_dev, variance on main; the gap is there


## ST-4: `fp32` and `fp64` have IEEE 754's range and precision (`type_classes.md`), and `equal` is `x == y`, but …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`fp32` and `fp64` have IEEE 754's range and precision (`type_classes.md`), and `equal` is `x == y`, but nothing says how NaN and `-0.0` compare, group, sort or deduplicate. `index_in` alone has an option for it (`nan_equality`). Sorting follows the type's "quality function", which is not defined for NaN or `-0.0`.

Reproduction:

- `GROUP BY x`, `DISTINCT`, a join on `x`, `ORDER BY x` and `equal(x, x)` with `x` in `{NaN, -0.0, 0.0}`.
- DuckDB 2.0: one NaN, equal to itself and above `+inf`; `-0.0` sorts before `0.0`; `signbit` sees a NaN's sign.

How sverify handles it:

- The core leaves `nan_equality`, `nan_order`, `zero_sign` and `nan_kind` open; the reference has one NaN, equal to itself and greatest, and one zero (#89).
- Could be expressed as: Extend `nan_equality` to `equal`, the comparisons and the relations that compare keys, and add an option or a stated rule for NaN's place in a sort and for `-0.0`.

Status: Still open on main (a4d8e00342d0): [`type_classes.md` L20-L21](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/types/type_classes.md#L20-L21) gives `fp32`/`fp64` IEEE 754's range and precision, [`functions_comparison.yaml` L23-L27](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_comparison.yaml#L23-L27) defines `equal` as `x == y`, only `index_in` has `nan_equality` ([`functions_set.yaml` L8-L28](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_set.yaml#L8-L28)), and the sort's "quality function" ([`basics.md` L64-L71](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/relations/basics.md#L64-L71)) is defined nowhere. No existing issue; the open draft [\#1322](https://github.com/substrait-io/substrait/pull/1322) leaves NaN in RANGE frames implementation-defined.

See: facts [duckdb-R14](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R14), [duckdb-signbit](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-signbit), [duckdb-arg-min-nulls](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-arg-min-nulls), [duckdb-quantile-disc](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-quantile-disc), [polars-zero-sign](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-zero-sign), [polars-nan-sign](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-nan-sign), [polars-nan-equality](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-nan-equality), [polars-nan-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-nan-order), [polars-min-max-nan](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-min-max-nan), [polars-zero-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-zero-order), [duckdb-nan-equality](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-nan-equality); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/pull/1322>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: type_classes.md, functions_comparison.yaml, functions_set.yaml, relations/basics.md on main; the gap is there


## ST-5: `add`, `subtract` and `multiply` on `fp32`/`fp64` have only `rounding`


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`add`, `subtract` and `multiply` on `fp32`/`fp64` have only `rounding`. `inf - inf`, `inf + (-inf)` and `0 * inf` have no IEEE value, and the YAML neither says they give NaN nor offers `on_domain_error`, as `divide` and `sqrt` do.

Reproduction:

- `subtract(inf::fp64, inf::fp64)`, `multiply(0.0::fp64, inf::fp64)`.
- DuckDB 2.0: NaN under every setting.

How sverify handles it:

- The core allows NaN or a raise (`nan_creation`); the reference raises (#257), and DuckDB's written plan guards these cases.
- Could be expressed as: `on_domain_error: [NAN, NULL, ERROR]` on the floating-point `add`, `subtract`, `multiply` and `sum`, as `divide` has.

Status: Still open on main (a4d8e00342d0): the fp impls of `add`, `subtract` and `multiply` ([`functions_arithmetic.yaml` L45-L62](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L45-L62), [`functions_arithmetic.yaml` L103-L120](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L103-L120), [`functions_arithmetic.yaml` L161-L178](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L161-L178)) take `rounding` only, while `divide` ([`functions_arithmetic.yaml` L180-L187](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L180-L187)) has `on_domain_error`; nothing says `inf - inf` or `0 * inf` gives NaN. Closest issue [\#1275](https://github.com/substrait-io/substrait/issues/1275) (IEEE divide); see also [\#996](https://github.com/substrait-io/substrait/issues/996) (options inconsistent across functions).

See: facts [duckdb-R15-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R15-double-arith), [duckdb-nonfinite-aggregates](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-nonfinite-aggregates), [polars-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-double-arith), [polars-nonfinite-aggregates](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-nonfinite-aggregates); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/issues/1275>, <https://github.com/substrait-io/substrait/issues/996>, <https://github.com/substrait-io/substrait/issues/254>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml fp add/subtract/multiply/divide and their test cases on main; the gap is there


## ST-6: The cast expression (`specialized_record_expressions.md`, `Cast` in `algebra.proto`) does not say how a …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


The cast expression (`specialized_record_expressions.md`, `Cast` in `algebra.proto`) does not say how a cast from `fp32`/`fp64` or a decimal to an integer rounds, and `FAILURE_BEHAVIOR_UNSPECIFIED` is not described.

Reproduction:

- `CAST(0.55::fp64 AS i32)` and `CAST(-0.55::fp64 AS i64)`: `0`, or `1` and `-1`?
- DuckDB 2.0: rounds half away from zero (`1`, `-1`); DataFusion truncates (`0`, `0`).

How sverify handles it:

- The core leaves [float_to_int](../reference/sql.Dialect.md#sverify.sql.Dialect.float_to_int) open and reads an unspecified failure behaviour as either; the reference truncates toward zero (#209) and throws. DuckDB's written plan casts `trunc(x)`.
- Could be expressed as: A rounding field on the cast (the `rounding` option's values), and a sentence on what `FAILURE_BEHAVIOR_UNSPECIFIED` means.

Status: Still open on main (a4d8e00342d0): [`specialized_record_expressions.md` L14-L17](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/expressions/specialized_record_expressions.md#L14-L17) describes the cast's failure behaviour and nothing on how fp or decimal to integer rounds; [`algebra.proto` L1502-L1512](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/proto/substrait/algebra.proto#L1502-L1512) leaves `FAILURE_BEHAVIOR_UNSPECIFIED` undescribed. No existing issue on rounding; [\#1069](https://github.com/substrait-io/substrait/issues/1069) (semantically meaningful `*_UNSPECIFIED`) does not list the cast.

See: facts [duckdb-R9](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R9), [duckdb-R8](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R8), [polars-cast-double-to-int](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-cast-double-to-int); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/issues/1069>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: specialized_record_expressions.md and algebra.proto Cast on main; the gap is there


## ST-7: A sort field's direction is required (`relations/basics.md`), and the directions it lists are the four of …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


A sort field's direction is required (`relations/basics.md`), and the directions it lists are the four of NULL placement, a custom function and clustered. `SORT_DIRECTION_UNSPECIFIED`, the enum's default value, is not described: an error, or a direction the consumer picks?

Reproduction:

- A `SortRel` whose field has `direction: SORT_DIRECTION_UNSPECIFIED` over a column with NULLs.

How sverify handles it:

- The core reads it as ascending with the NULL placement left open (docs/core-semantics.md, D6); the reference and each engine fix one (the reference and DuckDB: NULLs last, D8). The parser reads it in a `SortRel` (SubstraitLean/Parse.lean, `parseSortKey`; \#444 step 1c) and refuses it in a window's or a measure's order.
- Could be expressed as: Say whether `SORT_DIRECTION_UNSPECIFIED` is invalid or means a consumer-chosen direction and NULL placement.

Status: Still open on main (a4d8e00342d0): [`basics.md` L58-L73](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/relations/basics.md#L58-L73) requires a direction and lists none for `SORT_DIRECTION_UNSPECIFIED` ([`algebra.proto` L1842-L1857](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/proto/substrait/algebra.proto#L1842-L1857)). Existing issue: [\#213](https://github.com/substrait-io/substrait/issues/213) asks exactly this (question 5, 2022; comments lean to "reject the plan"), unresolved; [\#1069](https://github.com/substrait-io/substrait/issues/1069) covers `*_UNSPECIFIED` defaults but does not list `SortDirection`.

See: facts [duckdb-F2](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-F2), [polars-null-order](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-null-order); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/issues/213>, <https://github.com/substrait-io/substrait/issues/1069>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md), [`SubstraitLean/Parse.lean`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/SubstraitLean/Parse.lean).

Found by the design pass of the loose core (#444), docs/core-semantics.md.

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: the extension YAMLs and site/docs on main; the gap is there
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: relations/basics.md orderedness and algebra.proto SortField on main; the gap is there


## ST-8: `functions_arithmetic_decimal.yaml` gives each function's result type, and nothing about how a result with …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`functions_arithmetic_decimal.yaml` gives each function's result type, and nothing about how a result with more digits than the result's scale is rounded: always for `divide`, and for `add`, `subtract`, `multiply` when the precision passes 38 and the scale is borrowed. Casts between decimal scales (`specialized_record_expressions.md`) leave it open too. Engines round half to even (Polars) or half away from zero (DuckDB).

Reproduction:

- `multiply(DECIMAL<10,2> 0.05, DECIMAL<10,1> 0.5)` at a result scale of 2 (an engine's own result type, or a cast to `DECIMAL<10,2>`): Polars 2.1.0 gives 0.02, half away from zero gives 0.03. `divide(DECIMAL<10,2> 1.00, DECIMAL<10,0> 8)` at scale 2: 0.12 or 0.13.

How sverify handles it:

- The core's `decimal_rescale` option allows `TIE_AWAY_FROM_ZERO`, `TIE_TO_EVEN` and `TRUNCATE` (docs/core-semantics.md); the reference rounds half away from zero. Decimal division is refused in every profile until \#27.
- Could be expressed as: a `rounding` option on the decimal functions and casts, with the values of `round`'s.

Status: Still open on main (a4d8e00342d0): [`functions_arithmetic_decimal.yaml` L49-L87](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic_decimal.yaml#L49-L87) (and `add`/`subtract` L8-L47) give result types and `overflow` only, with no rounding. Existing issue: [\#1224](https://github.com/substrait-io/substrait/issues/1224) asks exactly this for the precision-38 borrow; divide's always-inexact result and casts between scales are not in it. Related: [\#1318](https://github.com/substrait-io/substrait/issues/1318) (decimal handling, vbarua), [\#1223](https://github.com/substrait-io/substrait/pull/1223), [\#1274](https://github.com/substrait-io/substrait/pull/1274).

See: facts [polars-decimal-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-decimal-arith), [duckdb-decimal-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-decimal-arith); issues [\#27](https://github.com/AlexanderNenninger/substrait-lean/issues/27), [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/issues/1224>, <https://github.com/substrait-io/substrait/issues/1318>, <https://github.com/substrait-io/substrait/pull/1223>, <https://github.com/substrait-io/substrait/pull/1274>, <https://github.com/substrait-io/substrait/pull/1213>, <https://github.com/substrait-io/substrait/issues/1216>; files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md), [`characterization/polars/probes.json`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/polars/probes.json).

Found by the Polars characterization (sverify_dev.probe_polars, characterization/polars/probes.json).

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: functions_arithmetic_decimal.yaml on main: result types only, no rounding and no options
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic_decimal.yaml and the cast docs on main; the gap is there


## ST-9: The `fp32` and `fp64` implementations of `add`, `subtract`, `multiply`, `divide`, `power`, `exp` and the …


Project: Substrait 0.106.0; status: confirmed; kind: spec-gap.


The `fp32` and `fp64` implementations of `add`, `subtract`, `multiply`, `divide`, `power`, `exp` and the other elementary functions have no option for a result too large for the type: only `rounding` (and `on_domain_error`, `on_division_by_zero` where they apply). The test cases expect IEEE 754's `±inf` with the default options (`multiply.test`, since substrait#738), but nothing lets a plan ask for an error instead. `sum` and `avg` of `fp64` take `overflow: SILENT | SATURATE | ERROR`, which the YAML defines for integers only.

Reproduction:

- `multiply(fp64 1e308, fp64 10)`, `exp(fp64 1000)`, `power(fp64 10, fp64 400)`, and `sum` of `1e308` and `1e308`.
- DuckDB 2.0 gives `inf` for all of them (fact duckdb-double-overflow); Polars gives `inf` (fact polars-double-arith); sverify's reference raises (#575).

How sverify handles it:

- The reference raises when an operation on finite doubles gives `±inf` (`Issue.infinite`): an inferred precondition the written plan checks on the data, as for a `SUM` that leaves 64 bits. The core allows both behaviours.
- Could be expressed as: an `overflow` option on the floating-point implementations, with `IEEE` (`±inf`) and `ERROR`, and the meaning of `sum`'s existing `overflow` values stated for `fp32` and `fp64` (`SATURATE` to the largest finite value).

Status: Narrower than recorded, still open on main (a4d8e00342d0): the test cases expect IEEE `±inf` on overflow with the default options (`multiply.test` L19-L21, likewise `add`, `subtract`, `divide`, `sum`, `exp`, since [\#738](https://github.com/substrait-io/substrait/pull/738)), but no fp implementation offers raising instead ([`functions_arithmetic.yaml` L45-L62](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L45-L62), [`functions_arithmetic.yaml` L401-L412](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L401-L412), [`functions_arithmetic.yaml` L445-L468](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L445-L468)), and `sum`'s `overflow` values ([`functions_arithmetic.yaml` L1092-L1111](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L1092-L1111)) are undefined for floats. No existing issue; [\#254](https://github.com/substrait-io/substrait/issues/254) (options undocumented).

See: facts [duckdb-double-overflow](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-double-overflow), [polars-double-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-double-arith); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444), [\#575](https://github.com/AlexanderNenninger/substrait-lean/issues/575); upstream <https://github.com/substrait-io/substrait/issues/254>, <https://github.com/substrait-io/substrait/issues/996>; files [`SubstraitLean/Safety.lean`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/SubstraitLean/Safety.lean), [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md), [`docs/reference-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/reference-semantics.md).

Found by the terminology of the loose core (#574), docs/core-semantics.md.

- Checked 2026-11-04 against substrait-extensions 0.106.0: functions_arithmetic.yaml: the fp implementations of add, subtract, multiply, divide, power and exp have `rounding` only; sum and avg of fp64 have `overflow`
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml fp impls and tests/cases/arithmetic/{add,subtract,multiply,divide,sum,exp}.test on main; the tests answer the default (±inf), the ERROR option and sum's overflow on floats are open


## ST-10: `upper` and `lower` with `char_set: UTF8` say the implementation "should follow the utf8_unicode_ci …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`upper` and `lower` with `char_set: UTF8` say the implementation "should follow the utf8_unicode_ci collations" of the Unicode Collation Algorithm (UTR \#10), which is a collation, not a case mapping. Nothing says whether the mapping is Unicode's simple one (one code point to one, the length kept) or the full one of SpecialCasing.txt (`ß` to `SS`, `fi` to `FI`, `İ` to `i̇`, a final sigma). Engines differ: DuckDB maps code point by code point, Rust's `str::to_uppercase` (Polars, DataFusion) maps in full. The `varchar<L1>` and `fixedchar<L1>` signatures return the input's length, which a full mapping can exceed.

Reproduction:

- `upper('ß')`: DuckDB 2.0.0 gives `ẞ` (U+1E9E), Polars 2.1.0 gives `SS`. `lower('ΣΑΣ')`: DuckDB `σασ`, Polars `σας`. `upper('fi')`: DuckDB `fi`, Polars `FI`. `lower('İ')`: DuckDB `i` (one character), Polars `i̇` (two).

How sverify handles it:

- The reference defines `upper` and `lower` as black boxes with Rust's full mappings (`Text.upper`, `Text.lower`), and the written SQL raises on non-ASCII text for every engine (`ascii_only`, \#70), where every engine agrees.
- Could be expressed as: a `case_mapping` option (`SIMPLE`, `FULL`) beside `char_set`, or `UTF8` defined as one of the two, with the length rule for the `varchar<L1>` and `fixedchar<L1>` signatures.

Status: Still open on main (a4d8e00342d0): [`functions_string.yaml` L985-L1037](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_string.yaml#L985-L1037) point `lower`/`upper` at the utf8_unicode_ci collation and return `varchar<L1>` for `varchar<L1>`, with nothing on simple or full case mapping; the test cases are ASCII only. No existing issue.

See: facts [duckdb-case-mapping](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-case-mapping), [polars-case](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-case); issues [\#70](https://github.com/AlexanderNenninger/substrait-lean/issues/70), [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); files [`python/src/sverify/sql/core/strings.py`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/python/src/sverify/sql/core/strings.py), [`characterization/duckdb/probes.json`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/duckdb/probes.json).

Found by the DuckDB characterization (sverify_dev.probe observations, characterization/duckdb/probes.json).

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: functions_string.yaml on main: upper, lower with char_set \[UTF8, ASCII_ONLY\] and the utf8_unicode_ci sentence, nothing on simple or full mappings
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_string.yaml lower/upper and their test cases on main; the gap is there


## ST-11: `power` of `i64` (`functions_arithmetic.yaml`) returns `i64` and takes only `overflow`


Project: Substrait 0.106.0; status: confirmed; kind: spec-gap.


`power` of `i64` (`functions_arithmetic.yaml`) returns `i64` and takes only `overflow`. Nothing says what a negative exponent gives, whose result is not an integer: `power(2, -1)` could be `0` (truncated), an error, or a domain error, and the integer implementation has no `on_domain_error`.

Reproduction:

- `power(2::i64, -1::i64)` and `power(-2::i64, -3::i64)`: the YAML's description, "Take the power with x as the base and y as exponent", defines neither.
- Polars 2.1: a negative integer exponent raises (`InvalidOperationError`, fact polars-int-arith); sverify's reference raises (`Issue.negExponent`).

How sverify handles it:

- The reference raises on a negative exponent (`Issue.negExponent`, `SubstraitLean/Safety.lean`), an inferred precondition. The core allows raising anywhere (D2), so no option of the catalogue names it; `Profile.substrait` accepts any `on_domain_error` preference for integer `power`, which the YAML does not give it.
- Could be expressed as: `on_domain_error: [NULL, ERROR]` on the integer implementations of `power`, as integer `divide` has, with a negative exponent as its domain error, or a sentence in the description.

Status: Still open on main (a4d8e00342d0): [`functions_arithmetic.yaml` L389-L412](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_arithmetic.yaml#L389-L412) gives `power(i64, i64) -> i64` with `overflow` only and nothing on a negative exponent; `power.test` has positive integer exponents only. No existing issue; [\#1001](https://github.com/substrait-io/substrait/pull/1001) (closed) proposed `fp64` results and was declined to keep `int, int -> int`.

See: facts [polars-int-arith](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-int-arith); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444); upstream <https://github.com/substrait-io/substrait/pull/1001>; files [`SubstraitLean/SubstraitProfile.lean`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/SubstraitLean/SubstraitProfile.lean), [`SubstraitLean/Safety.lean`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/SubstraitLean/Safety.lean).

Found by writing Profile.substrait (#444 step 2), SubstraitLean/SubstraitProfile.lean.

- Checked 2026-11-04 against substrait-extensions 0.106.0: functions_arithmetic.yaml: power(i64, i64) has `overflow` only; the fp implementations have no options
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: functions_arithmetic.yaml power and tests/cases/arithmetic/power.test on main; the gap is there


## ST-12: `IfThen` and `Switch` short-circuit and `coalesce` stops at the first non-null argument, so the spec makes …


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: confirmed; kind: spec-gap.


`IfThen` and `Switch` short-circuit and `coalesce` stops at the first non-null argument, so the spec makes those lazy. It does not say whether `and` and `or` evaluate an operand that does not decide the result (it gives Kleene truth tables only), or whether a filter or join condition may be evaluated on rows that a relation below it removes. Both decide whether a function that raises (an integer division by zero, a failing cast, an overflow) raises for a plan. DuckDB's `AND`/`OR` are lazy as conditions and eager as values; Polars's `&` and `|` evaluate every operand (#604). Polars's eager `when/then/otherwise` (under `group_by().agg` and `over()`) and `coalesce` depart from the spec's lazy `IfThen` and `coalesce`.

Reproduction:

- `and(x <> 0, 10 / x > 1)` over `x = 0` with `on_division_by_zero: ERROR`, as a projected value: DuckDB 2.0.0's `SELECT (x <> 0) AND (10 // x > 1)` raises at `x = 0`, and Polars 2.1.0's `(pl.col('x') != 0) & (10 // pl.col('x') > 1)` with a strict cast in place of the division raises too; a reference that evaluates `and` lazily returns `false` (#604).

How sverify handles it:

- sverify's guards look for raises on the rows of `Rel.loose`, the plan without the filters an engine may reorder (`Rel.HasIssue`, `SubstraitLean/Guards.lean`), so a filter pushed below a join is covered; whether a raise inside an `IfThen` branch counts on rows its condition excludes is for the round-2 source check. The `execution` area's `evaluation_order` item records what each engine does (duckdb-exec-short-circuit, duckdb-exec-filter-pushdown, polars-exec-when-eager, polars-exec-predicate-pushdown).
- Could be expressed as: a statement in the expression semantics that a function's raise counts only on rows where its value is needed (lazy `IfThen`, `coalesce`, `and`, `or`), and that a filter is evaluated only on the rows of its input; or an option on those functions (`evaluation: LAZY | EAGER`) for producers to ask for.

Status: Partly specified on main (a4d8e00342d0): `IfThen` and `Switch` short-circuit, so a branch not taken cannot raise ([`specialized_record_expressions.md` L30-L53](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/expressions/specialized_record_expressions.md#L30-L53)), and `coalesce` does not evaluate the arguments after the first non-null ([`functions_comparison.yaml` L262-L267](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_comparison.yaml#L262-L267)). Still open: `and`/`or` give Kleene truth tables only ([`functions_boolean.yaml` L8-L66](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/extensions/functions_boolean.yaml#L8-L66)), and nothing says whether a filter or join condition may be evaluated on rows a relation below removes ([`logical_relations.md` L124-L142](https://github.com/substrait-io/substrait/blob/a4d8e00342d0/site/docs/relations/logical_relations.md#L124-L142)). No existing issue.

See: facts [duckdb-exec-short-circuit](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-exec-short-circuit), [duckdb-exec-filter-pushdown](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-exec-filter-pushdown), [polars-exec-when-eager](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-exec-when-eager), [polars-exec-predicate-pushdown](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-exec-predicate-pushdown); issues [\#444](https://github.com/AlexanderNenninger/substrait-lean/issues/444), [\#604](https://github.com/AlexanderNenninger/substrait-lean/issues/604); files [`characterization/areas.json`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/areas.json), [`SubstraitLean/Guards.lean`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/SubstraitLean/Guards.lean).

Found by the characterization pipeline, round 1 (execution area).

- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions 0.106.0: Not checked against the spec text yet; to confirm in round 2 (expressions/conditionals, functions_boolean.yaml).
- Checked 2026-11-04 against substrait main@a4d8e00342d0, substrait-extensions v0.108.0: specialized_record_expressions.md (IfThen, Switch), functions_comparison.yaml (coalesce), functions_boolean.yaml, relations/logical_relations.md (Filter, Join) on main; IfThen/Switch/coalesce are specified lazy, and/or and relation evaluation order are open


## ST-16: `on_log_zero` lists `NAN`, `ERROR` and `MINUS_INFINITY`


Project: Substrait 0.106.0 to main@a4d8e00342d0; status: unverified; kind: spec-gap.


`on_log_zero` lists `NAN`, `ERROR` and `MINUS_INFINITY`. Spark (and Hive before it) returns NULL for the logarithm of zero, as it does for a negative argument, which `on_domain_error: NULL` covers. Substrait cannot express Spark's `ln(0)`.

Reproduction:

- `ln(0.0::fp64)` on Spark 4.3.0: NULL, under ANSI and without it (probe double-math-domain).
- DuckDB 2.0 and Polars 2.1.0: `-inf` (duckdb-R15-math-domain, polars-math-domain).

How sverify handles it:

- The reference raises (`on_log_zero: ERROR`); the Spark profile guards `x = 0` before the log, so a plan never sees Spark's NULL.
- Could be expressed as: add `NULL` to `on_log_zero`'s values, as `on_domain_error` has it.

Status: Open on main (a4d8e00342d0): `functions_logarithmic.yaml` gives `ln`, `log10`, `log2`, `logb` and `log1p` `on_log_zero: [NAN, ERROR, MINUS_INFINITY]`, while their `on_domain_error` lists `NULL`. No existing issue found (`gh issue list --repo substrait-io/substrait --search "on_log_zero null"`, "log of zero null": none); not yet checked against Substrait's issues in depth.

See: facts [spark-math-domain](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/other-facts.md#spark-math-domain), [polars-math-domain](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/polars-facts.md#polars-math-domain), [duckdb-R15-math-domain](https://github.com/AlexanderNenninger/substrait-lean/blob/main/upstream/bugs/duckdb-facts.md#duckdb-R15-math-domain); issues [\#738](https://github.com/AlexanderNenninger/substrait-lean/issues/738), [\#215](https://github.com/AlexanderNenninger/substrait-lean/issues/215); files [`docs/core-semantics.md`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/docs/core-semantics.md), [`characterization/spark/probes.json`](https://github.com/AlexanderNenninger/substrait-lean/blob/main/characterization/spark/probes.json).

Found by the Spark characterization (#738): sverify_dev.probe_spark, probe double-math-domain.

- Checked 2026-11-05 against substrait main@a4d8e00342d0: extensions/functions_logarithmic.yaml on main: on_log_zero values \[NAN, ERROR, MINUS_INFINITY\] for every logarithm