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

Pass 13 — P13-D1: run the ledger re-anchor for undo-driven event tombstones 

An undo of an event-minting transaction tombstoned the events graph-side
(materialize_graph_tombstones → materialize_graph_delete re-anchors/cascades a
structure whose anchor died) but never ran the ledger-side
reanchor_for_tombstone — so a structure orphaned by the undo left the graph
while staying Live in objects, with no RepairRecord. Ch6's same-step
RepairRecord MUST was unmet for undo-driven tombstones (slurs/spanners/repeats).

Fix: tombstone_undo_targets now captures each event target's voice (before the
graph half clears voice_occupancy) and runs reanchor_for_tombstone per event
target after the graph half. The orphaned structure now cascades or re-anchors
in objects with a same-step RepairRecord, agreeing with the already-updated
graph — both use the same min-survivor rule, so they converge on existence and
target. reanchor_for_tombstone gains a liveness guard (skip a non-Live
structure) so the undo's own tombstoned mints — whose stale structures-index
entries linger — aren't re-processed into duplicate repairs; the direct-delete
path already drops tombstoned structures from the index, so the guard is a
no-op there.

canonical_bytes embeds both objects and the effect log, so this corrects the
reduced state (an inconsistency never previously exercised — no existing test
broke). Regression: undo_orphaning_a_pre_existing_slur_cascades_it_in_the_
ledger_p13_d1 (cascade + recorded repair + order-independent convergence).
939 tests, convergence/equivocation/conformance green. PASS13: P13-D1 resolved.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
Levi Neuwirth 2026-07-08 18:17:51 -04:00
parent 382aff23a2
commit 79c8e1da2e
3 changed files with 156 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1081,6 +1081,23 @@ against the triggering event before that event's own tombstone lands in
`Reanchored{to: X}` and `CascadeDeleted` in one effect (plausible by code
trace, unexecuted). Neither is repeat-specific; neither is fixed here.
**P13-D1 resolved (Pass 13, 2026-07-08).** `tombstone_undo_targets` now runs
the ledger half after the graph half: it captures each event target's voice
(before `materialize_graph_tombstones` clears `voice_occupancy`), then calls
`reanchor_for_tombstone` per event target. A structure orphaned by an
undo-tombstoned anchor now cascades or re-anchors in `objects` with a
same-step `RepairRecord`, so the ledger and the already-updated graph agree —
both use the same `min`-survivor rule, so they converge on existence and
target. `reanchor_for_tombstone` gained a **liveness guard** (skip a
non-`Live` structure) so the undo's own tombstoned mints — whose stale
`structures` index entries linger — are not re-processed into duplicate
repairs; the direct-delete path drops a tombstoned structure from `structures`,
so the guard is a no-op there. Because `canonical_bytes` embeds both `objects`
and the effect log, this corrects the reduced state (an inconsistency that was
simply never exercised — no existing test broke). Locked by
`undo_orphaning_a_pre_existing_slur_cascades_it_in_the_ledger_p13_d1`
(cascade + recorded repair + order-independent convergence).
**Noted, not implemented:** no writer path derives a chunk schema *minor*
from appended kind discriminants (a major-0 block carrying discriminant 29
stamps the same fixed minor as always) — pre-existing for the Phase-3

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

