This paper is a theoretical follow-up to the 2020 DBLog paper, which described a change-data-capture (CDC) mechanism for 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 is now adopted by Debezium and Apache Flink CDC. The 2020 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 requiring 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 asserts no single 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 two source-side algebra facts: on the same scope, a cut advances to later frontiers by appending the scope-filtered faithful CDC segment committed in between, and a cut restricts to sub-scopes. Each result is Conditional on premises stated where it 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.

翻译：本文是2020年DBLog论文的理论续作，该论文描述了一种变更数据捕获机制，用于从活跃的源数据库中回填下游系统并持续流式传输其变更，同时源数据库持续接受写入操作。DBLog通过主键范围扫描（数据块）读取数据库表，并与源变更日志交错执行：水位线在日志顺序中定位每个数据块，数据块行变为刷新事件，而CDC事件修复陈旧的数据块观测结果。该机制无需表锁、无需暂停写入操作、无需全局读取事务，现已被Debezium和Apache Flink CDC采用。2020年论文从操作层面描述了该机制，但未形式化其正确性目标。本文形式化了该目标：DBLog在不依赖单个物理快照读取的情况下构建了快照等价回放证书。核心形式化对象是认证虚拟切割：一种有限证据包，其认证回放能够在所选键范围与所选前沿上达到与源数据库一致的逐键状态。虚拟切割是外延性的：其本质是前沿上的回放等价性，而非物理快照读取，且不宣称数据块行间存在统一的源时间戳。本文证明了每个构造良好的DBLog运行在其前沿与作用域上满足逐键回放等价性，且通过忠实源观测评估的已接受证书能佐证此类运行并产生虚拟切割。本文还证明了两个源端代数性质：在同一作用域上，通过追加作用域过滤的忠实CDC段（即两次切割间提交的变更），切割可延展至更晚的前沿；切割可限制至子作用域。每条结论均基于其出现位置所声明的先决条件。全表正确性、恰好一次投递、下游状态收敛性及其向命名部署的迁移并非仅凭证书接受即可推导的结论。所有证明均在Isabelle/HOL中经过机器检验。