Repository navigation
[Quality] Correctness prevention: SQL semantics, lifecycle testing and bounded Verus proofs #1225
Description
Recent correctness reports motivate a focused follow-up to the existing quality work: expand the semantic cases tests can reach, strengthen what a passing test establishes, exercise recovery histories, and add small production-used Verus proofs.
This issue tracks proposed quality improvements from the October 22 research review. It does not claim new runtime reproductions, reopen the entire historical Verus roadmap, or make every future proof an immediate release gate.
Work items and recommended order
First: strengthen executable tests
- [Quality] Expand DVM generators and regression coverage for PostgreSQL semantic boundaries #1217 — Expand SQL-semantic generators and permanent regressions: composite NULLs, three-valued transitions, exceptional values, evaluation protection, histories and consumer order.
- [Quality] Strengthen result oracles, negative controls and changed-data execution witnesses #1218 — Strengthen result observations, expected negative-control failures, changed-data route witnesses and local semantic mutants.
- [Quality] Add bounded lifecycle and deterministic concurrency tests for recovery #1219 — Add bounded lifecycle histories and witnessed concurrency/recovery schedules using existing Testcontainers barriers.
Next: deliver proofs in bounded production slices
- [Quality][Verus] Verify production predicate visibility and aggregate lifecycle decisions #1220 — First proof pilot: predicate visibility and aggregate lifecycle decisions.
- [Quality][Verus] Verify CDC normalization and observation-safe change elision #1221 — CDC normalization and observation-safe change elision, including protected consumer windows.
- [Quality][Verus] Verify receipt batching, cleanup eligibility and recovery transitions #1222 — Receipt batch completeness, cleanup eligibility and recovery transitions.
- [Quality][Verus] Verify a restricted join plan checker with snapshot and expression safety #1223 — Restricted join-plan checking with snapshot provenance and expression safety.
- [Quality][Verus] Verify bounded row-identity framing and encoding #1224 — Lower-priority row-identity framing and bounded encoding.
This is a prioritization recommendation, not a serial execution requirement. The SQL tests and protocol tests provide runtime evidence for the corresponding proof slices. The source-to-SQL and database boundaries must remain visible even after a proof passes.
Relationship to existing work
- bug(dvm): COUNT(composite) drops non-NULL records containing NULL fields #1203, bug(dvm): aggregate FILTER evaluates excluded arguments and raises errors #1204, bug(dvm): HAVING UNKNOWN transition leaves stale group after differential refresh #1205, bug(dvm): deleting numeric Infinity corrupts differential SUM with NaN #1209, bug(cdc): numeric scale changes are lost by equality-based changed_cols mask #1210 and bug(dvm): inner JOIN delta evaluates invalid cross-snapshot predicates #1211 retain ownership of the six reports in BUG: Several correctness issues in differential refresh #1201. Reuse their regressions; these quality issues target broader prevention.
- bug: WAL UPDATE-to-NULL retains the old decoded column value #1172–Scheduler pause can report drained while an inline refresh is still active #1187 provide additional lifecycle/capture leads with their existing evidence and confirmation status. A source-supported report is not automatically a reproduced defect.
- [Quality] Trustworthy results, recovery, and releases #1090 narrowed the previous quality program; Epic: [Verus] Deliver production-connected verified correctness in safe slices #1056 and its historical proof issues were deferred, not all implemented. The new issues revisit explicitly bounded opportunities prompted by the recent reports.
- ci: rebalance PR correctness coverage across component, E2E, and nightly tiers #1188 owns CI allocation work. Current CI already runs execution-backed DVM component tests. Extend those tests for cheap semantic combinations, retain installed-extension coverage for parser/capture/scheduler behavior, and use scheduled jobs for larger products.
- Preserve Make public-result and schema comparisons trustworthy #1091–Exercise critical unsafe boundaries under assertions and sanitizers #1098's existing oracles, runtime checks, LSN proof and candidate-binding mechanisms rather than creating parallel evidence infrastructure.
Acceptance criteria (proposed)
- R1: Each linked issue records its scoped outcome, actual verification evidence and remaining limits. Correct baselines pass; representative semantic defects are rejected for the intended reason.
- R2: Existing regression protection is retained and new checks run in the documented CI tier. Empty selection, skipped paths, fallback masking and infrastructure errors cannot masquerade as semantic coverage.
- R3: Every claimed proof uses the production executable implementation, enforced caller assumptions and a reviewed specification. SQL lowering, PostgreSQL semantics, transactions and FFI remain separately qualified where unproved.
- R4: Progress and release wording distinguish implemented tests, model proofs, executable proofs and runtime-qualified behavior. Partial delivery can ship without implying whole-extension verification.
Verification — PROPOSED — NOT RUN
Use each work item's focused verification plan and existing CI/release records. Record candidate revision, material configuration, actual runtime path and semantic-control outcomes. Follow repository formatting/linting and SQL-facing testing requirements for implementation changes.
Evidence and limits
Research baseline: 00d21749bc20af8b19940b857fae461e0ccfe471. The linked issues include inspected source locations and primary PostgreSQL/Verus references.
The preparatory review was read-only and sampled; no project code, tests, builds or proofs were executed. Acceptance criteria are proposals, and no separate saved Intentline contract was created.
Activity
grove commentedon Oct 29, 2026
Progress since the merged #1232 integration candidate: #1220 is now closed against its narrow acceptance using the pinned Verus baseline, five rejected executable mutants, packaged PostgreSQL 18 lifecycle cases, and candidate-binding evidence from CI run 40853118868. #1217 and #1222 are also closed. #1218, #1219, #1221, #1223, and #1224 remain open with exact partial evidence and limits recorded in their issue comments; #1198 remains open pending exact-head CI and required sole-owner source review. The umbrella acceptance is still incomplete.
grove commentedon Oct 29, 2026
Update: #1219 is now closed after exact-main DVM deep-tier run 40866922269 passed the 10-seed × 12-cycle histories; its 10 traces and 21/21 extended-history suite are retained in the run artifact. #1220, #1217 and #1222 are also closed. #1218, #1221, #1223 and #1224 remain open with their bounded implementation evidence and explicit limits recorded; #1198 remains open on the React 0.108.4 admission gate and pending owner review. The umbrella acceptance remains incomplete.
grove commentedon Oct 29, 2026
Update: #1218 is now closed after its bounded acceptance was verified on merged main candidate PR #1232 (run 40853118868). Exact numeric-scale observation, declared negative-control failures and setup rejection, the 12-case trigger/WAL × FULL/DIFFERENTIAL route witness, four SQL semantic mutants, and the installed receipt-prefix control passed; case and candidate evidence are retained in run artifacts.
#1219, #1220, #1217 and #1222 are also closed. #1221, #1223 and #1224 remain open with broader proof/qualification gaps recorded. #1198 remains open: PR #1199 has green exact-head CI, but the separate React 0.108.4 admission audit fails and the required sole-owner review is absent. Umbrella acceptance remains incomplete.
grove commentedon Oct 29, 2026
Update: #1218 and #1224 are now closed against merged main candidate PR #1232 after all bounded acceptance criteria passed in exact CI run 40853118868. Their comments link the semantic-control, identity-frame proof, and candidate-binding artifacts and state the remaining scope limits.
#1219, #1220, #1217 and #1222 are also closed. #1221 and #1223 remain open with explicit proof and runtime qualification gaps. #1198 remains open: PR #1199 has green exact-head CI, but its separate React 0.108.4 admission audit fails and the required sole-owner review is absent. Umbrella acceptance remains incomplete.
grove commentedon Oct 29, 2026
Current delivery status
The new PRs close only their documented bounded slices. #1221 and #1223 remain open for the acceptance recorded in their latest comments, so this umbrella issue remains open as well.
grove commentedon Oct 29, 2026
CI update for candidate PRs
Release evidence runtime controls, failed in the existingtest_dvm_failpoint_preserves_last_committed_result_and_recovers: CI observedeffective_refresh_mode=NO_DATAwhere the assertion expectedDIFFERENTIAL. Its scenario contains no TRUNCATE and does not exercise the new compaction guard. The same focused test passed twice locally, so a scheduler timing race is suspected but not yet confirmed. The parent workflow still has Unsafe ASan, Sensitive E2E 2/2, and packaged LSN runtime jobs in progress; I will rerun the failed job when the workflow completes.No PR has been merged. The #1198 compatibility admission and checksum remain unchanged pending the requested authorization.
grove commentedon Oct 29, 2026
CI update for candidate PRs
Sensitive E2E gate (1/2)failed in the existingtest_sum_case_differential_inserts: after the first insert refresh, the stream table held 20 while the defining query returned 50. The exact focused test passed locally, and the complete eight-test SUM CASE file passed on the same candidate. This points to a possible full-shard timing issue, but causality is not established.Release evidence runtime controlsfailpoint test also passed twice locally; its CI failure remains unexplained. The packaged checked-LSN runtime job passed.Sensitive E2E gate (2/2)is still running; I will retry only failed jobs once the parent workflow completes.grove commentedon Oct 29, 2026
Candidate CI update
refresh_st(), which can return after a lock-busy notice; commit06f6d584switches the SUM CASE scenarios to the existing convergence helper. All eight tests pass locally on the updated fix(dvm): correct nested join delta corrections (#1223) #1287 package; new exact-head CI is pending.grove commentedon Oct 29, 2026
Delivery update
c0b06387after 17/17 CI jobs passed on the final head.9e07d049after 26 checks passed and GitHub confirmed a clean merge state.grove commentedon Oct 29, 2026
Progress update: #1221 now has a bounded follow-up in PR #1293 at candidate 89ea301. The shared compaction eligibility decision is used by base and ST buffers, with local unit/lint/verification and 19 targeted E2E tests passing. GitHub CI is queued; full history and protected-window proof obligations remain open. #1221 and #1223 are still open, and previously excluded mutation issues remain excluded.
grove commentedon Oct 29, 2026
Additional scoped progress: #1292 now has a design-only PR, #1295, at candidate 980fe38. It records a source-traced design and preserves the INTERSECT admission guard until implementation and qualification. #1292 remains open; CI is queued. Existing #1221 and #1223 work also remains partial, and the excluded mutation issues remain out of scope.