P13-S29 LANDED: the violation tag stops multiplexing
Graph invariant 10 reported Chapter 3 and Chapter 4 failures under its own number, through a public API. `InvariantViolation` becomes `WellFormednessViolation` carrying a two-armed `ViolationKind`: `Invariant` for a numbered graph invariant, `Requirement` for a normative rule named by its `req:` label. Invariant 10 keeps only reference resolution. `check_invariants` stays comprehensive, so every broad caller keeps its rule coverage; `check_invariant` narrows to the invariant arm and a symmetric `check_requirement` is added. Both are projections of the aggregate. Four rules move to their own labels, one of which this rung mints: `req:time:tempo-segment-shape`, stating the enforced shape/end_tempo compatibility without resolving P13-S8. `GraphInvariant` did not move: 21 variants, unchanged. 44 suites / 1606 passed / 0 failed / 0 ignored (1586 -> 1606, 43 -> 44) clippy -D warnings clean; fmt -p epiphany-core -p epiphany-testkit clean core_spec.pdf rebuilt, undefined references cleared Gates 1-16 pass; evidence in spec/EVIDENCE_P13S29_EXECUTION.md. All 54 mutations of §3 observed, none compile-only, none passing. Amendment 1 corrected M1·C6 and M1·C7 from one observer to two after measurement contradicted the derived cell. Six execution faults are recorded rather than left in the transcript, none a contract defect. Three are worth naming here because no tool would have caught them: - Pin 10's eleventh row was read as a note, not a test, so `reversed_aleatoric_bounds_stay_invariant_four` was never written. M11's cell named it, and the omission surfaced only as a radius mismatch. - `display_renders_each_arm_exactly` carried a comment stating its pinned fixture correctly above code that built a different one. Pin 10 had foreclosed the choice precisely because it moves radii; with the fixture repaired the test entered M11's cell and left M17·C1's, both as pinned. - Pin 9's `/// 10.` rider note was the one prose row left unmigrated, naming three labels where four were required and still filing the multiplexing as pending. Gate 16 states these outcomes have no machine observer; eight rows were verified by their own stale phrase, and the ninth was not there. Gate 10 rejected the ledger append over one character: the artifact read 2026-08-12 where pin 13 pins 2026-08-11. The artifact was corrected to the pin, and the date question is flagged for the owner as a possible administrative amendment rather than settled here. CLAUDE.md's baseline still reads 43 suites / 1586 tests and is not in the touch table; it follows in a separate reconciliation commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x
This commit is contained in:
parent
e7bd12c19e
commit
52fcf3739a
|
|
@ -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`
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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:?}"
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -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,
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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<WellFormednessViolation> = check_requirement;
|
||||
let _ = |k: &ViolationKind| matches!(k, ViolationKind::Requirement(_));
|
||||
}
|
||||
|
|
@ -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);
|
||||
|
|
|
|||
|
|
@ -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<String> {
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.*
|
||||
|
|
|
|||
File diff suppressed because one or more lines are too long
Binary file not shown.
|
|
@ -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}
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue