diff --git a/crates/epiphany-core/src/invariants.rs b/crates/epiphany-core/src/invariants.rs index abe4683..93b18ca 100644 --- a/crates/epiphany-core/src/invariants.rs +++ b/crates/epiphany-core/src/invariants.rs @@ -2633,6 +2633,34 @@ impl<'a> GraphIndex<'a> { /// ALREADY-RESOLVING signatures are compared (pin 9b, "a resolving /// `Some(id)`"), whether that is the measure's own declared /// signature or a grid entry's. + /// + /// **The nine non-success paths** below the body's two `match` + /// ladders, enumerated and classified by + /// `spec/CONTRACT_P13S18_MATRIX.md` pins 1–2 (a diagnostic listing: + /// descriptive of existing behaviour, not normative, and it moves no + /// line of the executable body below). Exactly three are genuine + /// abstentions; the rest are inapplicable, vacuous, delegated + /// elsewhere, or a separately-filed deferral: + /// + /// | Id | Clause | Path | Class | + /// |---|---|---|---| + /// | A1 | agreement | `m.time_signature` is `None` | inapplicable — no declared signature can disagree with anything | + /// | A2 | agreement | declared signature does not resolve | delegated to invariant 10's per-measure arm | + /// | A3 | agreement | `Governing20::None` | vacuous — no governing signature exists to disagree with | + /// | A4 | agreement | `Governing20::Indeterminate` | genuine abstention — the relation cannot place a candidate | + /// | B1 | boundary | first measure (`i == 0`) | the pickup/anacrusis deferral, filed as `P13-S19` | + /// | B2 | boundary | governing signature does not resolve | delegated to invariant 10's grid-level arms | + /// | B3 | boundary | `Governing20::None` | vacuous, same as A3 | + /// | B4 | boundary | `Governing20::Indeterminate` | genuine abstention, same as A4 | + /// | B5 | boundary | musical delta not computable | genuine abstention — order without distance | + /// + /// A2 and B2 are `delegated`, not merely unenforced, only because + /// invariant 10 actually reports the same unresolving reference on + /// the same graph (`spec/CONTRACT_P13S18_MATRIX.md` pin 3) — see + /// `g3b_measure20_tests::m39_unresolvable_reference_is_invariant_ + /// 10_only` (A2) and `matrix_b2_governing_signature_unresolving_ + /// delegated` (B2) below, and M7/M8 in the contract's mutation + /// plan. fn check_measure_meter_consistency(&self, out: &mut Vec) { let time_sigs: HashMap = self .score @@ -4546,6 +4574,7 @@ mod g3a_tests { #[cfg(test)] mod g3b_measure20_tests { use super::*; + use crate::event::Rest; use crate::graph::{ BeatGroup, Measure, MeterChange, MetricGrid, MetricTimeModel, PowerOfTwo, Region, RegionContent, RegionTimeModel, StaffBasedContent, StaffExtent, StaffInstance, TimeExtent, @@ -4672,6 +4701,31 @@ mod g3b_measure20_tests { region } + /// Inserts a minimal LIVE `Rest` event into `score` and returns its id + /// (`spec/CONTRACT_P13S18_MATRIX.md` pin 4, S6/S7): `Measure.start` and + /// `MeterChange.anchor` are unrestricted `TimeAnchor`s, so an + /// `Event`-anchored measure is a legal graph, not a hypothetical one -- + /// the event this mints and inserts is genuinely live in `score.events`, + /// not a dangling/ghost id (contrast `inv10_flags_dangling_spanner_ + /// anchor`'s `ghost_event`, in `review_fix_tests` above, which is the + /// deliberately-NOT-live case). + fn insert_live_event(score: &mut Score) -> crate::ids::EventId { + let event_id: crate::ids::EventId = score.identity.mint(); + let voice_id: crate::ids::VoiceId = score.identity.mint(); + score + .events + .insert(Event::Rest(Rest { + id: event_id, + voice: voice_id, + position: EventPosition::Musical(MusicalPosition(RationalTime::from_int(0))), + duration: EventDuration::Musical(MusicalDuration::whole()), + vertical_position: None, + visible: true, + })) + .unwrap(); + event_id + } + #[test] fn agreement_and_boundary_hold_together() { let replica = ReplicaId(7); @@ -4859,6 +4913,1101 @@ mod g3b_measure20_tests { unresolving reference is only invariant 10's violation" ); } + + // ------------------------------------------------------------------- + // spec/CONTRACT_P13S18_MATRIX.md: the outcome matrix (9 shapes x 2 + // clauses = 18 cells) plus the four non-shape-driven paths (A1, A3, B2, + // B3) that pin 4's shapes do not themselves exercise. A2 and B1 reuse + // `m39_unresolvable_reference_is_invariant_10_only` and + // `m38_pickup_first_measure_not_flagged` above respectively; S3 reuses + // `m34_agreement_flags_disagreement` and `m35_boundary_flags_wrong_ + // distance` above (Region same id, same edge, Musical offsets is + // exactly their shape). Every other cell gets a dedicated fixture below. + // ------------------------------------------------------------------- + + /// Matrix cell A1: `m.time_signature` is `None` -- inapplicable, not + /// concealed disagreement. A single (first) measure keeps the boundary + /// clause vacuous (B1) so only A1 is live here. M4 flips this measure to + /// a resolving, DISAGREEING `Some(id)` and must turn this from silent to + /// a violation. + #[test] + fn matrix_a1_none_time_signature_inapplicable() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let region = probe_region_id(); + let m0 = measure_at(MeasureId::new(replica, 10), region, 0, None); + let (score, _) = score_with(Some(active), vec![ts_active], vec![m0]); + assert!( + !fires(&score, GraphInvariant::MeasureMeterConsistency), + "A1: a measure with no declared time signature must not be \ + flagged by the agreement clause" + ); + } + + /// Matrix cell A3: `Governing20::None` -- vacuous, not a violation, + /// because the region-default grid is empty (pin 6c case 1) so there is + /// no candidate at all. A single (first) measure keeps the boundary + /// clause vacuous (B1) so only A3 is live here. A bare `fires` boolean + /// cannot distinguish "vacuous" from any of the other eight paths, so + /// this uses a paired positive control: fixture 1 is the claimed + /// abstention (`m0` declares a DISAGREEING, resolving signature against + /// an EMPTY grid); fixture 2 changes ONLY the grid -- from empty to a + /// real entry naming the very signature `m0` disagrees with -- and must + /// decide and flag. The flip from fixture 1 to fixture 2 is exactly + /// M10's edit, now inside the test. + #[test] + fn matrix_a3_vacuous_agreement() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let region = probe_region_id(); + let m0 = measure_at(MeasureId::new(replica, 10), region, 0, Some(wrong)); + // Fixture 1: no grid at all, so there is no candidate for the + // governing search to find regardless of what m0 declares. + let (empty_score, _) = score_with( + None, + vec![ts_active.clone(), ts_wrong.clone()], + vec![m0.clone()], + ); + let empty_violations = + check_invariant(&empty_score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + empty_violations.len(), + 0, + "A3: with no grid entries at all, the agreement clause must \ + abstain as vacuous -- got {empty_violations:?}" + ); + // Fixture 2 (positive control): ONLY the grid changes, from empty + // to a real, disagreeing entry. + let (populated_score, _) = score_with(Some(active), vec![ts_active, ts_wrong], vec![m0]); + let populated_violations = + check_invariant(&populated_score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + populated_violations.len(), + 1, + "A3 positive control: a non-empty, disagreeing grid must decide \ + and flag -- got {populated_violations:?}" + ); + assert!( + populated_violations[0] + .witness + .contains("declares time signature"), + "A3 positive control: the violation must be the agreement \ + clause's -- witness was {:?}", + populated_violations[0].witness + ); + } + + /// Matrix cell B2 (delegated -- verified, not asserted, pin 3): the + /// SAME graph that makes invariant 20's boundary clause abstain (B2, + /// the grid's OWN governing signature does not resolve) must + /// independently violate invariant 10's grid-level resolution arm. + /// `m39_unresolvable_reference_is_invariant_10_only` (above) is the twin + /// observation for A2 (the MEASURE's own declared signature failing to + /// resolve); this is the grid-entry case, and M8 shows the SAME + /// condition go unreported by the whole suite once invariant 10's + /// grid-level arm is deleted. + #[test] + fn matrix_b2_governing_signature_unresolving_delegated() { + let replica = ReplicaId(7); + let undeclared = TimeSignatureId::new(replica, 999); + let region = probe_region_id(); + let m0 = measure_at(MeasureId::new(replica, 10), region, 0, None); + let m1 = measure_at(MeasureId::new(replica, 11), region, 1, None); + // The INSTANCE-LOCAL grid's own entry (not the region default -- + // M8 targets invariant 10's instance-local-grid arm specifically) + // names a signature that is never declared -- unresolvable by + // either invariant's own logic, but reported ONLY by invariant 10. + let (mut score, _) = score_with(None, vec![], vec![m0, m1]); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.staff_instances[0].local_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }, + time_signature: undeclared, + }], + }); + } + assert!( + fires(&score, GraphInvariant::CrossCuttingRefsResolve), + "the instance-local grid's undeclared time-signature reference \ + must violate invariant 10's instance-local-grid arm" + ); + assert!( + !fires(&score, GraphInvariant::MeasureMeterConsistency), + "B2: invariant 20's boundary clause must abstain rather than \ + duplicate invariant 10's resolution check -- the grid's own \ + governing signature does not resolve" + ); + } + + /// Matrix cell B3: `Governing20::None` at the boundary clause -- vacuous, + /// same as A3, because the region-default grid is empty (pin 6c case + /// 1). A wrong boundary distance (2 whole notes, not 1) is baked in + /// deliberately so the abstention is load-bearing. As with A3, a bare + /// boolean cannot distinguish "vacuous" from the other eight paths, so + /// this uses a paired positive control: fixture 1 is the claimed + /// abstention (empty grid, wrong distance already staged); fixture 2 + /// changes ONLY the grid -- from empty to a real, comparable entry -- + /// and the SAME wrong distance must now be flagged. The flip from + /// fixture 1 to fixture 2 is M10's edit, now inside the test. + #[test] + fn matrix_b3_vacuous_boundary() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let region = probe_region_id(); + let m0 = measure_at(MeasureId::new(replica, 10), region, 0, None); + let m1 = measure_at(MeasureId::new(replica, 11), region, 2, None); + // Fixture 1: no grid at all. + let (empty_score, _) = + score_with(None, vec![ts_active.clone()], vec![m0.clone(), m1.clone()]); + let empty_violations = + check_invariant(&empty_score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + empty_violations.len(), + 0, + "B3: with no grid entries at all, the boundary clause must \ + abstain as vacuous -- got {empty_violations:?}" + ); + // Fixture 2 (positive control): ONLY the grid changes, from empty + // to a real, comparable entry -- the SAME wrong distance (2 whole + // notes, not 1) is untouched. + let (populated_score, _) = score_with(Some(active), vec![ts_active], vec![m0, m1]); + let populated_violations = + check_invariant(&populated_score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + populated_violations.len(), + 1, + "B3 positive control: a non-empty, comparable grid must decide \ + and flag the wrong distance -- got {populated_violations:?}" + ); + assert!( + populated_violations[0] + .witness + .contains("is not exactly one"), + "B3 positive control: the violation must be the boundary \ + clause's -- witness was {:?}", + populated_violations[0].witness + ); + } + + /// Matrix row S1 (`WallClock` measures, `WallClock`-anchored meter + /// changes): agreement DECIDES (`D`) and boundary abstains as B5 -- + /// pin 5's split. `m0`'s agreement clause and `m1`'s boundary clause + /// share the EXACT SAME governing search + /// (`measure20_governing_time_signature(sequence, &m0.start)`), so + /// `m0`'s violation firing is itself the proof that search decided + /// `Unique`, not `Indeterminate` -- ruling out B4 and pinning the + /// boundary abstention to B5 (the `WallClock` delta, structurally never + /// computable) rather than an incomparable governing search. `m1` sits + /// at a deliberately wrong `WallClock` distance from `m0`, so a live + /// boundary clause would flag it; only ONE violation (agreement, on + /// `m0`) is observed. + #[test] + fn matrix_s1_wallclock_measures_wallclock_meter_changes() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let m0 = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let m1 = Measure { + id: MeasureId::new(replica, 11), + start: TimeAnchor::WallClock { + time: WallClockTime(999_999_999), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + let (mut score, _) = score_with(None, vec![ts_active, ts_wrong], vec![]); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![m0, m1]; + } + let violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + violations.len(), + 1, + "S1: expected exactly one violation (m0's agreement) -- got {violations:?}" + ); + assert!( + violations[0].witness.contains("declares time signature"), + "S1: the sole violation must be the agreement clause's, not the \ + boundary clause's -- witness was {:?}", + violations[0].witness + ); + } + + /// Matrix row S2, agreement cell (`WallClock` measures, `Region`- + /// anchored meter changes): `comparable_order` has no arm for + /// `WallClock`<->`Region` at all (falls to the catch-all `_ => None`) + /// -- structurally incomparable regardless of any offset or timestamp. + /// `x` (a single, `WallClock`-anchored measure) declares a resolving, + /// disagreeing signature and is not flagged: A4. Paired positive + /// control: fixture 2 changes ONLY `x.start`, from `WallClock` to the + /// grid's own `Region` shape, and the SAME disagreement must decide and + /// flag -- M1 is fixture 1's `x.start` edit. + #[test] + fn matrix_s2_agreement_a4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let x_wallclock = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + // Fixture 1: `x` is WallClock-anchored -- incomparable to the + // Region-anchored grid. + let (mut score, region) = score_with( + Some(active), + vec![ts_active.clone(), ts_wrong.clone()], + vec![], + ); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.staff_instances[0].measures = vec![x_wallclock]; + } + let wallclock_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + wallclock_violations.len(), + 0, + "S2 agreement: a WallClock-anchored measure against a \ + Region-anchored grid must abstain (A4) -- got \ + {wallclock_violations:?}" + ); + // Fixture 2 (positive control): ONLY `x.start` changes, to the + // grid's own Region{Start, Zero} shape. + let x_region = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let (mut score2, _) = score_with(Some(active), vec![ts_active, ts_wrong], vec![]); + if let RegionContent::StaffBased(content) = &mut score2.canvas.regions[0].content { + content.staff_instances[0].measures = vec![x_region]; + } + let region_violations = check_invariant(&score2, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + region_violations.len(), + 1, + "S2 agreement positive control: a Region-anchored measure \ + matching the grid must decide and flag -- got \ + {region_violations:?}" + ); + assert!( + region_violations[0] + .witness + .contains("declares time signature"), + "S2 agreement positive control: the violation must be the \ + agreement clause's -- witness was {:?}", + region_violations[0].witness + ); + } + + /// Matrix row S2, boundary cell: `x` (index 1, `WallClock`-anchored, + /// carrying a resolving disagreeing signature so it is structurally + /// eligible for A4 too -- see `matrix_s2_agreement_a4`) is preceded by + /// `prev` (index 0, also `WallClock`-anchored): B4. A `WallClock` + /// measure's boundary clause can NEVER decide-and-flag (`measure20_ + /// musical_delta` has no `WallClock` arm at all, pin 5/S1), so the + /// positive control cannot be "x's boundary now flags" -- instead it + /// changes ONLY `prev.start` to the grid's `Region` shape and observes + /// `prev`'s OWN agreement clause, which reuses the IDENTICAL governing + /// search `x`'s boundary clause performs on `prev.start`. That the + /// identical search decides once `prev.start` alone is comparable is + /// the proof that the silence in fixture 1 was genuine indeterminacy + /// (B4), not vacuity (B3) or non-resolution (B2) -- and `x`'s own + /// boundary clause is asserted silent in BOTH fixtures, confirming the + /// change didn't leak into a delta becoming computable. M2 is fixture + /// 1's `prev.start` edit. + #[test] + fn matrix_s2_boundary_b4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let prev_wallclock = Measure { + id: MeasureId::new(replica, 9), + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let x = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::WallClock { + time: WallClockTime(500), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + // Fixture 1: `prev` is WallClock-anchored -- incomparable to the + // Region-anchored grid. + let (mut score, region) = score_with( + Some(active), + vec![ts_active.clone(), ts_wrong.clone()], + vec![], + ); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.staff_instances[0].measures = vec![prev_wallclock, x.clone()]; + } + let wallclock_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + wallclock_violations.len(), + 0, + "S2 boundary: with `prev` WallClock-anchored against a \ + Region-anchored grid, both `prev`'s agreement and `x`'s \ + boundary must abstain (A4/B4) -- got {wallclock_violations:?}" + ); + // Fixture 2 (positive control): ONLY `prev.start` changes, to the + // grid's own Region{Start, Zero} shape. `x` is untouched. + let prev_region = Measure { + id: MeasureId::new(replica, 9), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let (mut score2, _) = score_with(Some(active), vec![ts_active, ts_wrong], vec![]); + if let RegionContent::StaffBased(content) = &mut score2.canvas.regions[0].content { + content.staff_instances[0].measures = vec![prev_region, x]; + } + let region_violations = check_invariant(&score2, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + region_violations.len(), + 1, + "S2 boundary positive control: with `prev` now comparable to \ + the grid, `prev`'s OWN agreement clause (the identical \ + governing search `x`'s boundary performs) must decide and \ + flag -- got {region_violations:?}" + ); + assert!( + region_violations[0] + .witness + .contains("declares time signature"), + "S2 boundary positive control: the violation must be `prev`'s \ + agreement clause's, not a new boundary violation on `x` -- a \ + WallClock delta is structurally never computable (pin 5), so \ + `x`'s boundary stays silent even though `prev`'s governing \ + search now decides -- witness was {:?}", + region_violations[0].witness + ); + } + + /// Matrix row S4: `Measure` **same id**, `pos: End` on both sides, + /// `Musical` offsets (c2) -- the shape that falsifies "any `Measure` + /// end anchor is incomparable": same id AND same `pos` decides via c2's + /// offset comparison, exactly like same-id `Start`. Both clauses DECIDE + /// (`D`/`D`), deliberately wrong so the decision is observed as a + /// violation rather than a pass that could have come from anywhere. + #[test] + fn matrix_s4_measure_same_id_end_end_decides() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let shared_end = MeasureId::new(replica, 500); + let m0 = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Measure { + id: shared_end, + position: MeasurePosition::End, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let m1 = Measure { + id: MeasureId::new(replica, 11), + start: TimeAnchor::Measure { + id: shared_end, + position: MeasurePosition::End, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(2))), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + let (mut score, _) = score_with(None, vec![ts_active, ts_wrong], vec![]); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Measure { + id: shared_end, + position: MeasurePosition::End, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![m0, m1]; + } + let violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + violations.len(), + 2, + "S4: same-id End<->End must decide BOTH clauses (D/D) -- got \ + {violations:?}" + ); + assert!( + violations + .iter() + .any(|v| v.witness.contains("declares time signature")), + "S4: expected an agreement violation on m0 -- got {violations:?}" + ); + assert!( + violations + .iter() + .any(|v| v.witness.contains("is not exactly one")), + "S4: expected a boundary violation on m1 -- got {violations:?}" + ); + } + + /// Matrix row S5 (`Measure` **distinct** ids, `Start`, `Zero` -- c3): + /// the contrast to S4. c3's vector-index ordering DOES decide + /// (agreement: `D`) but supplies no distance at all (boundary: B5) -- + /// pin 10's second deficiency. Three measures in one instance: + /// `filler` (index 0, purely an anchor target), `prev` (index 1) and + /// `m` (index 2, under test). The grid's sole entry is anchored to + /// `filler`'s id -- DISTINCT from both `prev`'s and `m`'s own + /// self-referencing ids -- so every governing search below goes + /// through c3's vector order, never c2. `m` declares a disagreeing + /// signature (agreement fires); the boundary delta between `prev` and + /// `m` is structurally impossible (distinct ids), so it must abstain + /// regardless of distance -- no wrong distance is even staged here. + #[test] + fn matrix_s5_measure_distinct_ids_start_zero() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let filler_id = MeasureId::new(replica, 20); + let prev_id = MeasureId::new(replica, 21); + let m_id = MeasureId::new(replica, 22); + let filler = Measure { + id: filler_id, + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + let prev = Measure { + id: prev_id, + start: TimeAnchor::Measure { + id: prev_id, + position: MeasurePosition::Start, + offset: AnchorOffset::Zero, + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + let m = Measure { + id: m_id, + start: TimeAnchor::Measure { + id: m_id, + position: MeasurePosition::Start, + offset: AnchorOffset::Zero, + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let (mut score, _) = score_with(None, vec![ts_active, ts_wrong], vec![]); + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Measure { + id: filler_id, + position: MeasurePosition::Start, + offset: AnchorOffset::Zero, + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![filler, prev, m]; + } + let violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + violations.len(), + 1, + "S5: expected exactly one violation (m's agreement, decided via \ + c3's vector order) -- got {violations:?}" + ); + assert!( + violations[0].witness.contains("declares time signature"), + "S5: the sole violation must be the agreement clause's -- \ + boundary (B5) has no distance to report even though its \ + governing search also decided via c3 -- witness was {:?}", + violations[0].witness + ); + } + + /// Matrix row S6 (`Event` **same id**, a LIVE event, `Musical` offsets + /// -- c1): `Measure.start` and `MeterChange.anchor` are unrestricted + /// `TimeAnchor`s, so an `Event`-anchored measure is a legal (if + /// unusual) graph, not a hypothetical one -- the event inserted here is + /// genuinely live in `score.events`. Both clauses DECIDE (`D`/`D`), + /// deliberately wrong. + #[test] + fn matrix_s6_event_same_id_live_event_decides() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, _) = score_with(None, vec![ts_active, ts_wrong], vec![]); + let live = insert_live_event(&mut score); + let m0 = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Event { + id: live, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let m1 = Measure { + id: MeasureId::new(replica, 11), + start: TimeAnchor::Event { + id: live, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(2))), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Event { + id: live, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![m0, m1]; + } + let violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + violations.len(), + 2, + "S6: same-id live-Event anchors must decide BOTH clauses (D/D) \ + -- got {violations:?}" + ); + assert!( + violations + .iter() + .any(|v| v.witness.contains("declares time signature")), + "S6: expected an agreement violation on m0 -- got {violations:?}" + ); + assert!( + violations + .iter() + .any(|v| v.witness.contains("is not exactly one")), + "S6: expected a boundary violation on m1 -- got {violations:?}" + ); + } + + /// Matrix row S7, agreement cell (`Event`, DISTINCT ids, otherwise + /// identical to S6): isolates the distinct-`Event` fall-through -- + /// unlike `Measure`'s c3, there is no vector-index fallback for + /// `Event`s, so distinct ids are UNCONDITIONALLY incomparable. `x` (a + /// single, live-`Event`-anchored measure referencing `event_a`) + /// declares a resolving, disagreeing signature against a grid entry + /// referencing the DISTINCT `event_b`: A4. Paired positive control: + /// fixture 2 changes ONLY the grid's referent, from `event_b` to + /// `event_a` (matching `x`), and the SAME disagreement must decide and + /// flag -- exactly the case the retained P11-C5 citation at + /// `CONTRACT_GENESIS_G3B_MEASURE.md:223` exists for. (M1/M2, the + /// contract's ratified A4/B4 mutation pair, target S8 below; this cell + /// has no separately-numbered mutation, matching A3/A2's ratified + /// scope.) + #[test] + fn matrix_s7_agreement_a4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, _) = score_with(None, vec![ts_active.clone(), ts_wrong.clone()], vec![]); + let event_a = insert_live_event(&mut score); + let event_b = insert_live_event(&mut score); + let x = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Event { + id: event_a, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(2))), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + // Fixture 1: the grid references `event_b`, distinct from `x`'s + // own `event_a`. + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Event { + id: event_b, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![x]; + } + let distinct_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + distinct_violations.len(), + 0, + "S7 agreement: a distinct-Event-id grid entry must abstain \ + (A4) -- got {distinct_violations:?}" + ); + // Fixture 2 (positive control): ONLY the grid's referent changes, + // from `event_b` to `event_a`, matching `x`. + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Event { + id: event_a, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + } + let matching_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + matching_violations.len(), + 1, + "S7 agreement positive control: a matching-Event-id grid entry \ + must decide and flag -- got {matching_violations:?}" + ); + assert!( + matching_violations[0] + .witness + .contains("declares time signature"), + "S7 agreement positive control: the violation must be the \ + agreement clause's -- witness was {:?}", + matching_violations[0].witness + ); + } + + /// Matrix row S7, boundary cell: `x` (index 1, `Event`-anchored to + /// `event_a`, carrying a resolving disagreeing signature so it is + /// structurally eligible for A4 too -- see `matrix_s7_agreement_a4`) is + /// preceded by `prev` (index 0, ALSO `Event`-anchored to `event_a` -- + /// `prev` and `x` already share a referent; only the grid's `event_b` + /// is the outlier): B4. Unlike S2's structurally-forced `WallClock` + /// delta (never computable, pin 5), `measure20_musical_delta`'s + /// `Event` arm decides fine once ids match, so the paired positive + /// control here changes ONLY the grid's referent (`event_b` -> + /// `event_a`, matching what `prev`, and `x`, already share) and THREE + /// clauses decide and flag together: `prev`'s own agreement, `x`'s own + /// agreement (it too references `event_a` and disagrees), and `x`'s + /// boundary -- a stronger, triply-confirmed observation than S2's + /// single witness, for the same underlying governing-search reason. + #[test] + fn matrix_s7_boundary_b4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, _) = score_with(None, vec![ts_active.clone(), ts_wrong.clone()], vec![]); + let event_a = insert_live_event(&mut score); + let event_b = insert_live_event(&mut score); + let prev = Measure { + id: MeasureId::new(replica, 9), + start: TimeAnchor::Event { + id: event_a, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let x = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Event { + id: event_a, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(2))), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + // Fixture 1: the grid references `event_b`, distinct from `prev`'s + // own `event_a`. + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Event { + id: event_b, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![prev.clone(), x.clone()]; + } + let distinct_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + distinct_violations.len(), + 0, + "S7 boundary: with `prev` referencing a distinct Event id from \ + the grid, both `prev`'s agreement and `x`'s boundary must \ + abstain (A4/B4) -- got {distinct_violations:?}" + ); + // Fixture 2 (positive control): ONLY the grid's referent changes, + // from `event_b` to `event_a`, matching `prev` (and `x`, since both + // still reference `event_a`). + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Event { + id: event_a, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: active, + }], + }); + } + let matching_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + matching_violations.len(), + 3, + "S7 boundary positive control: with the grid now matching \ + `prev`, and `x` (same event id), THREE clauses all newly \ + comparable at once decide and flag: `prev`'s own agreement, \ + `x`'s own agreement (it too shares `event_a` and disagrees), \ + and `x`'s boundary (now a computable Event delta, unlike S2's \ + structurally-impossible WallClock case) -- got \ + {matching_violations:?}" + ); + assert_eq!( + matching_violations + .iter() + .filter(|v| v.witness.contains("declares time signature")) + .count(), + 2, + "S7 boundary positive control: expected agreement violations \ + on BOTH prev and x -- got {matching_violations:?}" + ); + assert!( + matching_violations + .iter() + .any(|v| v.witness.contains("is not exactly one")), + "S7 boundary positive control: expected x's boundary violation \ + -- got {matching_violations:?}" + ); + } + + /// Matrix row S8, agreement cell (matching referent, DIFFERING + /// `pos`/`edge` selector): the `ia == ib && ea == eb` conjunction + /// (Region) requires an IDENTICAL selector, never merely an identical + /// id. `x` (a single, `Region`-anchored measure at `End`) declares a + /// resolving, disagreeing signature against a grid entry at `Start`, + /// same `Region` id: A4. Paired positive control: fixture 2 changes + /// ONLY `x`'s own edge, from `End` to `Start` (matching the grid), and + /// the SAME disagreement must decide and flag. M1 is fixture 1's + /// `x`-edge edit. + #[test] + fn matrix_s8_agreement_a4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, region) = + score_with(None, vec![ts_active.clone(), ts_wrong.clone()], vec![]); + let x_end = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::End, + offset: AnchorOffset::Zero, + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![x_end]; + } + let end_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + end_violations.len(), + 0, + "S8 agreement: an End-anchored measure against a Start-anchored \ + grid entry (same Region id) must abstain (A4) -- got \ + {end_violations:?}" + ); + // Fixture 2 (positive control): ONLY `x`'s own edge changes, from + // `End` to `Start`, matching the grid. + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.staff_instances[0].measures[0].start = TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }; + } + let start_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + start_violations.len(), + 1, + "S8 agreement positive control: a Start-anchored measure \ + matching the grid must decide and flag -- got \ + {start_violations:?}" + ); + assert!( + start_violations[0] + .witness + .contains("declares time signature"), + "S8 agreement positive control: the violation must be the \ + agreement clause's -- witness was {:?}", + start_violations[0].witness + ); + } + + /// Matrix row S8, boundary cell: `x` (index 1, `Region`-anchored at + /// `End`, carrying a resolving disagreeing signature so it is + /// structurally eligible for A4 too -- see `matrix_s8_agreement_a4`) is + /// preceded by `prev` (index 0, also `Region`-anchored at `End`): B4. + /// The positive control moves the GRID entry's edge to `End`, not + /// `prev`'s. Both levers restore the governing search, but only this one + /// leaves `prev` and `x` c4-comparable to each other, so + /// `measure20_musical_delta`'s Region arm (`ia == ib && ea == eb`) still + /// yields a delta and **`x`'s own boundary clause fires**. Moving `prev` + /// instead would break that match and leave the boundary silent for a + /// second reason, signing this cell by inference from a shared call + /// rather than by observing it. **S2 has no such lever** -- a `WallClock` + /// delta is never computable (pin 5) -- so its control legitimately + /// observes `prev`'s agreement, and that exception is S2's alone. + /// M2 is fixture 1's grid-edge edit. + #[test] + fn matrix_s8_boundary_b4() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, region) = + score_with(None, vec![ts_active.clone(), ts_wrong.clone()], vec![]); + let prev_end = Measure { + id: MeasureId::new(replica, 9), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::End, + offset: AnchorOffset::Zero, + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let x = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::End, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(2))), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.default_metric_grid = Some(MetricGrid { + meter_sequence: vec![MeterChange { + anchor: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Zero, + }, + time_signature: active, + }], + }); + content.staff_instances[0].measures = vec![prev_end, x]; + } + let end_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + end_violations.len(), + 0, + "S8 boundary: with `prev` End-anchored against a Start-anchored \ + grid entry, both `prev`'s agreement and `x`'s boundary must \ + abstain (A4/B4) -- got {end_violations:?}" + ); + // Fixture 2 (positive control): ONLY the grid entry's edge changes, + // from `Start` to `End`, matching both measures. Neither measure + // moves -- which is the point: `prev` and `x` stay Region{End} and + // therefore stay c4-comparable to EACH OTHER, so the delta survives + // and `x`'s boundary clause itself decides. Moving `prev` instead + // would restore the governing search while breaking `prev`<->`x`, + // leaving the boundary silent for a second reason and signing this + // cell by inference rather than observation. (S2 has no such option: + // a WallClock delta is structurally never computable, pin 5, so its + // control legitimately observes `prev`'s agreement instead. That + // exception is S2's alone.) + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content + .default_metric_grid + .as_mut() + .expect("the grid was just installed") + .meter_sequence[0] + .anchor = TimeAnchor::Region { + id: region, + edge: RegionEdge::End, + offset: AnchorOffset::Zero, + }; + } + let matching_violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + matching_violations.len(), + 3, + "S8 boundary positive control: with the grid now End-anchored, \ + three clauses newly decide at once -- `prev`'s agreement, \ + `x`'s agreement, and `x`'s BOUNDARY (a computable c4 delta, \ + since both measures are still Region{{End}}) -- got \ + {matching_violations:?}" + ); + assert_eq!( + matching_violations + .iter() + .filter(|v| v.witness.contains("declares time signature")) + .count(), + 2, + "S8 boundary positive control: expected agreement violations on \ + BOTH prev and x -- got {matching_violations:?}" + ); + assert!( + matching_violations + .iter() + .any(|v| v.witness.contains("is not exactly one")), + "S8 boundary positive control: expected `x`'s OWN boundary \ + violation, which is what attributes fixture 1's silence to B4 \ + rather than to a downstream delta failure -- got \ + {matching_violations:?}" + ); + } + + /// Matrix row S9 (pin 7's behavioural lock): one instance, heterogeneous + /// measure anchors. THREE measures, deliberately distinct roles so the + /// pin-7 contrast and the row's own A4/B4 cell pair don't get + /// conflated into one false "same measure" claim (the mistake defect 2 + /// found in this row's first draft): + /// + /// - `q` (index 0, `Region`-anchored, matching the grid) is pin 7's + /// REQUIRED contrast -- "another measure ... reaches a decision" -- + /// and decides (deliberately wrong, so it flags). + /// - `r` (index 1, `WallClock`-anchored, `None` declared) is purely + /// `p`'s predecessor; it carries no claim of its own. + /// - `p` (index 2, `WallClock`-anchored like `r`, resolving disagreeing + /// signature) is the row's A4/B4 EXHIBIT: its own agreement clause + /// abstains (A4, `p.start` incomparable to the grid) AND its own + /// boundary clause abstains (B4, `r.start` -- `p`'s predecessor -- + /// ALSO incomparable to the grid), on ONE measure, per defect 2. + /// + /// `q` cannot double as `p`'s predecessor: if it did, `p`'s boundary + /// governing search would use `q.start`, which IS comparable to the + /// grid (that's why `q` decides) -- and `p`'s boundary would then + /// decide too, not abstain. Splitting the roles across THREE measures + /// is what makes both claims true at once. Exactly ONE violation -- + /// naming `q`, never `p` or `r` -- is pin 7's behavioural proof; a + /// prose claim that "one incomparable change disables the whole + /// instance" would predict zero. M6 gives `q` the SAME `WallClock` + /// shape as `r`/`p` and only then does its agreement clause stop + /// deciding. + #[test] + fn matrix_s9_heterogeneous_measure_anchors() { + let replica = ReplicaId(7); + let (active, ts_active) = sig(replica, 1); + let (wrong, ts_wrong) = sig(replica, 2); + let (mut score, region) = score_with(Some(active), vec![ts_active, ts_wrong], vec![]); + let q = Measure { + id: MeasureId::new(replica, 9), + start: TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Musical(MusicalDuration::zero()), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + let q_id = q.id; + let r = Measure { + id: MeasureId::new(replica, 10), + start: TimeAnchor::WallClock { + time: WallClockTime(0), + }, + time_signature: None, + explicit_number: None, + number_visibility: Default::default(), + }; + let p = Measure { + id: MeasureId::new(replica, 11), + start: TimeAnchor::WallClock { + time: WallClockTime(500), + }, + time_signature: Some(wrong), + explicit_number: None, + number_visibility: Default::default(), + }; + if let RegionContent::StaffBased(content) = &mut score.canvas.regions[0].content { + content.staff_instances[0].measures = vec![q, r, p]; + } + let violations = check_invariant(&score, GraphInvariant::MeasureMeterConsistency); + assert_eq!( + violations.len(), + 1, + "S9: exactly one measure's agreement clause (q's) must decide \ + in this instance -- got {violations:?}" + ); + assert!( + violations[0].witness.contains(&format!("{q_id:?}")), + "S9: the sole violation must name q, proving p's abstention \ + (A4) and r's presence did not disable the whole instance -- \ + witness was {:?}", + violations[0].witness + ); + } } /// Genesis tranche G3b packet 2: M40, asserted BEHAVIOURALLY against diff --git a/spec/CONTRACT_GENESIS_G3B_MEASURE.md b/spec/CONTRACT_GENESIS_G3B_MEASURE.md index c1d7286..325950a 100644 --- a/spec/CONTRACT_GENESIS_G3B_MEASURE.md +++ b/spec/CONTRACT_GENESIS_G3B_MEASURE.md @@ -203,7 +203,7 @@ and core says so.** With a nonzero offset the selector does not bound the point: `Region{edge: Start, off: Musical(100)}` is **not** provably before `Region{edge: End, off: Zero}` without knowing the region's length. The same holds for `Measure` Start vs End — and -`crates/epiphany-core/src/invariants.rs:400`ff records exactly this: the +`crates/epiphany-core/src/invariants.rs:466`ff records exactly this: the prototype anchor resolver places `Measure` **start** anchors and `Region` edges but returns `None` for a `Measure` **end**, because a coordinate "cannot be placed without the deferred tempo/measure-length machinery." @@ -344,7 +344,8 @@ is deliberate: **not** a safety property. File the residue as **P13-S18**: invariant 20's agreement and boundary checks -are partial, and P11-C5 resolved positions are what would close them. +are partial, and **P13-S23** — the general common-timeline/musical-distance +capability, filed against this residue — is what would close them. **Status: open, deliberately.** **Pin 8 — referential preconditions.** diff --git a/spec/CONTRACT_P13S18_MATRIX.md b/spec/CONTRACT_P13S18_MATRIX.md index 419dc30..b70446f 100644 --- a/spec/CONTRACT_P13S18_MATRIX.md +++ b/spec/CONTRACT_P13S18_MATRIX.md @@ -1,6 +1,6 @@ # Contract — P13-S18: the invariant-20 outcome matrix -**Status:** DRAFT. +**Status:** RATIFIED. **Rung type:** diagnostic and bookkeeping. **No behaviour change.** No graph that violates invariant 20 today may stop violating it, and no graph that passes today @@ -30,7 +30,7 @@ and re-confirmed unaffected at `f33673d` (see §4). - **Same id, same position — `End`↔`End` is comparable *when its offsets compare*.** c2 requires `ia == ib && pa == pb` and then delegates to `measure20_offset_order`, which returns `None` for `Musical`↔`WallClock` - (`:2427`–`:2428`). So "any `Measure` end anchor" is false as written, but + (`:2428`–`:2429`). So "any `Measure` end anchor" is false as written, but the counter-example is conditional and must be stated that way. - **Distinct ids — `End` anchors remain incomparable**, because c3 returns `None` unless `*pa == MeasurePosition::Start` with both offsets `Zero`. A diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index c06bc8e..ab1118a 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -95,8 +95,9 @@ visible — a value with a wire form and no canonical carrier to reach it.) | P13-S15 | **The `OperationKind` wire golden lock stops at discriminant 29, so kinds 30–39 — ten of them, every kind appended since the lock was written — have no byte-level lock at all.** `operation_kind_wire_discriminants_are_golden` (`crates/epiphany-ops/src/payload.rs:2189`) declares `let table: [(OperationKind, u8); 30]` (`:2233`), covering 0..=29 and asserting for each that `kind.discriminant()` has not moved *and* that the discriminant byte truly leads the canonical encoding. **Absent from that table: `TransposeInterval` (30, Push 4a), `CreateInstrument` (31, G1), `SetCanvasLayoutDefaults` (32) and `SetSpellingPrecedence` (33, G2a), `SetTuningContext` (34, G2b), `CreateStaffGroup` (35), `CreatePartDefinition` (36), `CreateAnalysisLayer` (37) and `CreateView` (38, G3a), and `CreateMeasure` (39, G3b).** Their wire discriminants are unlocked: a hand edit to `OperationKind::discriminant()`'s match — itself the site Push 4a got wrong — would move any of the ten silently, and the encoding-leads-with-the-byte assertion never runs for them. **The shape is the failure this project keeps rediscovering:** a hand-maintained parallel table that quietly stopped being extended, exactly like the four literal sites found at Push 4a and the six found during G2a — and the golden lock is the one guard specifically meant to catch that class, so its own staleness is the worst place for it. The gap widened from four kinds to ten while the entry sat open, which is itself the argument for closing it now that the genesis ladder has stopped appending | this file (found 2026-07-28 by the G-minor implementation while building s1's coverage; **scope corrected 2026-07-30**, after the genesis ladder closed at G3b — the original text scoped the repair to kinds 30–33 and an array length of `; 34`, both of which were accurate when written and are now six kinds short. Re-verified against the working tree at `4f141ce`: the length literal is still `30`, and no arm for 30–39 appears in the table) | **RESOLVED 2026-07-30** (its own rung, no rider). **Never a live incorrectness:** every one of the ten discriminants was correct throughout, and `binary_format.tex:1443`ff (kind table rows 30–39) and `:1548`–`:1552` (tag table rows 30–39) carry them normatively — the gap is the *absence of a guard*, not a wrong byte. **The repair, as landed:** `operation_kind_wire_discriminants_are_golden`'s table goes from 30 to **40** entries, locking kinds 30–39 individually — each row asserting both that `kind.discriminant()` has not moved and that the discriminant byte leads the canonical encoding. **No wire, schema-version, or specification change**: this adds a guard over assignments that were already normative. **Mutation evidence:** `OperationKind::discriminant()`'s `SetTuningContext` arm was edited 34 → 44 and the extended lock failed (*"wire discriminant for SetTuningContext moved — canonical encodings are append-only"*); with the same mutation still applied, restricting the loop to `&table[..30]` — the exact pre-repair coverage — made it **pass**, which is P13-S15 itself reproduced in the tree rather than argued for. Both edits restored by hand. **On the sibling:** the tag half is total by construction and needs no extension. `the_tag_vocabulary_is_complete` (`payload.rs:2652`) is derived, not hand-written — it computes `first_unknown_discriminant()` from `PAYLOAD_FREE`'s maximum and asserts the payload-free discriminants are exactly `0..unknown` minus `Registered`'s, dense and each decoding — so it already covers 30–39, and `operation_kind_tag_vocabulary!` makes a tag without a discriminant a compile error rather than a silent omission. **One residue, scoped out and stated rather than papered over:** density plus round-trip does not pin *which* tag holds which byte, so a permutation inside the dense range (swapping two assigned discriminants) survives both that test and `phase3_tag_discriminants_are_golden` (`payload.rs:2728`), which pins literals for 24–29 only. The same permutation on the *kind* side is caught by this rung's extended table. The tag-side gap is **not** part of this rung and is **filed as P13-S22** rather than left as a closing remark — a residue recorded only inside a resolved row is a residue that gets lost | | P13-S16 | **`StaffGroup.members` and `Staff.group` may disagree in both directions, and nothing detects it.** The two fields encode the same relation twice. `Staff.group` (`core_spec.tex:5578`, `graph.rs:819`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4231`, `graph.rs:1614`) lists the staves in a group. **The specification declares both and states neither an authority nor an agreement requirement.** Graph invariant 10 checks that each side *resolves* — a staff's group is declared (`invariants.rs:1126`), a group's members are declared (`:1135`) — and never that the two agree, so **both stale forms pass every check in the tree**: a *missing* member (`s.group == Some(g)` while `g.members` omits `s`) and a *spurious* member (`g.members` contains `s` while `s.group` is `None` or names a different group). Genesis G3a ruled `Staff.group` the sole authority and `StaffGroup.members` a non-authoritative denormalized projection (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, ratified 2026-07-29) — a normative semantic ruling that makes the disagreement *defined* rather than merely undetected, but does not make it *impossible*: G3a stores the projection without maintaining it | `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1 (found 2026-07-29 during G3a contract review; the authorship cycle is what surfaced it — with mints only, no authoring order produces an agreeing pair, since `CreateStaff` requires its group live at `reduce.rs:4117` and `CreateStaffGroup` requires its members live) | **open.** Deliberately no code change in G3a. The fix is disposition **A**: maintain the projection under reduction — `create_staff` with `group: Some(g)` appends to `g.members` — plus a candidate **graph invariant 21** enforcing agreement in both directions, and a decision on whether a re-carried `CreateStaffGroup` compares against its *carried* `members` (empty) or the current derived state. **Consumers must read `Staff.group`, never `StaffGroup.members`, for membership** until that lands. Sequence it after G3b so an invariant append is not competing with G3b's invariant 20 | | P13-S17 | **Binary Format revision history omitted genesis tranche G2b entirely, including the accept-set raise it performed.** `spec/binary_format.tex`'s Revision History chapter ran G2a 0.12.0 straight to G-minor 0.13.0 to G3a 0.14.0, with no row anywhere recording G2b (`spec/CONTRACT_GENESIS_G2B_TUNING.md`, kind/tag 34, `SetTuningContext`) — even though `OperationEnvelopeBlock`'s accept-set raise 2→3, the first accept-set move since genesis tranche G2a explicitly recorded staying at 2, reached the normative tables (the per-chunk-role accept-set prose at `binary_format.tex:2353`–`:2363`, which names the `OperationEnvelopeBlock` role's maximum as 3 "as of genesis tranche G2b", and the `OperationKind` minor-additive bullet at `:2395`–`:2418`, which records "genesis tranche G2b took 34 (`SetTuningContext`)") and never the history. G2b's own contract touch table row 27 required "version, Revision History row" among the four-document ritual, and the rung was signed off without it — the gate did not catch a documentation MUST because nothing tests the revision history | `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` §0 (found 2026-07-29 during the G3a undo-repair contract review, verified against the working tree: `binary_format.tex:3599`, `:3628`, `:3643` before this rung's edit) | **RESOLVED in this same commit.** The chronology is restored: G2b lands as its own 0.14.0 row between G-minor and G3a, and G3a renumbers to 0.15.0 (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet B, pins B2–B3). A new scoped guard in `epiphany-testkit` makes the omission recurrence-detectable — a distinct principal marker per standalone-row rung (G2a, G-minor, G2b, G3a — G1 is deliberately unguarded, having no standalone row of its own), strictly ordered, with G2b's content anchored within its own row segment — so the entry is filed and closed by the same packet that finds it, unlike **P13-S15** and **P13-S16**, which stay open because their fixes are sequenced to later rungs | -| P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, and nothing yet closes the residue.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 7) makes invariant 20 ABSTAIN — emit no violation — wherever pin 6's comparable relation cannot order two measure starts or pin 6b's musical delta cannot be computed between them: cross-clock offsets (`Musical` vs `WallClock`), differing boundary selectors (`pos`/`edge`), and any `Measure` *end* anchor (unresolvable without the deferred tempo/measure-length machinery, `invariants.rs:400`ff). This is deliberate — base-ingested data may predate the rule, so flagging every incomputable case would make the invariant useless on real scores — but it is a real gap: a score whose measure/meter disagreement happens to fall in one of these incomputable shapes passes invariant 20 silently | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 7 (filed 2026-07-30 during the G3b contract's own drafting, ratified as deliberate abstention rather than a defect) | **open, deliberately.** Closing it needs the deferred P11-C5 resolved-position machinery: once a `Measure` end, or an event position on a wall-clock-placed region, can be placed on a common timeline, the comparable relation and the musical delta both widen and the abstention residue shrinks. No code change is owed by G3b itself | +| P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, but only three of the checker's nine non-success paths are the real gap — not the whole checker, as first filed and over-sized.** `check_measure_meter_consistency` (`invariants.rs:2662`) has nine non-success paths across its two clauses, enumerated and classified by both its own doc comment and `spec/CONTRACT_P13S18_MATRIX.md`'s 18-cell outcome matrix (agreement: A1-A4; boundary: B1-B5). A1 (`None` declared signature) is **inapplicable** — nothing to disagree with. A3/B3 (`Governing20::None`, an empty governing candidate set) are **vacuous** (pin 6c case 1). A2/B2 (an unresolving declared or governing signature) are **delegated** to invariant 10's own resolution check (`invariants.rs:1220`ff, its per-measure and instance-local-grid arms) — verified, not merely asserted: the matrix rung's mutations M7/M8 delete each arm in turn and show the SAME condition go unreported by the ENTIRE workspace suite, not merely by invariant 20. B1 (the first measure) is the already-filed pickup/anacrusis deferral, **P13-S19**. **Exactly three paths are genuine abstention: A4 and B4 (`Governing20::Indeterminate` — the comparable relation cannot place a candidate) and B5 (a decided governing selection with no computable musical delta — order without distance).** Also corrected: the earlier **"any `Measure` *end* anchor is incomparable"** claim was wrong only in its "any" — same-id, same-position `End`<->`End` IS comparable under c2 **when its offsets compare** (`measure20_offset_order`, `:2419`, returns `None` only for `Musical` against `WallClock`); distinct-id `End` anchors genuinely are incomparable (c3 restricts to `Start`+`Zero`) and do reach A4/B4/B5; and the `resolve_anchor` `Measure` arm citation (now `:503`-`:516`, formerly miscited as `:400`ff — see the companion line-number repair to `CONTRACT_GENESIS_G3B_MEASURE.md:206`) names the missing duration machinery, not invariant 20's own execution path, which never calls `resolve_anchor`. And the `WallClock`-anchored measure start `epiphany-ops::valuegen::measure` (`ops/src/valuegen.rs:447`) actually emits does **not** uniformly abstain both clauses: against `WallClock`-anchored meter changes (c5) agreement DECIDES and only the boundary clause abstains (B5, since `measure20_musical_delta` never returns a `WallClock` delta); against `Region`-anchored meter changes both abstain (A4/B4), because `WallClock` against `Region` has no comparability arm at all | `spec/CONTRACT_P13S18_MATRIX.md` pin 8 (ratified 2026-07-31, a diagnostic and bookkeeping rung: test coverage over `check_measure_meter_consistency`'s existing nine paths plus these three ledger repairs, no behaviour change) | **open, at its true size.** A4, B4 and B5 remain real, still gated on the deferred common-timeline machinery — but the capability that closes them is now filed as **P13-S23** (below), not P11-C5: P11-C5 is a narrower re-anchoring proximity metric this entry previously over-cited as the gate; P13-S23 is the broader "place any anchor pair on a common timeline and measure musical distance" capability that actually owns A4, B4 and B5 | | P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes | | P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 16–18), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions | | P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 16–18 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it | | P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 24–29 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 35–38 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 2–15, 17–23, and 30–33 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548`–`:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental** — `ops/src/vectors.rs:201`–`:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the six scattered fragments rather than adding a seventh — a seventh band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** | +| P13-S23 | **No filed candidate owns "place any anchor pair on a common timeline and measure musical distance along it" — P13-S18 previously mis-cited a narrower capability as its gate.** Two disjoint deficiencies, both owned by this candidate. (1) **No ordering.** The pair is not comparable under any of `measure20_comparable_order`'s five shapes c1-c5 (`invariants.rs:2457`) at all — whether the failure is in the **referent** (distinct `Event` ids; distinct `Measure` ids outside c3's `Start`+`Zero` restriction), the **variant or selector** (`Event` against `Measure`, `Measure` against `Region`, differing `pos`/`edge`), or the **clock** (`Musical` against `WallClock`, including inside `measure20_offset_order`, `:2419`) — this is what invariant 20's A4 and B4 are made of. (2) **Ordering without a usable delta.** The pair IS comparable and still yields no musical distance: c3 supplies a vector index (an order, never a distance), and c5 compares two `WallClock`s, and `measure20_musical_delta` (`:2522`) never returns a `WallClock` delta (`:2527`) — this is what invariant 20's B5 is made of. Scoping this as merely "anchors of differing shapes" or "not directly comparable under c1-c5" would exclude B5 entirely — S5 (distinct-id `Measure` `Start`/`Zero`) is c3-comparable and S1 (`WallClock` measures, `WallClock` meter changes) is c5-comparable, and both still reach B5 — an earlier draft of this filing made exactly that narrower mistake. **Explicitly broader than P11-C5**: P11-C5 (`PASS11_WORKLIST.md:159`) is a re-anchoring proximity metric that resolves "when the graph-mutation phase tracks resolved positions", and covers narrowly the two-distinct-`Event`s case (`CONTRACT_GENESIS_G3B_MEASURE.md:223`, `effect.rs:139`-`:142`'s `PositionOutsideRegion` Reserved note); P13-S23 is the timeline itself, whatever positions get placed on it. Names its dependents: invariant 20's A4, B4 and B5, and `PositionOutsideRegion`'s Reserved status | `spec/CONTRACT_P13S18_MATRIX.md` pin 10 (filed 2026-07-31 during the same rung that corrected P13-S18's over-narrow P11-C5 citation) | **open.** No code owed by this rung. Closing it needs the deferred common-timeline/duration machinery — once a `Measure` end, a distinct-id `Measure`/`Event` referent, or an `Event` position on a wall-clock-placed region can be placed on a common timeline with a musical distance, invariant 20's A4/B4/B5 residue and `PositionOutsideRegion`'s Reserved status shrink together |