diff --git a/crates/epiphany-core/DECISIONS.md b/crates/epiphany-core/DECISIONS.md index 7706d1d..cfae1a5 100644 --- a/crates/epiphany-core/DECISIONS.md +++ b/crates/epiphany-core/DECISIONS.md @@ -1062,6 +1062,16 @@ underdetermined pitch spaces) — inventing one would itself be the wired into `check_invariants` as `GraphIndex::check_accidental_modification_compatibility` — the `req:tuning:accidental-modification-compatibility` invariant + +> **SUPERSEDED 2026-08-12 by P13-S29** (`spec/CONTRACT_P13S29_VIOLATION_KIND.md`). +> Calling this an *invariant* was accurate about the tag it borrowed and wrong +> about what it is: a Chapter 4 requirement reported under a Chapter 5 graph +> invariant's number, through a public API. It now reports +> `ViolationKind::Requirement("req:tuning:accidental-modification-compatibility")` +> and is retrievable through `check_requirement`. **The decision above is left +> as written** — it records why borrowing the tag was defensible when no other +> arm existed, which is what a later reader needs in order to understand why it +> was accepted and then reversed. (`core_spec.tex:3120`). `space` resolves structurally against `built_in_position_structure` (Push 4b tranche 1), the same catalog `Pitch::transposed` uses. The requirement's two named rules (`CmnChromatic` diff --git a/crates/epiphany-core/README.md b/crates/epiphany-core/README.md index 98fcea9..916b0ec 100644 --- a/crates/epiphany-core/README.md +++ b/crates/epiphany-core/README.md @@ -22,7 +22,7 @@ of the core specification (`spec/core_spec.pdf`). This is Agent B's crate per | Events | the `Event` taxonomy (7 variants) and the `slotmap`-backed `EventArena` | Ch. 5 §"The Event Arena" | | Graph | `Canvas`, `Region`, `Staff` vs `StaffInstance`, `Voice`/`VoiceOrigin`, `Measure`, `BarlineAlignmentGroup`, aleatoric `EventOrderingDAG` (acyclic by construction), the full cross-cutting registry, the full top-level `Score` | Ch. 5 | | Indexes | `ScoreIndexes`: the four mandatory indexes (event-time, cross-cutting-reference, measure, spelling-attachment) | Ch. 5 §"Indexes" | -| Invariants | `check_invariants` over all 19 enumerated graph invariants, with a typed `InvariantViolation` witness per check | Ch. 5 §"Graph Invariants" | +| Invariants | `check_invariants` over all variants returned by `GraphInvariant::all()`, with a typed `WellFormednessViolation` witness per check | Ch. 5 §"Graph Invariants" | | Generators | `generators::valid_score`/`valid_score_rich` (positive), `violating_score` (negative, per invariant), `shrink` (witness minimizer) | QUICKSTART, Agent B hand-off | ## The identity discipline this crate enforces diff --git a/crates/epiphany-core/src/generators.rs b/crates/epiphany-core/src/generators.rs index b8b0f22..563a521 100644 --- a/crates/epiphany-core/src/generators.rs +++ b/crates/epiphany-core/src/generators.rs @@ -976,6 +976,7 @@ pub fn shrink(score: &Score, inv: GraphInvariant) -> Score { mod tests { use super::*; use crate::check_invariants; + use crate::invariants::ViolationKind; #[test] fn positive_corpus_runs_clean() { @@ -1092,7 +1093,8 @@ mod tests { else, got {violations:?}" ); assert_eq!( - violations[0].invariant, inv, + violations[0].kind, + ViolationKind::Invariant(inv), "{leg}: the single violation must be invariant 21, got {violations:?}" ); assert!( @@ -1171,8 +1173,11 @@ mod tests { for inv in GraphInvariant::all() { let s = violating_score(inv, 99); let all = check_invariants(&s); - let kinds: std::collections::BTreeSet<_> = all.iter().map(|v| v.invariant).collect(); - assert!(kinds.contains(&inv), "{inv:?} not among {kinds:?}"); + let kinds: std::collections::BTreeSet<_> = all.iter().map(|v| v.kind).collect(); + assert!( + kinds.contains(&ViolationKind::Invariant(inv)), + "{inv:?} not among {kinds:?}" + ); assert!( kinds.len() <= 3, "{inv:?} corruption fired too many invariants: {kinds:?}" diff --git a/crates/epiphany-core/src/invariants.rs b/crates/epiphany-core/src/invariants.rs index 9d739ad..d0c99a3 100644 --- a/crates/epiphany-core/src/invariants.rs +++ b/crates/epiphany-core/src/invariants.rs @@ -1,11 +1,16 @@ //! The Chapter 5 graph invariants (Chapter 5 §"Graph Invariants"). //! +//! Violations carry a two-armed [`ViolationKind`]: `Invariant` for the Chapter 5 +//! graph invariants, `Requirement` for a normative requirement named by its +//! label. A requirement failure is not an invariant failure, and neither arm is +//! a fallback for the other. +//! //! The spec enumerates a set of structural invariants every well-formed score //! graph must satisfy. They are *property tests in CI, not runtime assertions //! in release builds* (QUICKSTART, Agent B): this module is the checker the //! property tests and generators (see [`crate::generators`]) drive. Each //! enumerated invariant has exactly one check returning a typed -//! [`InvariantViolation`] witness identifying the smallest offending objects. +//! [`WellFormednessViolation`] witness identifying the smallest offending objects. //! //! **Count.** [`GraphInvariant::all`] is the single origin: its length *is* the //! count, and no prose here restates it — a restated count goes stale silently @@ -116,17 +121,19 @@ pub enum GraphInvariant { /// - TempoSegment.start — anchor target. /// - TempoSegment.end — anchor target. /// - /// Beyond that surface, further checks are reported under this same tag - /// and are NOT part of the normative invariant 10: tempo-map segment - /// shape, ordering and non-overlap (Chapter 3, - /// `req:time:tempo-segment-order`); aleatoric ordering and bounds - /// region locality (Chapter 3, + /// Beyond that surface, the checker reaches four rules that are NOT + /// part of the normative invariant 10 and **no longer report under this + /// tag**. Since P13-S29 each carries its own `req:` label in the + /// `Requirement` arm of [`ViolationKind`]: tempo segment shape + /// (Chapter 3, `req:time:tempo-segment-shape`); tempo segment ordering + /// and non-overlap (Chapter 3, `req:time:tempo-segment-order`); + /// aleatoric ordering and bounds region locality (Chapter 3, /// `req:time:aleatoric-reference-locality`); and accidental /// modification expressibility (Chapter 4, - /// `req:tuning:accidental-modification-compatibility`). That - /// multiplexing is filed as P13-S29 — the public `check_invariant` - /// filter and this violation's `Display` attribute those failures to - /// invariant 10. Repairing it is a behaviour change, out of scope here. + /// `req:tuning:accidental-modification-compatibility`). Neither + /// `check_invariant` nor this violation's `Display` attributes them to + /// invariant 10 any more. [`check_invariants`] still returns them, so a + /// caller asking "is this graph well-formed" keeps its coverage. CrossCuttingRefsResolve, /// 11. Identifiers are unique within their kind (every id kind), with /// reserved-namespace (`SYSTEM_DERIVED`) misuse, tombstone/live @@ -243,49 +250,65 @@ impl GraphInvariant { } } -/// A violation of a graph invariant: which invariant, and a short witness -/// naming the smallest offending objects (Chapter 5; QUICKSTART: "minimizes -/// invariant violations to a small witness for debugging"). +/// What a [`WellFormednessViolation`] failed. `Invariant` names a numbered +/// Chapter 5 graph invariant; `Requirement` names a normative requirement by its +/// label. A requirement failure is not an invariant failure, and there is no +/// third arm and no unclassified fallback. +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +pub enum ViolationKind { + Invariant(GraphInvariant), + Requirement(&'static str), +} + +/// A well-formedness failure: one [`ViolationKind`] — `Invariant` or +/// `Requirement` — and the witness identifying the smallest offending objects. +/// A requirement failure is not an invariant failure. #[derive(Clone, PartialEq, Eq, Debug)] -pub struct InvariantViolation { - pub invariant: GraphInvariant, +pub struct WellFormednessViolation { + pub kind: ViolationKind, pub witness: String, } -impl InvariantViolation { - fn new(invariant: GraphInvariant, witness: impl Into) -> Self { - InvariantViolation { - invariant, +impl WellFormednessViolation { + fn invariant(which: GraphInvariant, witness: impl Into) -> Self { + WellFormednessViolation { + kind: ViolationKind::Invariant(which), + witness: witness.into(), + } + } + + fn requirement(label: &'static str, witness: impl Into) -> Self { + WellFormednessViolation { + kind: ViolationKind::Requirement(label), witness: witness.into(), } } } -impl core::fmt::Display for InvariantViolation { +impl core::fmt::Display for WellFormednessViolation { fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result { - write!( - f, - "invariant {} ({:?}) violated: {}", - self.invariant.number(), - self.invariant, - self.witness - ) + match self.kind { + ViolationKind::Invariant(which) => write!( + f, + "invariant {} ({:?}) violated: {}", + which.number(), + which, + self.witness + ), + ViolationKind::Requirement(label) => { + write!(f, "requirement {label} violated: {}", self.witness) + } + } } } -/// A Chapter 5 well-formedness check this crate could not *decide* for a given -/// score — e.g., a region-overlap test whose extents use symbolic -/// [`crate::TimeAnchor`]s that need the full tempo/measure machinery (out of this -/// crate's scope) to place on a common timeline. -/// -/// [`check_invariants`] stays *sound* — it never raises a false positive on an -/// undecidable check — but a sound-and-silent checker would treat "couldn't -/// decide" identically to "clean". [`deferred_checks`] makes the undecided cases -/// explicit and testable instead, so a stricter conformance profile can choose -/// to reject them rather than have them pass unseen. +/// A check the graph could not decide, reported instead of silently passed. #[derive(Clone, PartialEq, Eq, Debug)] pub struct DeferredCheck { /// The invariant whose decision was deferred. + /// + /// **Not affected by P13-S29's two-arm split**: every deferred check today is + /// a genuine graph invariant, correctly attributed. pub invariant: GraphInvariant, /// A human-readable witness explaining why it could not be decided. pub reason: String, @@ -320,11 +343,18 @@ pub fn deferred_checks(score: &Score) -> Vec { /// Checks every Chapter 5 graph invariant over `score`, returning all /// violations found (empty iff the graph is well-formed). /// +/// **Comprehensive across both arms of [`ViolationKind`].** It returns graph +/// invariant failures *and* the Chapter 3/4 requirement failures the checker +/// reaches, so a caller that wants "is this score well-formed" keeps exactly the +/// coverage it had before P13-S29 split the tag. The two selectors, +/// [`check_invariant`] and [`check_requirement`], are projections of this +/// result; neither is a substitute for it. +/// /// This is *sound but incomplete* for the few invariants that need absolute-time /// resolution: it never raises a false positive, and the cases it could not /// decide are reported separately by [`deferred_checks`] rather than silently /// passed. -pub fn check_invariants(score: &Score) -> Vec { +pub fn check_invariants(score: &Score) -> Vec { let idx = GraphIndex::build(score); let mut v = Vec::new(); idx.check_event_voice_backlink(&mut v); @@ -386,10 +416,26 @@ pub fn measure_anchor_relation( } /// Checks a single invariant (useful for targeted negative property tests). -pub fn check_invariant(score: &Score, which: GraphInvariant) -> Vec { +/// Every violation of one graph invariant. +/// +/// **Projection of [`check_invariants`], filtered to the `Invariant` arm.** A +/// Chapter 3 or Chapter 4 requirement failure is *not* returned here, however +/// the checker happens to reach it — use [`check_requirement`] for those. +pub fn check_invariant(score: &Score, which: GraphInvariant) -> Vec { check_invariants(score) .into_iter() - .filter(|v| v.invariant == which) + .filter(|v| v.kind == ViolationKind::Invariant(which)) + .collect() +} + +/// Every violation of one normative requirement, by its label. +/// +/// **Projection of [`check_invariants`], filtered to the `Requirement` arm** — +/// the symmetric counterpart of [`check_invariant`]. +pub fn check_requirement(score: &Score, label: &str) -> Vec { + check_invariants(score) + .into_iter() + .filter(|v| matches!(v.kind, ViolationKind::Requirement(l) if l == label)) .collect() } @@ -619,11 +665,11 @@ impl<'a> GraphIndex<'a> { } // --- 1. Event -> voice backlink. ---------------------------------------- - fn check_event_voice_backlink(&self, out: &mut Vec) { + fn check_event_voice_backlink(&self, out: &mut Vec) { for e in self.score.events.iter() { let vid = e.voice(); match self.voice.get(&vid) { - None => out.push(InvariantViolation::new( + None => out.push(WellFormednessViolation::invariant( GraphInvariant::EventVoiceBacklink, format!( "event {:?} names voice {:?}, which is not in the graph", @@ -631,32 +677,34 @@ impl<'a> GraphIndex<'a> { vid ), )), - Some(v) if !v.events.contains(&e.id()) => out.push(InvariantViolation::new( - GraphInvariant::EventVoiceBacklink, - format!( - "event {:?} names voice {:?}, which does not list it", - e.id(), - vid - ), - )), + Some(v) if !v.events.contains(&e.id()) => { + out.push(WellFormednessViolation::invariant( + GraphInvariant::EventVoiceBacklink, + format!( + "event {:?} names voice {:?}, which does not list it", + e.id(), + vid + ), + )) + } _ => {} } } } // --- 2. Voice -> event backlink. ---------------------------------------- - fn check_voice_event_backlink(&self, out: &mut Vec) { + fn check_voice_event_backlink(&self, out: &mut Vec) { for (_r, _si, v) in self.score.voices() { for e in &v.events { match self.score.events.get(*e) { - None => out.push(InvariantViolation::new( + None => out.push(WellFormednessViolation::invariant( GraphInvariant::VoiceEventBacklink, format!( "voice {:?} lists event {:?}, absent from the arena", v.id, e ), )), - Some(ev) if ev.voice() != v.id => out.push(InvariantViolation::new( + Some(ev) if ev.voice() != v.id => out.push(WellFormednessViolation::invariant( GraphInvariant::VoiceEventBacklink, format!( "voice {:?} lists event {:?} whose voice is {:?}", @@ -672,7 +720,7 @@ impl<'a> GraphIndex<'a> { } // --- 3. Events sorted and non-overlapping within a voice. --------------- - fn check_voice_events_sorted_non_overlap(&self, out: &mut Vec) { + fn check_voice_events_sorted_non_overlap(&self, out: &mut Vec) { for (_r, _si, v) in self.score.voices() { let mut prev: Option<(EventId, Endpoints)> = None; for e in &v.events { @@ -685,7 +733,7 @@ impl<'a> GraphIndex<'a> { if !p_end.le_same_clock(&c_start) { // Either out of order (start < prev start) or // overlapping (prev end > cur start). - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::VoiceEventsSortedNonOverlap, format!( "in voice {:?}, event {:?} starts before event {:?} ends", @@ -701,7 +749,7 @@ impl<'a> GraphIndex<'a> { } // --- 4. Coordinate variants agree with the region's time model. --------- - fn check_event_coordinate_model(&self, out: &mut Vec) { + fn check_event_coordinate_model(&self, out: &mut Vec) { for e in self.score.events.iter() { let Some((region, _)) = self.voice_parent.get(&e.voice()) else { continue; // unparented voice: invariant 1/5 reports it @@ -710,7 +758,7 @@ impl<'a> GraphIndex<'a> { continue; }; if !coordinate_ok(e, *disc) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::EventCoordinateModel, format!( "event {:?} coordinates {:?}/{:?} contradict region {:?} discipline {:?}", @@ -726,13 +774,13 @@ impl<'a> GraphIndex<'a> { } // --- 5. Containment is a tree. ------------------------------------------ - fn check_containment_tree(&self, out: &mut Vec) { + fn check_containment_tree(&self, out: &mut Vec) { // Voice id appearing under more than one instance. let mut voice_seen: HashMap = HashMap::new(); for (_r, si, v) in self.score.voices() { if let Some(prev) = voice_seen.insert(v.id, si) { if prev != si { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::ContainmentTree, format!( "voice {:?} appears in instances {:?} and {:?}", @@ -748,7 +796,7 @@ impl<'a> GraphIndex<'a> { for si in r.staff_instances() { if let Some(prev) = inst_seen.insert(si.id, r.id) { if prev != r.id { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::ContainmentTree, format!( "staff instance {:?} appears in regions {:?} and {:?}", @@ -762,12 +810,12 @@ impl<'a> GraphIndex<'a> { } // --- 6. Instance.staff resolves; no StaffId twice in one region. -------- - fn check_staff_instance_resolves(&self, out: &mut Vec) { + fn check_staff_instance_resolves(&self, out: &mut Vec) { for r in &self.score.canvas.regions { let mut staff_in_region: HashSet = HashSet::new(); for si in r.staff_instances() { if !self.declared_staves.contains(&si.staff) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::StaffInstanceResolves, format!( "staff instance {:?} references undeclared staff {:?}", @@ -776,7 +824,7 @@ impl<'a> GraphIndex<'a> { )); } if !staff_in_region.insert(si.staff) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::StaffInstanceResolves, format!( "staff {:?} is manifested by two instances in region {:?}", @@ -789,7 +837,7 @@ impl<'a> GraphIndex<'a> { } // --- 7. Region extents: staff_extent matches; no double overlap. -------- - fn check_region_extents(&self, out: &mut Vec) { + fn check_region_extents(&self, out: &mut Vec) { for r in &self.score.canvas.regions { // staff_extent must list exactly the manifested staves, no dups. let manifested: BTreeSet = @@ -797,14 +845,14 @@ impl<'a> GraphIndex<'a> { let mut listed = BTreeSet::new(); for s in &r.staff_extent.staves { if !listed.insert(*s) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::RegionExtents, format!("region {:?} staff_extent lists staff {:?} twice", r.id, s), )); } } if listed != manifested { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::RegionExtents, format!( "region {:?} staff_extent {:?} != manifested staves {:?}", @@ -828,7 +876,7 @@ impl<'a> GraphIndex<'a> { continue; } if self.regions_overlap_in_time(a, b) == Some(true) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::RegionExtents, format!( "regions {:?} and {:?} overlap in both time and staff extent", @@ -881,11 +929,11 @@ impl<'a> GraphIndex<'a> { } // --- 8. Each measure belongs to exactly one instance. ------------------- - fn check_measure_single_instance(&self, out: &mut Vec) { + fn check_measure_single_instance(&self, out: &mut Vec) { for (mid, owners) in &self.measure_instances { let distinct: BTreeSet<_> = owners.iter().copied().collect(); if distinct.len() > 1 { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::MeasureSingleInstance, format!("measure {:?} belongs to instances {:?}", mid, distinct), )); @@ -894,10 +942,10 @@ impl<'a> GraphIndex<'a> { } // --- 9. Anchor offset variant agrees with target's time model. ---------- - fn check_anchor_offset_model(&self, out: &mut Vec) { + fn check_anchor_offset_model(&self, out: &mut Vec) { for a in self.collect_anchors() { if let Some(false) = self.offset_ok(a) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::AnchorOffsetModel, format!( "anchor {:?} offset contradicts its target region's time model", @@ -1035,11 +1083,11 @@ impl<'a> GraphIndex<'a> { } // --- 10. Cross-cutting references resolve. ------------------------------ - fn check_cross_cutting_refs(&self, out: &mut Vec) { + fn check_cross_cutting_refs(&self, out: &mut Vec) { let live_event = |e: &EventId| self.score.events.contains(*e); let mut flag = |cond: bool, what: String| { if !cond { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::CrossCuttingRefsResolve, what, )); @@ -1420,17 +1468,21 @@ impl<'a> GraphIndex<'a> { // // The spec enumerates no dedicated tempo graph invariant, but the tempo // map's segment anchors are graph references and its segments carry - // structural requirements; both are surfaced here under invariant 10 - // (reference resolution + graph integrity). Segment-anchor *offset* + // structural requirements. **Since P13-S29 these report under two different + // arms**: the anchors stay invariant 10, while shape/`end_tempo` + // compatibility reports `req:time:tempo-segment-shape` and ordering and + // non-overlap report `req:time:tempo-segment-order`. Segment-anchor *offset* // agreement is invariant 9's (the anchors are in `collect_anchors`). - fn check_tempo_maps(&self, out: &mut Vec) { + fn check_tempo_maps(&self, out: &mut Vec) { use crate::tempo::TempoShape; - let mut flag = |cond: bool, what: String| { + // P13-S29: anchor existence is invariant 10; shape, order and overlap + // are Chapter 3 requirements and say so. + let mut flag = |kind: ViolationKind, cond: bool, what: String| { if !cond { - out.push(InvariantViolation::new( - GraphInvariant::CrossCuttingRefsResolve, - what, - )); + out.push(WellFormednessViolation { + kind, + witness: what, + }); } }; // Self-contained musical position of a segment boundary: a region-start @@ -1458,11 +1510,13 @@ impl<'a> GraphIndex<'a> { for seg in &tm.segments { // Segment boundary anchor targets must resolve (invariant 10). flag( + ViolationKind::Invariant(GraphInvariant::CrossCuttingRefsResolve), self.anchor_target_exists(&seg.start), format!("tempo segment start anchor target {:?} dangling", seg.start), ); if let Some(end) = &seg.end { flag( + ViolationKind::Invariant(GraphInvariant::CrossCuttingRefsResolve), self.anchor_target_exists(end), format!("tempo segment end anchor target {end:?} dangling"), ); @@ -1470,12 +1524,14 @@ impl<'a> GraphIndex<'a> { // Missing end_tempo / shape consistency (Chapter 3). match seg.shape { TempoShape::Constant => flag( + ViolationKind::Requirement("req:time:tempo-segment-shape"), seg.end_tempo .as_ref() .is_none_or(|et| et == &seg.start_tempo), "constant tempo segment has end_tempo != start_tempo".to_string(), ), TempoShape::Linear | TempoShape::Exponential | TempoShape::Curve => flag( + ViolationKind::Requirement("req:time:tempo-segment-shape"), seg.end_tempo.is_some(), "non-constant tempo segment is missing its end_tempo".to_string(), ), @@ -1483,10 +1539,15 @@ impl<'a> GraphIndex<'a> { // Ordering and non-overlap, where resolvable. let start = seg_pos(&seg.start); if let (Some(ps), Some(s)) = (&prev_start, &start) { - flag(s >= ps, "tempo segments are out of start order".to_string()); + flag( + ViolationKind::Requirement("req:time:tempo-segment-order"), + s >= ps, + "tempo segments are out of start order".to_string(), + ); } if let (Some(pe), Some(s)) = (&prev_end, &start) { flag( + ViolationKind::Requirement("req:time:tempo-segment-order"), s >= pe, "tempo segments overlap in musical time".to_string(), ); @@ -1500,10 +1561,11 @@ impl<'a> GraphIndex<'a> { // --- Aleatoric ordering / bounds well-formedness (Chapter 3 §"Aleatoric // Time"). The ordering DAG and the per-event bounds map are graph // references: they must name events that exist *in the region*, and each - // bound window must be ordered (`min <= max`). Dangling references go under - // invariant 10; a reversed window is a region-time-model defect (invariant - // 4). (The DAG's acyclicity is enforced at construction in `graph`.) - fn check_aleatoric_models(&self, out: &mut Vec) { + // bound window must be ordered (`min <= max`). **Since P13-S29 the locality + // rule reports `req:time:aleatoric-reference-locality`**, not invariant 10 — + // it asks about region membership, which is stronger than existence. A + // reversed window remains a region-time-model defect (invariant 4). (The DAG's acyclicity is enforced at construction in `graph`.) + fn check_aleatoric_models(&self, out: &mut Vec) { for r in &self.score.canvas.regions { let RegionTimeModel::Aleatoric(model) = &r.time_model else { continue; @@ -1517,8 +1579,8 @@ impl<'a> GraphIndex<'a> { }; for e in model.ordering.referenced_events() { if !in_region(e) { - out.push(InvariantViolation::new( - GraphInvariant::CrossCuttingRefsResolve, + out.push(WellFormednessViolation::requirement( + "req:time:aleatoric-reference-locality", format!( "aleatoric region {:?} ordering references event {:?}, absent from the region", r.id, e @@ -1528,8 +1590,8 @@ impl<'a> GraphIndex<'a> { } for (e, bounds) in &model.bounds { if !in_region(*e) { - out.push(InvariantViolation::new( - GraphInvariant::CrossCuttingRefsResolve, + out.push(WellFormednessViolation::requirement( + "req:time:aleatoric-reference-locality", format!( "aleatoric region {:?} bounds key event {:?} is absent from the region", r.id, e @@ -1541,7 +1603,7 @@ impl<'a> GraphIndex<'a> { .flatten() { if time_bounds_ordered(tb) == Some(false) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::EventCoordinateModel, format!( "aleatoric region {:?} has a reversed (min > max) bound for event {:?}", @@ -1555,17 +1617,13 @@ impl<'a> GraphIndex<'a> { } // --- Accidental modification / pitch-space compatibility (Chapter 4 - // §"Accidental Registries", `req:tuning:accidental-modification-compatibility`, - // `core_spec.tex:3120`; Push 4b tranche 3a, - // `spec/CONTRACT_PUSH4B_ACCIDENTALS.md`). Not one of the spec-enumerated - // Chapter 5 graph invariants (this is a Chapter 4 - // requirement), so — like the tempo-map and aleatoric-model checks above - // — it is surfaced under an existing `GraphInvariant` tag rather than - // minting a new one. `CrossCuttingRefsResolve` is the closest fit: like - // those checks, this is "does this cross-cutting structure's content - // hold against the rest of the score", not a per-event/per-voice - // structural rule. - fn check_accidental_modification_compatibility(&self, out: &mut Vec) { + // §"Accidental Registries", `req:tuning:accidental-modification-compatibility`; + // Push 4b tranche 3a, `spec/CONTRACT_PUSH4B_ACCIDENTALS.md`). Not one of the + // spec-enumerated Chapter 5 graph invariants, and **since P13-S29 it no + // longer borrows one**: it reports under its own requirement label, which is + // what it always meant. The witness does not restate that label — `Display` + // renders it as the prefix. + fn check_accidental_modification_compatibility(&self, out: &mut Vec) { // Every pitch space the score's tuning context concretely // references: the default, plus any per-scope override's pitch // space (`crate::tuning::TuningOverride::pitch_space`). This @@ -1591,12 +1649,11 @@ impl<'a> GraphIndex<'a> { &def.modification, space, ) { - out.push(InvariantViolation::new( - GraphInvariant::CrossCuttingRefsResolve, + out.push(WellFormednessViolation::requirement( + "req:tuning:accidental-modification-compatibility", format!( "accidental {:?} (registry {:?}) modification {:?} is not \ - expressible in pitch space {:?}'s interval algebra \ - (req:tuning:accidental-modification-compatibility)", + expressible in pitch space {:?}'s interval algebra", def.id, ext.base, def.modification, space ), )); @@ -1607,11 +1664,11 @@ impl<'a> GraphIndex<'a> { } // --- 11. Identifiers unique within their kind. -------------------------- - fn check_unique_identifiers(&self, out: &mut Vec) { + fn check_unique_identifiers(&self, out: &mut Vec) { let mut regions = BTreeSet::new(); for r in &self.score.canvas.regions { if !regions.insert(r.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("region id {:?} is used twice", r.id), )); @@ -1623,14 +1680,14 @@ impl<'a> GraphIndex<'a> { for r in &self.score.canvas.regions { for si in r.staff_instances() { if !instances.insert(si.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("staff-instance id {:?} is used twice", si.id), )); } for v in &si.voices { if !voices.insert(v.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("voice id {:?} is used twice", v.id), )); @@ -1638,7 +1695,7 @@ impl<'a> GraphIndex<'a> { } for m in &si.measures { if !measures.insert(m.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("measure id {:?} is used twice", m.id), )); @@ -1649,7 +1706,7 @@ impl<'a> GraphIndex<'a> { let mut staves = BTreeSet::new(); for s in &self.score.staves { if !staves.insert(s.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("staff id {:?} is used twice", s.id), )); @@ -1660,7 +1717,7 @@ impl<'a> GraphIndex<'a> { let cc = &self.score.cross_cutting; let mut dup = |used: bool, what: String| { if used { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, what, )); @@ -1818,7 +1875,7 @@ impl<'a> GraphIndex<'a> { // Stability" forbids — "never reassigned, even after deletion"). for e in self.score.events.ids_canonical() { if self.score.tombstoned_events.contains(&e) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("event id {:?} is both live and tombstoned", e), )); @@ -1826,7 +1883,7 @@ impl<'a> GraphIndex<'a> { } for p in &self.live_pitches { if self.score.tombstoned_pitches.contains(p) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("pitch id {:?} is both live and tombstoned", p), )); @@ -1840,7 +1897,7 @@ impl<'a> GraphIndex<'a> { // *other* kind in that namespace is misuse. let mut sysmisuse = |used: bool, what: String| { if used { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, what, )); @@ -2021,13 +2078,13 @@ impl<'a> GraphIndex<'a> { // but `get_mut` exposes the fields, so re-check here (catches an id or // pitch-list mutated after insertion). for id in self.score.events.index_inconsistencies() { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("arena index entry {id:?} disagrees with the stored event's id"), )); } for id in self.score.events.malformed_pitched_events() { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::UniqueIdentifiers, format!("pitched event {id:?} has no pitches (malformed; Chapter 5)"), )); @@ -2035,7 +2092,7 @@ impl<'a> GraphIndex<'a> { } // --- 12. Embedded PitchId uniqueness. ----------------------------------- - fn check_pitch_id_unique(&self, out: &mut Vec) { + fn check_pitch_id_unique(&self, out: &mut Vec) { let mut seen: BTreeSet = BTreeSet::new(); let mut buf = Vec::new(); for e in self.score.events.iter() { @@ -2043,7 +2100,7 @@ impl<'a> GraphIndex<'a> { e.collect_identified_pitches(&mut buf); for ip in &buf { if !seen.insert(ip.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::PitchIdUnique, format!("pitch id {:?} appears more than once", ip.id), )); @@ -2053,13 +2110,13 @@ impl<'a> GraphIndex<'a> { } // --- 13. SpellingScope::Pitch resolves to live or tombstoned. ----------- - fn check_spelling_scope_resolves(&self, out: &mut Vec) { + fn check_spelling_scope_resolves(&self, out: &mut Vec) { for a in &self.score.spelling_attachments { if let SpellingScope::Pitch(pid) = &a.scope { let live = self.live_pitches.contains(pid); let tomb = self.score.tombstoned_pitches.contains(pid); if !live && !tomb { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::SpellingScopeResolves, format!( "spelling attachment targets pitch {:?}, neither live nor tombstoned", @@ -2074,7 +2131,7 @@ impl<'a> GraphIndex<'a> { (&a.scope, &a.directive), (SpellingScope::Range { .. }, SpellingDirective::Explicit(_)) ) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::SpellingScopeResolves, "explicit spelling on a range scope (only valid with a pitch scope)" .to_string(), @@ -2086,7 +2143,7 @@ impl<'a> GraphIndex<'a> { // validation rather than leaving it advisory. if let SpellingDirective::Explicit(sp) = &a.directive { if !sp.accidental_stack_is_well_formed() { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::SpellingScopeResolves, format!( "spelling attachment has a repeated accidental in its stack: {:?}", @@ -2099,7 +2156,7 @@ impl<'a> GraphIndex<'a> { // `AnalysisLayer` (Chapter 5 §"Analysis Layers and Views"). if let Some(layer) = a.layer { if !self.analysis_layers.contains(&layer) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::SpellingScopeResolves, format!( "spelling attachment layer {layer:?} is not a declared analysis layer" @@ -2111,12 +2168,12 @@ impl<'a> GraphIndex<'a> { } // --- 14. Decomposition target resolves to live or tombstoned. ----------- - fn check_decomposition_target_resolves(&self, out: &mut Vec) { + fn check_decomposition_target_resolves(&self, out: &mut Vec) { for d in &self.score.decomposition_attachments { let live = self.score.events.contains(d.target); let tomb = self.score.tombstoned_events.contains(&d.target); if !live && !tomb { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::DecompositionTargetResolves, format!( "decomposition targets event {:?}, neither live nor tombstoned", @@ -2128,7 +2185,7 @@ impl<'a> GraphIndex<'a> { } // --- 15. Live decomposition component sum == event duration. ------------ - fn check_decomposition_sum(&self, out: &mut Vec) { + fn check_decomposition_sum(&self, out: &mut Vec) { for d in &self.score.decomposition_attachments { let Some(ev) = self.score.events.get(d.target) else { continue; // tombstoned target: invariant 14 territory @@ -2144,7 +2201,7 @@ impl<'a> GraphIndex<'a> { sum = sum + c.sounding_duration(ratio); } if &sum != dur { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::DecompositionSum, format!( "decomposition of event {:?} sums to {:?}, event duration is {:?}", @@ -2156,7 +2213,7 @@ impl<'a> GraphIndex<'a> { } // --- 16. Tuplet member durations sum to required total. ----------------- - fn check_tuplet_sum(&self, out: &mut Vec) { + fn check_tuplet_sum(&self, out: &mut Vec) { for t in &self.score.cross_cutting.tuplets { // Degenerate ratios (a zero term or actual == notated) are rejected // at construction by `TupletRatio::new` (Chapter 3 §"Tuplets", @@ -2176,7 +2233,7 @@ impl<'a> GraphIndex<'a> { } } if measurable && sum != t.required_total { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TupletSum, format!( "tuplet {:?} members sum to {:?}, required total is {:?}", @@ -2222,7 +2279,7 @@ impl<'a> GraphIndex<'a> { } let sounding = notated.mul(&scale); if &sounding != sd.rational() { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TupletSum, format!( "tuplet {:?} ratio {}:{} is inconsistent with member {:?}'s notation \ @@ -2237,7 +2294,7 @@ impl<'a> GraphIndex<'a> { } // --- 17. Tie pairing references and class rules. ------------------------ - fn check_tie_pairing(&self, out: &mut Vec) { + fn check_tie_pairing(&self, out: &mut Vec) { for t in &self.score.cross_cutting.ties { let empty = BTreeSet::new(); let start_pitches = self.event_pitches.get(&t.start_event).unwrap_or(&empty); @@ -2254,13 +2311,13 @@ impl<'a> GraphIndex<'a> { // require it. for (sp, ep) in pairs { if !start_pitches.contains(sp) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!("tie {:?} pairs pitch {:?} not in start event", t.id, sp), )); } if !end_pitches.contains(ep) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!("tie {:?} pairs pitch {:?} not in end event", t.id, ep), )); @@ -2268,7 +2325,7 @@ impl<'a> GraphIndex<'a> { if requires_enharmonic { if let (Some(a), Some(b)) = (self.pitch.get(sp), self.pitch.get(ep)) { if !a.enharmonic_equivalent(b) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!( "tie {:?} pairs non-enharmonic pitches {:?}/{:?}", @@ -2288,7 +2345,7 @@ impl<'a> GraphIndex<'a> { // — a deterministic matching that survives chord reordering, // not a positional zip. if start_pitches.len() != end_pitches.len() { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!( "tie {:?} (implicit pairing): {} start vs {} end pitches", @@ -2314,7 +2371,7 @@ impl<'a> GraphIndex<'a> { Some(ep) => { used.insert(*ep); } - None => out.push(InvariantViolation::new( + None => out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!( "tie {:?} (implicit pairing): start pitch {:?} has no enharmonic end-event counterpart", @@ -2335,14 +2392,14 @@ impl<'a> GraphIndex<'a> { Endpoints::of(self.score.events.get(eid)?).start_key() } - fn check_tie_class_rules(&self, t: &crate::graph::Tie, out: &mut Vec) { + fn check_tie_class_rules(&self, t: &crate::graph::Tie, out: &mut Vec) { let start = self.event_voice_index.get(&t.start_event); let end = self.event_voice_index.get(&t.end_event); match t.class { TieClass::Standard => { if let (Some((sv, si)), Some((ev, ei))) = (start, end) { if sv != ev || *ei != si + 1 { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!( "standard tie {:?} is not same-voice immediately adjacent", @@ -2355,7 +2412,7 @@ impl<'a> GraphIndex<'a> { TieClass::Editorial => { if let (Some((sv, si)), Some((ev, ei))) = (start, end) { if sv != ev || ei <= si { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!("editorial tie {:?} is not same-voice forward", t.id), )); @@ -2367,7 +2424,7 @@ impl<'a> GraphIndex<'a> { let einst = self.event_instance.get(&t.end_event); if let (Some(a), Some(b)) = (sinst, einst) { if a != b { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!("cross-voice tie {:?} crosses staff instances", t.id), )); @@ -2381,7 +2438,7 @@ impl<'a> GraphIndex<'a> { self.event_start_key(t.end_event), ) { if !s.le_same_clock(&e) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::TiePairing, format!("cross-voice tie {:?} has start position after end", t.id), )); @@ -2393,7 +2450,7 @@ impl<'a> GraphIndex<'a> { } // --- 18. Voice origin consistency / promoted-id derivation. ------------- - fn check_voice_origin_consistent(&self, out: &mut Vec) { + fn check_voice_origin_consistent(&self, out: &mut Vec) { for (_r, si, v) in self.score.voices() { match &v.origin { VoiceOrigin::SystemPromoted { @@ -2411,7 +2468,7 @@ impl<'a> GraphIndex<'a> { *losing_operation, ); if v.id != expected { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::VoiceOriginConsistent, format!( "system-promoted voice {:?} != its derivation {:?}", @@ -2422,7 +2479,7 @@ impl<'a> GraphIndex<'a> { } VoiceOrigin::UserDeclared | VoiceOrigin::Imported { .. } => { if v.id.replica() == ReplicaId::SYSTEM_DERIVED { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::VoiceOriginConsistent, format!( "user/imported voice {:?} uses the reserved SYSTEM_DERIVED replica", @@ -2436,7 +2493,7 @@ impl<'a> GraphIndex<'a> { } // --- 19. Barline group members stay within one region. ------------------ - fn check_barline_group_same_region(&self, out: &mut Vec) { + fn check_barline_group_same_region(&self, out: &mut Vec) { for r in &self.score.canvas.regions { let region_instances: BTreeSet = r.staff_instances().iter().map(|si| si.id).collect(); @@ -2448,7 +2505,7 @@ impl<'a> GraphIndex<'a> { for g in r.content.barline_alignment_groups() { for m in &g.members { if !region_instances.contains(&m.staff_instance) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::BarlineGroupSameRegion, format!( "barline group {:?} member instance {:?} is outside region {:?}", @@ -2462,7 +2519,7 @@ impl<'a> GraphIndex<'a> { .map(|ms| ms.contains(&m.measure)) .unwrap_or(false) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::BarlineGroupSameRegion, format!( "barline group {:?} measure {:?} is not in instance {:?}", @@ -2741,7 +2798,7 @@ impl<'a> GraphIndex<'a> { /// 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) { + fn check_measure_meter_consistency(&self, out: &mut Vec) { let time_sigs: HashMap = self .score .time_signatures @@ -2770,7 +2827,7 @@ impl<'a> GraphIndex<'a> { if time_sigs.contains_key(&sig) { match self.measure20_governing_time_signature(sequence, &m.start) { Governing20::Unique(active) if active != sig => { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::MeasureMeterConsistency, format!( "measure {:?} declares time signature {:?} but the \ @@ -2803,7 +2860,7 @@ impl<'a> GraphIndex<'a> { match self.measure20_musical_delta(&prev.start, &m.start) { Some(delta) if &delta == ts.measure_duration() => {} Some(_) => { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::MeasureMeterConsistency, format!( "measure {:?} start is not exactly one \ @@ -2848,7 +2905,7 @@ impl<'a> GraphIndex<'a> { /// A staff naming a group that does not exist is **not** flagged here: /// dangling reference resolution belongs to the referential invariants, and /// abstaining keeps this invariant's witnesses about *agreement* only. - fn check_staff_names_absent_group(&self, out: &mut Vec) { + fn check_staff_names_absent_group(&self, out: &mut Vec) { let members: HashMap> = self .score .staff_groups @@ -2861,7 +2918,7 @@ impl<'a> GraphIndex<'a> { }; if let Some(ids) = members.get(&group_id) { if !ids.contains(&staff.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::StaffGroupMembershipAgreement, format!( "S->G: staff {:?} names group {:?}, but that group's members omit it", @@ -2879,7 +2936,7 @@ impl<'a> GraphIndex<'a> { /// /// A member id with no live staff is **not** flagged here, for the same /// reason as the S→G direction. - fn check_group_lists_unowned_staff(&self, out: &mut Vec) { + fn check_group_lists_unowned_staff(&self, out: &mut Vec) { let owner: HashMap> = self .score .staves @@ -2892,7 +2949,7 @@ impl<'a> GraphIndex<'a> { continue; }; if *named != Some(group.id) { - out.push(InvariantViolation::new( + out.push(WellFormednessViolation::invariant( GraphInvariant::StaffGroupMembershipAgreement, format!( "G->S: group {:?} lists staff {:?}, but that staff names {:?}", @@ -4216,7 +4273,8 @@ mod review_fix_tests_3 { #[cfg(test)] mod review_fix_tests_4 { //! Tests for this review pass: aleatoric ordering/bounds validation (F3), - //! tempo-map segment invariants (F4), metric overlap via tempo conversion + //! tempo-map segment conditions (F4) — **requirements, not invariants, since + //! P13-S29** — metric overlap via tempo conversion //! (F5), inv-11 time-signature/barline/graphic namespace + uniqueness (F6), //! inv-10 staff-group/part/view/meter reference resolution (F8), dangling //! decomposition tuplet refs (F9), and tuplet ratio consistency (F10). @@ -4237,6 +4295,11 @@ mod review_fix_tests_4 { !check_invariant(s, inv).is_empty() } + /// P13-S29: the Chapter 3/4 riders no longer answer to `check_invariant`. + fn fires_req(s: &Score, label: &str) -> bool { + !check_requirement(s, label).is_empty() + } + fn aleatoric_region_events(s: &Score) -> (usize, Vec) { // valid_score_rich's region C (index 2) is aleatoric (musical). let idx = s @@ -4261,7 +4324,7 @@ mod review_fix_tests_4 { if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { m.ordering = EventOrderingDAG::try_new(edges).unwrap(); } - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); + assert!(fires_req(&s, "req:time:aleatoric-reference-locality")); } #[test] @@ -4273,7 +4336,7 @@ mod review_fix_tests_4 { if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { m.bounds.insert(ghost, EventBounds::default()); } - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); + assert!(fires_req(&s, "req:time:aleatoric-reference-locality")); // A reversed (min > max) window on a real region event. let mut s = valid_score_rich(202); @@ -4318,7 +4381,7 @@ mod review_fix_tests_4 { shape: TempoShape::Linear, }], }; - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); + assert!(fires_req(&s, "req:time:tempo-segment-shape")); // Constant segment whose end_tempo disagrees with start_tempo. let mut s = base.clone(); @@ -4332,7 +4395,7 @@ mod review_fix_tests_4 { shape: TempoShape::Constant, }], }; - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); + assert!(fires_req(&s, "req:time:tempo-segment-shape")); // Out-of-order segments (start 2 then start 1). let mut s = base.clone(); @@ -4347,7 +4410,7 @@ mod review_fix_tests_4 { initial: None, segments: vec![seg(2, 3), seg(1, 2)], }; - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); + assert!(fires_req(&s, "req:time:tempo-segment-order")); // Segment anchored to a non-existent region (dangling anchor target). let mut s = base.clone(); @@ -4602,8 +4665,12 @@ mod accidental_compatibility_tests { use crate::generators::valid_score; use crate::pitch::PitchSpaceId; - fn fires(s: &Score, inv: GraphInvariant) -> bool { - !check_invariant(s, inv).is_empty() + /// P13-S29 pin 11b. The label moved from the witness text to the selector, + /// so these observations select by label instead of grepping the witness — + /// a witness search would pass on *any* violation once pin 8a removed the + /// suffix, leaving both negatives green and vacuous. + fn compatibility_violations(s: &Score) -> Vec { + check_requirement(s, "req:tuning:accidental-modification-compatibility") } #[test] @@ -4616,13 +4683,11 @@ mod accidental_compatibility_tests { "cmn-accidentals", PitchSpaceModification::CmnChromatic(1), )); - let violations = check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve); assert!( - violations - .iter() - .all(|v| !v.witness.contains("accidental-modification-compatibility")), + compatibility_violations(&s).is_empty(), "a CmnChromatic accidental in cmn-12 must not violate the compatibility \ - invariant, got: {violations:?}" + requirement, got: {:?}", + compatibility_violations(&s) ); } @@ -4638,13 +4703,22 @@ mod accidental_compatibility_tests { "cmn-accidentals", PitchSpaceModification::CmnChromatic(1), )); - assert!(fires(&s, GraphInvariant::CrossCuttingRefsResolve)); - let violations = check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve); + let violations = compatibility_violations(&s); assert!( - violations - .iter() - .any(|v| v.witness.contains("accidental-modification-compatibility")), - "expected an accidental-modification-compatibility violation, got: {violations:?}" + !violations.is_empty(), + "expected an accidental-modification-compatibility violation" + ); + // Pin 8a: the label is the Display prefix now, so the witness must not + // carry it. Label-free and exact in the two ways that matter. + assert!( + violations[0].witness.ends_with("interval algebra"), + "witness must end with the algebra clause, got: {:?}", + violations[0].witness + ); + assert!( + !violations[0].witness.contains("req:"), + "witness must not restate its own label, got: {:?}", + violations[0].witness ); } @@ -4655,10 +4729,7 @@ mod accidental_compatibility_tests { // be silent across the existing test/property-test corpus. let s = valid_score(301); assert!(s.tuning_context.accidental_extensions.is_empty()); - let violations = check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve); - assert!(violations - .iter() - .all(|v| !v.witness.contains("accidental-modification-compatibility"))); + assert!(compatibility_violations(&s).is_empty()); } } @@ -4693,6 +4764,112 @@ mod g3a_tests { /// /// **Mutation:** revert the doc comment to its pre-G3a text (naming only /// cross-cutting structures and event-internal references); must fail. + #[test] + fn violation_types_declare_their_pinned_derives() { + // P13-S29 pin 1b. Placed HERE, not beside pin 10's tests, because + // `production_source()` is private to this module. + // + // Six equalities, not needles: a guard that merely searches for `Eq`, + // `Hash` or one phrase passes every deletion mutation while failing + // every promise the pin makes. + let src = production_source(); + + let before = |decl: &str| -> Vec { + let at = src + .find(decl) + .unwrap_or_else(|| panic!("{decl} is declared")); + src[..at] + .lines() + .rev() + .take_while(|l| { + let t = l.trim(); + t.starts_with("///") || t.starts_with("#[derive") + }) + .map(|l| l.trim().to_owned()) + .collect() + }; + + let struct_lines = before("pub struct WellFormednessViolation {"); + let enum_lines = before("pub enum ViolationKind {"); + + // 1 and 2: the derive line immediately preceding each declaration. + assert_eq!( + struct_lines.first().map(String::as_str), + Some("#[derive(Clone, PartialEq, Eq, Debug)]"), + "WellFormednessViolation's derives are pinned" + ); + assert_eq!( + enum_lines.first().map(String::as_str), + Some("#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]"), + "ViolationKind's derives are pinned" + ); + + // 4 and 5: the /// block immediately preceding THAT derive. + let doc = |lines: &[String]| -> String { + lines + .iter() + .skip(1) + .rev() + .map(|l| l.trim_start_matches("///").trim()) + .collect::>() + .join(" ") + }; + assert_eq!( + doc(&struct_lines), + "A well-formedness failure: one [`ViolationKind`] — `Invariant` or \ + `Requirement` — and the witness identifying the smallest offending objects. \ + A requirement failure is not an invariant failure.", + "WellFormednessViolation's rustdoc is pinned" + ); + assert_eq!( + doc(&enum_lines), + "What a [`WellFormednessViolation`] failed. `Invariant` names a numbered \ + Chapter 5 graph invariant; `Requirement` names a normative requirement by its \ + label. A requirement failure is not an invariant failure, and there is no \ + third arm and no unclassified fallback.", + "ViolationKind's rustdoc is pinned" + ); + + // 3: the module header's two-arm paragraph, first line to next blank //!. + let head = src + .find("//! Violations carry a two-armed") + .expect("the module header states the two-arm split"); + let para_end = src[head..].find("\n//!\n").expect("the paragraph ends") + head; + let para = src[head..para_end] + .lines() + .map(|l| l.trim_start_matches("//!").trim()) + .collect::>() + .join(" "); + assert_eq!( + para, + "Violations carry a two-armed [`ViolationKind`]: `Invariant` for the Chapter 5 \ + graph invariants, `Requirement` for a normative requirement named by its \ + label. A requirement failure is not an invariant failure, and neither arm is \ + a fallback for the other.", + "the module header's two-arm paragraph is pinned" + ); + + // 6: the whole of the integration test, so its no-call constraint is + // observed rather than assumed. + assert_eq!( + include_str!("../../epiphany-core/tests/public_surface.rs"), + include_str!("../tests/public_surface.rs"), + "public_surface.rs is read from one path" + ); + let surface = include_str!("../tests/public_surface.rs"); + assert!( + surface.contains( + "use epiphany_core::{check_requirement, ViolationKind, WellFormednessViolation};" + ), + "the integration test must import all three names from the root" + ); + assert!( + !surface.contains("check_requirement(&"), + "public_surface.rs must stay type-level: a call whose result is asserted \ + would widen M3's and M9's radii" + ); + } + #[test] fn t12_invariant_10_doc_block_slices_and_is_non_empty() { // Narrowed by P13-S26 pin 8. The exact (token, target) comparison lives @@ -6279,9 +6456,9 @@ mod g3b_dispatch_tests { "the score must violate invariant 20 directly" ); assert!( - check_invariants(&s) - .iter() - .any(|v| v.invariant == GraphInvariant::MeasureMeterConsistency), + check_invariants(&s).iter().any( + |v| v.kind == ViolationKind::Invariant(GraphInvariant::MeasureMeterConsistency) + ), "check_invariants (the top-level dispatch) must surface the invariant-20 \ violation -- this is the behavioural assertion M40 needs, since \ an all().len() count alone passes even with the dispatch arm deleted" @@ -6348,8 +6525,8 @@ mod s16_agreement_dispatch_tests { got {violations:?}" ); assert_eq!( - violations[0].invariant, - GraphInvariant::StaffGroupMembershipAgreement, + violations[0].kind, + ViolationKind::Invariant(GraphInvariant::StaffGroupMembershipAgreement), "the single violation must be invariant 21, got {violations:?}" ); assert!( @@ -6421,8 +6598,8 @@ mod s16_agreement_dispatch_tests { got {violations:?}" ); assert_eq!( - violations[0].invariant, - GraphInvariant::StaffGroupMembershipAgreement, + violations[0].kind, + ViolationKind::Invariant(GraphInvariant::StaffGroupMembershipAgreement), "the single violation must be invariant 21, got {violations:?}" ); assert!( @@ -6451,3 +6628,604 @@ mod s16_agreement_dispatch_tests { ); } } + +#[cfg(test)] +mod s29_violation_kind_tests { + //! P13-S29 pin 10: the closed per-condition matrix, one fixture per emitted + //! condition, plus the whole-surface tests. + //! + //! Requirement-arm assertions are on `(kind, witness)` **pairs**, never on + //! the label alone: three labels are shared by two conditions each, and C6's + //! natural fixture emits C6 *and* C7, so a label-only assertion survives + //! mislabelling one of them. + use super::*; + use crate::accidental::{fixture_extensions, PitchSpaceModification}; + use crate::generators::valid_score; + use crate::graph::{EventOrderingDAG, RegionTimeModel}; + use crate::pitch::PitchSpaceId; + use crate::tempo::{Tempo, TempoMap, TempoSegment, TempoShape}; + use crate::time::{AnchorOffset, RationalTime, RegionEdge, TimeAnchor}; + + const SHAPE: &str = "req:time:tempo-segment-shape"; + const ORDER: &str = "req:time:tempo-segment-order"; + const LOCALITY: &str = "req:time:aleatoric-reference-locality"; + const TUNING: &str = "req:tuning:accidental-modification-compatibility"; + + fn anchor(id: crate::ids::RegionId, at: i32) -> TimeAnchor { + TimeAnchor::Region { + id, + edge: RegionEdge::Start, + offset: AnchorOffset::Musical(crate::time::MusicalDuration(RationalTime::from_int(at))), + } + } + + /// A region id no score declares. + fn ghost_region(s: &Score, n: u64) -> crate::ids::RegionId { + crate::ids::RegionId::new(s.identity.replica_id, n) + } + + fn tempo(bpm: f64) -> Tempo { + Tempo::quarter(bpm).unwrap() + } + + /// Pin 10's requirement-arm template: the aggregate carries the pair, the + /// invariant selector does **not** carry it, `check_requirement` does, and + /// the fixture's invariant arm is **empty** — the last being what keeps + /// these seven structurally out of M2a's radius. + fn assert_requirement_condition(s: &Score, label: &'static str, witness: &str) { + let all = check_invariants(s); + let expected = (ViolationKind::Requirement(label), witness.to_owned()); + let pairs: Vec<_> = all.iter().map(|v| (v.kind, v.witness.clone())).collect(); + assert!( + pairs.contains(&expected), + "aggregate must carry {expected:?}; got {pairs:?}" + ); + assert!( + check_invariant(s, GraphInvariant::CrossCuttingRefsResolve).is_empty(), + "the rider must not answer to invariant 10; got {:?}", + check_invariant(s, GraphInvariant::CrossCuttingRefsResolve) + ); + let via = check_requirement(s, label); + assert!( + via.iter().any(|v| v.witness == witness), + "check_requirement({label}) must return the pair; got {via:?}" + ); + assert!( + !all.iter() + .any(|v| matches!(v.kind, ViolationKind::Invariant(_))), + "fixture must violate no invariant at all; got {all:?}" + ); + } + + fn assert_invariant_condition(s: &Score, witness_fragment: &str) { + let all = check_invariants(s); + assert!( + all.iter().any(|v| v.kind + == ViolationKind::Invariant(GraphInvariant::CrossCuttingRefsResolve) + && v.witness.contains(witness_fragment)), + "aggregate must carry invariant 10 for {witness_fragment:?}; got {all:?}" + ); + assert!( + check_invariant(s, GraphInvariant::CrossCuttingRefsResolve) + .iter() + .any(|v| v.witness.contains(witness_fragment)), + "the invariant selector must return it" + ); + } + + /// The production half of this file — everything before the first test + /// module. `g3a_tests` has its own copy; that one is private to it, which + /// pin 1b records as the reason its derives guard lives there rather than + /// here. + fn production_source() -> &'static str { + include_str!("invariants.rs") + .split_once("#[cfg(test)]") + .map(|(before, _)| before) + .expect("this file contains at least one #[cfg(test)] module") + } + + fn one_segment(seed: u64, seg: impl Fn(crate::ids::RegionId) -> TempoSegment) -> Score { + let mut s = valid_score(seed); + let rid = s.canvas.regions[0].id; + s.tempo_map = TempoMap { + initial: None, + segments: vec![seg(rid)], + }; + s + } + + // ---- C1-C3: the invariant arm ------------------------------------------- + + #[test] + fn cross_cutting_refs_stay_invariant_ten() { + // Any condition of `check_cross_cutting_refs` serves; a staff's + // declared instrument is the most stable across generator changes. + let mut s = valid_score(400); + let ghost = crate::ids::InstrumentId::new(s.identity.replica_id, 9_400_101); + s.staves[0].instrument = ghost; + assert_invariant_condition(&s, "is not declared"); + } + + #[test] + fn tempo_start_anchor_stays_invariant_ten() { + let base = valid_score(401); + let ghost = ghost_region(&base, 9_400_201); + let s = one_segment(401, |_| TempoSegment { + start: anchor(ghost, 0), + end: None, + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Constant, + }); + assert_invariant_condition(&s, "start anchor target"); + } + + #[test] + fn tempo_end_anchor_stays_invariant_ten() { + let base = valid_score(402); + let ghost = ghost_region(&base, 9_400_202); + let s = one_segment(402, |rid| TempoSegment { + start: anchor(rid, 0), + end: Some(anchor(ghost, 1)), + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Constant, + }); + assert_invariant_condition(&s, "end anchor target"); + } + + // ---- C4-C10: the requirement arm ---------------------------------------- + + #[test] + fn tempo_constant_mismatch_reports_shape() { + let s = one_segment(403, |rid| TempoSegment { + start: anchor(rid, 0), + end: None, + start_tempo: tempo(60.0), + end_tempo: Some(tempo(120.0)), + shape: TempoShape::Constant, + }); + assert_requirement_condition( + &s, + SHAPE, + "constant tempo segment has end_tempo != start_tempo", + ); + } + + #[test] + fn tempo_nonconstant_missing_end_reports_shape() { + let s = one_segment(404, |rid| TempoSegment { + start: anchor(rid, 0), + end: Some(anchor(rid, 1)), + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Linear, + }); + assert_requirement_condition( + &s, + SHAPE, + "non-constant tempo segment is missing its end_tempo", + ); + } + + fn two_segments(seed: u64, a: (i32, i32), b: (i32, i32)) -> Score { + let mut s = valid_score(seed); + let rid = s.canvas.regions[0].id; + let seg = |from: i32, to: i32| TempoSegment { + start: anchor(rid, from), + end: Some(anchor(rid, to)), + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Constant, + }; + s.tempo_map = TempoMap { + initial: None, + segments: vec![seg(a.0, a.1), seg(b.0, b.1)], + }; + s + } + + #[test] + fn tempo_out_of_order_reports_order() { + let s = two_segments(405, (2, 3), (1, 2)); + assert_requirement_condition(&s, ORDER, "tempo segments are out of start order"); + } + + #[test] + fn tempo_overlap_reports_order() { + let s = two_segments(406, (2, 3), (1, 2)); + assert_requirement_condition(&s, ORDER, "tempo segments overlap in musical time"); + } + // ---- C8-C10 need their fixtures from the existing corpus ---------------- + + fn aleatoric_idx_and_events(s: &Score) -> (usize, Vec) { + let idx = s + .canvas + .regions + .iter() + .position(|r| matches!(r.time_model, RegionTimeModel::Aleatoric(_))) + .expect("valid_score_rich region C is aleatoric"); + let evs = s.canvas.regions[idx].staff_instances()[0].voices[0] + .events + .clone(); + (idx, evs) + } + + #[test] + fn aleatoric_ordering_outside_region_reports_locality() { + let mut s = crate::generators::valid_score_rich(407); + let (idx, evs) = aleatoric_idx_and_events(&s); + let ghost = crate::ids::EventId::new(s.identity.replica_id, 9_400_401); + let mut edges = std::collections::BTreeMap::new(); + edges.insert(evs[0], vec![ghost]); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.ordering = EventOrderingDAG::try_new(edges).unwrap(); + } + assert_requirement_condition( + &s, + LOCALITY, + &format!( + "aleatoric region {:?} ordering references event {:?}, absent from the region", + s.canvas.regions[idx].id, ghost + ), + ); + } + + #[test] + fn aleatoric_bounds_outside_region_reports_locality() { + let mut s = crate::generators::valid_score_rich(408); + let (idx, _) = aleatoric_idx_and_events(&s); + let ghost = crate::ids::EventId::new(s.identity.replica_id, 9_400_402); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.bounds.insert(ghost, crate::time::EventBounds::default()); + } + assert_requirement_condition( + &s, + LOCALITY, + &format!( + "aleatoric region {:?} bounds key event {:?} is absent from the region", + s.canvas.regions[idx].id, ghost + ), + ); + } + + #[test] + fn accidental_incompatible_reports_tuning_requirement() { + let mut s = valid_score(410); + s.tuning_context.default_pitch_space = PitchSpaceId::new("edo-31"); + s.tuning_context + .accidental_extensions + .push(fixture_extensions( + "cmn-accidentals", + PitchSpaceModification::CmnChromatic(1), + )); + let via = check_requirement(&s, TUNING); + assert!(!via.is_empty(), "expected a compatibility violation"); + assert!( + via[0].witness.ends_with("interval algebra") && !via[0].witness.contains("req:"), + "witness must be label-free and end with the algebra clause; got {:?}", + via[0].witness + ); + assert!( + check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve).is_empty(), + "the rider must not answer to invariant 10" + ); + } + + // ---- whole-surface ------------------------------------------------------- + + #[test] + fn graph_invariant_all_is_unchanged() { + let seq: Vec<(GraphInvariant, u8)> = GraphInvariant::all() + .into_iter() + .map(|i| (i, i.number())) + .collect(); + let expected: Vec<(GraphInvariant, u8)> = vec![ + (GraphInvariant::EventVoiceBacklink, 1), + (GraphInvariant::VoiceEventBacklink, 2), + (GraphInvariant::VoiceEventsSortedNonOverlap, 3), + (GraphInvariant::EventCoordinateModel, 4), + (GraphInvariant::ContainmentTree, 5), + (GraphInvariant::StaffInstanceResolves, 6), + (GraphInvariant::RegionExtents, 7), + (GraphInvariant::MeasureSingleInstance, 8), + (GraphInvariant::AnchorOffsetModel, 9), + (GraphInvariant::CrossCuttingRefsResolve, 10), + (GraphInvariant::UniqueIdentifiers, 11), + (GraphInvariant::PitchIdUnique, 12), + (GraphInvariant::SpellingScopeResolves, 13), + (GraphInvariant::DecompositionTargetResolves, 14), + (GraphInvariant::DecompositionSum, 15), + (GraphInvariant::TupletSum, 16), + (GraphInvariant::TiePairing, 17), + (GraphInvariant::VoiceOriginConsistent, 18), + (GraphInvariant::BarlineGroupSameRegion, 19), + (GraphInvariant::MeasureMeterConsistency, 20), + (GraphInvariant::StaffGroupMembershipAgreement, 21), + ]; + assert_eq!( + seq, expected, + "GraphInvariant::all() is frozen by P13-S29 pin 8" + ); + + // `all()` is not the enum: a variant declared and omitted from `all()` + // leaves the sequence untouched. Independent declaration inventory. + let src = production_source(); + let a = src.find("pub enum GraphInvariant {").expect("declaration"); + let b = src[a..].find("\n}").expect("close") + a; + let declared: Vec<&str> = src[a..b] + .lines() + .filter_map(|l| l.trim().strip_suffix(',')) + .filter(|l| !l.starts_with("///") && !l.starts_with("//")) + .collect(); + let names: Vec = expected.iter().map(|(i, _)| format!("{i:?}")).collect(); + assert_eq!( + declared, names, + "the enum declares exactly all()'s variants, in order" + ); + } + + #[test] + fn display_renders_each_arm_exactly() { + // Invariant side: a reversed aleatoric bound (invariant 4), acquired + // from the aggregate -- pinned, because acquisition decides M3's radius. + let s = reversed_aleatoric_bound(411); + let inv = check_invariants(&s) + .into_iter() + .find(|v| v.kind == ViolationKind::Invariant(GraphInvariant::EventCoordinateModel)) + .expect("an invariant-arm violation"); + assert_eq!( + inv.to_string(), + format!( + "invariant 4 (EventCoordinateModel) violated: {}", + inv.witness + ) + ); + + // Requirement side: a real accidental violation, from the aggregate. + let mut s = valid_score(412); + s.tuning_context.default_pitch_space = PitchSpaceId::new("edo-31"); + s.tuning_context + .accidental_extensions + .push(fixture_extensions( + "cmn-accidentals", + PitchSpaceModification::CmnChromatic(1), + )); + let req = check_invariants(&s) + .into_iter() + .find(|v| v.kind == ViolationKind::Requirement(TUNING)) + .expect("a requirement-arm violation"); + assert!( + !req.witness.contains("req:"), + "independent oracle: the witness must not carry its own label" + ); + assert_eq!( + req.to_string(), + format!("requirement {TUNING} violated: {}", req.witness) + ); + } + + #[test] + fn mixed_fixture_splits_by_arm() { + // Pinned fixture: a dangling tempo START anchor (C2, invariant arm) and + // an out-of-region aleatoric ORDERING event (C8, requirement arm). + let mut s = crate::generators::valid_score_rich(409); + let (idx, evs) = aleatoric_idx_and_events(&s); + let ghost_event = crate::ids::EventId::new(s.identity.replica_id, 9_400_501); + let mut edges = std::collections::BTreeMap::new(); + edges.insert(evs[0], vec![ghost_event]); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.ordering = EventOrderingDAG::try_new(edges).unwrap(); + } + let ghost_rid = ghost_region(&s, 9_400_502); + s.tempo_map = TempoMap { + initial: None, + segments: vec![TempoSegment { + start: anchor(ghost_rid, 0), + end: None, + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Constant, + }], + }; + + // All three surfaces, not the aggregate alone. + let all = check_invariants(&s); + assert!( + all.iter().any( + |v| v.kind == ViolationKind::Invariant(GraphInvariant::CrossCuttingRefsResolve) + ), + "aggregate must carry the anchor as invariant 10; got {all:?}" + ); + assert!( + all.iter() + .any(|v| v.kind == ViolationKind::Requirement(LOCALITY)), + "aggregate must carry the rider as its requirement; got {all:?}" + ); + + let via_inv = check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve); + assert!( + via_inv.iter().all(|v| v.witness.contains("anchor target")), + "the invariant selector must return the anchor only; got {via_inv:?}" + ); + let via_req = check_requirement(&s, LOCALITY); + assert!( + !via_req.is_empty() + && via_req + .iter() + .all(|v| v.witness.contains("ordering references")), + "the requirement selector must return the rider only; got {via_req:?}" + ); + } + + #[test] + /// Pin 3a. The `.tex` requirement block equals pin 3's pinned source, by + /// whitespace-collapsed **equality** — not required phrases plus a + /// forbidden-stem list. A stem inventory cannot anticipate the sentence + /// someone will actually write, and M14e is exactly that sentence: it uses + /// no forbidden stem and settles P13-S8 inside a requirement minted not to. + fn tempo_segment_shape_requirement_states_its_clauses_and_stays_s8_neutral() { + const TEX: &str = include_str!("../../../spec/core_spec.tex"); + const LABEL: &str = r"\label{req:time:tempo-segment-shape}"; + + let at = TEX.find(LABEL).expect("the requirement is minted"); + let start = TEX[..at] + .rfind(r"\begin{requirement}") + .expect("its block opens"); + let end_tag = r"\end{requirement}"; + let end = TEX[at..].find(end_tag).expect("its block closes") + at + end_tag.len(); + let collapse = |s: &str| s.split_whitespace().collect::>().join(" "); + + assert_eq!( + collapse(&TEX[start..end]), + collapse( + r"\begin{requirement} + \label{req:time:tempo-segment-shape} + A tempo segment's \texttt{shape} and its \texttt{end\_tempo} \MUST{} be + compatible. If \texttt{shape} is \texttt{Constant} and \texttt{end\_tempo} + is present, it \MUST{} equal \texttt{start\_tempo}. If \texttt{shape} is + \texttt{Linear}, \texttt{Exponential} or \texttt{Curve}, \texttt{end\_tempo} + \MUST{} be present. + + This requirement states the compatibility that is enforced. It does not + determine whether a constant segment records an \texttt{end\_tempo} at all. +\end{requirement}" + ), + "pin 3's block is frozen; any edit must be deliberate" + ); + } + + /// A region-local aleatoric bound whose window is reversed (`min > max`). + /// The bounds key is **in** the region, so this trips invariant 4 and + /// **not** C9's locality requirement. + fn reversed_aleatoric_bound(seed: u64) -> Score { + let mut s = crate::generators::valid_score_rich(seed); + let (idx, evs) = aleatoric_idx_and_events(&s); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.bounds.insert( + evs[0], + crate::time::EventBounds { + start: Some(crate::time::TimeBounds::MusicalRange { + min: crate::time::MusicalPosition(RationalTime::new(1, 2).unwrap()), + max: crate::time::MusicalPosition::origin(), + }), + end: None, + }, + ); + } + s + } + + #[test] + /// Pin 10's eleventh row: the reversed-bounds condition is **unchanged** by + /// this rung and stays in the invariant arm as invariant 4. + fn reversed_aleatoric_bounds_stay_invariant_four() { + let s = reversed_aleatoric_bound(414); + let all = check_invariants(&s); + let pair = all + .iter() + .find(|v| v.witness.contains("reversed")) + .expect("the reversed bound must be reported"); + assert_eq!( + pair.kind, + ViolationKind::Invariant(GraphInvariant::EventCoordinateModel), + "reversed bounds are invariant 4, not a requirement; got {pair:?}" + ); + let four = check_invariant(&s, GraphInvariant::EventCoordinateModel); + assert!( + four.iter().any(|v| v.witness.contains("reversed")), + "invariant 4's selector must return it; got {four:?}" + ); + // Two assertions, not three: pin 10's invariant-arm template is the + // aggregate and the selector. A `check_requirement` negative here would + // put this test in M3's radius, which §3 pinned without it. + } + + #[test] + fn invariant_selector_discriminates_its_payload() { + // Two different invariant variants in one score: a dangling staff + // instrument (10) and a reversed aleatoric bound (4). + let mut s = crate::generators::valid_score_rich(413); + let ghost = crate::ids::InstrumentId::new(s.identity.replica_id, 9_400_601); + s.staves[0].instrument = ghost; + let (idx, evs) = aleatoric_idx_and_events(&s); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.bounds.insert( + evs[0], + crate::time::EventBounds { + start: Some(crate::time::TimeBounds::MusicalRange { + min: crate::time::MusicalPosition(RationalTime::new(1, 2).unwrap()), + max: crate::time::MusicalPosition::origin(), + }), + end: None, + }, + ); + } + + let ten = check_invariant(&s, GraphInvariant::CrossCuttingRefsResolve); + assert!( + !ten.is_empty() && ten.iter().all(|v| v.witness.contains("is not declared")), + "invariant 10's selector must return only its own; got {ten:?}" + ); + let four = check_invariant(&s, GraphInvariant::EventCoordinateModel); + assert!( + !four.is_empty() && four.iter().all(|v| v.witness.contains("reversed")), + "invariant 4's selector must return only its own; got {four:?}" + ); + } + + #[test] + fn requirement_selector_discriminates_its_payload() { + // Two different requirement labels in one score: C5 (shape) and C8 + // (locality). + let mut s = crate::generators::valid_score_rich(414); + let (idx, evs) = aleatoric_idx_and_events(&s); + let ghost_event = crate::ids::EventId::new(s.identity.replica_id, 9_400_701); + let mut edges = std::collections::BTreeMap::new(); + edges.insert(evs[0], vec![ghost_event]); + if let RegionTimeModel::Aleatoric(m) = &mut s.canvas.regions[idx].time_model { + m.ordering = EventOrderingDAG::try_new(edges).unwrap(); + } + let rid = s.canvas.regions[0].id; + s.tempo_map = TempoMap { + initial: None, + segments: vec![TempoSegment { + start: anchor(rid, 0), + end: Some(anchor(rid, 1)), + start_tempo: tempo(60.0), + end_tempo: None, + shape: TempoShape::Linear, + }], + }; + + let shape = check_requirement(&s, SHAPE); + assert!( + !shape.is_empty() && shape.iter().all(|v| v.witness.contains("end_tempo")), + "the shape label must return only its own; got {shape:?}" + ); + let locality = check_requirement(&s, LOCALITY); + assert!( + !locality.is_empty() + && locality + .iter() + .all(|v| v.witness.contains("ordering references")), + "the locality label must return only its own; got {locality:?}" + ); + } + + #[test] + fn violation_kind_has_exactly_two_arms() { + let src = production_source(); + let a = src.find("pub enum ViolationKind {").expect("declaration"); + let b = src[a..].find("\n}").expect("close") + a; + let arms: Vec<&str> = src[a..b] + .lines() + .filter_map(|l| l.trim().strip_suffix(',')) + .collect(); + assert_eq!( + arms, + vec!["Invariant(GraphInvariant)", "Requirement(&'static str)"], + "ViolationKind has exactly two arms and no unclassified fallback" + ); + } +} diff --git a/crates/epiphany-core/src/lib.rs b/crates/epiphany-core/src/lib.rs index c04aea0..a78668c 100644 --- a/crates/epiphany-core/src/lib.rs +++ b/crates/epiphany-core/src/lib.rs @@ -181,6 +181,6 @@ pub use codec::{CanonicalValue, ScoreDecodeError}; pub use indexes::ScoreIndexes; pub use invariants::{ - check_invariant, check_invariants, deferred_checks, measure_anchor_relation, DeferredCheck, - GraphInvariant, InvariantViolation, + check_invariant, check_invariants, check_requirement, deferred_checks, measure_anchor_relation, + DeferredCheck, GraphInvariant, ViolationKind, WellFormednessViolation, }; diff --git a/crates/epiphany-core/tests/public_surface.rs b/crates/epiphany-core/tests/public_surface.rs new file mode 100644 index 0000000..b6333d9 --- /dev/null +++ b/crates/epiphany-core/tests/public_surface.rs @@ -0,0 +1,17 @@ +//! P13-S29 pin 1b: the root re-export has an observer. +//! +//! An integration test, not a unit test: a unit test inside the crate reaches +//! `invariants::` regardless of what the root re-exports, so only a consumer +//! outside the crate can observe touch row 2 at all. +//! +//! **Type-level only.** It calls nothing. A call whose result were asserted +//! would put this file in M3's and M9's radii; the file stays type-level so the +//! question never arises. + +use epiphany_core::{check_requirement, ViolationKind, WellFormednessViolation}; + +#[test] +fn public_violation_surface_is_reexported() { + let _: fn(&epiphany_core::Score, &str) -> Vec = check_requirement; + let _ = |k: &ViolationKind| matches!(k, ViolationKind::Requirement(_)); +} diff --git a/crates/epiphany-core/tests/score_graph.rs b/crates/epiphany-core/tests/score_graph.rs index a8a0947..1beb235 100644 --- a/crates/epiphany-core/tests/score_graph.rs +++ b/crates/epiphany-core/tests/score_graph.rs @@ -11,7 +11,7 @@ use epiphany_core::{ Pitch, PitchId, PitchSpaceId, PitchSpacePosition, PitchedEvent, RationalTime, Region, RegionContent, RegionTimeModel, ReplicaId, ScalePosition, Score, StaffBasedContent, StaffExtent, StaffInstance, StaffLineConfiguration, StemConfiguration, TimeAnchor, TimeExtent, - TuningReference, Voice, WallClockTime, + TuningReference, ViolationKind, Voice, WallClockTime, }; use epiphany_core::{Staff, StaffId, StaffInstanceId, VoiceId}; @@ -136,7 +136,7 @@ fn deleting_an_event_from_its_voice_list_is_caught() { let v = check_invariants(&score); assert!(v .iter() - .any(|x| x.invariant == GraphInvariant::EventVoiceBacklink)); + .any(|x| x.kind == ViolationKind::Invariant(GraphInvariant::EventVoiceBacklink))); } #[test] @@ -146,7 +146,9 @@ fn full_invariant_sweep_via_public_api() { for inv in GraphInvariant::all() { let bad = generators::violating_score(inv, 0xBEEF); assert!( - check_invariants(&bad).iter().any(|v| v.invariant == inv), + check_invariants(&bad) + .iter() + .any(|v| v.kind == ViolationKind::Invariant(inv)), "{inv:?} not reported on its negative graph" ); let shrunk = generators::shrink(&bad, inv); diff --git a/crates/epiphany-testkit/tests/requirement_labels.rs b/crates/epiphany-testkit/tests/requirement_labels.rs index e2e85c3..2f06a5a 100644 --- a/crates/epiphany-testkit/tests/requirement_labels.rs +++ b/crates/epiphany-testkit/tests/requirement_labels.rs @@ -16,12 +16,16 @@ use std::path::{Path, PathBuf}; // spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md) — an aleatoric region's ordering // and bounds references must name events of that same region. Measured at // execution, never predicted. -const CORE_REQUIREMENT_COUNT: usize = 215; +// +1 for req:time:tempo-segment-shape (P13-S29, pin 3: +// spec/CONTRACT_P13S29_VIOLATION_KIND.md) — the tempo rider that had no label. +// Measured at execution, never predicted. +const CORE_REQUIREMENT_COUNT: usize = 216; // +1 for req:textproj:manifest-schema-carried (G-minor, pins 8/11: // spec/PLAN_GMINOR_SCHEMA_MINOR.md); +1 for req:format:container-epoch (above); -// +1 for req:time:aleatoric-reference-locality (above). -const SUITE_REQUIREMENT_COUNT: usize = 286; -const SUITE_LABEL_COUNT: usize = 286; +// +1 for req:time:aleatoric-reference-locality (above); +// +1 for req:time:tempo-segment-shape (above). +const SUITE_REQUIREMENT_COUNT: usize = 287; +const SUITE_LABEL_COUNT: usize = 287; /// The normative chapter-to-area assignment. Keeping this as data makes adding a /// requirement under the wrong chapter fail without encoding chapter names in @@ -397,16 +401,6 @@ const DISCUSSED_NOT_CITED: &[(&str, &str)] = &[ spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md and recorded in \ spec/EVIDENCE_P13S26_EXECUTION.md as M6's verbatim diagnostic. PERMANENT.", ), - ( - "req:time:tempo-segment-shape", - "proposed by spec/CONTRACT_P13S29_VIOLATION_KIND.md; the requirement does not \ - exist until that contract's pin 3 lands. TEMPORARY -- pin 3 REMOVES this row \ - when it mints the requirement, because this row's own claim (discussed, never \ - cited) becomes false at that moment. A stale row is inert, so nothing else \ - will catch it; that contract's landing gate does. Remove by hand if S29 is \ - abandoned or the label changes. Prerequisite review scaffolding, NOT dispatch: \ - it licenses no other pin work.", - ), ]; fn requirement_strings(text: &str) -> BTreeSet { diff --git a/spec/CONTRACT_P13S29_VIOLATION_KIND.md b/spec/CONTRACT_P13S29_VIOLATION_KIND.md index 0a61b48..3db8b93 100644 --- a/spec/CONTRACT_P13S29_VIOLATION_KIND.md +++ b/spec/CONTRACT_P13S29_VIOLATION_KIND.md @@ -1,11 +1,16 @@ # Contract — P13-S29: the violation tag stops multiplexing -STATUS: RATIFIED; DISPATCHED. +STATUS: LANDED by this commit. **Ratified 2026-08-12 on the authority of the repository owner**, the final whole-artifact review returning zero findings. Review-round records accumulate above §0. +> **DATED HISTORICAL RECORD — the eighteen review-round blocks above §0 (revisions +> A–R) are an account of what was found and decided between drafting and +> ratification on 2026-08-12. They state no current condition.** The pins as +> ratified are §1's; §6's amendment 1 corrects two of §3's radius cells. + **THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during execution is **reported, not patched in place** — if it needs a pin change, that is its own amendment with its own review round. @@ -1682,7 +1687,11 @@ execution confirms it and any difference is a finding.* ## §6. AMENDMENT 1 — §3's M1·C6 AND M1·C7 RADII, MID-EXECUTION -STATUS: RATIFIED; FROZEN. Execution of P13-S29 resumes at M2. +STATUS: LANDED by this commit. + +> **DATED HISTORICAL RECORD — amendment 1 is ratified and executed. §6's finding, +> its defect class and its dispositions are an account of what was found and +> decided on 2026-08-12, and state no current condition.** Ratified 2026-08-12 on the authority of the repository owner, the final review round returning zero findings. The replacements are executed, not edited; a diff --git a/spec/EVIDENCE_P13S29_EXECUTION.md b/spec/EVIDENCE_P13S29_EXECUTION.md index a9817b6..50db1b5 100644 --- a/spec/EVIDENCE_P13S29_EXECUTION.md +++ b/spec/EVIDENCE_P13S29_EXECUTION.md @@ -354,9 +354,42 @@ suites=44 passed=1604 failed=0 ignored=0 --- -## §6. Gate 6 — pin 9's boundary check, verbatim +## §6. Gate 6 — the identifier and field migration, verbatim -*(pending)* +**6a. No `InvariantViolation` identifier in Rust code.** Gate 6 scopes this to +`crates/**/*.rs`; the contract, the ledger and this annex quote the old name +historically and are out of scope. + +``` +$ find crates -name '*.rs' -type f -exec grep -Hn 'InvariantViolation' {} + +$ echo $? +1 +``` + +*Run with `find … -exec`, not a piped `grep | head`: a universal negative from a +truncated pipe is the failure mode `CLAUDE.md` names, and this gate is a +universal negative.* + +**6b. No `.invariant` field access on a `WellFormednessViolation`.** Three hits +survive, and gate 6 requires each to be attributed rather than counted: + +``` +crates/epiphany-core/src/invariants.rs:320: self.invariant.number(), +crates/epiphany-core/src/invariants.rs:321: self.invariant, +crates/epiphany-core/src/invariants.rs:3326: assert_eq!(deferred[0].invariant, GraphInvariant::RegionExtents); +``` + +**All three are `DeferredCheck`, not the violation type.** Lines 320–321 are +inside `impl core::fmt::Display for DeferredCheck` (opened at `:315`); line 3326 +indexes the result of `deferred_checks(&s)`. + +**6c. `DeferredCheck.invariant` retained**, as §0.5 requires: + +``` +crates/epiphany-core/src/invariants.rs:305:pub struct DeferredCheck { +crates/epiphany-core/src/invariants.rs-306- /// The invariant whose decision was deferred. +crates/epiphany-core/src/invariants.rs-310- pub invariant: GraphInvariant, +``` --- @@ -465,3 +498,299 @@ they were compared against, not the observation. The mutation sequence resumes at **M2**. M1 is complete — C4, C5, C8, C9 and C10 matched their dispatched cells, and C6 and C7 match the corrected cells above. + +--- + +## §9. The mutation phase, resumed at M2 + +**§5 is closed at M1 by the digest gate (contract §6.5c-bis); this section +continues the matrix.** Every row was run as +`cargo test --workspace --no-fail-fast`, preceded by +`cargo build --tests --workspace` checked for `error[` — **a mutation that does +not compile observed nothing** — and restored by hand write-back. + +### 9.1 Five more execution faults, none a contract defect + +**They are recorded here rather than appended to §3** because §3 is the +pre-amendment record committed at `29ef3af` as amendment 1's oracle. Its count of +five is true as of that commit; these four are later events. + +#### 9.1.1 Pin 10's eleventh row was never built + +Pin 10's matrix has **eleven** rows. The eleventh is marked `—` rather than a +C-number: + +| — | reversed aleatoric bounds | **invariant 4, unchanged** | `reversed_aleatoric_bounds_stay_invariant_four` | + +It was read as a note and no test was written. **M11's cell names that test**, so +the omission surfaced as a radius mismatch — expected 4, observed 2 — and not +before. + +*A row whose identifier is a dash reads as commentary. The other ten rows carry +C-numbers; the eleventh carries the same three columns and a dash, and only the +columns matter.* + +#### 9.1.2 `display_renders_each_arm_exactly`'s invariant side was the wrong fixture + +Its comment read: + +```rust +// Invariant side: a reversed aleatoric bound (invariant 4), acquired +// from the aggregate -- pinned, because acquisition decides M3's radius. +``` + +The code beneath it built a **dangling staff instrument** and searched for +`CrossCuttingRefsResolve` — invariant 10, a C1 fixture. **The comment recorded +the pin; the code did something else.** + +Pin 10 forecloses exactly this: + +> *The choice changes radii, so it cannot be the executor's: a C1 fixture would +> put this test in M17·C1's cell, a tempo-anchor fixture in M17·C2/C3's, and +> reversed bounds put it in **M11's**, which is where it now belongs and where +> M11's cell names it.* + +Both halves of that prediction were then observed: with the fixture repaired, +`display_renders_each_arm_exactly` **entered M11's radius** (§9.3) and is +**absent from M17·C1's measured 20** (§9.4). Under the unrepaired fixture it +would have failed M17·C1 too — a second mismatch the first one pre-empted. + +*This is the most dangerous of the five fault classes in this rung: a comment +that states the pin correctly next to code that does not. Nothing reads the +comment.* + +#### 9.1.3 Pin 3a's guard did not exist + +`tempo_segment_shape_requirement_states_its_clauses_and_stays_s8_neutral` was +absent from the tree. **Thirteen mutations target it** — M12pre, M12, M13, +M13post, M13neutral, M14a–e, M15a, M15b — so thirteen cells had no possible +observer. Found when the `.tex` batch went to look for it. + +It is now implemented as pin 3a requires: the `.tex` slice from the +`\begin{requirement}` preceding the label to the first `\end{requirement}` at or +after it, whitespace-collapsed, **equal** to pin 3's pinned source. + +**M14e is the vindication of equality over a stem inventory.** It appends +`A \texttt{Constant} segment's \texttt{end\_tempo} \MUST{} be absent.` — no +`canonic`, no `normaliz`, no `prefer`, and it settles P13-S8 inside a requirement +minted not to. Equality fails it; every phrase-and-stem form passes it. + +#### 9.1.4 An interrupted run left a mutation applied + +The mutation harness restores in a `finally`. A **killed** process runs no +`finally`, so an interrupted batch leaves the tree mutated. One did: M2a's +wildcard survived at `invariants.rs:425`. + +It was found by re-reading the file, and `invariant_selector_discriminates_its_payload` +confirmed it: + +``` +invariant 10's selector must return only its own; got [ + WellFormednessViolation { kind: Invariant(CrossCuttingRefsResolve), witness: "staff ... + WellFormednessViolation { kind: Invariant(EventCoordinateModel), witness: "aleatoric ... +``` + +**Restored by hand-editing**, never git, and the full suite returned to +`44 / 1606 / 0 / 0`. + +*The lesson is not "be careful with interrupts": it is that a restore guaranteed +only by process exit is not a guarantee. **Verify the baseline after any +interrupted mutation run, before trusting the next measurement** — a stray +mutation makes every subsequent radius wrong in a way that looks like a +mismatch in the wrong place.* + +### 9.2 The surface moved twice, and what that obliges + +| Surface | Cause | +|---|---| +| 1604 | §4's surface — pin 10's 16 tests, pin 1b's two | +| **1605** | §9.1.1's missing test added | +| **1606** | §9.1.3's missing guard added | + +**Radii are measured against the final surface.** The 17 mutations first measured +at 1604 were **re-run in full** at 1605 and all matched. The 38 measured at 1605 +were **not** re-run in full at 1606; the justification is bounded and stated: + +- **Pin 3a's guard has exactly two inputs** — `core_spec.tex` via `include_str!` + and a string literal. Verified mechanically: no `production_source`, no + `check_*` call, one `include_str!` target. +- **None of those 38 modifies `core_spec.tex`.** They edit `invariants.rs`, + `generators.rs` or `public_surface.rs`. +- **Two representatives were re-run at 1606 anyway**, one per interaction class: + **M2a** — the widest selector radius, 21 — and **M20b**, a prose edit inside + `invariants.rs`. Both matched unchanged. + +*This is an argument from a test's complete input set, not from reasoning about +fixture reach — the thing this rung has repeatedly got wrong. It is recorded as +an argument, not presented as a measurement.* + +### 9.3 Expected versus observed — all 54 mutations + +| M | Cell | Observed | | +|---|---|---|---| +| M1·C4 | 2 | 2 | ✅ | +| M1·C5 | 3 | 3 | ✅ | +| M1·C6 | 2 *(amendment 1)* | 2 | ✅ | +| M1·C7 | 2 *(amendment 1)* | 2 | ✅ | +| M1·C8 | 4 | 4 | ✅ | +| M1·C9 | 2 | 2 | ✅ | +| M1·C10 | 3 | 3 | ✅ | +| M2 | 8 | 8 | ✅ | +| M2a | 21 *(measured pre-ratification)* | 21 | ✅ | +| M3 | 13 | 13 | ✅ | +| M3a | 1 | 1 | ✅ | +| M4 | 1 | 1 | ✅ | +| M5 | 1 | 1 | ✅ | +| M6 | 1 | 1 | ✅ | +| M7 | 7 | 7 | ✅ | +| M7a | 1 | 1 | ✅ | +| M7b | 1 | 1 | ✅ | +| M7c | 1 | 1 | ✅ | +| M7d | 1 | 1 | ✅ | +| M8 | 5 | 5 | ✅ | +| M9 | 14 | 14 | ✅ | +| M10 | 3 | 3 | ✅ | +| M11 | 4 | 4 | ✅ | +| M12pre | 1 | 1 | ✅ | +| M12 | 1 | 1 | ✅ | +| M13 | 1 | 1 | ✅ | +| M13post | 1 | 1 | ✅ | +| M13neutral | 1 | 1 | ✅ | +| M14a–M14e | 1 each | 1 each | ✅ | +| M15a | 1 | 1 | ✅ | +| M15b | 1 | 1 | ✅ | +| M16a | 1 | 1 | ✅ | +| M16b | 1 | 1 | ✅ | +| M17·C1 | 20 *(18 measured + 2 new)* | 20 | ✅ | +| M17·C2 | 3 *(measured)* | 3 | ✅ | +| M17·C3 | 1 *(measured)* | 1 | ✅ | +| M18 | 1 | 1 | ✅ | +| M20 | 1 | 1 | ✅ | +| M20a–M20k | 1 each | 1 each | ✅ | + +**No compile-only result. No passing-outcome mutation** — §3 requires every row +to fail, and every row did. + +### 9.4 Three cells worth their own note + +**M2a, 21, unchanged from its pre-ratification measurement.** §3 warned its proxy +over-approximated for any test observing a rider through the selector, and that +none of the 20 legacy tests was a rider test. Confirmed: the legacy 20 are exactly +the `g3b_measure20_tests` set measured, plus the new discriminator. + +**M17·C1, 20, and `display_renders_each_arm_exactly` is not among them.** That +absence is the receipt for §9.1.2: under the unrepaired C1 fixture it would have +been. + +**M7b, 1.** §3 records that revision L wrongly named +`every_invariant_has_a_negative_generator` here, since that test iterates `all()` +and cannot detect an omission from `all()`. Observed: `graph_invariant_all_is_unchanged` +alone. + +### 9.5 Restoration + +After every row, and after the interrupted-run repair: + +``` +suites=44 passed=1606 failed=0 ignored=0 +cargo +1.95.0 clippy --workspace --all-targets -- -D warnings: clean +``` + +**1586 → 1606, twenty net-new tests**, and 43 → 44 suites: + +| Count | Where | +|---|---| +| 17 | pin 10's eleven-row matrix and its whole-surface tests | +| 1 | pin 3a's `.tex` prose guard | +| 1 | pin 1b's derives guard, in `g3a_tests` | +| 1 | pin 1b's integration test — the new suite | + +--- + +## §10. A sixth fault, found by gate 16 at the last moment + +**Pin 9's `/// 10.` rider note was never migrated.** It is one row of pin 9's +table, and it was the only row left undone — the other eight were verified +individually rather than assumed, which is how this one surfaced. + +The note still read: + +```rust +/// Beyond that surface, further checks are reported under this same tag +/// and are NOT part of the normative invariant 10: tempo-map segment +/// shape, ordering and non-overlap (Chapter 3, +/// `req:time:tempo-segment-order`); ... +/// multiplexing is filed as P13-S29 — the public `check_invariant` +/// filter and this violation's `Display` attribute those failures to +/// invariant 10. Repairing it is a behaviour change, out of scope here. +``` + +**Three statements, all false as of this rung**, and the gate names all three: +the riders are no longer *"reported under this same tag"*; P13-S29 is no longer +their *pending owner* — it is this commit; and the note listed **three** labels +where pin 9 requires **four**, `req:time:tempo-segment-shape` being the one this +rung minted. + +*The missing fourth label is the same defect shape as §9.1.1: a set that grew by +one, and a list that did not.* It is now rewritten to name all four and to say +that `check_invariants` still returns them, so a caller asking *"is this graph +well-formed"* keeps its coverage. + +**Why no test caught it.** Pin 9's prose outcomes have **no machine observer** — +gate 16 says so outright: *"Every one of these can be omitted with all other +gates green."* Eight rows had landed; the ninth had not; nothing in 1606 tests +could tell the difference. + +**Every other pin 9 row was re-verified by its own stale phrase**, not by +assumption: + +| Stale phrase | Found in | +|---|---| +| `surfaced here under invariant 10` | clean | +| `go under invariant 10` | clean | +| `surfaced under an existing` | clean | +| `the compatibility invariant` | clean | +| `tempo-map segment invariants` | clean | +| `all 19 enumerated graph invariants` | clean | +| `reported under this same tag` | **`invariants.rs`** → repaired | +| `filed as P13-S29` | **`invariants.rs`** → repaired | + +*`core_spec.tex:3120` still occurs in `DECISIONS.md` and `accidental.rs`. +Neither is a pin 9 row: pin 9 pins that locator's replacement in the **accidental +header comment** in `invariants.rs`, which is clean, and it explicitly does +**not** rewrite `DECISIONS.md`, which gains a supersession note instead.* + +--- + +## §11. Gate results, 1–16 + +| # | Gate | Result | +|---|---|---| +| 1 | `cargo test --workspace` | **44 suites / 1606 passed / 0 failed / 0 ignored** | +| 2 | clippy `-D warnings` | clean, 0 warnings and 0 errors | +| 3 | `fmt -p epiphany-core -p epiphany-testkit --check` | clean (never `--all`) | +| 4 | staged paths ⊆ §2 rows, all rows staged | 13 paths, 13 rows | +| 5 | `git diff --cached --check` | clean | +| 6 | identifier and field migration | §6 above, verbatim | +| 7 | every §3 mutation observed | §9.3 — 54 rows, all matched | +| 8 | `all()` re-derived at 21; `.tex` count claim unchanged | 21 entries, 21 unique, 21 `number()` arms 1..21, order identical; `core_spec.tex:6746` still reads *"exactly \textbf{21} invariants"* and is absent from the diff | +| 9 | `latexmk -xelatex core_spec` | undefined references cleared on pass 1; `core_spec.pdf` rebuilt | +| 10 | ledger append, removed-plus-added reconstruction | 1 removed / 1 added; `added` ends with `\|`; `strip(added) == strip(removed) + " " + APPEND` **true** | +| 11 | temporary allowlist row absent, two survivors present | `req:time:tempo-segment-shape` absent; `req:layoutir:vertical-bands` and `req:graph:aleatoric-reference-locality` present | +| 12 | `requirement_labels` passes with the row absent | 6 passed, 0 failed | +| 13 | pin 11's inventory | **25 observations: 9 migrated (5 + 4), 16 unchanged**, none deleted, none softened; M16a and M16b prove both negatives non-vacuous | +| 14 | pin 12's lifecycle | status block exactly `STATUS: LANDED by this commit.`, no hash; frozen-pins statement shows **0 hunks** in a zero-context staged diff; revisions A–R marked a dated historical record | +| 15 | placement and Revision History row | shape follows order's `\end{requirement}` with only a `\begin{requirement}` between; the added run equals pin 13's block, whitespace-collapsed | +| 16 | pin 9's prose outcomes | §10 — eight rows verified clean by their own stale phrase, one repaired | + +### 11.1 Gate 10's one-character finding + +The staged ledger append first read `RESOLVED 2026-08-12`; pin 13's `APPEND` is +pinned verbatim as `2026-08-11`. The reconstruction failed on that character +alone, and **the artifact was corrected to the pin, not the pin to the artifact.** + +*Flagged for the owner rather than silently reconciled: the contract's own +ratification line reads 2026-08-12, so the pinned append carries the date the +row was drafted rather than the date the rung resolved. Changing it is an +administrative amendment to pin 13, not an execution decision — gate 10 exists +to make exactly this deviation visible.* diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index af79e49..d4ddd56 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -124,5 +124,5 @@ evidence in isolation. | P13-S26 | **A doc comment in shipped code claims a specification repair that never landed, and the claim is guarded on the code side and nowhere on the specification side.** `crates/epiphany-core/src/invariants.rs:69`–`:71` enumerates invariant 10's four reference classes and states that *“genesis tranche G3a repairs this prose to name what the check body already enforced”*. **It did not.** `core_spec.tex:6570`–`:6572`, the normative enumeration item 10, still reads only *“Every cross-cutting structure's references resolve to extant objects in the graph, except where explicit re-anchoring rules permit transient dangling states during edits”* — naming neither a staff's declared instrument, a staff's group, a staff group's members, a part's staves, a view's active layers, nor any of the meter/time-signature references the Rust doc lists and the check body enforces. The repair landed in the Rust doc comment only. **The asymmetry is the defect's sharp edge:** the Rust doc block is protected by a grep-assert, `t12_invariant_10_doc_comment_names_the_four_reference_classes` (`invariants.rs:4554`, needles at `:4562`–`:4566`), so the side that is *wrong about the other* is the side that is **locked**, while the side that is actually stale is unguarded | this file (found 2026-07-31 during P13-S16 reconnaissance, while verifying that row's invariant-10 citations; no ledger entry covered it) | **open.** **Not a live incorrectness** — the check body is correct and enforces every class; only the normative prose under-describes it, and only the doc comment lies about that. **A P13-S9 instance**, and filed deliberately as one: the loud form (a dangling citation) is caught by `requirement_labels.rs`, and this quiet form — a *true-sounding claim about another document's state* — is caught by nothing. **`invariants.rs:69`–`:71` MUST NOT be “corrected” on its own.** It is currently the only artifact in the tree pointing at the `core_spec.tex` gap; softening the Rust claim in isolation would make the specification defect invisible and convert a caught defect into an uncaught one — which is P13-S9's stated failure mode verbatim. **Repair both sides in one rung**, and consider whether the LaTeX enumeration deserves the grep-assert its Rust mirror already has. **CONTRACT RATIFIED 2026-08-11 — `spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md`, on the authority of the repository owner, after independent whole-artifact passes the last of which returned zero findings; PINS FROZEN, executed not edited.** **DISPATCHED 2026-08-11, and LANDED by the commit carrying this row.** Execution stopped at pin 3 on a defect in a frozen pin — item 10's retained opening sentence is scoped to *cross-cutting structures*, a defined term narrower than the surface pin 1 requires beneath it — which was **reported, not patched**: amendment 1 (`f9170b0`, five review rounds) subordinates a universal to the re-anchoring rules that explicitly permit transient dangling, retains the original sentence verbatim beneath it, and rebuilds M19/M21; amendment 2 (`86bf7c6`) corrects amendment 1's own lifecycle prose, which ratification discharged the prescriptions of but not the surrounding claims. Execution then completed: **38 mutations, 38 matching radii**, evidence in `spec/EVIDENCE_P13S26_EXECUTION.md`. **One finding is open against the landed contract** and is not repaired here: pin 4a claims its requirement guard buys that *"neither referent can silently leave"*, and measurement showed a referent can leave the normative clause while surviving in a recap sentence. That is amendment 3's subject.** **AMENDMENT 3 RATIFIED AND LANDED (`7c8a30d` + the commit carrying this row): the finding is CLOSED, by strengthening the guard rather than softening the claim.** Test 3 now selects the requirement's normative clause — the sentence carrying its sole `\MUST{}` — and runs all four assertions on that slice alone, so a phrase surviving elsewhere in the block no longer counts. Six signing mutations, one per step of the selector, all observed failing with test 3 as their sole radius; evidence appended to `spec/EVIDENCE_P13S26_EXECUTION.md` with the rung's original 38/38 matrix preserved unchanged. `core_spec.tex` was not touched: the requirement's text was always correct, and only the guard was weak. Two of this row's own claims did not survive scoping and are corrected in that contract's §0.1 and §0.2: (1) the doc comment's G3a aside is **ambiguous, not false** — G3a's pin 6 is titled *doc-only* and `6c5e69f` wrote the aside, so "this prose" is self-referential; the row's "claims a specification repair that never landed" reading is **withdrawn**, and with it the "only artifact pointing at the gap" rationale. (2) The two-sided repair stands on a **different** rationale: normative enumeration and doc comment are **incomplete mirrors of each other**, incomplete in different places, so neither may be repaired from the other — the surface is derived from the check bodies instead. The rung also files **P13-S29** (the invariant-10 tag multiplexes Chapter 3/4 failures through a public API) and **P13-S30** (the repository's ad hoc TeX parsers assume exact `\label{`/`\begin{requirement}`/`\end{requirement}`/`\chapter{` spellings TeX does not require) | | P13-S27 | **The reduction-algorithm-version machinery is self-referential, so the one check that would detect a canonical-semantics change necessarily passes.** `core_spec.tex:11614`–`:11617` is normative — *"Snapshots produced under an earlier algorithm version cannot be used as canonical bases under a later one without rebuilding"* — and `:14369`–`:14372` states that replicas at differing versions *"may produce different canonical states from the same operation set."* The machinery to enforce it appears to exist: `ReductionAlgorithmVersion` (`bundle/src/ids.rs:291`) is a superblock wire field (bytes `68..72`, `superblock.rs:20`); `reduction_version_for` (`bundle.rs:989`) sets a new superblock's value; and `open` (`bundle.rs:396`–`:399`) rejects a mismatch. **But the writer sources the value from the canonical base's own self-report** (mapping the base's `reduction_algorithm_version` through `unwrap_or_default()`), **and the reader compares it only against the superblock that value seeded.** Nothing compares either against the semantics the running implementation actually implements. **The check is not vacuous** — it catches a corrupt or tampered base whose version disagrees with its superblock — but it **necessarily passes for a conformingly propagated stale base**, which is precisely the case the requirement exists to prevent. Supporting: **no constant or accessor anywhere names the implementation's current reduction semantics**, and `ids.rs:288`–`:289` states that *"the algorithm catalog itself lives in `epiphany-ops`"* while nothing of the kind exists in that crate — **a second instance of P13-S26's pattern**, a doc comment asserting a false fact about another module | `spec/CONTRACT_P13S16_PROJECTION.md` pin 0 (found 2026-07-31 while scoping P13-S16, which is a canonical reduction-semantics change and therefore the first rung to need this guarantee; filed in the same ledger edit as the row it blocks) | **UNBLOCKED 2026-08-07 — the format-epoch rung landed; dispatchable, and still blocking P13-S16.** (Was: open, BLOCKED on P13-S28.) **Scoped 2026-07-31 as `spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md` (DRAFT, not dispatchable).** Rulings taken: a typed `BundleCapabilities` required at both `Bundle::open` and `Bundle::create` and carried on the `Bundle` — no default, so every caller states the semantics it implements — and outright rejection on mismatch via a new `CanonicalBaseRequiresRebuild` error, not read-only and not an integrity anomaly. Storing the capability keeps all 57 `commit` sites unchanged; only `open` (57 sites) and `create` (32) move. **The scoping also falsified this row's first reading that the writer path was test-only:** `epiphany-textproj`'s `serialize_document` (`serialize.rs:119`) and `project.rs:936` are production paths that copy a base's `reduction_algorithm_version` verbatim into a fresh `SnapshotRef`, which `commit_versioned` then stamps into the superblock (`bundle.rs:798`) — so production mints self-consistent stale documents **without ever calling `open`**, and the capability must govern writers too. **What blocks it:** contract pin 2a. Baseline authority `0` does not preserve the corpus (`serialize.rs:327` stamps `1` and round-trips it; `vectors.rs:353`/`:363` likewise), and once P13-S16 moves the authority to `1`, a pre-S27 base that happens to carry `1` is **indistinguishable from a legitimately rebuilt one** — a raw `u32` carries no provenance. Four dispositions are recorded there; `FORMAT_MINOR` as a provenance carrier was proposed and **rejected** (the header never changes after creation, `core_spec.tex:10799`, so a legacy bundle committing a freshly validated base keeps its old minor forever; and a minor change may only append append-safe discriminants, `:12258`, not alter acceptance semantics). The surviving requirement — provenance must ride a container property **old readers cannot silently accept** and **a later commit cannot inherit unchanged** — is a format-epoch design, filed as **P13-S28**. **Scope of the claim, deliberately narrow:** this establishes that the **current implementation** has no detection mechanism. It does **not** establish that no reduction-semantics change in the project's history was ever detectable — that needs a history audit not yet done, and the stronger sentence is deliberately not written here. **What closing it requires:** an authority naming the semantics this build implements, and a rejection-or-rebuild path when a base disagrees with it. Until then any rung changing canonical reduction semantics can record its break in prose but cannot make stale bases unusable — which is why P13-S16's contract is complete, ratifiable as a plan, and **not dispatchable**. **Method note:** an earlier draft of S16's pin 0 claimed no writer path existed at all. That was false, and the way it was false is the point — the search behind it looked for `ReductionAlgorithmVersion(` constructor calls, which cannot find a path that propagates an existing value without constructing one. The instrument could not observe the thing it was used to rule out. **UNBLOCKED 2026-08-07:** the format-epoch rung landed and its pin 8 **resolves pin 2a** — reduction-version authority is meaningful only in major-1 containers, so legacy bases are refused by container epoch and never by version arithmetic. The collision pin 2a identified never has to be adjudicated: a pre-S27 base carrying `1` and a rebuilt S16 base carrying `1` are indistinguishable as numbers but can never meet, because the former exists only in a major-0 container, refused at the epoch boundary before any version is compared. The `u32` never has to carry provenance because the container does. **S27 now additionally owes three inherited items** (both interim refusals converted to validation, M8's deferred laundering demonstration, pin 3c's two suspended conformance assertions), recorded in its contract as required tests. **~~RATIFIED 2026-08-07 after review round 1~~ — RATIFICATION WITHDRAWN 2026-08-07, see round 2 below. **RATIFIED 2026-08-08 on the repository owner's authority, after NINETEEN adversarial review rounds the last of which returned zero findings. PINS FROZEN — executed, not edited; a defect found during execution is reported, not patched in place. DISPATCHED for execution, with the work to be left STAGED and the execution report subject to INDEPENDENT REVIEW before completion is accepted, covering in particular M7's three observations and its control. Not settled by ratification: M7's authority/base leg is unverifiable until this rung is implemented, and every gate, test and mutation is specified while none has been run.** Prior status through the review: NOT RATIFIED, NOT DISPATCHABLE, pins NOT frozen, **awaiting the next independent review round. Which rounds have closed and the running tally live in the contract's own history table and are deliberately NOT restated here — this clause carried a count through two rounds and went stale in both, and the round list went stale the same way**; no execution work may begin.** Round 1 was run because this contract had reached "dispatchable" with **zero** ratification rounds on record, against the standing rule that contracts go through adversarial review before dispatch. Round 1 returned **nine findings, four blocking**, all now carried in the contract. **Correcting this row's own preceding clause:** the three inherited items were *not* all "recorded as required tests" — obligation 2, M8's laundering demonstration, appeared in **neither** the contract's test section nor its mutation plan, while that section's preamble claimed all of them were tests. It is now **M7**, and ruled a **mutation** rather than a capability restoration: the format rung's text refusal is permanent, `COMPANION_VERSION` stays 0.14.0, and the text-projection corpus keeps `canonical_bases` reach 0. The other blocking three: §0.4's `commit`-site count counted a same-named method in `epiphany-editor-core`, **a crate with no `epiphany-bundle` dependency at all** — the third instrument failure recorded in that one section; three independent stale list-counts (the test-section header, gate 1, and three report items) all naming figures the document had outgrown; and `testkit/tests/requirement_labels.rs` missing from the touch table while pin 9 may move `CORE_REQUIREMENT_COUNT` 213 → 214 — **the escapee `CLAUDE.md` names by name**, which also escaped the format-epoch rung. Non-blocking: locator drift since `381c498` (`bc06706` grew `bundle.rs` by 338 lines; pin 5's own `:396`–`:399` confirmed unmoved), pin 2a's corpus evidence superseded by the 2 → 0 rebuild, `Bundle::open(` 57 → **60**, gate 6a's scope widened to `epiphany-testkit`, and a missing **commit-side positive** test now added as test 8. **REVIEW ROUND 2, 2026-08-07, against the frozen contract: six further findings, four blocking — and round 1's ratification was therefore premature.** (1) The call-site correction had been applied to §0.4 only, leaving the "Rung type" paragraph at **57** and touch row 2 claiming `bundle.rs` has **35** opens — a figure that was never `bundle.rs` alone and is stale besides — which made the required reconciliation impossible. (2) §0.4 called `project.rs:936` a **production** bundle writer; `#[cfg(test)]` starts at `:630` and every `Bundle` call in that file is below it, so the writer-path correction stands on `serialize.rs` alone. (3) **M5 was unexecutable**: `serialize_document` refuses bases at `serialize.rs:151`, so its output is base-free, and pin 5 with test 4 require base-free bundles to open at *any* authority — split into **M5a**/**M5b**. (4) **M6's second half was unexecutable**: `open` rejects a stale base, `create` rejects a base-bearing manifest (`bundle.rs:234`), and `commit` validates what it emits, so no caller can hold an open `Bundle` with a stale *inherited* base — replaced by broadening rather than narrowing, with the unreachability itself reported as the stronger result. Non-blocking: pin 3a's justification (*"production code mints a self-consistent stale document"*) is **false in-tree** — zero production paths stage a base — so it now rests on guarding the public `commit_versioned` API; and `serialize.rs:157` is dead code orphaned by the `:151` guard, recorded and explicitly **not** repaired here. **Two of round 2's findings were introduced by round 1** — ruling M7's refusal permanent is what made M5 unexecutable, and test 8 was added without re-deriving M6 against the same reachability. **Method note: an amendment is a change to the system, not a patch to a line**; a round must re-derive every mutation against every ruling the previous round made. **Round 3 is warranted before dispatch — the defect rate has not fallen (9, then 6), and "dispatchable" is a claim requiring evidence of convergence rather than a status reached by running out of findings.** **REVIEW ROUND 3, 2026-08-07, INDEPENDENT, against `b842975`: six findings, four blocking — and every blocking finding was a defect in text rounds 1 and 2 wrote.** (1) **Pin 3a still carried the rationale round 2 retracted** — §0.4 states there is no in-tree production base writer while pin 3a still said "§0.4 shows production code minting a stale document", so the contract asserted a claim and its negation; **the third occurrence of fix-one-site-leave-the-others**. Rewritten onto the footing that survives: `commit`/`commit_versioned` are **public API** and guard out-of-tree callers, not an in-tree path. (2) **M5a had no observation mechanism** — pin 3 required the capability be *stored* and nothing exposed it; `Bundle` carries 17 public accessors and none for capabilities, so no `epiphany-textproj` test could inspect it. **`Bundle::capabilities()` is now pinned** — new scope, flagged for round 4. (3) **M5b could not fail**: if the supplied capability and the base version both derive from `CURRENT_REDUCTION_ALGORITHM_VERSION` — the natural implementation, since `roundtrip.rs:367` currently hardcodes `ReductionAlgorithmVersion(0)` — both operands move together and the comparison passes for every value. **This is §0.1's own tautology reproduced inside the mutation built to detect it.** The base version must now come from a source that does not track the authority (persisted artifact or deliberate literal), with both operands' provenance reported. (4) **M6's replacement named a scenario with no test** — test 6 stops at opening, so nothing asserted that an unrelated commit *succeeds*, and an implementation rejecting every post-base commit passed tests 2/5/6/8 while the broadening had nothing to break; **test 9 added**. Cleanup: touch row 7 listed `generators.rs` as "call sites, real authority" though it has **zero** `Bundle::open`/`create` calls and its `rng.range(0, 8)` versions are precisely the arbitrary wire values pin 3b assigns to *synthetic* capabilities — split to **row 7a**; and §7's call-site attribution credited round 1 alone where rounds 1 and 2 are both load-bearing. **The pattern is now legible and it is not about counts: three separate mutations were unrunnable in three different ways — M5a could not observe, M5b could not fail, M6 had nothing to break. §7 item 4a now requires, for every mutation, the named test it breaks and the provenance of each operand.** **Defect rate across three rounds: 9, 6, 6 — not converging.** The newest text (pin 3's accessor, M5a, M5b, test 9, row 7a) has had **zero** adversarial passes and was written by the same agent whose previous two attempts round 3 falsified. **REVIEW ROUND 4, 2026-08-07, INDEPENDENT, against `53292f6`: five findings, four blocking.** It accepted pin 3's `capabilities()` accessor as **bounded** — the first new text any round has passed — and found the M5 pair defective a third time. (1) **M5b cited the wrong value**: `roundtrip.rs:367` sits in `assert_score_serialization_stable` (`:332`) and versions an **acceleration snapshot**, not a canonical base, while `assert_reduction_serialization_stable` has **no base at all** because pin 3c suspended it — so the value round 3 warned the implementer not to touch was irrelevant to the authority check. **The tautology diagnosis stands; only its evidence was wrong.** (2) **The instrument was left unchosen** — round 3 said "the rung picks one" and offered two, one of which does not exist for the nominated crate, since `craft_image_with_base` is a private `fn` inside `epiphany-bundle`'s `#[cfg(test)]` module (`:1648`). **Now chosen: commit-then-reopen through public API only** — build with `synthetic_for_fixture(0)`, commit a base carrying the literal `0`, reopen those bytes under the real constant. (3) **No test could assert the error fields**: `assert_reduction_serialization_stable` returns `()` and reopens with `.expect` (`:292`), so a mismatch panics rather than yielding a matchable `CanonicalBaseRequiresRebuild { base, current }`. **Test 10b added.** (4) **M5a violated §7 item 4a, the rule round 3 added in the same edit** — it named no test, and its natural assertion compares the constant with itself and cannot fail. **Test 10a added, asserting against a deliberate literal.** **Round 3's error is the one to carry: it grepped `ReductionAlgorithmVersion`, saw a `roundtrip.rs` hit, and attributed it without resolving the enclosing item — the same shape as §0.4's `.commit(` miscount that round 1 had already recorded as a lesson. Recording a defect is not the same as not committing it.** Both literals in tests 10a/10b are **load-bearing as literals**; §7 item 4b now requires confirming neither was tidied into the constant, a failure mode invisible to the suite. **Defect rate: 9, 6, 6, 5 — still not converging after four rounds, and every blocking finding in rounds 3 and 4 was in text written to fix the previous round.** **REVIEW ROUND 5, 2026-08-08, INDEPENDENT, against `df9e528`: four findings, two blocking — the first round in which blocking findings fell below four.** (1) **The status history was numerically stale again** — "amended three times … fifteen findings so far, eight blocking" were the round-2 figures, left standing through rounds 3 and 4 **while the tables recording those very rounds sat directly below them**. This is the **fifth** count-staleness defect in five rounds, and it was in the one block the author edited every round. Replaced with a **table**, so a round appends a row rather than requiring a number to be found and re-derived. (2) **Test 10b could not make the two-field assertion M5b requires**: §3 said only "assert it opens", and under mutation that yields a bare `Err` or a panic — **a `#[test] -> Result` that returns `Err` asserts nothing about that error's fields**, so M5b's required observation had no home in the test M5b names. Both `Result` arms are now pinned, plus a third for the wrong-error case, so the mutation run produces a *verified* observation rather than a stack trace. Smaller: **M5b's "cannot be tidied" claim was false** — keeping `synthetic_for_fixture` while passing `CURRENT_REDUCTION_ALGORITHM_VERSION` as both its argument and the base version preserves the fixture and fully restores the tautology, so the structure does not protect itself and the real protection is §7 item 4b; round 4 asserted a structural guarantee that undercut the procedural check actually doing the work, **which is the same error as reasoning that a mutation would fail instead of running it**. And §3's preamble still said the tests were "in `epiphany-bundle`" after round 4 added two that **cannot** be, since `epiphany-bundle` must not depend on `epiphany-ops` and reaching the real authority is their entire purpose — corrected, with each test's touch-table home named. **Blocking findings by round: 4, 4, 4, 4, 2 — the first movement in four rounds and the first weak evidence of convergence, set against the fact that every round since the third has found blocking defects in text written to fix its predecessor.** **REVIEW ROUND 6, 2026-08-08, INDEPENDENT, against `03c85dd`: three findings, ALL THREE BLOCKING, and all three in text round 5 wrote.** (1) **The amendment tally went stale inside the block round 5 restructured to prevent exactly that** — round 5 turned the review totals into a table and left "amended five times … rounds 1–4" as prose immediately above it. The amendment count is now **the number of rows**, with no separate figure to go stale. (2) **§3's test-home correction was itself false**: round 5 wrote "tests 1–9 in `epiphany-bundle`", but **test 7 *is* `assert_reduction_serialization_stable`**, which the same section names as `testkit/src/roundtrip.rs`. Two wrong versions of that sentence, both written while fixing it; replaced with a per-crate table (1–6/8/9 bundle, 7 and 10b testkit, 10a textproj). (3) **§7 item 4b protected one operand where test 10b has two** — replacing **both** `synthetic_for_fixture(0)` **and** the committed base's `ReductionAlgorithmVersion(0)` with the constant **keeps the synthetic call in place** and fully restores the tautology, and **test 10b's `Err` arm never executes in the unmutated run**, so its literal cannot detect it. Item 4b now enumerates all **three** fixture operands individually and requires each quoted verbatim. **All three findings are one defect in different clothes: a fix applied to the site named rather than to every site the claim covers** — the sixth count-staleness defect in six rounds and the third range-correction that did not check its own range. **The mechanism that works is structural, not vigilant: the review totals stopped going stale when they became a table, the amendment count did not because it stayed prose, and item 4b stopped being under-specified when it became a table.** **Demonstrated a seventh time inside round 6's own amendment**, where the new table's Total row was first written "6 amendments" — a free-standing count, three paragraphs after the sentence declaring no such count exists, and already wrong at seven rows; caught before commit and replaced with "one amendment per row". **Prose invites a number and a table does not; the defence must be the shape of the artifact, not the attention of the editor.** **REVIEW ROUND 7, 2026-08-08, INDEPENDENT, against `c0d896c`: three findings, all blocking, and all three the same defect — a claim living in two places and fixed in one.** (1) **§7 item 4a was unsatisfiable**: it required every mutation to name "the test it breaks", while item 1 four paragraphs above states that **M4 is observed to *compile*** (no test is possible — that is why pin 3's prohibition is a review rule) and **M7's expected outcome is *success***. A report obeying 4a literally could not be written, and the honest response would have been to invent a test. 4a is now a table of what each of the eight mutations owes, with M4 and M7 carved out explicitly. (2) **Round 6's three-literal correction reached §7 and not §3** — §3 still said "**both** literals … tidying **either**", so the contract carried the fixed and the broken version of the same claim, reopening exactly the narrow-scope ambiguity round 6 existed to close. §3 no longer states the count at all; it points at item 4b. (3) **"Rounds 3, 4 and 5 were independent"** went stale the instant round 6 closed, sitting in prose beside the table whose own column records it. Deleted. **Three rounds, one lesson: round 5 fixed the review totals and not the amendment tally beside them, round 6 fixed item 4b and not §3's copy of the same rule, round 7 found the classification sentence duplicating the table's column. The defect is duplication, and every previous remedy was vigilance — "check the other sites too" — which has now failed three rounds running. The remedy adopted here is deletion, not diligence: where a claim had two homes, one is removed and replaced with a pointer. A copy that cannot drift is one that does not exist.** **Findings by round: 9, 6, 6, 5, 4, 3, 3 — flattened rather than still falling. Blocking: 4, 4, 4, 4, 2, 3, 3 — rounds 6 and 7 were both 100% blocking and 100% in the previous round's text. Seven consecutive rounds, no clean round yet. The deduplication is the first structural remedy for this particular defect and therefore the first with a reason to work, but it is untested.** **REVIEW ROUND 8, 2026-08-08, INDEPENDENT, against `9829ae3`: two findings, both blocking — and the first round to reach into a mutation's mechanics rather than its bookkeeping.** (1) **M7 did not describe a runnable observation.** It instructed execution to *construct* a base-bearing `TextDocument`, which **bypasses `parse_document` entirely**, so the parser refusal it ordered removed was irrelevant and the demonstration was not the **import** laundering it is named for; `project_text_document` is the **export** direction (`&TextDocument -> Result`) and is not on the path at all, so "all three sides, since removing one leaves the others refusing and the document never reaches the writer" was simply false for it; and "byte-indistinguishable from one whose base was genuinely validated" named **no comparison artifact and no comparison method**, leaving the central claim a conclusion rather than an observation. Now: the input must be **text and must be parsed**; only the parser (`parse.rs:138`–`:147`) and serializer (`serialize.rs:151`) refusals are removed and restored; the comparison artifact is **test 10b's construction** with the same `FileUuid` and base bytes; and the comparison is a **field-by-field enumeration** of the `canonical_base` `SnapshotRef`, the superblock's reduction version and the header's major/epoch, **reported rather than concluded** — informative in both directions, since a field that *does* differ is a provenance signal nobody knew existed. (2) The round-7 deduplication was incomplete: the status block still carried "rounds 3 and 4 are closed" while declaring the history table the sole authority. **Finding 1 is the most substantive of any round, because every earlier one was about text agreeing with other text — this one is about whether the experiment runs at all, and it did not. M7 had been in the contract since round 1 and survived seven reviews, three of which specifically re-derived mutations, because reading it never required tracing what calls what. An observation stated in the right register can look complete for a long time; "indistinguishable" was a conclusion sitting inside the rung's own demonstration, which is the exact failure mode this rung exists to eliminate.** **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2. Blocking: 4, 4, 4, 4, 2, 3, 3, 2. Eight rounds, none clean. While amending, the author caught a third instance unaided — §7 item 4a's M7 row still said "all three refusals" — which is weak evidence the deduplication rule is being applied rather than merely stated. The M7 rewrite is now the newest and least-reviewed material in the contract, and its predecessor survived seven rounds while being unrunnable.** **REVIEW ROUND 9, 2026-08-08, INDEPENDENT, against `01e76d1`: two findings, both blocking, both in M7's comparator — the text round 8 had just rewritten.** (1) **Test 10b is not the "genuinely validated" reference M7 nominated**: its write-side capability is `synthetic_for_fixture(0)` and only its *reopen* uses the real authority, so M7 would have compared one synthetic fixture against another with the validated half of the claim simply absent. **This is a collision between two of the contract's own designs, not a typo** — round 4 made 10b synthetic-on-write *deliberately* so M5b's operands would be provably independent, and that is exactly what disqualifies it here. **One artifact cannot be both independent of the real authority and committed under it.** M7 now builds its own reference in `epiphany-testkit`, committing a base under `caps` derived from the real constant so pin 3a validates it on the way in. (2) **The field enumeration could not support its conclusion**: it claimed "everything that could carry provenance" while omitting `FixedHeader.file_uuid` — **the field it required to match** — plus the superblock's `generation`, `manifest_offset`, `manifest_length` and `manifest_hash`, and the whole manifest outside `canonical_base`. Replaced with **whole-`image()` byte comparison**, any difference enumerated and classified as justified nondeterminism (normalize, stating why) or as a **provenance signal** (a finding, since the refusal may then be stronger than needed). **Finding 2 retires a technique rather than an instance: a hand-written list of "every field" is a claim about a struct's contents that is wrong the moment the struct changes, and this one was wrong the day it was written. Comparing the whole artifact cannot be incomplete — the tables-over-numbers lesson applied to the experiment instead of the prose.** Three further sites were caught by the author while amending: §7 item 6 still said "M7's three text refusals", surviving round 8's correction of that exact count in two other places; §7 item 4a's M7 row still named the superseded method; and round 8's own disposition cell stated it as current. **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2. Nine rounds, none clean. Rounds 8 and 9 both found defects in the immediately preceding round's rewrite of the same paragraph, so M7 has now been wrong in three distinct ways across three consecutive rounds — unrunnable, then wrong-artifact, then wrong-method. The comparator is on its third design and has never been executed.** **REVIEW ROUND 10, 2026-08-08, INDEPENDENT, against `0efd543`: one finding, blocking — the smallest round yet, and again in M7.** **The whole-image comparison had no complete construction alignment.** Round 9 named four things to align, but `serialize_document` also fixes `document_id`, `lineage_id`, `profile_declarations`, every extension's fields and preserved chunks, the envelope payloads, the **staging order** (base root → extension chunks → operation-envelope block), the manifest schema `major` and `epoch_max`, and every chunk ref, hash and offset derived from those. **So a byte difference would have had a third possible cause — "the reference was built differently" — which is neither permitted classification; the result would have been unclassifiable and the comparison meaningless. A result that cannot be classified is not an observation.** M7 is now a **round trip**: build `B` validated under the real authority, export it to text via `document_from_bundle` + the crate-private `render_text_document`, parse that text back, re-serialize as `A` with `B`'s `FileUuid`, and compare whole images. **Alignment is inherited rather than enumerated** — every input `serialize_document` reads is already `B`'s own, so no list can be incomplete and the setup-mismatch category is eliminated by construction rather than by care. It is also the realistic form of the threat: export a validated document to text, re-import it, and observe the re-imported container is indistinguishable from the original having validated only the base's number, never its provenance. **This was the third hand-enumerated "complete set" in this contract and the third wrong on the day it was written — "every field that could carry provenance" (round 8), "every field to align" (round 9), and round 9's list again. The single rule earned across rounds 5–10: where a claim requires completeness, do not enumerate, derive. Tables instead of counts, whole artifacts instead of field lists, one shared origin instead of an alignment list.** No refusal count is stated anywhere in M7 any more; three successive wordings each had a wrong one. **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1. Ten rounds, none clean, and three consecutive rounds have found one paragraph — M7 — defective in a new way each time: unrunnable, wrong artifact, wrong method, incomplete alignment. Findings are falling steadily and each of the last three has been narrower than the last, the first sustained convergence signal here. Against that: M7 has never been executed and each of its four designs looked correct when written — the open question for round 11 is whether the next defect is findable by reading at all, or whether M7 must be run against a scratch branch before further paper review can add anything.** **BOUNDED SCRATCH PROBE, 2026-08-08, authorised as an explicit narrow exception in the contract's status block and run on a discarded branch: it FALSIFIED round 10.** First, recorded as evidence in its own right: **M7 cannot be executed at all until S27 lands** — `BundleCapabilities` and `CURRENT_REDUCTION_ALGORITHM_VERSION` do not exist in the tree, being S27's own deliverables, and M7 step 1 needs a base committed under the real authority. M7 is a mutation *of this rung's implementation*, so it runs after the rung. The probe therefore tested the round-trip machinery M7 depends on, base-free — which removes **no** refusal, since both `project_text_document` and `serialize_document` gate on `canonical_base.is_some()`, leaving §1.2 untouched. **Result: the round trip is byte-preserving, but only from a fixed point, and round 10's comparison did not compare from one.** Round 10 compared `A` against a `B` built from the *input* document, which is valid only when that document is already a fixed point of `document_from_bundle ∘ serialize_document`. `minimal_document(42)` happens to be one — so the first probe **passed**, and would have been reported as success — while `minimal_document(99)` was not, and the **one-extension case diverged by 295 bytes from offset 352**. Rebuilt from the fixed point, all three cases are byte-identical (1641 / 1800 / 1894). **The non-idempotent field is `envelopes`, not extensions:** diagnosed field-by-field, `document_id`, `manifest_schema_version`, `lineage_id`, `profiles`, `canonical_base`, `blobs` and `extensions` — including every `TextChunk` payload — survive exactly, while `document_from_bundle` applies a **canonical envelope ordering** (its own test says so), so any other arrival order is not a fixed point and its operation-block bytes differ. **`project_text_document` → `parse_document` proved LOSSLESS** (`b_doc == d` in every case) — the text leg was never the problem; the defect was entirely in which artifact round 10 chose as reference. **What M7 must add, for round 11 to ratify rather than for the probe to assume: an explicit fixed-point normalisation and assertion before any byte comparison, because otherwise a mismatch is round 10's own unclassifiable "third category".** Probe hygiene: the comparison was **mutation-verified** — a different `FileUuid` for `A` produced 20 differing bytes at offsets 32–47 and 60–63, observed, then restored by hand-editing, incidentally confirming round 9's point that `FixedHeader.file_uuid` is byte-visible and round 8's enumeration had omitted it; one file touched, 142 insertions, all inside `#[cfg(test)]`; no refusal removed; no canonical base carried; diff captured, branch deleted. **The methodological result: four paper rounds refined this comparison and none found that it silently depended on an unstated precondition. One execution found it in minutes, via the case a reviewer would least likely hand-pick — a document with an extension. Had the probe stopped at the case round 10 implied, the contract would have been ratified on a comparison that fails for most documents.** **REVIEW ROUND 11, 2026-08-08, INDEPENDENT, against `39f2617` (post-probe): three findings, two blocking. It confirmed the probe contained and its fixed-point result decisive, and kept M7 BLOCKED.** (1) **M7 still lacked a distinct normalised reference.** Round 10 named one artifact where the comparison needs two: build **`B_raw`** under the real authority, then **iterate derive-and-reserialize until `B_fixed` is a byte-level fixed point**, **assert that property explicitly as a hard failure**, and **compare the imported artifact only with `B_fixed`, never with `B_raw`** — otherwise an envelope-order normalisation difference remains **indistinguishable from a provenance result**, and a comparison whose failure mode cannot be told from its success condition decides nothing. Steps 1a–1c added, including a bounded convergence loop (the probe saw one pass suffice for three documents, which is not proof that one pass always suffices) and a required report of the iteration count and whether `B_raw` was already fixed. (2) **The claim was stated more broadly than any observation supports.** M7 read as though every direct bundle is byte-identical to its re-imported form; it is not, and the probe measured 295 differing bytes proving so. The contract now scopes it: M7 proves **the text path carries no provenance marker *after normalisation***, and explicitly **not** that every direct bundle is byte-identical before it — the pre-normalisation differences are `document_from_bundle`'s canonical envelope ordering and have nothing to do with provenance. **Both sentences must appear in the rung's report.** **This finding has consequences beyond M7: its conclusion is the sole evidence for a permanent capability loss — the text refusal that moved `COMPANION_VERSION` to 0.14.0 and took the corpus's `canonical_bases` from 2 to 0 — so justifying a permanent refusal from a claim broader than the result obtained is the same error as concluding instead of observing, one level up: not a false observation, but a true one asked to carry more than it can.** (3) Clarification rather than defect: **the probe cannot pre-verify M7's authority/base leg**, which needs `BundleCapabilities`, `capabilities()` and pin 3a's validation — S27's own deliverables — so it remains an **execution requirement after S27 implementation**, with the probe standing as evidence for the prerequisite and explicitly **not** as a demonstration of laundering, since it carried no base. Recorded as a standing prerequisite table: the round-trip leg is settled, the authority leg is not pre-verifiable by any review or probe. **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1, 3. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1, 2. Eleven rounds, none clean. Round 11 broke the falling trend, and did so because the probe supplied evidence that made a previously invisible defect findable — a reason to expect the next round to find more rather than less. The M7 comparator is on its fifth design: four were falsified by reading, the fifth by execution and then rebuilt on that evidence. It is the first with a measured result behind it and the first whose precondition is asserted rather than assumed, and it still cannot be executed end to end until S27 is implemented.** **REVIEW ROUND 12, 2026-08-08, INDEPENDENT, against `74dc994`: two findings, both blocking, and both the same defect — a requirement stated without the decision it requires, leaving execution to make a design choice silently.** (1) **The convergence loop was not actually bounded**: it demanded a bound and named no limit, so execution would have chosen when non-convergence becomes failure, changing what the experiment means. **Now pinned at one normalising step** — with `B₀ = B_raw` and `B₍ₙ₊₁₎ = serialize_document(document_from_bundle(Bₙ), uuid)`, compute at most `B₁` and `B₂`, permitted maximum `n = 1`, with a three-row outcome table (`B₁ == B₀` → already fixed; `B₁ != B₀` and `B₂ == B₁` → `n = 1`, the expected case; **`B₂ != B₁` → HARD FAILURE**, reporting all three image lengths and the first differing offset). **The bound is one step because it is a property, not a tolerance:** `document_from_bundle` canonicalises, so `serialize_document ∘ document_from_bundle` must reach its canonical form in a single application, and if it does not there is **no canonical form**, no principled reference artifact, and **M7 is invalid as a whole** — a finding about the projection rather than a signal to iterate further. A loop that runs until it happens to settle tests nothing; it reports how long it took. Raising the bound needs its own amendment and review round. (2) **M7's location was unchosen**: "in a crate that can reach the real constant" is true of two crates and decisive for neither, and `render_text_document` is **`pub(crate)` to `epiphany-textproj`** (`project.rs:595`), so `epiphany-testkit` could host M7 only via **an unpinned visibility change to another crate's public API**. **The harness is now pinned to `epiphany-textproj`**, which alone has both the renderer and (via its `epiphany-ops` dependency) the real constant — under **existing touch row 9**, no new row. **`render_text_document` stays `pub(crate)`:** handoff §1.3 records it as *the one intentional hole* in the text refusal, existing solely so a negative vector can carry the spelling it asserts is refused, and widening it to host a mutation that gets reverted would leave a permanently widened public surface behind — which is how a temporary harness becomes an API change nobody ratified. **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1, 3, 2. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1, 2, 2. Twelve rounds, none clean. The last two rounds found the same kind of defect — a requirement that reads as a decision but is not one — so the next scan should hunt remaining instructions that name a constraint without naming its value. Everything M7 now specifies is pinned to a number, a crate or a named artifact, which is a checkable property a round can test directly.** **REVIEW ROUND 13, 2026-08-08, INDEPENDENT, against `bff9c9a`: one finding, blocking — and it inverted M7's result.** **M7 claimed the capability check "does not fire".** Pin 3a requires `commit`/`commit_versioned` to validate a **newly emitted** canonical base, which is exactly what **both** `B_raw` and the parsed `A` commit — so **the check fires on both paths and ACCEPTS**, because the raw version equals the real authority. **That acceptance is the laundering result:** the base is not slipped past an absent check, it is admitted by a check working correctly that cannot tell a coincidence from a rebuild. **As written, M7 was satisfiable by deleting pin 3a's writer check entirely** — yielding a passing M7 that demonstrated the exact opposite of its purpose. M7 now requires **three observations** (`A.image()` equals `B_fixed.image()`; pin 3a's validation ran and accepted on both commits; and the control) plus a **required control**: in the same run, same harness, repeat the import with a base version deliberately **not** equal to the real authority and observe the commit **REJECTED** with `CanonicalBaseRequiresRebuild`. **M7's removals are now explicitly limited to the text refusals — pin 3a is not among them and may not be weakened, being the thing under observation rather than an obstacle to it.** **This is a new failure shape worth naming: an observation satisfiable by the absence of the thing it observes.** M7's earlier defects were about being unrunnable or comparing the wrong artifacts; this one would have run, passed and reported success on a tree with the writer check removed. **"The check does not fire" cannot distinguish a check that accepts from a check that is not there, and only one of those is the finding.** **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1, 3, 2, 1. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1, 2, 2, 1. Thirteen rounds, none clean. Round 13 is the narrowest since the probe, but it found a defect of a kind no earlier round had looked for — not "can this run?" or "does this compare the right things?" but "could this pass for the wrong reason?" — and that question has NOT been asked of M1–M6, M5a or M5b. Every mutation in §4 deserves the same check: what else, besides the intended defect, would make it pass?** **REVIEW ROUND 14, 2026-08-08, INDEPENDENT, against `f579172`: one finding, blocking — a contradiction round 13 created.** **The comparison method still said equal images "complete the observation and require nothing further"** — written in round 9, when byte equality *was* the whole of M7, and not swept when round 13 added the writer-check control. **The contract therefore simultaneously required the control and licensed omitting it, with the permissive sentence sitting earlier and reading as the summary.** Equality is now **necessary but not sufficient**: observation 1 of three, with the control still required, and that paragraph now specifies *how to compare*, never *what suffices*. **A second instance was found while amending, and round 14 reported none:** the "informative in both directions" note read *"if **every field matches**, the refusal is justified"* — the same sufficiency claim in different words, still carrying round 8's *"every field"* vocabulary that round 9 had replaced with whole-image comparison. **A search for "nothing further" or "sufficient" cannot reach a sentence that says "matches"** — the defect `CLAUDE.md` names, *searching one spelling and concluding about all sites*, met inside the fix for a sweep failure; neither the reviewer's search nor the author's first search found it, and a third pass on different terms did. **The round-13 lesson generalises further than round 13 stated: it is not only that a requirement must be swept to every site, but that the permissive statement usually reads *earlier* than the restrictive one, because requirements accumulate downward as a document is amended. A reader following the document in order stops at the first sentence that says "done". Where a later round narrows what suffices, the earlier summary is the site most likely to contradict it and least likely to be searched.** **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1, 3, 2, 1, 1. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1, 2, 2, 1, 1. Fourteen rounds, none clean — but the last two are single-finding rounds and round 14's was created by round 13 rather than pre-existing, the narrowest the defect stream has been. Against that, round 13's question — what else, besides the intended defect, would make this pass? — has still not been asked of M1–M6, M5a or M5b, and round 14 did not ask it either. That scan remains outstanding and is the largest known unexamined surface.** **REVIEW ROUND 15, 2026-08-08, INDEPENDENT, against `fa483cf`: one finding, blocking — and it ran the scan rounds 13 and 14 left outstanding.** **M6 accepted "test 5 fails" and "test 9 fails" as its observations.** A test fails for **every** reason, not only the one under test, so an unrelated writer rejection satisfies both exactly as well as the intended cause — M6 could have reported success while demonstrating nothing about pin 3a's scope. Both halves now require the **mutated outcome itself**: after removing pin 3a, test 5's stale commit must be observed to **SUCCEED** and the bundle to reopen at the new generation with the stale base present; after broadening pin 3a, test 9's otherwise-unchanged commit — one that does not touch `canonical_base` — must be observed **rejected specifically by the broadened writer rule**, named in the report, not merely erroring. **The scan is now complete: M1–M5b survive it, M6 did not.** That the one remaining instance was in M6 — the mutation twice rewritten for unexecutability — is worth noting: **a mutation can be made runnable and still not be evidential.** **The principle, stated once so it need not be rediscovered: the evidence a mutation owes is the behaviour it changed, not the assertion it broke. A broken assertion is a symptom with many possible causes; the changed behaviour has one. Every mutation in §4 now names an outcome, not a failure.** **Findings by round: 9, 6, 6, 5, 4, 3, 3, 2, 2, 1, 3, 2, 1, 1, 1. Blocking: 4, 4, 4, 4, 2, 3, 3, 2, 2, 1, 2, 2, 1, 1, 1. Fifteen rounds, none returning zero — but what changed in the last three is the character of the findings, not only the count: round 13 found a defect of a kind never looked for, round 14 found a contradiction round 13 created, and round 15 found the last instance of round 13's kind with the scan reported complete across every mutation. The known unexamined surfaces are now enumerable, which they were not before: §4 is scanned and clean, and M7's authority/base leg remains unverifiable until S27 is implemented by construction, carried as an execution requirement rather than a gap in the document.** **ROUNDS 16–19, 2026-08-08, recorded together.** **Round 16 (independent, 4 findings, all blocking):** round 15 stated a rule covering every mutation and applied it only to M6 — **M1, M2, M3 and M5a still took a broken assertion as evidence**, and each now requires the mutated behaviour itself: the stale base observed *opening*; the corrupt fixture observed returning `CanonicalBaseRequiresRebuild`; the base-free fixture observed rejected by the wrongly widened check, with `base` named as the superblock's no-base default and **that synthetic source prohibited from shipped validation**; and `serialize_document`'s stored capability observed equal to the changed authority. Round 15's completeness claim is marked **FALSIFIED IN ROUND 16** at its original site. **Round 17 (authored-side sweep of §3 and §5, 10 findings, 5 blocking):** round 13's *could-this-pass-for-the-wrong-reason* question had never been asked of the tests or the gates, and both yielded immediately. **Gate 6's derive alternative could never match** — `grep` is line-oriented, so `[[:space:]]*` cannot cross the newline rustfmt puts between `#[derive(…, Default)]` and `pub struct BundleCapabilities`; the likelier violation returned 0 matches and the gate **passed**, while being the sole mechanical guard on the pin-3 prohibition M4 exists for because no test can catch it. **Gate 6a was vacuous under a rename** — pin 3b offered `synthetic_for_fixture` as an example, and the name is now pinned. **Gates 2 and 3 named no toolchain** in a repo whose CI records 1.95/1.97 lint divergence and whose default is 1.97.1; both are now `cargo +1.95.0`. **Gate 4's "staged list exactly §2" was unsatisfiable** with a conditional touch row, now subset-both-ways. **Tests 1, 6, 7, 8 and 9 could all pass on a base-free bundle**, since pin 5 makes base-free the permissive case and base-bearing fixtures are the awkward ones to build — test 1 degenerated into test 4. Also: tests 1/6 given distinct construction routes, test 4's caps asserted unequal, gate 1 requiring **0 ignored**, gate 7 given a method, gate 5 quoting all three dependency tables. **The unifying defect: a gate proving absence is only as strong as the string it searches for — a regex that cannot match, a name that was an example, a clause with no method, all reporting success while checking nothing. The remedy throughout is §4's: require an artifact quoted and read, not a pattern matched.** **Round 18 (independent, 2 findings, both blocking, both created by round 17):** the base-presence rule **demanded the opposite of what test 8 is for** — it grouped tests 8 and 9 as "the ones that commit", but test 8 *introduces* the base and must start `is_none()`, so the rule was either unsatisfiable or satisfiable by a fixture that made the test assert nothing; and **test 6's construction was self-contradictory**, assigned the commit path while required to arrive as its hand-built ancestor did (`bundle.rs:1866` calls `craft_image_with_base` at `:1869`). Fixed by a per-test state table and by **swapping the routes**, which makes the attribution true rather than deleting it. **Round 19 (independent): ZERO FINDINGS — the first clean round in nineteen**, confirming the per-test table, the route swap and the revised gate mechanics. **Running total: 65 findings, 47 blocking, across 19 rounds. A clean round is the criterion named at round 11 and the first evidence of convergence this contract has produced; it is not proof of correctness, and no round has re-derived the whole document. Still open after any ratification: M7's authority/base leg is unverifiable until S27 is implemented, those being S27's own deliverables, and every gate, test and mutation is specified but none has been run.** **RESOLVED — IMPLEMENTED 2026-08-09 (pin 10).** The authority now exists: `epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION` (a plain `u32`, baseline **0**, with its bump discipline beside it and the standing note that **no mechanism can detect a semantics change** — the discipline is the guarantee), wrapped at the composition boundary into a required `BundleCapabilities` that **has no `Default`** and is carried on the `Bundle` so all `commit` sites stay unchanged. Both boundaries validate: `Bundle::open` refuses a base disagreeing with the session's authority (pin 5), and `commit`/`commit_versioned` refuse a **newly emitted or replaced** base that does (pin 3a) — a scope that turns out to be **forced rather than chosen**, since no caller can hold an open `Bundle` whose *inherited* base is stale. Mismatch is `BundleError::CanonicalBaseRequiresRebuild { base, current }`: not read-only, not an integrity anomaly, and kept distinct from the malformed-document failure a base disagreeing with its own superblock produces. The format rung's temporary `ReductionAuthorityUnavailable` is **deleted**; its three negative assertions were re-pointed rather than dropped. **Both rulings taken as scoped:** the baseline stays `0` (starting anywhere else would manufacture the breakage the rung exists to detect), and the writer-path correction of §0.4 holds — though execution found §0.4 **overstated** it: `serialize_document` is a production writer, but `project.rs` is entirely `#[cfg(test)]`, and **no in-tree production path stages a base at all** now that the format rung's pin 3b closed the only one, so pin 3a guards the **public API** against out-of-tree callers rather than an internal path. **Pin 2a's disposition is the container epoch**, settled from outside by the format rung. **Signature change: `open` 60 sites, `create` 32**, reconciling exactly to §0.4's corrected table; `epiphany-bundle` sites take `synthetic_for_fixture`, `epiphany-testkit` and `epiphany-textproj` a named `production_caps()` wrapping the real constant. **`ids.rs`'s claim that "the algorithm catalog lives in `epiphany-ops`" is now true** — pin 8 is the rung that earned the sentence. **Inherited obligations all discharged:** both interim refusals converted to validation (not one); pin 3c's two suspended conformance assertions restored in `assert_reduction_serialization_stable` with the **suspension marker deleted**; and M8's laundering demonstration **performed for the first time** — see below. **Normative:** `core_spec.tex` gains `req:format:reduction-authority` (213 → **214** requirements; suite 284 → **285**, so touch row 12 was used and needed **three** constants, not one) plus a Revision History row, and `core_spec.pdf` is rebuilt. **P13-S16 becomes dispatchable when this lands** — pin 10 as amended in review round 12, its "ratified and tested within this rung" clause having been unsatisfiable by the only route pin 2a permitted. **ACCEPTED AND LANDED 2026-08-09 at `4df8e25`**, after eight independent reviews of the staged execution (95 findings, 70 blocking, across 19 pre-dispatch rounds and 8 post-execution reviews; the last returned zero). Gates re-run cold against the landed tree: **1577 passed / 0 failed / 0 ignored across 42 suites**, clippy and fmt clean on pinned 1.95.0. **Correction to pin 10's own wording:** it said S16 becomes *dispatchable*, but by this repo's definition — ratified and frozen, therefore ready to execute — S16 is **UNBLOCKED, not dispatchable**; its contract is still a DRAFT awaiting ratification. That is the same *unblocked*/*dispatchable* conflation this contract's own round 1 committed and had to disambiguate | | P13-S28 | **No container property distinguishes a document produced under a validated reduction authority from one produced before any authority existed — and the two candidates that look like they would, cannot.** P13-S27 installs an authority and validates it at read and write time, but cannot state what to do with a canonical base that predates the authority: a raw `ReductionAlgorithmVersion` is a bare `u32` (`bundle/src/ids.rs:291`) carrying no provenance, and the text-projection parser accepts an unbounded one from a document (`textproj/src/parse.rs:591`), so no numeric convention — including a deliberately high epoch — is safe from a hand-authored or third-party document declaring it. **`FORMAT_MINOR` does not work either, for two independent reasons:** the header *"never changes after the file is created"* (`core_spec.tex:10799`–`:10800`) and `commit_versioned` publishes only a superblock (`bundle.rs:791`), so a legacy bundle that commits a base S27 just validated keeps its old minor **permanently** — rejecting minor-≤1 bases would then reject a base the authority itself accepted, and accepting them leaves S16's `1` ambiguous; and `core_spec.tex:12258`–`:12262` limits a minor change to appending append-safe discriminants and calls it backward-compatible, whereas making a previously-valid base newly rejectable is a **semantic acceptance change**, with current readers ignoring minor entirely (`header.rs:119` gates on major alone) so the boundary would bind only readers that already comply. **The requirement that survives:** provenance MUST ride a container property that **old readers cannot silently accept** and that **a later commit cannot inherit unchanged** | `spec/CONTRACT_P13S27_REDUCTION_AUTHORITY.md` pin 2a (filed 2026-07-31; the disposition S27 cannot make from inside itself) | **IMPLEMENTED 2026-08-07 (`bc06706`, fix `be244df`). Was the critical path; both P13-S27 and P13-S16 were blocked on it.** **This rung must own all five, and none may be deferred into S27:** (1) an **old-reader rejection boundary** — pre-boundary readers must fail closed rather than silently open a document whose safety check they do not run; (2) **provenance that survives commits correctly**, i.e. is not inherited unchanged by a later generation and is not lost by one; (3) **legacy-base rebuild/repack behaviour**, stated for real artifacts rather than assumed away; (4) **every writer path, including text projection** — `serialize_document`, `project.rs`, and the committed `.txt` vectors, since a text document can declare any version; (5) **the exact format-version and compatibility consequences**, most plausibly a **major**-version boundary or a generation-scoped attestation paired with an incompatibility boundary. **Not a sub-pin of S27 and must not drift into it** — S27's pin 2a carries an explicit prohibition against being amended into a disposition without its own ratification round. **Scoped and RATIFIED 2026-07-31 as `spec/CONTRACT_FORMAT_EPOCH_MAJOR1.md`** after four adversarial review rounds — 11 pins, 11 tests, 11 mutations, 15 touch rows, 7 gate items. **This row is now a dependency record only; the work lives there and P13-S28 does not execute as a Pass 13 rung.** Rulings taken: the carrier is the **format major** (`FORMAT_MAJOR` 0 → 1, `FORMAT_MINOR` 1 → 0), decoded three ways through a named `FormatEpoch` rather than a bool, with **no** generation-scoped attestation in this epoch; legacy resolves to **hard rejection, not read-only**; and an eight-row epoch matrix in which a major-0 bundle with no base may open, one carrying a base is rejected, and one attempting to *add* a base is rejected and told to repack — **the non-inheritance rule that `FORMAT_MINOR` could not express**. All five things this row required the rung to own are pinned: old-reader boundary (pin 2), commit-surviving provenance (pin 3), legacy repack (pins 4, 5), every writer path including text projection (pins 3b, 6), and the exact format/compatibility consequences (pins 1, 7). **Three findings from the review rounds that changed the rung's shape**, none of them visible at filing: (1) **it cannot stamp major 1 before S27's writer enforcement exists**, so pin 3a temporarily refuses *both* boundaries — opening a major-1 bundle already carrying a base, and committing one into it — through a third, temporary `ReductionAuthorityUnavailable` error that must name P13-S27 and must **not** name repack; (2) **text projection launders provenance straight through the boundary** (`serialize_document` stages a carried base into a fresh bundle and `build_manifest` writes it), resolved as **symmetric document-level refusal** — projection, parsing and a new dedicated `SerializeError` variant, none of which existed to be "retained" — which forces `COMPANION_VERSION` 0.13.0 → **0.14.0** and rebuilds the committed corpus to **20 vectors, ten rejection classes, `canonical_bases` reach 2 → 0**, a real and stated capability loss; (3) **corruption precedence binds in both epochs** — a corrupt major-1 base must still fail as malformed, never as the *temporary* authority error a user would reasonably retry. **IMPLEMENTED 2026-08-07** — amended once before dispatch (pin 3c, touch rows 10/11, gate 8) after reconnaissance found pin 3a's refusals reaching a conformance criterion through a file the touch table did not carry. All 11 tests landed under their contract names, all 11 mutations run and observed, workspace green at 1569. **P13-S27 is unblocked and P13-S16 remains blocked on S27** — pin 8 resolved S27's open pin 2a (legacy bases are refused by container epoch, never by version arithmetic), and S27 additionally inherits three obligations recorded in its own contract: converting **both** interim refusals to validation, M8's deferred laundering demonstration, and pin 3c's two suspended conformance assertions. **Two touch-table gaps found during execution, both of the same shape** — a `.tex` requirement addition moves hardcoded counts in `testkit/tests/requirement_labels.rs`, and a companion-version bump moves a second normative version literal spelled `version~0.13.0` rather than `(0 13 0)`; neither file was in any touch table, and the second was caught only because `requirements_name_only_this_companion_version` exists. **A third gap was caught in review, after the rung was committed:** pin 3b's projection refusal had been implemented only on the **bundle** side (`document_from_bundle`), leaving the public `project_text_document` free to emit a `(canonical-base ...)` line for a directly constructed `TextDocument` — text the parser then rejects. A projector that can produce what the parser refuses is exactly the asymmetry pin 3b exists to close, and the refusal is unreachable through a `Bundle` during the interval anyway, so the *only* reachable half was the unguarded one. The public projector now returns `Result` and refuses; a crate-private `render_text_document` retains the base spelling for the one legitimate caller, the `canonical_base_present` negative vector. **The lesson is the rung's own recurring one:** a guard placed on the path that happened to be named, rather than on every path a caller can reach | -| P13-S29 | **Graph invariant 10's tag multiplexes: Chapter 3 and Chapter 4 failures are reported, through a public API, as invariant-10 violations.** `GraphInvariant::CrossCuttingRefsResolve` is emitted from five sites in four functions — `check_cross_cutting_refs`, `check_tempo_maps`, `check_aleatoric_models` and `check_accidental_modification_compatibility`. Only the first, plus the tempo map's two segment-anchor conditions, are reference resolution. The rest are Chapter 3 tempo shape/order/overlap, Chapter 3 aleatoric region locality, and a Chapter 4 expressibility rule whose own comment concedes it is *"not one of the spec-enumerated Chapter 5 graph invariants … surfaced under an existing `GraphInvariant` tag rather than minting a new one"*. This is **not internal**: `check_invariant(score, which)` is `pub`, and `impl Display for InvariantViolation` renders e.g. `invariant 10 (CrossCuttingRefsResolve) violated: non-constant tempo segment is missing its end_tempo` — a Chapter 3 tempo rule attributed in user-visible text to a Chapter 5 graph invariant | this file (found 2026-08-11 while scoping P13-S26; classification is per emitted condition, not per function) | **open.** Filed by `spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md` pin 7. **Not repaired there, deliberately:** S26 is documentation-and-guard and its pin 9 forbids any tag or behaviour change, while repairing this means minting tags or re-tagging emissions — both behaviour changes. S26's ruling was to keep invariant 10 **normatively** limited to reference resolution and to have the Rust doc comment distinguish the normative surface from the extra checks reported under the same tag, rather than widen a Chapter 5 invariant to absorb Chapter 3/4 rules because the implementation multiplexes them | +| P13-S29 | **Graph invariant 10's tag multiplexes: Chapter 3 and Chapter 4 failures are reported, through a public API, as invariant-10 violations.** `GraphInvariant::CrossCuttingRefsResolve` is emitted from five sites in four functions — `check_cross_cutting_refs`, `check_tempo_maps`, `check_aleatoric_models` and `check_accidental_modification_compatibility`. Only the first, plus the tempo map's two segment-anchor conditions, are reference resolution. The rest are Chapter 3 tempo shape/order/overlap, Chapter 3 aleatoric region locality, and a Chapter 4 expressibility rule whose own comment concedes it is *"not one of the spec-enumerated Chapter 5 graph invariants … surfaced under an existing `GraphInvariant` tag rather than minting a new one"*. This is **not internal**: `check_invariant(score, which)` is `pub`, and `impl Display for InvariantViolation` renders e.g. `invariant 10 (CrossCuttingRefsResolve) violated: non-constant tempo segment is missing its end_tempo` — a Chapter 3 tempo rule attributed in user-visible text to a Chapter 5 graph invariant | this file (found 2026-08-11 while scoping P13-S26; classification is per emitted condition, not per function) | **open.** Filed by `spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md` pin 7. **Not repaired there, deliberately:** S26 is documentation-and-guard and its pin 9 forbids any tag or behaviour change, while repairing this means minting tags or re-tagging emissions — both behaviour changes. S26's ruling was to keep invariant 10 **normatively** limited to reference resolution and to have the Rust doc comment distinguish the normative surface from the extra checks reported under the same tag, rather than widen a Chapter 5 invariant to absorb Chapter 3/4 rules because the implementation multiplexes them **RESOLVED 2026-08-11 by `spec/CONTRACT_P13S29_VIOLATION_KIND.md`, disposition (b) type-neutral.** `InvariantViolation` becomes `WellFormednessViolation` with `kind: ViolationKind`, whose two arms are `Invariant(GraphInvariant)` and `Requirement(&'static str)`. `check_invariants` stays **comprehensive** — every broad caller keeps its rule coverage — while `check_invariant` deliberately narrows to the invariant arm and a symmetric `check_requirement` is added. `req:time:tempo-segment-shape` is minted for the one rider that had no label, stating enforced compatibility without resolving P13-S8. **`GraphInvariant` did not move: 21 variants, unchanged.** | | P13-S30 | **The repository's ad hoc TeX parsers assume a spelling TeX does not require, and two of the four consequences can pass silently.** `\label {x}`, `\begin {requirement}`, `\end {requirement}` and `\chapter {X}` are all legal and all missed, because every scanner matches an exact `\command{` needle. **(i) A requirement block can vanish.** `load_spec` finds blocks by `text.find(r"\begin{requirement}")`; a spaced opener is never pushed into `requirements`, and **is silent when the block is additive and carries no `req:` label** — the block counts (`CORE_REQUIREMENT_COUNT`, `SUITE_REQUIREMENT_COUNT`) and the label count (`SUITE_LABEL_COUNT`) count different things, and a whole-text label scan keeps the latter level. Re-spacing an *existing* block is loud on the block counts; a hidden block carrying a `req:` label is loud on the label counts. **Exact opener with spaced closer** either panics (no later exact close) or **consumes through** a later block's close, which is silent when the consuming block is additive, label-free and immediately precedes a single-label block in the same chapter. **(ii) A `req:` label yields a false "cited but undefined" diagnosis** — missed on the defining side by `labels()`, still found on the citing side by `requirement_strings`. **(iii) Chapter association is missed or shifted**, with four outcomes: no prior recognized chapter → `load_spec` panics; predecessor absent from `CHAPTER_AREAS` → the area test panics; predecessor in a different area → loud mismatch; **predecessor in the same area → silent**, which is reachable — `Graph Value Layouts` (`binary_format.tex:814`) immediately precedes `Operation Wire Forms` (`:1196`) and both map to `binfmt`. Of that file's twelve chapter headings, seven appear in `CHAPTER_AREAS`. **(iv) The blind spot is replicated across independently written scanners**, so a fix in one leaves the others unrepaired; divergence is a **latent risk, not an observed fact** — the read proves duplication only. Known consumer inventory, from an exhaustive grep of exact TeX-form literals across `crates/`, **all test-scope**: `text_projection_grammar.rs` at `:73`, `:341`, `:363`, `:508`, `:538`, `:591`, and the paired requirement-block delimiters `:596`/`:647` (openers) with `:649` (the matching exact `\end{requirement}`); `requirement_labels.rs:166`–`:167`; `binary_format_history.rs:107`–`:112`, whose `.expect` panics on a spaced heading; `epiphany-textproj/src/parse.rs:726`, inside `#[cfg(test)] mod tests`. **No production consumer was found during scoping**; a later one extends this row rather than contradicting it | this file (found 2026-08-11 while scoping P13-S26; the owner ruled it be filed rather than left in a contract section that becomes historical) | **open.** Filed by `spec/CONTRACT_P13S26_INVARIANT10_SURFACE.md` pin 7; repairing the parsers is out of scope there. **Evidence for consequence (i)** is that rung's mutation **M20**, whose transcript in `spec/EVIDENCE_P13S26_EXECUTION.md` shows a spaced `\begin {requirement}` passing every existing suite — S26's own guard is the only thing that catches it. **M20 evidences the spaced-opener case only**: its probe spaces both delimiters, so no parser reaches the opener and none ever hunts a close; the exact-open/spaced-close behaviour is established by code read, and a rung wanting it exhibited owes its own probe. P13-S22 and P13-S25 do not own this: they concern misleading diagnoses in the decode corpus, not a syntax/parser mismatch across the `.tex` suite | diff --git a/spec/core_spec.pdf b/spec/core_spec.pdf index 42d1086..da19d5b 100644 Binary files a/spec/core_spec.pdf and b/spec/core_spec.pdf differ diff --git a/spec/core_spec.tex b/spec/core_spec.tex index 76259ee..cefbe97 100644 --- a/spec/core_spec.tex +++ b/spec/core_spec.tex @@ -2277,6 +2277,18 @@ pub struct Tempo { \texttt{start\_tempo} if no earlier segment exists. \end{requirement} +\begin{requirement} + \label{req:time:tempo-segment-shape} + A tempo segment's \texttt{shape} and its \texttt{end\_tempo} \MUST{} be + compatible. If \texttt{shape} is \texttt{Constant} and \texttt{end\_tempo} + is present, it \MUST{} equal \texttt{start\_tempo}. If \texttt{shape} is + \texttt{Linear}, \texttt{Exponential} or \texttt{Curve}, \texttt{end\_tempo} + \MUST{} be present. + + This requirement states the compatibility that is enforced. It does not + determine whether a constant segment records an \texttt{end\_tempo} at all. +\end{requirement} + \subsection{Conversion} Conversion between musical and wall-clock time integrates the tempo map. @@ -17029,6 +17041,20 @@ layouts they own versus inherit: region --- a locality rule the checker has always enforced and no requirement stated. \\ + \today & \sectionsc{Graph Invariants}, \sectionsc{Time and Duration} & + \textbf{P13-S29: the violation tag stops multiplexing.} Graph invariant~10 + reported Chapter~3 and Chapter~4 failures under its own number, through a + public API. The violation type becomes \texttt{WellFormednessViolation} + carrying a two-armed \texttt{ViolationKind}: an invariant arm and a + requirement arm naming a \texttt{req:} label. Invariant~10 keeps only + reference resolution; tempo segment shape, tempo segment order, aleatoric + reference locality and accidental modification expressibility now report + under their own requirements. \sectionsc{Time and Duration} gains + Requirement~\ref{req:time:tempo-segment-shape}, stating the enforced + shape/\texttt{end\_tempo} compatibility without determining whether a + constant segment records an \texttt{end\_tempo} at all. The enumeration is + unchanged. + \\ \bottomrule \end{longtable}