diff --git a/crates/epiphany-testkit/tests/binary_format_history.rs b/crates/epiphany-testkit/tests/binary_format_history.rs index dec1283..609441d 100644 --- a/crates/epiphany-testkit/tests/binary_format_history.rs +++ b/crates/epiphany-testkit/tests/binary_format_history.rs @@ -36,6 +36,13 @@ //! guard to its own Revision History row, closing the genesis ladder: the //! contract's own M71 deletes the G3b row, observes this guard fail, and //! restores it by hand. +//! +//! **P13-S21** extends the file past rung identity to one vocabulary gap of +//! the same shape: `PreconditionFailureReason` 14 and 15 entered at Push 4a +//! and reached this document at neither of the two places that owe them — +//! not the bounded enumeration that assigns discriminants, and not Push 4a's +//! own history row. See +//! `precondition_failure_reasons_14_and_15_are_documented` below. use std::fs; use std::path::Path; @@ -221,3 +228,87 @@ fn revision_history_g2b_row_states_what_g2b_did() { 2 -> 3: {row_segment:?}" ); } + +/// Slice one `longtable` row: from `marker` to the `\\` that terminates the +/// row. Rows in this document carry no internal `\\`, so the first +/// terminator after the marker ends that row and nothing else. +fn row_segment<'a>(haystack: &'a str, marker: &str) -> &'a str { + let offsets = find_all(haystack, marker); + assert_eq!( + offsets.len(), + 1, + "expected exactly one occurrence of the row marker {marker:?}, found {} \ + (offsets {offsets:?})", + offsets.len() + ); + let start = offsets[0]; + let end = haystack[start..] + .find(r"\\") + .map(|relative| start + relative) + .unwrap_or(haystack.len()); + &haystack[start..end] +} + +/// `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 +/// (`TranspositionOutOfRange`) entered the vocabulary at Push 4a — the +/// Operation Catalog documented both at its own 0.8.0, and `effect.rs` has +/// carried both ever since — but this document named neither anywhere, its +/// bounded enumeration running 13 straight to G3b's 16. That is P13-S21, and +/// it is why P13-S20's decoder could stop at 13 unchallenged: an implementer +/// reading only the wire specification would have built exactly that decoder +/// and been right. +/// +/// **Both sites are checked, each bounded to its own row**, because either +/// alone is satisfiable by the wrong thing. The G3b history row and the +/// bounded enumeration both discuss `PreconditionFailureReason` at length, so +/// an unbounded search for these names would go green the moment any row +/// mentioned them — the same hole P13-S17 was filed over, one vocabulary +/// down. No document version number appears here either; the Push 4a row is +/// located by its version-free `--- Transpose algebra (Push~4a)` separator +/// form, for the reason the module comment gives. +/// +/// The enumeration is asserted as a **discriminant/name adjacency**, since it +/// is the normative assignment and must be exact. The history row is asserted +/// by name and discriminant presence within its own bounded segment: it is +/// prose, its wording may legitimately be rewritten, and the bounding is what +/// makes presence load-bearing there. +#[test] +fn precondition_failure_reasons_14_and_15_are_documented() { + let source = binary_format_source(); + let normalized = normalize_whitespace(&source); + + let enumeration = row_segment( + &normalized, + r"\texttt{Precondition\allowbreak FailureReason} &", + ); + for pairing in [ + r"\tablenums{14} AcousticRealizationPinned", + r"\tablenums{15} TranspositionOutOfRange", + ] { + assert!( + enumeration.contains(pairing), + "the bounded PreconditionFailureReason enumeration does not assign \ + {pairing:?}; it is the normative discriminant assignment and the \ + pairing must be exact: {enumeration:?}" + ); + } + + let push4a = row_segment( + revision_history_slice(&normalized), + "--- Transpose algebra (Push~4a)", + ); + for owed in [ + "AcousticRealizationPinned", + "TranspositionOutOfRange", + r"\tablenums{14}", + r"\tablenums{15}", + ] { + assert!( + push4a.contains(owed), + "Push 4a's own Revision History row does not record {owed:?}. Both \ + reasons were appended in Push 4a's epoch alongside OperationKind 30, \ + and a row that records only the kind leaves the append unattributable: \ + {push4a:?}" + ); + } +} diff --git a/spec/CONTRACT_GENESIS_G3B_MEASURE.md b/spec/CONTRACT_GENESIS_G3B_MEASURE.md index 228e6c2..c1d7286 100644 --- a/spec/CONTRACT_GENESIS_G3B_MEASURE.md +++ b/spec/CONTRACT_GENESIS_G3B_MEASURE.md @@ -623,7 +623,16 @@ events only**: |---|---|---|---| | 10 | G2b | `13c3d2f` | 2026-07-29 | | 11 | G3a | `6c5e69f` | 2026-07-29 | -| 12 | G3b | this rung | — | +| 12 | G3b | `e64a4b7` | 2026-07-30 | + +**Closed by the pre-push repair.** G3b landed across six commits, so its row +needed the same distinction the 2026-07-28 correction draws for G2a: the +introducing commit is **`e64a4b7`** (packet 1), where kind/tag 39 enters +`ops/src/payload.rs` and reasons 16–18 enter `ops/src/effect.rs`. The four +commits after it introduce no discriminant, and the rung *completes* at +`d58eee8` (packet 3b, documentation). Recorded by the pre-push repair rather +than by G3b itself, because a commit cannot cite its own hash and G3b closed +the ladder — there was no later rung to fill it in. **G-minor and P13-S17 (`6170015`) do NOT belong in this chain** — G-minor built the epoch machinery and P13-S17 restored a document's history; neither diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 4f238a7..954b0c5 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -98,3 +98,4 @@ visible — a value with a wire form and no canonical carrier to reach it.) | P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, and nothing yet closes the residue.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 7) makes invariant 20 ABSTAIN — emit no violation — wherever pin 6's comparable relation cannot order two measure starts or pin 6b's musical delta cannot be computed between them: cross-clock offsets (`Musical` vs `WallClock`), differing boundary selectors (`pos`/`edge`), and any `Measure` *end* anchor (unresolvable without the deferred tempo/measure-length machinery, `invariants.rs:400`ff). This is deliberate — base-ingested data may predate the rule, so flagging every incomputable case would make the invariant useless on real scores — but it is a real gap: a score whose measure/meter disagreement happens to fall in one of these incomputable shapes passes invariant 20 silently | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 7 (filed 2026-07-30 during the G3b contract's own drafting, ratified as deliberate abstention rather than a defect) | **open, deliberately.** Closing it needs the deferred P11-C5 resolved-position machinery: once a `Measure` end, or an event position on a wall-clock-placed region, can be placed on a common timeline, the comparable relation and the musical delta both widen and the abstention residue shrinks. No code change is owed by G3b itself | | P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes | | P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 16–18), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions | +| P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 16–18 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it | diff --git a/spec/PLAN_GMINOR_SCHEMA_MINOR.md b/spec/PLAN_GMINOR_SCHEMA_MINOR.md index b24149e..6ce5ddd 100644 --- a/spec/PLAN_GMINOR_SCHEMA_MINOR.md +++ b/spec/PLAN_GMINOR_SCHEMA_MINOR.md @@ -199,8 +199,14 @@ numbering spaces are unrelated and must not be cross-read. > the rung's one kind and its three `PreconditionFailureReason` appends > together, the Push 4a precedent (epoch 7 bundled kind 30 with reasons 14–15) > rather than a kind epoch and a reason epoch separately. The introducing -> commit is this packet's own — the committing session owns `HEAD`, not this -> packet, so the hash is recorded once committed rather than invented here. +> commit is **`e64a4b7`** (2026-07-30), where kind/tag 39 enters +> `ops/src/payload.rs` and reasons 16–18 enter `ops/src/effect.rs` — G3b landed +> across six commits, and the four that follow packet 1 introduce no +> discriminant, exactly the distinction the 2026-07-28 correction below draws +> between `7df5ca1` and `55eff00`. The rung *completes* at **`d58eee8`** +> (2026-07-30), the documentation half; the hash was filled in by the pre-push +> repair that follows it, because a commit cannot cite itself and G3b closed +> the ladder, leaving no later rung to do it. > The ladder stays monotonic (G3b follows G3a) and prefix-closed. **The ladder is complete against the audit** — every post-baseline variant in @@ -215,8 +221,9 @@ introducing commits rather than assumed: M2c `a207077` (2026-06-25) → Push 3 `92aaccf` (07-02) → Phase-3 `0316160` (07-02) → G-pass `e4edea6` (07-07) → repeat pair `9b5339f` (07-07) → Push 4a `2740a6c` (07-09) → G1 `3b09595` (07-24) → **G2a `7df5ca1`** (07-28) → **G2b `13c3d2f`** (07-29) → **G3a -`6c5e69f`** (07-29) → **G3b** (this packet's own commit — the committing -session owns `HEAD`, hash recorded there rather than invented here). The two +`6c5e69f`** (07-29) → **G3b `e64a4b7`** (07-30, the packet-1 commit where +kind/tag 39 and reasons 16–18 enter the vocabularies; the rung completes at +`d58eee8`, which introduces no discriminant). The two events sharing 2026-07-07 are ordered correctly: the G-pass precedes the repeat revision. The two events sharing 2026-07-29 are ordered **by ancestry, not timestamp**: `13c3d2f` is an ancestor of `6c5e69f` (verified with diff --git a/spec/binary_format.pdf b/spec/binary_format.pdf index 8fb792e..9b10fdf 100644 Binary files a/spec/binary_format.pdf and b/spec/binary_format.pdf differ diff --git a/spec/binary_format.tex b/spec/binary_format.tex index c9aaf6a..5224bea 100644 --- a/spec/binary_format.tex +++ b/spec/binary_format.tex @@ -1637,6 +1637,8 @@ trailing bytes are decode errors. \tablenums{11} TempoMapMalformed; \tablenums{12} SystemDerivedContentImmutable (Pass~12, P12-K3); \tablenums{13} RecreateContentMismatch (Pass~12, P12-K9); + \tablenums{14} AcousticRealizationPinned; + \tablenums{15} TranspositionOutOfRange (both Push~4a); \tablenums{16} MeasureMeterMismatch, \tablenums{17} MeasureOutOfOrder, \tablenums{18} MeasureOrderUnverifiable (genesis tranche G3b). \\ \texttt{RepairRecord} & @@ -3548,10 +3550,17 @@ only}: implementations need not agree on an error taxonomy. $\mathrm{seq}^{\Uparrow}$ notation (strictly increasing; a decoder \MUST{} reject a duplicate rather than normalize it) and marks \tablenums{9} (\texttt{Transpose}) frozen, its - $\mathrm{seq}^{\uparrow}$ being a multiset. No existing assignment - changed. Semantics: Operation Catalog \sectionsc{TransposeInterval}, - 0.8.0; algebra: core Chapter~2, \sectionsc{Transposition and the - Interval Type}. \\ + $\mathrm{seq}^{\uparrow}$ being a multiset. Appends two + \texttt{PreconditionFailureReason} discriminants in the same epoch, + \tablenums{14} (\texttt{AcousticRealizationPinned}: a target whose + \texttt{AcousticRealization::AbsoluteHz} overrides the tuning system, so + moving its scale position would move the notehead without moving the + sound) and \tablenums{15} (\texttt{TranspositionOutOfRange}: an + \texttt{alteration} or \texttt{octave} driven past its \texttt{i8} + bound, where the frozen \tablenums{9} saturates and reports success). + No existing assignment changed. Semantics: Operation Catalog + \sectionsc{TransposeInterval}, 0.8.0; algebra: core Chapter~2, + \sectionsc{Transposition and the Interval Type}. \\ \today & Chunk references & 0.8.0 --- Strict \texttt{CompressionAlgorithm} decode (Push~5, P3): \texttt{req:binfmt:compression-none-parameter} \MUST{} reject a non-zero parameter byte on the \texttt{None} discriminant. Ignoring