mv-constraints.md

Derived-Row Constraints and Covering Structures

Stability: Beta — see Stability Tiers.

Two halves of one subject. The first is what happens when a materialized view carries a declared constraint — a CHECK, a foreign key, a secondary UNIQUE — given that derivation writes bypass the ordinary DML constraint pipeline. The second is the covering structure: the vocabulary for the physical shapes that enforce a UNIQUE constraint, one of which is a materialized view.

Covering structures are documented here rather than in Lenses and Layered Schemas because enforcement is what they exist for: a covering materialized view is admitted precisely when it can answer a UNIQUE conflict probe at the moment of the write. The lens layer is a consumer of that fact, not its home.

Derived-row constraint validation (declared CHECK / FK / secondary UNIQUE)

Invariant: MV-017, MV-018

A create table … maintained as table registers through the ordinary createTable path, so declared CHECK, FOREIGN KEY, and secondary (non-PK) UNIQUE constraints live on the backing TableSchema — but derivation writes bypass the DML constraint pipeline entirely (they go through the privileged backing surface). Declared constraints are real claims over the derivation: the writing statement fails when a row the derivation writes violates a declared CHECK, child-side FK, or secondary UNIQUE, with a diagnostic attributed to the maintained table — attribution is load-bearing because the failing statement targeted a different table (a source write, or the create/attach statement itself):

CHECK constraint failed: <name> (<expr>) — row derived into maintained table 'main.mt' violates its declared constraint
FOREIGN KEY constraint failed: <name> — row derived into maintained table 'main.mt' references a missing 'main.parent'
UNIQUE constraint failed: <name> (<cols>) — row derived into maintained table 'main.mt' collides on its declared UNIQUE constraint (key: <values>)

Two mechanisms, one semantic, split exactly along the subsystem's bulk-vs-incremental line:

• Bulk paths (create-fill, attach/re-attach reconcile, and constraint-bearing refresh) — after the 'replace-all' reconcile lands the derived row set in the pending layer, validateDeclaredConstraintsOverContents (runtime/emit/materialized-view-helpers.ts) runs a whole-table SQL scan over the table's effective (pending-over-committed) contents: select 1 from <t> where not (<check>) limit 1 per CHECK (validateChecksOverExistingRows) and the existing anti-join FK scan (validateForeignKeyOverExistingRows) per FK — the same engine-level validators ALTER ADD COLUMN/CONSTRAINT use. A maintained table resolves through the ordinary table path on read, so the scan reads the backing's pending state (never a re-derivation). A violation restores the prior catalog record (restorePrior) and the pending writes roll back with the statement; a failed create … maintained as drops the half-built table. Folding caveat: the optimizer trusts a declared constraint as a proven invariant (ruleFilterContradiction / ruleAntiJoinFkEmpty would fold the validation scan to empty), and unlike the ALTER paths the constraints under validation are already on the live record — so the live record is swapped for a constraint-stripped clone for the duration of the scans, then restored (the ADD COLUMN intermediate-schema discipline). Manual refresh materialized view of a constraint-bearing table-form maintained table runs the same bulk scan inside rebuildBacking — its real trigger is a stale table whose row-time plan was released, so source writes drifted in unvalidated and the refresh recomputes the drifted set. The sequence is assertRefreshRowsAreSet (duplicate-key reject, parity with replaceContents) → pending-layer applyMaintenance('replace-all') → the bulk scan → commit-first conn.commit() (matching replaceContents's existing commit-first semantics, and load-bearing for the reshape arm's post-reconcile data-validating ops, which scan committed contents). A violation throws before the commit, so the statement unwinds and the pending reconcile is discarded — the pre-refresh committed contents stay intact and the MV stays stale (the emitter clears stale only after a successful rebuild). A constraint-less / MV-sugar refresh keeps the validation-free replaceContents fast path unchanged (hasApplicableConstraints gates the branch; a pragma foreign_keys = off FK-only table stays on the fast path too, since its FK scan would no-op).

