diff --git a/crates/epiphany-editor-core/src/lib.rs b/crates/epiphany-editor-core/src/lib.rs index 41c810c..f9e36e5 100644 --- a/crates/epiphany-editor-core/src/lib.rs +++ b/crates/epiphany-editor-core/src/lib.rs @@ -5322,6 +5322,37 @@ mod tests { ); } + #[test] + fn undo_of_a_transpose_restores_the_spelling_as_well_as_the_pitch() { + // EditorSession::undo re-materializes from a truncated log rather than + // riding the CRDT UndoTransaction path, so it exercises the reducer's + // spelling rewrite from the other side: the transpose must simply not + // happen, attachments and all. + use epiphany_core::{SpellingScope, SpellingSource}; + let mut session = open_rich(0x5EED); + let selection = click_a_notehead(&mut session); + let TypedObjectId::Pitch(pid) = selection.source else { + panic!("a notehead selects a pitch"); + }; + let before = session.current_pitch(pid).unwrap(); + + session.alter_selection(1).expect("sharpen"); + assert!(session.score().spelling_attachments.iter().any(|a| { + matches!(a.source, SpellingSource::Propagated { .. }) + && matches!(&a.scope, SpellingScope::Pitch(p) if *p == pid) + })); + + session.undo().expect("undo"); + assert_eq!(session.current_pitch(pid).unwrap(), before); + assert!( + !session.score().spelling_attachments.iter().any(|a| { + matches!(a.source, SpellingSource::Propagated { .. }) + && matches!(&a.scope, SpellingScope::Pitch(p) if *p == pid) + }), + "the propagated attachment did not survive the undo" + ); + } + #[test] fn undo_and_redo_a_transpose() { let mut session = open_rich(0x5EED); diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index cfa1371..036aa51 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -1320,3 +1320,76 @@ the other graph-aware-only preconditions"). It also *writes* nothing base-free, so the two modes agree on `objects`, and on the effect log for every operation whose targets are all transposable — the only case base-free reduction can distinguish. + +## Push 4a follow-up — the three gaps a green gate did not catch (2026-07-09) + +An audit reopened P12-K2 after Push 4a landed. All three findings reproduced. +The focused suites passed throughout, which is the point: they were coverage +gaps, not regressions. + +**1. Extreme intervals panicked instead of refusing.** `Pitch::transposed` did +its arithmetic in `i32` while `TranspositionInterval`'s components *are* `i32`, +so `diatonic_steps = i32::MAX` overflowed `12 * new_octave`. The comment above +it said "widen before arithmetic" — it widened `i8` to `i32`, which is exactly +not wide enough. `inverse()` negated `i32::MIN`. Now `i64` throughout, and +`inverse()` returns `Option`. + +I checked whether this was worse than a panic, since `epiphany-core` is a +library and a downstream release profile has `overflow-checks` off. A 10.5M-case +sweep of wrapping-vs-exact arithmetic found **zero** inputs where wrapping +produced a wrong `Ok` rather than a refusal. So: a panic, not silent corruption. +The audit's characterisation was right and my instinct was wrong. + +**2. The Propagated attachment met the requirement and missed its purpose.** +Default precedence ranks `UserChosen` and `Imported` *above* `Propagated` +(`SpellingPrecedence::default`), so the attachment a transpose writes is +outranked exactly when it matters. Reproduced: a C4 the author spelled "C", +sharpened to C♯4, resolves to `Authored(UserChosen)` with `accidentals: []`. The +notehead draws a C natural for a pitch sounding C♯ — the accidental disappears. +The Push-4a test could not see it because it deliberately started with no +attachment. + +Ratified fix: authored spellings are **moved**, not left and not discarded, by +transposing their **nominal** — the nominal is what carries the enharmonic +decision. B♯3 (sounding C4) up a fifth is F𝄪4 (sounding G4), not G. Source, +priority and layer are preserved: a transposed `UserChosen` spelling is still +the user's choice. An authored spelling that cannot be written at the transposed +position refuses the whole operation, resolved before any write. + +**3. Value-restoring undo did not restore either transpose.** Neither kind +recorded into `pitch_modify_chain`; `UndoTransaction(StrictInverse)` reduced to +`NoOp(TargetMissing)` and left the pitch shifted. `EditorSession::undo` works +because it re-materializes from a truncated log, an entirely separate mechanism. + +The *behaviour* gap was pre-existing — the frozen `Transpose` behaves the same, +and the pre-Push-4a catalog said so honestly ("an inverse-interval undo is a +Phase-3 refinement, P11-C8"). What was new was **my false claim** that the write +chain handled it, written into the catalog for both kinds. + +Ratified fix, and the interesting part: **`TransposeInterval` becomes undoable; +the frozen `Transpose` stays un-undoable, permanently.** Making `Transpose` +record into the chain would not change its own reduction rule, but it *would* +change what a stored `{Transpose, UndoTransaction}` history replays to — from +"the pitch stays shifted" to "the pitch returns". That is a change in what an +existing document means, which is the one thing the freeze forbids. So the +freeze bites, and gives another reason never to author the old kind. +`the_frozen_transpose_is_not_undoable_and_that_is_frozen_too` guards it, verified +by the inverse mutation (making it undoable fails the test). + +**The new chain.** `transposed_spelling_chain: BTreeMap>>` holds the engraved-layer, pitch-scoped, +explicit attachment *set* per pitch, so undo restores the moved authored +attachments and removes the propagated one together. Deliberately **not** +`respell_chain`: `RespellPitch` owns that, its last write is the LWW working +state its conflict detection reads, and folding transposes in would make a +concurrent respell conflict with a transpose *and* move the canonical bytes of +every existing history. + +**Two false locks, found by mutation, not by the gate.** +- The enharmonic test spelled a C♯4 pitch as "C♯", so the authored nominal + coincided with the pitch's own and re-inference gave the same answer. + Replacing `spelling.transposed(..)` with `simplest_spelling(..)` **passed**. + Rewritten around B♯3-sounding-C4, it fails as it must. +- 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. diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index da95568..c9fd21a 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -770,6 +770,13 @@ enum ValueRestoration { pitch: PitchId, predecessor: Option>, }, + /// 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 { + pitch: PitchId, + predecessor: Option>>, + }, CrossCutting { id: TypedObjectId, value: Option, @@ -867,6 +874,18 @@ 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. + /// + /// 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>>, event_modify_chain: BTreeMap>, pitch_modify_chain: BTreeMap>, cross_cutting_modify_chain: BTreeMap>, @@ -945,6 +964,18 @@ 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. + /// + /// 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>>, event_modify_chain: BTreeMap>, pitch_modify_chain: BTreeMap>, cross_cutting_modify_chain: BTreeMap>, @@ -1223,6 +1254,7 @@ impl<'a> Reducer<'a> { event_pitches: BTreeMap::new(), voice_occupancy: BTreeMap::new(), respell_chain: BTreeMap::new(), + transposed_spelling_chain: BTreeMap::new(), event_modify_chain: BTreeMap::new(), pitch_modify_chain: BTreeMap::new(), cross_cutting_modify_chain: BTreeMap::new(), @@ -1626,6 +1658,62 @@ impl<'a> Reducer<'a> { } } } + // Seed the transpose-owned attachment sets, so undoing the FIRST + // transpose of a base-seeded pitch restores the base's attachments + // rather than the ledger's key-absence. + let mut by_pitch: BTreeMap> = BTreeMap::new(); + for attachment in &score.spelling_attachments { + if let Some(pitch) = Self::transpose_owned_attachment(attachment) { + by_pitch.entry(pitch).or_default().push(attachment.clone()); + } + } + for (pitch, set) in by_pitch { + self.transposed_spelling_chain + .entry(pitch) + .or_insert_with(WriteChain::new) + .seed(set); + } + } + + /// The pitch whose spelling set `attachment` belongs to, if a + /// `TransposeInterval` would rewrite it: engraved layer, pitch-scoped, + /// explicit. Both the authored attachments it moves and the propagated one + /// it writes. + fn transpose_owned_attachment(attachment: &SpellingAttachment) -> Option { + if attachment.layer.is_some() { + return None; + } + let SpellingScope::Pitch(pitch) = &attachment.scope else { + return None; + }; + matches!(attachment.directive, SpellingDirective::Explicit(_)).then_some(*pitch) + } + + /// The current engraved-layer explicit attachment set for `pitch`, in the + /// graph's canonical order. + fn graph_spelling_set(&self, pitch: PitchId) -> Vec { + let Some(score) = self.graph.as_ref() else { + return Vec::new(); + }; + score + .spelling_attachments + .iter() + .filter(|a| Self::transpose_owned_attachment(a) == Some(pitch)) + .cloned() + .collect() + } + + /// Replaces `pitch`'s engraved-layer explicit attachment set with `set`, + /// leaving every other attachment (other pitches, other layers) untouched + /// and preserving the list's canonical order. + fn graph_replace_spelling_set(&mut self, pitch: PitchId, set: &[SpellingAttachment]) { + let Some(score) = self.graph.as_mut() else { + return; + }; + score + .spelling_attachments + .retain(|a| Self::transpose_owned_attachment(a) != Some(pitch)); + score.spelling_attachments.extend(set.iter().cloned()); } fn run(mut self) -> (MaterializedState, Option) { @@ -4855,6 +4943,22 @@ impl<'a> Reducer<'a> { } } } + for (pitch, chain) in &self.transposed_spelling_chain { + if !slot_live(TypedObjectId::Pitch(*pitch)) { + continue; + } + match chain.undo_verdict(tx) { + ChainUndoVerdict::NotWritten => {} + ChainUndoVerdict::Superseded { by } => superseded.push(by), + ChainUndoVerdict::Restore(predecessor) => { + restorations.push(ValueRestoration::TransposedSpellings { + pitch: *pitch, + predecessor, + }) + } + } + } + for (id, chain) in &self.cross_cutting_modify_chain { if !slot_live(*id) { continue; @@ -5044,6 +5148,17 @@ impl<'a> Reducer<'a> { self.graph_remove_respell(pitch); } }, + ValueRestoration::TransposedSpellings { pitch, predecessor } => { + let set: Vec = match predecessor { + Some(Predecessor::Write(set)) | Some(Predecessor::Base(set)) => set, + None => Vec::new(), + }; + self.transposed_spelling_chain + .entry(pitch) + .or_insert_with(WriteChain::new) + .record(env.id, env.transaction, set.clone()); + self.graph_replace_spelling_set(pitch, &set); + } ValueRestoration::CrossCutting { id, value } => { if let Some(value) = value { self.structures.insert(id, value.endpoints()); @@ -5572,7 +5687,7 @@ impl<'a> Reducer<'a> { /// can distinguish. fn transpose_interval( &mut self, - _env: &OperationEnvelope, + env: &OperationEnvelope, op: &TransposeIntervalOp, ) -> OperationEffect { if op @@ -5672,6 +5787,23 @@ impl<'a> Reducer<'a> { for r in &resolved { self.graph_propagate_spelling(r.pitch, &r.value); } + + // Value-restoring undo (`operation_catalog` §TransposeInterval). Record + // AFTER the graph writes, so the recorded spelling set is the + // post-transpose one and the chain's predecessor is the pre-transpose + // state. Restoring the pitch alone would leave a notehead spelled for a + // pitch that is no longer there. + for r in &resolved { + self.pitch_modify_chain + .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); + } OperationEffect::Applied } @@ -7005,6 +7137,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(), 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(), @@ -7040,6 +7173,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.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; @@ -9421,6 +9555,113 @@ mod tests { assert_eq!(cmn_of(&pitch_of(&score, pid)), (CmnNominal::C, 0, 4)); } + /// A declared transaction containing one `TransposeInterval`, plus a + /// `StrictInverse` undo of it. Returns the reduced score. + fn transpose_then_undo(base: &Score, pid: PitchId, iv: TranspositionInterval) -> Score { + let tx = TransactionId::new(ReplicaId(1), 900); + let tr = tx_member( + 1, + 1, + 11, + seen_r1(0), + tx, + OperationKind::TransposeInterval(TransposeIntervalOp { + targets: [pid].into_iter().collect(), + interval: iv, + }), + ); + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx), + tr, + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + set.reduce_onto(base).score + } + + #[test] + fn undoing_a_transpose_interval_restores_the_pitch_and_its_spelling() { + // operation_catalog §TransposeInterval, "Undo semantics". Before this, + // TransposeInterval never recorded into the pitch's value chain, so + // UndoTransaction(StrictInverse) reduced to NoOp(TargetMissing) and left + // the pitch shifted. + let (mut base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + author_spelling(&mut base, pid, PitchSpelling::cmn(CmnNominal::C, 4)); + let before_attachments = base.spelling_attachments.clone(); + + let score = transpose_then_undo(&base, pid, interval(4, 7)); + + // The pitch is back. + assert_eq!(cmn_of(&pitch_of(&score, pid)), (CmnNominal::C, 0, 4)); + // And so is its spelling: the moved UserChosen attachment is restored, + // and the Propagated one the transpose added is gone. Restoring the + // pitch alone would leave a notehead spelled for a pitch that is not + // there. + assert_eq!(score.spelling_attachments, before_attachments); + let (provenance, spelling) = engraved_spelling(&score, pid); + assert_eq!( + provenance, + epiphany_core::SpellingProvenance::Authored( + epiphany_core::SpellingSourceKind::UserChosen + ) + ); + assert_eq!(spelling.accidentals.len(), 0, "the sharp is gone again"); + } + + #[test] + fn undoing_a_transpose_of_an_unspelled_pitch_removes_the_propagated_attachment() { + // No authored spelling: the transpose adds a Propagated attachment where + // there was none. Undo must remove it, not leave it naming a pitch that + // no longer exists. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + assert!(base.spelling_attachments.is_empty()); + + let score = transpose_then_undo(&base, pid, interval(0, 1)); + assert_eq!(cmn_of(&pitch_of(&score, pid)), (CmnNominal::C, 0, 4)); + assert!( + score.spelling_attachments.is_empty(), + "undo removed the propagated attachment" + ); + } + + #[test] + fn the_frozen_transpose_is_not_undoable_and_that_is_frozen_too() { + // req:opcat:transpose-frozen. Transpose records no write into the value + // chain, so value-restoring undo leaves the shifted pitch shifted. + // + // This is a DEFECT, pinned. Making it record would not change its own + // reduction rule, but it WOULD change what a stored + // {Transpose, UndoTransaction} history replays to — from "the pitch stays + // shifted" to "the pitch returns" — and that is a change in what an + // existing document means. If this test ever "fails better", history has + // been rewritten. + let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4)); + let tx = TransactionId::new(ReplicaId(1), 900); + let tr = tx_member( + 1, + 1, + 11, + seen_r1(0), + tx, + OperationKind::Transpose(TransposeOp { + targets: vec![pid], + chromatic_steps: 1, + }), + ); + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx), + tr, + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = set.reduce_onto(&base); + assert_eq!( + cmn_of(&pitch_of(&out.score, pid)), + (CmnNominal::C, 1, 4), + "the frozen transpose is not undone by value restoration" + ); + } + #[test] fn transpose_interval_skips_a_tombstoned_target_but_refuses_a_missing_one() { // The skip/refuse distinction: a deleted pitch is not an untransposable