@ -4655,6 +4655,31 @@ impl<'a> Reducer<'a> {
targets: &[TypedObjectId],
) -> Vec<RepairRecord> {
let mut repairs = Vec::new();
// Each tombstoned event's voice, captured BEFORE the graph tombstone
// removes it from `voice_occupancy` — the containment-proximity key for
// the re-anchoring reasons below (mirrors `delete_event`).
let event_voices: Vec<(TypedObjectId, Option<VoiceId>)> = targets
.iter()
.filter(|t| matches!(t, TypedObjectId::Event(_)))
.map(|t| {
let TypedObjectId::Event(id) = t else {
unreachable!()
};
let voice = self
.voice_occupancy
.iter()
.find_map(|(voice, events)| {
events.iter().find(|(_, _, e)| e == id).map(|_| *voice)
})
.or_else(|| {
self.graph
.as_ref()
.and_then(|score| score.events.get(*id))
.map(Event::voice)
});
(*t, voice)
})
.collect();
for t in targets {
let minter = self.minted_by.get(t).copied().unwrap_or(env.id);
self.objects.insert(
@ -4670,6 +4695,22 @@ impl<'a> Reducer<'a> {
});
}
repairs.extend(self.materialize_graph_tombstones(env, targets));
// P13-D1: mirror the graph re-anchoring in the LEDGER. The graph side
// (`materialize_graph_delete`, run above) silently re-anchors or
// cascade-deletes a structure whose anchor event was undo-tombstoned,
// on the standing assumption that `reanchor_for_tombstone` records the
// repair and updates `objects`. The direct-delete path pairs the two;
// the undo path historically ran only the graph half, leaving an
// orphaned structure Live in `objects` with no RepairRecord — a Ch6
// same-step-recording MUST unmet for undo-driven tombstones. Running
// the ledger half here brings the two into agreement (the same
// `min`-survivor rule, so graph and ledger converge on existence and
// target). Every target is already tombstoned in `objects` above, so
// `surviving_endpoints` sees the full undo, and the liveness guard in
// `reanchor_for_tombstone` skips the target-structures themselves.
for (ev, voice) in event_voices {
self.reanchor_for_tombstone(env, ev, &mut repairs, voice);
}
repairs
}
@ -5821,6 +5862,16 @@ impl<'a> Reducer<'a> {
.map(|(sid, _)| *sid)
.collect();
for sid in referencing {
// Skip a structure that is no longer Live — it may already have
// been tombstoned by this same effect (an undo tombstones a whole
// transaction's mints together, and its stale index entry lingers)
// or cascaded by an earlier referent in this call. Re-processing it
// would push a duplicate repair. The direct-delete path never hits
// this (a tombstoned structure is dropped from `structures`), so the
// guard is a no-op there and load-bearing only for the undo path.
if !matches!(self.objects.get(&sid), Some(ObjectState::Live)) {
continue;
}
match sid {
TypedObjectId::Tie(_) => {
// A tie's existence requires both endpoints: cascade-delete.
@ -9567,6 +9618,93 @@ mod tests {
);
}
#[test]
fn undo_orphaning_a_pre_existing_slur_cascades_it_in_the_ledger_p13_d1() {
// P13-D1: a PRE-EXISTING structure whose every anchor event is
// undo-tombstoned must cascade in the LEDGER (`objects` → Tombstoned)
// with a same-step RepairRecord — not merely leave the graph while
// staying Live with no record (Ch6 §Re-Anchoring MUST). The slur is
// created OUTSIDE the undone transaction, so the undo ORPHANS it rather
// than tombstoning it directly. Before the fix the undo path ran only
// the graph half of the re-anchor, leaving `objects[slur]` Live and no
// repair recorded.
use epiphany_core::SlurId;
let tx = TransactionId::new(ReplicaId(1), 900);
let e1 = EventId::new(ReplicaId(1), 100);
let e2 = EventId::new(ReplicaId(1), 101);
let slur_id = SlurId::new(ReplicaId(9), 500);
let sid = TypedObjectId::Slur(slur_id);
let insert_kind = |event: EventId, at: i64| {
OperationKind::InsertEvent(InsertEventOp {
staff_instance: StaffInstanceId::new(ReplicaId(9), 0),
event: crate::valuegen::insert_event_value(
event,
VoiceId::new(ReplicaId(9), 1),
pos(at),
epiphany_core::MusicalDuration::whole(),
&[],
),
})
};
let slur_op = OperationKind::CreateCrossCutting(CreateCrossCuttingOp {
structure: CrossCuttingValue::Slur(crate::valuegen::slur(slur_id, e1, e2)),
});
let undo = undo_env(1, 4, 40, seen_r1(3), tx, UndoPolicy::StrictInverse);
let mut set = OperationSet::new();
set.accept_all(vec![
declare_transaction(1, 0, 10, CausalContext::new(), tx),
tx_member(1, 1, 11, seen_r1(0), tx, insert_kind(e1, 0)),
tx_member(1, 2, 12, seen_r1(1), tx, insert_kind(e2, 10)),
prim_env(1, 3, 13, seen_r1(2), slur_op),
undo.clone(),
]);
let state = set.reduce();
// The orphaned slur cascades in the ledger (not left Live)…
assert!(
matches!(
state.objects.get(&sid),
Some(ObjectState::Tombstoned { .. })
),
"the orphaned slur cascades in the ledger, not left Live with no repair"
);
// …and the undo records the same-step CascadeDeleted repair (Ch6 MUST).
let undo_records_cascade = matches!(
state.effects.iter().find(|(id, _)| *id == undo.id).map(|(_, e)| e),
Some(OperationEffect::AppliedWithRepair { repairs })
if repairs.iter().any(|r| r.target == sid
&& matches!(r.kind, RepairKind::CascadeDeleted))
);
assert!(
undo_records_cascade,
"the undo records the orphaned slur's cascade repair (Ch6 same-step MUST)"
);
// Determinism: a permuted delivery reduces to identical bytes.
let mut permuted = OperationSet::new();
permuted.accept_all(vec![
undo.clone(),
prim_env(
1,
3,
13,
seen_r1(2),
OperationKind::CreateCrossCutting(CreateCrossCuttingOp {
structure: CrossCuttingValue::Slur(crate::valuegen::slur(slur_id, e1, e2)),
}),
),
tx_member(1, 2, 12, seen_r1(1), tx, insert_kind(e2, 10)),
tx_member(1, 1, 11, seen_r1(0), tx, insert_kind(e1, 0)),
declare_transaction(1, 0, 10, CausalContext::new(), tx),
]);
assert_eq!(
state.canonical_bytes(),
permuted.reduce().canonical_bytes(),
"the orphan-cascade converges regardless of delivery order"
);
}
#[test]
fn a_rank_four_reanchor_records_same_canvas_nearer_p12_c4() {
// Pass 12 (P12-C4): the rank-4 (same-canvas) proximity survivor has

2
spec/PASS13_CANDIDATES.md
View File

@ -8,6 +8,6 @@ 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) | **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-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) | **resolved** (Pass 13: `tombstone_undo_targets` runs the ledger re-anchor per event target; liveness guard; convergence-locked) |
| 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") |