• Steady state (row-time maintenance) — scanning the whole table per source row would be pathological and is unnecessary: every row already in the backing was validated when it entered (the bulk validation seeds the induction), so only the delta is validated. registerMaterializedView compiles a per-table derived-row validator (core/derived-row-validator.ts) — declared CHECKs via buildConstraintChecks over an INSERT-shaped OLD/NEW pair and child-side FK EXISTS checks via buildChildSideFKChecks, the DML pipeline's own builders, so collations, scope resolution, determinism gating (pragma nondeterministic_schema included), and the auto-defer heuristic cannot drift. The maintenance manager validates each insert/update BackingRowChange's new image before cascading (a consumer never consumes an invalid producer row); the full-rebuild arm validates its 'replace-all' diff once at the end-of-statement flush. A non-subquery CHECK evaluates inline and aborts the writing statement immediately; a subquery-bearing CHECK and every child-side FK (inherently EXISTS-shaped) route to the deferred-constraint queue and validate at commit against final state — exactly ordinary-table deferral semantics, with the attribution threaded through a wrapped evaluator.

  Constraint-dependency invalidation. The validator is compiled once and bakes in the live incarnations of the tables its checks reference — the FK parent and any subquery-CHECK target. These constraint-only dependencies are not derivation sources (the source-change path never rebuilds them), so the validator records them on dependencyTables and the maintenance manager's schema-change subscription rebuilds it (validator only — the derivation is untouched, no staleness, no maintenance interruption) when one is renamed, dropped, or re-created. The trigger is either a table_removed/table_modified/table_added naming a dependencyTables member, or — for the rename case — a table_modified on the maintained table itself: an FK-parent / CHECK-target rename rewrites the maintained table's own FK referencedTable / CHECK AST in place and fires that event, while the old dependency name is already gone from the catalog. The rebuild reads the current catalog record (so it re-resolves against the new name) and refreshes dependencyTables. A dropped FK parent rebuilds cleanly to the absent-parent null-guards fallback (a non-NULL ref then fails the maintained-table FK constraint; a NULL ref is admitted); a dropped subquery-CHECK target cannot recompile, so a poisoned validator is installed that re-throws the sited "table not found" planning error on the next derivation write (the listener never fails the DDL that triggered it) and self-heals if the dependency is re-created. Without this, the once-compiled validator would keep connecting to the dead/renamed incarnation and fail maintenance writes with an internal Module 'memory' connect failed … not found error.

Semantics shared by both mechanisms:

• CHECK op-mask collapse. Whether maintenance realizes a change as an insert or update is an artifact of backing-key movement, so a derived row image is validated against every CHECK whose operations mask intersects insert | update — check on insert (…) and check on update (…) both apply (a deliberate divergence from the user-DML distinction). Evaluation is INSERT-shaped: the OLD section is all-NULL. A delete delta writes no row image and is never CHECK-validated; a delete-only CHECK never fires on derivation writes.
• No OLD/NEW image references. An applicable CHECK that references old.<col> / new.<col> is rejected at registration — create/attach fails with a sited diagnostic. A derived row has no OLD image (a transition CHECK would be vacuous) and NEW is the row itself (expressible unqualified); the bulk SQL scan also could not resolve the qualifiers. Delete-only CHECKs are exempt (they never fire on derivation writes).
• FK pragma gate at evaluation time. Child-side FK existence is evaluated only while pragma foreign_keys is on, re-read per validated row (never cached at registration). Rows admitted while the pragma was off are not retro-validated when it flips on (matching ordinary tables). MATCH SIMPLE: a row with any NULL FK column is admitted regardless of parent.
• Always a hard abort. Derivation writes carry no user OR clause; a violation is never masked by IGNORE/REPLACE (matching the DML rule that REPLACE never masks CHECK/FK).
• Zero overhead when nothing is declared. The validator is built only when the backing declares ≥1 applicable CHECK or ≥1 FK; every MV-sugar backing (buildBackingTableSchema hard-codes empty constraints) and every constraint-less maintained table builds and runs nothing.
• Detach guarantee. The bulk validation covers all rows the table holds post-reconcile and steady state validates every subsequent delta, so the table never commits a violating row — alter table … drop maintained therefore leaves an ordinary table whose every row already satisfies its (now user-enforced) constraints. No special detach handling exists or is needed.

