From ab430ec52df3c77d9642c5349635bfda1405b2db Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Fri, 31 Jul 2026 17:50:02 -0400 Subject: [PATCH] Contract for P13-S19, tracked as DRAFT before dispatch P13-S19 is filed as a deferral. It is closer to a live defect, and the tree already contains the proof: m35_boundary_flags_wrong_distance places a first measure at offset 0 and its successor half a whole note later, under a signature whose measure_duration is a whole, and asserts invariant 20 fires. That is a pickup, and the test has been labelled "wrong distance" since packet 2. create_measure applies the same rule as a refusal. So authoring a pickup does not merely leave it unmodelled -- it makes the rest of the instance unauthorable. The rung corrects seven surfaces, three of them normative, one of them outright false: ops/DECISIONS.md says all three CreateMeasure clauses are vacuous for a first measure, and the agreement clause has no predecessor dependency at all. It observes the reducer refusal rather than citing it, files the Chapter 3 splitter deferral as its own candidate, and introduces no partial-measure notion -- that is a semantic rung and pin 9 stops this one at its edge. Three over-readings committed while drafting are recorded inside the contract rather than smoothed away, because text that is locally true and globally misleading is the rung's own subject. It claimed a pickup is "neither refused nor flagged" (the agreement clause runs on a first measure); it claimed that again more weakly after the first fix (referential preconditions and invariant 10 still apply); and it listed core/DECISIONS.md as an understated surface by matching "never flagged" without reading the qualifier that makes it correct. That file is now explicitly out of bounds, with the reason, so a later reader comparing it against the corrected ops entry does not "fix" the one site that already draws the distinction. The absence gate replaces a grep that could not fail. Two of its seven phrases straddle a newline, so a line-oriented search would have returned nothing before the correction as well as after; the gate normalizes whitespace, and all seven anchors were confirmed present at 339269b so it fails today and can pass only once the work lands. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV --- spec/CONTRACT_P13S19_PARTIAL.md | 324 ++++++++++++++++++++++++++++++++ 1 file changed, 324 insertions(+) create mode 100644 spec/CONTRACT_P13S19_PARTIAL.md diff --git a/spec/CONTRACT_P13S19_PARTIAL.md b/spec/CONTRACT_P13S19_PARTIAL.md new file mode 100644 index 0000000..74a0cb2 --- /dev/null +++ b/spec/CONTRACT_P13S19_PARTIAL.md @@ -0,0 +1,324 @@ +# Contract — P13-S19: what a partial measure actually costs + +**Status:** DRAFT. + +**Rung type:** correction and observation. **No behaviour change.** Not one +graph's invariant-20 verdict may move, and not one operation's effect may +change. The rung makes the tree say what it already does. + +--- + +## §0. What was verified before drafting + +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 + 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 + successor — a pickup — and the test passes today inside the 1556. It has + been labelled "wrong distance" since packet 2. +2. **`create_measure` applies the same rule as a refusal.** Clause 3 + (`reduce.rs:5548`ff) resolves the governing signature at `prev_start`, then + `(Some(_), Some(_)) => MeasureMeterMismatch` when the delta differs from + `measure_duration()`. **Read, not executed** — pin 4 makes observing it a + deliverable, because this rung's headline claim rests on it. +3. **The exemption is index-based, not partial-aware, and it is narrower than + an earlier draft of this contract claimed.** Invariant 20 skips only the + *boundary* clause at `i == 0`; `create_measure` skips only clauses 1 and 3 + when `predecessor` is `None`. **The agreement clause is not + predecessor-dependent**: `invariants.rs:2684`ff evaluates it *before* the + `i == 0` bypass, and `reduce.rs:5526`ff is ungated. Neither asks whether any + measure is partial. +4. **Seven surfaces carry the understated form**, three of them normative + documents and one of them outright **false**: + + | # | Site | Form | + |---|---|---| + | a | `spec/PASS13_CANDIDATES.md`, the P13-S19 row | "MUST NOT be refused or flagged by either" | + | b | `crates/epiphany-core/src/graph.rs:598`–`:599` | "never refused or flagged by this rung" | + | 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") | + | 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 + catalog and then rows a/b/g. They are included because the scope's own + reasoning applies to each verbatim: narrow literal truth leaving the + misleading conclusion intact. + + **`crates/epiphany-core/DECISIONS.md:1559`–`:1560` is NOT a surface and MUST + NOT be edited.** An earlier draft of this contract listed it as one, having + matched the phrase "never flagged" without reading its qualifier. It reads + "has no predecessor and is therefore never flagged **by the boundary + clause**" — accurate, correctly scoped, and the only site in the tree that + already states the distinction this whole rung exists to draw. It is recorded + here so that a later reader comparing it against the corrected row **g** does + not "fix" it into agreement and destroy the one correct statement. +5. **A fifth pickup surface is a different deferral.** `core_spec.tex:2484` says + the integer-grid metric splitter "assumes the region origin falls on a + barline (anacrusis/pickup handling deferred)". Chapter 3, derived notation, + predating G3b, filed nowhere. Pin 6. +6. `grep -rn "pickup\|anacrusis" spec/*.tex` returns **exactly** those three + `.tex` sites. There is no fourth to miss. +7. `operation_catalog.tex` is at **0.13.0** (title `:234`, changelog `:481`). + `core_spec.tex` carries no title-page version and never has. +8. **§4's absence gate was proven non-vacuous before ratification.** All seven + phrases were confirmed **present** in their files at `339269b` under the + gate's own normalization, and the positive check confirmed present — so the + gate **fails today** and can pass only once the corrections land. A gate that + already passes before the work is done proves nothing, which is the defect + the bare `grep -rn "pickup\|anacrusis"` would have shipped. + +--- + +## §1. Pins + +**Pin 1 — the real consequence, stated exactly, and the exemption's true +width.** A first measure is exempt from the **predecessor-dependent** checks +only: invariant 20's boundary clause (`i == 0` → `continue`) and +`create_measure`'s clauses 1 and 3 (`predecessor: None`). **The agreement clause +is not predecessor-dependent and applies to a first measure like any other** — +so a pickup carrying a **resolving signature that disagrees with the governing +grid is flagged by invariant 20 and refused by `create_measure` with +`MeasureMeterMismatch`.** An earlier draft of this contract said a pickup "is +itself neither refused nor flagged"; that was wrong, and it is the same +over-reading the rung exists to correct, committed inside the correction. + +**What a first measure avoids is exactly this and no more:** the +predecessor-dependent checks, plus the agreement check when it declares `None` +or a matching signature — **and only when its other preconditions are +satisfied.** It can still be refused for a dead parent `StaffInstance`, an +unresolving `measure.time_signature` referent, or an unresolving referent of +`measure.start`; and invariant 10 can still flag an unresolved signature +reference on it. "A pickup is not refused or flagged" is false as a general +claim in **both** directions, and the corrected text must not trade one +over-reading for another. + +**Its successor is measured against the governing signature's full +`measure_duration()`, and is refused (`MeasureMeterMismatch`) by +`create_measure` and flagged by invariant 20.** The old ledger form — "a partial +first measure MUST NOT be refused or flagged by either" — is true only of the +pickup itself, only under the conditions above, and reads as "pickups work". + +**Pin 2 — the scope, corrected.** P13-S19 covers **boundaries following any +partial measure**, not "every partial measure". The check compares +`prev.start → current.start`, so a **mid-score partial may itself enter +successfully** — nothing examines its own duration — while **its successor is +what exposes the partial duration and fails**. The failure is always attributed +to the measure *after* the partial one, which is also why the witness text names +the wrong measure. Mid-score partials have **no exemption at all**, unlike the +first measure. + +**Pin 3 — the root cause is a missing quantity, not a missing exemption.** Both +rules compare `delta(prev.start, m.start)` against the *governing signature's* +`measure_duration()`, when the distance actually equals **`prev`'s own content +duration**. Those coincide only for full measures. Closing this needs a +per-measure duration — the "partial measure" notion the entry correctly names — +and **this rung does not introduce it.** Widening the exemption instead would +suppress the symptom and lose real violations. + +**Pin 4 — the reducer refusal must be observed, not read.** The conclusion is +incomplete until `create_measure` is driven end-to-end through the envelope +harness (`g3b_region_and_instance_envs` / `prim_env` / +`g3b_region_anchor`, modelled on `g3b_create_measure_ordering_agreement_boundary`, +`reduce.rs:19573`) and observed returning +`NoOp { PreconditionFailedUnderReduction { MeasureMeterMismatch } }` for the +successor of a pickup. **The same test must observe the pickup's own mint +`Applied`** — that is pin 1's true half, and asserting only the refusal would +leave it unsigned. + +**The pickup must carry `time_signature: None` or a signature that matches the +governing grid.** Per pin 1 the agreement clause runs on a first measure, so a +pickup declaring a mismatching signature is refused by **clause 2** — and the +test would then observe a `MeasureMeterMismatch` that has nothing to do with +partiality, while appearing to confirm exactly this rung's claim. Both refusals +carry the *same reason code*, so the fixture is the only thing separating them. +The report must state which form the pickup used. + +**Pin 5 — `m35` records what it demonstrates.** Rename and extend it so the tree +says it is the pickup case. **Its existing assertion may not be weakened**: it +must still fire, for the same reason, on the same shape. Extension only. + +**Pin 6 — P13-S24, filed separately and cross-linked.** The Chapter 3 splitter +deferral (`core_spec.tex:2484`, mirrored at +`crates/epiphany-core/DECISIONS.md:340`, "barline (anacrusis/pickup deferred)") +gets its own candidate. It **shares the missing partial-duration concept** with +P13-S19 and is otherwise **independent**: it affects **derived notation**, not +invariant 20 and not `CreateMeasure`. Each entry links the other, and P13-S24 +names both of its sites so the next reader does not have to rediscover the +mirror the way this contract rediscovered surface h. Filing it inside S19 would merge two subsystems' work +into one id; leaving it unfiled is what let it sit invisible since Chapter 3. + +**Pin 7 — the catalog pays the full ritual.** `operation_catalog.tex:1678` is +normative. Correct it to state the real behaviour: the first measure skips its +predecessor check, **and its successor is still checked against a full +`measure_duration()` and refused**. Then **0.13.0 → 0.14.0** on the title page +(`:234`), a changelog paragraph modelled on `:481`'s, and a regenerated PDF. +`core_spec.tex:6632` gets the same correction; it carries no version, so it +needs only the text and its PDF. + +**Pin 8 — a workaround may not be named unless it is executed.** Reading +suggests a pickup carrying its own shorter meter change satisfies clause 3, +because the governing signature at `prev_start` becomes the short one. +**Unverified.** If any corrected text names a workaround, a test must observe +it end-to-end; otherwise no text may name one. A normative document acquiring an +untested recommendation is how the last four rungs' defects started. + +**Pin 9 — the hard stop.** No production logic edit. No change to any +invariant-20 verdict or any operation effect. `check_measure_meter_consistency` +and `create_measure` both stay byte-identical. **If the work suggests the +current behaviour is wrong rather than merely undocumented — including "the +successor should be exempt" — stop and report.** That is a semantic rung and it +needs the partial-duration notion first. + +--- + +## §2. Touch table + +| # | File | Change | +|---|---|---| +| 1 | `crates/epiphany-core/src/invariants.rs` | **tests plus doc only** — pin 5's rename/extension of `m35`; surface **f** (`m38`'s name, comment, assertion message); surface **e** (the public doc comment on `GraphInvariant::MeasureMeterConsistency`, `:111`–`:112`) | +| 2 | `crates/epiphany-core/src/graph.rs` | surface **b**, the `Measure` doc comment (`:598`–`:599`) | +| 3 | `crates/epiphany-ops/src/reduce.rs` | **tests only** — pin 4's observed refusal, plus the mid-score case of pin 2 | +| 4 | `spec/operation_catalog.tex` | surface **c** (`:1678`); title `:234` 0.13.0 → **0.14.0**; changelog paragraph | +| 5 | `spec/core_spec.tex` | surface **d** (`:6632`–`:6633`). **No version bump** — this document has none | +| 6 | `spec/operation_catalog.pdf`, `spec/core_spec.pdf` | regenerated, **after** their sources are final | +| 7 | `spec/PASS13_CANDIDATES.md` | surface **a** — P13-S19 corrected per pins 1–3; **P13-S24** filed per pin 6 | +| 8 | `crates/epiphany-ops/DECISIONS.md` | surface **g**, `:2161` — repair the **false** "all three clauses are vacuous" | +| 9 | this contract | DRAFT → RATIFIED | + +**Nine rows. `crates/epiphany-core/DECISIONS.md` is NOT among them** — see +§0.4's closing note. It is correct as written and is out of bounds for this +rung. + +**No `binary_format.tex`** — no wire, discriminant, or accept-set change. + +**Rows 8 and 9 do not overturn the standing "no `DECISIONS.md` entry" ruling.** +That ruling says this class of rung adds no new record, and it holds: nothing is +appended. What rows 8 and 9 do is **repair statements already there that are +false or misleading**, which no ruling protects. Row 8 in particular is the only +place in the tree where the understatement has hardened into an outright false +claim. + +--- + +## §3. Mutation plan + +| M | Edit | Row it signs | +|---|---|---| +| M1 | in the extended `m35`, change `m1`'s offset from `Musical(1/2)` to a full `measure_duration` | invariant 20 fires **because** the predecessor is partial, not for some other reason | +| M2 | in pin 4's reducer test, move the successor to a full `measure_duration` after the pickup | the refusal is the partial distance: the effect becomes `Applied` | +| M3 | in pin 4's reducer test, repoint the `Applied` assertion at the **successor's** already-executed effect — the `NoOp` in the same harness | the pickup's `Applied` assertion is *precise*, not merely satisfied: it fails when aimed one operation over. No new fixture; a separate refusal fixture would test a different graph, not this assertion | +| M4 | in the mid-score test, move the **successor** to one full `measure_duration` after the partial measure | pin 2: the failure follows the partial predecessor, and a mid-score partial has no exemption. **There is no "make the measure full" edit** — `Measure` carries no duration field, and pin 3 is precisely that its length is inferred only from its successor's start | + +**Four mutations, one edit each.** Each observed red and restored by +hand-editing back — never `git checkout`, never `git stash`. Report the observed +count; any deviation is a finding. + +**Prose-only surfaces have no mutation** — surfaces a, b, c, d, e, g. They +are covered by the §4 grep gate, and the report must say so rather than implying +mutation coverage. Surface **f** is the exception: `m38` is a test, so its +corrected assertion message must still describe an assertion that actually +holds, and pin 5's no-weakening rule applies to it as it does to `m35`. + +**Anti-traps.** A mutation that does not compile signs nothing. Envelope counter +gaps make operations permanently pending — a reducer fixture whose ops never +execute asserts nothing, and the refusal this rung exists to observe would be +indistinguishable from an op that never ran. **Assert the pickup's mint +`Applied` before asserting the successor's `NoOp`**, so a vacuous fixture cannot +masquerade as a refusal. Transaction-block members reduce atomically at the +first member's canonical position. + +--- + +## §4. Gate + +- `cargo test --workspace` — baseline **1556 / 0** at `339269b`; delta explained. +- `cargo clippy --workspace --all-targets` — zero warnings. +- `cargo fmt -p epiphany-core -p epiphany-ops -- --check` — clean. **Never + `cargo fmt --all`**: it crosses into the `spikes/` workspace. +- All **4** mutations observed red and hand-restored. +- **Byte-identical bodies** for `check_measure_meter_consistency` **and** + `create_measure`, demonstrated mechanically against `339269b`. State the + command and paste its output. +- **The absence gate.** A bare `grep -rn "pickup\|anacrusis"` is + **non-discriminating** — it lists occurrences and succeeds whether every + obsolete claim survives or not. It is replaced by an **absence check on seven + specific phrases**, each in its own file, plus one **positive** check. + + **Whitespace must be normalized before matching.** Phrases **d** and **g** + straddle a newline in their sources today (`core_spec.tex:6632`–`:6633`, + `ops/DECISIONS.md:2160`–`:2161`), so a line-oriented search for either would + return nothing **before** the correction as well as after — born green, the + same defect in the opposite direction. The gate must read each file whole, + collapse whitespace runs to a single space, and strip `///`, `//!`, and `//` + markers, before searching. + + | # | File | Phrase that MUST be absent | + |---|---|---| + | a | `spec/PASS13_CANDIDATES.md` | `MUST NOT be refused or flagged by either` | + | b | `crates/epiphany-core/src/graph.rs` | `never refused or flagged by this rung` | + | c | `spec/operation_catalog.tex` | `never refused or flagged on this account` | + | d | `spec/core_spec.tex` | `first measure has no predecessor and is never flagged` | + | e | `crates/epiphany-core/src/invariants.rs` | `first measure has no predecessor and is never flagged (P13-S19, deferred)` | + | f | `crates/epiphany-core/src/invariants.rs` | `must never be flagged by invariant 20` | + | g | `crates/epiphany-ops/DECISIONS.md` | `All three clauses are vacuous for an instance's first measure` | + + **Positive check:** `crates/epiphany-core/DECISIONS.md` MUST still contain + `never flagged by the boundary clause`. That file is correct as written + (§0.4's closing note) and this check is what stops a later reader from + "fixing" it into agreement with the corrected row **g**. + + The report must paste the gate's output, not merely assert it ran. +- **Renames strand citations.** `m35_boundary_flags_wrong_distance` and + `m38_pickup_first_measure_not_flagged` are cited **in this contract** + (`:16`, `:44`) and nowhere else in `spec/` or `crates/` — verified. Pin 5's + rename must update those two citations in the same commit, and the report must + confirm the post-rename names appear nowhere stale. +- Both regenerated PDFs, with `operation_catalog.pdf`'s title page read back. +- `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`. +3. Commit. +4. `git diff --check ..HEAD -- crates/ spec/`. + +**A concurrent session commits to `spikes/`.** Re-check `HEAD` before +committing; never `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`, `.claude/worktrees/`. + +## §7. Report requirements + +- The observed `MeasureMeterMismatch` refusal, with the effect value and the + test name — and the pickup's own `Applied` alongside it. +- The mid-score observation for pin 2. +- All **4** mutations with their observed failing test names. +- Both byte-identical-body commands and their output. +- The corrected text of **all seven** surfaces (a–g), quoted, with row **g**'s + false claim shown before and after. +- Confirmation that `crates/epiphany-core/DECISIONS.md` was **not** touched. +- Which form pin 4's pickup used — `time_signature: None` or a matching + signature — and confirmation that the observed refusal is clause 3's, not + clause 2's. +- `operation_catalog.pdf`'s title-page version as rendered. +- Whether pin 8's workaround was executed, and if not, confirmation that no + corrected text names one. +- **Anything the contract did not anticipate** — a fifth understated surface, a + behaviour that contradicts pin 1, or anything suggesting the current + behaviour is wrong rather than undocumented. Report it and **stop**.