neuwirth
/
epiphany
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Pass 13 — P13-D3: reject spanners anchored to a missing region/measure 

A spanner anchored to a missing region/measure minted dangling: the
CreateCrossCutting mint checked only CrossCuttingValue::endpoints() (events),
so a region/measure TimeAnchor with no live target slipped past — the exact
sibling of the repeat mint gap fixed in Phase D.

Per the user's call ("fix the mint only"): CrossCuttingValue::anchor_object_refs()
returns the full anchor object set (events + a spanner's measure/region anchors;
wall-clock references nothing), and create_cross_cutting's liveness precondition
now checks it, so such a spanner is refused (TargetMissing) rather than minted
dangling. Deterministic across both reduction modes (the base seed registers
regions/measures in objects). endpoints() stays event-only — it feeds the
re-anchoring referent index, and non-event referent re-anchoring stays deferred,
ratified events-only (the spanner discipline).

Regression: create_cross_cutting_spanner_preconditions_region_measure_anchors
(missing region → refused; live measure/region → mints, invariant-clean).
937 tests, convergence/equivocation/conformance green. PASS13_CANDIDATES.md:
P13-D3 resolved.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Levi Neuwirth 2026-07-08 18:01:08 -04:00
parent e6308371d5
commit cd998142f5
4 changed files with 143 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
crates/epiphany-ops/DECISIONS.md
View File

@ -1102,6 +1102,18 @@ SPANNERS — `CrossCuttingValue::endpoints()` filters to events, so a spanner
anchored to a missing region/measure mints dangling past the invariant
(`anchor_target_exists` checks spanner anchors at all three kinds), and
non-event referent tombstones (a `DeleteRegion` under a region-anchored
spanner or repeat) re-anchor nothing. Pre-existing, ratified-as-implemented
("every referenced endpoint is live" reads events-only in the code);
changing it is a catalog-semantics decision, not a Phase-D fix.
spanner or repeat) re-anchor nothing.
**P13-D3 resolved (Pass 13, 2026-07-08; user: "fix the mint only").** The MINT
is fixed: `CrossCuttingValue::anchor_object_refs()` returns the full anchor
object set (events + a spanner's measure/region anchors; wall-clock references
nothing), and `create_cross_cutting`'s liveness precondition now checks it —
so a spanner anchored to a missing region/measure is refused
(`TargetMissing`) rather than minted dangling, exactly as the repeat mint's
`anchor_object_refs` fix does. Deterministic across both reduction modes (the
base seed registers regions and measures in `objects`). `endpoints()` stays
event-only — it feeds the re-anchoring referent index, and **non-event
referent re-anchoring stays deferred, ratified events-only** (the spanner
discipline; extending the referent index to region/measure tombstones is the
larger change the user parked). Regression:
`create_cross_cutting_spanner_preconditions_region_measure_anchors`.

26
crates/epiphany-ops/src/payload.rs
View File

