diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index 76da5f1..9d4fe4b 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -159,6 +159,17 @@ and delete semantics are **empty-only (precondition)**. feeding the cross-cutting re-anchoring table) are a strictly larger design than the slice needs. The empty-only gate is the conservative floor a cascade could later build on. Catalog §Structural Containers (M2e) states this normatively. +- **A create must carry an empty container, too — for *every* typed child + object, not just the structural hierarchy.** `create_region` / + `create_staff_instance` / `create_voice` reject (`ContainerNotEmpty`) a carried + value bearing any nested object with a distinct `TypedObjectId`: a region's + staff instances, barline-alignment groups, or graphic objects; a staff + instance's voices or measures; a voice's events. Graph creation clones the full + value into the score, so a carried child would materialize an object the reducer + never mints in its `objects` bookkeeping — a graph/ledger faithfulness gap. The + check reads the carried value only, so `reduce()` and `reduce_onto()` agree. + *(Review-driven: the first cut checked only the hierarchy vectors; + `barline_alignment_groups` / `graphic_objects` / `measures` were added after.)* - **Live-child sets are tracked in the reducer, not re-derived from the graph.** `region_instances: RegionId → {StaffInstanceId}` and `instance_voices: StaffInstanceId → {VoiceId}` (a voice's live events are read from @@ -196,8 +207,13 @@ classification names. Recorded here because the review changed code/tests. indices. - **`SetUserPageBreak` mirrors `SetUserSystemBreak` exactly, under the canonical LWW key.** Both now (i) share the live-and-staff-based precondition via a - `staff_based_regions` index, so `reduce()` and `reduce_onto()` agree on - missing / tombstoned / FreeGraphic targets, and (ii) materialize the graph break + `staff_based_regions` index, so for any region *represented in reducer state* + `reduce()` and `reduce_onto()` reach the same missing / tombstoned / FreeGraphic + verdict — that is, regions an op stream creates or deletes. (`reduce_onto(base)` + additionally seeds the base regions into that state, which a base-free `reduce()` + does not see, so a layout op targeting a live *base* region can still apply under + `reduce_onto` and no-op under `reduce`; the corpus exercises only op-created + regions, where the two agree.) Both also (ii) materialize the graph break under the anchor's **resolved musical position** (`apply_break_lww` + `resolved_anchor_position`): any existing anchor resolving to the same position is dropped before the new one is added, so the graph break list stays in lockstep diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index 39b3dd2..aba04a2 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -353,10 +353,14 @@ struct Reducer<'a> { region_instances: BTreeMap>, instance_voices: BTreeMap>, // Regions whose content carries a staff-based slot (staff-based or hybrid), - // and so can hold a metric grid or user break. FreeGraphic regions cannot; - // tracking this in the base-free reducer lets SetMetricGrid / SetUserPageBreak - // / SetUserSystemBreak reach the same precondition verdict with or without a - // graph, so reduce() and reduce_onto() never disagree on those ops. + // and so can hold a metric grid or user break. FreeGraphic regions cannot. + // Tracking this lets SetMetricGrid / SetUserPageBreak / SetUserSystemBreak + // reach the same precondition verdict for any region *represented in reducer + // state* (those an op stream creates/deletes) whether or not a graph is + // present. A base-only region exists in reducer state solely after + // `seed_from_graph` (reduce_onto), so a base-free reduce() that never sees it + // can still diverge on a base-region target — the corpus targets only + // op-created regions, where the two agree. staff_based_regions: BTreeSet, migrated_regions: BTreeSet, region_migrator: BTreeMap, @@ -394,6 +398,17 @@ struct WorkingSnapshot { graph: Option, } +/// The precondition no-op a structural create or delete returns when a container +/// is non-empty where the operation requires it empty (a create carrying children, +/// or a delete of a container with live children). +fn container_not_empty() -> OperationEffect { + OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::ContainerNotEmpty, + }, + } +} + /// Apply a user break to a region's break list under the canonical LWW key — the /// anchor's resolved musical position. Any existing anchor resolving to that same /// position is dropped first, so two anchors at one position never both persist, @@ -2053,6 +2068,18 @@ impl<'a> Reducer<'a> { if let Some(effect) = self.mint_precondition(robj) { return effect; } + // A create mints an *empty* container: its child objects are minted (or + // base-seeded) separately. A carried value bearing any typed child object + // — a staff instance, a barline-alignment group, or a graphic object, each + // a distinct TypedObjectId the reducer does not mint here — would import an + // unminted object into the graph, so it is rejected (Catalog §Structural + // Containers). + if !op.region.content.staff_instances().is_empty() + || !op.region.content.barline_alignment_groups().is_empty() + || !op.region.content.graphic_objects().is_empty() + { + return container_not_empty(); + } self.graph_create_region(&op.region); self.mint_container(env, robj); self.region_instances.entry(op.region_id()).or_default(); @@ -2081,6 +2108,11 @@ impl<'a> Reducer<'a> { if let Some(effect) = self.mint_precondition(iobj) { return effect; } + // Reject a carried staff instance bearing any typed child object — a voice + // or a measure (the two object collections it can hold). + if !op.instance.voices.is_empty() || !op.instance.measures.is_empty() { + return container_not_empty(); + } self.graph_create_staff_instance(op.region, &op.instance); self.mint_container(env, iobj); self.region_instances @@ -2107,6 +2139,9 @@ impl<'a> Reducer<'a> { if let Some(effect) = self.mint_precondition(vobj) { return effect; } + if !op.voice.events.is_empty() { + return container_not_empty(); + } self.graph_create_voice(op.staff_instance, &op.voice); self.mint_container(env, vobj); self.instance_voices diff --git a/crates/epiphany-ops/tests/graph_reduction.rs b/crates/epiphany-ops/tests/graph_reduction.rs index 0a3fe7f..df7f5b2 100644 --- a/crates/epiphany-ops/tests/graph_reduction.rs +++ b/crates/epiphany-ops/tests/graph_reduction.rs @@ -1615,3 +1615,216 @@ fn user_breaks_at_one_resolved_position_collapse_to_a_single_anchor() { ); assert!(check_invariants(&result.score).is_empty()); } + +#[test] +fn create_rejects_a_non_empty_carried_container() { + let base = epiphany_core::generators::valid_score(100); + let region = base.canvas.regions[0].id; + let (staff_instance, _) = target(&base); + + let rejected = |effect: OperationEffect| { + matches!( + effect, + OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::ContainerNotEmpty, + }, + } + ) + }; + + // A create mints an empty container; carrying a child the create does not + // itself mint must be rejected (else the graph gains unminted objects). + let fresh_region_id = epiphany_core::RegionId::new(ReplicaId(80), 0); + let mut region_with_child = valuegen::region(fresh_region_id); + region_with_child + .content + .staff_instances_mut() + .expect("staff based") + .push(valuegen::staff_instance( + StaffInstanceId::new(ReplicaId(80), 1), + base.staves[0].id, + )); + let create_region = envelope( + 80, + 0, + 10, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateRegion(epiphany_ops::CreateRegionOp { + region: region_with_child, + })), + ); + + let mut instance_with_child = + valuegen::staff_instance(StaffInstanceId::new(ReplicaId(80), 2), base.staves[0].id); + instance_with_child + .voices + .push(valuegen::voice(VoiceId::new(ReplicaId(80), 3))); + let create_instance = envelope( + 81, + 0, + 11, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateStaffInstance( + epiphany_ops::CreateStaffInstanceOp { + region, + instance: instance_with_child, + }, + )), + ); + + let mut voice_with_child = valuegen::voice(VoiceId::new(ReplicaId(80), 4)); + voice_with_child.events.push(EventId::new(ReplicaId(80), 5)); + let create_voice = envelope( + 82, + 0, + 12, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateVoice(epiphany_ops::CreateVoiceOp { + staff_instance, + voice: voice_with_child, + })), + ); + + let mut set = OperationSet::new(); + set.accept_all(vec![ + create_region.clone(), + create_instance.clone(), + create_voice.clone(), + ]); + let result = set.reduce_onto(&base); + + assert!( + rejected(effect_of(&result, create_region.id)), + "a region carrying a staff instance is rejected" + ); + assert!( + rejected(effect_of(&result, create_instance.id)), + "a staff instance carrying a voice is rejected" + ); + assert!( + rejected(effect_of(&result, create_voice.id)), + "a voice carrying an event is rejected" + ); + assert!( + !result + .score + .canvas + .regions + .iter() + .any(|r| r.id == fresh_region_id), + "the non-empty region is not materialized into the graph" + ); + assert!(check_invariants(&result.score).is_empty()); +} + +#[test] +fn create_rejects_carried_non_hierarchy_children() { + let base = epiphany_core::generators::valid_score(100); + let region = base.canvas.regions[0].id; + let staff = base.staves[0].id; + + let rejected = |effect: OperationEffect| { + matches!( + effect, + OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::ContainerNotEmpty, + }, + } + ) + }; + + // A region carrying a barline-alignment group (a typed object, not a staff + // instance) must still be rejected. + let mut region_with_barline = valuegen::region(epiphany_core::RegionId::new(ReplicaId(83), 0)); + region_with_barline + .content + .staff_based_mut() + .expect("staff based") + .barline_alignment_groups + .push(epiphany_core::BarlineAlignmentGroup { + id: epiphany_core::BarlineAlignmentGroupId::new(ReplicaId(83), 1), + members: Vec::new(), + }); + let create_barline = envelope( + 83, + 0, + 10, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateRegion(epiphany_ops::CreateRegionOp { + region: region_with_barline, + })), + ); + + // A free-graphic region carrying a graphic object. + let mut region_with_graphic = valuegen::region(epiphany_core::RegionId::new(ReplicaId(83), 2)); + region_with_graphic.content = + epiphany_core::RegionContent::FreeGraphic(epiphany_core::GraphicContent { + objects: vec![epiphany_core::GraphicObject { + id: epiphany_core::GraphicObjectId::new(ReplicaId(83), 3), + }], + }); + let create_graphic = envelope( + 83, + 1, + 11, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateRegion(epiphany_ops::CreateRegionOp { + region: region_with_graphic, + })), + ); + + // A staff instance carrying a measure (a typed object, not a voice). + let mut instance_with_measure = + valuegen::staff_instance(StaffInstanceId::new(ReplicaId(83), 4), staff); + instance_with_measure.measures.push(epiphany_core::Measure { + id: epiphany_core::MeasureId::new(ReplicaId(83), 5), + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }); + let create_measure = envelope( + 84, + 0, + 12, + CausalContext::new(), + None, + OperationPayload::Primitive(OperationKind::CreateStaffInstance( + epiphany_ops::CreateStaffInstanceOp { + region, + instance: instance_with_measure, + }, + )), + ); + + let mut set = OperationSet::new(); + set.accept_all(vec![ + create_barline.clone(), + create_graphic.clone(), + create_measure.clone(), + ]); + let result = set.reduce_onto(&base); + + assert!( + rejected(effect_of(&result, create_barline.id)), + "a region carrying a barline-alignment group is rejected" + ); + assert!( + rejected(effect_of(&result, create_graphic.id)), + "a region carrying a graphic object is rejected" + ); + assert!( + rejected(effect_of(&result, create_measure.id)), + "a staff instance carrying a measure is rejected" + ); + assert!(check_invariants(&result.score).is_empty()); +} diff --git a/spec/operation_catalog.pdf b/spec/operation_catalog.pdf index d8534a8..e97094e 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 f3b8ea2..91e4cdc 100644 --- a/spec/operation_catalog.tex +++ b/spec/operation_catalog.tex @@ -505,8 +505,10 @@ recorded but not materialised. \emph{differing} values produce a \texttt{StructuralFieldCollision} on the field \texttt{event}, recording the winner (later in canonical order) and the loser. -\textbf{Undo semantics.} Undo restores the pre-operation event value under the -active policy. +\textbf{Undo semantics.} Under the prototype's minted-object undo +(Section~\ref{sec:k0:undo}) a field overwrite mints nothing, so undoing the +enclosing transaction does not restore the prior event value; a snapshot-and- +restore inverse is a Phase-3 refinement (P11-C8). \textbf{Re-anchoring.} If the target event is tombstoned, the modification is a no-op (\texttt{TargetTombstoned}/\texttt{TargetMissing}). @@ -541,10 +543,11 @@ bookkeeping, which tombstones or mints the pitch object either way. is idempotent). Modify: two concurrent differing writes of one pitch produce a \texttt{StructuralFieldCollision} on the field \texttt{pitch}. -\textbf{Undo semantics.} Insert undoes by tombstoning the minted pitch (re-rest -if it was the only pitch); delete undoes by re-introducing the tombstoned pitch -(re-note from a degraded rest); modify restores the prior value --- each under -the active policy. +\textbf{Undo semantics.} Insert is the only minting member: undoing the enclosing +transaction tombstones the minted pitch, re-resting the event if it was the only +one (Section~\ref{sec:k0:undo}). The prototype's minted-object undo has nothing +to tombstone for delete or modify, so neither is inverted under it (re-introducing +a tombstoned pitch or restoring a prior value is a Phase-3 refinement, P11-C8). \textbf{Re-anchoring.} An operation whose target event or pitch is tombstoned is a no-op; tombstoning a pitch runs the cross-cutting re-anchoring table over any @@ -571,8 +574,9 @@ deferred (Chapter~4 tuning catalog; P12-K2). \textbf{Conflict cases.} None --- composition is deterministic in canonical order (a deterministic repair, not a conflict). -\textbf{Undo semantics.} Undo applies the negated interval to the same targets -under the active policy. +\textbf{Undo semantics.} Transpose mints nothing, so the prototype's minted-object +undo (Section~\ref{sec:k0:undo}) does not negate it; an inverse-interval undo is a +Phase-3 refinement (P11-C8). \textbf{Re-anchoring.} Tombstoned targets are skipped (the transpose applies only to live pitches). @@ -607,8 +611,9 @@ when one of its endpoints is later tombstoned (see DeleteEvent). 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. +unmigratable (read-only), alongside the respell case of P12-K1, and remains so. +A faithful spanner migration awaits a richer v0 projection that carries the +anchors --- a Phase-3 / Pass-12 extension, not yet implemented. \section{DeleteCrossCutting} \label{sec:k0:delete-cross-cutting} @@ -627,8 +632,9 @@ reduction removes the structure from the score. \textbf{Conflict cases.} None (delete-wins is idempotent). -\textbf{Undo semantics.} Undo re-introduces the tombstoned structure under the -active policy. +\textbf{Undo semantics.} A delete mints nothing, so the prototype's minted-object +undo (Section~\ref{sec:k0:undo}) does not re-introduce the tombstoned structure +(P11-C8). \textbf{Re-anchoring.} The deletion is direct (the structure is the target, not a referenced endpoint); it does not itself trigger the endpoint re-anchoring table. @@ -654,8 +660,9 @@ Graph-aware reduction overwrites the structure in place. \textbf{Conflict cases.} Two concurrent differing modifications of one structure produce a \texttt{StructuralFieldCollision} on the field \texttt{cross\_cutting}. -\textbf{Undo semantics.} Undo restores the prior structure value under the active -policy. +\textbf{Undo semantics.} A modification mints nothing, so the prototype's +minted-object undo (Section~\ref{sec:k0:undo}) does not restore the prior +structure value (a snapshot-and-restore inverse is Phase-3, P11-C8). \textbf{Re-anchoring.} If the target structure is tombstoned, the modification is a no-op; re-deriving the endpoints lets a subsequent endpoint tombstone re-anchor @@ -704,8 +711,8 @@ the catalog's to design when graph-aware migration is the only reduction path. \texttt{DeleteStaffInstanceOp \{ staff\_instance: StaffInstanceId \}}; \texttt{CreateVoiceOp \{ staff\_instance: StaffInstanceId, voice: Voice \}} / \texttt{DeleteVoiceOp \{ voice: VoiceId \}}. Each create carries the full -container value (v1); the reduction preconditions it carries no children (an -empty container). +container value (v1); the reduction preconditions it bears \emph{no typed child +object} --- an empty container. \textbf{Canonical encoding.} Create: the parent id (where the schema names one), then the length-framed canonical bytes of the container value. Delete: the @@ -714,8 +721,11 @@ container id. \textbf{Reduction rule.} Set-union creation of an \emph{empty} container, and an \emph{empty-only} delete-wins tombstone. A create mints the container live if its id is fresh and (for staff instance and voice) its parent is live; it -preconditions the carried value to have no live children, so contents are added -by subsequent operations. A delete is a delete-wins tombstone, but a +preconditions the carried value to bear no typed child object (a region: no staff +instances, barline-alignment groups, or graphic objects; a staff instance: no +voices or measures; a voice: no events), since those carry distinct +\texttt{TypedObjectId}s the reducer mints separately --- so contents are added by +subsequent operations. A delete is a delete-wins tombstone, but a \emph{precondition no-op} (\texttt{ContainerNotEmpty}) unless the container has no live children --- the caller deletes contents first. Graph-aware reduction adds or removes the container and maintains the region's staff extent so @@ -725,9 +735,11 @@ or removes the container and maintains the region's staff extent so create is idempotent), and the empty-only delete is a deterministic precondition gate, not a conflict. -\textbf{Undo semantics.} Undo of a create tombstones the minted container; undo -of a delete re-introduces it. \texttt{StrictInverse} conflicts if the target was -concurrently mutated; the policy treatment is as for InsertEvent. +\textbf{Undo semantics.} Undo of a \emph{create} tombstones the minted container +(Section~\ref{sec:k0:undo}); \texttt{StrictInverse} conflicts if it was +concurrently mutated, with the policy treatment as for InsertEvent. A +\emph{delete} mints nothing, so the prototype's minted-object undo does not +re-introduce it (P11-C8). \textbf{Re-anchoring.} Not applicable (the containers are minted/tombstoned by id; the empty-only precondition means a delete never strands live children). @@ -788,9 +800,10 @@ single slot). SetMetricGrid: two concurrent differing grids for one region produce a \texttt{StructuralFieldCollision} on the field \texttt{metric\_grid}. -\textbf{Undo semantics.} Undo restores the prior metadata, the prior region grid, -or the prior \texttt{(region, resolved-position)} break preference, under the -active policy. +\textbf{Undo semantics.} All three are field overwrites that mint nothing, so the +prototype's minted-object undo (Section~\ref{sec:k0:undo}) does not restore the +prior metadata, grid, or break preference (a snapshot-and-restore inverse is a +Phase-3 refinement, P11-C8). \textbf{Re-anchoring.} The advisory breaks degrade as for SetUserSystemBreak; the metric grid and metadata are keyed by region / singleton and do not re-anchor (a @@ -873,8 +886,11 @@ opens read-only. The reference implementation (\texttt{epiphany-ops::migrate}) reconstructs the \texttt{InsertEvent} event, the \texttt{DeleteEvent} compensation, the \texttt{ChangeRegionTimeModel} model, the \texttt{SetUserSystemBreak} anchor, and -the cross-cutting structure self-containedly from the v0 projection; it recovers -a \texttt{RespellPitch} spelling from the context (P12-K1, +the event-anchored cross-cutting structures (\texttt{Tie} / \texttt{Slur} / +\texttt{Beam}) self-containedly from the v0 projection; a \texttt{Spanner}, +anchored by \texttt{TimeAnchor}s rather than event endpoints, remains unmigratable +until the projection carries them. It recovers a \texttt{RespellPitch} spelling +from the context (P12-K1, Section~\ref{sec:k0:respell-pitch}). The migration's merge gate (\texttt{epiphany-testkit::migration}) drives the inverse direction --- projecting a v1 corpus to v0 and migrating it back --- and asserts byte-identical reduction