minguyen9988 · Sep 20, 2026 · Sep 20, 2026 · Sep 20, 2026 · Sep 20, 2026 · Sep 20, 2026
diff --git a/doc/architecture_and_flow_specification.md b/doc/architecture_and_flow_specification.md
@@ -323,7 +323,7 @@ In `PreparedStatementExecutor.insertBatch()` and `PreparedStatementFieldMapper.i
    - If an UPDATE modifies a column that is part of the ClickHouse `ORDER BY` sorting key:
      - `updateRelocatesSortingKey()` detects the mismatch between `beforeStruct` and `afterStruct`.
      - An explicit tombstone row is inserted for the *old* sorting key:
-       `insertTombstonePreparedStatement()` binds the before-image values with `is_deleted = 1` and `_version = record.getVersion() - 1`.
+       `insertTombstonePreparedStatement()` binds the before-image values with `is_deleted = 1` and `_version = record.getVersion()` (the same version as the after-image; a same-transaction relocation shares its version with the row it retires, and ClickHouse's equal-version tie resolves to the later-inserted row, i.e. the tombstone).
      - The live after-image row is then inserted for the *new* sorting key with `is_deleted = 0` and `_version = record.getVersion()`.
 2. **Type Conversion (`ClickHouseDataTypeMapper.convert`)**:
    - Binds values to `PreparedStatement` parameter positions:
@@ -497,7 +497,7 @@ The following catalog specifies the behavioral contract, synchronization boundar
 - **Purpose**: Binds an explicit `ReplacingMergeTree` delete tombstone row for an UPDATE that changes the row sorting key.
 - **Inputs**: Column index map, statement `ps`, before-image fields, record, before struct, config, column types, engine, table name.
 - **Outputs**: None.
-- **Mutations**: Calls `insertPreparedStatement` with `beforeSection = true`. Overrides delete column to `1` (or `-1`) and overrides version column to `record.getVersion() - 1`.
+- **Mutations**: Calls `insertPreparedStatement` with `beforeSection = true`. Overrides delete column to `1` (or `-1`) and binds the version column to `record.getVersion()` unchanged.
 
 ---
 

diff --git a/doc/configuration.md b/doc/configuration.md
@@ -78,4 +78,4 @@
 | connection.pool.min.idle                                  | **Optional**, Minimum number of idle connections in the pool.                                                                                                                                                                                                                                                                                                                                                                                                                
 | connection.pool.max.lifetime                              | **Optional**, Maximum lifetime of a connection in the pool.                                                                                                                                                                                                                                                                                                                                                                                                                
 | use.nongraceful.disconnect                                | **Optional**, Default: false. Required for fixing bug with freeze in debezium loop. Set to true for non-graceful disconnects.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
-| non.default.value                                         | **Optional**, Default: false. If set to true, a non-default value will be set. For example, if NULL is passed from source, the value will be NULL.                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                                |
+| non.default.value                                         | **Deprecated, no effect.** The connector always binds the source value, including NULL, and never substitutes the column DEFAULT. The key is accepted for backward compatibility; setting it to `false` logs a deprecation warning once.                                                                                                                                                                                                                                                            
8
        
10BC8
                                                                                                                                                                                                                                                                            |
diff --git a/formal_specs/lean/README.md b/formal_specs/lean/README.md
@@ -80,7 +80,16 @@ The replication engine maps each binlog event into ClickHouse insertions:
   - If $k_{\text{old}} = k_{\text{new}}$:
     $[ \{ k_{\text{new}}, v, \text{encode}(p), \text{false} \} ]$
   - If $k_{\text{old}} \ne k_{\text{new}}$:
-    $[ \{ k_{\text{old}}, \emptyset, \text{encode}(p) - 1, \text{true} \}, \{ k_{\text{new}}, v, \text{encode}(p), \text{false} \} ]$
+    $[ \{ k_{\text{old}}, \emptyset, \text{encode}(p), \text{true} \}, \{ k_{\text{new}}, v, \text{encode}(p), \text{false} \} ]$
+
+    The tombstone and the live row carry the **same** version (the connector
+    binds `record.getVersion()` for both). They never share a key, so they
+    never compete; against an older live row at $k_{\text{old}}$ the tombstone
+    wins by version, or — when that row was written by the same transaction
+    and has the same version — by the `FINAL` tie rule below.
+- `FINAL` tie rule: `maxStep` uses `>=`, so of two records with one key and
+  equal version the one appended **later** wins (ClickHouse keeps the last
+  inserted row). Proved as `tombstone_wins_version_tie`.
 - $\text{translate}(\text{Delete}(k), p) = [ \{ k, \emptyset, \text{encode}(p), \text{true} \} ]$
 
 ---
@@ -97,10 +106,12 @@ on Lean's standard axioms `[propext, Quot.sound]` (verified via `#print axioms`)
 | `delete_convergence_single` | $\text{view}_{\text{CH}}(\text{replicate}([e_{\text{insert}}, e_{\text{delete}}])) = \text{None}$ | Tombstones erase rows in `FINAL`. |
 | `update_same_key_convergence` | $\text{view}_{\text{CH}}(\text{replicate}([e_{\text{ins}}, e_{\text{upd}}])) = \text{Some}(v_{\text{new}})$ | In-place updates supersede earlier inserts. |
 | `update_pk_relocation_soundness` | $\text{view}_{\text{CH}}(k_{\text{old}}) = \text{None} \land \text{view}_{\text{CH}}(k_{\text{new}}) = \text{Some}(v)$ | The two-phase tombstone protocol eliminates ghost rows on PK mutation. |
