Abstract↩︎

This paper is a theoretical follow-up to the 2019 DBLog paper [1], which introduced a change-data-capture (CDC) mechanism for both backfilling a downstream system from a live source database and streaming its ongoing changes, while the source keeps accepting writes. DBLog reads the table in primary-key range scans (chunks) interleaved with the source change log: watermarks locate each chunk in log order, chunk rows become refresh events, and CDC events repair stale chunk observations. The mechanism requires no table lock, no pause in writes, and no global read transaction, and has since been adopted by Debezium [2] and Apache Flink CDC [3].

The 2019 paper described the mechanism operationally but did not formalize its correctness object. This paper formalizes that object: DBLog constructs a snapshot-equivalent replay certificate without a single physical snapshot read.

The central formal object is a certified virtual cut: a finite evidence bundle whose certified replay reaches the same per-key state as the source at a chosen frontier on a chosen key scope. A virtual cut is extensional: replay equality at a frontier, not a physical snapshot read, and does not assert one source timestamp across chunk rows. The paper proves per-key replay equality for every wellformed DBLog run at its frontier and scope, and that an accepted certificate, evaluated against faithful source observation, witnesses such a run and yields a virtual cut. It also proves a source-side continuation result: on the same scope, an established cut advances to later frontiers by appending the scope-filtered faithful CDC segment committed in between. Each result is Conditional on premises stated where the result appears. Whole-table correctness, exactly-once delivery, sink-state convergence, and transfer to named deployments are not consequences of certificate acceptance alone. All proofs are machine-checked in Isabelle/HOL.

Keywords. databases, distributed systems, online backfill, change-data-capture, formal verification, Isabelle/HOL.

1 Introduction↩︎

The DBLog change-data-capture (CDC) backfill mechanism was introduced in the 2019 DBLog paper [1] and the companion Netflix Tech Blog post [4], which described it operationally: online primary-key chunk reads, watermarks bracketing each chunk in the source log, refresh events derived from chunk rows, ordinary CDC events filling the gaps, and stale refresh rows suppressed when newer log evidence dominates them. DBLog-style mechanisms have since shipped in Debezium [2] and Apache Flink CDC [3], where the chunk-based capture phase this paper calls the backfill is exposed as the incremental snapshot.

Live-source backfills are deceptively simple. A database operator wants to copy a table, or a selected range of keys, into a downstream system while the source keeps accepting writes. A direct physical snapshot would give one clear answer: read the table at one database timestamp, then replay changes after that timestamp. In many production settings that is exactly what the operator is trying to avoid. Holding a read transaction over a large table can be expensive; an interrupted snapshot cannot be resumed and must restart in full; and a table lock taken to read it consistently may block writes to the source.

DBLog-style backfills take a different route. They read the table in primary-key chunks, observe the source log while those chunk reads happen, and combine the two streams of evidence into a finite replay. The chunk reads do not all occur at the same source-log coordinate. Writes can land between them. Some chunk-read rows may already be stale by the time the chosen frontier (the source-log coordinate the backfill aims to match) is reached. The central question is therefore not “which physical snapshot did DBLog read?” but:

Can the evidence DBLog gathered be replayed to the same per-key state as the source at a chosen frontier on a chosen scope, and can that replay-equivalence claim be advanced as the source commits later events?

This paper answers that question extensionally. A virtual cut is replay equality at a frontier on a scope. A certified virtual cut is a virtual cut packaged behind a finite certificate and evidence bundle: the replay prefix, the claimed scope, the claimed frontier, and the source-side evidence needed to justify them.

A virtual cut is point-in-time, but it is not one-shot. DBLog’s backfill phase, the chunk loop, bootstraps the first certified virtual cut for a scope and frontier; once the chunk loop closes, appending the source’s faithful change data advances that cut to later frontiers. Ongoing DBLog operation is therefore a sequence of source-side replay-equivalence claims, and this paper proves both the point-in-time equality and the source-side continuation that links them.

The original papers named the mechanism, motivated its operational shape, and argued informally that watermark bracketing together with stale-row suppression yields a consistent capture of the chosen scope; they did not state that consistency as a formal object, give it a specification, or machine-check it. This paper supplies that account through a layered theorem ladder. The ladder links wellformed DBLog runs to accepted certificates evaluated against faithful source observation, specializes the result to whole-table backfills, and extends it through a source-side continuation that carries a cut to later frontiers. Every theorem in the ladder is mechanically checked in the companion formal development, archived on Zenodo at https://doi.org/10.5281/zenodo.20389697. The paper is therefore a theoretical study of an existing system: neither a re-introduction of DBLog nor a product-verification claim about any named implementation.

The technical development is layered through the source-side core. Figure 1 separates that core ladder from the post-core extension map. Layers 0 through 4 form the core dependency ladder: the source and replay model, abstract DBLog runs, source-side virtual-cut soundness, accepted-certificate soundness, and the whole-table specialization.

Beyond that core, the paper records independent extension paths rather than further ladder rungs. The source-side virtual-cut algebra path has one machine-checked Conditional result: continuation across frontiers and restriction to a sub-scope (Section 11). The remaining certificate-algebra program, disjoint composition, concrete extended-certificate verification, and raw overlap/retry normalization, remains Future work. The destination-side sink path, covering ACK-only receipt and strong sink-state barrier convergence, also remains Future work in this paper; applied destination-state correctness is a Non-claim without a separate fenced, idempotent sink contract and visible apply-barrier evidence.

The practitioner reading path is deliberately front-loaded. Section 2 walks a concrete backfill, and shows the cut advancing, before formal notation appears. Section 3 names the DBLog mechanism in operational terms. Section 4 states what DBLog is, what it is not, and which failure modes matter. Section 8 can be read informally as the certificate and verifier vocabulary, Section 11 records the proved source-side continuation and restriction results, and Section 12 records the sink-state Non-claim. A theory reader can then follow Sections 5 through 11 for the formal definitions, theorem statements, and proof explanations, with Layers 0–4 forming the core ladder and Section 11 the proved post-core source-side algebra.

We use six status labels throughout:

This status vocabulary is part of the contribution. Every strong claim is either proved under visible assumptions, assigned to the deployment, marked as external observation, or explicitly kept outside the theorem.

2 Bootstrapping and Advancing a Virtual Cut: A Running Example↩︎

This section walks through one concrete scenario before any formal definitions appear. It shows what DBLog gathers from a live source database while concurrent writes are happening, how that material is assembled into a replay, what it means for the replay to be “equivalent to a snapshot” without any single physical snapshot read having taken place, and how the equivalence point advances as the source keeps committing writes.

The same example is reused throughout the rest of the paper. The formal model later in the paper makes every term in this section precise; here we stay strictly operational.

2.1 Setup↩︎

A source database carries a single table:

with two live rows at the moment our story starts:

A third user, Carol, has not yet opened an account; account_id 300 does not exist in the table.

A DBLog backfill is running concurrently with normal application traffic. The application keeps writing to the source database while DBLog reads chunks of rows and watches the source log. Our goal in the example is to assemble the replay evidence for these accounts and to show that replaying it has the same per-account outcome as the source at one consistent point in time, even though no two reads happened at exactly that same instant.

2.2 What the Source Log Records During the Backfill Window↩︎

While DBLog is working, four committed writes land in the source log in this order:

Each c_i is a source-log coordinate, a position in the source database’s commit order. We will not need anything more precise than “\(c_1\) happened before \(c_2\), which happened before \(c_3\), which happened before \(c_4\).”

By the time \(c_4\) commits, the source state on these three accounts is:

That is the per-account state we want the assembled replay to reconstruct.

2.3 What the Chunks Read↩︎

DBLog does not pause writes and does not start a global read transaction. It splits the table into two chunks by primary key range:

• Chunk A covers \(\mathit{account\_id} \in \{100, 200\}\).

• Chunk B covers \(\mathit{account\_id} \in \{300\}\).

Each chunk is read at its own moment in source-log time. That a multi-row chunk read counts as a read at one such coordinate is itself a deployment obligation, made precise in Section 3.2.

Chunk A runs at coordinate \(c_1\), so its read sees the state immediately after \(c_1\)’s update committed:

Chunk B runs later, at coordinate \(c_3\), so its read sees Carol’s row after Carol’s \(c_2\) insert but before Carol’s \(c_4\) update:

Notice that the two chunks run at different source-log moments. No single physical snapshot of the table at one timestamp has been taken. Chunk A saw Bob at $100; by the time chunk B was reading, Bob’s balance had already moved to $120.

Both chunk reads here find their rows present, but a chunk read can equally record a key as absent: had chunk B run before Carol’s \(c_2\) insert, it would have observed account 300 not yet in the table, and that observed absence is replayed like any observed value.

2.4 The Chosen Point of Equivalence↩︎

The backfill targets a specific source-log moment for the assembled replay to match. We pick frontier \(f = c_4\): the source-log position immediately after the last write in our story. The scope of the backfill is the set of accounts we are claiming: \(K = \{100, 200, 300\}\) (Alice, Bob, Carol).

We will see that DBLog’s gathered material assembles, deterministically, into a per-account state that equals the source state at \(f\) restricted to \(K\), even though no read in our story happened at \(f\), no read happened on all three accounts at the same time, and the source database was never paused.

2.5 How DBLog Assembles the Replay↩︎

DBLog treats every observed source-log event as an ordinary CDC event, every chunk-read row as a refresh event, and concatenates them in source-log order. Such an event is a refresh because it re-states a key’s current stored value, read directly from the table, rather than reporting an incremental change as a CDC event does. For our example the assembled replay sequence is:

Both refreshes from chunk A sit at \(c_1\); the refresh from chunk B sits at \(c_3\). CDC events sit at the source-log coordinate they were committed at. Where a CDC event and a chunk refresh share a coordinate — as item 1 and items 2–3 all sit at \(c_1\) — the CDC event is placed first, because a chunk read at a coordinate already reflects every write committed at that coordinate. Figure 2 places these chunk reads and CDC events on the source-log timeline.

This is the raw replay form: it shows the chunk refreshes DBLog gathered even when a later CDC event for the same key supersedes them. The normalized clean prefix may drop dominated refreshes such as item 3 for account 200 and item 6 for account 300, but \(\mathit{apply}\) produces the same final per-key state from the raw and normalized forms. The raw sequence is useful operationally because it shows what was observed; the normalized sequence is useful mathematically because it makes stale-refresh suppression explicit.

To reconstruct per-account state, we play the seven raw items left to right, each one writing the per-account map. When two items concern the same account, the later one wins for that account’s value.

Walking through:

• Item 1 sets account 100 to 3000.

• Item 2, chunk A’s refresh of account 100, confirms 100 = 3000. No change.

• Item 3, chunk A’s refresh of account 200, sets account 200 to 10000.

• Item 4 introduces account 300 at 2500.

• Item 5 sets account 200 to 12000. This overrides chunk A’s earlier observation of account 200: chunk A saw $100 because it read at \(c_1\), but the \(c_3\) log event is newer and authoritative.

• Item 6, chunk B’s refresh of account 300, confirms 300 = 2500. No change yet.

• Item 7 sets account 300 to 3500. This overrides chunk B’s earlier observation of account 300: chunk B saw $25 because it read at \(c_3\), but the \(c_4\) log event is newer and authoritative.

The final per-account state, restricted to scope \(K = \{100, 200, 300\}\):

Compare against the source state at \(f = c_4\) restricted to \(K\):

They match. The assembled replay reproduces the source state at \(f\) on every account in the scope \(K\), even though chunk A and chunk B each read at a different earlier moment, and even though one of chunk A’s observations and chunk B’s only observation were both already stale by the time \(f\) was reached.

2.6 Continuation Beat: Advancing the Cut to a Later Frontier↩︎

The seven-item replay above is a virtual cut at one frontier: applying it reaches the source state at \(f = c_4\) on the scope \(K = \{100, 200, 300\}\). A DBLog deployment does not stop there. The chunk loop has closed, but the source keeps committing writes and DBLog keeps consuming the source log, so the cut can be advanced.

Suppose one more write lands after \(c_4\):

DBLog does not re-read a chunk to account for this. The single CDC event the source committed after \(c_4\) and through \(c_5\) is the continuation segment for that interval, and advancing the cut is just appending it — provided the CDC feed faithfully delivers exactly that segment and the source log still retains the interval, obligations Section 11 makes precise. The replay gains one item:

Playing item 8 after the seven-item replay makes account 200 absent. The delete overrides both chunk A’s earlier refresh of account 200 and the \(c_3\) update, exactly as the \(c_3\) update had overridden chunk A’s older value: a refresh that once observed a value does not force that value to survive when a later source-log event supersedes it, and a delete supersedes with absence rather than a new value. Deletes are not a special escape hatch; absence is just another state the latest event can leave behind.

