diff --git a/crates/epiphany-core/src/graph.rs b/crates/epiphany-core/src/graph.rs index 06e8bc7..4effa8a 100644 --- a/crates/epiphany-core/src/graph.rs +++ b/crates/epiphany-core/src/graph.rs @@ -596,7 +596,15 @@ impl Voice { /// comparison or delta they need is not computable (contract pin 7): this is /// deliberate, not a safety property, because base-ingested data may predate /// the rule. Pickup/anacrusis (a partial first measure) is deferred -/// (P13-S19) and is never refused or flagged by this rung. +/// (P13-S19): a first measure skips only the predecessor-dependent checks +/// — invariant 20's boundary clause and `create_measure`'s clauses 1 and 3 +/// — plus the agreement check when it declares `None` or a matching +/// signature; it can still be refused for other reasons (a dead parent, an +/// unresolving referent). Its own successor is unaffected by any of this: +/// the successor is measured against the governing signature's full +/// `measure_duration()` regardless, and is refused (`MeasureMeterMismatch`) +/// and flagged by invariant 20 when the pickup's actual length is shorter +/// than a full bar. #[derive(Clone, PartialEq, Eq, Debug)] pub struct Measure { pub id: MeasureId, diff --git a/crates/epiphany-core/src/invariants.rs b/crates/epiphany-core/src/invariants.rs index 93b18ca..c1172b5 100644 --- a/crates/epiphany-core/src/invariants.rs +++ b/crates/epiphany-core/src/invariants.rs @@ -108,8 +108,12 @@ pub enum GraphInvariant { /// comparable relation or pin 6b's musical delta cannot decide the /// comparison (base-ingested data may predate the rule); this is /// deliberate abstention, not a soundness gap (pin 7). A - /// pickup/anacrusis first measure has no predecessor and is never - /// flagged (P13-S19, deferred). + /// pickup/anacrusis first measure has no predecessor for the + /// boundary clause, which is vacuous for it; the agreement clause + /// has no such exemption and still applies. Its successor is + /// measured against the governing signature's full + /// `measure_duration()` and can be refused and flagged (P13-S19, + /// deferred). MeasureMeterConsistency, } @@ -4756,15 +4760,34 @@ mod g3b_measure20_tests { ); } - /// M35: removing the boundary clause must let this go undetected. Both + /// M35: this IS the pickup/anacrusis demonstration (spec/CONTRACT_P13S19_ + /// PARTIAL.md pin 1). `m0` is a first measure occupying only half a bar + /// -- a pickup -- and by itself is flagged by neither clause: it has no + /// predecessor, so the boundary clause is vacuous, and it avoids the + /// agreement clause here by declaring `None` (not by any first-measure + /// exemption -- there is none). `m1` is its successor, comparable and + /// correctly ordered, but only HALF a `measure_duration` away -- the + /// pickup's own actual length, not the governing signature's full bar. + /// Removing the boundary clause must let THAT go undetected. Both /// measures avoid the agreement clause (`None`) so only boundary can /// fire. #[test] - fn m35_boundary_flags_wrong_distance() { + fn m35_pickup_successor_boundary_flags_wrong_distance() { let replica = ReplicaId(7); let (active, ts_active) = sig(replica, 1); let region = probe_region_id(); let m0 = measure_at(MeasureId::new(replica, 10), region, 0, None); + + // The pickup by itself: a first measure has no predecessor, so the + // boundary clause is vacuous for it, and `None` separately avoids + // the agreement clause -- neither is an exemption granted TO the + // agreement clause itself (pin 1). + let (lone, _) = score_with(Some(active), vec![ts_active.clone()], vec![m0.clone()]); + assert!( + !fires(&lone, GraphInvariant::MeasureMeterConsistency), + "the pickup by itself, first measure, no predecessor, must not be flagged" + ); + // Half a whole note later — not a full measure_duration away. let m1 = Measure { id: MeasureId::new(replica, 11), @@ -4855,20 +4878,26 @@ mod g3b_measure20_tests { ); } - /// M38: a pickup (partial) first measure must never be flagged -- it - /// has no predecessor, so the boundary clause is vacuous for it. + /// M38: a pickup (partial) first measure declaring no time signature + /// must never be flagged BY THE BOUNDARY CLAUSE -- it has no + /// predecessor, so that clause is vacuous for it. This is narrower than + /// "never flagged" in general: the agreement clause is not + /// predecessor-dependent and would apply to this same measure if it + /// declared a disagreeing signature instead of `None` (spec/CONTRACT_ + /// P13S19_PARTIAL.md pin 1) -- this fixture's `None` avoids agreement + /// separately, not as a consequence of being a first measure. /// /// **On the mutation's failure mode:** the M38 mutation (removing the /// `if i == 0 { continue; }` guard in `check_measure_meter_consistency`) /// is observed as an `attempt to subtract with overflow` PANIC, not a /// wrong-flag assertion failure. This is expected and still a valid red /// signal, not a weak one: that `i == 0` guard is simultaneously the - /// pickup-measure exemption AND the only thing standing between `i - 1` - /// and a `usize` underflow, so any mutation that removes or weakens it - /// crashes before it could ever produce a wrong (but well-formed) - /// verdict to assert against. + /// pickup-measure boundary-clause exemption AND the only thing standing + /// between `i - 1` and a `usize` underflow, so any mutation that removes + /// or weakens it crashes before it could ever produce a wrong (but + /// well-formed) verdict to assert against. #[test] - fn m38_pickup_first_measure_not_flagged() { + fn m38_pickup_first_measure_boundary_clause_not_flagged() { let replica = ReplicaId(7); let (active, ts_active) = sig(replica, 1); let region = probe_region_id(); @@ -4888,7 +4917,9 @@ mod g3b_measure20_tests { let (score, _) = score_with(Some(active), vec![ts_active], vec![m0]); assert!( !fires(&score, GraphInvariant::MeasureMeterConsistency), - "a lone first (pickup) measure must never be flagged by invariant 20" + "a lone first (pickup) measure declaring no time signature must not be flagged \ + by invariant 20's boundary clause -- vacuous, no predecessor (its agreement \ + clause is separately avoided by `None`, not exempted by being first)" ); } @@ -4919,10 +4950,11 @@ mod g3b_measure20_tests { // clauses = 18 cells) plus the four non-shape-driven paths (A1, A3, B2, // B3) that pin 4's shapes do not themselves exercise. A2 and B1 reuse // `m39_unresolvable_reference_is_invariant_10_only` and - // `m38_pickup_first_measure_not_flagged` above respectively; S3 reuses - // `m34_agreement_flags_disagreement` and `m35_boundary_flags_wrong_ - // distance` above (Region same id, same edge, Musical offsets is - // exactly their shape). Every other cell gets a dedicated fixture below. + // `m38_pickup_first_measure_boundary_clause_not_flagged` above + // respectively; S3 reuses `m34_agreement_flags_disagreement` and + // `m35_pickup_successor_boundary_flags_wrong_distance` above (Region + // same id, same edge, Musical offsets is exactly their shape). Every + // other cell gets a dedicated fixture below. // ------------------------------------------------------------------- /// Matrix cell A1: `m.time_signature` is `None` -- inapplicable, not diff --git a/crates/epiphany-ops/DECISIONS.md b/crates/epiphany-ops/DECISIONS.md index 02ef8f9..a05bcdd 100644 --- a/crates/epiphany-ops/DECISIONS.md +++ b/crates/epiphany-ops/DECISIONS.md @@ -2157,11 +2157,19 @@ and strictly after it (`MeasureOutOfOrder`, or `MeasureOrderUnverifiable` if incomparable); agreement against the effective grid's active signature (`MeasureMeterMismatch`); and the boundary distance from the predecessor equals the governing `measure_duration()` (`MeasureMeterMismatch`, or -`MeasureOrderUnverifiable` if the delta is not computable). All three -clauses are vacuous for an instance's first measure — no predecessor to -compare against — which is the pickup/anacrusis deferral filed as -**P13-S19**, open by design (core `DECISIONS.md` files the invariant-side -mirror). `CreateMeasure` fails **closed** on every incomputable case; graph +`MeasureOrderUnverifiable` if the delta is not computable). Clauses 1 +(ordering) and 3 (boundary distance) are vacuous for an instance's first +measure — no predecessor to compare against. Clause 2 (agreement) has **no** +predecessor dependency and runs on a first measure exactly as on any other: +a pickup declaring a signature that disagrees with the governing grid is +refused by clause 2 alone, first measure or not. And clause 3's exemption is +narrower than "vacuous" suggests: the pickup's *own successor* is measured +against the governing signature's full `measure_duration()`, not the +pickup's own (shorter) length, so `create_measure` refuses that successor +too. This is the pickup/anacrusis deferral filed as **P13-S19**, open by +design (core `DECISIONS.md` files the invariant-side mirror, correctly +scoped to "never flagged **by the boundary clause**" — not never flagged at +all). `CreateMeasure` fails **closed** on every incomputable case; graph invariant 20 (core `DECISIONS.md`) **abstains** on the identical cases — deliberately opposite postures, not an inconsistency. diff --git a/crates/epiphany-ops/src/reduce.rs b/crates/epiphany-ops/src/reduce.rs index f9dce04..5891b40 100644 --- a/crates/epiphany-ops/src/reduce.rs +++ b/crates/epiphany-ops/src/reduce.rs @@ -19832,6 +19832,246 @@ mod tests { ); } + /// Pin 4 (spec/CONTRACT_P13S19_PARTIAL.md): a pickup's successor is + /// refused end-to-end, not merely read off the reducer's source. The + /// pickup itself — first measure of the instance, `time_signature: + /// None` so the agreement clause (clause 2, which is NOT + /// predecessor-dependent) is avoided by declaration rather than by any + /// first-measure exemption — mints `Applied`: clauses 1 and 3 are + /// vacuous for it (no predecessor). Its successor, ALSO declaring + /// `time_signature: None` (so its own clause 2 is out of the way and + /// the refusal below cannot be clause 2's), starts only HALF a + /// `measure_duration` after the pickup — the pickup's own actual + /// (unmodelled) content length, not the governing signature's full + /// whole-note bar — and clause 3 refuses it: `MeasureMeterMismatch`. + /// The governing signature's own write and the pickup's mint are both + /// asserted `Applied` before the refusal is asserted, so envelope + /// counter gaps cannot make either op silently pending and pass the + /// refusal off as something it isn't. + #[test] + fn g3b_create_measure_pickup_successor_refused_end_to_end() { + let region = RegionId::new(ReplicaId(1), 90); + let instance = StaffInstanceId::new(ReplicaId(1), 91); + let staff = StaffId::new(ReplicaId(1), 92); + let mut envs = g3b_region_and_instance_envs(1, region, instance, staff); + + let sig_a = TimeSignatureId::new(ReplicaId(1), 93); + // numerator 4 -> measure_duration = 4/4 = one whole note ("a full bar"). + let set_sig_a = prim_env( + 1, + 2, + 2, + CausalContext::new(), + OperationKind::SetTimeSignature(SetTimeSignatureOp { + region, + anchor: g3b_region_anchor(region, 0), + time_signature: Some(crate::valuegen::time_signature(sig_a, 4)), + }), + ); + envs.push(set_sig_a.clone()); + + fn measure(id: u64, start: TimeAnchor, sig: Option) -> Measure { + Measure { + id: MeasureId::new(ReplicaId(1), id), + start, + time_signature: sig, + explicit_number: None, + number_visibility: epiphany_core::MeasureNumberVisibility::Auto, + } + } + + // The pickup: first measure, `None` (pin 4's fixture constraint — + // `Some` of a disagreeing signature would be refused by clause 2 + // instead, for a reason that has nothing to do with partiality). + let pickup = g3b_measure_env( + 1, + 3, + 3, + instance, + measure(400, g3b_region_anchor(region, 0), None), + ); + + // The successor: also `None`, so ITS clause 2 is equally out of the + // way. Half a whole note after the pickup — not the full bar sig_a + // demands. + let successor = g3b_measure_env( + 1, + 4, + 4, + instance, + measure( + 401, + TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Musical(MusicalDuration( + RationalTime::new(1, 2).unwrap(), + )), + }, + None, + ), + ); + + envs.extend([pickup.clone(), successor.clone()]); + let mut set = OperationSet::new(); + set.accept_all(envs); + let state = set.reduce(); + + assert_eq!( + g3b_effect_of(&state, set_sig_a.id), + Some(OperationEffect::Applied), + "the governing signature must itself be applied, or the refusal below proves nothing" + ); + assert_eq!( + g3b_effect_of(&state, pickup.id), + Some(OperationEffect::Applied), + "pin 1: the pickup itself is neither refused nor flagged — clauses 1 and 3 are \ + vacuous for a first measure, and clause 2 is avoided here by declaring `None`, \ + not by any first-measure exemption" + ); + assert_eq!( + g3b_effect_of(&state, successor.id), + Some(OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::MeasureMeterMismatch + } + }), + "pin 4: the pickup's successor is measured against the governing signature's FULL \ + measure_duration (one whole note), not the pickup's own half-note actual length — \ + clause 3 refuses it MeasureMeterMismatch, and (both sides declaring `None`) this \ + refusal cannot be clause 2's" + ); + } + + /// Pin 2 (spec/CONTRACT_P13S19_PARTIAL.md): a mid-score partial measure + /// — index >= 1, so it has no first-measure exemption at all — enters + /// successfully, because the boundary check run when IT is created only + /// examines the distance from ITS predecessor (`m0`, a full measure), + /// never its own eventual length. The failure surfaces one measure + /// later, on `m1`'s own successor (`m2`), whose distance from `m1` + /// exposes `m1`'s actual (partial) length against the same governing + /// signature's full `measure_duration()`. + #[test] + fn g3b_create_measure_mid_score_partial_successor_refused_end_to_end() { + let region = RegionId::new(ReplicaId(1), 94); + let instance = StaffInstanceId::new(ReplicaId(1), 95); + let staff = StaffId::new(ReplicaId(1), 96); + let mut envs = g3b_region_and_instance_envs(1, region, instance, staff); + + let sig_a = TimeSignatureId::new(ReplicaId(1), 97); + // numerator 4 -> measure_duration = 4/4 = one whole note. + let set_sig_a = prim_env( + 1, + 2, + 2, + CausalContext::new(), + OperationKind::SetTimeSignature(SetTimeSignatureOp { + region, + anchor: g3b_region_anchor(region, 0), + time_signature: Some(crate::valuegen::time_signature(sig_a, 4)), + }), + ); + envs.push(set_sig_a.clone()); + + fn measure(id: u64, start: TimeAnchor, sig: Option) -> Measure { + Measure { + id: MeasureId::new(ReplicaId(1), id), + start, + time_signature: sig, + explicit_number: None, + number_visibility: epiphany_core::MeasureNumberVisibility::Auto, + } + } + + // m0: an ordinary, FULL first measure — not itself a pickup, so + // this scenario cannot be mistaken for pin 4's first-measure case. + let m0 = g3b_measure_env( + 1, + 3, + 3, + instance, + measure(410, g3b_region_anchor(region, 0), None), + ); + + // m1: index 1, one full measure_duration after m0 — enters + // successfully. This validates m0's implied length (full), NOT + // m1's own eventual length; nothing examines that until m1 gets a + // successor of its own. m1 is the mid-score partial: it has no + // exemption from clauses 1/3 (it HAS a predecessor), it merely + // happens to satisfy them here because m0 was full. + let m1 = g3b_measure_env( + 1, + 4, + 4, + instance, + measure( + 411, + TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Musical(MusicalDuration(RationalTime::from_int(1))), + }, + None, + ), + ); + + // m2: m1's successor, only HALF a measure_duration after m1 — m1's + // own actual (partial) length, not sig_a's full bar. This is where + // the partial duration surfaces, on the measure AFTER the partial + // one, exactly as pin 2 describes. + let m2 = g3b_measure_env( + 1, + 5, + 5, + instance, + measure( + 412, + TimeAnchor::Region { + id: region, + edge: RegionEdge::Start, + offset: AnchorOffset::Musical(MusicalDuration( + RationalTime::new(3, 2).unwrap(), + )), + }, + None, + ), + ); + + envs.extend([m0.clone(), m1.clone(), m2.clone()]); + let mut set = OperationSet::new(); + set.accept_all(envs); + let state = set.reduce(); + + assert_eq!( + g3b_effect_of(&state, set_sig_a.id), + Some(OperationEffect::Applied), + "the governing signature must itself be applied, or nothing below proves anything" + ); + assert_eq!( + g3b_effect_of(&state, m0.id), + Some(OperationEffect::Applied), + "m0: an ordinary full first measure" + ); + assert_eq!( + g3b_effect_of(&state, m1.id), + Some(OperationEffect::Applied), + "pin 2: a mid-score partial measure enters successfully — its creation only checks \ + the distance from ITS predecessor (m0, full), never its own eventual length" + ); + assert_eq!( + g3b_effect_of(&state, m2.id), + Some(OperationEffect::NoOp { + reason: NoOpReason::PreconditionFailedUnderReduction { + reason: PreconditionFailureReason::MeasureMeterMismatch + } + }), + "pin 2: m1's successor is what exposes the partial duration — measured against the \ + governing signature's full measure_duration, not m1's own half-note actual length. \ + m1 has NO first-measure exemption (index 1, it HAS a predecessor); it simply \ + satisfied clause 3 because m0 happened to be full" + ); + } + /// Repair 2 (spec/CONTRACT_GENESIS_G3B_MEASURE.md pin 6c case 1 / pin 7): /// creating a measure against a WHOLLY EMPTY effective grid — no /// `local_metric_grid`, no region `default_metric_grid`, and no diff --git a/spec/CONTRACT_P13S19_PARTIAL.md b/spec/CONTRACT_P13S19_PARTIAL.md index 74a0cb2..3d8390e 100644 --- a/spec/CONTRACT_P13S19_PARTIAL.md +++ b/spec/CONTRACT_P13S19_PARTIAL.md @@ -1,6 +1,6 @@ # Contract — P13-S19: what a partial measure actually costs -**Status:** DRAFT. +**Status:** RATIFIED. **Rung type:** correction and observation. **No behaviour change.** Not one graph's invariant-20 verdict may move, and not one operation's effect may @@ -13,7 +13,8 @@ change. The rung makes the tree say what it already does. Read out of the working tree at `339269b`, not recalled. 1. **An existing test is already the pickup demonstration.** - `m35_boundary_flags_wrong_distance` (`invariants.rs`) places `m0` at region + `m35_boundary_flags_wrong_distance` (`invariants.rs`, renamed by this rung + to `m35_pickup_successor_boundary_flags_wrong_distance`) places `m0` at region start offset `0` and `m1` at offset `Musical(1/2)`, under a signature whose `measure_duration()` is a **whole** (`sig()`, `:4597`), and asserts invariant 20 **fires**. That is a first measure occupying half a bar followed by its @@ -41,7 +42,7 @@ Read out of the working tree at `339269b`, not recalled. | c | `spec/operation_catalog.tex:1678` | "never refused or flagged on this account" | | d | `spec/core_spec.tex:6632`–`:6633` | "has no predecessor and is never flagged" | | e | `crates/epiphany-core/src/invariants.rs:111`–`:112` | the **public doc comment** on `GraphInvariant::MeasureMeterConsistency`, same form | - | f | `m38_pickup_first_measure_not_flagged` | its **name**, its comment, and its assertion message ("must never be flagged by invariant 20") | + | f | `m38_pickup_first_measure_not_flagged` (renamed by this rung to `m38_pickup_first_measure_boundary_clause_not_flagged`) | its **name**, its comment, and its assertion message ("must never be flagged by invariant 20") | | g | `crates/epiphany-ops/DECISIONS.md:2161` | **"All three clauses are vacuous for an instance's first measure — no predecessor to compare against."** This is not understatement, it is **false**: clause 2 has no predecessor dependency and runs | Rows **d, e, f** were **absent from the ratified scope**, which named the diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index ab1118a..99e4f4a 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -96,7 +96,8 @@ visible — a value with a wire form and no canonical carrier to reach it.) | P13-S16 | **`StaffGroup.members` and `Staff.group` may disagree in both directions, and nothing detects it.** The two fields encode the same relation twice. `Staff.group` (`core_spec.tex:5578`, `graph.rs:819`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4231`, `graph.rs:1614`) lists the staves in a group. **The specification declares both and states neither an authority nor an agreement requirement.** Graph invariant 10 checks that each side *resolves* — a staff's group is declared (`invariants.rs:1126`), a group's members are declared (`:1135`) — and never that the two agree, so **both stale forms pass every check in the tree**: a *missing* member (`s.group == Some(g)` while `g.members` omits `s`) and a *spurious* member (`g.members` contains `s` while `s.group` is `None` or names a different group). Genesis G3a ruled `Staff.group` the sole authority and `StaffGroup.members` a non-authoritative denormalized projection (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, ratified 2026-07-29) — a normative semantic ruling that makes the disagreement *defined* rather than merely undetected, but does not make it *impossible*: G3a stores the projection without maintaining it | `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1 (found 2026-07-29 during G3a contract review; the authorship cycle is what surfaced it — with mints only, no authoring order produces an agreeing pair, since `CreateStaff` requires its group live at `reduce.rs:4117` and `CreateStaffGroup` requires its members live) | **open.** Deliberately no code change in G3a. The fix is disposition **A**: maintain the projection under reduction — `create_staff` with `group: Some(g)` appends to `g.members` — plus a candidate **graph invariant 21** enforcing agreement in both directions, and a decision on whether a re-carried `CreateStaffGroup` compares against its *carried* `members` (empty) or the current derived state. **Consumers must read `Staff.group`, never `StaffGroup.members`, for membership** until that lands. Sequence it after G3b so an invariant append is not competing with G3b's invariant 20 | | P13-S17 | **Binary Format revision history omitted genesis tranche G2b entirely, including the accept-set raise it performed.** `spec/binary_format.tex`'s Revision History chapter ran G2a 0.12.0 straight to G-minor 0.13.0 to G3a 0.14.0, with no row anywhere recording G2b (`spec/CONTRACT_GENESIS_G2B_TUNING.md`, kind/tag 34, `SetTuningContext`) — even though `OperationEnvelopeBlock`'s accept-set raise 2→3, the first accept-set move since genesis tranche G2a explicitly recorded staying at 2, reached the normative tables (the per-chunk-role accept-set prose at `binary_format.tex:2353`–`:2363`, which names the `OperationEnvelopeBlock` role's maximum as 3 "as of genesis tranche G2b", and the `OperationKind` minor-additive bullet at `:2395`–`:2418`, which records "genesis tranche G2b took 34 (`SetTuningContext`)") and never the history. G2b's own contract touch table row 27 required "version, Revision History row" among the four-document ritual, and the rung was signed off without it — the gate did not catch a documentation MUST because nothing tests the revision history | `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` §0 (found 2026-07-29 during the G3a undo-repair contract review, verified against the working tree: `binary_format.tex:3599`, `:3628`, `:3643` before this rung's edit) | **RESOLVED in this same commit.** The chronology is restored: G2b lands as its own 0.14.0 row between G-minor and G3a, and G3a renumbers to 0.15.0 (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet B, pins B2–B3). A new scoped guard in `epiphany-testkit` makes the omission recurrence-detectable — a distinct principal marker per standalone-row rung (G2a, G-minor, G2b, G3a — G1 is deliberately unguarded, having no standalone row of its own), strictly ordered, with G2b's content anchored within its own row segment — so the entry is filed and closed by the same packet that finds it, unlike **P13-S15** and **P13-S16**, which stay open because their fixes are sequenced to later rungs | | P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, but only three of the checker's nine non-success paths are the real gap — not the whole checker, as first filed and over-sized.** `check_measure_meter_consistency` (`invariants.rs:2662`) has nine non-success paths across its two clauses, enumerated and classified by both its own doc comment and `spec/CONTRACT_P13S18_MATRIX.md`'s 18-cell outcome matrix (agreement: A1-A4; boundary: B1-B5). A1 (`None` declared signature) is **inapplicable** — nothing to disagree with. A3/B3 (`Governing20::None`, an empty governing candidate set) are **vacuous** (pin 6c case 1). A2/B2 (an unresolving declared or governing signature) are **delegated** to invariant 10's own resolution check (`invariants.rs:1220`ff, its per-measure and instance-local-grid arms) — verified, not merely asserted: the matrix rung's mutations M7/M8 delete each arm in turn and show the SAME condition go unreported by the ENTIRE workspace suite, not merely by invariant 20. B1 (the first measure) is the already-filed pickup/anacrusis deferral, **P13-S19**. **Exactly three paths are genuine abstention: A4 and B4 (`Governing20::Indeterminate` — the comparable relation cannot place a candidate) and B5 (a decided governing selection with no computable musical delta — order without distance).** Also corrected: the earlier **"any `Measure` *end* anchor is incomparable"** claim was wrong only in its "any" — same-id, same-position `End`<->`End` IS comparable under c2 **when its offsets compare** (`measure20_offset_order`, `:2419`, returns `None` only for `Musical` against `WallClock`); distinct-id `End` anchors genuinely are incomparable (c3 restricts to `Start`+`Zero`) and do reach A4/B4/B5; and the `resolve_anchor` `Measure` arm citation (now `:503`-`:516`, formerly miscited as `:400`ff — see the companion line-number repair to `CONTRACT_GENESIS_G3B_MEASURE.md:206`) names the missing duration machinery, not invariant 20's own execution path, which never calls `resolve_anchor`. And the `WallClock`-anchored measure start `epiphany-ops::valuegen::measure` (`ops/src/valuegen.rs:447`) actually emits does **not** uniformly abstain both clauses: against `WallClock`-anchored meter changes (c5) agreement DECIDES and only the boundary clause abstains (B5, since `measure20_musical_delta` never returns a `WallClock` delta); against `Region`-anchored meter changes both abstain (A4/B4), because `WallClock` against `Region` has no comparability arm at all | `spec/CONTRACT_P13S18_MATRIX.md` pin 8 (ratified 2026-07-31, a diagnostic and bookkeeping rung: test coverage over `check_measure_meter_consistency`'s existing nine paths plus these three ledger repairs, no behaviour change) | **open, at its true size.** A4, B4 and B5 remain real, still gated on the deferred common-timeline machinery — but the capability that closes them is now filed as **P13-S23** (below), not P11-C5: P11-C5 is a narrower re-anchoring proximity metric this entry previously over-cited as the gate; P13-S23 is the broader "place any anchor pair on a common timeline and measure musical distance" capability that actually owns A4, B4 and B5 | -| P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes | +| P13-S19 | **A pickup's *successor*, not the pickup itself, is what `CreateMeasure` and invariant 20 refuse — pickup/anacrusis measures are authorable, but the rest of the instance becomes unauthorable once one exists.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes `create_measure`'s clauses 1 (ordering) and 3 (boundary distance) vacuous for a first measure, and invariant 20's boundary clause is symmetrically exempt at `i == 0` — both for lack of a predecessor. **The agreement clause (clause 2) is not predecessor-dependent and applies to a first measure like any other**: a pickup declaring a signature that disagrees with the governing grid is itself refused (`MeasureMeterMismatch`) and flagged; only a pickup declaring `None` or a matching signature clears it, and only when its other preconditions (a live parent `StaffInstance`, resolving referents) are satisfied too. **The real defect is one measure downstream**: both rules compare `delta(prev.start, m.start)` against the *governing signature's full* `measure_duration()`, when the true distance is `prev`'s own content duration — those coincide only for full measures. A pickup's successor is therefore refused (`MeasureMeterMismatch`) by `create_measure` and flagged by invariant 20, which is what actually makes the rest of the instance unauthorable once a pickup is minted. This applies to **any** partial measure, not only a first one: a mid-score partial measure enters successfully (nothing examines its own duration when it is created), while *its* successor is refused the identical way — the failure is always attributed to the measure after the partial one. Closing this needs a per-measure duration — the "partial measure" notion this entry already names — and that is deliberately **not** introduced by the correction that reworded this entry. See also **P13-S24**, the Chapter 3 derived-notation deferral that shares this same missing concept but touches neither invariant 20 nor `CreateMeasure` | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting); corrected 2026-07-31 by `spec/CONTRACT_P13S19_PARTIAL.md`, which found the original wording true only of the pickup itself and, read as written, indistinguishable from "pickups work" | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes; it now depends on a per-measure duration concept, which does not yet exist | +| P13-S24 | **The Chapter 3 integer-grid metric splitter assumes the region origin falls on a barline, deferring anacrusis/pickup handling — a second, independent site carrying the same missing partial-measure-duration concept P13-S19 names for invariant 20 and `CreateMeasure`.** `core_spec.tex:2484` (Chapter 3, derived notation) states the assumption directly; the same deferral is mirrored at `crates/epiphany-core/DECISIONS.md:340` ("region origin assumed to be a barline (anacrusis/pickup deferred)"). **Not a duplicate of P13-S19**: it predates genesis tranche G3b, lives in the derived-notation splitter rather than the graph model, and does not touch invariant 20 or `CreateMeasure` at all — a pickup measure can now be *authored* (P13-S19's corrected scope) with no effect whatsoever on this splitter's own barline assumption. The two entries are filed separately because they own different subsystems' work — merging them would conflate a graph-model rung with a derived-notation one — and both wait on the same underlying capability: a per-measure partial-duration notion neither rung introduces. See also **P13-S19** | `core_spec.tex:2484` and `crates/epiphany-core/DECISIONS.md:340` (mirrored deferral sites; filed 2026-07-31 during `spec/CONTRACT_P13S19_PARTIAL.md`'s drafting, pin 6) | **open.** No code owed by this rung — filed so the deferral is discoverable on its own terms, independent of P13-S19, with which it shares a root cause but not a subsystem | | P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 16–18), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions | | P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 16–18 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it | | P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 24–29 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 35–38 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 2–15, 17–23, and 30–33 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548`–`:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental** — `ops/src/vectors.rs:201`–`:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the six scattered fragments rather than adding a seventh — a seventh band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** | diff --git a/spec/core_spec.pdf b/spec/core_spec.pdf index 9b41cff..bf3ceaa 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 97cf78f..292b813 100644 --- a/spec/core_spec.tex +++ b/spec/core_spec.tex @@ -6629,8 +6629,16 @@ The score graph maintains a set of structural invariants. Implementations raises no violation --- wherever the comparison or the distance cannot be decided (base-ingested data may predate this rule); this is deliberate abstention, not a soundness - gap. A pickup/anacrusis first measure has no predecessor and - is never flagged. + gap. A pickup/anacrusis first measure has no predecessor, so + only the BOUNDARY clause is vacuous for it; the AGREEMENT + clause is not predecessor-dependent and still applies (unless + \texttt{time\_signature} is \texttt{None} or agrees with the + governing grid). Regardless of what the pickup itself + declares, its successor's boundary distance is measured + against this same governing signature's full + \texttt{measure\_duration()}, and IS flagged when that + distance is the pickup's own shorter length rather than a + full bar. \end{enumerate} Implementations \MUST{} reject graph configurations that violate any diff --git a/spec/operation_catalog.pdf b/spec/operation_catalog.pdf index 94303ec..bff93b3 100644 Binary files a/spec/operation_catalog.pdf and b/spec/operation_catalog.pdf differ diff --git a/spec/operation_catalog.tex b/spec/operation_catalog.tex index 897b7f1..d59c2d5 100644 --- a/spec/operation_catalog.tex +++ b/spec/operation_catalog.tex @@ -231,7 +231,7 @@ {\Large\scshape\color{epiphanyslate}Operation Catalog}\\[6pt] {\large\itshape\color{epiphanyslate}A companion to the Core Specification}\\[14pt] {\color{epiphanygold}\rule{3in}{0.8pt}}\\[24pt] - {\normalsize\color{epiphanyink}Version 0.13.0 --- The genesis operation tranche closes: \texttt{CreateMeasure} and graph invariant 20 (G3b)}\\[4pt] + {\normalsize\color{epiphanyink}Version 0.14.0 --- Pickup/anacrusis: what a partial measure actually costs (P13-S19)}\\[4pt] {\small\color{epiphanyslate}Normative for the operation kinds it defines} \vfill \end{titlepage} @@ -517,6 +517,31 @@ G2b left it. This closes the genesis ladder (\texttt{spec/PLAN\_GENESIS\_OPS.md} \S4): G1 $\rightarrow$ G2a $\rightarrow$ G-minor $\rightarrow$ G2b $\rightarrow$ G3a $\rightarrow$ G3b. +\medskip + +\noindent\textbf{Version 0.14.0 (P13-S19, correction and observation, +\texttt{spec/CONTRACT\_P13S19\_PARTIAL.md}).} No payload byte changes, no +behaviour change: \texttt{create\_measure} and graph invariant 20 are +byte-identical to 0.13.0. Corrects this section's ordering and +boundary-distance description above, which read as though a pickup/anacrusis +first measure --- and everything downstream of it --- were simply exempt. A +first measure skips only the \emph{predecessor-dependent} clauses (ordering +and boundary distance) for lack of a predecessor, and the agreement clause +only when it declares \texttt{None} or a signature that agrees with the +governing grid; a disagreeing declared signature is refused +(\texttt{MeasureMeterMismatch}) even on a first measure, since agreement is +not predecessor-dependent. Independently of what the pickup itself declares, +its \textbf{successor} is measured against the governing signature's full +\texttt{measure\_duration()} regardless, and is refused +(\texttt{MeasureMeterMismatch}) and flagged by invariant 20 whenever the +pickup's actual length is shorter than a full bar --- which, for an authored +pickup, it always is. The same gap applies to any partial measure at any +position, not only a first one: a mid-score partial measure is itself +unexamined at creation (nothing checks its own length), while \emph{its} +successor is refused the identical way. Closing this needs a per-measure +duration concept this rung does not introduce +(\texttt{spec/PASS13\_CANDIDATES.md}, P13-S19, still open). + % =========================================================================== \chapter{The Catalog Framework} \label{ch:framework} @@ -1675,19 +1700,25 @@ every non-\texttt{WallClock} referent of \texttt{measure.start} (an \textbf{Ordering and boundary-distance preconditions (core specification \sectionsc{Graph Invariants}, invariant 20).} Graph-aware, against the current last live measure of the same instance (vacuous for an instance's first -measure --- a pickup/anacrusis is never refused or flagged on this account): -the carried \texttt{start} must be \textbf{comparable} to the predecessor's -start and \textbf{strictly after} it (else \texttt{MeasureOutOfOrder}), and, -when a governing time signature is determinable, the \textbf{musical delta} -between the two starts must equal that signature's -\texttt{measure\_duration()} (else \texttt{MeasureMeterMismatch}). Either -comparison being \textbf{unverifiable} --- the two starts are not comparable, -or the delta is not computable --- refuses with -\texttt{MeasureOrderUnverifiable} rather than silently permitting an -unverifiable mint. A resolving \texttt{time\_signature} that \textbf{disagrees} -with the effective grid's active signature at the measure's start also refuses -with \texttt{MeasureMeterMismatch}; \texttt{time\_signature: None} skips only -this agreement check, not the boundary-distance check above. +measure's own ordering and boundary-distance clauses, for lack of a +predecessor to compare against --- but \textbf{not} for that same pickup's own +successor, which is checked against this same governing signature's full +\texttt{measure\_duration()} from the pickup's start, and refuses with +\texttt{MeasureMeterMismatch} when the pickup's actual, shorter length +disagrees with it): the carried \texttt{start} must be \textbf{comparable} to +the predecessor's start and \textbf{strictly after} it (else +\texttt{MeasureOutOfOrder}), and, when a governing time signature is +determinable, the \textbf{musical delta} between the two starts must equal +that signature's \texttt{measure\_duration()} (else +\texttt{MeasureMeterMismatch}). Either comparison being \textbf{unverifiable} +--- the two starts are not comparable, or the delta is not computable --- +refuses with \texttt{MeasureOrderUnverifiable} rather than silently permitting +an unverifiable mint. A resolving \texttt{time\_signature} that +\textbf{disagrees} with the effective grid's active signature at the +measure's start also refuses with \texttt{MeasureMeterMismatch} --- this +agreement check is \textbf{not} predecessor-dependent and applies to a first +measure like any other; \texttt{time\_signature: None} skips only this +agreement check, not the boundary-distance check above. \textbf{The effective grid} is \texttt{StaffInstance.local\_metric\_grid} when present, else the enclosing region's default metric grid, reconstructed from