diff --git a/crates/epiphany-core/src/pitch.rs b/crates/epiphany-core/src/pitch.rs index 1923d27..3cd3e01 100644 --- a/crates/epiphany-core/src/pitch.rs +++ b/crates/epiphany-core/src/pitch.rs @@ -770,7 +770,8 @@ impl PitchSpelling { /// [`Pitch::twelve_tet_semitone`]. /// /// So B♯3 (sounding C4) transposed by a perfect fifth `(4, 7)` becomes - /// F×3 (sounding G4): the letter moved four diatonic steps, and the + /// F×4 (sounding G4): the letter moved four diatonic steps — B→F carries + /// the octave — and the /// double-sharp is what F needs to sound a G. The chromatic component never /// touches the spelling directly; it reaches it only through the pitch. /// diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index 036aa51..8e240a9 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -1393,3 +1393,46 @@ every existing history. - My own mutation harness restored the file between two tests, so the second ran unmutated and "passed". A mutation that no-ops looks exactly like a test that passes — the trap recorded after Push 4a, hit again in a new form. + +## P13-S3 — a shared undo key with one writer (2026-07-09) + +The `engraved_spelling_chain` added to make `TransposeInterval` undoable was +written only by the transpose. But `RespellPitch` mutates the same graph +attachments, and a chain with one writer is wrong in **both** directions: + +- **Prior respell erased.** `respell → [tx: transpose] → StrictInverse undo` + returned `Applied`, restored the pitch to C4, and removed *every* attachment. + The respell was an operation, not part of the base, so it existed only as a + chain write — and the transpose's chain had never seen it, so its predecessor + was absence. +- **Later respell wiped.** `[tx: transpose] → respell → StrictInverse undo` + returned `Applied` and erased the newer authoring, because the respell was + invisible to the chain and so did not register as a superseding writer. The + catalog's general rule is that a later canonical writer supersedes a strict + undo. +- **Best-effort split the unit.** With the spelling set superseded but the pitch + value not, `BestEffort` restored the pre-transpose pitch and left a spelling + authored against the transposed one attached to it. + +**Fix.** Both operations record on the shared key (`record_engraved_spellings`), +and the pitch value and its spelling set undo as one unit: if either half is +superseded, neither is restored. `StrictInverse` already refuses on any +supersession, so the coupling only bites for `BestEffort`. + +**The physical separation stands, and my earlier note was only half right.** I +kept `engraved_spelling_chain` distinct from `respell_chain` because the latter +is `RespellPitch`'s LWW working state, read by its concurrent-differing conflict +detection — folding transposes in would make a concurrent respell *conflict* with +a transpose and would move the canonical bytes of every existing history. That +reasoning holds. What it did **not** license was letting one operation own the +key. Two physical chains, two responsibilities (`respell_chain`: the ledger +spelling and the LWW verdict; `engraved_spelling_chain`: the graph attachments), +but *every* writer of the attachments records on the attachment chain. + +Recording is gated on `self.graph.is_some()`, so base-free reduction is +byte-unchanged and the seeded fuzz corpus's canonical-base digest does not move. + +Spec: `req:opcat:spelling-set-chain`. Mutation-verified: removing the respell's +record fails all three new tests; removing the coupling fails the best-effort +one with the pitch back at C4 and the spelling still at C-sharp. Also covered: +both permutations of a concurrent respell/transpose reduce to identical bytes. diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index c9fd21a..fdf7993 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -773,7 +773,7 @@ enum ValueRestoration { /// The engraved-layer explicit spelling attachments a `TransposeInterval` /// rewrote, restored as a set. `None` predecessor means the pitch carried /// none before, so they are removed. - TransposedSpellings { + EngravedSpellings { pitch: PitchId, predecessor: Option>>, }, @@ -874,18 +874,25 @@ struct Reducer<'a> { // what value-restoring undo walks. Advisory families (metadata, breaks, // staff layout) keep chains for undo but record no conflicts. respell_chain: BTreeMap>, - /// The engraved-layer, pitch-scoped, explicit spelling attachments a - /// `TransposeInterval` rewrites (`req:opcat:transpose-interval-spelling`): - /// the moved authored ones and the propagated one, as a single per-pitch - /// value so undo restores them together. + /// A pitch's engraved-layer, pitch-scoped, explicit spelling attachment + /// **set**, as one value. Written by *every* operation that changes it: + /// `RespellPitch` and `TransposeInterval` alike (P13-S3). /// - /// Deliberately NOT `respell_chain`. `RespellPitch` owns that chain, and - /// its last write is the LWW working state its concurrent-differing - /// conflict detection reads; folding transposes into it would make a - /// concurrent respell conflict with a transpose and would move the - /// canonical bytes of every existing history. A transpose that also moves a - /// `UserChosen` spelling is restored from here. - transposed_spelling_chain: BTreeMap>>, + /// Both must record here or undo is wrong in both directions. If only the + /// transpose recorded, a prior respell would not be its chain-predecessor + /// and undoing the transpose would erase the respell; and a *later* respell + /// would be invisible, so a strict undo would report `Applied` and wipe it + /// instead of refusing as superseded. + /// + /// This is a *second* physical chain, not a replacement for `respell_chain`: + /// that one is `RespellPitch`'s LWW working state, read by its + /// concurrent-differing conflict detection, and folding transposes into it + /// would make a concurrent respell conflict with a transpose and move the + /// canonical bytes of every existing history. This chain owns the *graph + /// attachments*; `respell_chain` owns the *ledger spelling* and the LWW + /// verdict. Only ever written when a graph is present, so base-free + /// reduction is byte-unchanged. + engraved_spelling_chain: BTreeMap>>, event_modify_chain: BTreeMap>, pitch_modify_chain: BTreeMap>, cross_cutting_modify_chain: BTreeMap>, @@ -964,18 +971,25 @@ struct WorkingSnapshot { event_pitches: BTreeMap>, voice_occupancy: BTreeMap>, respell_chain: BTreeMap>, - /// The engraved-layer, pitch-scoped, explicit spelling attachments a - /// `TransposeInterval` rewrites (`req:opcat:transpose-interval-spelling`): - /// the moved authored ones and the propagated one, as a single per-pitch - /// value so undo restores them together. + /// A pitch's engraved-layer, pitch-scoped, explicit spelling attachment + /// **set**, as one value. Written by *every* operation that changes it: + /// `RespellPitch` and `TransposeInterval` alike (P13-S3). /// - /// Deliberately NOT `respell_chain`. `RespellPitch` owns that chain, and - /// its last write is the LWW working state its concurrent-differing - /// conflict detection reads; folding transposes into it would make a - /// concurrent respell conflict with a transpose and would move the - /// canonical bytes of every existing history. A transpose that also moves a - /// `UserChosen` spelling is restored from here. - transposed_spelling_chain: BTreeMap>>, + /// Both must record here or undo is wrong in both directions. If only the + /// transpose recorded, a prior respell would not be its chain-predecessor + /// and undoing the transpose would erase the respell; and a *later* respell + /// would be invisible, so a strict undo would report `Applied` and wipe it + /// instead of refusing as superseded. + /// + /// This is a *second* physical chain, not a replacement for `respell_chain`: + /// that one is `RespellPitch`'s LWW working state, read by its + /// concurrent-differing conflict detection, and folding transposes into it + /// would make a concurrent respell conflict with a transpose and move the + /// canonical bytes of every existing history. This chain owns the *graph + /// attachments*; `respell_chain` owns the *ledger spelling* and the LWW + /// verdict. Only ever written when a graph is present, so base-free + /// reduction is byte-unchanged. + engraved_spelling_chain: BTreeMap>>, event_modify_chain: BTreeMap>, pitch_modify_chain: BTreeMap>, cross_cutting_modify_chain: BTreeMap>, @@ -1254,7 +1268,7 @@ impl<'a> Reducer<'a> { event_pitches: BTreeMap::new(), voice_occupancy: BTreeMap::new(), respell_chain: BTreeMap::new(), - transposed_spelling_chain: BTreeMap::new(), + engraved_spelling_chain: BTreeMap::new(), event_modify_chain: BTreeMap::new(), pitch_modify_chain: BTreeMap::new(), cross_cutting_modify_chain: BTreeMap::new(), @@ -1668,7 +1682,7 @@ impl<'a> Reducer<'a> { } } for (pitch, set) in by_pitch { - self.transposed_spelling_chain + self.engraved_spelling_chain .entry(pitch) .or_insert_with(WriteChain::new) .seed(set); @@ -3185,6 +3199,27 @@ impl<'a> Reducer<'a> { .or_insert_with(WriteChain::new) .record(env.id, env.transaction, op.spelling.clone()); self.graph_respell_pitch(op.pitch, &op.spelling); + // A respell changes the graph attachment set, so it is a writer on + // `engraved_spelling_chain` too (P13-S3). Without this, a transpose + // undone after a respell would erase it, and a respell landing after a + // transposed transaction would be silently wiped by that undo instead + // of superseding it. + self.record_engraved_spellings(env, op.pitch); + } + + /// Records `pitch`'s current graph attachment set as a write on + /// [`Self::engraved_spelling_chain`]. A no-op under base-free reduction, + /// which has no graph attachments to own — so base-free canonical bytes do + /// not move. + fn record_engraved_spellings(&mut self, env: &OperationEnvelope, pitch: PitchId) { + if self.graph.is_none() { + return; + } + let set = self.graph_spelling_set(pitch); + self.engraved_spelling_chain + .entry(pitch) + .or_insert_with(WriteChain::new) + .record(env.id, env.transaction, set); } fn graph_respell_pitch(&mut self, pitch: PitchId, spelling: &PitchSpelling) { @@ -4894,6 +4929,14 @@ impl<'a> Reducer<'a> { ) -> (Vec, Vec) { let mut restorations = Vec::new(); let mut superseded: Vec = Vec::new(); + // A `TransposeInterval` writes a pitch's value and its engraved spelling + // set as one act, so they undo as one unit (P13-S3). If either half was + // superseded, neither is restored: `BestEffort` must not put the pitch + // back while leaving a spelling written for the pitch it used to be. + // (`StrictInverse` refuses outright on any supersession, so this only + // bites for `BestEffort`.) + let mut superseded_pitches: std::collections::BTreeSet = + std::collections::BTreeSet::new(); let slot_live = |obj: TypedObjectId| { matches!(self.objects.get(&obj), Some(ObjectState::Live)) && !targets.contains(&obj) }; @@ -4919,7 +4962,10 @@ impl<'a> Reducer<'a> { } match chain.undo_verdict(tx) { ChainUndoVerdict::NotWritten => {} - ChainUndoVerdict::Superseded { by } => superseded.push(by), + ChainUndoVerdict::Superseded { by } => { + superseded.push(by); + superseded_pitches.insert(*pitch); + } ChainUndoVerdict::Restore(predecessor) => { restorations.push(ValueRestoration::Pitch { pitch: *pitch, @@ -4943,15 +4989,18 @@ impl<'a> Reducer<'a> { } } } - for (pitch, chain) in &self.transposed_spelling_chain { + for (pitch, chain) in &self.engraved_spelling_chain { if !slot_live(TypedObjectId::Pitch(*pitch)) { continue; } match chain.undo_verdict(tx) { ChainUndoVerdict::NotWritten => {} - ChainUndoVerdict::Superseded { by } => superseded.push(by), + ChainUndoVerdict::Superseded { by } => { + superseded.push(by); + superseded_pitches.insert(*pitch); + } ChainUndoVerdict::Restore(predecessor) => { - restorations.push(ValueRestoration::TransposedSpellings { + restorations.push(ValueRestoration::EngravedSpellings { pitch: *pitch, predecessor, }) @@ -5090,6 +5139,20 @@ impl<'a> Reducer<'a> { } } } + // Couple the two halves a transpose writes together. Dropping a `Pitch` + // restoration whose spelling set was superseded (and vice versa) is what + // makes them one undo unit. It cannot mis-fire on an unrelated operation: + // a chain reports `Superseded` only when the transaction actually wrote + // it, and `ModifyIdentifiedPitch` never writes the spelling set. + if !superseded_pitches.is_empty() { + restorations.retain(|r| match r { + ValueRestoration::Pitch { pitch, .. } + | ValueRestoration::EngravedSpellings { pitch, .. } => { + !superseded_pitches.contains(pitch) + } + _ => true, + }); + } superseded.sort(); superseded.dedup(); (restorations, superseded) @@ -5148,12 +5211,12 @@ impl<'a> Reducer<'a> { self.graph_remove_respell(pitch); } }, - ValueRestoration::TransposedSpellings { pitch, predecessor } => { + ValueRestoration::EngravedSpellings { pitch, predecessor } => { let set: Vec = match predecessor { Some(Predecessor::Write(set)) | Some(Predecessor::Base(set)) => set, None => Vec::new(), }; - self.transposed_spelling_chain + self.engraved_spelling_chain .entry(pitch) .or_insert_with(WriteChain::new) .record(env.id, env.transaction, set.clone()); @@ -5798,11 +5861,7 @@ impl<'a> Reducer<'a> { .entry(r.pitch) .or_insert_with(WriteChain::new) .record(env.id, env.transaction, r.value.clone()); - let set = self.graph_spelling_set(r.pitch); - self.transposed_spelling_chain - .entry(r.pitch) - .or_insert_with(WriteChain::new) - .record(env.id, env.transaction, set); + self.record_engraved_spellings(env, r.pitch); } OperationEffect::Applied } @@ -7137,7 +7196,7 @@ impl<'a> Reducer<'a> { event_pitches: self.event_pitches.clone(), voice_occupancy: self.voice_occupancy.clone(), respell_chain: self.respell_chain.clone(), - transposed_spelling_chain: self.transposed_spelling_chain.clone(), + engraved_spelling_chain: self.engraved_spelling_chain.clone(), event_modify_chain: self.event_modify_chain.clone(), pitch_modify_chain: self.pitch_modify_chain.clone(), cross_cutting_modify_chain: self.cross_cutting_modify_chain.clone(), @@ -7173,7 +7232,7 @@ impl<'a> Reducer<'a> { self.event_pitches = s.event_pitches; self.voice_occupancy = s.voice_occupancy; self.respell_chain = s.respell_chain; - self.transposed_spelling_chain = s.transposed_spelling_chain; + self.engraved_spelling_chain = s.engraved_spelling_chain; self.event_modify_chain = s.event_modify_chain; self.pitch_modify_chain = s.pitch_modify_chain; self.cross_cutting_modify_chain = s.cross_cutting_modify_chain; @@ -9662,6 +9721,222 @@ mod tests { ); } + // --- P13-S3: RespellPitch and TransposeInterval share the engraved + // spelling set, so undo must see both. --------------------------------- + + fn respell_env( + replica: u64, + counter: u64, + physical: i64, + ctx: CausalContext, + pitch: PitchId, + nominal: CmnNominal, + ) -> OperationEnvelope { + prim_env( + replica, + counter, + physical, + ctx, + OperationKind::RespellPitch(RespellPitchOp { + pitch, + spelling: PitchSpelling::cmn(nominal, 4), + }), + ) + } + + fn transpose_member( + replica: u64, + counter: u64, + physical: i64, + ctx: CausalContext, + tx: TransactionId, + pitch: PitchId, + iv: TranspositionInterval, + ) -> OperationEnvelope { + tx_member( + replica, + counter, + physical, + ctx, + tx, + OperationKind::TransposeInterval(TransposeIntervalOp { + targets: [pitch].into_iter().collect(), + interval: iv, + }), + ) + } + + /// `(source, nominal, accidental count)` of every engraved-layer explicit + /// attachment on `pitch`. + fn attachments_of(score: &Score, pitch: PitchId) -> Vec<(SpellingSource, CmnNominal, usize)> { + score + .spelling_attachments + .iter() + .filter(|a| a.layer.is_none()) + .filter(|a| matches!(&a.scope, SpellingScope::Pitch(p) if *p == pitch)) + .filter_map(|a| match (&a.directive, &a.source) { + (SpellingDirective::Explicit(sp), src) => match sp.nominal { + epiphany_core::SpellingNominal::Cmn(n) => { + Some((src.clone(), n, sp.accidentals.len())) + } + _ => None, + }, + _ => None, + }) + .collect() + } + + fn undo_effect(state: &MaterializedState, id: OperationId) -> OperationEffect { + state + .effects + .iter() + .find(|(e, _)| *e == id) + .map(|(_, eff)| eff.clone()) + .expect("effect recorded") + } + + #[test] + fn undoing_a_transpose_restores_a_prior_respell() { + // P13-S3, direction one. The respell is an OPERATION, not part of the + // base, so it exists only as a write on the shared chain. Before the + // fix, the transpose's chain had no predecessor for it and the undo + // wiped every attachment on the pitch. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + let tx = TransactionId::new(ReplicaId(1), 900); + let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::StrictInverse); + let undo_id = undo.id; + + let mut set = OperationSet::new(); + set.accept_all(vec![ + respell_env(1, 0, 10, CausalContext::new(), pid, CmnNominal::C), + declare_transaction(1, 1, 11, seen_r1(0), tx), + transpose_member(1, 2, 12, seen_r1(1), tx, pid, interval(0, 1)), + undo, + ]); + let out = set.reduce_onto(&base); + + assert_eq!(undo_effect(&out.state, undo_id), OperationEffect::Applied); + assert_eq!(cmn_of(&pitch_of(&out.score, pid)), (CmnNominal::C, 0, 4)); + assert_eq!( + attachments_of(&out.score, pid), + vec![(SpellingSource::UserChosen, CmnNominal::C, 0)], + "the prior respell survives the undo, and the propagated one is gone" + ); + } + + #[test] + fn a_respell_after_a_transposed_transaction_supersedes_its_strict_undo() { + // P13-S3, direction two. The respell lands canonically AFTER the + // transaction, so it is a later writer on the pitch's spelling set: + // strict undo must refuse rather than erase it. Before the fix the + // respell was invisible to the transpose's chain, so the undo reported + // Applied and wiped the newer authoring. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + let tx = TransactionId::new(ReplicaId(1), 900); + let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::StrictInverse); + let undo_id = undo.id; + + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx), + transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)), + respell_env(1, 2, 12, seen_r1(1), pid, CmnNominal::D), + undo, + ]); + let out = set.reduce_onto(&base); + + assert!( + matches!( + undo_effect(&out.state, undo_id), + OperationEffect::Conflicted { .. } + ), + "a later canonical writer supersedes a strict undo" + ); + // Nothing was rolled back: the pitch stays transposed and the newer + // authored spelling stands. + assert_eq!(cmn_of(&pitch_of(&out.score, pid)), (CmnNominal::C, 1, 4)); + let atts = attachments_of(&out.score, pid); + assert!( + atts.contains(&(SpellingSource::UserChosen, CmnNominal::D, 0)), + "the later respell was not erased: {atts:?}" + ); + } + + #[test] + fn best_effort_undo_will_not_restore_a_pitch_whose_spelling_was_superseded() { + // The pitch value and its engraved spelling set are one undo unit. + // Restoring the pitch alone would leave a spelling authored against the + // transposed pitch attached to the pitch it used to be. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + let tx = TransactionId::new(ReplicaId(1), 900); + let undo = undo_env(1, 3, 13, seen_r1(2), tx, UndoPolicy::BestEffort); + let undo_id = undo.id; + + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx), + transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)), + respell_env(1, 2, 12, seen_r1(1), pid, CmnNominal::D), + undo, + ]); + let out = set.reduce_onto(&base); + + assert_eq!(undo_effect(&out.state, undo_id), OperationEffect::Applied); + assert_eq!( + cmn_of(&pitch_of(&out.score, pid)), + (CmnNominal::C, 1, 4), + "best-effort skipped the pitch because its spelling set was superseded" + ); + assert!(attachments_of(&out.score, pid).contains(&( + SpellingSource::UserChosen, + CmnNominal::D, + 0 + ))); + } + + #[test] + fn a_concurrent_respell_and_transpose_converge_in_canonical_order() { + // Neither sees the other. Both write the pitch's engraved spelling set, + // so the canonically-last writer owns it — and both permutations of the + // input reduce to the same score, which is the only property that + // matters. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + let tx = TransactionId::new(ReplicaId(1), 900); + + let build = || { + vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx), + // Concurrent: replica 2's respell has not seen replica 1's + // transpose, and vice versa. + transpose_member(1, 1, 11, seen_r1(0), tx, pid, interval(0, 1)), + respell_env(2, 0, 12, CausalContext::new(), pid, CmnNominal::D), + ] + }; + let mut forward = OperationSet::new(); + forward.accept_all(build()); + let a = forward.reduce_onto(&base); + + let mut reversed = OperationSet::new(); + let mut envs = build(); + envs.reverse(); + reversed.accept_all(envs); + let b = reversed.reduce_onto(&base); + + assert_eq!(a.score, b.score, "reduction is permutation-invariant"); + assert_eq!(a.state.canonical_bytes(), b.state.canonical_bytes()); + // The pitch moved; exactly one authored spelling stands, plus the + // propagated record. + assert_eq!(cmn_of(&pitch_of(&a.score, pid)), (CmnNominal::C, 1, 4)); + let atts = attachments_of(&a.score, pid); + assert_eq!( + atts.iter() + .filter(|(s, _, _)| matches!(s, SpellingSource::UserChosen)) + .count(), + 1, + "one authored spelling: {atts:?}" + ); + } + #[test] fn transpose_interval_skips_a_tombstoned_target_but_refuses_a_missing_one() { // The skip/refuse distinction: a deleted pitch is not an untransposable diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 46b206b..e48b903 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -41,13 +41,16 @@ batch reopens the pass. | P13-I2 | `Staff::default_clef` is never consulted: `to_constrained` takes the active clef from the staff instance's `clef_sequence` and falls back to `Clef::default()` (treble), so a bass-clef staff that declares its clef only on the `Staff` engraves as treble. The field is decorative in the projection — is it the fallback, or should it not exist? | `crates/epiphany-layout-ir/DECISIONS.md` ("`Staff::default_clef` is never consulted") | **resolved** (Pass 13: it IS the fallback. `StaffContent` carries it, `active_clef_or` resolves against it, and `editor-core`'s hit-test reads the same function — else a click on a bass staff would resolve its pitch as treble. Removal was rejected: the field is named for its purpose, is encoded on the wire, and dropping it is schema-major) | | P13-I3 | `BRAVURA_METRICS`' `NOTEHEAD_ANCHORS` are hand-written, unconsumed, and doubly suspect: they name `stemUpNW`/`stemDownSE` — the corners a normal notehead's stems do *not* attach to, and a pair Bravura's `noteheadBlack` does not define — and their x of `1180` reads like 1.18 staff spaces written in thousandths rather than the table's `1/1024` units (1.18 sp = 1208). They enter only `metrics_hash`, so any correction moves the `GlyphCatalogIdentity` every conformance claim declares. The font is not vendored, so the values cannot be verified in-tree | `crates/epiphany-layout-ir/DECISIONS.md` ("the notehead stem anchors are unusable as written") | **resolved** (Pass 13: deleted. Unverifiable in-tree, unconsumed, and hand-derived where every neighbouring number is machine-extracted. `extract_bravura_outlines.py --anchors` now emits them from the pinned `bravura_metadata.json`, so the table regains them generated rather than remembered; the metadata's SHA-256 is deliberately unpinned and the script refuses until an operator with the font pins it. `GlyphCatalogIdentity` moves once, now, while no conformance claim declares the old one; user "delete them + teach the extractor") | -## Open candidates (Batch 3 not yet open) +## Batch 3 — OPEN (2026-07-09) -Filed as found; the pass reopens at three (the house rule). Neither is a live -incorrectness — each is a place where the spec cannot yet support a claim it -makes about itself. +Three candidates, so the pass reopens per the house rule. P13-S3 arrived as a +**live incorrectness** — a Push-4a follow-up audit found that the spelling-set +chain introduced to make `TransposeInterval` undoable had only one writer, so +undo erased an ordinary `RespellPitch` on either side of it. It is resolved. +S1 and S2 remain open. | Id | One-line statement | Filed in | Status | |---|---|---|---| | P13-S1 | **169 of core_spec's 207 `requirement` blocks carry no `\label`**, so no conformance claim can cite them. Chapter 4 (`Tuning Systems and Pitch Spaces`) is 9/9 unlabeled and Chapter 11 (`Determinism Contract`) is 15/15, but the gap is universal, not local: `Semantic Operations` 24/27, `The Score Graph` 22/28, `Pitch` 10/13. The requirements *are* normative and *are* implemented; they simply cannot be named. Every `req:*` label the repo cites was added ad hoc by the pass that needed it | this file | **open** (found while auditing Push 4a; the audit that surfaced it scoped it to Chapter 4, which is where it was noticed, not where it lives) | | P13-S2 | `cmn-24` is declared in the built-in pitch-space table (`core_spec.tex` §"Built-in Catalog") as "CMN extended with 24-EDO quarter-tone accidentals", but **cannot be represented**: `PitchSpacePosition::Cmn.alteration` is an `i8` documented as *whole semitones*, and a quarter-tone is half of one. Either the space is not `Cmn`-representable (and needs `Integer`/`Registered`), or `alteration` needs a finer unit — a data-model major | `crates/epiphany-core/DECISIONS.md` (Push 4b blockers) | **open** (blocks Push 4b) | +| P13-S3 | The `engraved_spelling_chain` introduced with `TransposeInterval`'s undo had a **single writer**. `RespellPitch` mutates the same graph attachments but recorded only on `respell_chain`, so (a) undoing a transposed transaction after a prior respell restored the pitch and **erased the respell**, and (b) a respell landing canonically *after* the transaction was invisible to the chain, so a `StrictInverse` undo reported `Applied` and **wiped the newer authoring** instead of refusing as superseded. A `BestEffort` undo could also restore the pre-transpose pitch while leaving a spelling authored against the transposed one | `crates/epiphany-ops/DECISIONS.md` (P13-S3) | **resolved** (both operations now record on the shared key; pitch value + spelling set undo as one unit; new `req:opcat:spelling-set-chain`. The chain stays *physically* separate from `respell_chain`, which is `RespellPitch`'s LWW conflict state — folding transposes in would make a concurrent respell conflict with a transpose and move the canonical bytes of every existing history) | diff --git a/spec/operation_catalog.pdf b/spec/operation_catalog.pdf index 79abe7c..bcd8bca 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 ad605ef..e2db626 100644 --- a/spec/operation_catalog.tex +++ b/spec/operation_catalog.tex @@ -786,12 +786,40 @@ is transposed by \texttt{interval}. \textbf{Undo semantics.} Nothing is minted. \texttt{TransposeInterval} \MUST{} record each transposed pitch's new value into that pitch's value chain, -and each spelling attachment it rewrote into the corresponding spelling chain, so -that value-restoring undo recovers the pre-transpose pitch \emph{and} its -pre-transpose spelling. Restoring the pitch alone would leave a notehead spelled -for a pitch that no longer exists. This is where \texttt{TransposeInterval} -departs from the frozen \texttt{Transpose}, which records nothing and is -therefore not undoable. +and that pitch's resulting \emph{engraved spelling set} into the spelling-set +chain, so that value-restoring undo recovers the pre-transpose pitch \emph{and} +its pre-transpose spelling. Restoring the pitch alone would leave a notehead +spelled for a pitch that no longer exists. This is where +\texttt{TransposeInterval} departs from the frozen \texttt{Transpose}, which +records nothing and is therefore not undoable. + +\begin{requirement} + \label{req:opcat:spelling-set-chain} + The pitch's engraved spelling set is a single undo key with \emph{more than + one writer}. Every operation that changes it --- \texttt{RespellPitch} and + \texttt{TransposeInterval} alike --- \MUST{} record a write on that key. + Consequently a \texttt{RespellPitch} causally prior to a transposed + transaction is that transaction's chain-predecessor and is restored by its + undo; and a \texttt{RespellPitch} canonically \emph{later} supersedes the + transaction's write, so a \texttt{StrictInverse} undo conflicts rather than + erasing it, per the general superseded-writer rule. + + A pitch's value and its engraved spelling set \MUST{} undo as one unit: if + either is superseded, neither is restored. A \texttt{BestEffort} undo + \MUSTNOT{} restore the pre-transpose pitch while leaving a spelling authored + against the transposed one. +\end{requirement} + +\begin{rationale} + Ratified as P13-S3. An implementation may keep the spelling-set chain + physically separate from whatever chain drives \texttt{RespellPitch}'s + last-writer-wins conflict detection --- the reference implementation does, + because folding transposes into that chain would make a concurrent respell + \emph{conflict} with a transpose and would move the canonical bytes of every + existing history. What it may not do is let one writer own the key. A chain + with a single writer cannot see the other's prior value (so undo erases it) and + cannot see the other's later value (so undo overwrites it). +\end{rationale} An inverse interval usually exists ($(-d, -c)$), because the reduction never saturates --- but not always: $\texttt{i32::MIN}$ has no negation. Undo does not