362 lines
21 KiB
Markdown
362 lines
21 KiB
Markdown
# Contract — P13-S18: the invariant-20 outcome matrix
|
||
|
||
**Status:** RATIFIED.
|
||
|
||
**Rung type:** diagnostic and bookkeeping. **No behaviour change.** No graph that
|
||
violates invariant 20 today may stop violating it, and no graph that passes today
|
||
may start violating it. If the work suggests otherwise, **stop** (§1 pin 6).
|
||
|
||
---
|
||
|
||
## §0. What was verified before drafting
|
||
|
||
Every claim below was read out of the working tree at `cc49533`, not recalled,
|
||
and re-confirmed unaffected at `f33673d` (see §4).
|
||
|
||
1. **`check_measure_meter_consistency` has nine non-success paths**, not the five
|
||
an earlier scoping note claimed. Enumerated with line numbers in pin 1.
|
||
2. **Only three are abstentions.** The other six are one inapplicability, two
|
||
delegations, two vacuities, and one separately-filed deferral (pin 2).
|
||
3. **Invariant 10 really does own the two delegated paths.**
|
||
`invariants.rs:1220`ff checks that time-signature references resolve *"at
|
||
every level a `MeterChange` can appear"* and its loops cover **per-measure**
|
||
(`si.measures`, emitting `"measure {:?} time signature {:?} is not
|
||
declared"`), **instance-local grids** (`si.local_metric_grid`), the
|
||
**region-default grid**, and the **metric time model's own meter sequence**.
|
||
4. **P13-S18's "`Measure` *end* anchor" claim is wrong only in its "any", and
|
||
two successive scoping notes each overcorrected it.** The first called the
|
||
claim simply false; the second called it merely misattributed. The precise
|
||
position has three parts, all read out of `measure20_comparable_order`:
|
||
- **Same id, same position — `End`↔`End` is comparable *when its offsets
|
||
compare*.** c2 requires `ia == ib && pa == pb` and then delegates to
|
||
`measure20_offset_order`, which returns `None` for `Musical`↔`WallClock`
|
||
(`:2428`–`:2429`). So "any `Measure` end anchor" is false as written, but
|
||
the counter-example is conditional and must be stated that way.
|
||
- **Distinct ids — `End` anchors remain incomparable**, because c3 returns
|
||
`None` unless `*pa == MeasurePosition::Start` with both offsets `Zero`. A
|
||
vector index orders measure *reference points*, not arbitrary points near
|
||
them. Distinct-id `End` anchors therefore genuinely do reach **A4, B4 and
|
||
B5**, and are a real residue shape.
|
||
- **The resolver citation describes the missing duration machinery, not
|
||
invariant 20's execution path.** `resolve_anchor`'s `Measure` arm
|
||
(`invariants.rs:503`–`:516`) returns `None` for any `position !=
|
||
MeasurePosition::Start` because a measure's length "needs the deferred
|
||
decomposition/tempo machinery" — a true statement about *why* the duration
|
||
is unavailable. **Invariant 20 never calls it: zero occurrences in
|
||
`:2636`–`:2725`.** The citation explains the underlying gap; it does not
|
||
describe how invariant 20 reaches its abstentions.
|
||
|
||
The `invariants.rs:400` line number is separately stale (§0.7).
|
||
5. **P11-C5 is not P13-S18's gate.** `PASS11_WORKLIST.md:159` defines it as the
|
||
*"nearest surviving anchor" stand-in* — a re-anchoring proximity metric that
|
||
*"resolves when the graph-mutation phase tracks resolved positions"*. The G3b
|
||
contract cites it correctly but **narrowly**, for the two-distinct-`Event`s
|
||
case, via `PositionOutsideRegion`'s Reserved note (`effect.rs:139`–`:142`).
|
||
The capability P13-S18 waits on — placing on a common timeline **any pair
|
||
c1–c5 cannot order, and any pair it orders without yielding a usable musical
|
||
delta** — is strictly broader and is owned by **no filed candidate**. Pin 10
|
||
is the authoritative scoping; this item must not restate it more narrowly.
|
||
6. **Step 0 is per measure reference.** `measure20_governing_by_anchor` is
|
||
called once per measure with that measure's own `start`, and
|
||
`measure20_comparable_order` is a property of the *pair*. An incomparable
|
||
meter change therefore disables agreement for every measure whose start is
|
||
incomparable **to it** — not for every measure in the instance, when the
|
||
instance's measures carry heterogeneous anchor shapes. An earlier scoping
|
||
note said "every measure in that instance"; that was wrong and pin 7 locks
|
||
the correction behaviourally rather than in prose.
|
||
7. **The G3b contract's `invariants.rs:400`ff citation (`:206`) has drifted.**
|
||
The resolver it describes now begins at `invariants.rs:466`, with the
|
||
`Measure` arm at `:503`–`:516`. The paragraph's own narrower claim — that
|
||
cross-boundary comparison stays unverifiable without the boundary's
|
||
duration — remains **correct** and is not touched (pin 9).
|
||
|
||
---
|
||
|
||
## §1. Pins
|
||
|
||
**Pin 1 — the nine paths, and their sites.** These are exhaustive over
|
||
`check_measure_meter_consistency` (`invariants.rs:2636`). Any tenth found during
|
||
execution is a finding, reported before proceeding.
|
||
|
||
| Id | Clause | Path | Site |
|
||
|---|---|---|---|
|
||
| A1 | agreement | `m.time_signature` is `None` | `:2661` |
|
||
| A2 | agreement | declared signature does not resolve | `:2662` |
|
||
| A3 | agreement | `Governing20::None` | `:2675` |
|
||
| A4 | agreement | `Governing20::Indeterminate` | `:2677` |
|
||
| B1 | boundary | first measure (`i == 0`) | `:2683` |
|
||
| B2 | boundary | governing signature does not resolve | `:2689`–`:2693` |
|
||
| B3 | boundary | `Governing20::None` | `:2717` |
|
||
| B4 | boundary | `Governing20::Indeterminate` | `:2719` |
|
||
| B5 | boundary | musical delta not computable | `:2713` |
|
||
|
||
**Pin 2 — the classification, ratified.** Six labels. Every path takes exactly
|
||
one.
|
||
|
||
| Id | Class | Why |
|
||
|---|---|---|
|
||
| A1 | **inapplicable** | no declared signature can disagree with anything; pin 9b makes `None` avoid *only* this clause, never the boundary clause |
|
||
| A2 | **delegated** | invariant 10, per-measure arm (§0.3) |
|
||
| A3 | **vacuous** | no governing signature exists to disagree with (pin 6c case 1) |
|
||
| A4 | **genuine abstention** | the relation cannot place a candidate |
|
||
| B1 | **P13-S19** | the pickup/anacrusis deferral, already filed |
|
||
| B2 | **delegated** | invariant 10, grid-level arms (§0.3) |
|
||
| B3 | **vacuous** | pin 6c case 1 |
|
||
| B4 | **genuine abstention** | as A4 |
|
||
| B5 | **genuine abstention** | order without distance |
|
||
|
||
**Exactly three genuine abstentions: A4, B4, B5.** This is the whole point of
|
||
the rung — P13-S18 currently presents all nine as one undifferentiated residue,
|
||
which both overstates the gap and hides which part of it is real.
|
||
|
||
**Pin 3 — delegation must be verified, not asserted.** A2 and B2 are classed
|
||
`delegated` only if some *other* invariant actually reports the condition. The
|
||
matrix must show, for each, that invariant 10 emits a violation on the same
|
||
graph — and M7/M8 must show that removing invariant 10's arm makes the condition
|
||
go **unreported by the whole suite**, not merely by invariant 20. A delegation
|
||
nobody discharges is an abstention wearing a better name.
|
||
|
||
**Pin 4 — the outcome matrix.** Rows are representative anchor shapes, columns
|
||
are the two clauses, each cell names the path id that fired and its class.
|
||
Minimum shapes:
|
||
|
||
| Shape | Description |
|
||
|---|---|
|
||
| S1 | `WallClock` start, `WallClock`-anchored meter changes |
|
||
| S2 | `WallClock` start, `Region`-anchored meter changes |
|
||
| S3 | `Region` same id, same edge, `Musical` offsets — fully decidable |
|
||
| S4 | `Measure` **same id, `pos: End` on both sides**, `Musical` offsets (c2) |
|
||
| S5 | `Measure` distinct ids, `Start`, `Zero` (c3) |
|
||
| S6 | `Event` same id, **live** event, `Musical` offsets (c1) |
|
||
| S7 | `Event` distinct ids, otherwise identical to S6 |
|
||
| S8 | matching referent, **differing** `pos`/`edge` selector |
|
||
| S9 | one instance, **heterogeneous** measure anchors (pin 7) |
|
||
|
||
**S6 and S7 are a positive/negative pair and neither may be dropped.**
|
||
`Measure.start` and `MeterChange.anchor` are unrestricted `TimeAnchor`s, so
|
||
`Event`-anchored measures are valid rather than hypothetical. S6 proves such a
|
||
measure genuinely reaches c1. S7 changes **only the referent identity** and
|
||
isolates the distinct-`Event` fall-through — which is precisely the case the
|
||
retained P11-C5 citation at `CONTRACT_GENESIS_G3B_MEASURE.md:223` exists for.
|
||
Both use live events and `Musical` offsets.
|
||
|
||
**S4 is the row that falsifies "any `End`", and it must do so by observation.**
|
||
It is deliberately an `End`↔`End` pair on the **same** measure id with `Musical`
|
||
offsets — c2's exact shape — and its meter changes carry the same anchor form,
|
||
so both clauses reach a decision. It is therefore `D`/`D` and, per the rule
|
||
below, deliberately wrong. S5 supplies the contrast on distinct ids. A contract
|
||
that only *stated* "same-id `End` is fine" would be repeating the mistake this
|
||
pin exists to correct.
|
||
|
||
**Every cell holds either a path id (A1–B5) or `D`.** A fully comparable shape
|
||
takes *none* of the nine paths — it decides — and a cell left blank because
|
||
"nothing fired" is indistinguishable from a cell nobody looked at. **Every `D`
|
||
fixture must be deliberately wrong**, so that the emitted violation is what
|
||
proves the clause decided. S3 and S6 are `D` in both columns; an S6 that emits
|
||
nothing has demonstrated nothing.
|
||
|
||
Every cell must be **observed**, never derived. A cell filled in by reading the
|
||
match arms and reasoning about which one wins is unsigned.
|
||
|
||
**Pin 5 — the `WallClock` finding, and the split an earlier draft got wrong.**
|
||
`valuegen::measure` (`ops/src/valuegen.rs:447`) anchors starts to
|
||
`TimeAnchor::WallClock`. An earlier draft of this contract said that shape makes
|
||
**both** clauses abstain. It does not, and the difference is the meter changes'
|
||
anchors, not the measures':
|
||
|
||
- **S1 — `WallClock` measures, `WallClock` meter changes.** The anchors are
|
||
mutually comparable under c5, so step 0 passes and a unique maximum is found:
|
||
**agreement decides.** But `measure20_musical_delta` never returns a
|
||
`WallClock` delta (`:2527`, `AnchorOffset::WallClock(_) => None`), so the
|
||
boundary clause takes **B5**.
|
||
- **S2 — `WallClock` measures, `Region` meter changes.** `comparable_order`
|
||
falls through to `_ => None`, so step 0 returns `Indeterminate`: agreement
|
||
takes **A4** and the boundary clause takes **B4** — *not* B5, because the
|
||
`Governing20` match short-circuits before the delta is ever computed.
|
||
|
||
**A `WallClock` start does not by itself disable both clauses.** The report must
|
||
state the split, must **not** claim `WallClock` is the dominant shape in real
|
||
scores (measure starts are author-supplied), and may claim only that it is the
|
||
shape this repository's fixture generator emits.
|
||
|
||
**Pin 6 — the hard stop.** No widening of `measure20_comparable_order` or
|
||
`measure20_musical_delta`. No new violation. No change to which graphs violate
|
||
invariant 20. The G3b contract holds that defining a new comparability relation
|
||
*"is a specification question this rung has no authority over"*, and that is
|
||
unchanged. **If the classification work suggests a behaviour change — including
|
||
"A3 should really be a violation" or "B2 should be reported here rather than by
|
||
10" — stop, report, and let it be split into a separately ratified semantic
|
||
rung.** Do not implement it here, and do not soften a class label to avoid
|
||
raising it.
|
||
|
||
**Pin 7 — step-0 scope, locked behaviourally.** S9 must contain one instance
|
||
whose measures carry heterogeneous anchor shapes, such that **one measure's
|
||
agreement clause abstains via A4 while another measure's agreement clause in the
|
||
same instance reaches a decision**. Prose asserting this is not enough; the row
|
||
is what forbids the "one incomparable change disables the whole instance"
|
||
overstatement from reappearing.
|
||
|
||
**Pin 8 — the P13-S18 correction.** Five defects, all of them mine:
|
||
1. three abstention shapes → **nine paths**, classified;
|
||
2. **correct**, not delete, the "`Measure` *end* anchor" claim, to all three
|
||
parts of §0.4: same-id `End`↔`End` is comparable under c2 **when its offsets
|
||
compare** — `measure20_offset_order` rejects `Musical`↔`WallClock` — so
|
||
"any" is false but conditionally so; distinct-id `End` anchors **are**
|
||
incomparable and do reach A4/B4/B5; and the resolver citation names the
|
||
missing duration machinery rather than invariant 20's execution path;
|
||
3. re-gate: not P11-C5, but the broader capability filed as P13-S23 (pin 10);
|
||
4. name A2/B2 as delegated to invariant 10 with its line, so the entry stops
|
||
counting them as gap;
|
||
5. state the S1 finding.
|
||
The entry stays **open** — A4, B4 and B5 remain real — but open at its true size.
|
||
|
||
**Pin 9 — the G3b contract corrections, two of them and both narrow.**
|
||
|
||
1. **`:347`** says the residue's closure needs "P11-C5 resolved positions". That
|
||
is the overbroad claim. Correct it to name P13-S23 as the owner of the
|
||
general case.
|
||
2. **`:206`** cites `invariants.rs:400`ff for the prototype anchor resolver. The
|
||
resolver now begins at `:466` with its `Measure` arm at `:503`–`:516`.
|
||
**Correct the line number only.** The paragraph's claim — that cross-boundary
|
||
comparison stays unverifiable without the boundary's own duration — is
|
||
correct, is narrower than P13-S18's use of it, and must survive verbatim.
|
||
|
||
**`:223`'s citation is correct and stays.** It cites P11-C5 for the
|
||
two-distinct-`Event`s case specifically, which is genuinely what
|
||
`PositionOutsideRegion`'s Reserved note (`effect.rs:139`–`:142`) covers.
|
||
**The contract is RATIFIED and its pins are not reopened**; both edits are
|
||
citation repairs, and neither changes a ratified claim.
|
||
|
||
**Pin 10 — P13-S23.** File the unowned capability: *placing anchor pairs on a
|
||
common timeline and measuring musical distance along it, wherever **c1–c5 do not
|
||
already yield both**.* Two disjoint deficiencies, and the candidate owns both:
|
||
|
||
1. **No ordering.** The pair is not comparable at all. The failure may be in the
|
||
**referent** (distinct `Event` ids, distinct `Measure` ids outside c3's
|
||
`Start`+`Zero` restriction), the **variant or selector** (`Event`↔`Measure`,
|
||
`Measure`↔`Region`, differing `pos`/`edge`), or the **clock**
|
||
(`Musical`↔`WallClock`, including inside `measure20_offset_order`). This is
|
||
what A4 and B4 are made of.
|
||
2. **Ordering without a usable delta.** The pair *is* comparable and still
|
||
yields no musical distance: **c3** supplies a vector index, which is an order
|
||
and never a distance; **c5** compares two `WallClock`s, and
|
||
`measure20_musical_delta` never returns a `WallClock` delta (`:2527`). This
|
||
is what **B5** is made of.
|
||
|
||
**Scoping this as "not directly comparable under c1–c5" would have excluded B5
|
||
entirely** — S5 is c3-comparable and S1 is c5-comparable, and both reach B5 — so
|
||
the candidate would have disowned a third of the residue it is filed to own. An
|
||
earlier draft also said "anchors of differing shapes", which additionally
|
||
excluded the same-variant cases (distinct `Event`s, distinct `Measure`s).
|
||
|
||
Explicitly **broader than P11-C5**, with the distinction stated: P11-C5 is a
|
||
re-anchoring proximity metric that waits on resolved positions; P13-S23 is the
|
||
timeline itself. Name its dependents: invariant 20's A4/B4/B5, and
|
||
`PositionOutsideRegion`'s Reserved status. Filed **open**; no code owed.
|
||
|
||
---
|
||
|
||
## §2. Touch table
|
||
|
||
| # | File | Change |
|
||
|---|---|---|
|
||
| 1 | `crates/epiphany-core/src/invariants.rs` | **tests only**, plus a doc-comment classification on `check_measure_meter_consistency` naming each of the nine paths and its class. The doc comment is not normative and changes no behaviour. **No production logic edit of any kind.** |
|
||
| 2 | `spec/PASS13_CANDIDATES.md` | P13-S18 corrected per pin 8; **P13-S23** filed per pin 10 |
|
||
| 3 | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` | `:347` (overbroad P11-C5 claim) and `:206` (stale resolver line number), per pin 9. `:223` untouched |
|
||
| 4 | this contract | DRAFT → RATIFIED |
|
||
|
||
**No `.tex` change and no PDF.** The classification describes existing
|
||
behaviour; it makes no normative claim. **If the classification turns out to
|
||
contradict `core_spec.tex`'s invariant-20 text, that is a finding — stop and
|
||
report it** (pin 6), because a spec correction is a semantic rung.
|
||
|
||
**No `DECISIONS.md` entry.** Consistent with the P13-S15 ruling: test coverage
|
||
and ledger bookkeeping, not a semantic ruling.
|
||
|
||
---
|
||
|
||
## §3. Mutation plan
|
||
|
||
Every mutation is a specific edit to a specific site, each **observed** red and
|
||
restored by hand-editing back. Never `git checkout`, never `git stash`.
|
||
|
||
| M | Edit | Row it signs |
|
||
|---|---|---|
|
||
| M1 | make A4's graph comparable (swap the incomparable meter change's anchor to the measure's own shape) | A4 is an abstention, not a pass: the agreement violation **appears** |
|
||
| M2 | as M1 for B4 | B4 is an abstention |
|
||
| M3 | swap S5's two measure starts to `Region` same-id `Musical` offsets | B5 is an abstention: the delta becomes computable and the boundary violation appears |
|
||
| M4 | give A1's measure a resolving `time_signature` that disagrees | A1 is inapplicable, not concealing: the violation appears |
|
||
| M5 | make **S2**'s meter-change anchors `WallClock`, matching its measures | pin 5's split: S2's cell pair moves **A4/B4 → D/B5** — agreement stops abstaining and decides, and the boundary clause moves from indeterminate selection to incomputable delta. Writing this as "A4/B4 → B5" is wrong: A4 is an agreement path and cannot appear in the boundary column. **S2 is the target, not S1** — S1's agreement clause already decides, so no mutation of S1 could show it begin to |
|
||
| M6 | in S9, give the second measure the first's incomparable anchor shape | pin 7: its agreement clause stops deciding — and **only** then |
|
||
| M7 | delete invariant 10's per-measure time-signature arm (`:1250`ff) | A2 is delegated: the condition becomes **unreported by the whole suite** |
|
||
| M8 | delete invariant 10's instance-local-grid arm | B2 is delegated, same standard |
|
||
| M9 | make B1's measure a non-first measure | B1 is the P13-S19 deferral, not a silent pass |
|
||
| M10 | remove B3's emptying filter so a governing signature exists and disagrees | B3 is vacuity, not concealment |
|
||
|
||
**Ten mutations.** Report the observed count; any deviation is a finding.
|
||
|
||
**Anti-traps, all earned in this session.** A mutation that does not compile
|
||
signs nothing. A mutation in an operation that runs *before* the asserted state
|
||
cannot reach it. A guard written against an index that structurally cannot hold
|
||
the referent is born green. Transaction-block members reduce atomically at the
|
||
*first* member's canonical position. Envelope counter gaps make operations
|
||
permanently pending, which makes fixtures silently vacuous. **And the one this
|
||
rung is most exposed to: a matrix cell that agrees with the prediction is the
|
||
easiest place in the world to stop looking.** Each cell must fail loudly if the
|
||
path it names is not the path taken — assert the *outcome*, and construct the
|
||
graph so no other path could have produced it.
|
||
|
||
---
|
||
|
||
## §4. Gate
|
||
|
||
- `cargo test --workspace` — baseline **1541 / 0**, confirmed at `f33673d`
|
||
(the commits between `cc49533` and it are `spikes/`-only, a separate
|
||
workspace, so the root count is unmoved); delta explained.
|
||
- `cargo clippy --workspace --all-targets` — zero warnings.
|
||
- `cargo fmt -p epiphany-core -- --check` — clean. **Never `cargo fmt --all`**;
|
||
it crosses into the `spikes/` workspace through path dependencies.
|
||
- All **10** mutations observed red and hand-restored.
|
||
- **A diff check that `check_measure_meter_consistency`'s executable body is
|
||
byte-identical to `cc49533`** — the doc comment may grow; not one line of
|
||
logic may move. This is the rung's central claim and must be mechanically
|
||
demonstrated, not asserted.
|
||
- `git diff --cached --check` clean; nothing from `spikes/` or `.claude/`
|
||
staged.
|
||
|
||
## §5. Whitespace and staging
|
||
|
||
1. Stage the touch-table files explicitly. **Never `git add -A`.**
|
||
2. `git diff --cached --check` — catches staged and formerly-untracked files.
|
||
3. Commit.
|
||
4. `git diff --check <parent>..HEAD -- crates/ spec/` — path-scoped.
|
||
|
||
**A concurrent session commits to this repository.** Re-check `HEAD` before
|
||
committing, and never run `git reset`, `git restore --staged`, `git checkout`,
|
||
or `git stash` against the shared index.
|
||
|
||
## §6. Boundary — unchanged and absolute
|
||
|
||
MUST NOT be read, written, or staged: `spec/PLAN_EDITOR_APP.md`,
|
||
`spec/CONTRACT_EDITOR_*.md`, `spec/ANALYSIS_GENESIS_PERSISTENCE.md`,
|
||
`spec/ANALYSIS_TEXT_RUN_PRIMITIVES.md`, `spec/DRAFT_T4_FIXTURE_RECIPE.md`,
|
||
`crates/epiphany-editor-gui/goldens/*.png`, `crates/epiphany-render-svg/**`,
|
||
`crates/epiphany-glyphs/**`,
|
||
`crates/epiphany-testkit/benches/editor_pipeline.rs`, the entire `spikes/`
|
||
tree, the root `Cargo.toml` change, `.claude/worktrees/`.
|
||
|
||
## §7. Report requirements
|
||
|
||
- The **full matrix — nine shapes × two clauses, 18 cells** — every cell
|
||
observed, each holding a path id or `D`, with the test name that observed it.
|
||
- All **10** mutations with their observed failing test names.
|
||
- Explicit confirmation that `check_measure_meter_consistency`'s logic is
|
||
byte-identical, with the command that showed it.
|
||
- Explicit confirmation that **no new violation** is emitted anywhere, and that
|
||
the workspace count moved only by the tests added.
|
||
- For A2 and B2: the invariant-10 violation text observed, and the M7/M8 result
|
||
showing the condition otherwise goes unreported.
|
||
- **Anything the contract did not anticipate** — a tenth path, a cell that
|
||
contradicts pin 2, or anything suggesting a behaviour change. Report it and
|
||
**stop**; do not implement it.
|