Declared secondary UNIQUE

Invariant: MV-019

A UNIQUE collision is a property of a pair of rows, not a single row image, so it does not fit the per-row validator above. It is enforced by the backing host instead — exactly where each host's DML UNIQUE machinery already lives (memory: the auto-built covering index; store: the effective full scan) — as a post-batch check inside applyMaintenance: after an op batch lands in the pending state, each written (insert/update) image is checked against the batch's final effective contents for a row at a different primary key matching the constraint, and a hit throws the attributed error above (memory MemoryTableManager.enforceSecondaryUniqueOnMaintenance; store StoreTable.enforceSecondaryUniqueForMaintenance; contract in vtab/backing-host.ts § Constraint validation). One mechanism covers every maintenance shape — the attach/create-fill 'replace-all' reconcile (the bulk write IS a batch), steady-state bounded deltas, the full-rebuild flush, and MV-over-MV cascaded writes — with one diagnostic.

• Post-batch is load-bearing. A 'replace-all' diff applies its upserts before its deletes, so a per-op check would false-positive whenever the derived set moves a unique value from one primary key to another. After the batch, the pending state holds exactly the final contents, so checking each written image against it is exact. Checking only written images is also complete: pre-existing rows entered through DML / ADD CONSTRAINT / earlier validated maintenance, so any colliding pair includes at least one written image. Within a multi-row source statement, bounded-delta maintenance applies per source row — so a value swap across two source rows aborts mid-statement exactly as the equivalent multi-row UPDATE on an ordinary table would, while a full-rebuild body realizes the swap as one batch and succeeds.
• DML UNIQUE semantics preserved. Same-PK exclusion (a row never collides with itself, so a same-key upsert that changes a unique column is fine), NULLs distinct, partial-UNIQUE predicate scope (only in-scope images and in-scope candidates collide), and per-column declared collations (NOCASE collides case-insensitively) — all reused from the host's own enforcement implementation, not re-derived.
• Always a hard abort. The conflict action is forced to ABORT: a derivation write carries no user OR clause, and a declared on conflict replace/ignore default must not evict or drop derived rows — eviction would silently diverge the table from its derivation.
• Covering-MV route bypassed. A covering MV over the maintained table is cascade-maintained only after the batch returns, so it lags same-batch pairs; the check resolves through the synchronously-maintained index (or effective scan), never a covering MV.
• Zero overhead. Gated on uniqueConstraints being non-empty (the PK is not in uniqueConstraints); MV-sugar backings and UNIQUE-less maintained tables pay one empty-array check per batch.
• Detach guarantee holds identically: bulk + steady-state coverage means no committed state ever holds a colliding pair, so a detached table's rows already satisfy the (now user-enforced) UNIQUE.

Parent-side referential enforcement (M as an FK target)

Invariant: MV-020

Everything above is child-side — constraints declared on M. The dual case is an FK declared on an ordinary table C that references M (create table C (… references M(col) …)): a maintenance-driven delete or key-update of the referenced M row would silently orphan C, bypassing the declared RESTRICT / referential action. Because that FK lives on C, it never appears in M's plan or its derived-row validator — so it needs its own hook.

