# v0.87.5 - DVM Correctness Contracts and Semantic Coverage

> **Status:** Planned
> **Scope:** 7-8 person-weeks
> **User promise:** *"The DVM checks and reports the assumptions behind each delta."*
> **Blocked by:** [v0.87.4](v0.87.4.md)
> **Program:** [Composition-aware differential correctness](../plans/PLAN_DVM_COMPOSITION_CORRECTNESS.md)

## Theme

Move schema and snapshot assumptions from generated SQL into explicit DVM
contracts. Shape errors should fail in Rust with an operator path and both
schemas, not later as an opaque PostgreSQL error.

The fuzzer also records which DVM decisions ran. Coverage gates use observed
engine paths and state transitions, not only the query features requested by
the generator.

## Items

### COR-13: Typed relation schemas

Replace name-only `DiffResult` metadata with column names, type OIDs, typmods,
nullability, and provenance. Keep a temporary name accessor while operators
migrate.

Route generated `UNION`, `INTERSECT`, and `EXCEPT` operations through one typed
builder that rejects arity, type, alias, and internal-column mismatches.

### COR-14: Structured snapshot planning

Replace overlapping snapshot booleans with a `SnapshotPlan` that distinguishes
exact per-leaf reconstruction, exact combined reconstruction, post-change
correction, and unsupported compositions. Operators consume the selected plan
instead of deriving local approximations.

### COR-15: Decision trace and delta preflight

Under an explicit test setting, emit structured operator paths, schemas,
aggregate strategies, snapshot plans, pruning, cache, materialization, and
apply decisions. Test runs preflight generated delta SQL and compare
PostgreSQL's resolved row description with the declared schema.

### COR-16: Semantic coverage floors

Combine generator features, observed state transitions, DVM decisions, and
outcome classification. Pull requests require all mandatory #938-neighborhood
buckets, all P0 pairwise combinations, and changed-leaf coverage for one, two,
and all leaves.

## Exit criteria

- [ ] Every final delta has a declared and verified relation schema.
- [ ] Set-operation mismatches fail before PostgreSQL executes the delta.
- [ ] Snapshot selection uses a structured plan.
- [ ] Failure reports identify the operator path and both relevant schemas.
- [ ] CI publishes machine-readable and Markdown semantic-coverage reports.
- [ ] A pull request fails when a mandatory DVM path disappears.