diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index 0832e83..d6f94f5 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -965,16 +965,25 @@ each fixed with a regression test: `precondition_failure_reason`/`reanchor_reason` never emitted discriminants 12/13/6, so fuzz gates could not catch a renumbering regression. Fixed. -**Pass-13 candidate (P13-K1, filed not fixed):** the K3 verdict for a system -pitch *introduced by a ModifyEvent replacement value* (never minted — the -collision pre-walk deliberately excludes ModifyEvent) differs across a -snapshot cut: in-session the pitch is not Live (`TargetMissing`); after a -snapshot re-seeds objects + registry from the base graph, the same modify -reads `SystemDerivedContentImmutable`. The asymmetry **predates K3** (the -same split previously read `TargetMissing` vs a silent `Applied` rewrite) and -is a ModifyEvent-introduction question — whether a replacement value may -introduce never-minted pitch ids at all — batched for Pass 13, not -improvised here. +**Pass-13 candidate (P13-K1) — resolved (Pass 13, 2026-07-08; user: "reject +the introduction").** The K3 verdict for a system pitch *introduced by a +ModifyEvent replacement value* (never minted — the collision pre-walk excludes +ModifyEvent) differed across a snapshot cut: in-session the pitch was not Live +(slipped through — `system_mints` had no entry, so the identity check saw +nothing); after a snapshot re-seeded objects + registry from the base graph, +the same modify read `SystemDerivedContentImmutable`. + +Resolved by rejecting the introduction: `modify_event` now refuses a +replacement that carries a **never-minted system-derived pitch id** (replica +`SYSTEM_DERIVED`, absent-or-not-Live in `objects`) with `TargetMissing`, +*before* the P12-K3 identity check. The verdict no longer depends on the +registry — the pitch is not live in `objects` in either frame — so both frames +refuse identically, closing the asymmetry. Scoped to the system namespace +(where the asymmetry lives: only system pitches are re-seeded as system mints): +a user-replica pitch carries no namespace claim and has no snapshot asymmetry, +so `ModifyEvent` may still introduce user pitch content (the concurrent-modify +tests rely on it). Locked by +`a_modify_event_introducing_a_never_minted_system_pitch_is_refused_p13_k1`. ## Schema major 2: minimal stamping (landed with core Phase B, deliberately) diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index c2903cc..929dc29 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -5215,11 +5215,37 @@ impl<'a> Reducer<'a> { } Some(ObjectState::Live) => {} } + let mut carried = Vec::new(); + op.event.collect_identified_pitches(&mut carried); + // Introduction precondition (P13-K1, ratified: reject the + // introduction) before the identity one: a `ModifyEvent` may not + // *introduce* a never-minted SYSTEM-DERIVED pitch id — that id lives in + // the reserved system namespace and only the system mints it. A carried + // system-derived pitch absent from `objects` (never minted) is refused, + // consistently across a snapshot cut: this closes the asymmetry where + // an introduced system pitch slipped through in-session (`system_mints` + // had no entry, so the identity check below saw nothing) yet read + // `SystemDerivedContentImmutable` once a snapshot re-seeded it as a + // system mint. A user-replica pitch carries no such namespace claim and + // has no snapshot asymmetry, so it is untouched here; the event's own + // live system pitches are in `objects` (both reduction modes), so an + // in-place content rewrite passes. + if carried.iter().any(|ip| { + ip.id.replica() == ReplicaId::SYSTEM_DERIVED + && !matches!( + self.objects.get(&TypedObjectId::Pitch(ip.id)), + Some(ObjectState::Live) + ) + }) { + return OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::TargetMissing, + }, + }; + } // Identity precondition (P12-K3) before the placement precondition: // a replacement value that rewrites a system-derived pitch's // intrinsic content in place is refused outright. - let mut carried = Vec::new(); - op.event.collect_identified_pitches(&mut carried); if carried .iter() .any(|ip| self.system_derived_rewrite(ip.id, &ip.pitch)) @@ -9485,6 +9511,62 @@ mod tests { ); } + #[test] + fn a_modify_event_introducing_a_never_minted_system_pitch_is_refused_p13_k1() { + // P13-K1 (ratified: reject the introduction). The INTRODUCTION sibling + // of the p12_k3 rewrite refusal: a ModifyEvent whose replacement + // carries a *never-minted* system-derived pitch id is refused + // (`TargetMissing`) — the system namespace is the system's to mint. + // Before the fix this slipped through in-session (`system_mints` had no + // entry, so the identity check saw nothing) yet read + // `SystemDerivedContentImmutable` after a snapshot re-seeded the pitch + // as a system mint — the snapshot-cut asymmetry the candidate named. + // The verdict no longer depends on the registry: the pitch is not live + // in `objects` in either frame, so both refuse identically. + use epiphany_core::derive_system_pitch_id; + let content = crate::valuegen::pitch_value_nth(3); + let system_id = derive_system_pitch_id(&content); // never minted + + // A live, pitchless event modified to CARRY the never-minted system + // pitch (an introduction, not an in-place rewrite). + let insert = insert(1, 0, 10, 1, 100, 0); + let replacement = crate::valuegen::insert_event_value( + EventId::new(ReplicaId(1), 100), + VoiceId::new(ReplicaId(9), 1), + pos(0), + epiphany_core::MusicalDuration::whole(), + &[system_id], + ); + let modify = prim_env( + 1, + 1, + 20, + seen_r1(0), + OperationKind::ModifyEvent(ModifyEventOp { event: replacement }), + ); + let mut set = OperationSet::new(); + set.accept_all(vec![insert, modify.clone()]); + let state = set.reduce(); + + assert_eq!( + state + .effects + .iter() + .find(|(e, _)| *e == modify.id) + .map(|(_, eff)| eff), + Some(&OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::TargetMissing, + }, + }), + "a ModifyEvent introducing a never-minted system pitch is refused" + ); + assert!( + !state.objects.contains_key(&TypedObjectId::Pitch(system_id)), + "the introduced system pitch never enters the ledger" + ); + } + #[test] fn a_rank_four_reanchor_records_same_canvas_nearer_p12_c4() { // Pass 12 (P12-C4): the rank-4 (same-canvas) proximity survivor has diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 5f5cf59..b58de43 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -7,7 +7,7 @@ this file is the index, not the analysis. | Id | One-line statement | Filed in | Status | |---|---|---|---| -| 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-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) | **resolved** (Pass 13: reject the introduction — modify_event refuses a never-minted system-derived pitch, verdict now snapshot-cut-invariant; user "reject the introduction") | | 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) | **resolved** (Pass 13: mint fixed via `anchor_object_refs`; non-event referent re-anchoring ratified events-only, user "fix the mint only") |