# v0.87.4 - Stateful and Metamorphic Correctness

> **Status:** Planned
> **Scope:** 7-8 person-weeks
> **User promise:** *"Equivalent queries and mutation histories stay equivalent."*
> **Blocked by:** [v0.87.3](v0.87.3.md)
> **Program:** [Composition-aware differential correctness](../plans/PLAN_DVM_COMPOSITION_CORRECTNESS.md)

## Theme

Replace uniform random DML with mutations that cross DVM state boundaries.
The planner targets group creation and removal, aggregate winner replacement,
join-match transitions, key movement, NULL transitions, and simultaneous
changes to several source leaves.

Metamorphic checks then run equivalent query forms and mutation histories from
cloned starting states. PostgreSQL's direct result remains the oracle for every
branch.

## Items

### COR-10: State-directed mutation planner

Track enough source state to select effective mutations without becoming a
second expected-result engine. The planner records live rows, group membership,
MIN and MAX candidates, join multiplicity, nullable keys, and the leaves
changed in each cycle.

Every generated trace covers a selected set of boundary transitions. Exact
comparison runs after every cycle.

### COR-11: Multi-source histories

Distribute mutations across every source represented in a query. Required
cycles include one changed source, two changed sources, all changed sources,
parent-and-child changes, and an aggregate-winner change paired with a change
on another branch.

### COR-12: Metamorphic checks

Add these initial families:

- split refreshes versus one batched refresh;
- UPDATE versus the equivalent DELETE and INSERT;
- CTE versus inline subquery;
- alias renaming;
- unused physical-column widening;
- safe INNER JOIN reordering;
- projection placement;
- refresh idempotence; and
- commuting source-mutation orders.

Strategy equivalence is allowed only when each branch asserts the strategy it
actually used.

## Exit criteria

- [ ] Multi-table traces mutate every represented source.
- [ ] Changed-leaf buckets for one, two, and all leaves are observed.
- [ ] Group and outer-join boundary transitions are explicit dimensions.
- [ ] Every mutation is effective and recorded.
- [ ] Batching invariance runs for every mandatory #938-neighborhood case.
- [ ] At least six metamorphic families run in nightly CI.