Repository navigation
feat(upgrade): prove + spec drop-in upgrade safety (Invariant I11) - #1466
Merged
Merged
Conversation
Guarantees that a newer connector is a drop-in replacement for an older one: upgrading in place 2.8.0 / 2.9.1 / 2.10.x -> 2.11.0 (same ClickHouse tables, same persisted offset store, same schema history, same config) does NOT ruin data already in ClickHouse. Rows written by the old version and rows written by the new version coexist in one ReplacingMergeTree table and FINAL still equals the source. Formal verification (formal_specs/lean/Replication/Upgrade.lean): - Generalise the engine to an arbitrary version scheme v : Nat -> Nat (live version at ordinal i; relocation tombstone v i - 1) and prove replicate_convergesV: convergence holds for ANY gap-monotone scheme. So the absolute _version numbers a given connector emits are irrelevant to correctness - only their order matters. - upgrade_safe: replicating a stream whose first n ordinals use the OLD version scheme and the rest use the NEW scheme converges, provided the combined scheme stays gap-monotone (the new version continues strictly above the last version the old one wrote). That is the drop-in-replacement guarantee. - liveVersion_gapMono: the shipped ordinal scheme 2*i is gap-monotone. All three depend only on [propext, Quot.sound] (no sorryAx), verified via #print axioms. Compatibility analysis backing the theorem hypothesis (2.8.0/2.9.1/2.10.3 vs 2.11.0), recorded in specs/02-versioning/06-upgrade-compatibility.md: - _version formula precedence and arithmetic preserved (gtid > sequenceNumber > lsn > SnowFlakeId(ts,offset)); 2.11.0 only ADDS branches. The no-GTID sequence anchor moved from envelope ts to source ts (#1346), which cannot invert a post-upgrade row against a pre-upgrade one given the restart gap. - Debezium is 3.1.3.Final in all four versions, so the offset-store and schema-history serialisation is byte-compatible; 2.11.0 reads the committed position written by 2.8.0/2.9.1/2.10.x. - No config key removed or renamed; hardcoded replacingmergetree.delete.column default unchanged ("sign") - existing deployments keep their own config. Spec/governance: add Invariant I11 (Drop-in Upgrade Safety) to CONSTITUTION.md, add spec 02.06, wire Upgrade.lean into the lakefile roots and the validate_specs.py Lean module + no-sorry check, and document the theorems in the Lean README. Destructive-Op-Check: sites=3; result=pass
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR is opened for maintainer review and is marked WIP / DO NOT MERGE - the maintainers own the merge decision.
Purpose
Guarantee (in spec + formal verification) that a newer connector is a DROP-IN replacement for an older one: upgrading in place 2.8.0 / 2.9.1 / 2.10.x -> 2.11.0 - same ClickHouse tables, same persisted offset store, same schema history, same config - does NOT ruin data already in ClickHouse. Rows written by the old version and rows written by the new version coexist in one ReplacingMergeTree table and FINAL still equals the source.
Formal verification (formal_specs/lean/Replication/Upgrade.lean)
All three depend only on [propext, Quot.sound] (no sorryAx), verified via #print axioms. lake build is green; validate_specs.py rejects any sorry in the Lean sources.
Compatibility analysis backing the theorem hypothesis (2.8.0 / 2.9.1 / 2.10.3 vs 2.11.0)
Recorded in specs/02-versioning/06-upgrade-compatibility.md:
Governance
Adds Invariant I11 (Drop-in Upgrade Safety) to specs/CONSTITUTION.md, adds spec 02.06, wires Upgrade.lean into the lakefile roots and the validate_specs.py Lean module list + no-sorry gate, and documents the theorems in the Lean README. Built/checked with Lean 4.11.0.