diff --git a/spec/CONTRACT_GENESIS_G3A_ENTITIES.md b/spec/CONTRACT_GENESIS_G3A_ENTITIES.md index 12a2dc1..b062852 100644 --- a/spec/CONTRACT_GENESIS_G3A_ENTITIES.md +++ b/spec/CONTRACT_GENESIS_G3A_ENTITIES.md @@ -36,14 +36,15 @@ Two consequences hold in the tree today: * `TimeAnchor::Measure` (`reduce.rs:1280`) can never resolve from empty. That half is G3b's. -G3a completes the four root-level vectors. **How much of the staff-group half -it closes depends on §1.1, which is unresolved.** +G3a completes the four root-level vectors. **It closes the satisfiability half +only** — §1.1 (ratified) rules that a bidirectionally consistent staff group +remains unauthorable in this packet, by design and on the record. --- -## 1.1 The pin, UNRESOLVED — `StaffGroup`/`Staff` authorship authority +## 1.1 The pin, RESOLVED — `StaffGroup`/`Staff` authorship authority -**Must be ratified before dispatch.** Drafted in the contract, decided by the +**Ratified 2026-07-29: disposition B.** Drafted in the contract, decided by the user — the shape G2b's `accidental_extensions` pin took. ### The cycle @@ -90,31 +91,55 @@ 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 +### Disposition B — declare the authority, defer the enforcement — **RATIFIED** -`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. +Ratified 2026-07-29 with this precise meaning, which is **normative**: -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. +* **`Staff.group` is the sole authority for membership.** Every consumer reads + membership from `Staff.group`. Nothing may read `StaffGroup.members` to + decide whether a staff is in a group. +* **`StaffGroup.members` is a non-authoritative denormalized projection.** +* **G3a stores it but neither maintains nor trusts it.** `CreateStaffGroup` + carries `members` as given and validates resolution only (pin 4). +* **G3a permits both stale forms**, and they are equally permitted: + * a **missing** member — `s.group == Some(g)` while `g.members` omits `s`; + * a **spurious** member — `g.members` contains `s` while `s.group` is `None` + or names a *different* group. -### Recommendation + An earlier draft named only the first. Naming only the missing-member form + would have understated the ruling and left the spurious form looking like a + bug rather than a permitted state. -**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. +**This is a normative semantic ruling, not a deferral of one.** The earlier +draft's argument for B — that it "adds no semantics" while A does — was wrong +and is withdrawn. B *assigns authority to a field the specification left +unranked*, which is a semantic change; what it defers is **enforcement**, not +meaning. The honest statement of B's advantage over A is narrower: it adds +semantics without adding *machinery*, leaving the mint a mint. -**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*. +**Filed as P13-S16** (`spec/PASS13_CANDIDATES.md`) — the concrete gap, both +stale forms, the disposition-A fix, the candidate invariant 21, and the +instruction that consumers read `Staff.group` only. The earlier draft claimed +a "filed gap" while no such entry existed; it does now. + +**Disposition A remains the later maintenance/enforcement fix**, sequenced +after G3b so an invariant append is not competing with invariant 20. + +### What t8 must therefore claim + +**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*. + +**t8 must pin both asymmetric authoring orders**, not only the first: + +* `CreateStaffGroup(g, members: [])` → `CreateStaff(s, group: Some(g))` + ⟹ `s.group == Some(g)`, `g.members == []` — the **missing** form; +* `CreateStaff(s, group: None)` → `CreateStaffGroup(g, members: [s])` + ⟹ `g.members == [s]`, `s.group == None` — the **spurious** form. + +Both must be asserted to *hold*, as permitted states under the ruling. A test +that pins only one leaves the other free to change silently. --- @@ -337,9 +362,16 @@ Every line number below re-verified against the working tree 2026-07-29. ### Boundary crossings — budgeted up front (trap 6) -An `OperationKind` append is **not** containable to core + ops. All five -re-verified 2026-07-29; earlier revisions of the plan carried three drifted -citations. +An `OperationKind` append is **not** containable to core + ops. **Six +crossings: one exhaustive-match site plus five literal/prose sentinels.** All +six re-verified 2026-07-29; earlier revisions of the plan carried three drifted +citations, and earlier revisions of this contract alternated between five and +six by counting the exhaustive-match site inconsistently. + +The two classes fail differently, which is why they are counted together but +named apart. The **exhaustive-match** site fails loudly — the workspace will +not compile. The five **sentinels** fail silently: each stays green while +meaning something narrower than it says. | File | What | Why it bites | |---|---|---| @@ -407,12 +439,13 @@ 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 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.)* | +| t4 | Each op round-trips through `encode` → `envdecode` → reduce, byte-identical, with its decode vector pinned to **literal bytes** | **Four independent mutations, one per carried type** — swap two fields in each `struct_codec!` declaration: `PartDefinition { id, name, staves }` → `{ id, staves, name }` (`core/src/codec.rs:1790`), and likewise `AnalysisLayer` (`:1791`), `ViewDefinition` (`:1792`), `StaffGroup` (`:2329`). Each type's literal-byte vector must fail on its own. **These are four separate layouts; one mutation signs one of them.** Collapse to a single mutation only if the implementation consolidates all four behind one shared mechanism, and say so explicitly if it does. *(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 | | 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 | 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 | +| t8 | From empty, `CreateInstrument` → `CreateStaffGroup` → `CreateStaff` **with `group: Some(...)`** succeeds and reaches a note — i.e. `CreateStaff`'s group precondition becomes **satisfiable**. **Claim narrowed per §1.1: this asserts satisfiability, NOT that a bidirectionally consistent group is authorable** | 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 | +| t8b | **Both permitted stale forms are pinned** (§1.1): the missing form (`CreateStaffGroup(g, [])` → `CreateStaff(s, Some(g))` ⟹ `s.group == Some(g)`, `g.members == []`) and the spurious form (`CreateStaff(s, None)` → `CreateStaffGroup(g, [s])` ⟹ `g.members == [s]`, `s.group == None`). Both asserted to **hold**, as states the ruling permits | Make `create_staff_group` maintain the projection (append the staff to `g.members`), i.e. implement disposition A; the missing-form assertion must fail. Separately, make `create_staff` clear a spurious back-reference; the spurious-form assertion must fail. **Two mutations — a test pinning only one order leaves the other free to change silently** | | 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.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 | @@ -450,7 +483,8 @@ 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 +sweep; and the six boundary crossings — the one exhaustive-match site and the +five sentinels, each with its new value. 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/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index f773561..f6e2060 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -93,3 +93,4 @@ visible — a value with a wire form and no canonical carrier to reach it.) | 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–33 have no byte-level lock at all.** `operation_kind_wire_discriminants_are_golden` (`crates/epiphany-ops/src/payload.rs:1959`) declares `let table: [(OperationKind, u8); 30]`, covering 0..=29 and asserting for each that `kind.discriminant()` has not moved *and* that the discriminant byte truly leads the canonical encoding. **`TransposeInterval` (30, Push 4a), `CreateInstrument` (31, G1), `SetCanvasLayoutDefaults` (32) and `SetSpellingPrecedence` (33, G2a) are absent from that table**, so 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 four silently, and the encoding-leads-with-the-byte assertion never runs for them. The macro-guarded `OperationKindTag` half is unaffected (`operation_kind_tag_vocabulary!` is compile-enforced); this is the hand-written half. **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 | this file (found 2026-07-28 by the G-minor implementation while building s1's coverage; independently verified against the working tree at `ff9bd0f` — the array length literal is `30` and no arm for 30–33 appears in the table) | **open.** Deliberately no code change yet. **Not a live incorrectness:** every one of the four discriminants is currently correct, and `binary_format.tex:1443-1457`/`:1526-1527` carry them normatively — the gap is the *absence of a guard*, not a wrong byte. Fixing it is mechanical (extend the table to `; 34` and add the four rows), and the mutation that proves the fix is to change one of the four discriminants and watch the extended lock fail where it previously stayed green. **Worth doing as its own rung rather than as a rider**, because a golden-lock extension should land with its mutation evidence and nothing else in the diff. Note the sibling `phase3_tag_discriminants_are_golden` should be checked for the same drift at the same time | +| 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:5578`, `graph.rs:819`) names the group a staff belongs to; `StaffGroup.members` (`core_spec.tex:4231`, `graph.rs:1614`) 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:1126`), a group's members are declared (`:1135`) — 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:4117` 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, 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. Sequence it after G3b so an invariant append is not competing with G3b's invariant 20 | diff --git a/spec/PLAN_GENESIS_OPS.md b/spec/PLAN_GENESIS_OPS.md index 726cbc5..50328b7 100644 --- a/spec/PLAN_GENESIS_OPS.md +++ b/spec/PLAN_GENESIS_OPS.md @@ -25,11 +25,9 @@ remains, and it **splits into G3a and G3b** (ratified 2026-07-29, §4). * **G3a** — the four root-level mint families (`CreateStaffGroup`, `CreatePartDefinition`, `CreateAnalysisLayer`, `CreateView`), kinds/tags **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. + (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md`) and **ready to dispatch**; §1.1's + `StaffGroup`/`Staff` authorship-authority pin was ratified 2026-07-29 as + disposition B and filed as **P13-S16**. * **G3b** — `CreateMeasure` alone, kind/tag **39**, epoch **12**, carrying graph invariant **20** and a new `PreconditionFailureReason` at discriminant **16**. Scoped, not contracted. @@ -340,13 +338,24 @@ vocabulary.** Verified 2026-07-29 against the working tree: generated by the one `struct_codec!` macro (`codec.rs:510`, `:522`), so no `textvalue_graph.rs` work. What they lack is a `canonical_value!` entry. -**G3a closes a live defect, not merely a completeness gap.** All five object -kinds become `Live` **only** through base ingest (`reduce.rs:1449`–`:1563`); -no operation mints any of them. So `CreateStaff`'s group precondition -(`reduce.rs:4119`) is **currently unsatisfiable under from-empty reduction** — -a document built only from operations can never author a grouped staff — and -`TimeAnchor::Measure` (`reduce.rs:1280`) can never resolve. G1 opened this by -making from-empty reachable; G3a closes the staff-group half of it. +**G3a addresses a live defect, not merely a completeness gap — but it makes +the precondition *satisfiable*, not the relation *consistent*.** All five +object kinds become `Live` **only** through base ingest +(`reduce.rs:1449`–`:1563`); no operation mints any of them. So `CreateStaff`'s +group precondition (`reduce.rs:4119`) is **currently unsatisfiable under +from-empty reduction** — a document built only from operations can never author +a grouped staff — and `TimeAnchor::Measure` (`reduce.rs:1280`) can never +resolve. G1 opened this by making from-empty reachable. + +**What G3a closes is exactly the satisfiability half.** It does **not** make a +bidirectionally consistent staff group authorable: with mints only, no +authoring order yields agreement between `Staff.group` and +`StaffGroup.members`, and there is no modify operation to repair it. Ruled +2026-07-29 (`spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B): +`Staff.group` is the sole authority, `StaffGroup.members` is a +non-authoritative denormalized projection that G3a stores without maintaining, +and **both** stale forms — missing member and spurious member — are permitted. +Filed as **P13-S16**; disposition A is the later enforcement fix. **G3a — the four root-level mints.** Kinds/tags 35–38, epoch 11. Self-contained: `CreateView`'s precondition target is minted by `CreateAnalysisLayer` in the @@ -412,10 +421,14 @@ mints** — the same reasoning that kept the accept-set raise out of G2a. `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 - contract's touch table exists to prevent.)* + **Six crossings in total: one exhaustive-match site plus five + literal/prose sentinels.** The classes fail differently — the + exhaustive-match site refuses to compile, while every sentinel stays green + while meaning something narrower than it says. *(All six citations + re-verified 2026-07-29; 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 contract's touch table exists to + prevent.)* ## 6. Open rulings — needed before a dispatch contract