@ -732,6 +732,32 @@ impl CrossCuttingValue {
.collect(),
}
}
/// Every object this structure's anchors reference — its endpoint events,
/// and (for a spanner) the measures and regions its [`TimeAnchor`]s name.
/// The mint precondition checks all of these are live, so a spanner
/// anchored to a missing region or measure is rejected rather than minted
/// dangling (P13-D3). Distinct from [`Self::endpoints`], which stays
/// event-only: it feeds the re-anchoring referent index, which repairs
/// event tombstones only (the spanner discipline — non-event referent
/// re-anchoring stays deferred, ratified events-only).
pub fn anchor_object_refs(&self) -> Vec<TypedObjectId> {
match self {
// Event-anchored kinds reference exactly their endpoint events.
CrossCuttingValue::Tie(_) | CrossCuttingValue::Slur(_) | CrossCuttingValue::Beam(_) => {
self.endpoints()
}
CrossCuttingValue::Spanner(s) => [&s.start, &s.end]
.into_iter()
.filter_map(|anchor| match anchor {
TimeAnchor::Event { id, .. } => Some(TypedObjectId::Event(*id)),
TimeAnchor::Measure { id, .. } => Some(TypedObjectId::Measure(*id)),
TimeAnchor::Region { id, .. } => Some(TypedObjectId::Region(*id)),
TimeAnchor::WallClock { .. } => None,
})
.collect(),
}
}
}
impl CanonicalEncode for CrossCuttingValue {

103
crates/epiphany-ops/src/reduce.rs
View File

@ -3124,8 +3124,13 @@ impl<'a> Reducer<'a> {
}
None => {}
}
// Endpoints must exist (live).
for e in &endpoints {
// Every anchored object must exist (live) — events for the
// event-anchored kinds, and a spanner's region/measure anchor targets
// too, so a spanner anchored to a missing region/measure is rejected
// rather than minted dangling (P13-D3). Deterministic across both
// reduction modes: the base seed registers regions and measures in
// `objects` (as the repeat mint precondition relies on).
for e in &op.structure.anchor_object_refs() {
if !matches!(self.objects.get(e), Some(ObjectState::Live)) {
return OperationEffect::NoOp {
reason: NoOpReason::PreconditionFailedUnderReduction {
@ -8224,6 +8229,100 @@ mod tests {
);
}
#[test]
fn create_cross_cutting_spanner_preconditions_region_measure_anchors() {
// P13-D3 (fix the mint): a spanner anchored to a missing region or
// measure is refused (the mint checks `anchor_object_refs`, not just the
// event endpoints `endpoints()` returns), and a spanner anchored to a
// live region/measure mints. Non-event referent re-anchoring stays
// events-only (ratified — the spanner discipline).
use epiphany_core::generators::valid_score_rich;
use epiphany_core::{MeasurePosition, SpannerId};
let base = valid_score_rich(0x0D0E);
let (region_id, measure_id) = base
.canvas
.regions
.iter()
.find_map(|r| {
r.staff_instances()
.iter()
.find_map(|si| si.measures.first().map(|m| (r.id, m.id)))
})
.expect("the rich fixture has a measure");
let spanner = |id, start, end| {
OperationKind::CreateCrossCutting(CreateCrossCuttingOp {
structure: CrossCuttingValue::Spanner(epiphany_core::Spanner {
id,
start,
end,
staves: Vec::new(),
kind: Default::default(),
style: Default::default(),
}),
})
};
let region_anchor = |id| TimeAnchor::Region {
id,
edge: RegionEdge::End,
offset: AnchorOffset::Zero,
};
// Start names a missing region: refused, not minted dangling.
let dangling = SpannerId::new(ReplicaId(9), 810);
let mut set = OperationSet::new();
set.accept_all(vec![prim_env(
9,
0,
10,
CausalContext::new(),
spanner(
dangling,
TimeAnchor::Region {
id: RegionId::new(ReplicaId(9), 7_777),
edge: RegionEdge::Start,
offset: AnchorOffset::Zero,
},
region_anchor(region_id),
),
)]);
assert!(
!set.reduce_onto(&base)
.state
.objects
.contains_key(&TypedObjectId::Spanner(dangling)),
"a spanner anchored to a missing region is refused, not minted dangling"
);
// Live measure + live region anchors: mints, invariant-clean.
let live = SpannerId::new(ReplicaId(9), 811);
let mut set = OperationSet::new();
set.accept_all(vec![prim_env(
9,
0,
10,
CausalContext::new(),
spanner(
live,
TimeAnchor::Measure {
id: measure_id,
position: MeasurePosition::Start,
offset: AnchorOffset::Zero,
},
region_anchor(region_id),
),
)]);
let result = set.reduce_onto(&base);
assert!(
matches!(
result.state.objects.get(&TypedObjectId::Spanner(live)),
Some(ObjectState::Live)
),
"live region/measure anchors mint the spanner"
);
assert!(epiphany_core::check_invariants(&result.score).is_empty());
}
#[test]
fn deleting_an_event_rewires_a_dal_segno_jump_target() {
// The kind's jump targets are anchor SITES like any other: a dead

2
spec/PASS13_CANDIDATES.md
View File

@ -10,4 +10,4 @@ this file is the index, not the analysis.
| P13-K1 | The K3 verdict for a system pitch introduced by a ModifyEvent replacement value differs across a snapshot cut (in-session `TargetMissing` vs post-snapshot `SystemDerivedContentImmutable`); really "may ModifyEvent introduce never-minted pitch ids" | `crates/epiphany-ops/DECISIONS.md` (Pass-12 G-pass code tranche) | open |
| P13-D1 | Undo-driven event tombstones run graph-side re-anchor/cascade but never ledger-side `reanchor_for_tombstone`: structures leave the graph while staying `Live`, no `RepairRecord` — Ch6's same-step recording MUST is unmet for undo-driven tombstones (pre-existing class: slurs/spanners; repeats now too) | `crates/epiphany-ops/DECISIONS.md` (Schema major 2, Phase D) | open |
| P13-D2 | Cue-cascade recursion re-anchors against the triggering event before its tombstone lands in `objects`: a structure anchored on {X, cue-of-X} can record `Reanchored{to: X}` then `CascadeDeleted` in one effect (contradictory repair trail; plausible by code trace, unexecuted) | `crates/epiphany-ops/DECISIONS.md` (Schema major 2, Phase D) | open |
| P13-D3 | `CreateCrossCutting` validates only event endpoints (`CrossCuttingValue::endpoints()`), so a SPANNER anchored to a missing region/measure mints dangling past `anchor_target_exists`; and non-event referent tombstones (`DeleteRegion` under a region-anchored spanner/repeat) re-anchor nothing — "every referenced endpoint is live" is events-only as implemented | `crates/epiphany-ops/DECISIONS.md` (Phase D follow-up) | open |
| P13-D3 | `CreateCrossCutting` validates only event endpoints (`CrossCuttingValue::endpoints()`), so a SPANNER anchored to a missing region/measure mints dangling past `anchor_target_exists`; and non-event referent tombstones (`DeleteRegion` under a region-anchored spanner/repeat) re-anchor nothing — "every referenced endpoint is live" is events-only as implemented | `crates/epiphany-ops/DECISIONS.md` (Phase D follow-up) | **resolved** (Pass 13: mint fixed via `anchor_object_refs`; non-event referent re-anchoring ratified events-only, user "fix the mint only") |