diff --git a/crates/epiphany-testkit/src/migration.rs b/crates/epiphany-testkit/src/migration.rs index 97d8078..36b2ed2 100644 --- a/crates/epiphany-testkit/src/migration.rs +++ b/crates/epiphany-testkit/src/migration.rs @@ -77,11 +77,18 @@ pub fn run_migration_equivalence(n_ops: usize, seed: u64) { "v0->v1 migration changed the canonical reduction state (seed {seed})" ); - // The migration faithfully inverts the projection on the representative - // payloads (a stronger property than reduction-equivalence alone). + // Round-trip self-consistency over *this* corpus: because the corpus is + // built from the same `valuegen` helpers the migration reconstructs values + // with, `migrate(project(env)) == env` holds exactly here. This is a sharper + // check than reduction-equivalence for the corpus, but it is NOT a universal + // inverse: the v0 projection drops fields the migration cannot recover (e.g. + // a `ReplaceWithRest` rest's own voice — recovered from the deleted event's + // placement at reduction, not from the value). The spec-level property is the + // reduction-equivalence asserted above; widening `operation_envelopes` to emit + // such a payload would surface here and is M2's cue to revisit faithfulness. assert_eq!( v1, migrated, - "migration is not the inverse of projection (seed {seed})" + "migration round-trip diverged from the original on this corpus (seed {seed})" ); // Deterministic: migrating the same projection against the same context diff --git a/spec/operation_catalog.pdf b/spec/operation_catalog.pdf index 60e2006..e5734dd 100644 Binary files a/spec/operation_catalog.pdf and b/spec/operation_catalog.pdf differ diff --git a/spec/operation_catalog.tex b/spec/operation_catalog.tex index ca20b5a..a873ae5 100644 --- a/spec/operation_catalog.tex +++ b/spec/operation_catalog.tex @@ -500,6 +500,15 @@ policy. \textbf{Re-anchoring.} The structure participates in the re-anchoring rule table when one of its endpoints is later tombstoned (see DeleteEvent). +\textbf{Migration coverage.} The v0$\rightarrow$v1 migration +(Chapter~\ref{ch:migration}) reconstructs the event-anchored \texttt{Tie}, +\texttt{Slur}, and \texttt{Beam} from the v0 reference (id plus event endpoints). +A \texttt{Spanner} is anchored by \texttt{TimeAnchor}s rather than a fixed pair +of event endpoints, so its full value is not reconstructable from the v0 +event-reference projection; a \texttt{Spanner}-create is therefore reported +unmigratable (read-only) under M1, alongside the respell case of P12-K1. A +faithful spanner migration joins when the projection carries the anchors --- M2. + \section{ChangeRegionTimeModel} \label{sec:k0:change-region-time-model}