8000 spec(12): replication-history modes -- per-table SCD2 history and replication-log-only, specified from the 2.11.0 code with a Lean model (Domain 12, Replication.History) by minguyen9988 · Pull Request #1507 · Altinity/clickhouse-sink-connector · GitHub
[go: up one dir, main page]
Skip to content

spec(12): replication-history modes -- per-table SCD2 history and replication-log-only, specified from the 2.11.0 code with a Lean model (Domain 12, Replication.History) - #1507

Merged
minguyen9988 merged 1 commit into
Altinity:2.11.0from
minguyen9988:spec-replication-history-modes
Sep 26, 2026
Merged

spec(12): replication-history modes -- per-table SCD2 history and replication-log-only, specified from the 2.11.0 code with a Lean model (Domain 12, Replication.History)#1507
minguyen9988 merged 1 commit into
Altinity:2.11.0from
minguyen9988:spec-replication-history-modes

Conversation

@minguyen9988
@minguyen9988 minguyen9988 commented Sep 26, 2026
Copy link
Copy Markdown
Collaborator

Two of the three operating modes had no single specification. Per-table SCD2 history (replication.history.enable=true) was described in fragments across 04.04 s3.2, 02.01 s3.5, 08.05, 06.05, 06.09 and 05.02, and replication-log-only (replication.history.replication_log_only=true) had no spec coverage at all: it existed only as a config doc string, one integration test and two commented lines in the sample configs. This PR adds Domain 12 and the Lean module Replication.History, written from the 2.11.0 code on this branch, and registers both everywhere the validator and the governance documents expect. No src/main change. Every defect found while reading the code is RECORDED as a gap (house style: Gap, not fixed here) with a machine-checked Lean witness where the property is expressible, so the fixes can be reasoned about at the spec level first (Constitution Law 1/2/4).

Files

  • specs/12-replication-history/01-operating-modes.md -- the enable x replication_log_only matrix (modes 1/2/3 and the degenerate enable=false, log_only=true combination), the per-batch write order on both executors, database routing (with enable=true EVERY replicated table is routed to replication.history.database.name, bypassing prefix, schema suffix and clickhouse.database.override.map -- verified by BinLogHistoryIT), startup (history connection, CREATE DATABASE / TABLE with the swallowed failure), the config key table with defaults.
  • specs/12-replication-history/02-scd2-table-shape.md -- the sentinel 2100-01-01 00:00:00 (DATETIME32_MAX_TTL), the history columns, ReplacingMergeTree(_version, is_deleted), PARTITION BY toDate(_valid_to), ORDER BY (pk, _valid_to), TTL, and the record path (ClickHouseAutoCreateTable) vs DDL path (MySqlDDLParserListenerImpl) differences D-1 (_valid_from default), D-2 (timezone suffix), D-3 (TTL hardcoded 30 vs replication.history.ttl).
  • specs/12-replication-history/03-scd2-write-protocol.md -- INSERT binding (_valid_from = ts_sec, _valid_to = sentinel, _operation letter code), the UPDATE three-SELECT INSERT ... SELECT UNION ALL (close row at V, after image at V+1, deleted before copy at V), the DELETE two-SELECT (close row plus D marker), the inline UPDATE vs the flushed DELETE, version domains (SnowFlakeId(ts_ms, gtid) vs the standard path), operation-code spelling, what a reader must do.
  • specs/12-replication-history/04-binlog-history-audit-table.md -- the 19-column audit table (golden DDL), per-column values for DML rows and DDL rows, the coordinate sorting key with the row-index sequence fallback, is_deleted always 0, TTL from replication.history.ttl, failure behaviour (a DML audit failure fails the batch, a DDL audit failure is swallowed).
  • specs/12-replication-history/05-replication-log-only.md -- mode 3: audit rows only, data-table processing skipped on ClickHouseBatchRunnable when BOTH flags are true, DDL translated but not executed (executeDDL sits inside if(!log_only)), what the durable offset certifies (Invariant I8 on audit rows), the configuration contract.
  • formal_specs/lean/Replication/History.lean (new lakefile root) -- 18 theorems, lake build clean, no sorry / admit / native_decide.
  • Registration: specs/README.md (Domain 12 index and Lean list), specs/CONSTITUTION.md (section 4 taxonomy row, section 5 module bullet), specs/11-verification-tooling/03-lean-formal-simulation.md (module list), specs/04-query-generation/04-update-splitting.md (section 3.2 pointer and the U code), formal_specs/lean/README.md (tree), scripts/validate_specs.py EXPECTED_DOMAINS (the validator only scans listed domains).

