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

The pitch/spelling undo unit is broader than the transpose, on purpose 

A review of the P13-S3 fix caught the reducer's comment overclaiming. It said
the coupling "cannot mis-fire on an unrelated operation" because
ModifyIdentifiedPitch never writes the spelling set. That is true of the
OPERATION and irrelevant to the UNIT: the coupling is keyed on the pitch, and
on which keys the TRANSACTION wrote. A transaction whose members write the two
halves separately couples exactly the same way.

The editor's "move note" is precisely that -- ModifyIdentifiedPitch for the
value plus RespellPitch for the spelling set, in one transaction. Measured:

  no later respell,  BestEffort    -> Applied,    pitch restored to C4
  later respell,     BestEffort    -> Applied,    pitch STAYS D4, later E stands
  later respell,     StrictInverse -> Conflicted, pitch stays D4

The middle row is the coupling firing on a non-transpose pair, and it is
correct: restoring the pitch to C4 while the engraved spelling reads E --
authored against the moved pitch -- is exactly the stale-notehead defect the
coupling exists to prevent. Musically, undoing half of "move this note and
respell it" is not a smaller undo, it is a wrong score.

So the breadth is stated rather than left to be inferred.
req:opcat:spelling-set-chain now says the unit is keyed on the pitch and on the
transaction's writes, names the move-and-respell case, and notes that a
transaction writing only one of the two keys is unaffected -- an unwritten key
yields no supersession, which is the narrow claim the old comment should have
made.

Three regressions: full undo when nothing supersedes (guards against
OVER-coupling), best-effort skipping the pair when a later respell supersedes,
and strict undo conflicting. Mutation-verified by removing the coupling: only
the middle test fails, restoring the pitch to C4 with its spelling still
reading E, while the other two stay green -- they lock different properties.

Gate: fmt clean, clippy 0, 30 targets / 1001 passed / 0 failed, docs 0 under
-D warnings, conformance 8/8, zero golden churn, canonical-base digest unmoved.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Levi Neuwirth 2026-07-09 18:15:43 -04:00
parent 23521b4bcf
commit 958fffad4e
4 changed files with 168 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1436,3 +1436,33 @@ 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.
### P13-S3 follow-up: the coupling is broader than the transpose, on purpose
A review of the S3 fix caught the reducer's comment overclaiming. It said the
coupling "cannot mis-fire on an unrelated operation" because
`ModifyIdentifiedPitch` never writes the spelling set. True of the *operation*,
irrelevant to the *unit*: the coupling is keyed on the **pitch**, and on which
keys the **transaction** wrote. A transaction whose members write the two halves
separately is coupled exactly the same way.
The editor's "move note" is precisely that — `ModifyIdentifiedPitch` (the value)
plus `RespellPitch` (the spelling set), in one transaction
(`editor-core::apply_transaction`). Measured:
| later respell? | policy | undo effect | pitch | spelling |
|---|---|---|---|---|
| no | BestEffort | `Applied` | restored to C4 | attachment gone |
| yes | BestEffort | `Applied` | **stays D4** | the later E stands |
| yes | StrictInverse | `Conflicted` | stays D4 | the later E stands |
The middle row is the coupling firing on a non-transpose pair, and it is
**correct**: restoring the pitch to C4 while the engraved spelling reads E —
authored against the moved pitch — is exactly the stale-notehead defect the
coupling exists to prevent. So the breadth is intentional and now stated in
`req:opcat:spelling-set-chain` rather than left to be inferred.
Three regressions: full undo when nothing supersedes (guards against
*over*-coupling), best-effort skipping the pair when a later respell supersedes,
and strict undo conflicting. Mutation-verified: removing the coupling fails only
the middle one, restoring the pitch to C4 with the spelling still reading E.

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

