# v0.87.14 - Correctness Program Completion

> **Status:** Planned
> **Scope:** 6-7 person-weeks
> **User promise:** *"The correctness gate tests what the roadmap says it tests."*
> **Blocked by:** [v0.87.13](v0.87.13.md)
> **Program:** [Composition-aware differential correctness](../plans/PLAN_DVM_COMPOSITION_CORRECTNESS.md)

## Theme

An August 2026 source audit of the shipped v0.87.1–v0.87.6 program found that
the correctness *architecture* landed but several of its strongest claims are
not yet substantiated by executed tests. Named composition cases do not build
their named query shapes, most metamorphic families are an inventory rather
than live equivalence runs, semantic coverage is populated synthetically
instead of from observed DVM decisions, `SnapshotPlan` is descriptive rather
than authoritative, the "exact" schema oracle compares only column count and
type family, and the shrink ladder stops after mutation removal.

This release closes the gap between the roadmap text and the code. It adds no
new correctness *concepts*; it makes the existing ones real, and it removes
the unchecked exit criteria left behind by v0.87.3 and v0.87.4.

## Scope allocation

| Work package | Person-weeks |
|---|---:|
| Faithful mandatory composition cases and histories | 1.50 |
| Live metamorphic families and isolated histories | 1.25 |
| Observed-path semantic coverage wiring | 1.25 |
| Authoritative snapshot plan consumption | 1.25 |
| Exact schema oracle and structured admission outcomes | 0.75 |
| Deeper shrink ladder | 0.75 |
| Benchmark readiness and harness contracts | 0.75 |
| **Total** | **7.50** |

## Items

### COR-21: Faithful mandatory composition cases

Every named case in the composition matrix must build the query shape its name
describes. `three_aggregate_leaves` builds three aggregate leaves;
`four_level_left_deep_join` builds a four-level left-deep join. `build_query()`
stops hard-coding two aggregate CTEs and one join.

Each named case also executes its own mutation history — group creation, group
removal, first group, winner change, and one-leaf, two-leaf, and all-leaf
changes — instead of the same two `UPDATE` statements for every case.

A structural test asserts that each case's generated tree matches the shape
asserted by its name, so the two cannot drift apart again.

### COR-22: Live metamorphic families

At least six metamorphic families execute real equivalence runs against
PostgreSQL: `UPDATE` versus `DELETE`+`INSERT`, CTE versus inlined query, alias
renaming, projection widening, join reordering, and projection placement, in
addition to the shipped split-versus-batched and idempotence cases.

Delete the test that only asserts the family enum has at least six entries. The
nightly job counts *executed* families, and the coverage report records which
families ran.

### COR-23: Observed-path semantic coverage

`with_decision_trace` is enabled by the E2E fuzzer and its events feed
`SemanticCoverageObservation`. Snapshot plans, changed-leaf buckets, group
transitions, and outer-join transitions are recorded because the engine took
those paths, not because a test inserted them.

The synthetic unit test remains only as a validator test for the report format
and is renamed to say so. Coverage floors fail when a bucket is unobserved in a
real run.

### COR-24: Authoritative snapshot plan

Operators consume `SnapshotPlan::for_tree` as the execution decision. The local
snapshot heuristics each operator derives today are removed, not merely
shadowed by tracing.

A debug assertion fails when an operator's effective snapshot behaviour
disagrees with the selected plan, and the aggregate-CTE join path from #939
carries an explicit regression test for plan selection.

### COR-25: Exact schema oracle and structured admission outcomes

`compare_signatures()` compares column names, ordinals, typmods, and collations
in addition to arity and type family. Type-family tolerance stays only where
PostgreSQL genuinely permits it, and any relaxation is named in the failure
report.

Error classification stops using substring matching on message text. Unsupported
SQL, invalid generator output, and product failure are distinguished by
SQLSTATE and pg_trickle reason code, and unclassified errors fail closed.

### COR-26: Deeper shrink ladder

Extend `scripts/dvm_shrink.py` past mutation removal to rows, columns,
operators, types, constraints, and execution settings, in that order, keeping a
candidate only when it preserves the invariant, failure class, and operator-path
family. Remove the `ponytail:` deferral note once the ladder is complete.

### COR-27: Admission-boundary coverage

The program did not find issue #953 — DIFFERENTIAL mode rejecting immutable
time-bucket expressions because volatility is resolved by function *name* using
the worst volatility across all overloads. Fix the resolution to use the
resolved function OID, and add admission-boundary cases to the generator so
expression resolution, volatility, and support-matrix decisions are searched
rather than assumed.

### COR-28: Correctness harness integrity

Fix the pgbench correctness gate so it waits for all expected stream tables to
complete refresh before selecting a common frontier. A partial-ready result is
not a valid benchmark conclusion.

Keep equivalent-history tests on isolated source tables or independently
restored starting states. Add a regression test that performs both histories
without duplicate-key interference, and make ignored DML errors fail the test.

### COR-29: Regression contracts and honest gate claims

Keep permanent sensitivity cases for both original #938/#939 defect families,
the v0.87.3 aggregate-CTE row-identity family, and the active negative
controls. Preserve oracle compatibility cases for PostgreSQL-compatible type
families so the gate does not reintroduce the v0.87.1 false-positive behavior.

The release report distinguishes defects found from defect classes searched,
and states which roadmap claims are backed by live execution. Green CI is not
reported as proof that an unexecuted generator family or synthetic coverage
bucket is clean.

## Required tests

- Each named composition case has a structural assertion on its generated tree
  and executes its own mutation history.
- At least six metamorphic families produce live equivalence results in the
  nightly tier, with per-family pass counts in the coverage report.
- A semantic-coverage run driven only by observed decision traces meets the
  mandatory floors; removing an engine path makes it fail.
- Operator-level tests assert that snapshot behaviour follows the selected
  `SnapshotPlan`, including the #939 aggregate-CTE join shape.
- Schema-oracle tests reject equal-value relations that differ in column name,
  typmod, or collation.
- Admission tests cover overloaded functions where one overload is volatile and
  the resolved overload is immutable.
- Shrinking an injected failure reduces rows, columns, and operators, not only
  mutation cycles.
- The pgbench gate waits for every expected stream table, and equivalent-history
  tests use isolated source state with no ignored DML failures.
- Permanent #938/#939, aggregate-CTE identity, negative-control, and oracle
  compatibility regressions remain active and are reported separately from
  unsearched space.

## Exit criteria

- [ ] Every mandatory case builds the shape and history its name describes.
- [ ] At least six metamorphic families execute against live PostgreSQL.
- [ ] Semantic coverage is populated from observed DVM decisions.
- [ ] No operator derives its own snapshot approximation.
- [ ] The schema oracle compares names, typmods, and collations exactly.
- [ ] Admission outcomes are classified without substring matching.
- [ ] The shrink ladder reaches row, column, and operator level.
- [ ] Issue #953 is fixed and covered by an admission-boundary test.
- [ ] The benchmark readiness race and shared-source history bug have regression
  tests.
- [ ] Original and newly discovered DVM defect families, negative controls, and
  oracle compatibility cases remain active.
- [ ] Release reports distinguish executed coverage from unsearched space.
- [ ] The v0.87.3 and v0.87.4 exit criteria are checked off against executed
      tests.