diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index 79073c3..aab4dae 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -1983,12 +1983,69 @@ mutation-tested (t13, four sub-mutations, one per family) against a dedicated base-recarry test (t5b) that a from-empty-only re-carry test (t5) structurally cannot exercise. -**The tombstoned branch is implemented but, like `create_staff`'s and -`create_instrument`'s, not exercised by any test.** No delete exists for any -of these six mint-only families (`CreateStaff`, `CreateInstrument`, and now -the four G3a kinds), so `ObjectState::Tombstoned` is unreachable for any of -them through the public operation API today. This is the pre-existing -project convention, not a new gap this rung introduces. +**Correction of record (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md`, Packet A, +2026-07-29).** The paragraph that originally stood here claimed: "No delete +exists for any of these six mint-only families (`CreateStaff`, +`CreateInstrument`, and now the four G3a kinds), so `ObjectState::Tombstoned` +is unreachable for any of them through the public operation API today." That +claim is **false**, and it was signed off in error. It is not being silently +deleted; this paragraph replaces it and says so. + +The branch **is** reachable, with no delete operation required: mint the +object inside a declared transaction, then carry `UndoTransaction` +(`reduce.rs:5288`) against that transaction under `StrictInverse` or +`BestEffort`. `tombstone_undo_targets` (`reduce.rs:5387`) writes +`ObjectState::Tombstoned` into `objects` for every minted target this way — +`CreateStaff` and `CreateInstrument` included, and this was already true +**before** G3a landed. G3a's four kinds inherited the same reachable branch +and the same unexamined wrong claim; none of the six families needed a +dedicated delete operation to reach `Tombstoned`, only an undo of the +transaction that minted them. + +The claim's real defect was upstream of G3a: undoing a `StaffGroup`, +`PartDefinition`, `AnalysisLayer`, or `View` mint tombstoned the object in the +ledger but left its value sitting in the corresponding `Score` vector (no +removal arm in `materialize_graph_tombstones`), and undoing a `StaffGroup`, +`AnalysisLayer`, or `Instrument` mint could strand a live `Staff.group` / +`ViewDefinition.active_layers` / `Staff.instrument` reference (no guard in +`undo_strand_block`). G3a shipped without sign-off coverage for a branch that +was live and broken. `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet A +closes both gaps: + +- **Five removal arms** in `materialize_graph_tombstones` (pin A1): + `StaffGroup` → `score.staff_groups`, `PartDefinition` → `score.parts`, + `AnalysisLayer` → `score.analysis_layers`, `View` → `score.views`, + `Instrument` → `score.instruments` — each mirrors the pre-existing `Staff` + / `TimeSignature` arms exactly. +- **Three inbound-reference guards** in `undo_strand_block` (pins A2–A6): + `StaffGroup(g)` blocked by a live `Staff` whose `group == Some(g)`, + `AnalysisLayer(l)` blocked by a live `ViewDefinition` whose + `active_layers` contains `l`, `Instrument(i)` blocked by a live `Staff` + whose `instrument == i`. Each reads the carried-value maps + (`staff_values`/`view_values`), **not** `self.graph`, and is deliberately + **ungated** (pin A3, ratified ruling): the create-side referential + preconditions are graph-gated because base-free reduction has no universe + to resolve against, but the ledger's carried-value maps are populated by + mints regardless of graph presence — so gating the undo-side guard would + let base-free undo strand a reference the ledger can plainly see. Each + guard requires the referencer to be `ObjectState::Live` (pin A4 — an + already-tombstoned referencer never blocks) and excludes referencers + minted in the same transaction being undone (pin A5 — a transaction that + mints both sides is undoable whole). `restorations` is deliberately + **not** consulted by these three guards (pin A6, ratified ruling): unlike + `MeterChange`, none of `Staff.group`, `Staff.instrument`, or + `ViewDefinition.active_layers` has a modify operation, so no write chain's + restoration could ever change the prospective post-undo value — adding a + lookup here would be dead code asserting a write chain that does not + exist. + +`objects` outranks the retained value maps on re-create (pin A7): every +create reducer already checks `self.objects` before its value map, so a +re-create after undo hits `ObjectState::Tombstoned` and returns +`TargetTombstoned`, never reaching the stale retained value — verified by +row family u4 (u4a–u4e)'s byte-identical re-carry mutation (falling the +`Tombstoned` arm through to the value-map identity check misreports +`AlreadyApplied` instead). **§1.1, disposition B — the `Staff.group`/`StaffGroup.members` authority ruling, and why `create_staff_group` does the least possible thing.** diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index e95b2dc..a040ea9 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -2807,6 +2807,25 @@ impl<'a> Reducer<'a> { TypedObjectId::TimeSignature(id) => { score.time_signatures.retain(|value| value.id != *id); } + // Genesis tranche G3a mints, plus G1's `Instrument` (contract + // `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` pin A1): the + // ledger tombstones these five kinds too, and the graph must + // agree — mirroring the `Staff` / `TimeSignature` arms above. + TypedObjectId::StaffGroup(id) => { + score.staff_groups.retain(|value| value.id != *id); + } + TypedObjectId::PartDefinition(id) => { + score.parts.retain(|value| value.id != *id); + } + TypedObjectId::AnalysisLayer(id) => { + score.analysis_layers.retain(|value| value.id != *id); + } + TypedObjectId::View(id) => { + score.views.retain(|value| value.id != *id); + } + TypedObjectId::Instrument(id) => { + score.instruments.retain(|value| value.id != *id); + } _ => {} } } @@ -5451,10 +5470,14 @@ impl<'a> Reducer<'a> { /// `Some((blocked, referencer))` when tombstoning `target` under undo /// would strand a live reference: a minted `Staff` still manifested by a - /// live staff instance (operation_catalog §CreateStaff), or a minted + /// live staff instance (operation_catalog §CreateStaff), a minted /// `TimeSignature` still referenced by a meter change that survives the - /// restoration pass. References held by objects the same undo tombstones - /// do not block. + /// restoration pass, a minted `StaffGroup` still named by a live + /// `Staff.group`, a minted `AnalysisLayer` still named by a live + /// `ViewDefinition.active_layers`, or a minted `Instrument` still named by + /// a live `Staff.instrument` (contract + /// `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` pin A2). References held by + /// objects the same undo tombstones do not block. fn undo_strand_block( &self, target: &TypedObjectId, @@ -5497,6 +5520,42 @@ impl<'a> Reducer<'a> { }) }) } + // Genesis tranche G3a undo repair (pins A2-A6): these three + // guards read the carried-value maps, not `self.graph`, and are + // deliberately ungated (pin A3) — the ledger knows a live staff + // or view names this referent regardless of graph presence. + // `restorations` is not consulted (pin A6): none of + // `Staff.group`, `Staff.instrument`, or + // `ViewDefinition.active_layers` has a modify operation, so there + // is no write chain whose restoration could change the + // prospective post-undo value. + TypedObjectId::StaffGroup(group) => { + self.staff_values.iter().find_map(|(staff_id, staff)| { + let sobj = TypedObjectId::Staff(*staff_id); + (staff.group == Some(*group) + && !targets.contains(&sobj) + && matches!(self.objects.get(&sobj), Some(ObjectState::Live))) + .then_some((*target, sobj)) + }) + } + TypedObjectId::AnalysisLayer(layer) => { + self.view_values.iter().find_map(|(view_id, view)| { + let vobj = TypedObjectId::View(*view_id); + (view.active_layers.contains(layer) + && !targets.contains(&vobj) + && matches!(self.objects.get(&vobj), Some(ObjectState::Live))) + .then_some((*target, vobj)) + }) + } + TypedObjectId::Instrument(instrument) => { + self.staff_values.iter().find_map(|(staff_id, staff)| { + let sobj = TypedObjectId::Staff(*staff_id); + (staff.instrument == *instrument + && !targets.contains(&sobj) + && matches!(self.objects.get(&sobj), Some(ObjectState::Live))) + .then_some((*target, sobj)) + }) + } _ => None, } } @@ -15092,4 +15151,1190 @@ mod tests { "a block containing a G3a kind stamps minor 11" ); } + + // ========================================================================= + // The G3a undo repair (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md`, Packet + // A): the five `materialize_graph_tombstones` removal arms (pin A1) and + // the three `undo_strand_block` inbound-reference guards (pins A2-A6) + // this packet adds, plus the pin A7 re-create ordering they make correct. + // ========================================================================= + + fn instrument_env( + replica: u64, + counter: u64, + physical: i64, + ctx: CausalContext, + instrument: epiphany_core::Instrument, + ) -> OperationEnvelope { + prim_env( + replica, + counter, + physical, + ctx, + OperationKind::CreateInstrument(CreateInstrumentOp { instrument }), + ) + } + + fn staff_env( + replica: u64, + counter: u64, + physical: i64, + ctx: CausalContext, + staff: epiphany_core::Staff, + ) -> OperationEnvelope { + prim_env( + replica, + counter, + physical, + ctx, + OperationKind::CreateStaff(CreateStaffOp { staff }), + ) + } + + // --- u1a-u1e: removal and tombstoning (pin A1). ------------------------- + + /// (u1a) Undoing a `StaffGroup` mint removes it from `Score.staff_groups` + /// and tombstones it in `objects` (pin A1, table row 1). + /// + /// **Mutation:** delete the `StaffGroup` arm from + /// `materialize_graph_tombstones` (pin A1's table). Assertion (i) must + /// fail — the value stays in `Score.staff_groups`. + #[test] + fn u1a_undo_of_a_staff_group_mint_removes_it_and_tombstones() { + let identity = IdentityContext::new(ReplicaId(1)); + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: crate::valuegen::staff_group(group_id, vec![]), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + !out.score.staff_groups.iter().any(|g| g.id == group_id), + "(i) undo must remove the minted StaffGroup from Score.staff_groups" + ); + assert!( + matches!( + out.state.objects.get(&TypedObjectId::StaffGroup(group_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "(ii) undo must tombstone the minted StaffGroup in objects" + ); + } + + /// (u1b) Undoing a `PartDefinition` mint removes it from `Score.parts` + /// and tombstones it in `objects` (pin A1, table row 2). + /// + /// **Mutation:** delete the `PartDefinition` arm from + /// `materialize_graph_tombstones`. Assertion (i) must fail. + #[test] + fn u1b_undo_of_a_part_definition_mint_removes_it_and_tombstones() { + let identity = IdentityContext::new(ReplicaId(1)); + let part_id = PartDefinitionId::new(ReplicaId(1), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreatePartDefinition(CreatePartDefinitionOp { + part: crate::valuegen::part_definition(part_id, vec![]), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + !out.score.parts.iter().any(|p| p.id == part_id), + "(i) undo must remove the minted PartDefinition from Score.parts" + ); + assert!( + matches!( + out.state + .objects + .get(&TypedObjectId::PartDefinition(part_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "(ii) undo must tombstone the minted PartDefinition in objects" + ); + } + + /// (u1c) Undoing an `AnalysisLayer` mint removes it from + /// `Score.analysis_layers` and tombstones it in `objects` (pin A1, table + /// row 3). + /// + /// **Mutation:** delete the `AnalysisLayer` arm from + /// `materialize_graph_tombstones`. Assertion (i) must fail. + #[test] + fn u1c_undo_of_an_analysis_layer_mint_removes_it_and_tombstones() { + let identity = IdentityContext::new(ReplicaId(1)); + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: crate::valuegen::analysis_layer(layer_id), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + !out.score.analysis_layers.iter().any(|l| l.id == layer_id), + "(i) undo must remove the minted AnalysisLayer from Score.analysis_layers" + ); + assert!( + matches!( + out.state + .objects + .get(&TypedObjectId::AnalysisLayer(layer_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "(ii) undo must tombstone the minted AnalysisLayer in objects" + ); + } + + /// (u1d) Undoing a `View` mint removes it from `Score.views` and + /// tombstones it in `objects` (pin A1, table row 4). + /// + /// **Mutation:** delete the `View` arm from + /// `materialize_graph_tombstones`. Assertion (i) must fail. + #[test] + fn u1d_undo_of_a_view_mint_removes_it_and_tombstones() { + let identity = IdentityContext::new(ReplicaId(1)); + let view_id = ViewId::new(ReplicaId(1), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateView(CreateViewOp { + view: crate::valuegen::view(view_id, vec![]), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + !out.score.views.iter().any(|v| v.id == view_id), + "(i) undo must remove the minted View from Score.views" + ); + assert!( + matches!( + out.state.objects.get(&TypedObjectId::View(view_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "(ii) undo must tombstone the minted View in objects" + ); + } + + /// (u1e) Undoing an `Instrument` mint removes it from `Score.instruments` + /// and tombstones it in `objects` (pin A1, table row 5; pin A8 — + /// `Instrument` is in scope as collateral). + /// + /// **Mutation:** delete the `Instrument` arm from + /// `materialize_graph_tombstones`. Assertion (i) must fail. + #[test] + fn u1e_undo_of_an_instrument_mint_removes_it_and_tombstones() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: crate::valuegen::instrument(instrument_id), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + !out.score.instruments.iter().any(|i| i.id == instrument_id), + "(i) undo must remove the minted Instrument from Score.instruments" + ); + assert!( + matches!( + out.state + .objects + .get(&TypedObjectId::Instrument(instrument_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "(ii) undo must tombstone the minted Instrument in objects" + ); + } + + // --- u2a-u2c: a live outside referencer blocks the undo (pin A2). ------- + + /// (u2a) A live `Staff` naming a minted `StaffGroup` blocks the group's + /// strict undo, and the group survives (pin A2, table row 1). + /// + /// **Mutation:** delete the `StaffGroup` arm from `undo_strand_block` + /// (pin A2's table). The effect becomes `Applied` and the reference + /// strands. + #[test] + fn u2a_a_live_staff_naming_the_group_blocks_its_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(9), 1); + let mut base = Score::empty(identity); + base.instruments + .push(crate::valuegen::instrument(instrument_id)); + + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + let mut staff_value = crate::valuegen::staff(staff_id, instrument_id); + staff_value.group = Some(group_id); + + 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, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: crate::valuegen::staff_group(group_id, vec![]), + }), + ), + staff_env(2, 0, 20, CausalContext::new(), staff_value), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &base); + + assert!( + matches!( + effect_at(&out.state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "a live staff naming the group must block strict undo" + ); + assert!( + out.score.staff_groups.iter().any(|g| g.id == group_id), + "the group must remain since undo was blocked" + ); + } + + /// (u2b) A live `ViewDefinition` naming a minted `AnalysisLayer` blocks + /// the layer's strict undo, and the layer survives (pin A2, table row + /// 2). + /// + /// **Mutation:** delete the `AnalysisLayer` arm from `undo_strand_block`. + /// The effect becomes `Applied` and the reference strands. + #[test] + fn u2b_a_live_view_naming_the_layer_blocks_its_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let view_id = ViewId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: crate::valuegen::analysis_layer(layer_id), + }), + ), + view_env( + 2, + 0, + 20, + CausalContext::new(), + crate::valuegen::view(view_id, vec![layer_id]), + ), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + effect_at(&out.state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "a live view naming the layer must block strict undo" + ); + assert!( + out.score.analysis_layers.iter().any(|l| l.id == layer_id), + "the layer must remain since undo was blocked" + ); + } + + /// (u2c) A live `Staff` naming a minted `Instrument` blocks the + /// instrument's strict undo, and the instrument survives (pin A2, table + /// row 3). + /// + /// **Mutation:** delete the `Instrument` arm from `undo_strand_block`. + /// The effect becomes `Applied` and the reference strands. + #[test] + fn u2c_a_live_staff_naming_the_instrument_blocks_its_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: crate::valuegen::instrument(instrument_id), + }), + ), + staff_env( + 2, + 0, + 20, + CausalContext::new(), + crate::valuegen::staff(staff_id, instrument_id), + ), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + effect_at(&out.state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "a live staff naming the instrument must block strict undo" + ); + assert!( + out.score.instruments.iter().any(|i| i.id == instrument_id), + "the instrument must remain since undo was blocked" + ); + } + + // --- u2bf-a-u2bf-c: the guards hold base-free (signs pin A3). ----------- + + /// (u2bf-a) The `StaffGroup` guard holds under `reduce_operation_set` + /// (no base `Score`): base-free reduction skips `create_staff`'s + /// referential preconditions entirely, so the referencing staff mints + /// unconditionally and the ledger alone must refuse the group's undo. + /// + /// **Mutation:** wrap the `StaffGroup` guard arm in + /// `if self.graph.is_some() { .. } else { None }`. This row must go red + /// while u2a stays green — run both in the same pass and record both + /// observations. + #[test] + fn u2bf_a_the_staff_group_guard_holds_base_free() { + // Never minted; base-free reduction has no universe to check it + // against, so `create_staff` never looks. + let instrument_id = InstrumentId::new(ReplicaId(9), 1); + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + let mut staff_value = crate::valuegen::staff(staff_id, instrument_id); + staff_value.group = Some(group_id); + + 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, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: crate::valuegen::staff_group(group_id, vec![]), + }), + ), + staff_env(2, 0, 20, CausalContext::new(), staff_value), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let state = reduce_operation_set(&set); + + assert!( + matches!( + effect_at(&state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "pin A3: the StaffGroup guard must hold base-free — the ledger alone \ + knows the reference, with no graph to check against" + ); + } + + /// (u2bf-b) The `AnalysisLayer` guard holds base-free. + /// + /// **Mutation:** wrap the `AnalysisLayer` guard arm in + /// `if self.graph.is_some() { .. } else { None }`. This row must go red + /// while u2b stays green — run both in the same pass. + #[test] + fn u2bf_b_the_analysis_layer_guard_holds_base_free() { + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let view_id = ViewId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: crate::valuegen::analysis_layer(layer_id), + }), + ), + view_env( + 2, + 0, + 20, + CausalContext::new(), + crate::valuegen::view(view_id, vec![layer_id]), + ), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let state = reduce_operation_set(&set); + + assert!( + matches!( + effect_at(&state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "pin A3: the AnalysisLayer guard must hold base-free — the ledger alone \ + knows the reference, with no graph to check against" + ); + } + + /// (u2bf-c) The `Instrument` guard holds base-free. + /// + /// **Mutation:** wrap the `Instrument` guard arm in + /// `if self.graph.is_some() { .. } else { None }`. This row must go red + /// while u2c stays green — run both in the same pass. + #[test] + fn u2bf_c_the_instrument_guard_holds_base_free() { + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(2), 1); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: crate::valuegen::instrument(instrument_id), + }), + ), + staff_env( + 2, + 0, + 20, + CausalContext::new(), + crate::valuegen::staff(staff_id, instrument_id), + ), + undo_env(1, 2, 30, seen_r1(1), tx, UndoPolicy::StrictInverse), + ]); + let state = reduce_operation_set(&set); + + assert!( + matches!( + effect_at(&state, 2), + Some(OperationEffect::Conflicted { .. }) + ), + "pin A3: the Instrument guard must hold base-free — the ledger alone \ + knows the reference, with no graph to check against" + ); + } + + // --- u2tomb-a-u2tomb-c: a tombstoned referencer does not block (signs + // pin A4). ----------------------------------------------------------- + + /// (u2tomb-a) T1 mints `StaffGroup g`; T2 mints a `Staff s` naming it. + /// Undoing T2 first tombstones `s` (its value stays in `staff_values`, + /// pin A7); undoing T1 next must then proceed, since a tombstoned + /// referencer does not block (pin A4). + /// + /// **Mutation:** delete the + /// `matches!(self.objects.get(&sobj), Some(ObjectState::Live))` conjunct + /// from the `StaffGroup` guard arm. The dead referencer blocks; T1's + /// undo becomes `Conflicted`. + #[test] + fn u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(9), 1); + let mut base = Score::empty(identity); + base.instruments + .push(crate::valuegen::instrument(instrument_id)); + + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(1), 2); + let tx1 = TransactionId::new(ReplicaId(1), 900); + let tx2 = TransactionId::new(ReplicaId(1), 901); + + let mut staff_value = crate::valuegen::staff(staff_id, instrument_id); + staff_value.group = Some(group_id); + + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx1), + tx_member( + 1, + 1, + 11, + seen_r1(0), + tx1, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: crate::valuegen::staff_group(group_id, vec![]), + }), + ), + declare_transaction(1, 2, 20, seen_r1(1), tx2), + tx_member( + 1, + 3, + 21, + seen_r1(2), + tx2, + OperationKind::CreateStaff(CreateStaffOp { staff: staff_value }), + ), + undo_env(1, 4, 30, seen_r1(3), tx2, UndoPolicy::StrictInverse), + undo_env(1, 5, 40, seen_r1(4), tx1, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &base); + + assert!( + matches!( + out.state.objects.get(&TypedObjectId::Staff(staff_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "T2's undo must tombstone the referencing staff" + ); + assert!( + !out.score.staves.iter().any(|s| s.id == staff_id), + "the tombstoned staff leaves Score.staves" + ); + assert!( + matches!( + effect_at(&out.state, 5), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "with the referencer already tombstoned, T1's undo must proceed" + ); + assert!( + !out.score.staff_groups.iter().any(|g| g.id == group_id), + "the group leaves Score.staff_groups once T1's undo proceeds" + ); + } + + /// (u2tomb-b) T1 mints `AnalysisLayer l`; T2 mints a `ViewDefinition v` + /// naming it. Undoing T2 first tombstones `v`; undoing T1 next must then + /// proceed. + /// + /// **Mutation:** delete the liveness conjunct from the `AnalysisLayer` + /// guard arm. T1's undo becomes `Conflicted`. + #[test] + fn u2tomb_b_a_tombstoned_referencing_view_does_not_block_the_layers_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let view_id = ViewId::new(ReplicaId(1), 2); + let tx1 = TransactionId::new(ReplicaId(1), 900); + let tx2 = TransactionId::new(ReplicaId(1), 901); + + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx1), + tx_member( + 1, + 1, + 11, + seen_r1(0), + tx1, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: crate::valuegen::analysis_layer(layer_id), + }), + ), + declare_transaction(1, 2, 20, seen_r1(1), tx2), + tx_member( + 1, + 3, + 21, + seen_r1(2), + tx2, + OperationKind::CreateView(CreateViewOp { + view: crate::valuegen::view(view_id, vec![layer_id]), + }), + ), + undo_env(1, 4, 30, seen_r1(3), tx2, UndoPolicy::StrictInverse), + undo_env(1, 5, 40, seen_r1(4), tx1, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + out.state.objects.get(&TypedObjectId::View(view_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "T2's undo must tombstone the referencing view" + ); + assert!( + !out.score.views.iter().any(|v| v.id == view_id), + "the tombstoned view leaves Score.views" + ); + assert!( + matches!( + effect_at(&out.state, 5), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "with the referencer already tombstoned, T1's undo must proceed" + ); + assert!( + !out.score.analysis_layers.iter().any(|l| l.id == layer_id), + "the layer leaves Score.analysis_layers once T1's undo proceeds" + ); + } + + /// (u2tomb-c) T1 mints `Instrument i`; T2 mints a `Staff s` naming it. + /// Undoing T2 first tombstones `s`; undoing T1 next must then proceed. + /// + /// **Mutation:** delete the liveness conjunct from the `Instrument` + /// guard arm. T1's undo becomes `Conflicted`. + #[test] + fn u2tomb_c_a_tombstoned_referencing_staff_does_not_block_the_instruments_undo() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(1), 2); + let tx1 = TransactionId::new(ReplicaId(1), 900); + let tx2 = TransactionId::new(ReplicaId(1), 901); + + let mut set = OperationSet::new(); + set.accept_all(vec![ + declare_transaction(1, 0, 10, CausalContext::new(), tx1), + tx_member( + 1, + 1, + 11, + seen_r1(0), + tx1, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: crate::valuegen::instrument(instrument_id), + }), + ), + declare_transaction(1, 2, 20, seen_r1(1), tx2), + tx_member( + 1, + 3, + 21, + seen_r1(2), + tx2, + OperationKind::CreateStaff(CreateStaffOp { + staff: crate::valuegen::staff(staff_id, instrument_id), + }), + ), + undo_env(1, 4, 30, seen_r1(3), tx2, UndoPolicy::StrictInverse), + undo_env(1, 5, 40, seen_r1(4), tx1, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + out.state.objects.get(&TypedObjectId::Staff(staff_id)), + Some(ObjectState::Tombstoned { .. }) + ), + "T2's undo must tombstone the referencing staff" + ); + assert!( + !out.score.staves.iter().any(|s| s.id == staff_id), + "the tombstoned staff leaves Score.staves" + ); + assert!( + matches!( + effect_at(&out.state, 5), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "with the referencer already tombstoned, T1's undo must proceed" + ); + assert!( + !out.score.instruments.iter().any(|i| i.id == instrument_id), + "the instrument leaves Score.instruments once T1's undo proceeds" + ); + } + + // --- u3a-u3c: same-transaction teardown is allowed (signs pin A5). ----- + + /// (u3a) Minting `StaffGroup g` and a `Staff s` naming it inside the + /// *same* transaction undoes whole — the same-transaction exemption + /// (pin A5). + /// + /// **Mutation:** drop the `!targets.contains(&sobj)` conjunct from the + /// `StaffGroup` guard arm. The undo becomes `Conflicted`. + #[test] + fn u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(9), 1); + let mut base = Score::empty(identity); + base.instruments + .push(crate::valuegen::instrument(instrument_id)); + + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(1), 2); + let tx = TransactionId::new(ReplicaId(1), 900); + + let mut staff_value = crate::valuegen::staff(staff_id, instrument_id); + staff_value.group = Some(group_id); + + 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, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: crate::valuegen::staff_group(group_id, vec![]), + }), + ), + tx_member( + 1, + 2, + 12, + seen_r1(1), + tx, + OperationKind::CreateStaff(CreateStaffOp { staff: staff_value }), + ), + undo_env(1, 3, 20, seen_r1(2), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &base); + + assert!( + matches!( + effect_at(&out.state, 3), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "a transaction that mints both the group and its referencing staff must undo whole" + ); + assert!( + !out.score.staff_groups.iter().any(|g| g.id == group_id), + "the group leaves Score.staff_groups" + ); + assert!( + !out.score.staves.iter().any(|s| s.id == staff_id), + "the staff leaves Score.staves" + ); + } + + /// (u3b) Minting `AnalysisLayer l` and a `ViewDefinition v` naming it + /// inside the same transaction undoes whole. + /// + /// **Mutation:** drop the `!targets.contains(&vobj)` conjunct from the + /// `AnalysisLayer` guard arm. The undo becomes `Conflicted`. + #[test] + fn u3b_minting_the_layer_and_its_referencing_view_in_one_transaction_undoes_whole() { + let identity = IdentityContext::new(ReplicaId(1)); + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let view_id = ViewId::new(ReplicaId(1), 2); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: crate::valuegen::analysis_layer(layer_id), + }), + ), + tx_member( + 1, + 2, + 12, + seen_r1(1), + tx, + OperationKind::CreateView(CreateViewOp { + view: crate::valuegen::view(view_id, vec![layer_id]), + }), + ), + undo_env(1, 3, 20, seen_r1(2), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + effect_at(&out.state, 3), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "a transaction that mints both the layer and its referencing view must undo whole" + ); + assert!( + !out.score.analysis_layers.iter().any(|l| l.id == layer_id), + "the layer leaves Score.analysis_layers" + ); + assert!( + !out.score.views.iter().any(|v| v.id == view_id), + "the view leaves Score.views" + ); + } + + /// (u3c) Minting `Instrument i` and a `Staff s` naming it inside the same + /// transaction undoes whole. + /// + /// **Mutation:** drop the `!targets.contains(&sobj)` conjunct from the + /// `Instrument` guard arm. The undo becomes `Conflicted`. + #[test] + fn u3c_minting_the_instrument_and_its_referencing_staff_in_one_transaction_undoes_whole() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let staff_id = StaffId::new(ReplicaId(1), 2); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: crate::valuegen::instrument(instrument_id), + }), + ), + tx_member( + 1, + 2, + 12, + seen_r1(1), + tx, + OperationKind::CreateStaff(CreateStaffOp { + staff: crate::valuegen::staff(staff_id, instrument_id), + }), + ), + undo_env(1, 3, 20, seen_r1(2), tx, UndoPolicy::StrictInverse), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + assert!( + matches!( + effect_at(&out.state, 3), + Some(OperationEffect::Applied) | Some(OperationEffect::AppliedWithRepair { .. }) + ), + "a transaction that mints both the instrument and its referencing staff must undo whole" + ); + assert!( + !out.score.instruments.iter().any(|i| i.id == instrument_id), + "the instrument leaves Score.instruments" + ); + assert!( + !out.score.staves.iter().any(|s| s.id == staff_id), + "the staff leaves Score.staves" + ); + } + + // --- u4a-u4e: objects outranks the retained value map (signs pin A7). -- + + /// (u4a) After u1a's undo, a byte-identical re-carry of the same + /// `CreateStaffGroup` must report `TargetTombstoned`, not + /// `AlreadyApplied` — `objects` outranks `staff_group_values` (pin A7). + /// + /// **Mutation:** in `create_staff_group`, make the + /// `Some(ObjectState::Tombstoned { .. })` arm fall through to the + /// value-map identity check instead of returning `TargetTombstoned`. The + /// row must observe `AlreadyApplied`. + #[test] + fn u4a_a_recreate_of_a_tombstoned_staff_group_reports_target_tombstoned() { + let identity = IdentityContext::new(ReplicaId(1)); + let group_id = StaffGroupId::new(ReplicaId(1), 1); + let group_value = crate::valuegen::staff_group(group_id, vec![]); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateStaffGroup(CreateStaffGroupOp { + group: group_value.clone(), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + staff_group_env(2, 0, 20, CausalContext::new(), group_value), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + let recreate_effect = out + .state + .effects + .iter() + .find(|(id, _)| *id == OperationId::new(ReplicaId(2), 0)) + .map(|(_, e)| e.clone()) + .expect("recreate effect recorded"); + assert_eq!( + recreate_effect, + OperationEffect::NoOp { + reason: NoOpReason::TargetTombstoned + }, + "objects' Tombstoned state must outrank the retained staff_group_values \ + entry, got {recreate_effect:?}" + ); + } + + /// (u4b) After u1b's undo, a byte-identical re-carry of the same + /// `CreatePartDefinition` must report `TargetTombstoned`, not + /// `AlreadyApplied`. + /// + /// **Mutation:** in `create_part_definition`, make the + /// `Some(ObjectState::Tombstoned { .. })` arm fall through to the + /// value-map identity check. The row must observe `AlreadyApplied`. + #[test] + fn u4b_a_recreate_of_a_tombstoned_part_definition_reports_target_tombstoned() { + let identity = IdentityContext::new(ReplicaId(1)); + let part_id = PartDefinitionId::new(ReplicaId(1), 1); + let part_value = crate::valuegen::part_definition(part_id, vec![]); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreatePartDefinition(CreatePartDefinitionOp { + part: part_value.clone(), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + part_definition_env(2, 0, 20, CausalContext::new(), part_value), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + let recreate_effect = out + .state + .effects + .iter() + .find(|(id, _)| *id == OperationId::new(ReplicaId(2), 0)) + .map(|(_, e)| e.clone()) + .expect("recreate effect recorded"); + assert_eq!( + recreate_effect, + OperationEffect::NoOp { + reason: NoOpReason::TargetTombstoned + }, + "objects' Tombstoned state must outrank the retained part_definition_values \ + entry, got {recreate_effect:?}" + ); + } + + /// (u4c) After u1c's undo, a byte-identical re-carry of the same + /// `CreateAnalysisLayer` must report `TargetTombstoned`, not + /// `AlreadyApplied`. + /// + /// **Mutation:** in `create_analysis_layer`, make the + /// `Some(ObjectState::Tombstoned { .. })` arm fall through to the + /// value-map identity check. The row must observe `AlreadyApplied`. + #[test] + fn u4c_a_recreate_of_a_tombstoned_analysis_layer_reports_target_tombstoned() { + let identity = IdentityContext::new(ReplicaId(1)); + let layer_id = AnalysisLayerId::new(ReplicaId(1), 1); + let layer_value = crate::valuegen::analysis_layer(layer_id); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateAnalysisLayer(CreateAnalysisLayerOp { + layer: layer_value.clone(), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + analysis_layer_env(2, 0, 20, CausalContext::new(), layer_value), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + let recreate_effect = out + .state + .effects + .iter() + .find(|(id, _)| *id == OperationId::new(ReplicaId(2), 0)) + .map(|(_, e)| e.clone()) + .expect("recreate effect recorded"); + assert_eq!( + recreate_effect, + OperationEffect::NoOp { + reason: NoOpReason::TargetTombstoned + }, + "objects' Tombstoned state must outrank the retained analysis_layer_values \ + entry, got {recreate_effect:?}" + ); + } + + /// (u4d) After u1d's undo, a byte-identical re-carry of the same + /// `CreateView` must report `TargetTombstoned`, not `AlreadyApplied`. + /// + /// **Mutation:** in `create_view`, make the + /// `Some(ObjectState::Tombstoned { .. })` arm fall through to the + /// value-map identity check. The row must observe `AlreadyApplied`. + #[test] + fn u4d_a_recreate_of_a_tombstoned_view_reports_target_tombstoned() { + let identity = IdentityContext::new(ReplicaId(1)); + let view_id = ViewId::new(ReplicaId(1), 1); + let view_value = crate::valuegen::view(view_id, vec![]); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateView(CreateViewOp { + view: view_value.clone(), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + view_env(2, 0, 20, CausalContext::new(), view_value), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + let recreate_effect = out + .state + .effects + .iter() + .find(|(id, _)| *id == OperationId::new(ReplicaId(2), 0)) + .map(|(_, e)| e.clone()) + .expect("recreate effect recorded"); + assert_eq!( + recreate_effect, + OperationEffect::NoOp { + reason: NoOpReason::TargetTombstoned + }, + "objects' Tombstoned state must outrank the retained view_values entry, \ + got {recreate_effect:?}" + ); + } + + /// (u4e) After u1e's undo, a byte-identical re-carry of the same + /// `CreateInstrument` must report `TargetTombstoned`, not + /// `AlreadyApplied` (pin A8 — `Instrument` is in scope as collateral). + /// + /// **Mutation:** in `create_instrument`, make the + /// `Some(ObjectState::Tombstoned { .. })` arm fall through to the + /// value-map identity check. The row must observe `AlreadyApplied`. + #[test] + fn u4e_a_recreate_of_a_tombstoned_instrument_reports_target_tombstoned() { + let identity = IdentityContext::new(ReplicaId(1)); + let instrument_id = InstrumentId::new(ReplicaId(1), 1); + let instrument_value = crate::valuegen::instrument(instrument_id); + let tx = TransactionId::new(ReplicaId(1), 900); + + 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, + OperationKind::CreateInstrument(CreateInstrumentOp { + instrument: instrument_value.clone(), + }), + ), + undo_env(1, 2, 12, seen_r1(1), tx, UndoPolicy::StrictInverse), + instrument_env(2, 0, 20, CausalContext::new(), instrument_value), + ]); + let out = reduce_operation_set_onto(&set, &Score::empty(identity)); + + let recreate_effect = out + .state + .effects + .iter() + .find(|(id, _)| *id == OperationId::new(ReplicaId(2), 0)) + .map(|(_, e)| e.clone()) + .expect("recreate effect recorded"); + assert_eq!( + recreate_effect, + OperationEffect::NoOp { + reason: NoOpReason::TargetTombstoned + }, + "objects' Tombstoned state must outrank the retained instrument_values \ + entry, got {recreate_effect:?}" + ); + } } diff --git a/spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md b/spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md new file mode 100644 index 0000000..7d14ef0 --- /dev/null +++ b/spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md @@ -0,0 +1,532 @@ +# Contract: the G3a undo repair, and the Binary Format chronology restoration + +**Status:** **RATIFIED 2026-07-29.** Two packets, two commits. Pins A3 +(ungated ledger/map guards), A6 (no restoration lookup while those fields +have no write chain — revisit only if a modifying operation is introduced), +and A7 (retaining the maps is safe given A4's live-state filter and +object-first recreate refusal) were ratified explicitly. Mutation budget +ratified at twenty-two for Packet A and three for Packet B. +**Governs:** the defect that blocks G3a sign-off (Packet A), and P13-S17 +(Packet B). +**Predecessor:** `spec/CONTRACT_GENESIS_G3A_ENTITIES.md`, landed at `6c5e69f`. + +--- + +## §0. What was actually verified + +Every claim below was read out of the code, not relayed. + +**The tombstone branch is reachable.** `mint_container` +(`crates/epiphany-ops/src/reduce.rs:3922`) calls `note_minted` +(`:7848`), which pushes the object into `tx_minted` whenever +`self.current_tx` is set. `undo_transaction` (`:5288`) reads +`tx_minted` and `tombstone_undo_targets` (`:5387`) writes +`ObjectState::Tombstoned` into `objects` for every target. All four G3a +reducers reach `mint_container`: `create_staff_group` `:4283`, +`create_part_definition` `:4340`, `create_analysis_layer` `:4384`, +`create_view` `:4437`. `create_instrument` `:4214` and `create_staff` +`:4165` do the same. + +Therefore `crates/epiphany-ops/DECISIONS.md:1986` — "`ObjectState::Tombstoned` +is unreachable for any of them through the public operation API today" — is +**false**, and was false for `CreateStaff` and `CreateInstrument` before this +rung. It is a pre-existing wrong claim that G3a inherited and repeated. + +**The graph keeps ghosts.** `materialize_graph_tombstones` +(`:2737`) walks `targets` at `:2768` with arms for `Pitch`, `Voice`, +`Slur`, `Tie`, `Beam`, `Spanner`, `RepeatStructure`, `Staff`, +`TimeSignature`, then `_ => {}` at `:2810`. There is no arm for +`StaffGroup`, `PartDefinition`, `AnalysisLayer`, `View`, or `Instrument`. +The ledger tombstones; `Score.staff_groups` / `.parts` / `.analysis_layers` +/ `.views` / `.instruments` keep the value. Ledger and graph disagree — +the exact failure the `Spanner` arm's own comment at `:2793` records as +having been fixed once already. + +**The strand guard is silent on the new families.** `undo_strand_block` +(`:5458`) matches `Staff` and `TimeSignature`, then `_ => None` at +`:5500`. Undoing a `StaffGroup` mint while a live `Staff.group` +(`crates/epiphany-core/src/graph.rs:825`) names it strands the reference; +likewise `AnalysisLayer` ← `ViewDefinition.active_layers` (`graph.rs:1652`) +and `Instrument` ← `Staff.instrument` (`graph.rs:817`). + +`PartDefinition` and `View` need no guard: nothing in the graph references +them. Their own fields (`PartDefinition.staves` `graph.rs:1636`, +`ViewDefinition.active_layers`) are **outbound**, and removing the holder +strands nothing. + +**Count check.** `spec/PLAN_GMINOR_SCHEMA_MINOR.md:198` says "all ten +kind/tag pairs." The epoch table at `:170`–`:180` lists 24–27 (4), 28–29 +(2), 30 (1), 31 (1), 32–33 (2), 34 (1), 35–38 (4) = **fifteen**. + +**Binary Format chronology.** `spec/binary_format.tex` history rows: G2a +0.12.0 (`:3599`), G-minor 0.13.0 (`:3628`), G3a 0.14.0 (`:3643`). The +ladder order is G1 → G2a → G-minor → G2b → G3a, so **G2b is missing** +between 0.13.0 and G3a's row, and the accept-set raise +`OperationEnvelopeBlock` 2→3 that G2b performed is recorded nowhere in the +revision history — G3a's row at `:3657` merely observes the block "stays at +3 where genesis tranche G2b left it." + +**G1 has no standalone history row, by design.** It is recorded +retroactively *inside* the G2a row: the principal marker is at `:3599` +(`0.12.0 --- Genesis tranche G2a`), and G1 appears nested at `:3603` as +"(`CreateInstrument`, genesis tranche G1 --- landed at `3b09595` with no +matching entry here)". The row is explicit that G1 never got its own entry. +Pin B6 is scoped accordingly. + +--- + +# PACKET A — the undo repair + +## §A1. Pins + +**Pin A1 — five graph-removal arms.** In `materialize_graph_tombstones` +(`reduce.rs:2768`), before the `_ => {}` catch-all, add: + +| Target | Removal | +|---|---| +| `TypedObjectId::StaffGroup(id)` | `score.staff_groups.retain(\|v\| v.id != *id)` | +| `TypedObjectId::PartDefinition(id)` | `score.parts.retain(\|v\| v.id != *id)` | +| `TypedObjectId::AnalysisLayer(id)` | `score.analysis_layers.retain(\|v\| v.id != *id)` | +| `TypedObjectId::View(id)` | `score.views.retain(\|v\| v.id != *id)` | +| `TypedObjectId::Instrument(id)` | `score.instruments.retain(\|v\| v.id != *id)` | + +Each mirrors the existing `Staff` (`:2804`) and `TimeSignature` (`:2807`) +arms exactly. **No new `RepairRecord`**: `tombstone_undo_targets` already +pushes one `CascadeDeleted` per target at `:5427` before calling this +function, and none of the existing arms push more. + +**Pin A2 — three inbound-reference guards.** In `undo_strand_block` +(`:5458`), before `_ => None`: + +| Target | Blocked by | Read from | +|---|---|---| +| `StaffGroup(g)` | a live `Staff` whose `group == Some(g)` | `self.staff_values` | +| `AnalysisLayer(l)` | a live `ViewDefinition` whose `active_layers` contains `l` | `self.view_values` | +| `Instrument(i)` | a live `Staff` whose `instrument == i` | `self.staff_values` | + +Return `Some((*target, referencer_obj))` on the first match in map order. + +**Pin A3 — the guards are ledger-based and ungated.** They read the +carried-value maps (`staff_values` `:1001`, `view_values` `:1018`), **not** +`self.graph`, and are **not** wrapped in `if self.graph.is_some()`. + +Rationale, and it is a real decision: the *create*-side referential +preconditions **are** graph-gated (`create_staff:4137`, +`create_staff_group:4266`, `create_view:4420`) because base-free reduction +has no universe to resolve against. The *undo* side is different — the +carried-value maps are populated by mints regardless of graph presence and +are seeded from base when there is one, so under base-free reduction the +ledger still knows that a live staff names this group. Gating the guard +would let base-free undo strand a reference the ledger can plainly see. +The two existing guards (`instance_staff`, `meter_change_chain`) are +likewise ungated. **Stronger than the create side, and strictly safer.** + +**Pin A4 — liveness is read from `objects`, not from map presence.** The +value maps are insert-only; `tombstone_undo_targets` never removes from +them. A guard that treated map presence as liveness would let an +already-tombstoned staff block an unrelated undo forever. Each guard MUST +require `matches!(self.objects.get(&referencer_obj), Some(ObjectState::Live))`. + +**Pin A5 — same-transaction referencers do not block.** Each guard MUST +also require `!targets.contains(&referencer_obj)`, matching the `Staff` +guard's `!targets.contains(&iobj)` at `:5471` and the doc comment at +`:5456`. A transaction that mints a group and a staff in it must be +undoable whole. + +**Pin A6 — `restorations` is not consulted by the three new guards.** The +`TimeSignature` guard consults it (`:5483`) because `MeterChange` has a +write chain that undo may restore to a prior value. `Staff.group`, +`Staff.instrument` and `ViewDefinition.active_layers` have **no modify +operation at all** — that is the standing §1.1 condition — so no +restoration can change the prospective post-undo value. The implementer +MUST NOT cargo-cult the restoration lookup; its presence would be dead +code asserting a write chain that does not exist. + +**Pin A7 — the value maps are not pruned on undo.** `tombstone_undo_targets` +leaves `staff_group_values` and siblings untouched, matching the existing +`staff_values` / `time_signature_values` / `instrument_values` precedent. +This is safe **because every create reducer consults `self.objects` before +its value map**. The `match self.objects.get(..)` lines, not the function +declarations: `create_staff_group` `:4241`, `create_part_definition` +`:4298`, `create_analysis_layer` `:4356`, `create_view` `:4395`, +`create_staff` `:4109`, `create_instrument` `:4186`. A re-create after undo +therefore hits `Some(ObjectState::Tombstoned)` → `TargetTombstoned` and +never reaches the stale value. Row family **u4** signs that ordering, and it +is the only family that does — a re-create assertion bolted onto u1 would be +unsigned regression coverage, since u1's arm-deletion mutation cannot reach +it (§A3). + +**Pin A8 — Instrument is in scope as collateral.** It is the same root +cause, it already has normative undo semantics, and leaving it would mean +knowingly shipping a fifth instance of a defect this packet exists to fix. + +**Pin A9 — no new `OperationKind`, tag, epoch, discriminant, wire layout, +accept-set, or companion version.** This packet changes reducer behaviour +only. `spec/binary_format.tex` is **not** touched by Packet A. If any of +those surfaces appears in the diff, the packet is wrong. + +**Pin A10 — DECISIONS.md correction of record.** Replace the false +paragraph at `crates/epiphany-ops/DECISIONS.md:1986` with a correction that +states plainly: the branch **is** reachable via `UndoTransaction` over a +transaction containing the mint; it was reachable for `CreateStaff` and +`CreateInstrument` before G3a; the claim as written was wrong; and the +guards and removal arms this packet adds are what make it correct. Do not +silently delete it — the wrong claim was signed off and the record must say +so. + +## §A2. Touch table (Packet A) + +| # | File | Change | +|---|---|---| +| 1 | `crates/epiphany-ops/src/reduce.rs` | five arms in `materialize_graph_tombstones` (pin A1) | +| 2 | `crates/epiphany-ops/src/reduce.rs` | three arms in `undo_strand_block` (pins A2–A6) | +| 3 | `crates/epiphany-ops/src/reduce.rs` | doc comment on `undo_strand_block` `:5452` naming the three new blocks | +| 4 | `crates/epiphany-ops/src/reduce.rs` | test rows u1a–u1e, u2a–u2c, u2bf-a–c, u2tomb-a–c, u3a–u3c, u4a–u4e | +| 5 | `crates/epiphany-ops/DECISIONS.md` | pin A10 correction; record the five arms, three guards, and pin A3's ruling | +| 6 | `spec/PLAN_GENESIS_OPS.md:25` | "commit pending" → `6c5e69f`; note the undo repair rides after it | +| 7 | `spec/PLAN_GMINOR_SCHEMA_MINOR.md:190` | "introducing commit pending" → `6c5e69f` | +| 8 | `spec/PLAN_GMINOR_SCHEMA_MINOR.md:198` | "all ten kind/tag pairs" → "all fifteen kind/tag pairs" | +| 9 | `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` | **this file** — status line DRAFT → RATIFIED, dated, naming the ratifying decision on pins A3/A6/A7 | + +**Row 9 exists because the contract governing a commit must land with it.** +The file is currently untracked; without this row it would sit outside both +packets while §A2 says "nothing else" and §E permits staging only +touch-table files — a rule that excluded the rule-book. It joins Packet A. + +**Nothing else.** No `epiphany-bundle`, no `epiphany-core`, no spec `.tex`, +no editor-track file, no `spikes/` entry. + +## §A3. Test rows + +Every row names the mutation that MUST be **observed** to fail. Reasoning +that a mutation "would fail" does not sign a row — the G3a rung already +produced two such unsigned claims, both of which I had to run myself. + +**Twenty-two mutations in Packet A, three in Packet B: twenty-five total.** +The six row families below are u1 (5), u2 (3), u2bf (3), u2tomb (3), +u3 (3), u4 (5). + +### u1a–u1e — removal and tombstoning (5 mutations) + +One row per family: `StaffGroup`, `PartDefinition`, `AnalysisLayer`, +`View`, `Instrument`. Each mints the object inside a declared transaction +against a non-empty base, undoes the transaction with `StrictInverse`, and +asserts: + +- (i) the value is **gone** from the corresponding `Score` vector; +- (ii) `objects` reports `ObjectState::Tombstoned` for its `TypedObjectId`. + +> **Killing mutation, five independent runs:** delete that family's arm from +> pin A1's table. Assertion (i) must fail. Deleting one arm must not be +> observed to kill another family's row — run them one at a time and record +> five separate observations. + +**These rows do not sign pin A7.** A re-create assertion may be included as +regression coverage, but the arm-deletion mutation says nothing about it; +the ordering pin is signed by u4 below, and nowhere else. + +### u2a–u2c — a live outside referencer blocks the undo (3 mutations) + +Graph-aware (`reduce_operation_set_onto`). In each, transaction T mints the +referent; a **separate, non-transactional** op mints the referencer; undo T +under `StrictInverse` MUST be `Conflicted` and the referent MUST remain in +its `Score` vector. + +| Row | T mints | Outside op mints | +|---|---|---| +| u2a | `StaffGroup g` | `Staff s` with `group: Some(g)` | +| u2b | `AnalysisLayer l` | `ViewDefinition v` with `active_layers` ⊇ `[l]` | +| u2c | `Instrument i` | `Staff s` with `instrument: i` | + +> **Killing mutation, three independent runs:** delete that family's arm +> from pin A2. The effect becomes `Applied` and the reference strands. + +### u2bf-a–u2bf-c — the guards hold base-free (3 mutations) — signs pin A3 + +The same three shapes reduced through **`reduce_operation_set`** +(`reduce.rs:674`), with no base `Score`. Assert the effect is `Conflicted`. +There is no graph to assert against — `MaterializedState` carries no score — +so these rows assert the effect and the `objects` state only. + +Base-free reduction skips every create-side referential precondition +(`create_staff:4137`, `create_view:4420`), so the referencer mints +unconditionally and its value lands in `staff_values` / `view_values` +regardless. That is exactly the situation pin A3 exists to cover: the ledger +plainly knows the reference, and the undo must refuse. + +> **Killing mutation, three independent runs:** wrap that family's guard arm +> in `if self.graph.is_some() { … } else { None }`. The u2bf row must go red +> **while its u2 counterpart stays green** — that divergence is the whole +> signature. Record both observations per run. + +### u2tomb-a–u2tomb-c — a tombstoned referencer does not block (3 mutations) — signs pin A4 + +Graph-aware. Two transactions, undone in reverse order: + +1. T1 mints the referent (`g` / `l` / `i`). +2. T2 mints the referencer naming it (`s` / `v` / `s`). +3. Undo **T2** — the referencer is tombstoned in `objects`, leaves its + `Score` vector, and by pin A7 **its value is retained** in + `staff_values` / `view_values`. +4. Undo **T1** — MUST be `Applied` (or `AppliedWithRepair`), and the + referent MUST leave its `Score` vector. + +Step 3 is what creates the state pin A4 guards against: a value-map entry +present while its `objects` state is `Tombstoned`. + +> **Killing mutation, three independent runs:** delete the +> `matches!(self.objects.get(&…), Some(ObjectState::Live))` conjunct from +> that family's guard. The dead referencer blocks, step 4 becomes +> `Conflicted`, and the row goes red. + +### u3a–u3c — same-transaction teardown is allowed (3 mutations) — signs pin A5 + +The mirror of u2a–u2c: put **both** the referent and the referencer inside +T. Undo T MUST be `Applied` (or `AppliedWithRepair`), and **both** values +MUST leave their `Score` vectors. + +> **Killing mutation, three independent runs:** drop the +> `!targets.contains(…)` conjunct from that family's guard. The undo becomes +> `Conflicted`. + +### u4a–u4e — objects outranks the retained value map (5 mutations) — signs pin A7 + +One row per family. Take u1's state (minted in T, T undone, so the object is +`Tombstoned` while its value map still holds the value by pin A7), then +apply a **byte-identical re-carry** of the original `Create…`. It MUST yield +`NoOpReason::TargetTombstoned` — **not** `AlreadyApplied`. + +Byte-identical is the load-bearing choice: it is the one carried value for +which the retained map would return `identical == true` and produce +`AlreadyApplied`, so it is the only re-carry that can distinguish the two +orderings. A differing re-carry would yield a precondition no-op either way +and sign nothing. + +> **Killing mutation, five independent runs:** in that family's reducer, +> make the `Some(ObjectState::Tombstoned { .. })` arm fall through to the +> value-map identity check instead of returning `TargetTombstoned` — i.e. +> reorder so the retained value overrides the tombstone. The row must +> observe `AlreadyApplied` and go red. + +### Row-construction note + +`create_staff` preconditions instrument liveness at `:4137` and group +liveness at `:4149`; `create_view` preconditions layer liveness at `:4420`. +All are graph-gated, so they bind in the u2 / u2tomb / u3 / u4 rows and are +skipped in u2bf. + +- **u2a, u3a, u2tomb-a** need a base carrying a live `Instrument`: the + referencing `Staff` requires one, and the transaction under test mints a + `StaffGroup`, not an instrument. +- **u2c, u3c, u2tomb-c** need **no** base instrument — the instrument the + staff names is the one their own transaction mints. +- **u2b, u3b, u2tomb-b** need no base entity at all; `AnalysisLayer` and + `ViewDefinition` reference nothing outside the pair. + +In every graph-aware row the referent must be minted **before** the +referencing op in accepted order. A base-ingested instrument is `Live` in +`objects` through `seed_from_graph` without any mint. + +### Anti-traps + +A mutation that does not compile signs nothing. A mutation in an op that +runs *before* the state under assertion cannot reach it — the t8b defect +from G3a review. A mutation that leaves the row green signs nothing, and +must be reported as such rather than reasoned around. Confirm each mutation +produces a **red test**, then restore by editing the source back, never by +`git checkout` or `git stash`. + +## §A4. Gate (Packet A) + +- `cargo test --workspace` — full pass, count reported and compared to the + 1429 baseline at `6c5e69f`, with the delta explained by the new rows. +- `cargo clippy --workspace --all-targets` — zero warnings. +- `cargo fmt --check` — clean. +- Whitespace, per §C — **`git diff --cached --check` after staging**, then + the scoped committed-range check after the commit. +- All **twenty-two** Packet A mutations **observed** red and restored, each + reported with its actual failing test name. u2bf additionally reports its + paired u2 row staying green. + +--- + +# PACKET B — P13-S17, the Binary Format chronology + +Separate commit. The stack is unpublished, so the true chronology can be +restored rather than patched over. + +## §B1. Pins + +**Pin B1 — file P13-S17** in `spec/PASS13_CANDIDATES.md`: *Binary Format +revision history omitted genesis tranche G2b; the accept-set raise +`OperationEnvelopeBlock` 2→3 reached the normative tables but never the +history.* Record that G2b's own contract touch row 27 required "version, +Revision History row" and that the rung was signed off without it — the +gate did not catch a documentation MUST because nothing tests the history. + +**P13-S17 lands RESOLVED, in the same commit that files it.** Its ledger +disposition is not left open: pins B2–B4 restore the chronology and pins +B5–B6 add the guard that makes the omission recurrence-detectable, so the +entry is filed and closed by Packet B itself. It is filed rather than merely +fixed because the candidate ledger is the record of *how the gate failed*, +and a silent repair would erase that. Contrast **P13-S15** and **P13-S16**, +which remain open by design because their fixes are sequenced to later +rungs. + +**Pin B2 — restore the chronology.** Ladder order is G1 → G2a → G-minor → +G2b → G3a, so: + +| Document version | Event | Where | +|---|---|---| +| 0.12.0 | G2a | `binary_format.tex:3599`, unchanged | +| 0.13.0 | G-minor | `:3628`, unchanged | +| **0.14.0** | **G2b — new row** | inserted after the G-minor row | +| **0.15.0** | G3a | `:3643`, renumbered from 0.14.0 | + +The title line at `:243` moves to **0.15.0** with a description matching +G3a (it already names G3a; only the number changes). + +**Pin B3 — the G2b row must state what G2b actually did.** Read +`spec/CONTRACT_GENESIS_G2B_TUNING.md` and commit `13c3d2f` and write the +row from them, not from memory. It must name at minimum: `OperationKind` / +`OperationKindTag` **34** (`SetTuningContext`), epoch **10**, the payload as +the five-field subset `epiphany_core::TuningContextSettings` rather than the +full graph type, and — the omission that motivates this packet — the +accept-set raise **`OperationEnvelopeBlock` 2→3**, the first accept-set move +since G2a explicitly recorded staying at 2. + +**Pin B4 — regenerate `spec/binary_format.pdf`** from the amended source, +using the repository's existing build path. + +**Pin B5 — a scoped history guard, in `epiphany-testkit`.** A new test that +reads `spec/binary_format.tex` and **slices to the +`\chapter{Revision History}` section only**. Follow the loading precedent in +`crates/epiphany-testkit/tests/requirement_labels.rs` (`std::fs` from a path +relative to the manifest dir) or `text_projection_grammar.rs`'s +`include_str!` — either, but state which. + +**Pin B6 — presence of a rung *name* is not enough, and version numbers are +forbidden.** Two constraints that pull against each other, and the guard +must satisfy both. + +*Why bare name-presence fails:* "G2b" already occurs **inside the Revision +History chapter** at `binary_format.tex:3657`, in the G3a row's sentence +"`OperationEnvelopeBlock` stays at 3 where genesis tranche G2b left it." A +guard asserting only that "G2b" appears in the slice stays **green after the +new row is deleted**. It would be born dead. + +*Why version literals are also wrong:* encoding "0.14.0" would pin a number +this packet is itself moving, and the next chronology correction would have +to edit the guard — the stale hand-maintained parallel list failure +(`PLAN_GMINOR_SCHEMA_MINOR.md:156`). + +*Which rungs have principal markers:* **G2a, G-minor, G2b, G3a — not G1.** +G1 has no standalone row and this packet does not authorize inventing one +(pin B2 lists exactly four rows, one of them new). G1 is recorded +retroactively inside the G2a row at `:3603`, and that row states outright +that G1 landed "with no matching entry here." A guard demanding a G1 +principal marker would be **born red** against a document B2 leaves +correct — the guard would be wrong, not the spec. + +The guard MUST therefore assert: + +1. a **distinct principal marker** for each of **G2a, G-minor, G2b, G3a**, + matching the row form — the rung name immediately preceded by the row's + `---` separator, e.g. `--- Genesis tranche G2b`. Prose mentions cannot + satisfy this: `:3657` says "where genesis tranche G2b left it" and + `:3603` says "genesis tranche G1 --- landed at", where the separator + *follows* the name rather than preceding it. +2. **ordering** — marker offsets strictly increasing within the slice: + `G2a < G-minor < G2b < G3a`. +3. at least one **B3-specific content anchor** for the G2b row — + `SetTuningContext`, discriminant `34`, and the accept-set raise to + `OperationEnvelopeBlock` `3` — searched **only within the G2b row + segment**, i.e. the span from the G2b marker to the next marker (or the + slice end). Unbounded searching would let G3a's row, which names both + `OperationEnvelopeBlock` `3` and G2b, satisfy the anchor after the G2b + row is deleted — reintroducing the exact hole this pin exists to close. + +**G1 is deliberately unguarded.** Record that in the test's own comment, +citing `:3603`, so a later reader does not "fix" the omission by adding a +fifth marker assertion and rediscovering this contradiction. + +> **Killing mutations, three independent runs:** +> (a) delete the newly added G2b row entirely — the marker assertion goes +> red, *and* it must be confirmed that a name-only guard would have stayed +> green here, which is the finding this pin encodes; +> (b) strip the accept-set-raise clause from the G2b row, leaving its +> marker — the content anchor goes red; +> (c) move the G2b row after the G3a row — the ordering assertion goes red. +> +> All three MUST be **observed**. Packet B therefore carries **three** +> mutations, not one. + +## §B2. Touch table (Packet B) + +| # | File | Change | +|---|---|---| +| 1 | `spec/PASS13_CANDIDATES.md` | P13-S17 (pin B1) | +| 2 | `spec/binary_format.tex` | new G2b row; G3a 0.14.0 → 0.15.0; title `:243` → 0.15.0 | +| 3 | `spec/binary_format.pdf` | regenerated | +| 4 | `crates/epiphany-testkit/tests/` | the scoped history guard (pins B5–B6) | + +**Nothing else.** Packet B touches no reducer and no crate but the testkit. + +## §B3. Gate (Packet B) + +- Full workspace test, clippy, fmt, and the §C whitespace checks as in §A4. +- All **three** pin-B5/B6 mutations **observed** red and restored, + including the confirmation under (a) that a name-only guard would have + stayed green. +- The regenerated PDF's title page reads 0.15.0. + +--- + +## §C. Whitespace checking — the hole this packet closes + +`git diff --check -- crates/ spec/` is what the G3a rung used, and it is +**blind to untracked files**: it reported clean while this very contract sat +untracked. It is also blind to what is already staged. + +Per packet, in order: + +1. Stage the touch-table files explicitly. Never `git add -A`. +2. **`git diff --cached --check`** — catches whitespace in exactly what is + about to be committed, untracked-and-now-staged files included. +3. Commit. +4. **`git diff --check ..HEAD -- crates/ spec/`** — a scoped + committed-range check confirming the landed commit is clean. + +Step 4 is deliberately path-scoped. The unpushed range fails +`git diff --check` at `spikes/editor-toolkit/round1-oracle/ORACLE_SUMMARY.md:147`, +an editor-track file outside this packet's authorization. Scoping keeps that +pre-existing failure from masking a real one in `crates/` or `spec/`, and +keeps this packet from being tempted to "fix" a file it must not touch. + +--- + +## §D. Report requirements (both packets) + +State, per packet: the test count before and after; every mutation with the +**observed** failing test name; anything found that the contract did not +anticipate. If a pin turns out to be wrong or unsatisfiable, **stop and say +so** rather than working around it — pin A3 and pin A6 are rulings, not +suggestions, and pin A6 in particular forbids an addition that would look +like diligence. + +## §E. Boundary — unchanged and absolute + +These MUST NOT be read, written, or staged: `spec/PLAN_EDITOR_APP.md`, +`spec/CONTRACT_EDITOR_*.md`, `spec/ANALYSIS_GENESIS_PERSISTENCE.md`, +`spec/ANALYSIS_TEXT_RUN_PRIMITIVES.md`, `spec/DRAFT_T4_FIXTURE_RECIPE.md`, +`crates/epiphany-editor-gui/goldens/*.png`, `crates/epiphany-render-svg/**`, +`crates/epiphany-glyphs/**`, +`crates/epiphany-testkit/benches/editor_pipeline.rs`, the entire `spikes/` +tree, the unstaged root `Cargo.toml` change, and `.claude/worktrees/`. + +The narrow editor authorization granted for the G3a packet +(`epiphany-editor-core/src/barriers.rs`, `epiphany-layout-ir/src/barrier.rs`) +was spent by that packet and **does not carry forward**. This packet +authorizes no editor-crate change of any kind. + +Stage only the files in the two touch tables, explicitly. Never `git add -A`. diff --git a/spec/PLAN_GENESIS_OPS.md b/spec/PLAN_GENESIS_OPS.md index 65d8856..9f9070a 100644 --- a/spec/PLAN_GENESIS_OPS.md +++ b/spec/PLAN_GENESIS_OPS.md @@ -22,13 +22,16 @@ only **G3b** remains (ratified 2026-07-29, §4). `epiphany_core::TuningContextSettings`, **not** the full graph type — §5 trap 7's holdout, resolved in the contract as *subset over normalization*. Closed **P13-S13**. -* **G3a landed** (commit pending) — the four root-level mint families +* **G3a landed** (`6c5e69f`) — the four root-level mint families (`CreateStaffGroup`, `CreatePartDefinition`, `CreateAnalysisLayer`, `CreateView`), kinds/tags **35–38**, epoch **11**, all schema major **0**. Executed against `spec/CONTRACT_GENESIS_G3A_ENTITIES.md`; §1.1's `StaffGroup`/`Staff` authorship-authority pin was ratified 2026-07-29 as disposition B and filed as **P13-S16**. No `epiphany-bundle` change of any - kind; op-block accept-set stays at 3 where G2b left it. + kind; op-block accept-set stays at 3 where G2b left it. The undo repair + this rung's own sign-off missed — `ObjectState::Tombstoned` reachable but + under-covered for these four kinds plus `Instrument` — rides after it as + `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet A. * **G3b** — `CreateMeasure` alone, kind/tag **39**, epoch **12**, carrying graph invariant **20** and a new `PreconditionFailureReason` at discriminant **16**. Scoped, not contracted. diff --git a/spec/PLAN_GMINOR_SCHEMA_MINOR.md b/spec/PLAN_GMINOR_SCHEMA_MINOR.md index 6cc7447..d28eff1 100644 --- a/spec/PLAN_GMINOR_SCHEMA_MINOR.md +++ b/spec/PLAN_GMINOR_SCHEMA_MINOR.md @@ -187,15 +187,14 @@ numbering spaces are unrelated and must not be cross-read. > (G2b follows G2a) and prefix-closed. Epoch assignment remains a ratified > schema decision, never an implementer's choice. -> **Epoch 11 ratified 2026-07-29**, with G3a as the event (introducing commit -> pending — this rung has not yet landed a commit; update this citation once -> it does, per the same discipline as the G2a correction above). One epoch for +> **Epoch 11 ratified 2026-07-29**, with G3a as the event (introducing +> `6c5e69f`, per the same discipline as the G2a correction above). One epoch for > the whole rung's four kinds, the G2a precedent (two kinds at epoch 9) rather > than one epoch per kind. The ladder stays monotonic (G3a follows G2b) and > prefix-closed. **The ladder is complete against the audit** — every post-baseline variant in -`AUDIT_GMINOR_VOCABULARIES.md` appears exactly once: all ten kind/tag pairs, +`AUDIT_GMINOR_VOCABULARIES.md` appears exactly once: all fifteen kind/tag pairs, `OperationPayload` 3, `ReanchorReason` 6, and all six `PreconditionFailureReason` appends.