Steady-state maintenance therefore also fires parent-side referential enforcement on M's own backing delete/key-update, reusing the same referential-action engine the DML executor and the external-change seam use (runtime/foreign-key-actions.ts) — one engine, a third entry point, not a third copy. For each delete/update BackingRowChange (an insert has no parent-side action), MaterializedViewManager.enforceParentSideReferentialActions runs the transitive RESTRICT walk (assertTransitiveRestrictsForParentMutation) and then the declared CASCADE / SET NULL / SET DEFAULT propagation (executeForeignKeyActionsAndLens) — byte-for-byte the external-change seam's call shape (op-gated, lensRouted = false because a maintenance backing write is a physical basis write, RESTRICT walked POST-application now that the backing delta has already landed in the pending layer). It runs at both backing-write sites: the per-row inverse-projection apply in maintainRowTime (after the child-side validator, before the MV-over-MV cascade, so it fires whether or not M has MV consumers) and the deferred residual/full-rebuild flush in flushDeferredMaintenance (a deferred-arm M enforces at the end-of-statement flush, inside the statement-atomicity savepoint).

• RESTRICT fails the source write. A surviving RESTRICT child throws a CONSTRAINT error naming M (FOREIGN KEY constraint failed: DELETE on 'm' violates RESTRICT from 'c') that propagates up through maintenance → the DML executor → the statement, rolling the source write back, attributed to the maintained table.
• Cascade re-enters the write path. CASCADE / SET NULL / SET DEFAULT DML runs via _execWithinTransaction (the already-holding-the-mutex variant), nesting inside the source write's statement savepoint, so C's own constraints, watches, nested cascades, and — if C is itself a derivation source — its own maintenance all fire. A converging feedback loop (M is the parent of C and C is a source of M) terminates via the engine's visited-set cycle detection and the cascade-depth / flush-round backstops.
• Gate / cost. A foreign_keys-pragma early-return keeps the pragma-off path free. Beyond that it fires per delete/update change, resolving M's referencing FKs through SchemaManager.getReferencingForeignKeys — the catalog-level reverse-FK index. An unreferenced M pays a single map lookup that returns the shared empty bucket, so both engine calls early-return in O(1) with no catalog walk; a referenced M pays O(referencing-FKs). That is exact parity with an ordinary delete from M / update M, which route through the same index. It is not gated on the derived-row validator: that gate is child-side; an inbound FK lives on C and leaves M's plan untouched, so an M can be both a child and a parent and the two hooks coexist independently on the same BackingRowChanges.
• No-op cases. A value-identical maintenance update suppresses its backing op before enforcement runs (no change ⇒ no action); a delete of an M row whose referenced column is NULL participates in no FK match (MATCH SIMPLE); an insert has no parent-side action.

Re-validation on refresh materialized view of a stale table whose plan was released is covered by the constraint-bearing branch of the bulk-paths mechanism above (rebuildBacking — maintained-table-refresh-revalidation). Still out of scope (matching ordinary tables): rows admitted under pragma foreign_keys = off are not retro-validated when the pragma flips on, nor by a later refresh.

Covering structures

A UNIQUE constraint is logical; the structure that enforces it is optional and may take more than one physical shape. Quereus describes every such shape in one vocabulary — the covering structure — so the enforcement layer (and the lens layer above it) can pattern-match a single surface (CoveringStructure in vtab/memory/layer/manager.ts):

type CoveringStructure =
  | { kind: 'memory-index';      index: MemoryIndex }           // the auto-built secondary BTree
  | { kind: 'materialized-view'; view:  MaintainedTableSchema } // an explicit covering MV (the maintained table)

The recommended response to a lens.no-backing-index advisory. When the lens prover classifies a logical unique / primary key as enforced-set-level with mode: 'commit-time', it means no basis covering structure answers it, so enforcement falls back to the O(n) commit-time DeltaExecutor scan and warns. The fix is to declare an explicit basis covering materialized view (order by the constraint columns, projecting the UC columns + source PK — NULL-skipped via where … is not null for a nullable column) over the basis. The coverage prover then links it to the basis UC, proveLens resolves it via _findRowTimeCoveringStructure, and the obligation upgrades to mode: 'row-time' — O(log n) and conflict-resolution-capable (insert or replace / or ignore), which the commit-time scan cannot offer. In the logical-schema world (where the auto-index is retired) this covering MV is the sole row-time structure.