Gaps recorded, each with its Lean witness

  • G-12.03-1 -- the UPDATE history statement runs INLINE without the executeBatch() flush the DELETE branch performs. A row created and updated in one batch has its pre-update version never written to the history, while the current-state view stays correct, so row counts and current-value checks cannot detect it. Witness: staged_insert_writes_no_closed_row, staged_update_current_view_still_correct, and flushed_insert_writes_closed_row for the flushed case.
  • G-12.03-2 -- the close row (is_deleted=0) and the before copy (is_deleted=1) share sorting key (pk, ts) AND _version V. FINAL keeps whichever was physically inserted later inside one INSERT ... SELECT UNION ALL. Witness: close_and_before_share_sort_key_and_version, closed_history_row_depends_on_insert_order.
  • G-12.03-3 -- the close predicate is built from the AFTER image primary key, so an UPDATE that changes a primary-key column never closes the old key (two open rows for one source row). Witness: update_only_closes_after_image_key.
  • G-12.05-1 -- ClickHouseBatchWriter.persistRecords has no log_only skip: single.threaded=true with mode 3 replicates data as SCD2 tables into the history database (parity contract of Spec 03.02). Witness: writer_path_ignores_log_only.
  • G-12.01-1 -- the writer routes on enable or log_only, the runnable on enable alone, so the two engines diverge for enable=false, log_only=true. Witness: routing_diverges_on_log_only_alone.
  • Also recorded in the spec tables: timezone equality of the open-row predicate (G-12.02-1), _valid_to not appended to ORDER BY on the primary_key-override and regex branches of the DDL path (G-12.02-3), version-domain mixing and GTID-off collisions (G-12.03-4), NULL-bound unknown columns in history mode (G-12.03-5), TRUNCATE erasing the history window (G-12.03-6), the swallowed DDL audit insert (G-12.04-1) and startup creation failure (G-12.01-2), and the banner / doc-string wording.

Properties proved for the protocol as shipped: update_supersedes_open_row, delete_hides_open_row, closed_row_continuity, no_open_row_after_delete_marker, at_most_one_live_row_per_sort_key, plus the mode gating and routing theorems log_only_runnable_writes_no_data_rows, log_only_history_still_written, log_only_flag_alone_is_standard_on_runnable, scd2_routes_every_table_to_history_database, standard_mode_writes_no_history.

Verification

  • scripts/validate_specs.py --lake on this branch: PASSED -- 68 specifications, 714 verification citations, lake build exit 0 (Built Replication.History), Invariant I14 pass clean.
  • scripts/tests: 46 passed.
  • Every backticked test or method citation in the five specs resolves to an existing class or method, and every Replication.History.name resolves to a declared theorem (validator pass 5).

Assumptions

  • The Lean theorems assume every existing row at (k, sentinel) carries _version at most V -- the version-domain condition spelled out in 12.03 s3.5.
  • Behaviour statements come from reading the code on this branch (file and method cited in every Codebase Mapping section) and from the four history integration tests (VersionHistoryIT, VersionHistoryInitialIT, BinLogHistoryIT, ReplicationLogOnlyIT); each spec lists what those tests do NOT cover.

Follow-ups (not in this PR)

