Heterogeneous Database Migration Verifier

migration-verifier

Silent data corruption during a database migration is loss of injectivity -- and the same criterion decides whether the verifier you are using to look for it can see anything at all.

A migration moves 29 rows from H2 to SQLite. Nothing goes wrong. Every row comes back different.

account  source 10001            (String)     target 10001            (Integer)
amount   source 10.0000          (BigDecimal) target 10               (Integer)
active   source true             (Boolean)    target 1                (Integer)
seen     source 2024-01-15 09:00 (Timestamp)  target 1705309200000    (Long)

Three columns differ on every row of a migration in which nothing went wrong. The signal-to-noise ratio of a naive comparison is not poor -- it is zero, because the noise is total. So you write canonicalisation rules to normalise the noise away. Each rule you add makes the verifier quieter. Some of those rules are also deleting the evidence, and the verifier cannot tell you which, because a rule that hides a defect and a rule that removes noise produce the same output: silence.

This project measures which rules are which, and derives the criterion that separates them.

The result

A rule is safe if and only if it is injective -- if it never maps two distinct inputs to the same output. '0000007' -> 7 is not injective, so it is corruption. 0.1 -> 0.1000 is injective, so it is representation. That single test, applied to the verifier's own rules, predicts every blindfold measured here:

The converse does not hold and is not claimed: two non-injective rules never blinded anything here, which is a fact about this corpus, not a theorem.

What is measured

Everything in docs/results.md is generated by running the code against real H2 and SQLite JDBC drivers. Eleven predictions were registered before the runs; three held and eight were contradicted, and the contradictions are the interesting part. Highlights:

• The rule lattice has no gradient. Seven rules, 128 subsets. 120 of them false-flag all 27 clean rows; 8 flag none. Nothing in between. The 8 that work are exactly the subsets containing {numeric, boolean, temporal, identifier}. This is why verifier tuning gets abandoned: the first three correct fixes produce byte-identical output, so it looks like nothing you do helps.
• A set-level check catches what no row comparison can. COUNT(DISTINCT name) returns 26 on the source and 27 on the target across rows that are byte-identical one at a time -- the target's collation folds a smaller alphabet, so a UNIQUE(name) constraint silently weakens. Then three of the five defective migrators defeat that check by compensating error, their own damage merging a pair and cancelling the divergence back to 26 = 26.
• Copy migration and dual-write are not the same problem. Identical rule set: precision 1.00 verifying a copy, 0.07 verifying a dual write, because the write path binds the timestamp as a string and the temporal rule stops recognising it.
• The verifier certifies a column whose meaning is machine-dependent. 2024-03-31 02:30:00 does not exist in Europe/London. The target stores it as epoch milliseconds with no zone. Reading it back in four zones gives four different wall clocks. The verifier reports zero differences, correctly, because the bytes agree.
• The cutover gate. "The verifier reported no differences" is consistent with a correct migration and with a verifier that cannot detect anything. The gate plants known defects and requires the verifier to be observed catching its own controls before its silence is allowed to mean anything. The perfect-precision configuration -- the one anybody would ship -- fails that gate.

Running it

Requires a JDK 21 and Maven. No network at runtime; no database server (H2 is in-memory, SQLite is a temp file).

.\demo.ps1     # regenerate docs/results.md and print the headline numbers
.\test.ps1     # full verification: build, 121 tests, report freshness, determinism, mutation

Or directly:

$env:JAVA_HOME = '<jdk-21>'
mvn compile
mvn exec:java          # writes docs/results.md
mvn test               # 121 tests

The surefire JVM is pinned to -Duser.timezone=UTC in pom.xml. That is not a flaky-test workaround -- it is one of the findings expressed as build configuration, and the reason is documented at the setting.

Layout

Reading order

1. docs/results.md -- the measurements
2. docs/portfolio/01-the-problem.md -- why this is hard
3. docs/portfolio/03-the-injectivity-criterion.md -- the idea
4. docs/portfolio/04-what-the-tests-caught.md -- four defects the tests found in this code
5. docs/known-limitations.md -- what this does not show