Implicit covering structures (the auto-index, reframed)

Every declared UNIQUE constraint auto-builds a synchronously-maintained secondary BTree for efficient enforcement (ensureUniqueConstraintIndexes). That BTree is reframed as an implicit covering structure (ImplicitCoveringStructure, origin: 'implicit-from-unique-constraint' — the origin vocabulary lives only on this association), held lightweight on the memory-table manager — it is not a catalog object; the BTree is the structure. Row-time enforcement (findIndexForConstraint) returns this memory-index variant.

Implicit covering structures are a backing detail and are hidden from collectSchemaCatalog / schema export by default, surfaced only when the originating constraint carries the tag quereus.expose_implicit_index = true.

Explicit covering structures (the coverage prover)

A user-declared materialized view can cover a UNIQUE constraint. The coverage prover (planner/analysis/coverage-prover.ts) recognizes the canonical covering shape and records the link eagerly at MV-creation time. For

create table t (id integer primary key, x integer not null, y integer not null, unique (x, y));
create materialized view ix_t_xy as select x, y, id from t order by x, y;   -- covers unique(x,y)

the prover proves ix_t_xy covers unique(x, y) and stamps the link (see Schema § Covering-structure links).

Recognition is narrow and conservative — every check forgoes an optimization on doubt; a false NotCovers only forgoes an optimization, a false Covers would be unsound:

• Shape. The optimized body walks down to a single constrained base table T (TableReference → optional Filter/Alias → Project → optional Sort; physical access nodes are transparent). A binary join is admitted when T provably contributes exactly one MV row per governed T row (see the join decomposition below). Aggregation, DISTINCT, set operations, FanOutLookupJoin, AsofScan, or a LIMIT/OFFSET row cap ⇒ not covering.
• Join (1:1) decomposition. "Exactly one MV row per governed T row" splits into two independent obligations:
  • No row loss (≥1): proven during the plan walk, two ways: (a) row preservation — T on the row-preserving side of the join (a left join with T in the left subtree, or a right join with T in the right subtree); or (b) referential integrity — an inner/cross join whose equi-pairs witness an inclusion dependency from the T-side relation to the lookup table's primary key, over a lookup side that exposes the parent's full row set, so enforced RI makes the join 1:1 (innerJoinRetainsConstrainedTable). Obligation (b) is IND-derived: it first consults the propagated PhysicalProperties.inds surface on the T-side subtree (indDerivedNoRowLoss) and falls back to the structural NOT-NULL-FK-on-T check (lookupCoveringFK + !match.nullable). Both gate on the same preconditions, so they agree on every single-FK shape; the IND path additionally proves no-row-loss across multi-hop FK chains (T → M → P), where the threaded IND M.cols ⊆ P.pk — carried onto the T ⋈ M sub-frame by join propagation — discharges the outer ⋈ P join that a single lookupCoveringFK(T, P, …) call cannot see. Both lean on the same NOT-NULL-FK + full-parent-row-set inclusion-dependency trust rule-join-elimination's INNER branch uses, so this adds no assumption the optimizer doesn't already make. An inner/cross join without a covering NOT-NULL FK/IND, semi/anti, full, and T on the dropping side are rejected as shape. (FDs encode uniqueness, not existence, so obligation (a) is a structural plan-walk check; (b) is discharged from the propagated IND surface with the structural FK-schema read as fallback.)
  • No fan-out (≤1): T's primary key must be a unique key of the topmost join's output relation (read via isUnique). The optimizer emits T.pk → all_join_cols into the join's FDs exactly when the equi-pairs cover a unique key of the lookup side; the moment the lookup side can multiply a T row, no such FD is emitted and the gate fails (fanout). The check is against the join frame, not the projected body root. When the optimizer instead eliminates a key-preserving join (FK→PK aligned, lookup unprojected — see rule-join-elimination), the body collapses to a single-source chain and the single-source path covers it directly.