Fix PRs for G-12.03-1 (flush before the inline UPDATE, mirroring the DELETE branch), G-12.03-2 (a distinct version or key for the before copy), G-12.05-1 (the log_only skip on the single-threaded writer) and D-1..D-3 (unify the two creation paths). Each should first turn the corresponding Lean witness into the corrected property and update 12.x, then change the code.

@minguyen9988
spec(12): replication-history modes -- SCD2 tables and replication-lo…
892656b 
…g-only, with Lean model

Two of the three operating modes had no single specification: per-table SCD2
history (replication.history.enable=true) was scattered over 04.04 s3.2,
02.01 s3.5, 08.05, 06.05, 06.09 and 05.02, and replication-log-only
(replication.history.replication_log_only=true) had none at all. This adds
Domain 12 and a Lean module that follow the 2.11.0 implementation exactly and
record its defects as gaps with machine-checked witnesses, so they can be
debugged at the spec level before the code changes. No src/main change.

specs/12-replication-history/
  01-operating-modes.md            enable x log_only matrix, per-batch writes,
                                   database routing (every table -> history db),
                                   startup, the degenerate combination
  02-scd2-table-shape.md           columns, sentinel 2100-01-01, engine,
                                   PARTITION BY toDate(_valid_to),
                                   ORDER BY (pk, _valid_to), TTL; record-path
                                   vs DDL-path differences D-1..D-3
  03-scd2-write-protocol.md        INSERT binding, UPDATE 3-SELECT and DELETE
                                   2-SELECT statements, versions, key predicate,
                                   inline UPDATE vs flushed DELETE; gaps
                                   G-12.03-1..6
  04-binlog-history-audit-table.md the 19-colu
8000
mn audit table: DDL, per-column
                                   values, DML and DDL rows, TTL
  05-replication-log-only.md       audit rows only, DDL translated not
                                   executed, what the offset certifies,
                                   single-threaded parity gap

formal_specs/lean/Replication/History.lean (new lakefile root)
  SCD2 row sets over the FINAL view at (pk, _valid_to):
  update_supersedes_open_row, delete_hides_open_row, closed_row_continuity,
  at_most_one_live_row_per_sort_key; gap witnesses
  staged_insert_writes_no_closed_row (UPDATE runs inline without the flush the
  DELETE path performs), closed_history_row_depends_on_insert_order (close row
  and before copy tie on sorting key and version),
  update_only_closes_after_image_key (key predicate from the after image);
  log-only gating and routing on both executors (writer_path_ignores_log_only,
  routing_diverges_on_log_only_alone). lake build clean, no sorry.

Registration: specs/README.md, CONSTITUTION.md s4/s5, 11.03 module list,
04.04 s3.2 pointer, formal_specs/lean/README.md, validate_specs.py
EXPECTED_DOMAINS (+12-replication-history).

Verification: scripts/validate_specs.py --lake PASSED (65 specs, 622
citations, lake build exit 0); scripts/tests 39 passed.
@minguyen9988
minguyen9988 merged commit 7396c3c into Altinity:2.11.0 Sep 26, 2026
2 checks passed
This was referenced Sep 26, 2026
Merged
Merged
minguyen9988 added a commit to minguyen9988/clickhouse-sink-connector that referenced this pull request Sep 26, 2026
@minguyen9988
Merge branch 2.11.0 (upstream a1d51fa) into fix-replication-history-m…
fc93aa1 
…odes

Upstream squash-merged the Domain 12 specification as 7396c3c (Altinity#1507) and
then landed Altinity#1508-Altinity#1510; the ten add/add conflicts were the squash artefact
(upstream copies byte-identical to the spec commit) and were resolved to the
corrected specs and Lean model of this branch. The Java merges were automatic
and orthogonal (ResumeReplayLogSummary hooks in DebeziumChangeEventCapture,
writer-connection close in ClickHouseBatchRunnable). Both modules compile;
the history/DDL/clamp unit suites and the resume-replay and close-connection
suites are green; validate_specs.py --lake passes (68 specs, 748 citations).

Destructive-Op-Check: sites=0; result=pass
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

 3704

1 participant

@minguyen9988
0