fix: SS-2 invariant — nulls always sort last, regardless of direction (#6343)

* fix: SS-2 invariant — nulls always sort last, regardless of direction

The SS-2 invariant incorrectly specified that nulls sort before non-null
for descending columns. The actual production code uses nulls_first=false
everywhere — nulls always sort after non-null values, regardless of
direction. This is required for sorted_series key correctness: null
columns are omitted from the key, and their keys naturally sort after
keys that include those columns.

Fixed in all locations:
- TLA+ SortSchema.tla: CompareValues and SS2_NullOrdering
- Rust invariants/sort.rs: compare_with_null_ordering
- Rust models/sort_schema.rs: SS-2 property check and compare_values test
- Rust invariants/registry.rs: SS-2 description
- ADR-002: SS-2 invariant table
- Phase 1 design doc: null handling descriptions

Stateright exhaustive_sort_schema BFS passes with corrected model.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

* test: verify model detects null ordering violations

Added two tests to the Stateright sort_schema model:

- ss2_detects_null_before_non_null_in_descending: constructs rows
  with null before non-null in a descending column, verifies both
  row_leq and is_sorted reject this ordering (nulls always last).

- ss2_accepts_non_null_before_null_in_descending: verifies the
  correct ordering (non-null then null) is accepted.

These confirm the model can catch the exact class of bug that the
SS-2 invariant fix addresses.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: g-talbot

docs/internals/adr/002-sort-schema-parquet-splits.md

@@ -119,7 +119,7 @@ These invariants must hold across all code paths (ingestion, compaction, query).
 | ID | Invariant | Rationale |
 |----|-----------|-----------|
 | **SS-1** | All rows within a split are sorted according to the sort schema recorded in that split's metadata | Foundation for page-level pruning and sorted merge. Violated data produces incorrect merge results |
-| **SS-2** | Nulls sort after non-null values for ascending columns and before non-null values for descending columns | Consistent null ordering across ingestion and merge. Matches Husky convention |
+| **SS-2** | Nulls always sort after non-null values, regardless of sort direction (nulls last) | Consistent null ordering across ingestion and merge. Enables nulls to be implicit in sorted_series key encoding |
 | **SS-3** | If a sort column is missing from a split, all rows in that split are treated as null for that column. This is not an error | Enables schema evolution — columns can be added to the sort schema without rewriting existing splits |
 | **SS-4** | The sort schema stored in a split's metadata is the schema that was in effect when that split was written. Already-written splits are never re-sorted | Changes propagate forward only. Old splits age out via retention |
 | **SS-5** | The sort schema string is the same in the metastore (per-split metadata), the Parquet `key_value_metadata`, and the Parquet `sorting_columns` field for a given split | Three representations of the same truth. Inconsistency between them would cause incorrect merge or pruning behavior |

docs/internals/locality-compaction/phase-1-sorted-splits.md

@@ -85,7 +85,7 @@ Each column in the schema has:
   - **String/binary:** Sorted lexicographically by byte value.  
   - **Integer types** (i8, i16, i32, i64, u8, u16, u32, u64): Sorted numerically.  
   - **Float types** (f32, f64): Sorted numerically, with NaN handling matching IEEE 754 total order (NaN sorts after all other values).  
-- **Null handling:** Null values sort **after** all non-null values for ascending columns, and **before** all non-null values for descending columns. This matches Husky's behavior and ensures nulls cluster at the end of each column's range.
+- **Null handling:** Null values always sort **after** all non-null values, regardless of sort direction (`nulls_first: false`). This enables nulls to be implicit in the sorted_series key encoding — absent columns are simply omitted from the key, and their keys naturally sort after keys that include those columns.
 
 ### Timeseries ID (Optional Locality Tiebreaker)
 
@@ -286,7 +286,7 @@ The Parquet reader always reads the file footer first \-- the footer contains th
 
 Input splits may not have identical column sets. Schema evolution (adding or removing columns over time) means that splits from different time periods may have different columns. The merge handles this as follows:
 
-- **Sort columns.** If a sort column is missing from an input split, all rows from that split are treated as having null values for that column. Nulls sort after non-null values (ascending) or before non-null values (descending), as specified in the sort schema. The k-way merge handles this naturally.  
+- **Sort columns.** If a sort column is missing from an input split, all rows from that split are treated as having null values for that column. Nulls always sort after non-null values (`nulls_first: false`), regardless of direction. The k-way merge handles this naturally.  
 
 - **Non-sort columns.** The merge computes the **union** of all column names across all input splits. The output split contains every column that appears in at least one input. When streaming a column through the merge, rows originating from inputs that lack that column are filled with nulls. The output Parquet schema uses the type from whichever input(s) contain the column; if multiple inputs have the same column name with different types, the merge fails with an error (this indicates a schema evolution conflict that must be resolved at the index configuration level).
 

docs/internals/specs/tla/SortSchema.tla

@@ -11,7 +11,7 @@
 \*
 \* Key Invariants (from ADR-002):
 \*   - SS-1: All rows within a split are sorted according to its recorded sort schema
-\*   - SS-2: Nulls sort after non-null for ascending, before non-null for descending
+\*   - SS-2: Nulls always sort after non-null values (nulls last, regardless of direction)
 \*   - SS-3: Missing sort columns in a split are treated as null (not an error)
 \*   - SS-4: A split's sort schema never changes after it is written
 \*   - SS-5: The three copies of sort schema (metastore, KV metadata, sorting_columns)
@@ -37,7 +37,7 @@
 \* | ChangeSchema action          | Metastore update_index() changing sort_schema                |
 \* | CompactSplits action         | Parquet merge executor (sorted k-way merge, ADR-003)         |
 \* | RowsSorted property          | debug_assert! after lexsort_to_indices in sort_batch()       |
-\* | NullOrdering property        | SortColumn nulls_first field per direction                   |
+\* | NullOrdering property        | SortColumn nulls_first=false (nulls always last)             |
 \* | Columns                      | ParquetField enum variants in schema/fields.rs               |
 
 EXTENDS Integers, Sequences, FiniteSets, TLC
@@ -132,16 +132,13 @@ GetValue(row, col, columns_present) ==
 \* Compare two values for a single column with null ordering rules (SS-2)
 \* Returns: -1 (less), 0 (equal), 1 (greater)
 \*
-\* For ascending: nulls sort AFTER non-null (nulls are "greater")
-\* For descending: nulls sort BEFORE non-null (nulls are "lesser")
+\* Nulls always sort AFTER non-null values, regardless of direction.
+\* This matches the writer's nulls_first=false and enables nulls to be
+\* implicit in the sorted_series key.
 CompareValues(v1, v2, direction) ==
     CASE v1 = NULL /\ v2 = NULL -> 0
-      [] v1 = NULL /\ v2 /= NULL ->
-            IF direction = "asc" THEN 1    \* null after non-null for ascending
-            ELSE -1                         \* null before non-null for descending
-      [] v1 /= NULL /\ v2 = NULL ->
-            IF direction = "asc" THEN -1   \* non-null before null for ascending
-            ELSE 1                          \* non-null after null for descending
+      [] v1 = NULL /\ v2 /= NULL -> 1     \* null always after non-null
+      [] v1 /= NULL /\ v2 = NULL -> -1    \* non-null always before null
       [] v1 /= NULL /\ v2 /= NULL ->
             IF direction = "asc"
             THEN (CASE v1 < v2 -> -1 [] v1 = v2 -> 0 [] v1 > v2 -> 1)
@@ -218,13 +215,12 @@ SS1_RowsSorted ==
     \A s \in splits :
         IsSorted(s.rows, s.sort_schema, s.columns_present)
 
-\* SS-2: Null values are ordered correctly per column direction
+\* SS-2: Null values always sort after non-null (nulls last, regardless of direction)
 \* This is enforced by the CompareValues function used in IsSorted.
 \* We verify it explicitly: for every adjacent pair of rows, when all
 \* earlier sort columns are equal, if one value is NULL and the other
-\* is not, the NULL must be in the correct position:
-\*   - Ascending:  NULL comes AFTER non-null (nulls last)
-\*   - Descending: NULL comes BEFORE non-null (nulls first)
+\* is not, the NULL must come after the non-null value.
+\* This matches the writer's nulls_first=false.
 SS2_NullOrdering ==
     \A s \in splits :
         \A i \in 1..(Len(s.rows) - 1) :
@@ -241,10 +237,8 @@ SS2_NullOrdering ==
                         IN ev1 = ev2
                 IN
                 earlier_equal =>
-                    \* Ascending: null must NOT appear before non-null
-                    /\ ~(dir = "asc" /\ v_curr = NULL /\ v_next /= NULL)
-                    \* Descending: non-null must NOT appear before null
-                    /\ ~(dir = "desc" /\ v_curr /= NULL /\ v_next = NULL)
+                    \* Null must NOT appear before non-null (regardless of direction)
+                    ~(v_curr = NULL /\ v_next /= NULL)
 
 \* SS-3: If a sort column is missing from a split's data, all rows in that
 \*       split are treated as null for that column. This is not an error.

quickwit/quickwit-dst/src/invariants/registry.rs

@@ -32,7 +32,7 @@ use std::fmt;
 pub enum InvariantId {
     /// SS-1: all rows within a split are sorted according to the split's schema
     SS1,
-    /// SS-2: null values sort correctly per direction (nulls last asc, first desc)
+    /// SS-2: null values always sort after non-null (nulls last, regardless of direction)
     SS2,
     /// SS-3: missing sort columns are treated as NULL
     SS3,
@@ -113,7 +113,7 @@ impl InvariantId {
     pub fn description(self) -> &'static str {
         match self {
             Self::SS1 => "rows sorted by split schema",
-            Self::SS2 => "null ordering correct per direction",
+            Self::SS2 => "nulls always sort after non-null",
             Self::SS3 => "missing sort columns treated as NULL",
             Self::SS4 => "sort schema immutable after write",
             Self::SS5 => "three copies of sort schema identical",

quickwit/quickwit-dst/src/invariants/sort.rs

@@ -21,8 +21,9 @@ use std::cmp::Ordering;
 
 /// Compare two optional values with null ordering per SS-2.
 ///
-/// - Ascending:  nulls sort AFTER non-null (nulls last).
-/// - Descending: nulls sort BEFORE non-null (nulls first).
+/// Nulls always sort AFTER non-null values, regardless of sort direction.
+/// This matches the writer's `nulls_first: false` and enables nulls to be
+/// implicit in the sorted_series key (absent columns are simply omitted).
 ///
 /// For two non-null values, the natural ordering is used (reversed for
 /// descending). Two nulls compare as equal.
@@ -33,20 +34,8 @@ pub fn compare_with_null_ordering<T: Ord>(
 ) -> Ordering {
     match (a, b) {
         (None, None) => Ordering::Equal,
-        (None, Some(_)) => {
-            if ascending {
-                Ordering::Greater // null after non-null
-            } else {
-                Ordering::Less // null before non-null
-            }
-        }
-        (Some(_), None) => {
-            if ascending {
-                Ordering::Less // non-null before null
-            } else {
-                Ordering::Greater // non-null after null
-            }
-        }
+        (None, Some(_)) => Ordering::Greater, // null always after non-null
+        (Some(_), None) => Ordering::Less,    // non-null always before null
         (Some(va), Some(vb)) => {
             if ascending {
                 va.cmp(vb)
@@ -86,14 +75,14 @@ mod tests {
 
     #[test]
     fn descending_null_ordering() {
-        // null < non-null in descending
+        // null always after non-null, even in descending
         assert_eq!(
             compare_with_null_ordering(None::<&i32>, Some(&1), false),
-            Ordering::Less
+            Ordering::Greater
         );
         assert_eq!(
             compare_with_null_ordering(Some(&1), None::<&i32>, false),
-            Ordering::Greater
+            Ordering::Less
         );
         // non-null comparison reversed
         assert_eq!(

quickwit/quickwit-dst/src/models/sort_schema.rs

@@ -145,8 +145,7 @@ impl SortSchemaModel {
 
 /// Compare two values with null ordering (SS-2).
 /// Returns `Ordering`: Less, Equal, Greater.
-/// Ascending: nulls sort AFTER non-null.
-/// Descending: nulls sort BEFORE non-null.
+/// Nulls always sort AFTER non-null, regardless of direction.
 ///
 /// Delegates to the shared [`crate::invariants::sort::compare_with_null_ordering`]
 /// for the null ordering logic, converting model-specific `Value` to `Option`.
@@ -502,9 +501,9 @@ impl Model for SortSchemaModel {
                 },
             ),
             // SS-2: Null values ordered correctly per direction.
-            // Ascending: null must NOT appear before non-null.
-            // Descending: non-null must NOT appear before null.
-            // Mirrors SortSchema.tla lines 228-247
+            // Nulls must never appear before non-null values, regardless of
+            // sort direction. This matches the writer's nulls_first=false.
+            // Mirrors SortSchema.tla SS-2.
             Property::always(
                 "SS-2: null ordering",
                 |_model: &SortSchemaModel, state: &SortSchemaState| {
@@ -522,18 +521,9 @@ impl Model for SortSchemaModel {
                                 });
 
                                 if earlier_equal {
-                                    // Ascending: null must not appear before non-null.
-                                    if sc.direction == Direction::Asc
-                                        && v_curr.is_null()
-                                        && !v_next.is_null()
-                                    {
-                                        return false;
-                                    }
-                                    // Descending: non-null must not appear before null.
-                                    if sc.direction == Direction::Desc
-                                        && !v_curr.is_null()
-                                        && v_next.is_null()
-                                    {
+                                    // Null must not appear before non-null,
+                                    // regardless of direction (nulls always last).
+                                    if v_curr.is_null() && !v_next.is_null() {
                                         return false;
                                     }
                                 }
@@ -615,14 +605,72 @@ mod tests {
             std::cmp::Ordering::Less
         );
 
-        // Descending: null < non-null
+        // Descending: null still after non-null (nulls always last)
         assert_eq!(
             compare_values(Value::Null, Value::Val(1), Direction::Desc),
-            std::cmp::Ordering::Less
+            std::cmp::Ordering::Greater
         );
         assert_eq!(
             compare_values(Value::Val(1), Value::Null, Direction::Desc),
-            std::cmp::Ordering::Greater
+            std::cmp::Ordering::Less
+        );
+    }
+
+    /// Verify that the model detects null ordering violations.
+    /// Construct rows where a null appears before a non-null value in a
+    /// descending column. With nulls-always-last, this is wrong — the
+    /// model's `is_sorted` and `row_leq` must reject it.
+    #[test]
+    fn ss2_detects_null_before_non_null_in_descending() {
+        let schema = vec![SortColumn {
+            column: Column::C1,
+            direction: Direction::Desc,
+        }];
+
+        // WRONG order: null before non-null
+        let bad_rows = vec![
+            Row {
+                cells: BTreeMap::new(), // C1 missing = null
+            },
+            Row {
+                cells: [(Column::C1, Value::Val(5))].into(),
+            },
+        ];
+
+        // row_leq(null, non-null) must be false (null sorts after non-null).
+        assert!(
+            !row_leq(&bad_rows[0], &bad_rows[1], &schema),
+            "null row must not be <= non-null row (nulls always last)"
+        );
+
+        // is_sorted must reject this ordering.
+        assert!(
+            !is_sorted(&bad_rows, &schema),
+            "rows with null before non-null must not be considered sorted"
+        );
+    }
+
+    /// Verify the model accepts correct null ordering: non-null before null.
+    #[test]
+    fn ss2_accepts_non_null_before_null_in_descending() {
+        let schema = vec![SortColumn {
+            column: Column::C1,
+            direction: Direction::Desc,
+        }];
+
+        // CORRECT order: value before null (nulls last)
+        let good_rows = vec![
+            Row {
+                cells: [(Column::C1, Value::Val(5))].into(),
+            },
+            Row {
+                cells: BTreeMap::new(), // null
+            },
+        ];
+
+        assert!(
+            is_sorted(&good_rows, &schema),
+            "non-null before null must be accepted (nulls always last)"
         );
     }