• Projection. The output must include every UC column and every primary-key column of T (the PK identifies the source row for conflict resolution), each carrying the same collation as its base column (collation-mismatch otherwise) — a coarser-keyed backing (e.g. a NOCASE projection of a BINARY-constrained column, the coarsened-key shape) merges collation-equal/byte-different rows the constraint must keep distinct, so the link is never established across a collation mismatch. (Defense-in-depth today: a collation-changing projection mints a fresh attribute id and already fails projection coverage; the gate makes the requirement explicit.)
• Ordering. The body's order by columns must be a permutation of the UC columns. A missing order by does not cover. (Ordering and the WHERE predicate are read from the body AST, not the optimized plan, because the optimizer drops the Sort and absorbs a WHERE into an index range seek.)
• Predicate alignment. The body's materialized row set must equal the set the constraint governs: the WHERE predicate must entail uc.predicate (for partial UNIQUE) and an is not null per nullable UC column (NULL-skip), and must add no restriction beyond that. Entailment reuses the partial-UNIQUE clause vocabulary — see Coverage proving.

Multi-source 1:1 join bodies are covered: outer-join row preservation, and inner/cross lookup joins on an enforced NOT-NULL FK→PK (the no-row-loss obligation closed by referential integrity). That no-row-loss obligation is IND-derived — it discharges from the propagated PhysicalProperties.inds surface first (structural NOT-NULL-FK fallback retained), which additionally covers multi-hop FK chains (T → M → P) whose threaded IND a single lookupCoveringFK call cannot see. The AST ORDER BY / WHERE column resolution is qualifier-aware: alias.col resolves to a T column only when alias denotes T's reference (and a bare col only when unambiguous across the join's sources), so a 1:1 join whose lookup key reuses a UC column name covers — a term on a lookup column instead fails on its own terms (ordering-mismatch / predicate-entailment). Full-outer covering stays deferred (it injects lookup-only rows with no governed T row).

Enforcement through a covering MV

Row-time UNIQUE enforcement (the in-place substitution of insert or replace, the skip of insert or ignore, the conflict diagnostic of the default abort) requires the covering structure to be consistent at the moment of the write. A covering materialized view is eligible only when its contents are maintained synchronously with each source row-write (a per-row bounded-delta arm), so it is consistent mid-statement — the same property the auto-index has. A body that falls to the full-rebuild floor is reconciled only at the end-of-statement flush (its backing lags the source mid-statement), so it can never answer a synchronous per-row probe and is not an enforcing covering structure even when the coverage prover admits its shape — the auto-index answers instead.

findIndexForConstraint resolves it via Database._findRowTimeCoveringStructure(schema, table, uc) — a synchronous map lookup keyed on the constraint's coveringStructureName forward pointer (which names the covering MV's own table name), gated on a live covering plan that is per-row maintained (a deferred 'full-rebuild' plan is skipped) and not stale (structural breakage), with an O(1) negative fast path off rowTimeBySource so a non-covered table pays effectively nothing — and returns the materialized-view covering variant (carrying the MaintainedTableSchema) in preference to the memory-index auto-index. checkSingleUniqueConstraint's materialized-view arm then point-looks-up the covering maintained table (Database._lookupCoveringConflicts, reads-own-writes through the backing's coordinated connection) and recovers each conflicting source PK from the MV projection so REPLACE / IGNORE / ABORT resolve against the correct source row.