The eight-item replay is now a virtual cut at the later frontier \(f' = c_5\). Its per-account state on \(K\) is account 100 = 3000, account 200 absent, account 300 = 3500 — which is the source state at \(c_5\) on \(K\). The point of equivalence moved from \(c_4\) to \(c_5\) by appending the one event the source committed in between; no chunk was re-read. Had that event been an ordinary insert or update rather than a delete, it would have appended in exactly the same way. This is the running example’s instance of the continuation result of Section 11: ongoing DBLog operation is a sequence of virtual cuts, each later cut the earlier one extended by the source’s faithful change data.

This says nothing, by itself, about whether a destination consuming the replay has applied item 8 or reached the state in which account 200 is absent. That remains a separate sink-side question (Section 12).

2.7 What “Snapshot-Equivalent” Means Here↩︎

There is no moment in this story when DBLog read the entire table at one source-log position. Chunk A saw account 100 and account 200 at \(c_1\); chunk B saw account 300 at \(c_3\). Because the two reads happened at different points in the source database’s commit order, DBLog must reconcile them through the source log rather than read them as one instantaneous observation.

What DBLog does have is enough source-log evidence around each chunk read to know which observations are still authoritative at the chosen frontier and which have been superseded. That is the content of the assembled replay sequence above: a deterministic mix of chunk-read refreshes and CDC events that, taken together, have the same per-key replay outcome as the source state at \(f\) on the scope \(K\).

The phrase “snapshot-equivalent replay certificate without requiring a single physical snapshot read” is exactly this: the replay outcome equals the source state at \(f\) restricted to \(K\).

2.8 What This Example Does Not Show↩︎

The example is small on purpose. Several things it does not claim, and that the rest of the paper handles:

• It is not a physical cut. DBLog never performed a single read covering all of {100, 200, 300}: chunk A read accounts 100 and 200 at \(c_1\), and chunk B read account 300 at \(c_3\). The equivalence is extensional: outcomes match at \(f\) on \(K\), not that DBLog secretly took a snapshot.

• It is not a whole-table claim. The example claims only the three accounts in K. Other accounts in the source table are not addressed by this example. Whole-table correctness is a derived specialization handled later in the paper, with extra conditions attached.

• It is not a sink-state claim. What we have shown is the assembled replay sequence. Whether a sink that consumes this sequence converges to the same per-account state is an additional contract on the consumer: idempotency, ordering, and fencing. The example does not engage that contract. The paper’s later sections name the sink-state question explicitly and treat it as out of the headline.

2.9 What Coordination DBLog Still Needs↩︎

Avoiding a physical snapshot read does not mean working without coordination. The example silently relied on several pieces of source-side discipline that the paper makes explicit later:

• A source-log ordering that is monotone and well-defined enough to compare the chunk-read coordinate of chunk A (\(c_1\)) to the CDC event for account 200 at \(c_3\) and conclude that \(c_3\) is later. Without a comparable ordering on commit positions, the “later wins” rule cannot be applied.

• Chunk-read watermarks placed in the source log around each chunk read, so DBLog can locate chunk A’s read in source-log order — placing its observation of account 200 before the \(c_3\) event for account 200, and so recognizing that event as strictly newer. The example treats the chunk-read coordinate as known; the source-side mechanism that makes it known is the watermark bracket, made precise in the next section.

• Source-log retention: the source log must still carry \(c_1\) through \(c_4\) when DBLog assembles the replay. If the log had truncated \(c_1\) before chunk A was reconciled, the assembled replay would have a gap and DBLog would not be able to claim the scope \(K\) up to \(f\).

• Chunk-read consistency: chunk A’s two rows must both reflect the source at the single coordinate \(c_1\). The watermark bracket locates the read in source-log order but does not by itself establish that single-coordinate attribution; a consistent statement-level read, or per-row coordinate evidence, is what the deployment must supply. Section 3.2 makes this obligation precise.

These are concrete operational obligations on the deployment, not features DBLog removes. They reappear in the formal model as explicit predicates and assumptions, and again in the closing sections as deployment obligations and external observation assumptions.

2.10 What Comes Next↩︎

The next section names the operational vocabulary used above precisely: chunk plan, watermarks, refresh events, ordinary CDC events, raw replay, normalized clean prefix, stale-refresh dominance at replay time, clean prefix, frontier, scope. The section after that states what DBLog is, what it is not, and which failure modes matter; the formal sections then lift those names into definitions, and the per-account map produced by the seven-item replay sequence becomes the object the central theorem equates with the source state at the chosen frontier restricted to the chosen scope. By the time we reach the theorem statement, every move in this section will have a named formal counterpart.

The paper later proves the general theorems this example is meant to illustrate. Playing the seven-item replay sequence produces the same per-account map as the source state at the frontier \(f = c_4\) restricted to \(K\); appending the eighth item then advances that cut to the later frontier \(f' = c_5\).

3 The DBLog Mechanism↩︎

The running example used two chunks and four source-log events. This section abstracts from that example to the DBLog mechanism itself. The goal is not yet to prove the theorem; the goal is to give names to the operational pieces that the theorem later constrains. Figure 3 walks the same running example through the mechanism’s coordinate axis, source-log events, refresh windows, and the merged raw-replay matrix.

3.1 Chunks and Scope↩︎

DBLog begins with a scope: the set of primary keys for which the backfill will make a claim. In the example, the scope was the three account ids {100, 200, 300}. In a larger deployment the scope might be a table, a shard, a tenant, or a selected key range.

The scope is partitioned into chunks. Each key in the claimed scope belongs to exactly one responsible chunk in the model used by this paper. That strict ownership rule is not incidental. If two chunks both own the same key, or if a key in the claimed scope belongs to no chunk, then the replay no longer has a single disciplined source for that key’s refresh evidence. Overlap and retry can be modeled, but not by pretending strict ownership still holds; the paper treats richer overlap/retry schemes as future extensions unless their normalization is made explicit.

The model also abstracts from how the finite chunk plan is discovered. A deployment must still know when the chunk loop has reached the intended end of the claimed key scope. For a whole-table run, a common way to establish that fact is to record the table’s maximum primary key, or an equivalent end-of-table observation, with enough source-side context to know which table population the bound refers to. For a selected range, shard, tenant, or other scoped run, the analogous obligation is an end-of-scope witness for that chosen scope. This is a Deployment obligation; faithfulness of the primary-key ordering and of the source-side observation that supplies the bound remains an External observation assumption.

3.2 Watermarks and Chunk-Read Coordinates↩︎

A chunk read has to be located in source-log time: to merge a chunk’s rows with the live CDC stream, DBLog must know which source-log events precede the chunk’s observations and which supersede them. The mechanism that establishes this is the watermark. Just before it begins a chunk read, DBLog writes a marker row — a low watermark — into a dedicated watermark table in the source; when the chunk scan finishes, it writes a second marker, the high watermark. Both are ordinary source writes, so both surface in the source change log at definite coordinates, and the chunk SELECT ran between them. These watermark writes mean the baseline mechanism needs write access to the source database; a deployment that cannot write to the source would need another way to locate its chunk reads in the log.

The watermark pair establishes provenance: it brackets the chunk read in source-log order, fixing which committed source events precede the read and which follow it. The model then attributes the whole chunk read to a single chunk-read coordinate — the running example’s “chunk A read at \(c_1\)” — and treats every row image the chunk returned as faithful to the source at that coordinate. That single-coordinate attribution is a stronger fact than the watermark bracket alone supplies. A multi-row chunk SELECT is not instantaneous, so the bracket locates the read but does not by itself prove that every returned row image reflects the source at one shared coordinate. The attribution is sound only when the deployment also supplies one of two things: chunk-read semantics that make the returned rows a consistent read at a single source coordinate — for instance a statement-level snapshot or repeatable-read scan — or per-row coordinate evidence pinning each returned image to the coordinate at which it held. The shorthand “chunk A read at \(c_1\)” therefore stands for both facts together: chunk A’s watermarks bracket \(c_1\), and chunk A’s row images are faithful to the source at \(c_1\).

In the original DBLog mechanism the watermark pair does more than locate the read: the interval between the low and the high watermark is also the window over which stale chunk rows are suppressed — a chunk row is discarded when the source log shows a write for the same key inside that window. This paper’s model abstracts that windowed interleaving into two simpler pieces: a single chunk-read coordinate at which each returned row image is faithful, and a frontier-wide latest-event-wins replay (§3.3). The two views reach the same per-key state, by the window-suppression equivalence of §3.4. A write committed inside the watermark window is itself an ordinary CDC event the replay carries, and latest-event-wins lets it override the chunk row exactly as in-window suppression would; a write after the high watermark is carried the same way. So “suppressed inside the window” and “overridden later, at the frontier” are the same fact. The low and high watermarks are kept in the formal run only as the operational provenance of the chunk-read coordinate; they carry no separate state-equality obligation of their own beyond the chunk-read-coordinate provenance and row-image honesty obligations §5.5 makes explicit. The watermark pair is therefore the deployment’s means of establishing that coordinate, not a formal object the theorem itself consults.

Both facts are deployment obligations, not properties DBLog establishes for free: a source log that exposes an ordering and is retained long enough for DBLog to compare chunk rows against later CDC events, and the single-coordinate row-image faithfulness just described. §5.5 carries them as wellformed-run obligations, with the row-image fact appearing as the “Refresh honesty” obligation.

DBLog avoids a single physical snapshot read; it does not avoid source-log coordination.

3.3 Refresh Events and Ordinary CDC Events↩︎

DBLog turns each chunk-read row into a refresh event. A refresh says: “at this chunk-read coordinate, key \(k\) was observed with this value,” or “key \(k\) was observed absent.” A source-log write becomes an ordinary CDC event: insert, update, or delete at its source-log coordinate.

Both kinds of event enter one replay vocabulary. Ordinary CDC events carry committed source writes. Refresh events carry row observations from chunk reads. Applying a replay means walking the event sequence left to right and updating the per-key state; later events for the same key win. That latest-event-wins behavior is what made Bob’s \(c_3\) update override chunk A’s older refresh in the example.

3.4 Raw Replay and Normalized Clean Prefix↩︎

The replay evidence DBLog assembles is one finite sequence, the clean prefix, and it comes in two forms. This subsection defines both. The theorems in this paper are stated about the raw form; the normalized form is an optional, \(\mathit{apply}\)-equivalent presentation.

The raw replay is the evidence-preserving sequence: it may include a refresh even if a later CDC event for the same key dominates it. Raw replay is useful operationally because it shows exactly what DBLog observed.

The normalized clean prefix is an optional, \(\mathit{apply}\)-equivalent view: the formal development takes the raw clean prefix as its proof object, and normalization is a presentation that makes stale-refresh suppression explicit. It may suppress refresh events that are dominated by newer source-log evidence, provided suppressing them does not change the final \(\mathit{apply}\) state. In the example, Bob’s chunk-A refresh was dominated by Bob’s later c3 update; Carol’s chunk-B refresh was dominated by Carol’s later c4 update. Carrying or suppressing those dominated refreshes gives the same final per-key state. The proof-facing bridge is state equivalence on the claimed scope: suppressing only same-key dominated refreshes preserves \(\mathit{apply}\) for every claimed key.

Window-suppression equivalence. Retaining or suppressing a same-key refresh that a later source event dominates leaves \(\mathit{apply}\) unchanged on every claimed key. This is the fact that lets the raw and normalized clean prefixes be used interchangeably, and it is also why original DBLog’s in-window suppression and this paper’s frontier-wide latest-event-wins reach the same per-key state: a refresh overridden inside the watermark window and a refresh overridden later at the frontier are dominated the same way, so \(\mathit{apply}\) does not distinguish them. Section 7 uses this equivalence to state the Layer 2 theorem about the raw clean prefix while leaving normalization an optional presentation.

The theorem later relies on both sides of this story:

• no required CDC event is missing;

• no stale refresh is allowed to resurrect an older value past a newer event;

• suppressing a refresh is justified only when newer source-log evidence dominates it for the same key.

3.5 Frontier and Clean Prefix↩︎

The frontier is the source-log coordinate at which a cut is claimed (concretely, a MySQL executed-GTID set, a PostgreSQL LSN, or a CockroachDB resolved timestamp). A certificate does not merely claim “some eventual state”; it claims equality at a particular frontier. The clean prefix contains the replay evidence needed through that frontier for the claimed scope.

Operationally, a DBLog certificate is useful only when the operator can say:

for this scope \(K\) and frontier \(f\), here is the finite replay prefix whose application equals the source state at \(f\) on \(K\).

The rest of the paper makes that sentence precise. Section 5 defines the source and replay models. Section 6 names the equality as a virtual cut. Section 7 proves the source-side theorem for wellformed runs. Sections 8 and 9 move from runs to accepted certificates.

The clean prefix is finite but not necessarily small. It carries a refresh for each key in the claimed scope and every in-scope CDC event through the frontier, so it scales with the scope and the change volume over the certified interval — for a large table backfilled over a busy window it is a correspondingly large object. The normalized clean prefix trims refreshes that newer evidence dominates; the raw form, on which the theorems are stated, does not.

3.6 After the Chunk Loop: Advancing the Frontier↩︎

The backfill chunk loop is finite: it runs until the claimed key scope is covered, and then it closes. But the frontier of a virtual cut is not the end of DBLog’s story. Once the chunk loop has established a virtual cut at a frontier \(f\), DBLog continues as ordinary change data capture, consuming source-log events as the source commits them. The source-side story does not need a fresh chunk read for every later frontier. If the source log faithfully supplies the change data the source committed after \(f\) and through a later frontier \(f'\), appending that segment to the clean prefix advances the replay-equivalence claim from \(f\) to \(f'\).

This is the operational reading of the continuation result proved in Section 11: the backfill bootstraps the first virtual cut, and faithful CDC continuation advances it. The chunk reads are the hard part, and they happen once; advancing the established cut to a later frontier is then appending faithful source-log change data. Carrying the cut forward leans on the same source-side discipline the chunk loop already needed — a source-log ordering, and retention of the events between \(f\) and \(f'\) — and Section 11 states the result and its premises precisely.

Practitioner takeaway. DBLog’s mechanism is a small fixed vocabulary: a key scope split into chunks, watermark-bracketed chunk reads attributed to a chunk-read coordinate, refresh events and ordinary CDC events merged into one clean prefix, and a frontier at which the cut is claimed. None of it is free of coordination — a deployment owes a source log that is ordered and retained, chunk reads whose row images are faithful to their coordinate, and a finite chunk partition of the scope. Those obligations, not the watermark trick, are what a real backfill must get right.

4 What DBLog Is, What It Is Not, and Its Limitations↩︎

DBLog is a source-side CDC-plus-chunk-read evidence protocol: live backfill establishes an initial virtual cut, and faithful CDC continuation can advance that cut to later source frontiers. It is a way to synthesize a replay-equivalent stand-in for a snapshot on a chosen scope at a chosen frontier, and to carry that stand-in forward as the source frontier moves. It is not a loophole around coordination, observation faithfulness, or destination semantics. This section states those boundaries before the formal sections begin.

4.1 What DBLog Is↩︎

DBLog is a source-side evidence protocol. It combines:

• a claimed key scope;

• a certified frontier in source-log order;

• chunk reads whose observations become refresh events;

• ordinary CDC events from the source log;

• source-log and chunk-read evidence sufficient to justify the clean prefix;

• a finite replay prefix whose \(\mathit{apply}\) state can be compared with the source;

• a source-side continuation principle: an established virtual cut advances to a later source frontier by appending the faithful change data the source committed in between.

The paper’s positive claim is extensional: replaying the clean prefix reaches the same state as the source at the frontier, restricted to the claimed scope. The certificate does not make the source pause, and the theorem does not need a physical snapshot read.

4.2 What DBLog Is Not↩︎

DBLog is not coordination-free. It needs source-log ordering, retained CDC events, chunk-read coordinates, frontier discipline, and evidence tying those observations to the source. These are Deployment obligations or External observation assumptions, not details the theorem erases.

DBLog is not exactly-once delivery. The theorem is about the state reached by replay, not about how many times a downstream transport delivers an event.

DBLog is not whole-table correctness by default. The core theorem is scoped. Whole-table equality appears later as a derived specialization and only under explicit anchor-domain and no-unclaimed-replay-key side conditions.

DBLog is not sink-state correctness. A destination can receive a certified stream without having applied it, applied it in the intended order, or reached the corresponding state. Section 12 records this as a Non-claim.

DBLog is not continuous destination replication. The source-side continuation result (Section 11) advances a virtual cut to later source frontiers; it does not show that a sink has applied the replay, applied it once, or reached the corresponding state.

DBLog is not a claim that a single physical source-read timestamp existed for all chunk rows. A virtual cut is an equality of outcomes, not a hidden physical cut.

DBLog is not a product-by-name theorem. Debezium, Apache Flink CDC, and source engines such as MySQL, PostgreSQL, and MariaDB are relevant deployment and related-work contexts. This paper does not claim that any named system satisfies the theorem without checking the paper’s assumptions against that system.

4.3 Failure Modes the Certificate Story Must Expose↩︎

The following table is intentionally operational. It says what can go wrong, which part of the evidence story is responsible for catching it, and how the paper classifies the obligation.

The operational rows above, for the initial certificate, are the kind a certificate checker can make visible against the evidence bundle, under the source-side model and, for whole-table lifting, under the extra Layer 4 side condition. The continuation row is the exception: advancing a cut to a later frontier reuses the same evidence-boundary discipline, but a concrete checker for extended certificates is Future work. The final row is the trust boundary: the paper assumes faithful source observation when it turns accepted evidence into a theorem about the mathematical source history. Acceptance alone is not the theorem.

4.4 The Main Limitation to Keep in Mind↩︎

The strongest current statement in the paper is still source-side. It says that accepted evidence, under faithful source observation and the checker substrate obligations, yields a certified virtual cut. It does not say that a concrete parser is correct, that a connector never misreports the source, that a named product implements every assumption, or that a sink has applied the certified replay to state. Those are all meaningful engineering questions. This paper’s contribution is to make clear which ones are inside the theorem and which ones remain obligations or future work.

Practitioner takeaway. Read DBLog as a source-side evidence protocol with sharp edges: it is a replay-equivalent stand-in for a snapshot on a chosen scope and frontier, advanceable to later frontiers — and it is none of the things the boundaries above rule out, including exactly-once delivery, whole-table correctness by default, sink-state convergence, and product-by-name transfer. The failure-mode table is the operational checklist; the standing trust boundary is faithful source observation, which no certificate settles from the inside.

5 Formal Model (Layer 0 and Layer 1)↩︎

The formal model begins with two deliberately small layers. Layer 0 defines the source and replay vocabulary: source histories, source state at a frontier, replay events, replay application, and restriction to a key scope. Layer 1 defines abstract DBLog runs: chunks, watermarks, chunk reads, ordinary CDC observations, clean prefixes, and the wellformedness obligations that make the source-side theorem true.

Neither layer mentions certificates, verifiers, destination ACKs, or whole-table side conditions. That separation matters. Layer 2 proves a theorem about wellformed runs. Layer 3 later explains when an accepted certificate witnesses such a run.

Table 3 fixes the symbols the formal sections use. A predicate (short sans-serif tag like \(\mathsf{WF}\), \(\mathsf{FSO}\), \(\mathsf{Mat}\), \(\mathsf{Coh}\), \(\mathsf{VC}\), \(\mathsf{WTS}\)) is a relation that holds or fails on its arguments; an accessor function (italic word like \(\mathit{apply}\), \(\mathit{src}\), \(\mathit{scope}\), \(\mathit{frontier}\), \(\mathit{prefix}\)) returns a value.

5.1 Source Histories and Frontiers↩︎

A source database is modeled as a base state \(b_0\) together with a finite history \(H\) of committed source events. A source event is one of \[\mathsf{Insert}\,k\,v,\qquad \mathsf{Update}\,k\,v,\qquad \mathsf{Delete}\,k.\] Each event carries a source coordinate: a commit position, log sequence number, monotone source-side timestamp, or equivalent order-bearing token. We write \(c \le c'\) when coordinate \(c\) is no later than \(c'\). A source history is wellformed when its events are ordered by that coordinate, the base coordinate sits before every event, and same-coordinate events have a deterministic source-position order inside the history.

The source state at a frontier is written \(\mathit{src}(b_0,H,f)\). For each key \(k\), this state looks for the latest source event for \(k\) at or before frontier \(f\). An insert or update makes the key present with the written value; a delete makes it absent; no event leaves the key at its base state \(b_0(k)\).

The coordinate convention is inclusive. A chunk read recorded at coordinate \(c\) observes \(\mathit{src}(b_0,H,c)\), including source events at coordinate \(c\). The convention is not an arbitrary tie-break: a chunk read is attributed to the latest coordinate whose committed effects its row images already reflect. §3.2 sets out what a deployment must supply for that attribution to be sound — the watermark bracket locating the read, together with the chunk-read semantics or per-row coordinate evidence that make the returned row images faithful to one coordinate. Canonical replay therefore places same-coordinate CDC evidence before the refresh that records the post-\(c\) chunk-read state. Later source-coordinate events still appear after that refresh.

This is the source-side reference state that every virtual-cut theorem compares against.

5.2 Replay Events and Apply↩︎

DBLog does not replay source events alone. It replays two kinds of replay event: \[\begin{array}{ll} \mathsf{Cdc}\,c\,e & \text{source-log event e at coord.\;c,}\\ \mathsf{Refresh}\,k\,m\,c & \text{chunk-read of k at coord.\;c.} \end{array}\] In a refresh, \(m = \mathsf{Some}\,v\) means the chunk read observed value \(v\); \(m = \mathrm{None}\) means the chunk read observed row absence. Absence is a state fact, not an exception: replaying a refresh with \(\mathrm{None}\) deletes the key from the replay state.

The replay function is \(\mathit{apply}(\sigma)\), where \(\sigma\) is a finite replay sequence. \(\mathit{apply}\) walks the sequence from left to right, updating a per-key map. Later events for the same key win. \(\mathit{apply}\) starts from the all-absent per-key map: \(\mathit{apply}([\,])(k) = \mathrm{None}\) for every key \(k\). Thus the running example’s later update for Bob overrides chunk A’s older refresh, and a later delete would override both an earlier refresh and an earlier update.

State restriction is written \(m \mathbin{\upharpoonright}K\) in prose formulas below: it keeps only the entries whose keys lie in \(K\), so \((m \mathbin{\upharpoonright}K)(k) = m(k)\) when \(k \in K\), and \(\mathrm{None}\) otherwise. The displayed formulas use the \(\mathbin{\upharpoonright}\) symbol throughout.

5.3 Abstract DBLog Runs↩︎

A DBLog run \(R\) is held abstract. The model observes it only through a small set of accessors: \[\begin{align} \mathit{scope}(R)\quad &\text{claimed key scope},\\ \mathit{frontier}(R)\quad &\text{chosen source frontier},\\ \mathit{prefix}(R)\quad &\text{replay sequence of the run},\\ \mathit{chunks}(R)\quad &\text{run's chunk plan},\\ \mathit{srcHistory}(R) &\;\text{source history the run is about},\\ \mathit{cdcEvents}(R) &\;\text{observed CDC events consumed.} \end{align}\] Each chunk has a domain of keys, a responsible-chunk relation from keys to chunks, a lower and upper watermark, and a chunk-read coordinate. The model uses a strict canonical partition: each key in \(\mathit{scope}(R)\) belongs to exactly one responsible chunk, and every responsible chunk has a finite domain. The model also takes the chunk plan itself to be finite — the set of chunks is finite for every run. This is a modeling assumption, not a proof-engineering detail: it reflects that a real backfill runs a bounded chunk loop over a finite plan.

That strict partition is not a claim that real systems never retry or overlap chunk reads. It is the canonical run selected for the theorem. Raw overlap/retry evidence must be normalized into such a canonical run, or handled by a future extension.

5.4 Clean Prefix↩︎

The clean prefix of a run is the finite replay sequence produced from:

• chunk-read refreshes for the responsible chunks;

• observed CDC events for in-scope keys through the frontier;

• the clean-prefix ordering: events sorted by source coordinate, with a CDC event placed before a chunk refresh at a shared coordinate, and same-coordinate CDC events kept in source-log position order;

• suppression, or harmless retention, of refreshes dominated by newer same-key source-log evidence.

The theorem does not rely on a mysterious “good replay” primitive. The clean prefix is constrained by the run’s chunk plan, CDC observations, frontier, and scope. If a needed CDC event is missing, if a future event is replayed, if a refresh appears without a responsible chunk observation, or if same-coordinate CDC order is scrambled, the run is not wellformed for the theorem.

The proof-facing bridge invariant is per-key: for each key in scope, the latest replay event in the clean prefix is either the latest faithful source event through the frontier, or it is a refresh whose value or absence at its read coordinate remains unchanged until the frontier. This is the invariant Layer 2 unfolds rather than assuming as a primitive.

5.5 Wellformed Runs↩︎

We write \(\mathsf{WF}(b_0,R,H)\) for the wellformed DBLog run predicate; it packages the source-side obligations the proof needs. Its clauses say, in reader-facing terms:

The split between Deployment obligation and External observation assumption is intentional. The model can state what a wellformed run must satisfy. It cannot prove, from inside the run, that an external database connector reported every source event honestly or that a chunk read was faithful to the real source.

Refresh honesty carries both labels because it bundles two facts: that a returned row image reports the source value or absence faithfully is an External observation assumption, while that the chunk-read semantics pin those images to a single coordinate (§3.2) is a Deployment obligation.

The wellformed-run predicate carries one further conjunct, not listed above: clean-prefix closure. It is definition-derived — it holds for every run by the clean-prefix construction (Section 5.4) — so it is neither a deployment obligation nor an external observation assumption, and no wellformed run can fail it. The proof may use it; no deployment need establish it separately.

The lower and upper watermarks introduced above are source-log coordinates, not primary-key-range bounds. Accordingly, the Chunk partition row is a statement about the finite canonical partition consumed by the theorem; it is not a proof that a concrete chunk-selection loop stopped in the right place, and Layer 1 contains no maximum-key accessor or chunk-loop termination algorithm. A maximum-primary-key query, an empty-next-chunk observation, a predeclared range bound, or another end-of-scope witness may justify the finite partition operationally. Supplying the resulting partition, including evidence that the loop reached the intended end of the claimed key scope, is a Deployment obligation; the theorem consumes the partition, not the plan-construction algorithm.

5.6 Layer 0 and Layer 1 Lemmas↩︎

The source and replay model supplies the elementary facts used by the main proof:

• \(\mathit{apply}\) is latest-event-wins per key.

• Restricted states are equal exactly when they agree on every key in the scope.

• \(\mathit{src}\) is characterized by the latest source event at or before the frontier.

• A replay-side \(\mathsf{Cdc}\) event has the same per-key effect as its source event.

• A refresh has the source-state value at its chunk-read coordinate when the chunk-read honesty premise holds.

• The source state at a later frontier is the source state at an earlier frontier updated by exactly the source events strictly between them — immediate from the preceding characterization, since the source events at or before \(f'\) are those at or before \(f\) together with those in \((f,f']\). This interval characterization is what the continuation result of Section 11 builds on.

The run layer then contributes the bridge lemma:

\[\begin{align} \mathsf{WF}(b_0,R,H) \,\Longrightarrow{}& \mathit{apply}(\mathit{prefix}(R)) \mathbin{\upharpoonright}\mathit{scope}(R)\\ &{}= \mathit{src}(b_0,H,\mathit{frontier}(R)) \mathbin{\upharpoonright}\mathit{scope}(R). \end{align}\]

That bridge is the Layer 2 theorem stated and explained in Section 7. Section 6 first names the equality itself.

Practitioner takeaway. The objects in this section are the paper’s working vocabulary; the part a real deployment must act on is the wellformed-run obligation table (Table 4) — source-log retention and binding, a finite chunk partition, watermark-bracketed chunk reads, and CDC coverage and faithfulness. A backfill that meets those obligations is exactly the kind of run the soundness theorems in the following sections are about.

6 Virtual Cuts↩︎

The central formal object of the paper is a virtual cut. A virtual cut is not a physical read cut. It is an equality of outcomes: replay reaches the same per-key state as the source at a chosen frontier on a chosen scope.

We write \(\mathsf{VCS}(\sigma,K,f,H)\) for the state-level form, with the base state \(b_0\) left implicit in this four-argument shorthand:

\[\mathsf{VCS}(\sigma,K,f,H) \,\Longleftrightarrow\, \mathit{apply}(\sigma) \mathbin{\upharpoonright}K = \mathit{src}(b_0,H,f) \mathbin{\upharpoonright}K.\]

Here \(\sigma\) is a replay sequence, \(K\) is a key scope, \(f\) is a frontier, and \(H\) is the source history. The base state \(b_0\) is fixed by context; when it matters, the formulas write it explicitly.

The certificate-side form \(\mathsf{VC}(C,H)\) specializes the same equality to the accessors of a certificate:

\[\mathsf{VC}(C,H) \,\Longleftrightarrow\, \mathsf{VCS}\bigl(\mathit{prefix}(C),\mathit{scope}(C),\mathit{frontier}(C),H\bigr).\]

Expanded:

\[\begin{align} &\mathit{apply}(\mathit{prefix}(C)) \mathbin{\upharpoonright}\mathit{scope}(C)\\ &\qquad= \mathit{src}(b_0,H,\mathit{frontier}(C)) \mathbin{\upharpoonright}\mathit{scope}(C). \end{align}\]

The definition is deliberately extensional. It says that two per-key states are equal on a scope at a frontier. It does not say that every chunk row was read at that frontier, that one physical source snapshot existed, that the scope is the whole table, or that any destination has applied the replay. Figure 4 contrasts a physical cut with the virtual cut this paper proves.

Practitioner takeaway. A virtual cut is an equality of outcomes, not a physical snapshot: applying the replay reaches the same per-key state as the source at the chosen frontier on the chosen scope — and asserts nothing about how the rows were read, whether one snapshot timestamp ever existed, or whether any destination has applied the replay.

This is the exact shape illustrated by the running example. There, the replay sequence has seven items, the scope is \(\{100,200,300\}\), the frontier is \(c_4\), and \(\mathit{apply}\) produces the same balances as \(\mathit{src}\) at \(c_4\) on those three keys. Chunk A and chunk B were read at different coordinates; the virtual cut does not hide that fact. It says the replay outcome is snapshot-equivalent on the claimed keys.

The state-level form is useful because Layer 2 proves the equality for run accessors:

\[\mathsf{VCS}\bigl(\mathit{prefix}(R),\mathit{scope}(R),\mathit{frontier}(R),H\bigr).\]

Layer 3 then proves that an accepted certificate, under faithful source observation, witnesses a run whose accessors agree with the certificate. That is how the run-side theorem becomes the certificate-side theorem.

7 Source-Side Virtual-Cut Soundness (Layer 2)↩︎

Layer 2 proves the source-side theorem:

\[\begin{align} \mathsf{WF}(b_0,R,H) \,\Longrightarrow{}& \mathit{apply}(\mathit{prefix}(R)) \mathbin{\upharpoonright}\mathit{scope}(R)\\ &{}= \mathit{src}(b_0,H,\mathit{frontier}(R)) \mathbin{\upharpoonright}\mathit{scope}(R). \end{align}\]

Reader-facing theorem summary:

• Status: Conditional — machine-checked under the displayed premises.

• Claim: the clean prefix of a wellformed DBLog run reaches the source state at the run frontier on the run scope.

• Premises: the wellformed-run obligations in Section 5.5, including chunk partition, CDC coverage and faithfulness, chunk-read honesty, and read-before-frontier discipline.

• Boundary: this is a source-side run theorem, not yet a certificate, whole-table, or sink-state theorem.

Here, Conditional means machine-checked under the displayed premises, not unproved or merely plausible.

Equivalently, every wellformed DBLog run satisfies the virtual-cut-state equality at the run’s frontier on the run’s scope. The theorem is stated about the run’s raw clean prefix; by the window-suppression equivalence of §3.4, the normalized clean prefix yields the same \(\mathit{apply}\) state and therefore the same equality.

The theorem is Conditional on the wellformed-run model. That does not mean the proof is informal. It means the proof assumes exactly the wellformed-run predicate of Section 5.5: chunk partition, frontier discipline, CDC coverage and faithfulness, and chunk-read honesty. Each of these is visible because omitting it permits a real counterexample (Table 5). The predicate’s remaining conjunct, clean-prefix closure, is instead definition-derived: it holds for every run by the clean-prefix construction, so the proof may use it but no deployment need establish it separately.

7.1 Proof Idea↩︎

The proof is a per-key latest-event argument.

First, restricted-state equality reduces the theorem to pointwise equality. It is enough to show that for every key \(k\) in \(\mathit{scope}(R)\):

\[\mathit{apply}(\mathit{prefix}(R))(k) = \mathit{src}(b_0,H,\mathit{frontier}(R))(k).\]

Fix such a key \(k\). Since the run is wellformed, \(k\) has a unique responsible chunk, and the chunk-read evidence produces a value-or-absence refresh for \(k\) that belongs to \(\mathit{prefix}(R)\), including \(\mathsf{Refresh}\,k\,\mathrm{None}\,c\) when the row is absent at the chunk-read coordinate. Therefore the “no replay event for \(k\)” case cannot occur for an in-scope key, and the clean-prefix-of-latest correspondence — the per-key step that says every in-scope \(k\) has a latest event in \(\mathit{prefix}(R)\), and that event is either a CDC event or the responsible chunk’s refresh — collapses to the two cases below.

There are two real cases.

7.2 Case 1: The Latest Replay Event Is CDC↩︎

Suppose the latest replay event for \(k\) in \(\mathit{prefix}(R)\) is a CDC event \(\mathsf{Cdc}\,c\,e\). The clean-prefix coherence obligations say this replay event comes from an observed CDC pair. CDC faithfulness says that observed pair is a real source event in \(H\); because the event lies in the clean prefix, its source coordinate \(c\) is within the run’s frontier, i.e.\(c \le \mathit{frontier}(R)\). Order preservation and same-coordinate multiplicity say the replay did not silently reverse or drop competing source events for the same key and coordinate.

Now assume, for contradiction, that the source history has a later event for \(k\) at or before the frontier. CDC coverage would put that later event into the observed CDC list. Clean-prefix closure would put it into the replay. The clean-prefix ordering would place it after \(\mathsf{Cdc}\,c\,e\), contradicting the choice of \(\mathsf{Cdc}\,c\,e\) as the latest replay event for \(k\).

So the latest replay CDC event corresponds to the latest source event for \(k\) through the frontier. \(\mathit{apply}\) and \(\mathit{src}\) therefore make the same update at \(k\).

7.3 Case 2: The Latest Replay Event Is a Refresh↩︎

Suppose the latest replay event for \(k\) is \(\mathsf{Refresh}\,k\,m\,c_{\mathit{read}}\). The responsible-chunk obligations identify the chunk that produced it, and refresh honesty says:

\[m = \mathit{src}(b_0,H,c_{\mathit{read}})(k).\]

If there were a later source event for \(k\) in \((c_{\mathit{read}}, \mathit{frontier}(R)]\), CDC coverage and clean-prefix closure would place a corresponding \(\mathsf{Cdc}\) event after the refresh in the clean prefix. The interval is open at \(c_{\mathit{read}}\) because a read at \(c_{\mathit{read}}\) already observes source events at \(c_{\mathit{read}}\); the post-read repair obligation starts after the read coordinate and runs through the frontier. A later source event would contradict the refresh being latest for \(k\).

Therefore the source state for \(k\) at the read coordinate is still the source state for \(k\) at the frontier. The refresh writes exactly that value or absence, so \(\mathit{apply}(\mathit{prefix}(R))(k)\) equals \(\mathit{src}(b_0,H,\mathit{frontier}(R))(k)\). The value case and the row-absence case use the same equation; absence is just \(\mathrm{None}\) in the per-key state.

7.4 Why the Assumptions Are Load-Bearing↩︎

The proof fails if the obligations are weakened.

These negative cases are not side decoration. They are why the theorem’s premise is the full wellformed-run predicate rather than a vague statement that DBLog “collected some chunks and some CDC.”

Practitioner takeaway. This is the paper’s core guarantee: a backfill that meets the wellformed-run obligations emits chunk reads and CDC events that replay to exactly the source state at the chosen frontier, on the chosen key scope — with no table lock, no paused writes, and no global read transaction. The result is scoped to that run; the sections that follow add a checkable certificate and the side conditions under which it lifts to the whole table.

8 Certificates, Evidence, and Verifiers↩︎

Layer 2 proves a theorem about an abstract DBLog run: if the run is wellformed, its clean replay prefix reaches the source state at its frontier on its scope. A deployment, however, does not hand a reader an abstract run. It hands over a certificate and evidence. This section explains the certificate-side vocabulary informally; Section 9 gives the theorem and proof story.

8.1 Certificate↩︎

A sec:certificate is the claim object. It names: \[\begin{align} \mathit{scope}(C)\quad &\text{the keys being claimed},\\ \mathit{frontier}(C)\quad &\text{the source-log coordinate of the claim},\\ \mathit{prefix}(C)\quad &\text{the certified replay prefix.} \end{align}\] The clean-prefix accessor is semantic. It is not a permission for a serialized certificate to authenticate any arbitrary list of replay events by storing it. The prefix becomes safe only when accepted evidence materializes a wellformed run and ties the certificate accessors to the run accessors. Before acceptance, \(\mathit{prefix}(C)\) is only the claimed prefix; the certificate theorem uses it only after accepted evidence materializes a coherent wellformed run that agrees with that accessor.

8.2 Evidence↩︎

An evidence bundle contains the source-side material the checker inspects: certificate binding evidence, the chunk plan, chunk-read coordinates, chunk domains, observed row values or absences, ordinary CDC observations, and the construction evidence for the raw or normalized clean prefix.

The evidence bundle does not contain a destination-state proof. It does not contain sink ACK semantics. It does not contain whole-table claim-scope side conditions except where those are added later for the whole-table specialization. The certificate layer is source-side.

8.3 Materialized Run↩︎

The certificate theorem needs a bridge from artifact to model. That bridge is the materialization relation \(\mathsf{Mat}(C,E,R)\): certificate \(C\) and evidence \(E\) together describe the abstract DBLog run \(R\) consumed by the Layer 2 theorem. Materialization is structural — it connects the evidence to a run carrier with a scope, frontier, clean prefix, chunk plan, chunk-read observations, and CDC observations — but does not by itself say that the run is wellformed against the source history.

Concretely, \(\mathsf{Mat}\) is a transcription: the materialized run’s scope, frontier, clean prefix, chunk plan, chunk-read observations, and CDC observations are exactly the fields \(C\) names and \(E\) serializes. \(\mathsf{Mat}\) can fail: if the evidence does not serialize a usable run shape — a missing chunk-plan field, or fields too malformed to assemble into a run carrier — then no run \(R\) satisfies \(\mathsf{Mat}(C,E,R)\), so the relation is a real structural obligation, not a tautology. Materialization adds no wellformedness and no faithfulness of its own; that work is done by the coherence predicate and the checker-substrate obligations, not hidden inside the bridge.

Rejected and unsupported evidence need not materialize any run. Accepted evidence must not leave the checker free to choose an arbitrary convenient run; that is exactly what the coherence predicate below prevents.

8.4 Certificate / Run Coherence↩︎

We write \(\mathsf{Coh}(C,E,R)\) for the certificate / run coherence predicate. It packages materialization with accessor agreement between \(C\) and \(R\):

\[\begin{align} \mathsf{Coh}(C,E,R) \,\Longleftrightarrow\,& \mathsf{Mat}(C,E,R)\\ \land\,& \mathit{scope}(C)=\mathit{scope}(R)\\ \land\,& \mathit{frontier}(C)=\mathit{frontier}(R)\\ \land\,& \mathit{prefix}(C)=\mathit{prefix}(R). \end{align}\]

The evidence parameter is load-bearing. Coherence is not “there exists some run with matching accessors.” It is about the run materialized by this certificate/evidence pair.

8.5 Verifier Result↩︎

The verifier result has three cases:

\(\mathsf{Unsupported}\) matters because silently ignoring unknown evidence would be a soundness bug. If the checker cannot interpret an optional source-side feature, the certificate is not accepted as if that feature had been checked.

\(\mathsf{Accept}\), \(\mathsf{Reject}\), and \(\mathsf{Unsupported}\) are verifier results, not theorem-status labels. The verifier result here is an abstract source-side checker result, not a claim that a serialized certificate format, parser, or production verifier implementation has been proved correct.

8.6 What Accept Means, and What It Does Not Mean↩︎

\(\mathsf{Accept}\) means that, under faithful source observation, the evidence materializes a wellformed DBLog run whose scope, frontier, and clean prefix agree with the certificate. That is the bridge back to Layer 2.

\(\mathsf{Accept}\) does not mean that the database, connector, log, primary-key interpretation, source-coordinate semantics, concrete parser, wire format, or named product has been proved faithful by the certificate itself. It does not mean a sink applied the prefix. It does not mean the claim is whole-table. It does not remove the faithful-source-observation premise.

8.7 Faithful Source Observation↩︎

We write \(\mathsf{FSO}(E,b_0,H,\mathit{raw})\) for the faithful-source-observation assumption — the External observation assumption of the certificate layer. It ties the finite evidence bundle \(E\) to the mathematical source history \(H\) and base state \(b_0\), against a raw source- observation carrier \(\mathit{raw}\). In practical terms it covers:

• the source history and base state the certificate is about;

• the meaning and ordering of source-log coordinates;

• CDC retention and completeness over the certified interval;

• preservation of same-coordinate order and multiplicity where relevant;

• honesty of chunk-read values and absences at their recorded coordinates;

• the primary-key interpretation and the assumption that chunk reads observe committed source state.

The theorem statements write the raw source-observation carrier as \(\mathit{raw}\). \(\mathit{raw}\) is left abstract: it stands for whatever concrete record a deployment has of what the source emitted, interpreted by the faithful-source-observation assumption. It is not a destination log, not a sink-state proof, and not a claim that a named connector has been verified.

The certificate checker can compare evidence fields to one another. It cannot prove, from the certificate alone, that the outside world produced faithful observations. This is why the accepted-certificate theorem is Conditional and why faithful source observation is labelled as an External observation assumption.

8.8 Why This Layer Exists↩︎

The certificate layer is the bridge from operational artifacts to the theorem about replay equality. A wellformed run is the mathematical object Layer 2 needs. A certificate is the artifact DBLog can expose. The Layer 3 theorem says that accepted evidence gives enough of a bridge from the artifact to the mathematical run, under the visible trust boundary, for the source-side virtual-cut equality to follow.

Practitioner takeaway. A DBLog certificate is a finite, checkable claim object — scope, frontier, clean prefix — paired with an evidence bundle the checker inspects. Acceptance is an internal coherence verdict, not a proof that the connector, log, or parser is faithful: faithful source observation is part of every accepted-certificate claim, not a footnote to it. Evaluating a deployment means asking what its checker actually inspects and what it instead has to assume.

9 Accepted-Certificate Soundness (Layer 3)↩︎

Layer 3 gives the certificate-side theorem. It has two statements: an intermediate bridge theorem and the composed virtual-cut theorem.

9.1 Intermediate Theorem↩︎

The intermediate theorem is Conditional on the checker substrate: a small set of primitive obligations the abstract certificate checker must meet for acceptance to carry meaning. Table 7 lists them. They are stated as explicit assumptions; the paper does not prove a concrete parser, wire format, or production verifier discharges them.

Obligations S1–S4 are the conditional structure of the intermediate theorem: each is a property of the checker design from which an \(\mathsf{Accept}\) return licenses the theorem’s source-side conclusion. Table 7 carries no fifth row because Unsupported-evidence reporting is not part of that conditional list — it is a separate checker-design commitment, stated once outside the table.

Unsupported reporting. A checker meeting S1–S4 must also not accept evidence it cannot interpret as if it had been checked; uninterpretable evidence is reported \(\mathsf{Unsupported}\) rather than \(\mathsf{Accept}\). Status: Deployment obligation on the concrete checker, not a Layer 3 premise.

Under obligations S1–S4 the intermediate theorem is:

\[\begin{align} &\mathit{verify}(C,E)=\mathsf{Accept}\,\land\, \mathsf{FSO}(E,b_0,H,\mathit{raw})\\ &\quad\Longrightarrow\, \exists R.\; \mathsf{WF}(b_0,R,H) \,\land\, \mathsf{Coh}(C,E,R). \end{align}\]

In words: accepted evidence, when interpreted through faithful source observation, witnesses a wellformed abstract DBLog run whose accessors agree with the certificate. Obligations S1–S3 carry the materialization and accessor agreement, and S4 carries wellformedness. The Unsupported-reporting commitment stated after the table is what keeps uninterpretable evidence from being accepted as if it had been checked; it is operational, not part of the conditional list.

9.2 Composed Theorem↩︎

The headline certificate theorem is:

\[\begin{align} &\mathit{verify}(C,E)=\mathsf{Accept}\,\land\, \mathsf{FSO}(E,b_0,H,\mathit{raw})\\ &\quad\Longrightarrow\, \mathsf{VC}(C,H). \end{align}\]

Expanded:

\[\begin{align} &\mathit{verify}(C,E)=\mathsf{Accept}\,\land\, \mathsf{FSO}(E,b_0,H,\mathit{raw})\\ &\quad\Longrightarrow \mathit{apply}(\mathit{prefix}(C)) \mathbin{\upharpoonright}\mathit{scope}(C)\\ &\qquad= \mathit{src}(b_0,H,\mathit{frontier}(C)) \mathbin{\upharpoonright}\mathit{scope}(C). \end{align}\]

Reader-facing theorem summary:

• Status: Conditional — machine-checked under checker-substrate obligations S1–S4 (Table 7) and faithful source observation.

• Claim: an accepted certificate is a virtual-cut certificate when its evidence is interpreted through faithful source observation.

• Premises: checker-substrate obligations S1 (input wellformedness), S2 (materialization), S3 (accessor agreement), S4 (faithful materialization is wellformed); and faithful source observation of the evidence.

• Boundary: acceptance does not prove a concrete parser, wire format, production verifier, named product, whole-table claim, or sink application. The Unsupported-reporting commitment is a separate checker-design obligation, not part of the conditional list.

Here, Conditional means machine-checked under obligations S1–S4 and faithful source observation, not unproved or merely plausible.

This is the formal meaning of “an accepted DBLog certificate is a virtual-cut certificate.” The faithful-source-observation premise is part of the sentence, not a footnote. Acceptance alone is not a proof about the mathematical source history.

9.3 Proof Explanation↩︎

The proof composes the layers already introduced.

First, verifier acceptance and faithful source observation produce a witnessed run \(R\):

\[\begin{align} &\mathsf{WF}(b_0,R,H),\\ &\mathsf{Coh}(C,E,R). \end{align}\]

Second, Layer 2 applies to that wellformed run:

\[\begin{align} &\mathit{apply}(\mathit{prefix}(R)) \mathbin{\upharpoonright}\mathit{scope}(R)\\ &\qquad= \mathit{src}(b_0,H,\mathit{frontier}(R)) \mathbin{\upharpoonright}\mathit{scope}(R). \end{align}\]

Third, coherence substitutes certificate accessors for run accessors:

\[\begin{align} \mathit{scope}(C)&=\mathit{scope}(R),\\ \mathit{frontier}(C)&=\mathit{frontier}(R),\\ \mathit{prefix}(C)&=\mathit{prefix}(R). \end{align}\]

After substitution, the Layer 2 equality becomes:

\[\begin{align} &\mathit{apply}(\mathit{prefix}(C)) \mathbin{\upharpoonright}\mathit{scope}(C)\\ &\qquad= \mathit{src}(b_0,H,\mathit{frontier}(C)) \mathbin{\upharpoonright}\mathit{scope}(C). \end{align}\]

Fourth, Section 6’s definition folds that equality into \(\mathsf{VC}(C,H)\).

No sink premise appears in this proof. No whole-table premise appears in this proof. No named product premise appears in this proof. The proof is scoped to \(\mathit{scope}(C)\), source-side, and conditional on the checker substrate and faithful source observation.

9.4 Non-Vacuity and Boundary Cases↩︎

The certificate layer is not only a theorem statement. The paper also checks that the statement is meaningful:

• there is a nonempty accepted-certificate witness with a non-base frontier, a chunk read, a value-changing replay event, and faithful \(\mathit{raw}\)/\(b_0\)/\(H\) evidence;

• accepted-without-witness shapes are rejected by the checker-substrate obligations;

• wrong certificate/evidence binding is rejected;

• unknown source-side evidence is \(\mathsf{Unsupported}\) rather than silently accepted;

• mismatched certificate/run accessors fail coherence;

• unfaithful \(\mathit{raw}\), wrong \(b_0\), and wrong \(H\) fail faithful source observation;

• empty scope is a trivial boundary, not the positive witness.

These cases protect the main trust boundary. The theorem does not say that the certificate eliminates trust. It says that, under faithful source observation and explicit checker obligations, acceptance gives a coherent wellformed run; the already-proved source-side theorem then yields the certified virtual cut.

Practitioner takeaway. Rather than trusting a backfill pipeline end to end, a consumer can check a finite certificate against its evidence bundle. Acceptance is not self-authenticating: under explicit checker obligations it yields the virtual cut only given faithful source observation — that the captured evidence honestly reflects the real source — which no verifier can settle from inside the certificate.

10 Whole-Table Specialization (Layer 4)↩︎

Layers 2 and 3 prove a scoped result: the certified clean prefix reaches the source state at the certified frontier on \(\mathit{scope}(C)\). That is the right headline for ordinary DBLog certificates, because a backfill usually claims a finite key scope. That scope is in practice often the whole table or a whole shard, so the whole-table side conditions below are not an exotic case — they are what a typical full backfill must discharge. A whole-table statement needs more. It needs evidence that the claimed scope really covers every table key whose state could matter between a chosen anchor boundary and the certified frontier, and it needs the replay prefix not to mutate keys outside that claim.

The whole-table specialization is therefore a derived result, not a new meaning of certificate acceptance. Acceptance gives the scoped virtual cut. The additional side condition tells us when the restriction to \(\mathit{scope}(C)\) can be dropped.

10.1 Anchor Boundary and Anchor Domain↩︎

An anchor boundary \(b\) is a source coordinate used to name the table population the whole-table claim intends to cover. It is not a physical snapshot read. Chunks may be read after \(b\); the virtual-cut construction is precisely that stale chunk observations can be repaired by source-log evidence and replayed to the frontier.

For a certificate \(C\), the anchor must not be later than the certified frontier:

\[b \le \mathit{frontier}(C).\]

The anchor domain is the set of keys present in the source at that boundary:

\[\mathit{anchorDom}(H,b) = \{\,k \mid \mathit{src}(b_0,H,b)(k) \text{ is present}\,\}.\]

The anchor domain inherits its dependence on the base state \(b_0\) from \(\mathit{src}\). As with \(\mathit{src}\), \(b_0\) is a single base state fixed throughout the paper; we keep it implicit in \(\mathit{anchorDom}(H,b)\), and likewise in the whole-table claim scope \(\mathsf{WTS}(C,H,b)\) below, since it never varies. A key present at the anchor that no source event at or before \(b\) ever writes owes its anchor-domain membership entirely to \(b_0\) — the one place the base state does observable work in a whole-table claim.

Operationally, a whole-table deployment may use a maximum-primary-key or equivalent end-of-table witness to help show that the claimed scope covers this anchor domain. Such a witness does not replace \(\mathsf{WTS}\): it must be tied to the anchor boundary \(b\), or otherwise justify \(\mathit{anchorDom}(H,b) \subseteq \mathit{scope}(C)\). It also does not discharge the post-anchor touch condition below, including for keys beyond an anchor-time maximum.

Keys absent at \(b\) can still become relevant later. If the source inserts, updates, or deletes a key after \(b\) and at or before the certified frontier, the whole-table claim must account for that key too.

\(\mathit{touched}(H,b,f)\) is the set of keys \(k\) for which \(H\) has an insert, update, or delete at some source coordinate \(c\) with \(b < c \le f\), and the conservative interval table scope is \[\begin{align} &\mathit{tblScope}(H,b,f)\\ &\quad= \mathit{anchorDom}(H,b) \cup \mathit{touched}(H,b,f). \end{align}\]

This is a conservative event-touch scope. It is not a minimal semantic-difference set: even a delete of an already absent key is still a touch that the whole-table side condition can require the claim scope to cover.

10.2 A Small Anchor Example↩︎

Suppose the source contains keys \(100\) and \(200\) at anchor boundary \(b\). Between \(b\) and frontier \(f\), key \(300\) is inserted and key \(200\) is deleted.

\[\begin{align} \mathit{anchorDom}(H,b)&=\{100,200\},\\ \mathit{touched}(H,b,f)&=\{200,300\},\\ \mathit{tblScope}(H,b,f)&=\{100,200,300\}. \end{align}\]

A whole-table claim for this interval must include all three keys in \(\mathit{scope}(C)\). Key \(100\) is present at the anchor. Key \(200\) is present at the anchor and then deleted. Key \(300\) is absent at the anchor but inserted before the frontier. Omitting any of them would make the whole-table statement stronger than the evidence supports.

There is also a replay-side condition. If the certified clean prefix writes a bystander key \(999\) outside \(\mathit{scope}(C)\), then scoped equality over \(\{100,200,300\}\) may still be true, but whole-table equality is not justified: the replay has changed something outside the claimed table scope.

10.3 Whole-Table Claim Scope↩︎

We write \(\mathsf{WTS}(C,H,b)\) for the whole-table claim-scope side condition. It bundles four conjuncts:

\[\begin{align} &\mathsf{WTS}(C,H,b) \,\Longleftrightarrow\, b \le \mathit{frontier}(C)\\ &\,\land\, \mathit{anchorDom}(H,b) \subseteq \mathit{scope}(C)\\ &\,\land\, \mathit{touched}(H,b,\mathit{frontier}(C)) \subseteq \mathit{scope}(C)\\ &\,\land\, \mathit{keys}(\mathit{prefix}(C)) \subseteq \mathit{scope}(C). \end{align}\]

The first conjunct fixes the ordering of the anchor and frontier. The next two say that \(\mathit{scope}(C)\) covers every key present at the anchor and every key touched after the anchor through the frontier. The final conjunct says that the certified replay prefix does not write unclaimed keys. Figure 5 pictures the four conjuncts as nested key regions over the source-coordinate axis.

This predicate is explicit because whole-table correctness is not automatic. Certificate acceptance alone gives a scoped statement. The whole-table side condition is the extra bridge from “correct on the certified claim scope” to “correct on every table key”.

10.4 Whole-Table Theorem↩︎

Under certificate acceptance, faithful source observation, and the whole-table claim-scope side condition, the certified clean prefix reaches the source state at the certified frontier on the whole table:

\[\begin{align} &\mathit{verify}(C,E)=\mathsf{Accept}\,\land\, \mathsf{FSO}(E,b_0,H,\mathit{raw})\\ &\,\land\, \mathsf{WTS}(C,H,b)\\ &\,\Longrightarrow\, \mathit{apply}(\mathit{prefix}(C))=\mathit{src}(b_0,H,\mathit{frontier}(C)). \end{align}\]

Reader-facing theorem summary:

• Status: Conditional — machine-checked under checker-substrate obligations S1–S4 (Table 7), faithful source observation, and \(\mathsf{WTS}(C,H,b)\).

• Claim: the scoped certificate theorem lifts to whole-table source-state equality when the whole-table claim-scope side conditions cover boundary order, anchor-domain keys, post-anchor touches, and replay keys.

• Premises: certificate acceptance, faithful source observation, \(\mathsf{WTS}(C,H,b)\), and checker-substrate obligations S1–S4 (Table 7).

• Boundary: this remains source-side. It does not prove sink convergence, exactly-once delivery, or arbitrary destination correctness.

This is a Conditional source-side theorem. The certificate checker and faithful-source-observation assumption supply the certified scoped virtual cut; the whole-table side condition supplies the coverage needed to remove the scope restriction.

10.5 Proof Roadmap↩︎

Layer 3 gives the scoped equality:

\[\begin{align} &\mathit{apply}(\mathit{prefix}(C)) \mathbin{\upharpoonright}\mathit{scope}(C)\\ &\,= \mathit{src}(b_0,H,\mathit{frontier}(C)) \mathbin{\upharpoonright}\mathit{scope}(C). \end{align}\]

For keys inside \(\mathit{scope}(C)\), that is already the desired equality. For keys outside \(\mathit{scope}(C)\), the whole-table side condition does two jobs. The \(\mathsf{WTS}(C,H,b)\) inclusions \[\begin{align} \mathit{anchorDom}(H,b) &\subseteq \mathit{scope}(C), \\ \mathit{touched}(H,b,\mathit{frontier}(C)) &\subseteq \mathit{scope}(C), \\ \mathit{keys}(\mathit{prefix}(C)) &\subseteq \mathit{scope}(C) \end{align}\] contrapose to \(k \notin \mathit{scope}(C) \Rightarrow k \notin \mathit{anchorDom}(H,b)\), \(k \notin \mathit{scope}(C) \Rightarrow k \notin \mathit{touched}(H,b,\mathit{frontier}(C))\), and \(k \notin \mathit{scope}(C) \Rightarrow k \notin \mathit{keys}(\mathit{prefix}(C))\), which power the two cases. First, the \(b_0\)-aware anchor-domain definition makes absence outside the anchor domain mean absence at the anchor boundary, including keys from the base state. Together with \(b \le \mathit{frontier}(C)\) and no post-anchor touch through the frontier, this implies the key is absent from the source at the frontier. Second, because the key is outside \(\mathit{keys}(\mathit{prefix}(C))\), the clean prefix does not write it. Replay and source are therefore both absent outside \(\mathit{scope}(C)\). Combining the inside-scope and outside-scope cases gives unrestricted equality.

10.6 Boundaries↩︎

The specialization does not change the paper’s trust boundaries. It still depends on faithful observation of the source-side evidence. It does not prove that a concrete parser or production verifier implementation is correct. It does not prove sink-state convergence, exactly-once delivery, or arbitrary destination correctness. It also does not say that a virtual cut is a physical cut: the anchor is a source-coordinate boundary used for reasoning about table scope, not a single request-wide read timestamp.

Practitioner takeaway. A scoped certificate becomes a whole-table guarantee only when the claimed key scope covers every key present at the anchor boundary and every key touched between the anchor and the frontier — post-anchor inserts and deletes included — and the certified replay writes nothing outside that scope. Whole-table correctness is earned by discharging those side conditions; certificate acceptance alone does not grant it.

11 Source-Side Continuation and Restriction of Virtual Cuts↩︎

The theorem ladder so far certifies a virtual cut at one frontier. A certificate fixes a single frontier \(\mathit{frontier}(C)\) and proves replay equality there. But a DBLog deployment does not stop at that frontier. The backfill chunk loop is finite, and once it closes DBLog keeps running as ordinary change data capture, consuming source-log events as the source commits them. The certified virtual cut is therefore one observation of an ongoing process, not its end state.

This section proves two source-side algebra facts that connect point-in-time cuts into that ongoing process. Continuation across frontiers shows that a virtual cut at frontier \(f\) extends to a virtual cut at any later frontier \(f'\) by appending the faithful change-data segment the source committed in between. Restriction to a sub-scope shows that a virtual cut on a key scope \(K\) is also a virtual cut on any smaller scope. Together they make the informal reading precise: ongoing DBLog operation is a sequence of virtual cuts, each later cut obtained from an earlier one by appending a continuation segment.

The Future Work section (Section 14.3) lists continuation across frontiers and restriction to a sub-scope among the goals of a wider certificate-algebra program. This section discharges those two as machine-checked results; the remaining program — disjoint composition, concrete extended-certificate verification, and raw overlap/retry normalization — stays Future work. Every result here is source-side: each conclusion is again an \(\mathit{apply}\)-against-\(\mathit{src}\) equality on a scope, with no destination, replica, or delivery term.

Proof roadmap. Both theorems are proved pointwise per key. Continuation across frontiers rests on one new Layer 0 fact — the source state at a later frontier is fixed by the source state at the earlier frontier together with the events strictly between them (§5.6) — while restriction to a sub-scope is immediate from the per-key form of the virtual-cut equality. The section defines the continuation segment first, then proves the two theorems and a certificate-level corollary.

11.1 Continuation Segments↩︎

Continuation needs a precise object for “the change data the source committed between two frontiers.” We call it the continuation segment.

For a source history \(H\), a key scope \(K\), and source frontiers \(f \le f'\), the continuation segment for the half-open interval \((f,f']\) on \(K\) is built directly from the source history: keep every history event whose source coordinate \(c\) satisfies \(f < c \le f'\) and whose key lies in \(K\), in source order, and read each kept event as its CDC replay event. We write \(\mathsf{ContSeg}(H,K,f,f',\delta)\) for the predicate “\(\delta\) is that continuation segment.” By exact coverage, \(\delta\) contains exactly the change-data readings of the source events for keys in \(K\) on \((f,f']\) — no more, no less — preserving per-key order and multiplicity; this bidirectional equivalence between \(\delta\) and the source’s own interval events is what the predicate encodes by construction.

By construction, \(\mathsf{ContSeg}(H,K,f,f',\delta)\) entails \(f \le f'\): the predicate is false whenever \(f > f'\), independent of \(\delta\). Theorems whose premises include \(\mathsf{ContSeg}(H,K,f,f',\delta)\) therefore implicitly require \(f \le f'\); the order is not restated in their displayed formulas.

The interval is half-open because the coordinate convention is inclusive (Section 5.1): \(\mathit{src}(b_0,H,f)\) already reflects every event at coordinate \(f\), so a continuation starts strictly after \(f\) and runs through \(f'\) inclusive.

Defining the segment as the filtered source history, read as change data — rather than as “some list of CDC events between \(f\) and \(f'\)” — is deliberate. It fixes source order, same-coordinate source-position order, and event multiplicity by construction. A caller cannot present a segment that quietly reorders, drops, or duplicates the source’s own events; any such list simply fails to be \(\mathsf{ContSeg}(H,K,f,f',\delta)\). That a real CDC feed delivers exactly this segment is an External observation assumption, with a matching Deployment obligation to retain the source-log interval \((f,f']\) — the same trust boundary the certificate layer already names for chunk reads, now applied to the continuation.

The segment is filtered to the scope \(K\): it is the change data for the keys of \(K\), not the source’s entire change stream. A deployment whose CDC feed carries all keys must project that stream onto \(K\) to obtain the continuation segment for a \(K\)-scoped cut; for a whole-table continuation the scope is the universal key set, and the whole-table continuation result below is the form to use. The exactness cuts two ways. A segment that drops, reorders, or duplicates an in-scope event is not \(\mathsf{ContSeg}(H,K,f,f',\delta)\) and the continuation does not hold — these are the proof-critical clauses. A segment padded with an out-of-scope event also fails \(\mathsf{ContSeg}\), but that rejection is evidence-shaping discipline rather than soundness: the scoped equality constrains only the keys of \(K\).

11.2 Continuation Across Frontiers↩︎

The primary theorem of this section continues a virtual cut to a later frontier. Let \(H\) be a wellformed source history. If \(\sigma\) is a virtual cut at frontier \(f\) on scope \(K\), and \(\delta\) is the continuation segment for \((f,f']\) on \(K\), then \(\sigma\) followed by \(\delta\) — sequence concatenation, written \(\sigma \mathbin{@} \delta\) — is a virtual cut at the later frontier \(f'\) on the same scope:

\[\begin{align} &H \text{ wellformed} \,\land\, \mathsf{VCS}(\sigma,K,f,H)\\ &\,\land\, \mathsf{ContSeg}(H,K,f,f',\delta)\\ &\,\Longrightarrow\, \mathsf{VCS}(\sigma \mathbin{@} \delta, K, f', H). \end{align}\]

Reader-facing theorem summary:

• Status: Conditional — machine-checked under the displayed premises.

• Claim: appending the faithful continuation segment for \((f,f']\) carries a virtual cut at \(f\) to a virtual cut at \(f'\) on the same scope.

• Premises: \(H\) is a wellformed source history; \(\sigma\) is a virtual cut at \(f\) on \(K\); and \(\delta\) is exactly the continuation segment for \((f,f']\) on \(K\).

• Boundary: the conclusion is a replay-against-source equality on \(K\). It is not a whole-table claim, not a statement that a verifier accepts an extended certificate, and not a destination-apply claim.

The wellformedness premise is not decorative. The proof needs the source history’s coordinate order to know that the events in \((f,f']\) are exactly the ones between the two frontiers; without it the interval could interleave with events outside it.

Proof idea. The argument is pointwise on a key \(k \in K\). Replay of a sequence at \(k\) is fixed by the latest replay event for \(k\). If the continuation segment \(\delta\) carries an event for \(k\), then the latest \(k\)-event of \(\sigma \mathbin{@} \delta\) lies in \(\delta\) and is the change-data reading of the latest source event for \(k\) in \((f,f']\); a Layer 0 source-state interval lemma equates that event’s effect with \(\mathit{src}(b_0,H,f')\) at \(k\). If \(\delta\) carries no event for \(k\), replay of \(\sigma \mathbin{@} \delta\) at \(k\) equals replay of \(\sigma\) at \(k\), which the premise equates with \(\mathit{src}(b_0,H,f)\) at \(k\); the same interval lemma equates that with \(\mathit{src}(b_0,H,f')\) at \(k\), because no event for \(k\) in the interval means the source state for \(k\) does not change across it. The interval lemma — that \(\mathit{src}\) at \(f'\) is determined by \(\mathit{src}\) at \(f\) together with the source events in \((f,f']\) — is the one new Layer 0 fact the continuation needs; it is proved from the source-coordinate order.

Whole-table continuation. The whole-table specialization (Section 10) delivers, under its claim-scope side conditions, the unrestricted equality \(\mathit{apply}(\sigma) = \mathit{src}(b_0,H,f)\). Continuation specializes to that case: for a wellformed \(H\), if \(\mathit{apply}(\sigma) = \mathit{src}(b_0,H,f)\) holds on every key and \(\delta\) is the continuation segment for \((f,f']\) on every key, then \(\mathit{apply}(\sigma \mathbin{@} \delta) = \mathit{src}(b_0,H,f')\). This is the all-keys instance of the theorem above, Conditional on the same premises. It does not let a scoped continuation become whole-table for free: a key the source inserts outside \(K\) within \((f,f']\) changes the table while leaving the scoped equality on \(K\) intact. Whole-table continuation requires the continuation segment for every key, just as whole-table specialization requires its claim-scope side condition.

11.3 Restriction to a Sub-Scope↩︎

A virtual cut also restricts downward along the scope. If \(\sigma\) is a virtual cut at frontier \(f\) on scope \(K\), then it is a virtual cut at \(f\) on every sub-scope \(K' \subseteq K\):

\[\mathsf{VCS}(\sigma,K,f,H) \,\land\, K' \subseteq K \,\Longrightarrow\, \mathsf{VCS}(\sigma,K',f,H).\]

This is Conditional and premise-bearing: it holds for any \(K' \subseteq K\), and the \(K' \subseteq K\) premise is exactly what it needs. Restriction is one-directional. Widening a scope is unsound: for a key outside \(K\) the cut certifies nothing about that key’s state at \(f\), so there is no sound lemma carrying a cut from \(K\) to a larger scope.

The same fact holds through a certificate’s accessors. If \(C\) is a certificate with \(\mathsf{VC}(C,H)\) and \(K' \subseteq \mathit{scope}(C)\), then the certified clean prefix is a virtual cut at \(\mathit{frontier}(C)\) on the narrowed scope \(K'\):

\[\begin{align} &\mathsf{VC}(C,H) \,\land\, K' \subseteq \mathit{scope}(C)\\ &\quad\Longrightarrow\, \mathsf{VCS}\bigl(\mathit{prefix}(C),K',\mathit{frontier}(C),H\bigr). \end{align}\]

This restricts the equality a certificate already witnesses to a smaller scope. It is not a claim that a verifier accepts a restricted certificate: producing and accepting a concrete certificate for \(K'\) is an evidence-and-verifier obligation, not a consequence of the algebra.

11.4 Continuation Over an Accepted Certificate↩︎

Continuation composes with the certificate layer. Layer 3 (Section 9) proves that an accepted certificate, under faithful source observation, witnesses a virtual cut at \(\mathit{frontier}(C)\) on \(\mathit{scope}(C)\). Appending a continuation segment carries that cut forward. Let \(H\) be a wellformed source history. If a certificate \(C\) is accepted under faithful source observation, and \(\delta\) is the continuation segment for \((\mathit{frontier}(C),f']\) on \(\mathit{scope}(C)\), then the certified clean prefix followed by \(\delta\) is a virtual cut at \(f'\) on \(\mathit{scope}(C)\):

\[\begin{align} &\mathit{verify}(C,E)=\mathsf{Accept}\,\land\, \mathsf{FSO}(E,b_0,H,\mathit{raw})\\ &\,\land\, H \text{ wellformed}\\ &\,\land\, \mathsf{ContSeg}\bigl(H,\mathit{scope}(C),\mathit{frontier}(C),f',\delta\bigr)\\ &\,\Longrightarrow\, \mathsf{VCS}\bigl(\mathit{prefix}(C) \mathbin{@} \delta, \mathit{scope}(C), f', H\bigr). \end{align}\]

Reader-facing theorem summary:

• Status: Conditional — machine-checked under checker-substrate obligations S1–S4 (Table 7), faithful source observation, source-history wellformedness, and exact continuation on \((\mathit{frontier}(C),f']\).

• Claim: an accepted certificate’s virtual cut continues, by appending a faithful continuation segment, to a virtual cut at a later frontier.

• Premises: certificate acceptance under checker-substrate obligations S1–S4 (Table 7) and faithful source observation, as in Layer 3; a wellformed source history; and a continuation segment that is exactly the source’s change data on \((\mathit{frontier}(C),f']\).

• Boundary: the conclusion is a replay equality on the sequence \(\mathit{prefix}(C) \mathbin{@} \delta\). It is not a claim that the verifier accepts an “extended certificate”: acceptance for the longer prefix remains an evidence-and-verifier obligation.

The continuation segment \(\delta\) is itself an external observation of the source; its faithfulness to \(H\) is a premise discharged at deployment, exactly as the certificate’s own evidence is. The theorem composes the Layer 3 certificate theorem with continuation across frontiers; it adds no new trust to either.

11.5 Ongoing Operation as a Sequence of Cuts↩︎

Continuation segments chain. For a wellformed source history, the continuation segment for \((f,f']\) followed by the continuation segment for \((f',f'']\) is the continuation segment for \((f,f'']\). Wellformedness is again required: only a non-decreasing source history guarantees that the two coordinate ranges meet at \(f'\) without interleaving. Chaining is what licenses the informal picture — a finite prefix of ongoing change data is a fold of continuation segments, and a virtual cut can be advanced one segment at a time or many at once with the same result.

This is the precise source-side sense in which DBLog’s replay-equivalence claim can be advanced across frontiers rather than treated as a one-shot backfill claim. The certified virtual cut is point-in-time, but the point can be moved: each later frontier the source reaches is again a virtual cut, witnessed by the original cut extended with the change data in between.

Re-chunking and re-running. The same algebra explains what a fresh DBLog run produces. A virtual cut at \((K,f)\) is determined by the source state \(\mathit{src}(b_0,H,f)\) alone: any two replay sequences that are virtual cuts at \((K,f)\) agree on \(K\), because both equal that one source state there. So a fresh wellformed run — or a fresh accepted certificate, under the Layer 2 and Layer 3 theorems already proved — regenerates the same absolute source-side virtual cut on its scope, independent of any earlier cut and independent of any replica’s state. Re-chunking is therefore an absolute, source-determined reconstruction of the per-key state — the regenerated clean prefix need not be the same event sequence, but replaying it reaches the same source state — not a differential repair against a destination. Whether a destination then applies the regenerated prefix is a separate, sink-side question, which Section 12 keeps a Non-claim.

11.6 Boundaries↩︎

The continuation and restriction results do not move the paper’s trust boundaries. Each conclusion is a source-side \(\mathit{apply}\)-against-\(\mathit{src}\) equality. They depend on faithful observation of the source-log evidence: the continuation segment must be the source’s real change data on the interval, which is an External observation assumption with a Deployment obligation to retain that interval. They prove no whole-table claim beyond the explicit all-keys instance, no acceptance of an extended or restricted certificate, and no destination-state convergence. “Continuation across frontiers” and “restriction to a sub-scope” move from Future work to machine-checked Conditional results; the rest of the certificate-algebra program does not.

Practitioner takeaway. A certified virtual cut is a point-in-time object, but the point is not fixed: appending the source’s change data for \((f,f']\) carries a cut at \(f\) to a cut at \(f'\), so ongoing DBLog operation is a sequence of virtual cuts rather than a single one. A virtual cut also narrows to any sub-scope, never widens. And because a cut is fixed by the source state alone, a fresh wellformed run regenerates the same absolute cut — re-running a backfill is an absolute reconstruction, not a repair that depends on what a destination currently holds.

12 Sink-State Convergence (Non-Claim)↩︎

The theorem ladder through Layer 4 is source-side. It tells us what the certified replay prefix means with respect to the source database at the certified frontier. It does not, by itself, tell us what state a downstream destination has reached.

This distinction is easy to lose because replication systems often talk about ACKs, durable logs, and applied state in the same operational breath. This paper keeps them separate.

12.1 Receipt ACK↩︎

A destination ACK says that some material was received. It does not say that the destination applied that material, applied it in order, applied it idempotently, applied it only once, or reached the source state at the certified frontier. ACK-as-receipt can support a future stream-correctness story, but it is a Non-claim for sink-state correctness in this paper.

12.2 Durable Audit-Log Persistence↩︎

A destination may durably record the certified clean prefix together with a run id, scope, frontier, or digest. That is useful: it gives an auditable record of what arrived. But durable receipt is still stream-level evidence, not state-level evidence. A log can contain the right events while the destination table has not applied them or has applied them under different semantics.

12.3 Applied-State Evidence↩︎

To prove destination state convergence, a future layer would need a sink model: ordering, idempotence, fencing, visible apply barriers, and a way to observe that the destination state after the barrier corresponds to applying the certified clean prefix. That is a separate theorem surface. In this paper it is Future work by default.

Even that future theorem would be scoped. Schematically (where \(\mathit{sinkState}\) is a placeholder for the future sink-state accessor; this paper does not formalize such an accessor):

\[\mathit{sinkState}\mathbin{\upharpoonright}\mathit{scope}(C) = \mathit{src}(b_0,H,\mathit{frontier}(C)) \mathbin{\upharpoonright}\mathit{scope}(C).\]

Whole-table sink convergence would additionally need the whole-table side conditions from Section 10. There is no path from “DBLog accepted a certificate” to “the whole destination database is correct” without both the source-side certificate theorem and a separate sink contract.

Practitioner takeaway. A certified virtual cut is a source-side object: it says replay equals the source at the frontier on the scope. It does not say your destination has applied that replay — an ACK means received, not applied; a durable log means recorded, not applied. A guarantee about the destination table’s state needs a fenced, idempotent sink with a visible apply barrier, supplied and verified separately. DBLog does not grant it.

13 Related Work↩︎

DBLog sits between several bodies of work that usually meet only in production systems: change-data-capture platforms, distributed cuts and frontiers, stream-processing watermarks, database recovery, and formal certificate discipline. This section is organized by concept rather than by product. Named systems give positioning and deployment context; theorem authority remains with this paper’s definitions and proofs.

13.1 DBLog Mechanism Lineage and Production Adopters↩︎

The original DBLog work [1] introduced the watermark-based CDC backfill mechanism: online primary-key chunk reads are bracketed by source watermarks, chunk rows become refresh events, ordinary CDC events fill the log gaps, and stale refresh rows are suppressed when newer log evidence dominates them. This paper treats that mechanism as the seed and develops the formal object it produces: the certified virtual cut. The formal model takes the canonical, non-overlapping chunk partition; the original mechanism’s retried or overlapping chunk reads must first be normalized into that canonical form, and that normalizer is itself left as Future work (Section 14.3).

Debezium [2] and Apache Flink CDC [3] include DBLog-style mechanisms in open-source CDC deployments. Debezium provides incremental snapshot modes, including signaling-table watermarks and read-only variants based on observed source coordinates such as MySQL GTIDs [5], MariaDB GTIDs [6], or PostgreSQL log sequence numbers (LSNs) [7]. Apache Flink CDC combines Debezium-style connectors with Flink’s checkpointed streaming runtime [8], including parallel chunk readers.

Those systems are deployment relatives, not theorem instances by name. This paper does not claim that Debezium or Apache Flink CDC satisfies the theorem without checking the deployment’s source-log retention, watermark or coordinate semantics, frontier discipline, and faithful source observation.

13.2 Cuts, Frontiers, Watermarks, and Checkpoints↩︎

The phrase “virtual cut” deliberately echoes the distributed-systems language of logical time and consistent cuts. Lamport’s logical clocks [9], Chandy-Lamport snapshots [10], Mattern’s virtual time [11], Fidge’s vector clocks [12], and Pu’s on-the-fly consistent reading [13] are the nearest theoretical neighbors.

A DBLog virtual cut is not a global consistent cut over all processes. It is an extensional replay-equality statement: replaying a certified prefix yields the source state at a frontier on a key scope. The ordering substrate is a source-history coordinate, not a vector-clock model of inter-process channels. Each cut is point-in-time, fixed to one frontier, but the cuts chain: the source-side continuation result (Section 11) advances a cut from one frontier to a later one, so a DBLog run corresponds to a sequence of source-side virtual cuts rather than a single one.

Stream-processing systems use adjacent terms. The Dataflow model [14] popularized event time and watermarks; Naiad [15] uses frontiers as progress markers; Flink’s asynchronous snapshots [8] checkpoint operator state for recovery. DBLog’s watermarks are source evidence around chunk reads, and \(\mathit{frontier}(C)\) is the source-history boundary for replay equality. It is not a stream-processing checkpoint of operator state, and it is not an exactly-once processing claim.

13.3 CDC Infrastructure and Source-Log Semantics↩︎

Three infrastructure groups provide the comparison surface. Durable transport and coordination systems such as LinkedIn Databus [16], Facebook Wormhole [17], Kafka [18], Kafka Connect JDBC [19], and ZooKeeper [20] show the operating environment for CDC backfills, but they do not export the certificate object proved here. Source-database documentation for MySQL binary logs and GTIDs [5], PostgreSQL logical decoding [7], PostgreSQL logical replication [21], and MariaDB GTIDs [6] identifies the source-log ordering and row-event semantics a deployment must establish for faithful source observation. Database-native and cloud CDC systems — PostgreSQL logical replication [21], CockroachDB changefeeds [22], AWS DMS [23], GCP Datastream [24], Oracle GoldenGate [25], Striim [26], Materialize’s PostgreSQL ingestion [27], Databricks Lakeflow [28], and Microsoft SQL Server CDC [29] — sit in the broader “initial load plus change stream” family. The safe comparison is this: these systems show that the operational shape is real and widely deployed; this paper contributes a finite replay-equivalence certificate for the DBLog-style version of that shape — one checkable against an evidence bundle under explicit source-observation assumptions.

CockroachDB resolved timestamps give a close production analogue to a source frontier, and PostgreSQL logical replication illustrates the initial-copy-plus-ordered-change-stream pattern; in this paper, neither is treated as exporting the finite, scoped evidence bundle required for a virtual-cut certificate.

13.4 Recovery, Snapshots, Isolation, and Live Backfill↩︎

A database reader may hear “snapshot” and think of recovery snapshots, MVCC read views, or point-in-time recovery. That is not this paper’s object. ARIES [30] and PostgreSQL PITR [31] reconstruct database state from checkpoints and logs. CALC [32] shows that database systems can construct logically consistent checkpoints without conventional synchronous physical checkpointing. Consistent with the theoretical-follow-up framing of §1, the paper is not a firstness claim about asynchronous checkpoint construction or avoiding physical snapshots; its narrower contribution is a scoped, source-side replay-equivalence certificate for a DBLog-style backfill — whose clean replay prefix equals source state at a named frontier, and which the continuation result carries to later frontiers — under explicit source-observation assumptions. Berenson et al. [33], Adya et al. [34], and Oracle Flashback [35] belong to the transaction-isolation and as-of-read tradition.

DBLog is not a recovery algorithm, an online backup mechanism, an MVCC snapshot, or a snapshot-isolation transaction. It does not assert that all chunk reads happened at one source timestamp. It asserts replay equality at a chosen frontier on a chosen scope.

Online schema migration tools such as gh-ost [36], F1 online schema change [37], and lazy schema migration systems [38] share the operational pressure of copying or rewriting data while writes continue. Their overlap with DBLog is live backfill under concurrent writes. Their difference is the formal target: this paper is about certifying source-side replay equality for a DBLog-style backfill and its frontier advancement, not about schema-state transitions or table swaps.

13.5 Certificate Discipline↩︎

The certificate layer is closest in spirit to checkable evidence under explicit assumptions. Refinement mappings [39], proof-carrying code [40], translation validation [41], version certificate recovery [42], and VerIso [43] all help position the idea of a finite object that witnesses correctness relative to a model. Large mechanized artifacts such as seL4 [44], CompCert [45], TLA+ [46], Verdi [47], IronFleet [48], and Alloy [49] are cited for discipline and comparison, not as theorem sources.

A DBLog certificate is not self-authenticating proof-carrying code, not a sink refinement map, and not an isolation-level conformance certificate. It is checkable evidence that, under faithful source observation, witnesses a wellformed DBLog run and therefore a virtual cut.

13.6 Title-Promise and Product-Claim Boundaries↩︎

“Snapshot-equivalent replay” is intended literally but narrowly. A DBLog virtual cut is not a physical snapshot read, not a database snapshot-isolation read view, not PITR, not a stream-processing checkpoint, not a product replication guarantee, and not sink-state correctness. The short safe form is: DBLog constructs a snapshot-equivalent replay certificate without requiring a single physical snapshot read.

The paper also avoids product-by-name theorem transfer. It does not say that Debezium, Apache Flink CDC, MySQL, PostgreSQL, MariaDB, or any other named system is a theorem instance here. A named deployment can become a theorem subject only after its source-side assumptions, evidence semantics, and checker obligations are stated and proved or accepted as explicit deployment obligations.

Practitioner takeaway. DBLog’s neighbors — consistent cuts, stream-processing watermarks, CDC platforms, recovery snapshots, and certificate disciplines — each share one facet of the mechanism without the formal object this paper proves. The practical reading is that a named CDC product is a deployment relative, not a theorem instance: what carries over is the evidence discipline, and only once that product’s source-log, coordinate, and observation assumptions have been checked against the ones stated here.

14 Future Work↩︎

This paper proves the source-side certified virtual-cut story through the whole-table specialization, together with a first fragment of the certificate algebra beyond it — continuation across frontiers and restriction to a sub-scope (Section 11). Several further extensions are intentionally left as Future work. Listing them here is not a promise that they already hold; it is a map of the proof work needed to make them current claims.

14.1 Production Instantiation Paths↩︎

Debezium read-only mode would replace source watermark writes with observed source-coordinate witnesses: MySQL executed-GTID-set advance, PostgreSQL LSN advance, or related source-log observations. A future theorem would need a refinement showing that such observed-coordinate brackets provide the same clean-prefix obligations as written watermarks, under an explicit coordinate advancement assumption.

Apache Flink CDC parallel chunk execution would require a parallel chunk-plan model, per-worker recovery assumptions, and a theorem connecting checkpointed parallel execution to the same abstract wellformed run used in this paper. The key question is not whether Flink can run chunks in parallel; it is how the certificate records enough evidence to recover the single clean prefix that the proof consumes.

SELECT-at-LSN and source-positioned witness modes would replace low/high watermark intervals with a point witness: the source coordinate at which a chunk read’s row image is known to hold. These modes are attractive because they can avoid source writes, but they need new source-side assumptions and a new verifier story for the point witness.

14.2 Sink Extensions↩︎

The destination-side sink extensions are Future work and are not a continuation of the source-side proof ladder.

ACK-only stream correctness would study receipt of the certified stream prefix. An ACK can support a theorem about receipt, but it remains a Non-claim for applied destination state. The future proof would need a sink-receipt model and a stream-prefix equality theorem.

Strong sink barrier convergence would study the applied-state theorem operators often want. It needs a separate fenced and idempotent sink contract, visible apply-barrier evidence, and a proof that the destination state after the barrier realizes the certified clean prefix. It is not a consequence of the accepted-certificate theorem or the whole-table specialization by itself.

These two sink extensions should be read as sibling Future work paths, not as entailments: ACK-only receipt could support stream-prefix correctness, but it would not establish applied-state convergence without a fenced, idempotent apply contract and visible barrier evidence.

14.3 Certificate Algebra and Model Extensions↩︎

This paper proves two source-side algebra facts for virtual cuts (Section 11): restriction to a sub-scope and continuation across later source frontiers by faithful CDC segments. The remaining certificate-algebra program, including disjoint composition, concrete extended-certificate verification, and raw overlap/retry normalization, remains Future work.

Real deployments also need a raw overlap/retry normalizer theorem. The current Layer 1 model uses a strict canonical chunk partition. A future normalizer would take overlapping or retried raw chunk reads and produce a canonical strict-partition certificate plus residual obligations, then prove that acceptance after normalization preserves the same virtual-cut claim.

Finally, some notation and layer-boundary choices remain Future work. A future paper might expose \(\mathit{prefix}(C,E)\) instead of \(\mathit{prefix}(C)\), use a relation form such as \(\mathit{certifiesPrefix}\), or move overlap/retry concepts into Layer 1 instead of treating them through certificate materialization. Those changes would affect the public theorem surface and should not happen as silent notation churn.

15 Verification Methodology↩︎

The paper uses six status labels, and only these six:

• Proved

• Conditional

• Deployment obligation

• External observation assumption

• Future work

• Non-claim

Proved means the definitions, theorem statement, assumptions, and proof explanation appear in the paper body, and the proof has also been mechanically checked. The reader should be able to follow the argument in the paper without opening the checked development. In this paper no headline theorem reaches Proved: each is Conditional on premises stated where it appears, so Proved is part of the fixed vocabulary but is not applied to a result here.

Conditional means the result is proved under premises stated in the paper. The important premises in this paper are the DBLog wellformed-run obligations, checker obligations, whole-table side conditions, and faithful source observation.

Deployment obligation means a condition the operator or system configuration must establish: retained CDC, source-coordinate ordering, watermark or coordinate-witness discipline, frontier selection, chunk scope, and similar operational facts.

External observation assumption means the model relies on source-side observations being faithful to the real source: primary-key interpretation, CDC retention and row-image semantics, source-coordinate ordering, and the observation of committed source state during chunk reads. These facts cannot be proved inside the abstract model; they must be established by the deployment and the source connector.

Future work means a named follow-up, not a theorem in this paper. Non-claim means a boundary the paper deliberately refuses to prove or imply.

The methodology is deliberately two-channel. The paper itself carries the reader-facing definitions, theorem statements, proof roadmaps, and boundary cases. Separately, each formal object in the paper is cross-checked against a machine-checked companion development. The companion development validates the formal spine; it does not replace the explanations in the paper. Phrases such as “validated elsewhere” are not substitutes for a body-visible proof argument.

16 Conclusion↩︎

DBLog was introduced for a practical task: capture a copy of a live source table — or a chosen key scope of it — while it keeps taking writes, with no lock and no global read transaction. This theoretical follow-up asks what correctness object that operation honestly exposes. The answer is not a disguised physical cut. It is a certified virtual cut: a finite replay certificate whose clean prefix, at a chosen frontier and scope, has the same per-key outcome as the source. In the paper’s safe form, DBLog constructs a snapshot-equivalent replay certificate without requiring a single physical snapshot read.

The main technical move is to make freshness a per-key replay property rather than a hidden snapshot timestamp. For each claimed key, the last relevant replay item is either the latest faithful source-log event through the frontier, or a chunk-refresh value or absence that was honest at its read coordinate and not superseded before the frontier. That is why the premises are load-bearing: source ordering, retained CDC coverage, chunk-read coordinates, frontier discipline, same-coordinate order, and canonical chunk ownership let the replay’s latest event match the source’s.

The certificate theorem changes the question from “did the system take the right snapshot?” to “does this evidence justify the replay claim?” Its answer is Conditional. Acceptance must bind the certificate to coherent evidence and to the run whose scope, frontier, and clean prefix it names; faithful source observation must connect that evidence to the real source history. A certificate can reject incoherent evidence, but it cannot prove from itself that the connector, coordinate semantics, and row images it reports are faithful. Source-log retention, coordinate discipline, and frontier selection each remain a Deployment obligation; the source-observation boundary remains an External observation assumption.

The same discipline keeps the negative space visible. Whole-table equality is a derived source-side specialization, not a free consequence of acceptance. Destination ACKs are receipt evidence, not applied-state evidence; strong sink-state convergence, exactly-once delivery, concrete parser or verifier correctness, and product-by-name transfer remain outside the current theorem surface, with sink convergence left as Future work. The contribution is precision: where operators had an informal snapshot-equivalence intuition about a live CDC backfill, there is now a finite object — the certified virtual cut — and a machine-checked theory of exactly when its replay equals the source. The object is not terminal: the backfill bootstraps the first virtual cut, and faithful CDC continuation advances it as the source frontier moves, so ongoing DBLog operation is a frontier-indexed sequence of source-side replay-equivalence claims. That is the paper’s precise replacement for the operational intuition that DBLog-style systems fuse initial load and change capture into one process — an account that operators and theory readers can finally share.

Formal Development and Tools↩︎

The paper’s formal definitions and its named theorem ladder are formalized and machine-checked in the Isabelle/HOL proof assistant. The machine check covers the proofs under the assumptions stated in the paper; it does not, and cannot, discharge the Deployment obligations or the External observation assumption, which remain conditions a deployment must establish. Its role is to guard against drift between the paper and the mechanization, not to certify that any deployment satisfies the premises. The formal development is publicly archived as the Zenodo deposit [50] (https://doi.org/10.5281/zenodo.20389697).

AI assistance. During the preparation of this work the author used the generative AI assistants ChatGPT 5.5 (OpenAI) and Claude Opus 4.7 (Anthropic) to support drafting and revising the exposition and developing the Isabelle/HOL formalization. The author directed the research, reviewed and edited all resulting text, and checked every definition, theorem statement, and proof. The author is the sole author of this paper and takes full responsibility for its content; the AI assistants are tools, not authors.

References↩︎