TransposeInterval becomes undoable; the frozen Transpose stays un-undoable

Audit finding 3, reproduced and fixed. Neither transpose recorded into
pitch_modify_chain, so UndoTransaction(StrictInverse) over a transaction
containing one reduced to NoOp(TargetMissing) and left the pitch shifted.
EditorSession::undo works only because it re-materializes from a truncated log,
which is a different mechanism entirely.

The behaviour gap was pre-existing: the frozen Transpose does 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 claim, written into the catalog for
both kinds, that the write chain handled it. It did not.

Per the ratified call, the fix is asymmetric, and the asymmetry is the point.
TransposeInterval now records its pitch write and its spelling rewrites, so
value-restoring undo returns both. Transpose does NOT start recording: that
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, which is the one thing the freeze forbids. The old operation is
therefore permanently un-undoable, which is one more reason never to author it.
the_frozen_transpose_is_not_undoable_and_that_is_frozen_too pins that, and was
verified by the inverse mutation: making it undoable fails the test.

Restoring the pitch alone would leave a notehead spelled for a pitch that is no
longer there, so a new chain -- transposed_spelling_chain, keyed by pitch,
holding the engraved-layer explicit attachment SET -- restores the moved
authored attachments and removes the propagated one together. It is deliberately
not respell_chain: RespellPitch owns that chain, its last write is the LWW
working state its concurrent-differing conflict detection reads, and folding
transposes into it would make a concurrent respell conflict with a transpose and
would move the canonical bytes of every existing history.

Base-free reduction records nothing, because it writes nothing: the fuzz
corpus's canonical-base digest is unmoved.

Three mutations verified: the pitch-value record removed, the spelling-set
record removed (both undo tests fail), and the frozen Transpose "helpfully" made
undoable. The second of those first appeared to survive -- my harness restored
the file between the two tests, so the second ran unmutated. A mutation that
no-ops looks exactly like a test that passes; that trap, recorded after Push 4a,
was hit again here in a new form.

Gate: fmt clean, clippy 0, 30 targets / 993 passed / 0 failed, docs 0 under
-D warnings, conformance 8/8, zero golden churn.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Levi Neuwirth 2026-07-09 16:45:57 -04:00
parent 6369d331f1
commit 655cf8ef5b
3 changed files with 346 additions and 1 deletions

View File

@ -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);

View File

@ -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<PitchId,
WriteChain<Vec<SpellingAttachment>>>` 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.

View File

@ -770,6 +770,13 @@ enum ValueRestoration {
pitch: PitchId,
predecessor: Option<Predecessor<PitchSpelling>>,
},
/// 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<Predecessor<Vec<SpellingAttachment>>>,
},
CrossCutting {
id: TypedObjectId,
value: Option<CrossCuttingValue>,
@ -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<PitchId, WriteChain<PitchSpelling>>,
/// 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<PitchId, WriteChain<Vec<SpellingAttachment>>>,
event_modify_chain: BTreeMap<EventId, WriteChain<Event>>,
pitch_modify_chain: BTreeMap<PitchId, WriteChain<Pitch>>,
cross_cutting_modify_chain: BTreeMap<TypedObjectId, WriteChain<CrossCuttingValue>>,
@ -945,6 +964,18 @@ struct WorkingSnapshot {
event_pitches: BTreeMap<EventId, Vec<PitchId>>,
voice_occupancy: BTreeMap<VoiceId, Vec<(MusicalPosition, MusicalDuration, EventId)>>,
respell_chain: BTreeMap<PitchId, WriteChain<PitchSpelling>>,
/// 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<PitchId, WriteChain<Vec<SpellingAttachment>>>,
event_modify_chain: BTreeMap<EventId, WriteChain<Event>>,
pitch_modify_chain: BTreeMap<PitchId, WriteChain<Pitch>>,
cross_cutting_modify_chain: BTreeMap<TypedObjectId, WriteChain<CrossCuttingValue>>,
@ -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<PitchId, Vec<SpellingAttachment>> = 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<PitchId> {
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<SpellingAttachment> {
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<Score>) {
@ -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<SpellingAttachment> = 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