Collation eligibility gate (index-derived UNIQUE). A covering MV generates its conflict candidates by re-comparing each backing row under the declared source-column collation D (lookupCoveringConflicts / tryBuildCoveringPrefix), while the re-validators (memory checkUniqueViaMaterializedView, store findUniqueConflictViaCoveringMv) filter under the index per-column collation I (the index's COLLATE for a derivedFromIndex UNIQUE, else D). So the candidate set is a sound superset of the index-collation matches — safe to filter down — only when, per constrained column, D is coarser-or-equal to I (every I-equal pair is also D-equal). findRowTimeCoveringStructure proves this without a collation lattice (collations are opaque comparators) via coveringMvHonorsIndexCollation (schema/unique-enforcement.ts): each column is eligible iff I normalizes to BINARY (byte-identity ⊆ any D-equal, by reflexivity — the finer-index case, e.g. a BINARY index over a NOCASE column) or I == D (the common case, including every non-derived UNIQUE). A finer/incomparable index-derived UNIQUE — a coarser NOCASE index over a BINARY column, an RTRIM index over BINARY, or unrelated custom collations — would let the declared-collation candidate set silently miss conflicts, so the MV is declined and enforcement falls back to the per-scan / auto-index path (checkUniqueViaIndex / findUniqueConflict), which is already correct under I. The gate is per-column with AND semantics: one finer/incomparable member declines the whole MV. It is load-bearing, not mere defense-in-depth — the coverage prover's own collation-mismatch gate compares the output column collation against the declared base-column collation (not I), so it does link a coarser-index covering MV. The under-claim is safe: an exotic custom pair where D ⊒ I holds semantically but neither test fires is declined (a perf loss in an already-exotic shape, never a correctness loss); candidate generation (lookupCoveringConflicts / tryBuildCoveringPrefix) is unchanged — a declined MV is simply never selected. All three callers (store, memory, lens-prover) consult this one resolver, so they decline the same MV in lockstep.

Semantic-ordering identity in candidate generation. Collation is not the whole identity notion: a column whose declared type carries semantic ordering (types.md § Semantic ordering) calls two textually different values one value — TIMESPAN's 'PT1H' and 'PT60M' are one hour. lookupCoveringConflicts therefore builds its per-candidate comparisons through the shared uniqueEnforcementComparators (schema/unique-enforcement.ts): the declared type's compare for a semantic-ordering column, else the collation. This applies to both comparisons in the generator — the UC-column narrowing and the self-PK exclusion (a re-spelled PK still names the same row). It is orthogonal to the coarser-or-finer collation question above: the two spellings are one value at every site, so admitting them keeps the candidate set a superset either way. Without it a semantically-equal candidate was dropped in the generator and no re-validator ever saw it, so a duplicate slipped past the UNIQUE constraint (covering-mv-conflict-candidates-semantic).

The conflict check is a backing-PK prefix scan (O(log n + matches)), not a full backing scan. The body's order by columns are a permutation of the UC columns (the coverage prover's Ordering rule) and they seed the leading backing-PK columns (computeBackingPrimaryKey), so the leading k = uc.columns.length backing-PK columns are exactly the UC columns. lookupCoveringConflicts (tryBuildCoveringPrefix) builds the equality prefix in backing-PK column order (keyed prefix[i] = newRow[sourceCol(backingPkDefinition[i])], so a permuting order by still seeks to the right block), and scanLayer's equalityPrefix seek early-terminates when the leading columns stop matching. The fast path is taken only when the leading k backing-PK columns map to exactly the UC source-column set and every leading column (backing PK and its source UC column) is BINARY-collated; otherwise it falls back to the full layer scan. The collation gate is a soundness requirement, not a perf choice: the request carries no collation names, so the prefix seek's early-termination and planAppliesToKey resolve their comparators at the BINARY floor (resolveScanComparators), while the backing btree orders by the declared collation and the UNIQUE constraint conflicts by the source collation — under a non-binary collation a binary break could skip a collated-equal / binary-different conflict. The full-scan fallback re-compares with the source collation, so it stays collation-correct. DESC-leading prefixes use the fast path (equality on a column makes its direction irrelevant to grouping; the seek + ascending walk lands at the group start either way). A semantic-ordering column declares no collation, so it passes the BINARY gate and keeps the fast path — correctly: the BINARY floor is only the collation argument, and both backings still key such a column through the declared type (memory's createTypedComparator in resolveScanComparators, the store's storeSemanticKeyTransform — TIMESPAN's groupKey, JSON's structural byte encoder), so equal-value rows are physically contiguous and the seek lands on the whole group regardless of spelling. That holds for a DESC-leading and for a multi-column prefix alike (both pinned in test/covering-structure.spec.ts). Either path yields only candidates; the caller validates each against the live source row.