+| `tombstone_wins_version_tie` | live row $(k, V)$ then tombstone $(k, V)$ appended later $\implies \text{view}_{\text{CH}}(k) = \text{None}$ | Equal versions resolve to the later insert, so a same-transaction relocation (same `_version`) still retires the old key. |
 | `master_replication_convergence` | $\forall S, \forall k, \text{view}_{\text{CH}}(\text{replicate}(S), k) = \text{eval}_{\text{MySQL}}(S, k)$ | **Master Convergence Theorem**: inductive proof (via `replicate_converges_gen`) that ANY transaction stream — inserts, updates, relocations, deletes and truncates — achieves exact replica parity. |
 
 > Versioning note: the engine assigns versions by strictly increasing **stream
-> ordinal** (`liveVersion i = 2*i`, tombstone `2*i - 1`), so
+> ordinal** (`liveVersion i = 2*i`; the relocation tombstone carries the same
+> version, `tombstoneVersion i = liveVersion i`), so
 > `master_replication_convergence` needs no monotonic-position hypothesis. The
 > `encode` map above is a separate, documented order-witness proved monotonic only
 > within `BinlogPos.WellFormed`; it is not used by the engine.

diff --git a/formal_specs/lean/Replication/Engine.lean b/formal_specs/lean/Replication/Engine.lean
@@ -35,17 +35,29 @@ def BinlogPos.WellFormed (p : BinlogPos) : Prop :=
 
 /--
 The version assigned to the live record produced at 1-based stream ordinal `i`.
-Using `2 * i` leaves the odd slot `2 * i - 1` for the tombstone half of a
-primary-key relocation, so the tombstone strictly exceeds every version issued
-before ordinal `i` (which are all `≤ 2 * (i - 1)`) yet stays below its paired
-live row. This is the abstract form of the connector's guarantee that each
-committed event receives a strictly greater `_version` than every event before
-it.
+`2 * i` strictly exceeds every version issued before ordinal `i` (all
+`≤ 2 * (i - 1)`), which is the abstract form of the connector's guarantee that
+each committed event receives a strictly greater `_version` than every event
+before it. (The factor 2 is historical headroom; nothing now occupies the odd
+slots -- see `tombstoneVersion`.)
 -/
 def liveVersion (i : Nat) : Nat := 2 * i
 
-/-- The tombstone version paired with `liveVersion i` for a relocation at ordinal `i`. -/
-def tombstoneVersion (i : Nat) : Nat := 2 * i - 1
+/--
+The version of the tombstone half of a primary-key relocation at ordinal `i`:
+the SAME version as its paired live row, exactly as the connector binds
+`record.getVersion()` for both rows (Spec 05.02).
+
+The tombstone and the live row never share a key, so they never compete; what
+the tombstone must beat is the live row previously stored at the OLD key. In the
+model that row is strictly older (ordinal versioning), and in the connector it
+may carry the very same version (a relocation in the same transaction as the
+INSERT, under GTID versioning). The equal case is decided by the `FINAL` tie
+rule -- `maxStep` keeps the LATER record on `>=` -- which the tombstone wins by
+being written after the row it retires; see `tombstone_wins_version_tie`.
+A tombstone at `liveVersion i - 1` would lose that tie and leave a ghost row.
+-/
+def tombstoneVersion (i : Nat) : Nat := liveVersion i
 
 /--
 Translates a single MySQL binary log event, at 1-based stream ordinal `i`, into
@@ -88,8 +100,8 @@ def replicateFrom (i : Nat) (acc : CHTable) : List BinlogEvent → CHTable
 
 /--
 Replication Engine State Machine: takes a stream of MySQL binary log events and
-computes the resulting ClickHouse physical table. Ordinals start at 1 so the
-first tombstone version (`2*1 - 1 = 1`) is positive.
+computes the resulting ClickHouse physical table. Ordinals start at 1 so every
+version (`2*i`) is positive, matching the connector's rejection of `_version <= 0`.
 -/
 def replicateStream (events : List BinlogEvent) : CHTable :=
   replicateFrom 1 emptyCH events