diff --git a/spec/CONTRACT_P13S16_PROJECTION.md b/spec/CONTRACT_P13S16_PROJECTION.md new file mode 100644 index 0000000..b571a95 --- /dev/null +++ b/spec/CONTRACT_P13S16_PROJECTION.md @@ -0,0 +1,521 @@ +# Contract — P13-S16: the projection gets maintained + +**Status:** DRAFT — **BLOCKED on P13-S27.** Not executable as written. Pin 0 +exposes that no authority defines the implementation's current reduction +semantics, and prose saying old canonical bases "must be rebuilt" does not make +them unusable. `core_spec.tex:11614`'s requirement stays **unmet** until S27 +supplies a version authority and a rejection-or-rebuild path. This contract is +complete and ratifiable as a *plan*; it may not be dispatched until S27 has a +disposition. + +**Rung type:** **canonical reduction-semantics change.** This is stronger than +"behaviour change" and the first draft of this contract understated it. The same +operation set now reduces to a different canonical `Score`: a graph that reduces +cleanly today is refused, and a field that was never written is written. +Disposition **A** of `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, ratified +there as "the later maintenance/enforcement fix" and sequenced after G3b — which +has landed. + +**No schema major or minor moves and no wire byte changes** — but the Operation +Catalog's version *does* move (pin 10), and the reduction-semantics question is +**separate from the schema/wire version question**. See pin 0. + +**No policy ruling is owed.** Disposition A is already ratified. What follows is +its implementation. + +--- + +## §0. What was verified before drafting + +Read out of the working tree at `f876836`, not recalled. Every line number below +was confirmed by reading the line. + +### 0.1 The refusal needs no new machinery — and this is the rung's biggest saving + +Disposition A says `CreateStaffGroup` "MUST carry `members: []`; a non-empty +`members` is refused or normalized away at construction." An earlier reading of +this contract assumed refusal required a new `PreconditionFailureReason` — which +would have made S16 a schema-minor epoch event with a footprint in +`binary_format.tex`, `PLAN_GMINOR_SCHEMA_MINOR.md`, `decode.rs`, and the history +test. **It does not.** + +`reduce.rs:1236` already defines the shared helper, and its own doc comment +already covers this case: + +> The precondition no-op a structural create or delete returns when a container +> is non-empty where the operation requires it empty (**a create carrying +> children**, or a delete of a container with live children). + +Three creates already call it for exactly this reason — `create_region` +(`:4174`), `create_staff_instance` (`:4246`), `create_voice` (`:4310`) — each +refusing a carried value that bears a separately-minted typed child. +`create_staff_group` is **the sole outlier**: it accepts carried `members` and +merely checks each is live (`:4489`–`:4502`). + +So the refusal is the **fourth instance of an established pattern**, not a new +one. `PreconditionFailureReason::ContainerNotEmpty` stays at discriminant 10. +**No new reason, no epoch, no wire change, no accept-set move.** + +### 0.2 Normalizing at construction or decode is excluded, on ratified grounds + +Disposition A's "or normalized away" alternative must **not** be taken. The +committed decode vector at `ops/src/vectors.rs:829` pins 130 literal bytes of a +`CreateStaffGroup` envelope whose payload carries `members = [StaffId(…)]`, and +its contract is decode-then-re-encode injectivity. The text-projection golden at +`textproj/src/vectors.rs:198`–`:201` carries the same value. Folding `members` +away at decode would break both, and violates `req:binfmt:decode-vectors` +(`binary_format.tex:3404`ff): *"Canonical decode is injective: distinct byte +strings denote distinct values."* + +**Refusal happens at reduction. Decode is untouched, and both artifacts survive +unchanged.** This is the same fork P13-S8 faces, resolved the same way, for the +same ratified reason. + +### 0.3 The authorship cycle makes empty-at-mint the only self-consistent rule + +`create_staff` requires a carried `group` to be live (`:4372`–`:4383`); +`create_staff_group` requires each carried member to be live (`:4489`–`:4502`). +There is **no `ModifyStaff`, `ModifyStaffGroup`, `DeleteStaff`, or +`DeleteStaffGroup`** anywhere in `OperationKind` (`payload.rs:170`–`:307`; +confirmed normatively at `operation_catalog.tex:1288` and `:1553`). With mints +only, no authoring order produces an agreeing pair. + +Therefore the *only* authorable agreeing sequence is: mint the group empty, then +mint staves naming it. Requiring `members: []` is not an arbitrary restriction — +it is the sole rule consistent with the operation surface that exists. + +### 0.4 The re-carry hazard, and the base-ingest hazard hiding behind it + +`create_staff_group`'s idempotence check compares `op.group` against +`self.staff_group_values` (`:4466`–`:4469`). If maintenance wrote the appended +members into that map, a byte-identical re-carry of `CreateStaffGroup(g, [])` +would compare `[]` against `[s]` and return `RecreateContentMismatch` instead of +`AlreadyApplied`. Disposition A names this sub-pin explicitly. + +**The non-obvious half:** base ingest (`:1611`–`:1620`) reseeds +`staff_group_values` from `score.staff_groups` — the *maintained* value. So even +if reduction keeps carried and derived apart in one session, a snapshot round +trip launders the derived value into the carried slot, and the same misverdict +returns **after a reload**. A test that never reloads cannot see it. + +The resolution falls out of §0.1: once a non-empty carried `members` is refused, +**the carried value is by construction always empty**, so the base seed can +reconstruct it exactly rather than approximately (pin 4). + +### 0.5 `t8b` is the obstacle, and it inverts rather than dies + +`t8b_both_permitted_stale_forms_hold` (`reduce.rs:16339`, doc `:16317`–`:16337`) +asserts both stale forms **hold**, and its doc block names disposition A's two +maintenance rules as **mutations that must make those assertions fail**. The +test is a correctly-built detector for precisely this change. + +It is therefore rewritten, not deleted: the same two authoring orders, with the +verdicts inverted — the missing order now yields agreement, the spurious order +now yields `ContainerNotEmpty`. Its doc block's mutation notes become the +rung's own mutation evidence, pointing the other way. + +### 0.6 Invariant 21 has real work left after maintenance + +Maintenance plus refusal does not make disagreement impossible: + +- **Undo.** `reduce.rs:2967` removes a `Staff` from `score.staves` on undo but + leaves its id in any live group's `members`. The reverse direction *is* + guarded (`:6736`–`:6744`, which blocks undoing a group still named by a live + staff); **this direction is not.** +- **Base ingest.** A blob authored before this rung, or by another + implementation, can carry a disagreeing pair straight in. + +There are 20 invariants (`invariants.rs:149`, count guard `:6064`). 21 is free. + +--- + +## §1. Pins + +**Pin 0 — declare the reduction-semantics break; do not pretend it is +containable.** + +`core_spec.tex:14369`–`:14372` is normative: *"Two replicas with different +`ReductionAlgorithmVersion` may produce different canonical states from the same +operation set; the active superblock declares the version under which the +bundle's canonical base was materialized."* And `:11614`–`:11617`: *"Snapshots +produced under an earlier algorithm version cannot be used as canonical bases +under a later one without rebuilding."* This rung is exactly such a change. + +**The obvious disposition — bump the version — is not available, and the reason +is subtler than an absence of machinery.** The machinery exists; it is +**self-referential**, so it cannot detect what it appears to guard. + +`ReductionAlgorithmVersion` (`bundle/src/ids.rs:291`) is a wire field of the +bundle superblock (bytes `68..72`, `superblock.rs:20`), and there **is** a +production writer path: + +- `reduction_version_for` (`bundle.rs:989`) sets a new superblock's version from + **the canonical base's own reported version**, or `default()` (zero) when + there is no base — its doc: *"only a base records a reduction."* +- `open` (`bundle.rs:396`–`:399`) rejects a bundle whose base's version + **disagrees with the superblock's**. + +So a document's declared reduction version is sourced from the base and then +checked against itself. **Nothing anywhere compares either value against the +semantics the running implementation actually implements.** A base reduced under +old semantics carries its own version forward, agrees with the superblock it +seeded, and is accepted. **The check is not vacuous** — it catches a corrupt or +tampered base whose version disagrees with its superblock. What it cannot catch +is a *valid* stale base: one whose version was conformingly propagated. So the +check **necessarily passes for a conformingly propagated stale base**, which is +exactly the case `core_spec.tex:11614` exists to prevent. + +*(An earlier draft of this pin claimed "every construction site is an unrelated +hardcoded literal." That was false, and the error is instructive: the search +behind it looked for `ReductionAlgorithmVersion(` constructor calls, which by +construction cannot find a path that propagates an existing value without +constructing one. The instrument could not observe the thing it was used to +rule out.)* + +Two supporting facts stand: there is **no constant or accessor naming the +implementation's current reduction semantics**, and **`ids.rs:288`–`:289` states +that "the algorithm catalog itself lives in `epiphany-ops`" while nothing of the +kind exists there** — a doc comment asserting a false fact about another crate, +which is **P13-S26's pattern, second instance.** + +**Scope of the claim, deliberately narrowed:** this inspection establishes that +**the current implementation has no mechanism** to detect a reduction-semantics +change. It does **not** establish that no such change in the project's history +was ever detectable; that would need a history audit this rung has not done, and +the stronger sentence must not be written into the ledger. + +**Therefore this rung does NOT invent the missing machinery**, which would be a +scope explosion and a separate design — **and, because it does not, this rung +cannot execute.** Pin 0 records the break; it does not discharge it. S16 waits on +S27's disposition. What pin 0 still requires of the eventual rung: + +1. **State the break** in `spec/PASS13_CANDIDATES.md`'s P13-S16 row — which + stays **blocked on P13-S27**, not resolved — and in `operation_catalog.tex`'s + Revision History entry: canonical bases materialized before this rung must be + **rebuilt**, not reused, because `create_staff` now writes + `StaffGroup.members` and `create_staff_group` now refuses inputs it + previously accepted. +2. **File P13-S27** — that the reduction-version machinery is + **self-referential**: `reduction_version_for` (`bundle.rs:989`) sources a new + superblock's version from the canonical base's own self-report, and `open` + (`bundle.rs:396`) checks only that the two agree, so **the current + implementation has no mechanism comparing either against the semantics it + actually implements.** Supporting: no constant or accessor names the current + semantics, and `ids.rs:288`'s catalog claim is false. **The stronger + historical claim — that no such change has ever been detectable — is NOT + established by this inspection and must not be written.** This rung is the + occasion, not the cause. +3. **Assert nothing it cannot enforce.** No test may claim stale bases are + rejected; nothing rejects them. The break is recorded, not guarded, and the + contract says so plainly rather than implying coverage. + +**Pin 1 — refuse a non-empty carried `members`, using the existing helper.** +In `create_staff_group` (`reduce.rs:4458`), before the liveness loop, refuse a +carried non-empty `members` with `container_not_empty()`. Match the idiom and +comment style of `:4174`, `:4246`, `:4310`. **Do not introduce a new +`PreconditionFailureReason`**; `ContainerNotEmpty` stays at 10 and no schema +document moves. + +The liveness loop (`:4489`–`:4502`) becomes unreachable for non-empty members +and **must be deleted, not left dead** — a precondition that cannot fire is the +kind of residue this pass keeps finding. + +**No behavioural test can prove that deletion.** A retained dead loop passes M1 +and every other assertion here, because refusal short-circuits before it. Pin 1 +therefore requires a **structural gate**: read +`crates/epiphany-ops/src/reduce.rs`, slice the `create_staff_group` body +(brace-matched from its `fn` line to its closing brace, **production source +only** — never the test module), whitespace-normalize, and assert the slice +**contains** the empty-members refusal and **does not contain** any +`TypedObjectId::Staff` liveness check or `TargetMissing` construction. + +**Pin 1a — three existing tests assert what pin 1 removes; all three must be +revised.** Each currently *passes* by asserting the outgoing rule: + +| Test | Line | Currently asserts | Under pin 1 | +|---|---|---|---| +| `t6` | `reduce.rs:16154` | `CreateStaffGroup.members` naming a non-live target is `TargetMissing`, one of three referential loops asserted separately | that arm becomes `ContainerNotEmpty` and stops testing a *referential* loop at all; the `CreatePartDefinition.staves` and `CreateView.active_layers` arms are untouched and must stay | +| `t7` | `reduce.rs:16229` | those same preconditions are **not** enforced base-free | pin 1's refusal is **not** graph-gated — it is a property of the carried value — so this arm now refuses base-free too, inverting the claim for that arm only | +| `t9` | `reduce.rs:16454` | a from-empty score passes `check_invariants`, and **each skipped reducer check independently makes invariant 10 fire**, on a fixture that already attempts a dangling reference in each of the four ops | the dangling-member fixture can no longer enter the graph, so both the fixture and t9's own mutation set change | + +**`t7`'s inversion is the subtle one and must be stated in its doc block:** a +graph-aware precondition asks about the *universe* and cannot run base-free; an +empty-container precondition asks only about the *carried value* and therefore +runs everywhere. Different classes — conflating them is how a later reader would +wrongly "restore" the graph gate. + +Each keeps its id and gains a doc note recording what it asserted before this +rung and why the assertion inverted. + +**Pin 2 — maintain the projection in `create_staff`.** +In `create_staff` (`:4330`), after the graph push at `:4386` and only when +`op.staff.group == Some(g)`, append the new staff's id to `g`'s `members` **in +`self.graph`'s `score.staff_groups`**. Under base-free reduction +(`self.graph.is_none()`) there is no graph to maintain and nothing is written — +matching how `:4385` already guards the staff push itself. + +Appending is set-union and order-independent per staff id; the append must be +idempotent (never add an id already present), since convergence replays. + +**Pin 3 — carried and derived are kept apart, and `staff_group_values` holds the +carried value.** +`self.staff_group_values` (`:4507`) MUST continue to store the value **as +authored** — which pin 1 guarantees is always empty-membered. Pin 2 writes the +maintained members **only** into `self.graph`. The re-carry comparator at +`:4466` is not changed and must keep comparing against the carried value. + +**Pin 3a — a permanent named regression test, not only mutation M3.** Add +`t8c_recarry_compares_against_the_carried_members_not_the_derived`: in one +session, `CreateStaffGroup(g, [])` → `CreateStaff(s, group: Some(g))` → +re-carry `CreateStaffGroup(g, [])`, asserting `AlreadyApplied` **and** that the +graph's `g.members == [s]` at that moment. A mutation demonstrates the hazard +once; only a test keeps it demonstrated. + +**Pin 4 — base ingest reseeds the carried value, not the derived one.** +At `:1619`, seed `staff_group_values` with the group's value **with `members` +emptied**, not `group.clone()`. This is exact rather than lossy: pin 1 makes +empty the only authorable carried value, so the reconstruction is the carried +value. The comment at `:1614`–`:1618` must be extended to say why, naming the +reload hazard of §0.4 — otherwise a later reader "fixes" it back to +`group.clone()` and reintroduces a defect that only appears after a snapshot. + +**Pin 4a — a permanent named regression test for the reload path.** Add +`t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent`: reduce +the pin-3a sequence, materialize the score, **re-reduce onto that score as a +base**, then re-carry `CreateStaffGroup(g, [])` and assert `AlreadyApplied`. +This is the only test that would exercise the base-seed path; pin 4 is +unguarded without it. + +**Pin 5 — close the undo hole in the unguarded direction.** +The `Staff` undo `retain` arm (`:2967`) MUST also strip the removed staff's id +from every group's `members`, in both `self.graph` and — if any derived copy is +held — wherever else the projection lives. The `StaffGroup` arm (`:2977`) needs +no change: `:6736`'s reference guard already blocks undoing a group a live staff +names. + +**Pin 6 — graph invariant 21, `StaffGroupMembershipAgreement`.** +Flags both directions: a staff whose `group` names a group whose `members` omit +it, and a group listing a staff whose own `group` is not that group. Witnesses +must name both ids and the direction. + +This is an **append with a documentation footprint** — `invariants.rs:149`, +`all()`, the count guard at `:6064`, and `core_spec.tex`'s normative enumeration +(which currently ends at 20 and which **P13-S26 has just established is already +under-describing invariant 10** — do not attempt to repair invariant 10's prose +here; that is S26's rung). + +**The count is not the test.** `all().len() == 21` passes with the dispatch arm +deleted — the project already knows this, which is why +`m40_check_invariants_dispatches_invariant_20` exists +(`invariants.rs:6045`–`:6066`, whose own doc says *"`all().len() == 20` passes +even with the dispatch arm deleted, so this row must instead show a score +violating ONLY invariant 20 is actually flagged by the top-level +`check_invariants` entry point"*). Pin 6 requires the **same behavioural shape**: +a score violating *only* invariant 21, flagged through `check_invariants`, with +the dispatch-arm deletion as its signing mutation. A count assertion may +accompany it and may not replace it. + +**Pin 6 is coupled to pin 5 and they split only together.** M5 signs the undo +hole by requiring invariant 21 to *observe* the residue. If invariant 21 is +deferred to a later rung, then either pin 5 and M5 defer with it, or M5 must be +restated to assert the leftover member **directly** on the materialized score +rather than through `check_invariants`. Splitting pin 6 out while leaving M5 as +written would leave the undo repair unsigned. + +**Pin 7 — `t8b` inverts.** +Rewrite `t8b_both_permitted_stale_forms_hold` as +`t8b_the_projection_is_maintained_and_the_spurious_form_is_refused`: same two +authoring orders, verdicts inverted. Its doc block must record that it +previously pinned the opposite, and why the change is the ratified disposition +rather than a regression. **Deleting it is forbidden** — the pairing of the two +orders is the coverage. + +**Pin 8 — the four G3a undo-repair tests are re-verified, not assumed.** +`:16838`, `:16992`, `:17138`, `:17345` each construct the missing-member form, +which pin 2 now makes an agreeing form. They assert on undo effects rather than +on `members`, so they are expected to survive — **expected, not known.** Each +must be run and its verdict reported; any that changes is a finding. + +**Pin 9 — no byte artifact moves.** +`spec/vectors/decode_vectors.txt`, `ops/src/vectors.rs:829`'s literal-byte +vector, and `textproj/src/vectors.rs:198`'s golden are all **unchanged**, +because refusal is at reduction and decode is untouched (§0.2). Confirm, do not +assume. No schema major or minor, no accept-set move, and **no schema/binary-format +companion version bump**. This is narrower than "no version bump": pin 10 *does* +require an Operation Catalog version bump and Revision History row, because the +catalog's normative text about these two operations changes. + +**Pin 10 — specification surfaces.** +`operation_catalog.tex` §CreateStaff and §CreateStaffGroup currently state the +disposition-B stale-form semantics normatively (`:1265`–`:1278`, `:1531`–`:1540`) +and must be rewritten to the maintained rule, with a Revision History row and a +version bump. `core_spec.tex`'s `Staff.group` / `StaffGroup.members` docs +(`:5585`–`:5591`, `:4235`–`:4241`) and the two Rust doc comments +(`graph.rs:842`–`:847`, `:1643`–`:1649`) likewise. + +**The two Rust doc comments are grep-asserted** by +`graph.rs:2136` and `:2160` (needles at `:2139`, `:2142`, `:2163`, `:2166`, +`:2148`, `:2172`, `:2176`, `:2180`). Those guards must be updated in step, and +the updated needles must assert the *new* rule — a guard left asserting the old +words would fail loudly, but a guard weakened to a substring both rules share +would pass silently, which is the worse outcome. + +**Each new needle MUST be wording the disposition-B comments cannot satisfy.** +Retaining only "sole authority" and "non-authoritative" is insufficient: both +phrases are true under B and under A, so a guard built from them alone passes +against the text it is meant to have replaced. Require phrases that are false +under B — for example **"maintained from `Staff.group`"** and **"must agree"** — +so that reverting either comment to its B wording fails the guard. M7 signs +exactly this. + +**Pin 11 — the ledger.** +`spec/PASS13_CANDIDATES.md`'s P13-S16 row → **blocked on P13-S27**, recording the +`ContainerNotEmpty` reuse (and that a new reason was considered and proved +unnecessary), the base-ingest hazard, the `t8b` inversion, the `t6`/`t7`/`t9` +revisions, and — per pin 0 — that canonical bases materialized before this rung +must be rebuilt rather than reused. + +**File P13-S27 in the same `spec/PASS13_CANDIDATES.md` edit** — it is a +prerequisite discovered by this rung, not independent ledger cleanup, and the +two rows must land together so the blocking relation is visible from either end. +Its claim, at the scope §0's inspection supports: the reduction-version +machinery is **self-referential** — `reduction_version_for` (`bundle.rs:989`) +sources a new superblock's version from the canonical base's own self-report, +and `open` (`bundle.rs:396`) checks only that the two agree — so **the current +implementation has no mechanism comparing either against the semantics it +actually implements**, and `core_spec.tex:11614`'s rebuild requirement is +unenforced. Supporting: no constant or accessor names the current semantics, and +`ids.rs:288`'s claim that the catalog lives in `epiphany-ops` is false — a +second instance of **P13-S26**'s pattern. + +**Do not write the stronger historical claim** ("no reduction-semantics change +has ever been detectable"); §0 does not establish it. + +**The P13-S16 row does NOT move to RESOLVED in this edit.** It records the +disposition-A plan, names this contract, and is marked **blocked on P13-S27**. + +--- + +## §2. Touch table + +| # | File | Change | +|---|---|---| +| 1 | `crates/epiphany-ops/src/reduce.rs` | pins 1, 1a, 2, 3, 3a, 4, 4a, 5, 7, 8; and `create_staff_group`'s own doc comment, which states the disposition-B rule | +| 1b | `crates/epiphany-ops/src/payload.rs` | `CreateStaffGroupOp`'s doc (`:1789`ff) states that graph-aware reduction preconditions every carried member resolves to a live `Staff` and that "the mint stores `members` exactly as given and neither maintains nor trusts it" — **both clauses become false** | +| 1c | `crates/epiphany-ops/src/valuegen.rs` | `staff_group`'s doc (`:372`–`:375`). **Precision:** the helper still carries and preserves supplied `members` exactly, and "**never normalizes**" stays true and MUST be preserved — the helper is unchanged. What becomes false is the framing that such a non-empty value is "the value a `CreateStaffGroup` mints" (it can no longer mint one), and the disposition-B attribution. Rewrite those two clauses only | +| 2 | `crates/epiphany-core/src/invariants.rs` | pin 6 | +| 3 | `crates/epiphany-core/src/graph.rs` | pin 10 (two doc comments + their two grep guards) | +| 4 | `spec/operation_catalog.tex` (+ `.pdf`) | pin 10 | +| 5 | `spec/core_spec.tex` (+ `.pdf`) | pins 6, 10 | +| 6 | `spec/PASS13_CANDIDATES.md` | pin 11 | + +Regenerate the two PDFs **only after** their sources reach final form. + +--- + +## §3. Mutation plan + +Applied, **run**, output recorded verbatim, restored **by hand-editing back**. + +**M1 — the refusal fires.** Remove pin 1's emptiness check; the rewritten `t8b` +spurious-order assertion must fail. + +**M2 — the maintenance fires.** Remove pin 2's append; the rewritten `t8b` +missing-order assertion must fail. + +**M3 — the re-carry stays idempotent.** Make pin 3 write maintained members into +`staff_group_values`; a byte-identical re-carry must degrade from +`AlreadyApplied` to `RecreateContentMismatch`. **This mutation must be observed, +not reasoned about** — it is the sub-pin disposition A named. + +**M4 — the base-ingest hazard is real.** Restore `:1619` to `group.clone()`; +pin 4a's test must fail. **If it does NOT fail, pin 4 is unmotivated and that is +a finding** — report it rather than keeping a guard nothing needs. + +**M3 and M4 are signed by pins 3a and 4a, not by manual demonstration.** Run each +mutation against its named test so the guard, not the transcript, is what +survives the rung. + +**M8 — the dead loop is actually gone.** Reinstate the member-liveness loop in +`create_staff_group` **after** pin 1's refusal, where it cannot fire. Every +behavioural assertion in this contract must still pass, and the pin-1 structural +gate must fail. This is the only signature available for a deletion that no +behaviour observes. + +**M9 — `t7`'s inversion is real, not assumed.** With pin 1 in place, run the +`CreateStaffGroup` arm of `t7` base-free and confirm it refuses; then graph-gate +pin 1's refusal behind `self.graph.is_some()` and confirm that arm reverts to +applying. Signs that the empty-container precondition is deliberately +universe-independent. + +**M5 — the undo hole is closed.** Remove pin 5's strip; undoing a `CreateStaff` +must leave a disagreeing pair that invariant 21 flags. + +**M6 — invariant 21 sees both directions.** Delete each arm in turn; each +deletion must leave a distinct disagreeing fixture unreported. + +**M7 — the doc guards discriminate.** With pin 10's needles updated, revert one +doc comment to its disposition-B wording; the guard must fail. A guard that +passes against both wordings is weakened, not updated. + +--- + +## §4. Gate + +1. `cargo test --workspace` — full pass. **The count will move** (t8b renamed, + new invariant tests). Report the new total and the delta with its cause. +2. `cargo clippy --workspace --all-targets -- -D warnings` → clean. +3. `cargo fmt -p epiphany-ops -p epiphany-core --check` → clean. + **`cargo fmt --all` is forbidden.** +4. `git diff --cached --check` → clean, after staging; confirm the staged list + is exactly §2. +5. `spec/vectors/decode_vectors.txt` **unmodified** (pin 9). Confirm by `git + status`, not by inspection. +6. Invariant 21 is reached **through `check_invariants`** on a score violating + only it, in the shape of `m40_check_invariants_dispatches_invariant_20` + (`invariants.rs:6045`). `all().len() == 21` and the `core_spec.tex` + enumeration ending at 21 are checked **in addition**, never instead. +7. The four pin-8 tests each run, each verdict reported. +8. The pin-1 structural gate: `create_staff_group`'s production body contains + the empty-members refusal and no member-liveness/`TargetMissing` path. +9. `t8c` (pin 3a) and `t8d` (pin 4a) both present and passing, by name. + +--- + +## §5. Staging and boundary + +Stage only §2's files, by explicit path. **Never `git add -A`.** + +**A concurrent session commits here.** Re-check `HEAD` before staging and before +commit. **Never** `git reset`, `git restore --staged`, `git checkout`, or `git +stash`. + +**Out of bounds — MUST NOT be read, written, or staged:** the entire `spikes/` +tree, `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-render-svg/**`, +`crates/epiphany-glyphs/**`, `crates/epiphany-editor-gui/**`, +`crates/epiphany-testkit/benches/editor_pipeline.rs`, the root `Cargo.toml`, +`.claude/worktrees/`. + +**Ratified contracts MUST NOT be edited**, including +`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` and `…_G3A_UNDO_REPAIR.md`. + +**Do not repair `core_spec.tex`'s invariant-10 prose** — that is P13-S26, and +its evidence at `invariants.rs:69`–`:71` must stay intact. + +**The executing agent MUST NOT commit.** Leave the work staged. + +--- + +## §6. Report requirements + +1. The nine mutations (M1–M9), each with verbatim failure output. +2. The nine gate results, each with its command. +2a. For pin 0: confirmation that **nothing** was added claiming to reject or + detect stale canonical bases, and that the break is recorded only in prose. +3. The staged file list, and the test-count delta with its cause. +4. The four pin-8 verdicts, and the `t6`/`t7`/`t9` revisions with what each + asserted before and after. +5. Anything contradicting this contract. A contract defect reported is worth + more than a contract satisfied. diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 1b6dde4..9a91036 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -111,7 +111,7 @@ evidence in isolation. | P13-S13 | **The score tuning context has no canonical persistence path: it can be saved, but never authored, replicated, or merged.** Schema major 3 (Push 4b tranche 3b-i) put `smufl` and `overrides` on the wire, but the only *persisted* carrier that embeds a `ScoreTuningContext` is the **acceleration snapshot**, which Chapter 8 makes explicitly non-canonical and regenerable and which the bundle may discard and rebuild at will. No **canonical** carrier embeds it at all: no operation authors it (`epiphany-ops` has no tuning-context payload anywhere — the vocabulary's only `tuning` references are the per-pitch `TuningReference::Inherit`), and `MaterializedState` carries effects, conflicts, anomalies, objects, spellings, breaks, page-breaks, and pending, but no tuning context. So a user who selects a tuning system or sets a per-voice override has authored something the format cannot durably represent, and `req:tuning:tuning-resolution-order`'s scopes 2–4 (`overrides`) are in practice unreachable from any document a replica could exchange | this file (found 2026-07-24 while scoping text-projection parity; verified by searching the whole `epiphany-ops` operation vocabulary and `MaterializedState`'s field list) | **CLOSED by genesis tranche G2b** (`spec/CONTRACT_GENESIS_G2B_TUNING.md`). `SetTuningContext` — kind/tag **34**, schema major **3**, minor epoch **10** — makes an operation author the tuning context, and the op log is canonical. **The closure argument is the `metadata` precedent, not the canonical base:** the base embeds no graph values for *any* field, including `metadata`, which has been op-authored since M2d and is durable purely through its operations. The rung paid the accept-set raise this entry predicted (`OperationEnvelopeBlock` 2→3), charged to this one surface because minimal stamping is a pure function of each payload's value and `ScoreTuningContext` is the only genesis payload born at v3. **The payload carries `epiphany_core::TuningContextSettings`, a five-field subset, not the full graph type** — `accidental_extensions` is staged off the wire, so a full-value payload would have diverged between a live session and the same document reloaded, and `canonical_value!` could not have caught it (it compares bytes, never the originating value). Reduction leaves that field untouched. *Original filing and disposition follow.* — `spec/RULING_GENESIS_PERSISTENCE.md` (ratified 2026-07-24, 011c68a) reverses Pass-12 K8 and absorbs genesis into the operation set, naming `SetTuningContext` in its §2 settings table. **This was not a tuning-specific defect and did not get a tuning-specific fix:** the operation arrives as one of nine surfaces in a single coordinated tranche, and the wire layout is untouched. **The disposition, and the evidence that produced it:** `spec/ANALYSIS_GENESIS_PERSISTENCE.md` maps the same gap across the whole `Score`: **eight fields have no operation that can produce them** — `canvas.layout_defaults`, `instruments`, `staff_groups`, `parts`, `tuning_context` (this entry, its field 10), `spelling_precedence`, `analysis_layers`, `views`, plus `identity` — and one more (`decomposition_attachments`) can only be pruned back, never authored. Independently re-verified against the working tree: each field's sole `reduce.rs` mention is a read-only base-seed read. Of the four dispositions weighed there (a canonical genesis block; closing the op-coverage gap; promoting the canonical base to carry graph values; scope-limiting), **the second was taken** — every mutable `Score` field becomes operation-authored — so S13 closes when that tranche lands and is tracked *there*, not here. **One cost this entry contributes as evidence:** the per-field operation route is not the free schema-minor it appears. Blocks stamp *minimally*, at the lowest major whose layouts decode them, and `bundle.rs`'s `max_supported_major` currently caps `OperationEnvelopeBlock` at **2** on the explicit ground that no operation payload embeds the tuning context. A `SetTuningContext`-style operation would make its blocks stamp v3, dragging a role accept-set raise along with the kind append — for one field of eight. That is a concrete instance of the analysis's closing constraint, that any option enumerating fields must be re-audited against its table whenever `Score` gains a field. **This cost is now paid deliberately rather than avoided — but NOT amortised, as first written.** The ruling's "one accept-set raise, spent once" implied a single batch landing every new kind at `OperationEnvelopeBlock` major 3, spreading the raise across nine surfaces. Re-derived 2026-07-28 against the working tree, that is wrong: minimal stamping is a pure function of each payload's value, so the other eight surfaces stamp at major 0, 2, or 2 and never reach the raised bound at all. `SetTuningContext` is the sole payload born at v3, so the raise is charged to **exactly this surface** after all — which is why `spec/PLAN_GENESIS_OPS.md` §4 splits G2 and isolates it in **G2b**. **And the closure argument is not the canonical base:** the base is role-bound to major 0 (`mis_stamped_canonical_base`) and is a `MaterializedState`, which embeds no graph values for *any* field — including `metadata`, op-authored since M2d and durable purely through its operations. S13 closes on that precedent: the op log is canonical, and G2b makes an operation author the tuning context. Consequence to carry forward: once G2b lands, pruning would discard *authored* genesis state rather than merely re-derivable state, so the standing prohibition on pruning (blocked on disposition C) gains real teeth. Note `bundle.rs` documents the cap of 2 *with the tuning-context rationale in prose*, so that comment must move with the cap. Note the wire layouts themselves are already frozen and correct under every disposition: this was never about how the tuning context encodes, only about which carrier embeds it. Not a regression — nothing ever worked; major 3 made the gap visible by giving the value a wire form and no way to reach it) | | P13-S14 | **The chunk schema *minor* is a normative MUST that no writer has ever honoured, so every appended operation discriminant is unattributable to version skew.** `binary_format.tex:2330` requires a writer to raise the chunk schema minor when it emits any discriminant appended after the minor it otherwise declares, with a stated rationale: so that a decode failure on an unknown appended discriminant is attributable to a version skew rather than to corruption. `SchemaVersion::for_major` (`bundle/src/ids.rs:204`) maps a major to a fixed constant — `V0` is `{0, 1}`, not `{0, 0}` (`ids.rs:173`), and `V1`/`V2`/`V3` carry minor 0 — and, decisively, **takes only a major**, so no per-kind additive minor can reach it — and **both** writer-side staging paths derive nothing but the major (`testkit/src/bundle_harness.rs:25`, `textproj/src/serialize.rs:183`, each mapping `max(OperationEnvelope::schema_major)` through `for_major`). So every kind appended after the initial vocabulary has no additive-version record: **24–27** (Phase-3 first tranche), **28–29** (the schema-major-2 repeat revision), **30** (Push 4a `TransposeInterval`), and **31** (genesis G1 `CreateInstrument`). The requirement's own failure mode is exactly what the gap produces: a reader meeting kind 31 from a newer writer cannot distinguish "my vocabulary is stale" from "these bytes are damaged" | this file (found 2026-07-28 during G2a contract review; verified against the working tree — `for_major`'s signature admits no minor, and neither staging path computes one) | **RESOLVED at `ff9bd0f`** (the G-minor rung, 2026-07-28). Epoch ladder ratified as minors 2–9, one per additive event, complete against `spec/AUDIT_GMINOR_VOCABULARIES.md` and monotonic in the introducing commits' order. `introduced_minor()` landed on the five vocabularies with post-baseline variants, exhaustive and wildcard-free; envelope minor = max over emitted, block = max over envelopes, major and minor derived independently; baselines not normalised. **Two things the filing did not anticipate**, both from the audit that gated the rung: the scope was never just `OperationKind` (`OperationPayload` 3, `ReanchorReason` 6 and `PreconditionFailureReason` 10–15 also append), and the **manifest** reaches `OperationKindTag` through `edit_barriers` with no operation envelope in it — so the "no companion bump" note below is **superseded**: `TextDocument` carries the manifest `SchemaVersion` it cannot derive, and the companion moved 0.9.0 → 0.10.0. Op-block stamping did remain projection-invisible, exactly as scoped. Gate `[7f]` guards the manifest aggregate with an exact-equality oracle. *Original filing follows.* Ruled 2026-07-28: policy ratified 2026-07-28 as a **global additive epoch with content-minimal stamping** (`spec/PLAN_GMINOR_SCHEMA_MINOR.md` §4); the fix is its own rung, sequenced **after G2a and before G2b** — G2b appends kind 34, so running it first would either grow this sweep mid-flight or ship 34 with the very defect the rung retires. G2a appends kinds 32/33 and takes the violation from eight kinds to ten, knowingly — the debt is already eight deep, the +2 is immaterial against it, and one retroactive sweep over 24–33 is strictly less work than 24–31 now and 32–33 later. **What the rung owes:** a minor-assignment policy (which minor each past append belongs to — this is a retroactive judgement, not a derivation), a per-kind `schema_minor()` or equivalent, block minor = max over payloads, a `for_major` replacement that accepts one, and both staging paths. **Scoped 2026-07-28:** the minor IS in the chunk content-address preimage (`chunk_content_hash`, `chunk.rs:177`), so raising it moves every affected `ChunkId` and the manifest body naming it — real address churn, though **not** a `req:format:manifest-id` problem, since that promise is conditional on the same manifest body. It does **not** reach the text projection: op-block schemas are discarded during projection (`textproj/src/project.rs:424`), so no companion bump. And the problem is **not** per-`OperationKind`: an envelope also emits the outer `OperationPayload` discriminant (`ResolveEquivocation` = 3 carries no kind at all), so the gating work is an audit of every append-only vocabulary reachable from an affected payload. Note this is orthogonal to the *major* accept-set: `OperationEnvelopeBlock` stays at 2 through G2a and rises to 3 only at G2b | | P13-S15 | **The `OperationKind` wire golden lock stops at discriminant 29, so kinds 30–39 — ten of them, every kind appended since the lock was written — have no byte-level lock at all.** `operation_kind_wire_discriminants_are_golden` (`crates/epiphany-ops/src/payload.rs:2189`) declares `let table: [(OperationKind, u8); 30]` (`:2233`), covering 0..=29 and asserting for each that `kind.discriminant()` has not moved *and* that the discriminant byte truly leads the canonical encoding. **Absent from that table: `TransposeInterval` (30, Push 4a), `CreateInstrument` (31, G1), `SetCanvasLayoutDefaults` (32) and `SetSpellingPrecedence` (33, G2a), `SetTuningContext` (34, G2b), `CreateStaffGroup` (35), `CreatePartDefinition` (36), `CreateAnalysisLayer` (37) and `CreateView` (38, G3a), and `CreateMeasure` (39, G3b).** Their wire discriminants are unlocked: a hand edit to `OperationKind::discriminant()`'s match — itself the site Push 4a got wrong — would move any of the ten silently, and the encoding-leads-with-the-byte assertion never runs for them. **The shape is the failure this project keeps rediscovering:** a hand-maintained parallel table that quietly stopped being extended, exactly like the four literal sites found at Push 4a and the six found during G2a — and the golden lock is the one guard specifically meant to catch that class, so its own staleness is the worst place for it. The gap widened from four kinds to ten while the entry sat open, which is itself the argument for closing it now that the genesis ladder has stopped appending | this file (found 2026-07-28 by the G-minor implementation while building s1's coverage; **scope corrected 2026-07-30**, after the genesis ladder closed at G3b — the original text scoped the repair to kinds 30–33 and an array length of `; 34`, both of which were accurate when written and are now six kinds short. Re-verified against the working tree at `4f141ce`: the length literal is still `30`, and no arm for 30–39 appears in the table) | **RESOLVED 2026-07-30** (its own rung, no rider). **Never a live incorrectness:** every one of the ten discriminants was correct throughout, and `binary_format.tex:1443`ff (kind table rows 30–39) and `:1548`–`:1552` (tag table rows 30–39) carry them normatively — the gap is the *absence of a guard*, not a wrong byte. **The repair, as landed:** `operation_kind_wire_discriminants_are_golden`'s table goes from 30 to **40** entries, locking kinds 30–39 individually — each row asserting both that `kind.discriminant()` has not moved and that the discriminant byte leads the canonical encoding. **No wire, schema-version, or specification change**: this adds a guard over assignments that were already normative. **Mutation evidence:** `OperationKind::discriminant()`'s `SetTuningContext` arm was edited 34 → 44 and the extended lock failed (*"wire discriminant for SetTuningContext moved — canonical encodings are append-only"*); with the same mutation still applied, restricting the loop to `&table[..30]` — the exact pre-repair coverage — made it **pass**, which is P13-S15 itself reproduced in the tree rather than argued for. Both edits restored by hand. **On the sibling:** the tag half is total by construction and needs no extension. `the_tag_vocabulary_is_complete` (`payload.rs:2652`) is derived, not hand-written — it computes `first_unknown_discriminant()` from `PAYLOAD_FREE`'s maximum and asserts the payload-free discriminants are exactly `0..unknown` minus `Registered`'s, dense and each decoding — so it already covers 30–39, and `operation_kind_tag_vocabulary!` makes a tag without a discriminant a compile error rather than a silent omission. **One residue, scoped out and stated rather than papered over:** density plus round-trip does not pin *which* tag holds which byte, so a permutation inside the dense range (swapping two assigned discriminants) survives both that test and `phase3_tag_discriminants_are_golden` (`payload.rs:2728`), which pins literals for 24–29 only. The same permutation on the *kind* side is caught by this rung's extended table. The tag-side gap is **not** part of this rung and is **filed as P13-S22** rather than left as a closing remark — a residue recorded only inside a resolved row is a residue that gets lost | -| P13-S16 | **`StaffGroup.members` and `Staff.group` may disagree in both directions, and nothing detects it.** The two fields encode the same relation twice. `Staff.group` (`core_spec.tex:5592`, `graph.rs:848`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4242`, `graph.rs:1650`) lists the staves in a group. **The specification declares both and states neither an authority nor an agreement requirement.** Graph invariant 10 checks that each side *resolves* — a staff's group is declared (`invariants.rs:1188`), a group's members are declared (`invariants.rs:1196`) — and never that the two agree, so **both stale forms pass every check in the tree**: a *missing* member (`s.group == Some(g)` while `g.members` omits `s`) and a *spurious* member (`g.members` contains `s` while `s.group` is `None` or names a different group). Genesis G3a ruled `Staff.group` the sole authority and `StaffGroup.members` a non-authoritative denormalized projection (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, ratified 2026-07-29) — a normative semantic ruling that makes the disagreement *defined* rather than merely undetected, but does not make it *impossible*: G3a stores the projection without maintaining it | `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1 (found 2026-07-29 during G3a contract review; the authorship cycle is what surfaced it — with mints only, no authoring order produces an agreeing pair, since `CreateStaff` requires its group live at `reduce.rs:4372` and `CreateStaffGroup` requires its members live) | **open.** Deliberately no code change in G3a. The fix is disposition **A**: maintain the projection under reduction — `create_staff` with `group: Some(g)` appends to `g.members` — plus a candidate **graph invariant 21** enforcing agreement in both directions (20 exist; `invariants.rs:149` and the count guard at `:6064` both move), and a decision on whether a re-carried `CreateStaffGroup` compares against its *carried* `members` (empty) or the current derived state. **Consumers must read `Staff.group`, never `StaffGroup.members`, for membership** until that lands. The G3b sequencing note is now discharged — G3b landed, and invariant 20 is no longer competing. **Locators corrected 2026-07-31**; every code citation in this row had drifted, some by hundreds of lines, and `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` carries two of the same stale pointers (corrected separately, citation-only). **The concrete implementation cost, which this row did not state:** `t8b_both_permitted_stale_forms_hold` (`reduce.rs:16340`) **pins both stale forms as passing** — asserting `staff.group == Some(g)` while `g.members == vec![]`, and `g2.members == vec![staff2]` while `staff2.group == None` — and its own doc block (`:16317`–`:16339`) names disposition A's two maintenance rules as mutations that **must break** it. So the fix is precisely the mutation an existing test exists to detect: that test must be rewritten, not merely supplemented, and rewriting it is the rung's real cost. **Complete participant set**, none of it obvious from the two field declarations: `create_staff` (`reduce.rs:4330`) and `create_staff_group` (`:4458`); both byte-identical re-carry comparators (`:4334`, `:4466`), which under A must compare the **carried** value, never the derived one; both undo `retain` arms (`:2967`, `:2977`), where undoing a `CreateStaff` currently leaves its id in a live group's `members` with no guard — the reverse direction is guarded at `:6736` and this one is not; base ingest (`:1604`, `:1611`), which can seed a disagreeing pair from a blob authored before the rule; `valuegen::staff_group` (`valuegen.rs:376`), which documents that it never normalizes; and the four G3a undo-repair tests (`:16838`, `:16992`, `:17138`, `:17345`) that each construct the missing-member form. **No schema consequence:** `CreateStaffGroup` is schema major 0 and the accept-set does not move — but if A normalizes at *construction or decode* rather than at reduction, the pinned literal-byte vector at `ops/src/vectors.rs:829` and the text-projection golden at `textproj/src/vectors.rs:198` both break on re-encode injectivity. Reduction-time refusal leaves both untouched. That is the sharpest design fork in the rung | +| P13-S16 | **`StaffGroup.members` and `Staff.group` may disagree in both directions, and nothing detects it.** The two fields encode the same relation twice. `Staff.group` (`core_spec.tex:5592`, `graph.rs:848`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4242`, `graph.rs:1650`) lists the staves in a group. **The specification declares both and states neither an authority nor an agreement requirement.** Graph invariant 10 checks that each side *resolves* — a staff's group is declared (`invariants.rs:1188`), a group's members are declared (`invariants.rs:1196`) — and never that the two agree, so **both stale forms pass every check in the tree**: a *missing* member (`s.group == Some(g)` while `g.members` omits `s`) and a *spurious* member (`g.members` contains `s` while `s.group` is `None` or names a different group). Genesis G3a ruled `Staff.group` the sole authority and `StaffGroup.members` a non-authoritative denormalized projection (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, ratified 2026-07-29) — a normative semantic ruling that makes the disagreement *defined* rather than merely undetected, but does not make it *impossible*: G3a stores the projection without maintaining it | `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1 (found 2026-07-29 during G3a contract review; the authorship cycle is what surfaced it — with mints only, no authoring order produces an agreeing pair, since `CreateStaff` requires its group live at `reduce.rs:4372` and `CreateStaffGroup` requires its members live) | **open.** Deliberately no code change in G3a. The fix is disposition **A**: maintain the projection under reduction — `create_staff` with `group: Some(g)` appends to `g.members` — plus a candidate **graph invariant 21** enforcing agreement in both directions (20 exist; `invariants.rs:149` and the count guard at `:6064` both move), and a decision on whether a re-carried `CreateStaffGroup` compares against its *carried* `members` (empty) or the current derived state. **Consumers must read `Staff.group`, never `StaffGroup.members`, for membership** until that lands. The G3b sequencing note is now discharged — G3b landed, and invariant 20 is no longer competing. **Locators corrected 2026-07-31**; every code citation in this row had drifted, some by hundreds of lines, and `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` carries two of the same stale pointers (corrected separately, citation-only). **The concrete implementation cost, which this row did not state:** `t8b_both_permitted_stale_forms_hold` (`reduce.rs:16340`) **pins both stale forms as passing** — asserting `staff.group == Some(g)` while `g.members == vec![]`, and `g2.members == vec![staff2]` while `staff2.group == None` — and its own doc block (`:16317`–`:16339`) names disposition A's two maintenance rules as mutations that **must break** it. So the fix is precisely the mutation an existing test exists to detect: that test must be rewritten, not merely supplemented, and rewriting it is the rung's real cost. **Complete participant set**, none of it obvious from the two field declarations: `create_staff` (`reduce.rs:4330`) and `create_staff_group` (`:4458`); both byte-identical re-carry comparators (`:4334`, `:4466`), which under A must compare the **carried** value, never the derived one; both undo `retain` arms (`:2967`, `:2977`), where undoing a `CreateStaff` currently leaves its id in a live group's `members` with no guard — the reverse direction is guarded at `:6736` and this one is not; base ingest (`:1604`, `:1611`), which can seed a disagreeing pair from a blob authored before the rule; `valuegen::staff_group` (`valuegen.rs:376`), which documents that it never normalizes; and the four G3a undo-repair tests (`:16838`, `:16992`, `:17138`, `:17345`) that each construct the missing-member form. **No schema consequence:** `CreateStaffGroup` is schema major 0 and the accept-set does not move — but if A normalizes at *construction or decode* rather than at reduction, the pinned literal-byte vector at `ops/src/vectors.rs:829` and the text-projection golden at `textproj/src/vectors.rs:198` both break on re-encode injectivity. Reduction-time refusal leaves both untouched — the design fork is resolved that way in the contract. **Scoped 2026-07-31 as `spec/CONTRACT_P13S16_PROJECTION.md` (DRAFT), and immediately BLOCKED on P13-S27.** Two findings from that scoping changed the rung's size in opposite directions. **Cheaper than feared:** the refusal needs no new `PreconditionFailureReason` and no schema-minor epoch — `reduce.rs:1236`'s `container_not_empty()` helper already covers "a create carrying children" by its own doc, and three creates already call it for exactly this shape (`create_region` `:4174`, `create_staff_instance` `:4246`, `create_voice` `:4310`); `create_staff_group` is the sole outlier. **More expensive than feared:** this is a **canonical reduction-semantics change** — the same operation set now reduces to a different `Score` — so `core_spec.tex:11614` applies: canonical bases materialized beforehand cannot be reused without rebuilding. That requirement is currently **unenforceable** (P13-S27), so the rung may not execute until S27 has a disposition. Also found while scoping: base ingest (`reduce.rs:1619`) reseeds `staff_group_values` from the *maintained* value, so a snapshot round trip launders derived members into the carried slot and a re-carry misverdicts **only after a reload**; and `t6` (`:16154`), `t7` (`:16229`) and `t9` (`:16454`) each assert behaviour the refusal removes, alongside the already-known `t8b` | | P13-S17 | **Binary Format revision history omitted genesis tranche G2b entirely, including the accept-set raise it performed.** `spec/binary_format.tex`'s Revision History chapter ran G2a 0.12.0 straight to G-minor 0.13.0 to G3a 0.14.0, with no row anywhere recording G2b (`spec/CONTRACT_GENESIS_G2B_TUNING.md`, kind/tag 34, `SetTuningContext`) — even though `OperationEnvelopeBlock`'s accept-set raise 2→3, the first accept-set move since genesis tranche G2a explicitly recorded staying at 2, reached the normative tables (the per-chunk-role accept-set prose at `binary_format.tex:2353`–`:2363`, which names the `OperationEnvelopeBlock` role's maximum as 3 "as of genesis tranche G2b", and the `OperationKind` minor-additive bullet at `:2395`–`:2418`, which records "genesis tranche G2b took 34 (`SetTuningContext`)") and never the history. G2b's own contract touch table row 27 required "version, Revision History row" among the four-document ritual, and the rung was signed off without it — the gate did not catch a documentation MUST because nothing tests the revision history | `spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` §0 (found 2026-07-29 during the G3a undo-repair contract review, verified against the working tree: `binary_format.tex:3599`, `:3628`, `:3643` before this rung's edit) | **RESOLVED in this same commit.** The chronology is restored: G2b lands as its own 0.14.0 row between G-minor and G3a, and G3a renumbers to 0.15.0 (`spec/CONTRACT_GENESIS_G3A_UNDO_REPAIR.md` Packet B, pins B2–B3). A new scoped guard in `epiphany-testkit` makes the omission recurrence-detectable — a distinct principal marker per standalone-row rung (G2a, G-minor, G2b, G3a — G1 is deliberately unguarded, having no standalone row of its own), strictly ordered, with G2b's content anchored within its own row segment — so the entry is filed and closed by the same packet that finds it, unlike **P13-S15** and **P13-S16**, which stay open because their fixes are sequenced to later rungs | | P13-S18 | **Graph invariant 20's agreement and boundary-consistency checks are partial, but only three of the checker's nine non-success paths are the real gap — not the whole checker, as first filed and over-sized.** `check_measure_meter_consistency` (`invariants.rs:2662`) has nine non-success paths across its two clauses, enumerated and classified by both its own doc comment and `spec/CONTRACT_P13S18_MATRIX.md`'s 18-cell outcome matrix (agreement: A1-A4; boundary: B1-B5). A1 (`None` declared signature) is **inapplicable** — nothing to disagree with. A3/B3 (`Governing20::None`, an empty governing candidate set) are **vacuous** (pin 6c case 1). A2/B2 (an unresolving declared or governing signature) are **delegated** to invariant 10's own resolution check (`invariants.rs:1220`ff, its per-measure and instance-local-grid arms) — verified, not merely asserted: the matrix rung's mutations M7/M8 delete each arm in turn and show the SAME condition go unreported by the ENTIRE workspace suite, not merely by invariant 20. B1 (the first measure) is the already-filed pickup/anacrusis deferral, **P13-S19**. **Exactly three paths are genuine abstention: A4 and B4 (`Governing20::Indeterminate` — the comparable relation cannot place a candidate) and B5 (a decided governing selection with no computable musical delta — order without distance).** Also corrected: the earlier **"any `Measure` *end* anchor is incomparable"** claim was wrong only in its "any" — same-id, same-position `End`<->`End` IS comparable under c2 **when its offsets compare** (`measure20_offset_order`, `:2419`, returns `None` only for `Musical` against `WallClock`); distinct-id `End` anchors genuinely are incomparable (c3 restricts to `Start`+`Zero`) and do reach A4/B4/B5; and the `resolve_anchor` `Measure` arm citation (now `:503`-`:516`, formerly miscited as `:400`ff — see the companion line-number repair to `CONTRACT_GENESIS_G3B_MEASURE.md:206`) names the missing duration machinery, not invariant 20's own execution path, which never calls `resolve_anchor`. And the `WallClock`-anchored measure start `epiphany-ops::valuegen::measure` (`ops/src/valuegen.rs:447`) actually emits does **not** uniformly abstain both clauses: against `WallClock`-anchored meter changes (c5) agreement DECIDES and only the boundary clause abstains (B5, since `measure20_musical_delta` never returns a `WallClock` delta); against `Region`-anchored meter changes both abstain (A4/B4), because `WallClock` against `Region` has no comparability arm at all | `spec/CONTRACT_P13S18_MATRIX.md` pin 8 (ratified 2026-07-31, a diagnostic and bookkeeping rung: test coverage over `check_measure_meter_consistency`'s existing nine paths plus these three ledger repairs, no behaviour change) | **open, at its true size.** A4, B4 and B5 remain real, still gated on the deferred common-timeline machinery — but the capability that closes them is now filed as **P13-S23** (below), not P11-C5: P11-C5 is a narrower re-anchoring proximity metric this entry previously over-cited as the gate; P13-S23 is the broader "place any anchor pair on a common timeline and measure musical distance" capability that actually owns A4, B4 and B5 | | P13-S19 | **A pickup's *successor*, not the pickup itself, is what `CreateMeasure` and invariant 20 refuse — pickup/anacrusis measures are authorable, but the rest of the instance becomes unauthorable once one exists.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes `create_measure`'s clauses 1 (ordering) and 3 (boundary distance) vacuous for a first measure, and invariant 20's boundary clause is symmetrically exempt at `i == 0` — both for lack of a predecessor. **The agreement clause (clause 2) is not predecessor-dependent and applies to a first measure like any other**: a pickup declaring a signature that disagrees with the governing grid is itself refused (`MeasureMeterMismatch`) and flagged; only a pickup declaring `None` or a matching signature clears it, and only when its other preconditions (a live parent `StaffInstance`, resolving referents) are satisfied too. **The real defect is one measure downstream**: both rules compare `delta(prev.start, m.start)` against the *governing signature's full* `measure_duration()`, when the true distance is `prev`'s own content duration — those coincide only for full measures. A pickup's successor is therefore refused (`MeasureMeterMismatch`) by `create_measure` and flagged by invariant 20, which is what actually makes the rest of the instance unauthorable once a pickup is minted. This applies to **any** partial measure, not only a first one: a mid-score partial measure enters successfully (nothing examines its own duration when it is created), while *its* successor is refused the identical way — the failure is always attributed to the measure after the partial one. Closing this needs a per-measure duration — the "partial measure" notion this entry already names — and that is deliberately **not** introduced by the correction that reworded this entry. See also **P13-S24**, the Chapter 3 derived-notation deferral that shares this same missing concept but touches neither invariant 20 nor `CreateMeasure` | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting); corrected 2026-07-31 by `spec/CONTRACT_P13S19_PARTIAL.md`, which found the original wording true only of the pickup itself and, read as written, indistinguishable from "pickups work" | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes; it now depends on a per-measure duration concept, which does not yet exist | @@ -122,3 +122,4 @@ evidence in isolation. | P13-S23 | **No filed candidate owns "place any anchor pair on a common timeline and measure musical distance along it" — P13-S18 previously mis-cited a narrower capability as its gate.** Two disjoint deficiencies, both owned by this candidate. (1) **No ordering.** The pair is not comparable under any of `measure20_comparable_order`'s five shapes c1-c5 (`invariants.rs:2457`) at all — whether the failure is in the **referent** (distinct `Event` ids; distinct `Measure` ids outside c3's `Start`+`Zero` restriction), the **variant or selector** (`Event` against `Measure`, `Measure` against `Region`, differing `pos`/`edge`), or the **clock** (`Musical` against `WallClock`, including inside `measure20_offset_order`, `:2419`) — this is what invariant 20's 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 (an order, never a distance), and c5 compares two `WallClock`s, and `measure20_musical_delta` (`:2522`) never returns a `WallClock` delta (`:2527`) — this is what invariant 20's B5 is made of. Scoping this as merely "anchors of differing shapes" or "not directly comparable under c1-c5" would exclude B5 entirely — S5 (distinct-id `Measure` `Start`/`Zero`) is c3-comparable and S1 (`WallClock` measures, `WallClock` meter changes) is c5-comparable, and both still reach B5 — an earlier draft of this filing made exactly that narrower mistake. **Explicitly broader than P11-C5**: P11-C5 (`PASS11_WORKLIST.md:159`) is a re-anchoring proximity metric that resolves "when the graph-mutation phase tracks resolved positions", and covers narrowly the two-distinct-`Event`s case (`CONTRACT_GENESIS_G3B_MEASURE.md:223`, `effect.rs:139`-`:142`'s `PositionOutsideRegion` Reserved note); P13-S23 is the timeline itself, whatever positions get placed on it. Names its dependents: invariant 20's A4, B4 and B5, and `PositionOutsideRegion`'s Reserved status | `spec/CONTRACT_P13S18_MATRIX.md` pin 10 (filed 2026-07-31 during the same rung that corrected P13-S18's over-narrow P11-C5 citation) | **open.** No code owed by this rung. Closing it needs the deferred common-timeline/duration machinery — once a `Measure` end, a distinct-id `Measure`/`Event` referent, or an `Event` position on a wall-clock-placed region can be placed on a common timeline with a musical distance, invariant 20's A4/B4/B5 residue and `PositionOutsideRegion`'s Reserved status shrink together | | P13-S25 | **The committed decode corpus's numbered tag rows lock byte→byte, not variant→byte — one row already has the property the other thirty-nine lack.** `ops/src/vectors.rs:206`–`:209` emits one row per tag as `format!("tag_{:02}", tag.discriminant())` carrying `[discriminant]`: **both the name and the payload derive from the value alone**, so `tag_32` asserts that `0x20` round-trips and never that `SetCanvasLayoutDefaults` is 32. The `Registered` row (`:210`–`:217`) is different — its name is the hard-coded string `"registered"` while its bytes are computed from the variant, so the frozen literal at `spec/vectors/decode_vectors.txt:80` binds the association. **Disposition B of P13-S22:** give the numbered rows the same property. It **does** catch the coordinated permutation — by exactly the `Registered` mechanism, with the committed text serving as the independent statement — and it propagates the property to every implementation that reads the cross-impl corpus, which an in-crate Rust test cannot do | `spec/CONTRACT_P13S22_TAGLOCK.md` (disposition B, considered and deferred during the 2026-07-31 ruling; filed rather than left as a closing remark, per the same discipline that moved P13-S22 out of P13-S15's resolved row) | **open. Complementary to P13-S22, not a replacement for it, and not a re-litigation of it.** P13-S22 landed disposition A (`tag_wire_discriminants_are_golden`, `payload.rs:2730`), which fails **by variant name inside the crate**. B cannot supply that: its failure is still *"spec/vectors/decode_vectors.txt is stale. Regenerate: …"* (`testkit/src/vectors.rs:224`) — the misleading diagnosis P13-S22 was filed about — even though the diff text would now name variants. **What B buys is cross-implementation reach; what it costs is churn in a committed artifact other implementations pin.** Both are wanted; neither substitutes for the other. Sequencing note: run B's own signing mutation as the coordinated permutation (literals *and* declaration lines), since the literal-only form is caught today by row ordering and proves nothing | | P13-S26 | **A doc comment in shipped code claims a specification repair that never landed, and the claim is guarded on the code side and nowhere on the specification side.** `crates/epiphany-core/src/invariants.rs:69`–`:71` enumerates invariant 10's four reference classes and states that *“genesis tranche G3a repairs this prose to name what the check body already enforced”*. **It did not.** `core_spec.tex:6570`–`:6572`, the normative enumeration item 10, still reads only *“Every cross-cutting structure's references resolve to extant objects in the graph, except where explicit re-anchoring rules permit transient dangling states during edits”* — naming neither a staff's declared instrument, a staff's group, a staff group's members, a part's staves, a view's active layers, nor any of the meter/time-signature references the Rust doc lists and the check body enforces. The repair landed in the Rust doc comment only. **The asymmetry is the defect's sharp edge:** the Rust doc block is protected by a grep-assert, `t12_invariant_10_doc_comment_names_the_four_reference_classes` (`invariants.rs:4554`, needles at `:4562`–`:4566`), so the side that is *wrong about the other* is the side that is **locked**, while the side that is actually stale is unguarded | this file (found 2026-07-31 during P13-S16 reconnaissance, while verifying that row's invariant-10 citations; no ledger entry covered it) | **open.** **Not a live incorrectness** — the check body is correct and enforces every class; only the normative prose under-describes it, and only the doc comment lies about that. **A P13-S9 instance**, and filed deliberately as one: the loud form (a dangling citation) is caught by `requirement_labels.rs`, and this quiet form — a *true-sounding claim about another document's state* — is caught by nothing. **`invariants.rs:69`–`:71` MUST NOT be “corrected” on its own.** It is currently the only artifact in the tree pointing at the `core_spec.tex` gap; softening the Rust claim in isolation would make the specification defect invisible and convert a caught defect into an uncaught one — which is P13-S9's stated failure mode verbatim. **Repair both sides in one rung**, and consider whether the LaTeX enumeration deserves the grep-assert its Rust mirror already has | +| P13-S27 | **The reduction-algorithm-version machinery is self-referential, so the one check that would detect a canonical-semantics change necessarily passes.** `core_spec.tex:11614`–`:11617` is normative — *"Snapshots produced under an earlier algorithm version cannot be used as canonical bases under a later one without rebuilding"* — and `:14369`–`:14372` states that replicas at differing versions *"may produce different canonical states from the same operation set."* The machinery to enforce it appears to exist: `ReductionAlgorithmVersion` (`bundle/src/ids.rs:291`) is a superblock wire field (bytes `68..72`, `superblock.rs:20`); `reduction_version_for` (`bundle.rs:989`) sets a new superblock's value; and `open` (`bundle.rs:396`–`:399`) rejects a mismatch. **But the writer sources the value from the canonical base's own self-report** (mapping the base's `reduction_algorithm_version` through `unwrap_or_default()`), **and the reader compares it only against the superblock that value seeded.** Nothing compares either against the semantics the running implementation actually implements. **The check is not vacuous** — it catches a corrupt or tampered base whose version disagrees with its superblock — but it **necessarily passes for a conformingly propagated stale base**, which is precisely the case the requirement exists to prevent. Supporting: **no constant or accessor anywhere names the implementation's current reduction semantics**, and `ids.rs:288`–`:289` states that *"the algorithm catalog itself lives in `epiphany-ops`"* while nothing of the kind exists in that crate — **a second instance of P13-S26's pattern**, a doc comment asserting a false fact about another module | `spec/CONTRACT_P13S16_PROJECTION.md` pin 0 (found 2026-07-31 while scoping P13-S16, which is a canonical reduction-semantics change and therefore the first rung to need this guarantee; filed in the same ledger edit as the row it blocks) | **open, and blocking P13-S16.** **Scope of the claim, deliberately narrow:** this establishes that the **current implementation** has no detection mechanism. It does **not** establish that no reduction-semantics change in the project's history was ever detectable — that needs a history audit not yet done, and the stronger sentence is deliberately not written here. **What closing it requires:** an authority naming the semantics this build implements, and a rejection-or-rebuild path when a base disagrees with it. Until then any rung changing canonical reduction semantics can record its break in prose but cannot make stale bases unusable — which is why P13-S16's contract is complete, ratifiable as a plan, and **not dispatchable**. **Method note:** an earlier draft of S16's pin 0 claimed no writer path existed at all. That was false, and the way it was false is the point — the search behind it looked for `ReductionAlgorithmVersion(` constructor calls, which cannot find a path that propagates an existing value without constructing one. The instrument could not observe the thing it was used to rule out |