The preference tradeoff. With a linked covering MV present, the covering MV — not the auto-index — answers conflict resolution. The auto-index remains maintained but unconsulted (a redundant read-answering copy). For physical schemas this makes the MV path live and testable (the auto-index always exists, so the MV path is otherwise unreachable); it becomes the sole enforcement structure in the logical-schema world (the lens layer), where the auto-index is retired. The MV outranking the auto-index for physical schemas is defensible because the backing-PK prefix scan makes the MV's UNIQUE check O(log n + matches) — the same asymptotics as the auto-index probe — so a former O(n) backing scan (an O(n²) bulk-insert regression) is gone. The residual cost is a bounded constant factor (backing-connection resolution, amortized per statement via BackingConnectionCache on the maintenance path and re-resolved deterministically on the cold enforcement path; plus per-candidate live-source validation) plus the maintained-but-unconsulted auto-index. Keeping the MV in preference avoids a tuning flag and keeps the MV enforcement path exercised on physical schemas — identical to the sole enforcement path the lens world uses.

The eviction-maintenance edge. A REPLACE evicts the conflicting source row directly on the source storage (memory transaction layer / store delete), which bypasses the DML-executor row-time maintenance hook (it fires only for DML-executor row writes, not for evictions internal to a vtab's update). Rather than each substrate re-driving a slice of the pipeline itself, the eviction is reported to the executor via UpdateResult.evictedRows: the substrate only detects and deletes the evicted source row, then surfaces it, and the executor runs the same post-write delete pipeline it runs for an ordinary delete — including maintainRowTimeStructures({ op:'delete', oldRow }), which removes the evicted row's backing entry within the same statement (otherwise that entry would go stale and produce a phantom conflict for a later same-UC row). The executor processes a write's evictedRows before that write's own bookkeeping (evict-then-write), so the backing delete still lands mid-statement. Symmetrically, the conflict path validates every backing candidate against the live source row before acting, so a stale candidate is skipped rather than raised as a false conflict. Maintenance and cascades thus live solely in the executor (DRY); detection stays substrate-local.

Store-module parity. store-table-constraints.ts routes UNIQUE conflict resolution through the same _findRowTimeCoveringStructure / _lookupCoveringConflicts surface (the backing queried through the db via the backing host — memory by default, the store host under using store), validating candidates against the live store row (committed + this transaction's pending overlay). The constraint's coveringStructureName forward pointer is set by the eager prove-and-link on the schema-manager's constraint; a store table holds a copied schema whose constraint never received that mutation, so the resolver falls back to the authoritative schema-manager constraint matched by column set (resolveCoveringStructureName). The isolation-wrapped store path (createIsolatedStoreModule, exercised by yarn test:store) enforces UNIQUE via its own merged-view detection rather than the covering MV — but it needs no covering-MV routing to keep the backing consistent: its REPLACE evictions are reported via UpdateResult.evictedRows, and the executor's eviction pipeline maintains the backing uniformly across memory, direct store, and isolation alike. The backing consistency is obtained structurally (report the eviction, let the one pipeline maintain it) rather than by re-pasting covering-MV detection into the isolation layer.

FD-derived "body proves it" is a different proof. Separate from base-table covering, coverage-prover.ts exposes proveEffectiveKeyUnique, which proves the body's own output relation is unique on a set of output columns via its effective key (FD closure) — e.g. a group by x, y body is intrinsically one row per (x, y). This is the obligation primitive the lens layer's obligation: proved class consumes; it is a proof about the derived (output) relation, not a base-table covering structure, and is deliberately kept out of proveCoverage because an FD-derived output key masks base-row duplicates. See Effective-key proving and Lenses § the constraint-role split.