@ -5139,11 +5139,22 @@ 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.
// A pitch's value and its engraved spelling set undo as ONE unit
// (`req:opcat:spelling-set-chain`): if either was superseded, neither is
// restored. Restoring a pitch while leaving a spelling authored against
// the value it used to have is the stale-notehead defect this prevents.
//
// The unit is keyed on the PITCH and on which chains the TRANSACTION
// wrote — not on which operation wrote them. So it also couples a
// transaction that writes the two halves through *different* members:
// the editor's "move note" is `ModifyIdentifiedPitch` + `RespellPitch`,
// and a later respell makes a best-effort undo skip both. That is
// intentional, and regression-locked
// (`best_effort_undo_skips_a_move_and_respell_pair_a_later_respell_superseded`).
//
// It cannot fire on a transaction that wrote only one half: a chain
// reports `Superseded` only when the transaction actually wrote it, so
// an unwritten chain yields `NotWritten` and contributes nothing.
if !superseded_pitches.is_empty() {
restorations.retain(|r| match r {
ValueRestoration::Pitch { pitch, .. }
@ -9937,6 +9948,116 @@ mod tests {
);
}
/// The editor's "move note": a value change plus the matching respelling, in
/// one transaction (`epiphany-editor-core`, `apply_transaction`). Neither
/// member writes both undo keys, but the *transaction* writes both — the
/// modify writes the pitch value, the respell writes the engraved spelling
/// set.
fn move_and_respell(
base: &Score,
pid: PitchId,
tx: TransactionId,
later_respell: bool,
policy: UndoPolicy,
) -> (OperationEffect, Score) {
let mut envs = vec![
declare_transaction(1, 0, 10, CausalContext::new(), tx),
tx_member(
1,
1,
11,
seen_r1(0),
tx,
OperationKind::ModifyIdentifiedPitch(ModifyIdentifiedPitchOp {
pitch: pid,
value: cmn_pitch(CmnNominal::D, 0, 4),
}),
),
tx_member(
1,
2,
12,
seen_r1(1),
tx,
OperationKind::RespellPitch(RespellPitchOp {
pitch: pid,
spelling: PitchSpelling::cmn(CmnNominal::D, 4),
}),
),
];
let mut counter = 3;
if later_respell {
envs.push(respell_env(1, 3, 13, seen_r1(2), pid, CmnNominal::E));
counter = 4;
}
let undo = undo_env(1, counter, 20, seen_r1(counter - 1), tx, policy);
let undo_id = undo.id;
envs.push(undo);
let mut set = OperationSet::new();
set.accept_all(envs);
let out = set.reduce_onto(base);
(undo_effect(&out.state, undo_id), out.score)
}
#[test]
fn a_move_and_respell_undoes_fully_when_nothing_supersedes_it() {
// The coupling must not over-fire: with no later writer, both halves of
// the transaction restore.
let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
let tx = TransactionId::new(ReplicaId(1), 900);
let (effect, score) = move_and_respell(&base, pid, tx, false, UndoPolicy::BestEffort);
assert_eq!(effect, OperationEffect::Applied);
assert_eq!(cmn_of(&pitch_of(&score, pid)), (CmnNominal::C, 0, 4));
assert!(
attachments_of(&score, pid).is_empty(),
"the respell's attachment is gone with it"
);
}
#[test]
fn best_effort_undo_skips_a_move_and_respell_pair_a_later_respell_superseded() {
// The pitch/spelling-set coupling is keyed on the PITCH and on which
// chains the TRANSACTION wrote — not on which operation wrote them, and
// not on `TransposeInterval` specifically. Here the modify wrote the
// pitch value and the respell wrote the spelling set; a later respell
// supersedes the set.
//
// Skipping both is the point. Restoring the pitch to C4 while the
// engraved spelling reads E — authored against the moved pitch — is
// exactly the stale-notehead defect the coupling exists to prevent.
// This broader reach is intentional (`req:opcat:spelling-set-chain`).
let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
let tx = TransactionId::new(ReplicaId(1), 900);
let (effect, score) = move_and_respell(&base, pid, tx, true, UndoPolicy::BestEffort);
assert_eq!(effect, OperationEffect::Applied);
assert_eq!(
cmn_of(&pitch_of(&score, pid)),
(CmnNominal::D, 0, 4),
"best-effort left the moved pitch, because its spelling set was superseded"
);
assert_eq!(
attachments_of(&score, pid),
vec![(SpellingSource::UserChosen, CmnNominal::E, 0)],
"the later authoring stands"
);
}
#[test]
fn strict_undo_of_a_superseded_move_and_respell_conflicts() {
let (base, pid) = base_with_pitch(cmn_pitch(CmnNominal::C, 0, 4));
let tx = TransactionId::new(ReplicaId(1), 900);
let (effect, score) = move_and_respell(&base, pid, tx, true, UndoPolicy::StrictInverse);
assert!(
matches!(effect, OperationEffect::Conflicted { .. }),
"a later canonical writer supersedes a strict undo"
);
assert_eq!(cmn_of(&pitch_of(&score, pid)), (CmnNominal::D, 0, 4));
}
#[test]
fn transpose_interval_skips_a_tombstoned_target_but_refuses_a_missing_one() {
// The skip/refuse distinction: a deleted pitch is not an untransposable

BIN
spec/operation_catalog.pdf
View File

Binary file not shown.

14
spec/operation_catalog.tex
View File

@ -806,8 +806,18 @@ records nothing and is therefore not undoable.
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.
\MUSTNOT{} restore a pitch's earlier value while leaving a spelling authored
against the value it has since taken.
This unit is keyed on the \emph{pitch}, and on which keys the
\emph{transaction} wrote --- not on which operation wrote them, and not on
\texttt{TransposeInterval} in particular. A transaction whose members write
the two halves separately is coupled the same way: an editor's ``move note''
is a \texttt{ModifyIdentifiedPitch} (the value) together with a
\texttt{RespellPitch} (the spelling set), and a later respell makes a
\texttt{BestEffort} undo skip both. That breadth is intended. A transaction
that wrote only one of the two keys is unaffected, since an unwritten key
yields no supersession.
\end{requirement}
\begin{rationale}