neuwirth
/
epiphany
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
epiphany/spec/CONTRACT_P13S18_MATRIX.md

21 KiB
Raw Blame History

Contract — P13-S18: the invariant-20 outcome matrix

Status: DRAFT.

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:1220ff 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 (:2427–:2428). 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-Events 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:400ff 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 TimeAnchors, 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:400ff 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-Events 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 WallClocks, 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 Events, distinct Measures).

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 (:1250ff) 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.