From 012a2de16d63f3ca042d554c5b8158c28a468a67 Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Wed, 29 Jul 2026 11:26:41 -0400 Subject: [PATCH] G3a contract repairs: the authorship cycle, and four maps the pin promised without MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Five review findings, all confirmed against the tree before repair. 1. StaffGroup/Staff authorship cycle. CreateStaff requires its group live (reduce.rs:4117); CreateStaffGroup requires its members live. With mints only, NO authoring order yields a bidirectionally consistent group, and the inconsistency is unrepairable in-packet -- there is no ModifyStaffGroup and deletes are deferred. Invariant 10 checks resolution in both directions independently (invariants.rs:1126, :1135) and agreement in neither; the spec declares both fields (core_spec.tex:4231, :5578) without saying which is authoritative. Added as §1.1, UNRESOLVED, with two dispositions and a recommendation -- the shape G2b's accidental_extensions pin took. t8's claim is narrowed accordingly: what closes is that CreateStaff's group precondition becomes satisfiable, not that a consistent group becomes authorable. The unqualified "defect closes" framing was wrong. 2. Pin 4 promised byte-identical re-carry without the machinery that makes it work. Comparing "the same value" requires retaining it, and the object map holds only Live/Tombstoned. Exactly three carried-value maps exist (reduce.rs:999-1007), each threaded through seven sites; G3a needs four more, so 28 touch points the first draft omitted entirely. Added pin 4a with the seven sites enumerated. Site 4, base seeding, is the one that fails silently: a re-carry test that only reduces from empty cannot see a missing seed at all. Added t5b (base re-carry) and t13 (each of the four seeds killed separately), modelled on G1's documented instrument_values precedent at reduce.rs:13264. 3. The companion bump was stale. The tree is at 0.11.0 (G2b bumped it, textproj/src/lib.rs:47); the contract repeated G2b's 0.10.0 -> 0.11.0. Corrected to 0.11.0 -> 0.12.0 at both sites, with the negative vector rejecting 0.11.0. 4. Mutation table repairs: - t4's mutation was impossible. A create op's encode_canonical is a single push_lp_bytes line over one carried value, so there is nothing in the op to reorder. Moved to the carried type's struct_codec! declaration (codec.rs:1790), which is where the layout actually lives and is self-consistent across both halves -- exactly trap 4's shape. - t6 omitted PartDefinition.staves. Now three independent mutations, one per referential loop; an uncovered loop is a loop that deletes green. - t9 moved fixture and production together, which proves only that a bad score fails a checker. Fixture now constant and already dangling; only production mutates, one skipped check at a time. - t12 could not fail: grepping the whole file matches the implementation body, which contains the identifiers the doc comment is meant to gain. Now slices the invariant-10 doc block and searches only that. 5. Touch table missed testkit/src/layout_stub.rs:1373, whose 30..=34 range restates the coverage claim in prose. Added there and to the plan's trap 6, now five boundary-crossing literals rather than four. Editor authorization recorded as granted narrowly: barriers.rs for the four exhaustive subjects_of arms only, barrier.rs for the invalid-tag literal, comment, and assertions 35 -> 39 only. No other change in either crate. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV --- spec/CONTRACT_GENESIS_G3A_ENTITIES.md | 169 ++++++++++++++++++++++---- spec/PLAN_GENESIS_OPS.md | 17 ++- 2 files changed, 160 insertions(+), 26 deletions(-) diff --git a/spec/CONTRACT_GENESIS_G3A_ENTITIES.md b/spec/CONTRACT_GENESIS_G3A_ENTITIES.md index f330932..12a2dc1 100644 --- a/spec/CONTRACT_GENESIS_G3A_ENTITIES.md +++ b/spec/CONTRACT_GENESIS_G3A_ENTITIES.md @@ -36,8 +36,85 @@ Two consequences hold in the tree today: * `TimeAnchor::Measure` (`reduce.rs:1280`) can never resolve from empty. That half is G3b's. -G3a closes the staff-group half and completes the four root-level vectors. It -is the last genesis rung that moves no wire bound. +G3a completes the four root-level vectors. **How much of the staff-group half +it closes depends on §1.1, which is unresolved.** + +--- + +## 1.1 The pin, UNRESOLVED — `StaffGroup`/`Staff` authorship authority + +**Must be ratified before dispatch.** Drafted in the contract, decided by the +user — the shape G2b's `accidental_extensions` pin took. + +### The cycle + +`CreateStaff` requires its `group` to be a live `StaffGroup` +(`reduce.rs:4117`). `CreateStaffGroup` (pin 4) requires each of its `members` +to be a live `Staff`. Neither can name the other first, so **with mints only, +no authoring order produces a bidirectionally consistent group**: + +* `CreateStaffGroup(g, members: [])` → `CreateStaff(s, group: Some(g))` leaves + `s.group == Some(g)` while `g.members == []`. +* `CreateStaff(s, group: None)` → `CreateStaffGroup(g, members: [s])` leaves + the mirror image, and re-carrying `CreateStaff` with `group: Some(g)` is + `RecreateContentMismatch`, not an amendment. + +There is no `ModifyStaffGroup` and no `ModifyStaff`, and deletes are deferred +(§6.1). So the inconsistency is not merely unchecked — **it is unrepairable +within this packet.** + +### Why nothing in the tree decides it + +Invariant 10 checks resolution in **both** directions independently — a staff's +group is declared (`invariants.rs:1126`), a group's members are declared +(`:1135`) — and **agreement in neither**. No agreement check exists anywhere in +the crate. The specification declares `StaffGroup.members` +(`core_spec.tex:4231`) and `Staff.group` (`:5578`, "Visual grouping: which +staff group (if any) this staff belongs to") without stating which is +authoritative or requiring them to agree. **This is genuinely unspecified, not +merely unimplemented.** + +### Disposition A — `Staff.group` authoritative, `members` reduction-maintained + +`CreateStaffGroup` mints identity, name, and kind, and MUST carry +`members: []`; a non-empty `members` is refused or normalized away at +construction (the "subset over normalization" choice G2b faced). Thereafter +`StaffGroup.members` is maintained **by reduction**: `create_staff` with +`group: Some(g)` appends to `g.members`. Fully authorable from empty; joining +is commutative and set-union, which fits the CRDT discipline. + +Costs, stated honestly: it makes `members` a *derived* field of a stored type, +so byte-identical re-carry of `CreateStaffGroup` MUST compare against the +**carried** value (empty), never the current derived state — an explicit +sub-pin, and exactly the class of confusion `canonical_value!` cannot catch. It +also expands G3a beyond a pure mint packet, which is the property that made +this rung cheap. + +### Disposition B — declare the authority, defer the enforcement + +`Staff.group` is authoritative; `StaffGroup.members` is a denormalized +projection that **G3a does not maintain**. `CreateStaffGroup` carries `members` +as given and validates resolution only. Bidirectional agreement is stated as a +**known, filed gap** — a P13 candidate and a candidate invariant 21 — and G3a +claims nothing about it. + +Cost: a from-empty score can hold a grouped staff whose group lists no members. +That is *incomplete* data under a stated deferral, not silently wrong data — +but it is real, and the contract must not describe the defect as closed. + +### Recommendation + +**Disposition B**, and narrow the claim to match. A is the better end state, +but it invents an authoritative/derived split the specification does not make, +in the packet whose entire value is that it moves no bound and adds no +semantics. Ruling the authority now costs nothing and unblocks A later; +implementing A here buys a consistency property no consumer reads yet, at the +cost of turning a mint into a mint-plus-maintenance. + +**Under either disposition, t8's claim is narrowed** — see §4. The unqualified +"the defect closes" framing was wrong: what closes is that +`CreateStaff.group`'s precondition becomes *satisfiable*, not that a consistent +group becomes *authorable*. --- @@ -108,6 +185,38 @@ byte-identical value is `NoOp { AlreadyApplied }`; a live id with a differing value is `NoOp { PreconditionFailedUnderReduction { RecreateContentMismatch } }`; a tombstoned id is `NoOp { TargetTombstoned }`. +### Pin 4a — byte-identical re-carry needs a **carried-value map**, at seven sites each + +The first draft of pin 4 promised re-carry idempotence without the machinery +that makes it work, which would have shipped the promise and not the property. +Comparing "the same value" requires *retaining* the value; the object map holds +only `Live`/`Tombstoned`. + +Exactly three such maps exist today — `staff_values`, +`time_signature_values`, `instrument_values` (`reduce.rs:999`–`:1007`) — and +each is threaded through **seven** sites. G3a adds four more +(`staff_group_values`, `part_definition_values`, `analysis_layer_values`, +`view_values`), so this is **28 touch points**, none of which appeared in the +first draft's touch table: + +| # | Site | Existing lines | +|---|---|---| +| 1 | reducer state declaration | `reduce.rs:999`–`:1007` | +| 2 | `WorkingSnapshot` declaration | `:1106`–`:1108` | +| 3 | initialization | `:1388`–`:1390` | +| 4 | **base seeding** in `seed_from_graph` | `:1437`, `:1445`, `:1460` | +| 5 | mint insertion in the reducer | `:4134`, `:4183`, `:4219` | +| 6 | snapshot | `:7637`–`:7639` | +| 7 | restore | `:7677`–`:7679` | + +**Site 4 is the one that fails silently.** Without a base seed, a re-carry +against an entity that came from the *base* score — not from the log — finds no +retained value and misclassifies. G1 already documents this exact hazard and +its mutation for `instrument_values` (`reduce.rs:13264`–`:13268`); copy that +shape. **Each of the four omitted seeds must be killed separately** (t13), and +a base-recarry test must exist (t5b) — a re-carry test that only ever reduces +from empty cannot see a missing seed at all. + **The packet is self-contained**: `CreateView`'s precondition target is minted by `CreateAnalysisLayer` in this same packet, so the ordering is testable end-to-end without a base score. @@ -164,9 +273,13 @@ that is not repeatable. * `core_spec.tex` — the normative `OperationKind`/`OperationKindTag` listings and the spelled-out payload counts. * `text_projection.tex` — four new kind productions are a document-surface - change, so `COMPANION_VERSION` bumps (0.10.0 → 0.11.0), re-sweeping five live - version sites plus a changelog row and re-flipping the negative - `superseded_companion_version` vector. + change, so `COMPANION_VERSION` bumps **0.11.0 → 0.12.0**, re-sweeping five + live version sites plus a changelog row and re-flipping the negative + `superseded_companion_version` vector so it rejects **0.11.0**. + **The tree is already at 0.11.0** — G2b bumped it (`textproj/src/lib.rs:47` + and its doc comment). An earlier draft of this contract repeated G2b's + 0.10.0 → 0.11.0, which would have re-declared the current version as new and + left the negative vector rejecting a version no longer superseded. Use `\sectionsc{...}` for cross-document references. **`\ref` cannot cross documents** — `operation_catalog.tex` shipped an undefined reference that way. @@ -212,7 +325,7 @@ Every line number below re-verified against the working tree 2026-07-29. |---|---| | `crates/epiphany-ops/src/payload.rs` | four op structs + `CanonicalEncode`; `OperationKind` variants; `discriminant()` (`:390` region); `schema_major()` — **no arm**, pin 2; `introduced_minor()` (`:449` region); `tag()` (`:497` region); `encode_canonical` (`:543` region); tag vocabulary `@ Some(11)` (`:714` region); s1 epoch table (`:2475` region) | | `crates/epiphany-ops/src/envdecode.rs` | decode arms (`:599` region) and the tag-dispatch arms (`:901` region), plus validation | -| `crates/epiphany-ops/src/reduce.rs` | four dispatch arms + four mint reducers, on `create_staff`'s shape (`:4075`, `:4148`) | +| `crates/epiphany-ops/src/reduce.rs` | four dispatch arms + four mint reducers, on `create_staff`'s shape (`:4075`, `:4148`); **plus four carried-value maps at seven sites each — 28 touch points, see pin 4a** | | `crates/epiphany-ops/src/textproj_kind.rs` | production arms (`:232` region) **and** parse arms (`:572` region) | | `crates/epiphany-ops/src/migrate.rs` | both directions (`:192`, `:356` regions) | | `crates/epiphany-ops/src/v0.rs` | `V0OperationKind` variants (`:118` region) | @@ -234,18 +347,25 @@ citations. | `crates/epiphany-layout-ir/src/barrier.rs` | the "one past the vocabulary" tag `35` → `39` (`:1156`, assertion at `:1170`/`:1176`) and its comment | Deliberately a literal; unbumped, it pins a bug — a barrier prohibiting a new op encodes fine and cannot read back | | `crates/epiphany-testkit/tests/text_projection_grammar.rs` | count `35` → `39` and the message string (`:315`) | Hand-maintained literal parallel to a derived list | | `crates/epiphany-testkit/src/generators.rs` | drawn range `30..=34` → `30..=38` (`:1908`) and the never-drawn guard (`:1947`) | A kind never drawn is a kind never fuzzed | +| `crates/epiphany-testkit/src/layout_stub.rs` | the `30..=34` range in the s10/row-29 comment (`:1373`) | Prose, but it states the coverage claim the test rests on; stale text here is how a narrowed guard reads as a broad one | | `crates/epiphany-textproj/src/vectors.rs` | the negative vector whose "wrong version" moves with each bump | Silently passes for the wrong reason otherwise | -**Both `barriers.rs` and `barrier.rs` are editor-track files.** The one-time -authorization to edit them is per-packet and **does not generalise**; it is -granted for this packet for these two files only, for the exhaustiveness arms -and the literal bump. Touch nothing else in either crate. +**Both `barriers.rs` and `barrier.rs` are editor-track files.** Authorization +is per-packet and **does not generalise**. Granted 2026-07-29, narrowly: + +* `barriers.rs` — **the four required exhaustive `subjects_of` arms, and + nothing else.** +* `barrier.rs` — **the invalid-tag literal, its comment, and its assertions, + 35 → 39, and nothing else.** + +**No other change in either crate is authorized by this packet.** If the +workspace appears to need one, stop and report rather than widening. ### Text projection | File | What | |---|---| -| `crates/epiphany-textproj/src/lib.rs` | `COMPANION_VERSION` 0.10.0 → 0.11.0 and the live version sites | +| `crates/epiphany-textproj/src/lib.rs` | `COMPANION_VERSION` **0.11.0 → 0.12.0** (`:47`) and the live version sites | | `crates/epiphany-textproj/src/parse.rs` | kind productions | | `crates/epiphany-textproj/src/vectors.rs` | four positive document vectors + the negative-vector flip | @@ -287,15 +407,17 @@ t9 lesson from G2b. | t1 | All four kinds and tags are 35–38 in **both** spaces, and the discriminant byte leads each canonical encoding | Move any one kind to 39; then, separately, move its tag. Both must fail — the spaces are asserted independently (pin 1) | | t2 | `schema_major()` returns **0** for all four | Add them to the `=> 2` arm; must fail (pin 2's stated bug) | | t3 | A block containing all four stamps major **0**, and the op-block accept-set is untouched at 3 | Make one kind report major 2; must fail | -| t4 | Each op round-trips through `encode` → `envdecode` → reduce, byte-identical, with its decode vector pinned to **literal bytes** | Swap two fields in one op's `encode_canonical`; must fail. *(A self-consistent reorder applied to both codec halves passes round-trip tests — trap 4, the 3b-i lesson. Literal-byte vectors are what catch it.)* | +| t4 | Each op round-trips through `encode` → `envdecode` → reduce, byte-identical, with its decode vector pinned to **literal bytes** | **Swap two fields in the carried type's `struct_codec!` declaration** — e.g. `PartDefinition { id, name, staves }` → `{ id, staves, name }` (`core/src/codec.rs:1790`); the literal-byte vector must fail. *(A create op's `encode_canonical` is a single `push_lp_bytes` line over one carried value, so there is nothing in the op to reorder — the first draft's mutation was impossible. The reorder must go where the layout actually lives, and because `struct_codec!` moves both halves at once it is self-consistent and passes round-trip tests: trap 4, the 3b-i lesson. Literal-byte vectors are the only thing that catches it.)* | | t5 | Re-carrying a live id with a **byte-identical** value is `AlreadyApplied`; with a **differing** value is `RecreateContentMismatch`; a tombstoned id is `TargetTombstoned` | Return `Applied` for the differing-value case; must fail | -| t6 | Referential preconditions refuse under a graph: a `CreateStaffGroup` naming a non-live `Staff`, and a `CreateView` naming a non-live `AnalysisLayer`, are both `TargetMissing` | Drop the members loop from `create_staff_group`; must fail | +| t5b | **Re-carry against a base-derived entity**: reduce `new_onto` a score whose four vectors are already populated, re-carry each byte-identically, and get `AlreadyApplied` | Covered by t13 per-seed. A re-carry test that only reduces from empty **cannot see a missing base seed at all** — that is why this row is separate from t5 | +| t6 | All three referential loops refuse under a graph, **each asserted separately**: `CreateStaffGroup.members`, `CreatePartDefinition.staves`, and `CreateView.active_layers` naming a non-live target are each `TargetMissing` | **Three independent mutations**, one per loop: drop the members loop from `create_staff_group`; drop the staves loop from `create_part_definition`; drop the active-layers loop from `create_view`. Each must fail on its own row. *(The first draft omitted `PartDefinition.staves` entirely — one uncovered loop is one loop that can be deleted green.)* | | t7 | Those same preconditions are **not** enforced base-free | Remove the `if self.graph.is_some()` guard from one reducer; must fail — base-free has no universe to check against | -| t8 | **The defect closes**: from empty, `CreateInstrument` → `CreateStaffGroup` → `CreateStaff` **with `group: Some(...)`** succeeds and reaches a note | Replace the `CreateStaffGroup` dispatch arm with `OperationKind::CreateStaffGroup(_) => OperationEffect::Applied`, keeping the match exhaustive; must fail at the grouped-staff assertion while the spine stays applied | -| t9 | A score reduced from empty through all four ops **passes `check_invariants`** (pin 5) | Make `create_view` skip the `active_layers` check *and* author a dangling layer reference; invariant 10 must fire | +| t8 | From empty, `CreateInstrument` → `CreateStaffGroup` → `CreateStaff` **with `group: Some(...)`** succeeds and reaches a note — i.e. `CreateStaff`'s group precondition becomes **satisfiable** | Replace the `CreateStaffGroup` dispatch arm with `OperationKind::CreateStaffGroup(_) => OperationEffect::Applied`, keeping the match exhaustive; must fail at the grouped-staff assertion while the spine stays applied. **Claim narrowed per §1.1: this asserts satisfiability, NOT that a bidirectionally consistent group is authorable.** Under disposition B the test must additionally assert the known gap explicitly — `g.members` is empty while `s.group` is `Some(g)` — so the deferral is pinned rather than merely unmentioned | +| t9 | A score reduced from empty through all four ops **passes `check_invariants`**, and each skipped reducer check **independently** makes invariant 10 fire (pin 5) | **The fixture is constant across all mutations**: the baseline input already attempts a dangling reference in each of the three loops, and passes because the reducer refuses them. Then mutate **only production**, one skipped check at a time — three separate mutations, each of which must let its dangling reference through and make invariant 10 fire. *(The first draft moved the fixture and the production code together, which proves only that a hand-built bad score fails a checker — not that the reducer's refusal is what was holding the line.)* | | t10 | All four kinds carry **epoch 11**, and a block containing them stamps minor **11** | Assign epoch 10 to one kind; must fail. Run against **both** epoch sites separately (vocabulary annotation, s1 table) — each must be independently able to fail | -| t11 | Text projection round-trips all four kinds, and the companion version is 0.11.0 | Drop one parse arm; must fail | -| t12 | Invariant 10's doc comment names the four reference classes its body checks (pin 6) | Grep-assert the repaired prose is present; revert the comment to see it fail | +| t11 | Text projection round-trips all four kinds, and the companion version is **0.12.0**, with the negative vector rejecting **0.11.0** | Drop one parse arm; must fail. Separately, leave `COMPANION_VERSION` at 0.11.0; the negative vector must fail | +| t12 | Invariant 10's doc comment names the four reference classes its body checks (pin 6) | Grep-assert the repaired prose is present **within the invariant-10 doc block only** — slice the source from the `/// 10.` line to the `CrossCuttingRefsResolve,` line and search *that*. Revert the comment to see it fail. **Searching the whole file passes on the implementation body**, which contains the same identifiers the doc comment is supposed to gain — a guard that cannot fail | +| t13 | **Each of the four base seeds is load-bearing** (pin 4a, site 4) | **Four separate mutations**: skip seeding each of `staff_group_values`, `part_definition_values`, `analysis_layer_values`, `view_values` in `seed_from_graph`, one at a time. Each must make t5b fail. Model on G1's documented precedent for `instrument_values` (`reduce.rs:13264`–`:13268`) | **On t12's grep shape:** a self-matching needle is a real hazard — G2b hit it twice, once when a multi-line needle matched the test's own source and once @@ -323,7 +445,12 @@ iterate `include_str!` over each. State, with evidence: kinds/tags assigned and the two spaces asserted separately; that `schema_major()` gained **no** arm and no bundle file was touched; the four `canonical_value!` entries; that `textvalue_graph.rs` needed -no change; each precondition and its invariant-10 correspondence; the from-empty -grouped-staff defect closing; epoch 11 at both sites; the four-document sweep; -and the five boundary-crossing literals with their new values. Report each -mutation's **observed** output. Anything not done, say so plainly. +no change; **the four carried-value maps at all seven sites each, named site by +site**; each of the three referential loops and its invariant-10 +correspondence; **which §1.1 disposition was implemented and what t8 therefore +does and does not claim**; epoch 11 at both sites; the companion bump +0.11.0 → 0.12.0 with the negative vector rejecting 0.11.0; the four-document +sweep; and the six boundary-crossing literals with their new values. Report +each mutation's **observed** output — t6, t9, and t13 are multi-mutation rows +and each sub-mutation must be reported separately. Anything not done, say so +plainly. diff --git a/spec/PLAN_GENESIS_OPS.md b/spec/PLAN_GENESIS_OPS.md index a46bf27..726cbc5 100644 --- a/spec/PLAN_GENESIS_OPS.md +++ b/spec/PLAN_GENESIS_OPS.md @@ -24,7 +24,12 @@ remains, and it **splits into G3a and G3b** (ratified 2026-07-29, §4). Closed **P13-S13**. * **G3a** — the four root-level mint families (`CreateStaffGroup`, `CreatePartDefinition`, `CreateAnalysisLayer`, `CreateView`), kinds/tags - **35–38**, epoch **11**, all schema major **0**. Contracted. + **35–38**, epoch **11**, all schema major **0**. Contracted + (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md`), **blocked on one unresolved pin**: + §1.1, the `StaffGroup`/`Staff` authorship-authority ruling. With mints only + there is no authoring order that yields a bidirectionally consistent staff + group, and neither the tree nor the specification says which of + `Staff.group` and `StaffGroup.members` is authoritative. * **G3b** — `CreateMeasure` alone, kind/tag **39**, epoch **12**, carrying graph invariant **20** and a new `PreconditionFailureReason` at discriminant **16**. Scoped, not contracted. @@ -397,14 +402,16 @@ mints** — the same reasoning that kept the accept-set raise out of G2a. exhaustiveness forces an arm in `epiphany-editor-core`'s `subjects_of` (`barriers.rs:313`), and because `epiphany-testkit` depends on editor-core, a missing arm blocks conformance *and* `requirement_labels` — the gate - cannot run at all. Four further sites bake in a literal that only surfaces + cannot run at all. Five further sites bake in a literal that only surfaces once the workspace compiles: `layout-ir/src/barrier.rs:1156` (a tag "one past the vocabulary"), `testkit/tests/text_projection_grammar.rs:315` (a hardcoded kind *count*, with its message string at the same site), `testkit/src/generators.rs:1908` (a drawn-discriminant range plus a - never-drawn guard at `:1947`), and `textproj/src/vectors.rs` (a negative - vector whose "wrong version" is the one each bump moves to). Every G2/G3 - contract MUST enumerate these and budget the boundary crossing up front. + never-drawn guard at `:1947`), `testkit/src/layout_stub.rs:1373` (the same + range restated in prose that carries the coverage claim), and + `textproj/src/vectors.rs` (a negative vector whose "wrong version" is the + one each bump moves to). Every G2/G3 contract MUST enumerate these and + budget the boundary crossing up front. *(All four citations re-verified 2026-07-29; the three carried in earlier revisions had drifted — `barriers.rs:437`, `barrier.rs:1105`, `text_projection_grammar.rs:307` — which is exactly the failure mode a