From a65d79d752db0b6ae9917812e2e85150ff67af3b Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Mon, 10 Aug 2026 17:42:18 +0200 Subject: [PATCH] P13-S16 amendment 1: post-landing corrections, consolidated Five corrections against CONTRACT_P13S16_PROJECTION.md, all against the document rather than the code -- aee4ff9 is accepted and unchanged. Filed as one amendment on the owner's decision because the findings are not independent: two pairs share a root cause, and separate rounds would have recorded symptoms while hiding the causes. Root A -- the contract reasoned about MECHANISM where the question was what the test ASSERTS. Findings 1 and 3. Both cells are right about the production code and wrong about the observation, because a test that verifies its own fixture is meaningful fails for a second reason no mechanism argument reaches. Root B -- enumeration where completeness was required. Findings 2 and 4. Both lists were built by reading one file. The contract already carries derive-do- not-enumerate under pin 10a and 6 item 1, and broke it twice in its own apparatus. 1. Invariant 21 does not detect the undo residue (0.6, pin 5a, pin 6b). It abstains on dangling members by design; M5 shows invariant 10 firing instead. The hole was already covered before this rung. u5's direct members assertion is what signs pin 5 -- the fallback pin 6b itself names -- so nothing is unsigned. 2. 3's M6a row names six failing tests; seven occur. The fifth all() consumer is in tests/score_graph.rs, outside the four-in-generators.rs list. 3. 3's t8d-under-M2 survivor cell is falsified -- it fails on non-vacuity, not idempotence. The assertion must not be weakened: under M2 t8d is genuinely vacuous. The other falsifiable cell, t9 under M1, was CONFIRMED. 4. Pin 10 cites four of the nine sites its instruction covers, and gate 6 cannot see core_spec.tex's "exactly 20 invariants" sentence. 5. cargo test --workspace truncates the failure set at the first failing suite -- exactly the condition every mutation creates. 3's uniform rule and gate 1 now specify --no-fail-fast. Finding 6 is WITHDRAWN as false and retained as record. Pin 8's line numbers were exact on the ratified tree 34232dc -- all four verified -- and only stopped matching because this rung inserted ~1,500 lines above them. It had been reported without the cited locations ever being measured. Writing the amendment is what forced the check, which is an argument for consolidating rather than filing six rounds. Touch row 12 added, so spec/EVIDENCE_P13S16_EXECUTION.md is committed rather than left untracked: the findings are conclusions, and the annex is the evidence they were derived from, including the runs that falsified two of this contract's own predictions. Its trailing whitespace is stripped so gate 4 passes, and it says so. CLAUDE.md, the handoff and the ledger row are corrected in step -- all three said "six findings", which is now the count before review rather than after. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01Ps1szk2mSfgp4Cz21eVH9x --- CLAUDE.md | 2 +- spec/CONTRACT_P13S16_PROJECTION.md | 221 +++- spec/EVIDENCE_P13S16_EXECUTION.md | 1657 ++++++++++++++++++++++++++++ spec/HANDOFF_2026-08-07.md | 16 +- spec/PASS13_CANDIDATES.md | 2 +- 5 files changed, 1881 insertions(+), 17 deletions(-) create mode 100644 spec/EVIDENCE_P13S16_EXECUTION.md diff --git a/CLAUDE.md b/CLAUDE.md index 5831811..91e4e02 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -17,7 +17,7 @@ model with a LaTeX specification suite as its source of truth. | Track | Lives in | Current head | |---|---|---| -| **Spec / Pass 13** — wire format, bundle, ops, text projection, the `.tex` suite | `spec/`, `crates/epiphany-{core,ops,bundle,textproj,testkit}` | **P13-S27 LANDED** (`4df8e25`); **P13-S16 LANDED** (`aee4ff9`) — six findings against its own contract are unamended, see its `PASS13_CANDIDATES.md` row | +| **Spec / Pass 13** — wire format, bundle, ops, text projection, the `.tex` suite | `spec/`, `crates/epiphany-{core,ops,bundle,textproj,testkit}` | **P13-S27 LANDED** (`4df8e25`); **P13-S16 LANDED** (`aee4ff9`), its post-landing corrections amended in at `CONTRACT_P13S16_PROJECTION.md` §7 | | **Editor / T4** — the editing seam, engraving, the toolkit spike | `spec/PLAN_EDITOR_APP.md`, `spec/CONTRACT_EDITOR_*`, `spikes/`, `crates/epiphany-{editor-core,editor-gui,engrave,layout-ir,glyphs,render-svg}` | T4 spike, round 2 built but not run | They are currently independent. The T1b/P13-S27 collision in diff --git a/spec/CONTRACT_P13S16_PROJECTION.md b/spec/CONTRACT_P13S16_PROJECTION.md index 1258ec8..007afb9 100644 --- a/spec/CONTRACT_P13S16_PROJECTION.md +++ b/spec/CONTRACT_P13S16_PROJECTION.md @@ -1,22 +1,30 @@ # Contract — P13-S16: the projection gets maintained -**Status:** **RATIFIED 2026-08-09, on the authority of the repository owner, on the -evidence of the review records below — the last of which returned zero findings. -DISPATCHABLE.** +**Status:** **LANDED 2026-08-10 at `aee4ff9`**, accepted by the repository owner after +independent review of every pin, gate and mutation; reconciled at `3328b2c`. +**RESOLVED — the rung is closed.** **THE PINS ARE FROZEN. They may be executed, not edited.** A defect found during execution is **reported, not patched in place** — if it needs a pin change, that is its own amendment with its own review round. *(S27's discipline, and the reason its post-execution findings -became amendments 1–7 rather than silent edits to frozen text.)* +became amendments 1–7 rather than silent edits to frozen text.)* **That discipline held: +execution reported six findings against this contract and patched none of them. They are +§7 — where a seventh review, of the findings themselves, **withdrew one as false**, leaving +five.** -**NOT YET DISPATCHED.** Ratification and dispatch are separate acts; no execution -instruction has been given, and **no implementation work has begun.** +> *(This block read **"RATIFIED … DISPATCHABLE"** and **"NOT YET DISPATCHED … +> no implementation work has begun"** until the rung landed. Both were true when written. +> The pins are still frozen — landing does not unfreeze them, it only means nothing +> further will execute them.)* **P13-S27 landed and was accepted at `4df8e25`**, so pin 0's blocker is discharged: an authority now defines the implementation's current reduction semantics -(`epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION`, currently **`0`**), and +(`epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION`), and `core_spec.tex:11614`'s requirement is **met** — a stale canonical base is refused with -`CanonicalBaseRequiresRebuild` on both the read and write paths. +`CanonicalBaseRequiresRebuild` on both the read and write paths. **This rung then made +that constant's first bump, `0` → `1`** *(this block said "currently `0`", true until +pin 12 executed; the constant's own `Bumps` list is the single origin for its value and +no figure is restated here)*. > **Which independent rounds closed, and what each found, are the review records below. > This block does not restate them, and states no count and no ordinal** — a status line @@ -2222,3 +2230,200 @@ its evidence at `invariants.rs:69`–`:71` must stay intact. asserted before and after. 5. Anything contradicting this contract. A contract defect reported is worth more than a contract satisfied. + +--- + +## §7. POST-LANDING CORRECTIONS — AMENDMENT 1, 2026-08-10 + +**The rung landed at `aee4ff9` and was reconciled at `3328b2c`. None of these +corrections changes that**: the implementation is accepted, and every finding below is +against *this document*, not against the code. What they correct is the **evidence +apparatus** — tables, citations and attributions a later reader would otherwise take as +accurate. §6 item 5 asked for exactly this: *"a contract defect reported is worth more +than a contract satisfied."* + +**Consolidated into one amendment on the owner's decision**, against this repository's +usual one-finding-one-round rhythm. The reason is not economy: **the findings are not +independent.** Two pairs share a root cause, and separate rounds would have recorded +symptoms while hiding the two causes — which are the more useful finding and the only +part of this section that generalises to the next contract. + +### The two root causes + +**Root A — the contract reasoned about MECHANISM; execution wrote assertions that check +their own NON-VACUITY.** Findings 1 and 3. Both cells are correct about what the +production code does and wrong about what the test observes, because a test that +verifies its own fixture is meaningful fails for a *second* reason the mechanism +argument never considered. **A survivor cell derived from "what does this code do?" +is incomplete: the question is "what does this test assert?"** + +**Root B — enumeration where completeness was required.** Findings 2 and 4. Both lists +were built by reading one file and generalising. This contract already carries that rule +under pin 10a and §6 item 1 — *derive, do not enumerate* — and broke it twice in its own +supporting apparatus. **A list that must be exhaustive has to be produced by a search +over the whole tree, and the search has to be stated so it can be re-run.** + +Finding 5 is a singleton: a tooling default that silently truncates evidence. **Finding 6 +was withdrawn** — writing this section is what forced its citations to be measured rather +than assumed, which is the argument for consolidating rather than filing six rounds. + +### Finding 1 — invariant 21 does not detect the undo residue. §0.6, pin 5a, pin 6b + +**Claimed.** §0.6's first bullet motivates invariant 21 partly by the undo hole: +*"`reduce.rs:2967` removes a `Staff` from `score.staves` on undo but leaves its id in any +live group's `members`."* Pin 5a's assertion 3 asks for the invariant-21 exactness form +*"so the test fails on a residue whichever direction it leaves"*, and pin 6b closes by +saying M5 *"signs the undo hole by requiring invariant 21 to **observe** the residue."* + +**Observed.** M5 was run. Invariant 21 reported `[]`. Invariant 10 +`CrossCuttingRefsResolve` reported *"staff group … member staff … is not declared"*. + +**Why.** The residue is a **dangling** member — the staff is gone from the graph +entirely — and invariant 21 abstains on those by design. That is not an implementation +choice made at the keyboard: pin 6 defines the G→S direction as *"a group listing a staff +**whose own `group` is not that group**"*, and pin 6a's `m41b` fixture is a **live** staff +pointing elsewhere. A staff that does not exist has no `group` to compare against. + +**Consequence.** The undo hole was **already covered, by invariant 10, before this rung**. +It is not invariant 21's work, and pin 5a's assertion 3 cannot fail on it — under M5 that +assertion passes. Invariant 21's remaining justification is §0.6's *second* bullet, base +ingest admitting a disagreeing pair of **live** objects, which is untouched and +sufficient. + +**What signs pin 5, then.** `u5`'s assertion 2 — the direct `!members.contains(&s)` +check — which is the fallback pin 6b names in its own next sentence. **Nothing is +unsigned**; the coupling's conclusion survives its mechanism being wrong. Execution also +added an assertion 4 asserting the *whole* invariant set clean, which does catch the +dangling residue. + +**Correction.** §0.6's first bullet is a claim about invariant **10**. Pin 5a's assertion +3 is a genuine check on the *agreement* directions and no more; the residue check is +assertion 2. Pin 6b's closing sentence should read that M5 signs the undo hole by +requiring the leftover member to be absent **directly on the materialized score**. + +### Finding 2 — §3's M6a row names six failing tests; seven occur + +**Claimed.** *"**M6a** delete S→G dispatch | **six** — see M6's own table"*, its +dependency list citing *"touch row 8 (`GraphInvariant`'s four `all()` consumers, +`generators.rs:991`/`:1004`/`:1025`/`:1042`)"*. + +**Observed.** Seven, under `cargo test --workspace --no-fail-fast`. The seventh is +`full_invariant_sweep_via_public_api`, `crates/epiphany-core/tests/score_graph.rs:146` — +a **fifth** `all()` consumer, in an integration suite rather than in `generators.rs`. + +**Why.** The consumer list was built by reading `generators.rs`. Derived across the +workspace, `GraphInvariant::all()` has **five** iterating consumers plus the count guard +in `invariants.rs`. + +**Correction.** M6a's MUST-fail column is seven. The dependency list must cite the +derivation — a workspace-wide search for `GraphInvariant::all()` — not four line numbers +in one file. **Per §3's own rule, a failure outside the MUST-fail column is a finding; +this is that finding, produced as designed.** + +### Finding 3 — §3's `t8d`-under-M2 survivor cell is falsified + +**Claimed.** *"`t8d` — pin 4 seeds from the carried value with `members` emptied, so its +re-carry still matches"*, listed among M2's required survivors and flagged in §3 as one +of two cells *"stated so they can be falsified."* + +**Observed.** `t8d` **fails** under M2, at +*"precondition: the materialized base must carry the maintained members, or this test is +not exercising the reload hazard at all"* — `Some([])` against `Some([staff])`. + +**Why.** The cell's reasoning about the re-carry is **correct**: with `members` emptied +both sides compare `[]` and the idempotence assertion would still pass. But `t8d` also +asserts that its base is non-trivial, and under M2 it is not. That assertion did not +exist when the table was written — pin 4a says only *"add `t8d`"*. + +**And it must not be weakened.** Under M2 `t8d` genuinely is vacuous: the base carries +`[]`, the re-carry trivially matches, and the test would pass while exercising nothing +about the reload hazard. Removing the guard would make `t8d` stop testing pin 4 exactly +when maintenance is broken. + +**Correction.** `t8d` moves to M2's MUST-fail column, annotated: *fails on non-vacuity, +not on idempotence.* **The other falsifiable cell, `t9` under M1, was CONFIRMED** — it +survived, because pin 1a emptied its fixture. + +### Finding 4 — pin 10 cites four of nine sites, and gate 6 cannot see the count sentence + +**Claimed.** Pin 10 names `operation_catalog.tex:1265`–`:1278` and `:1531`–`:1540`, and +`core_spec.tex:5585`–`:5591` and `:4235`–`:4241`. + +**Observed.** Its *instruction* — rewrite the disposition-B semantics to the maintained +rule — covers **nine** sites. The five uncited: `operation_catalog.tex`'s **ruling block** +(which said *"Disposition A … remains the later maintenance/enforcement fix, sequenced +after G3b"* — superseded by this very rung), its referential-precondition list naming +`CreateStaffGroup.members`, §CreateStaffGroup's **Reduction rule** paragraph stating the +graph-aware liveness precondition pin 1 removed; and `core_spec.tex`'s `OperationKind` +enum comment and its **"This enumeration contains exactly 20 invariants"** sentence. + +**And gate 6 cannot catch the last one.** It checks *"the `core_spec.tex` enumeration +ending at 21"*, which passes with the count sentence still reading 20 — leaving the +specification asserting a count its own box contradicts. + +**Correction.** Pin 10's citations are illustrative, not exhaustive, and must say so; +the obligation is the instruction. Gate 6 must additionally read the count sentence. +*(Execution rewrote all nine plus two consequences — §CreateStaff's undo paragraph, which +otherwise described an undo leaving the projection disagreeing, and an explicit note that +`CreateStaffGroup` is deliberately outside the graph-aware list.)* + +### Finding 5 — `cargo test --workspace` truncates the failure set + +**Claimed.** §3's uniform rule requires *"the complete set of tests that failed"*, and +gate 1 names the bare command. + +**Observed.** Bare, `cargo test --workspace` stops at the first failing suite. Under M6a +it reported **6 failures across 4 suites / 475 tests**; with `--no-fail-fast`, **7 across +42 suites / 1583**. + +**Consequence.** Every mutation creates precisely the condition that truncates the +output, so the bare command **cannot** produce the evidence §3 demands — and the +truncated set reads as a complete one, which is how M6a's seventh failure would have gone +unseen and the table would have appeared to be confirmed. + +**Correction.** §3's uniform rule and gate 1 both specify +`cargo test --workspace --no-fail-fast`. *(`CLAUDE.md` now carries this too, since it +generalises to every future mutation rung.)* + +### ~~Finding 6 — pin 8's line numbers had drifted~~ — **WITHDRAWN, IT WAS NOT A DEFECT** + +**This was reported during execution and is false.** It is retained rather than deleted +because a withdrawn finding is part of the review record. + +**Claimed at the time.** That pin 8's `:16826`, `:16983`, `:17125`, `:17333` had drifted, +and that the tests had to be located by name instead. + +**Measured against `34232dc`, the ratified tree those numbers describe:** + +| test | pin 8 says | actual at `34232dc` | +|---|---|---| +| `u2a_a_live_staff_naming_the_group_blocks_its_undo` | `:16826` | `16826` | +| `u2bf_a_the_staff_group_guard_holds_base_free` | `:16983` | `16983` | +| `u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo` | `:17125` | `17125` | +| `u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole` | `:17333` | `17333` | + +**All four exact.** The numbers only stopped matching *during* execution, because this +rung inserted roughly 1,500 lines above them — on the landed tree they sit at `17235`, +`17392`, `17534`, `17742`. **That is not drift in the pin; it is the pin describing the +tree it was written against, while the tree changed underneath it.** Every contract's +line numbers do that the moment execution begins. + +**How the false finding was produced, since that is the transferable part.** The tests +were located by name — correctly, per the pin's own instruction — and the line numbers +were then *assumed* stale without being measured, and a fabricated `+21` was attached to +make the claim concrete. **A locator that was never consulted cannot be reported as +wrong.** The check costs one `git show : | grep -n`, and it reverses +the conclusion. + +**Pin 8 needs no correction.** Its own warning — *"names are stable; line numbers are a +convenience"* — is what made the drift harmless, and it worked exactly as intended. + +### Touch row 12 — the evidence annex. ADDED BY THIS AMENDMENT + +| # | File | Change | +|---|---|---| +| **12** | `spec/EVIDENCE_P13S16_EXECUTION.md` | **ADDED POST-LANDING.** The execution evidence annex: every mutation's verbatim failing output, every required survivor's pass verdict by name, and every gate's command, output and source quotation. Held untracked through execution because no touch row covered it and gate 4 requires every staged path to be a §2 row. **This row is that touch row.** The file states in its own header that it is a review artifact and not part of the candidate; that header stays accurate — it documents `aee4ff9`, it is not part of it | + +**Why it is worth committing.** The findings above are conclusions; the annex is the +evidence they were derived from, including the runs that falsified two of this contract's +own predictions. **A finding whose evidence has been discarded is a claim.** diff --git a/spec/EVIDENCE_P13S16_EXECUTION.md b/spec/EVIDENCE_P13S16_EXECUTION.md new file mode 100644 index 0000000..da823ab --- /dev/null +++ b/spec/EVIDENCE_P13S16_EXECUTION.md @@ -0,0 +1,1657 @@ +# P13-S16 — execution evidence annex + +Companion to the §6 report for `spec/CONTRACT_P13S16_PROJECTION.md`. + +**Status: review artifact, NOT part of the candidate.** This file is deliberately +**not staged**: it does not appear in the contract's §2 touch table, and gate 4 +requires every staged path to be a §2 row. Including it in the commit would need +its own amendment adding a touch row. It is written here rather than kept in a +temporary directory so the evidence survives the review. + +**Whitespace.** Trailing whitespace has been stripped throughout, so that +`git diff --cached --check` passes. It carried no information: it appears only where a +quoted source line or panic-message line is empty and this file's `: ` +prefix left a space behind. No other character of any quotation is altered. + +**Provenance.** Part 1 is generated from the retained +`cargo test --workspace --no-fail-fast` logs of each mutation run; Part 2 is +extracted from the staged tree and from `git show HEAD`. Neither part is retyped +from memory: failing output is reproduced verbatim, survivors are matched to +their `... ok` verdict lines from the same run, and source slices are located by +brace matching rather than by line number. + +**Candidate this evidence describes:** 14 staged paths on `HEAD` = `34232dc`, +working tree byte-identical to the index, `git diff --cached --check` clean, +1583 passed / 0 failed / 0 ignored across 42 suites. + +--- + +# P13-S16 — EVIDENCE ANNEX, PART 1: MUTATIONS + +Generated from the retained `cargo test --workspace --no-fail-fast` logs. +Every failing test's stdout is reproduced verbatim; every required survivor +is listed by its full name with the verdict line matched from the same run. + + +============================================================================== +## M1 — remove pin 1's refusal +============================================================================== + +Aggregate: passed 1580 failed 3 + +### Complete observed failure set (3) + + reduce::tests::t6_g3a_referential_loops_refuse_a_dangling_target_under_a_graph + reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free + reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused + +### Verbatim failing output + +---- reduce::tests::t6_g3a_referential_loops_refuse_a_dangling_target_under_a_graph stdout ---- +thread 'reduce::tests::t6_g3a_referential_loops_refuse_a_dangling_target_under_a_graph' (3108457) panicked at crates/epiphany-ops/src/reduce.rs:16276:9: +assertion `left == right` failed: CreateStaffGroup carrying a non-empty members must refuse ContainerNotEmpty (P13-S16 pin 1), not TargetMissing + left: Some(Applied) + right: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: ContainerNotEmpty } }) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +---- reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free stdout ---- +thread 'reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free' (3108459) panicked at crates/epiphany-ops/src/reduce.rs:16361:9: +assertion `left == right` failed: an empty-container precondition asks only about the carried value, so it refuses base-free too (P13-S16 pin 1a); a graph gate here would wrongly accept + left: Some(Applied) + right: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: ContainerNotEmpty } }) + +---- reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused stdout ---- +thread 'reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused' (3108463) panicked at crates/epiphany-ops/src/reduce.rs:16625:9: +assertion `left == right` failed: spurious order: CreateStaffGroup carrying [s] must refuse ContainerNotEmpty (P13-S16 pin 1) + [1] spurious-order CreateStaffGroup effect: Some(Applied) + [2] spurious-order g.members: Some([StaffId(0000000000000002:0000000000000005)]) + [3] missing-order g.members: Some([StaffId(0000000000000001:0000000000000005)]) + [4] missing-order invariant-21 violations: [] + left: Some(Applied) + right: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: ContainerNotEmpty } }) + +#### Structural gate — Gate 8 under M1 (refusal removed) + +``` +$ read the brace-matched create_staff_group slice (4551..4598), production source + empty-members refusal present : False + TypedObjectId::Staff( present : False + TargetMissing present : False + => GATE 8 FAILS +``` + +### Required survivors, each by name (16) + + PASS t8c_recarry_compares_against_the_carried_members_not_the_derived + test reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived ... ok + PASS t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent + test reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent ... ok + PASS u5_undoing_a_staff_strips_it_from_the_live_groups_members + test reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members ... ok + PASS u2a_a_live_staff_naming_the_group_blocks_its_undo + test reduce::tests::u2a_a_live_staff_naming_the_group_blocks_its_undo ... ok + PASS u2bf_a_the_staff_group_guard_holds_base_free + test reduce::tests::u2bf_a_the_staff_group_guard_holds_base_free ... ok + PASS u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo + test reduce::tests::u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo ... ok + PASS u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole + test reduce::tests::u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole ... ok + PASS m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok + PASS m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok + PASS invariant_21_negative_generator_breaks_staff_to_group_only + test generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only ... ok + PASS every_invariant_has_a_negative_generator + test generators::tests::every_invariant_has_a_negative_generator ... ok + PASS every_invariant_shrinks_to_a_small_witness + test generators::tests::every_invariant_shrinks_to_a_small_witness ... ok + PASS shrink_is_idempotent + test generators::tests::shrink_is_idempotent ... ok + PASS negative_generators_are_reasonably_targeted + test generators::tests::negative_generators_are_reasonably_targeted ... ok + PASS full_invariant_sweep_via_public_api + test full_invariant_sweep_via_public_api ... ok + PASS t9_from_empty_through_all_four_g3a_ops_passes_check_invariants + test reduce::tests::t9_from_empty_through_all_four_g3a_ops_passes_check_invariants ... ok + +============================================================================== +## M2 — remove pin 2's append +============================================================================== + +Aggregate: passed 1580 failed 3 + +### Complete observed failure set (3) + + reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused + reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived + reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent + +### Verbatim failing output + +---- reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused stdout ---- +thread 'reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused' (3116580) panicked at crates/epiphany-ops/src/reduce.rs:16612:9: +assertion `left == right` failed: missing order: g.members is MAINTAINED to [s] (P13-S16 pin 2), not left empty as disposition B permitted + [1] spurious-order CreateStaffGroup effect: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: ContainerNotEmpty } }) + [2] spurious-order g.members: None + [3] missing-order g.members: Some([]) + [4] missing-order invariant-21 violations: [InvariantViolation { invariant: StaffGroupMembershipAgreement, witness: "S->G: staff StaffId(0000000000000001:0000000000000005) names group StaffGroupId(0000000000000001:0000000000000003), but that group's members omit it" }] + left: Some([]) + right: Some([StaffId(0000000000000001:0000000000000005)]) + +---- reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived stdout ---- +thread 'reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived' (3116581) panicked at crates/epiphany-ops/src/reduce.rs:16742:9: +assertion `left == right` failed: and the graph's derived members must genuinely hold [s] at that moment — otherwise AlreadyApplied proves nothing about separation + left: Some([]) + right: Some([StaffId(0000000000000001:0000000000000005)]) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +---- reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent stdout ---- +thread 'reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent' (3116582) panicked at crates/epiphany-ops/src/reduce.rs:16834:9: +assertion `left == right` failed: precondition: the materialized base must carry the maintained members, or this test is not exercising the reload hazard at all + left: Some([]) + right: Some([StaffId(0000000000000001:0000000000000005)]) + +#### Structural gate — Gate 8 under M2 (append removed; pin 1 untouched) + +``` +$ read the brace-matched create_staff_group slice (4552..4598), production source + empty-members refusal present : True + TypedObjectId::Staff( present : False + TargetMissing present : False + => GATE 8 PASSES +``` + +### Required survivors, each by name (9) + + PASS u5_undoing_a_staff_strips_it_from_the_live_groups_members + test reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members ... ok + PASS m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok + PASS m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok + PASS invariant_21_negative_generator_breaks_staff_to_group_only + test generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only ... ok + PASS every_invariant_has_a_negative_generator + test generators::tests::every_invariant_has_a_negative_generator ... ok + PASS every_invariant_shrinks_to_a_small_witness + test generators::tests::every_invariant_shrinks_to_a_small_witness ... ok + PASS shrink_is_idempotent + test generators::tests::shrink_is_idempotent ... ok + PASS negative_generators_are_reasonably_targeted + test generators::tests::negative_generators_are_reasonably_targeted ... ok + PASS full_invariant_sweep_via_public_api + test full_invariant_sweep_via_public_api ... ok + +============================================================================== +## M3 — pin 3 writes derived members +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived + +### Verbatim failing output + +---- reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived stdout ---- +thread 'reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived' (3213206) panicked at crates/epiphany-ops/src/reduce.rs:16746:9: +assertion `left == right` failed: a byte-identical re-carry must compare against the CARRIED members and read AlreadyApplied; graph members at this moment: Some([StaffId(0000000000000001:0000000000000005)]) + left: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: RecreateContentMismatch } }) + right: Some(NoOp { reason: AlreadyApplied }) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (4) + + PASS t8b_the_projection_is_maintained_and_the_spurious_form_is_refused + test reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused ... ok + PASS u5_undoing_a_staff_strips_it_from_the_live_groups_members + test reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members ... ok + PASS m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok + PASS m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok + +============================================================================== +## M4 — restore group.clone() at the base seed +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent + +### Verbatim failing output + +---- reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent stdout ---- +thread 'reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent' (3221152) panicked at crates/epiphany-ops/src/reduce.rs:16838:9: +assertion `left == right` failed: across a reload the re-carry must still compare against the CARRIED members (P13-S16 pin 4); base members were Some([StaffId(0000000000000001:0000000000000005)]) + left: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: RecreateContentMismatch } }) + right: Some(NoOp { reason: AlreadyApplied }) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (1) + + PASS t8c_recarry_compares_against_the_carried_members_not_the_derived + test reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived ... ok + +============================================================================== +## M5 — remove pin 5's strip +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members + +### Verbatim failing output + +---- reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members stdout ---- +thread 'reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members' (3229174) panicked at crates/epiphany-ops/src/reduce.rs:18265:9: +P13-S16 pin 5: undoing the staff must strip StaffId(0000000000000001:0000000000000005) from the live group's members + post-undo g.members: Some([StaffId(0000000000000001:0000000000000005)]) + invariant-21 violations: [] + staff StaffId(0000000000000001:0000000000000005) still in graph: false + ALL violations: [InvariantViolation { invariant: CrossCuttingRefsResolve, witness: "staff group StaffGroupId(0000000000000001:0000000000000001) member staff StaffId(0000000000000001:0000000000000005) is not declared" }] +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (9) + + PASS t8b_the_projection_is_maintained_and_the_spurious_form_is_refused + test reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused ... ok + PASS t8c_recarry_compares_against_the_carried_members_not_the_derived + test reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived ... ok + PASS t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent + test reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent ... ok + PASS u2a_a_live_staff_naming_the_group_blocks_its_undo + test reduce::tests::u2a_a_live_staff_naming_the_group_blocks_its_undo ... ok + PASS u2bf_a_the_staff_group_guard_holds_base_free + test reduce::tests::u2bf_a_the_staff_group_guard_holds_base_free ... ok + PASS u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo + test reduce::tests::u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo ... ok + PASS u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole + test reduce::tests::u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole ... ok + PASS m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok + PASS m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok + +============================================================================== +## M6a — delete the S->G dispatch call +============================================================================== + +Aggregate: passed 1576 failed 7 + +### Complete observed failure set (7) + + full_invariant_sweep_via_public_api + generators::tests::every_invariant_has_a_negative_generator + generators::tests::every_invariant_shrinks_to_a_small_witness + generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only + generators::tests::negative_generators_are_reasonably_targeted + generators::tests::shrink_is_idempotent + invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + +### Verbatim failing output + +---- full_invariant_sweep_via_public_api stdout ---- +thread 'full_invariant_sweep_via_public_api' (3704413) panicked at crates/epiphany-core/tests/score_graph.rs:148:9: +StaffGroupMembershipAgreement not reported on its negative graph +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +---- generators::tests::every_invariant_has_a_negative_generator stdout ---- +thread 'generators::tests::every_invariant_has_a_negative_generator' (3704120) panicked at crates/epiphany-core/src/generators.rs:1015:13: +negative generator for StaffGroupMembershipAgreement did not violate it; full report: [] + +---- generators::tests::every_invariant_shrinks_to_a_small_witness stdout ---- +thread 'generators::tests::every_invariant_shrinks_to_a_small_witness' (3704121) panicked at crates/epiphany-core/src/generators.rs:954:5: +shrink starting point must violate the target invariant + +---- generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only stdout ---- +thread 'generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only' (3704122) panicked at crates/epiphany-core/src/generators.rs:1088:9: +assertion `left == right` failed: raw: expected exactly the invariant-21 S->G violation and nothing else, got [] + left: 0 + right: 1 +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +---- generators::tests::negative_generators_are_reasonably_targeted stdout ---- +thread 'generators::tests::negative_generators_are_reasonably_targeted' (3704123) panicked at crates/epiphany-core/src/generators.rs:1175:13: +StaffGroupMembershipAgreement not among {} + +---- generators::tests::shrink_is_idempotent stdout ---- +thread 'generators::tests::shrink_is_idempotent' (3704126) panicked at crates/epiphany-core/src/generators.rs:954:5: +shrink starting point must violate the target invariant + +---- invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group stdout ---- +thread 'invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group' (3704211) panicked at crates/epiphany-core/src/invariants.rs:6288:9: +assertion `left == right` failed: expected exactly the invariant-21 S->G violation and nothing else, got [] + left: 0 + right: 1 + +#### Structural gate — Gate 12 under M6a (S->G dispatch call deleted) + +``` +$ grep -c "fn check_staff_names_absent_group" crates/epiphany-core/src/invariants.rs # a +1 +$ grep -c "fn check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs # b +1 +$ grep -c "idx.check_staff_names_absent_group(&mut v)" crates/epiphany-core/src/invariants.rs # c +0 +$ grep -c "idx.check_group_lists_unowned_staff(&mut v)" crates/epiphany-core/src/invariants.rs # d +1 + => GATE 12 FAILS (a/b/c/d = 1/1/0/1) +``` + +### Required survivors, each by name (2) + + PASS m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok + PASS u5_undoing_a_staff_strips_it_from_the_live_groups_members + test reduce::tests::u5_undoing_a_staff_strips_it_from_the_live_groups_members ... ok + +============================================================================== +## M6b — delete the G->S dispatch call +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff + +### Verbatim failing output + +---- invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff stdout ---- +thread 'invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff' (3710920) panicked at crates/epiphany-core/src/invariants.rs:6361:9: +assertion `left == right` failed: expected exactly the invariant-21 G->S violation and nothing else, got [] + left: 0 + right: 1 + +#### Structural gate — Gate 12 under M6b (G->S dispatch call deleted) + +``` +$ grep -c "fn check_staff_names_absent_group" crates/epiphany-core/src/invariants.rs # a +1 +$ grep -c "fn check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs # b +1 +$ grep -c "idx.check_staff_names_absent_group(&mut v)" crates/epiphany-core/src/invariants.rs # c +1 +$ grep -c "idx.check_group_lists_unowned_staff(&mut v)" crates/epiphany-core/src/invariants.rs # d +0 + => GATE 12 FAILS (a/b/c/d = 1/1/1/0) +``` + +### Required survivors, each by name (7) + + PASS m41_check_invariants_dispatches_invariant_21_staff_names_absent_group + test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok + PASS invariant_21_negative_generator_breaks_staff_to_group_only + test generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only ... ok + PASS every_invariant_has_a_negative_generator + test generators::tests::every_invariant_has_a_negative_generator ... ok + PASS every_invariant_shrinks_to_a_small_witness + test generators::tests::every_invariant_shrinks_to_a_small_witness ... ok + PASS shrink_is_idempotent + test generators::tests::shrink_is_idempotent ... ok + PASS negative_generators_are_reasonably_targeted + test generators::tests::negative_generators_are_reasonably_targeted ... ok + PASS full_invariant_sweep_via_public_api + test full_invariant_sweep_via_public_api ... ok + +============================================================================== +## M7a — revert Staff.group's doc block to B +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + graph::g3a_tests::t14_staff_group_field_doc_comment_states_sole_authority + +### Verbatim failing output + +---- graph::g3a_tests::t14_staff_group_field_doc_comment_states_sole_authority stdout ---- +thread 'graph::g3a_tests::t14_staff_group_field_doc_comment_states_sole_authority' (3379269) panicked at crates/epiphany-core/src/graph.rs:2191:9: +Staff.group's doc comment must state the projection is maintained from it (P13-S16 disposition A); block was: + /// M7a ACTIVE — RESTORE THE DISPOSITION-A WORDING + /// Which staff group (if any) this staff belongs to. **The sole authority + /// for group membership** (genesis tranche G3a, + /// `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, disposition B, filed as + /// P13-S16): every consumer MUST read membership from this field, not + /// from [`StaffGroup::members`], which is a non-authoritative denormalized + /// projection that may disagree with this field in either direction. + +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (1) + + PASS t14_staff_group_members_field_doc_comment_states_non_authoritative_projection + test graph::g3a_tests::t14_staff_group_members_field_doc_comment_states_non_authoritative_projection ... ok + +============================================================================== +## M7b — revert StaffGroup.members's doc block to B +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + graph::g3a_tests::t14_staff_group_members_field_doc_comment_states_non_authoritative_projection + +### Verbatim failing output + +---- graph::g3a_tests::t14_staff_group_members_field_doc_comment_states_non_authoritative_projection stdout ---- +thread 'graph::g3a_tests::t14_staff_group_members_field_doc_comment_states_non_authoritative_projection' (3418176) panicked at crates/epiphany-core/src/graph.rs:2220:9: +StaffGroup.members's doc comment must state it is maintained from Staff.group; block was: + /// M7b ACTIVE — RESTORE THE DISPOSITION-A WORDING + /// A **non-authoritative denormalized projection** of group membership + /// (genesis tranche G3a, `spec/CONTRACT_GENESIS_G3A_ENTITIES.md` §1.1, + /// disposition B, filed as P13-S16). [`Staff::group`] is the sole + /// authority: this field MUST NOT be read to decide whether a staff is in + /// a group, and MAY be stale in **both** directions — a member missing + /// here while `Staff.group` names this group, or a staff listed here + /// while its own `Staff.group` is `None` or names a different group. + +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (1) + + PASS t14_staff_group_field_doc_comment_states_sole_authority + test graph::g3a_tests::t14_staff_group_field_doc_comment_states_sole_authority ... ok + +============================================================================== +## M8 — reinstate the dead liveness loop +============================================================================== + +Aggregate: passed 1583 failed 0 + +### Complete observed failure set (0) + + (empty — no test failed) +#### Structural gate — Gate 8 under M8 (dead liveness loop reinstated) + +``` +$ read the brace-matched create_staff_group slice (4551..4612), production source + empty-members refusal present : True + TypedObjectId::Staff( present : True + TargetMissing present : True + => GATE 8 FAILS +``` + +### Required survivors, each by name (0) + + §3 names no individual survivors: "every behavioural assertion". + Discharged by the aggregate above — passed 1583, failed 0. + +============================================================================== +## M9 — graph-gate pin 1's refusal +============================================================================== + +Aggregate: passed 1582 failed 1 + +### Complete observed failure set (1) + + reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free + +### Verbatim failing output + +---- reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free stdout ---- +thread 'reduce::tests::t7_g3a_referential_preconditions_are_not_enforced_base_free' (3459823) panicked at crates/epiphany-ops/src/reduce.rs:16361:9: +assertion `left == right` failed: an empty-container precondition asks only about the carried value, so it refuses base-free too (P13-S16 pin 1a); a graph gate here would wrongly accept + left: Some(Applied) + right: Some(NoOp { reason: PreconditionFailedUnderReduction { reason: ContainerNotEmpty } }) +note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace + +### Required survivors, each by name (1) + + PASS t8b_the_projection_is_maintained_and_the_spurious_form_is_refused + test reduce::tests::t8b_the_projection_is_maintained_and_the_spurious_form_is_refused ... ok + +--- + +# P13-S16 — EVIDENCE ANNEX, PART 2: GATES AND SOURCE QUOTATIONS + +Commands with their outputs, and source slices read from the staged tree. + + +## Gate 1 +``` +$ cargo test --workspace --no-fail-fast +suites 42 passed 1583 failed 0 ignored 0 +exit 0 +``` + +## Gate 2 +``` +$ cargo +1.95.0 clippy --workspace --all-targets -- -D warnings +(no error or warning lines) +``` + +## Gate 3 +``` +$ cargo +1.95.0 fmt -p epiphany-ops -p epiphany-core -p epiphany-textproj -p epiphany-testkit --check +(no output) +``` + +## Gate 4 +``` +$ git diff --cached --check +(no output; exit 0) + +$ git diff --cached --name-only +crates/epiphany-core/src/generators.rs +crates/epiphany-core/src/graph.rs +crates/epiphany-core/src/invariants.rs +crates/epiphany-ops/src/lib.rs +crates/epiphany-ops/src/payload.rs +crates/epiphany-ops/src/reduce.rs +crates/epiphany-ops/src/valuegen.rs +crates/epiphany-testkit/src/roundtrip.rs +crates/epiphany-textproj/src/serialize.rs +spec/PASS13_CANDIDATES.md +spec/core_spec.pdf +spec/core_spec.tex +spec/operation_catalog.pdf +spec/operation_catalog.tex +``` + +Row 11 (`requirement_labels.rs`) is the only §2 row not staged: unused per pin 10a. + +## Gate 5 +``` +$ git diff --stat HEAD -- spec/vectors/decode_vectors.txt +(no output) +``` + +## Gate 6 — invariant 21 reached through `check_invariants` + +``` +$ cargo test -p epiphany-core --lib m41 +test invariants::s16_agreement_dispatch_tests::m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff ... ok +test invariants::s16_agreement_dispatch_tests::m41_check_invariants_dispatches_invariant_21_staff_names_absent_group ... ok +test result: ok. 2 passed; 0 failed; 0 ignored; 0 measured; 322 filtered out; finished in 0.00s + +$ cargo test -p epiphany-core --lib invariant_21_negative +test generators::tests::invariant_21_negative_generator_breaks_staff_to_group_only ... ok +test result: ok. 1 passed; 0 failed; 0 ignored; 0 measured; 323 filtered out; finished in 0.00s +``` + +The exact-set and direction assertions these three carry are quoted under items +2d/2e below; a passing exact-set assertion is the observation, and no runtime +witness dump is claimed. + +### Checked *in addition*, never instead +``` +$ grep -n 'assert_eq!(GraphInvariant::all().len(), 21);' crates/epiphany-core/src/invariants.rs +6163: assert_eq!(GraphInvariant::all().len(), 21); + +$ grep -n 'pub fn all() -> \[GraphInvariant; 21\]' crates/epiphany-core/src/invariants.rs +169: pub fn all() -> [GraphInvariant; 21] { + +$ grep -n 'This enumeration contains exactly' spec/core_spec.tex +6673:This enumeration contains exactly \textbf{21} invariants. (Earlier + +$ count \item entries inside the req:graph:score-graph-invariants requirement box +21 +``` + +Invariant 21 is a 21st `\item` inside the pre-existing box; no new label is minted. + +## Gate 7 — every test named in pin 8, final candidate + +``` +$ cargo test -p epiphany-ops --lib u2a_a_live_staff_naming_the_group_blocks_its_undo +test reduce::tests::u2a_a_live_staff_naming_the_group_blocks_its_undo ... ok + +$ cargo test -p epiphany-ops --lib u2bf_a_the_staff_group_guard_holds_base_free +test reduce::tests::u2bf_a_the_staff_group_guard_holds_base_free ... ok + +$ cargo test -p epiphany-ops --lib u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo +test reduce::tests::u2tomb_a_a_tombstoned_referencing_staff_does_not_block_the_groups_undo ... ok + +$ cargo test -p epiphany-ops --lib u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole +test reduce::tests::u3a_minting_the_group_and_its_referencing_staff_in_one_transaction_undoes_whole ... ok + +``` + +None changed; each was expected to survive, and each was run rather than assumed. + +## Gate 8 — brace-matched `create_staff_group`, production source +```rust +4551: fn create_staff_group( +4552: &mut self, +4553: env: &OperationEnvelope, +4554: op: &CreateStaffGroupOp, +4555: ) -> OperationEffect { +4556: let gobj = TypedObjectId::StaffGroup(op.staff_group_id()); +4557: match self.objects.get(&gobj) { +4558: Some(ObjectState::Live) => { +4559: let identical = self +4560: .staff_group_values +4561: .get(&op.staff_group_id()) +4562: .is_some_and(|known| known == &op.group); +4563: return if identical { +4564: OperationEffect::NoOp { +4565: reason: NoOpReason::AlreadyApplied, +4566: } +4567: } else { +4568: OperationEffect::NoOp { +4569: reason: NoOpReason::PreconditionFailedUnderReduction { +4570: reason: PreconditionFailureReason::RecreateContentMismatch, +4571: }, +4572: } +4573: }; +4574: } +4575: Some(ObjectState::Tombstoned { .. }) => { +4576: return OperationEffect::NoOp { +4577: reason: NoOpReason::TargetTombstoned, +4578: } +4579: } +4580: None => {} +4581: } +4582: // Reject a carried non-empty `members`: the mint authors the group, and +4583: // membership is maintained from `Staff.group` (P13-S16 pin 2). Unlike the +4584: // sibling mints' referential preconditions this is NOT graph-gated — an +4585: // empty-container precondition asks only about the carried value, so it +4586: // holds base-free as well (pin 1; `t7` asserts the inversion). +4587: if !op.group.members.is_empty() { +4588: return container_not_empty(); +4589: } +4590: if let Some(score) = self.graph.as_mut() { +4591: score.staff_groups.push(op.group.clone()); +4592: } +4593: self.mint_container(env, gobj); +4594: self.staff_group_values +4595: .insert(op.staff_group_id(), op.group.clone()); +4596: OperationEffect::Applied +4597: } +``` + +## Gate 9 — `t8c` and `t8d`, by name, final candidate + +``` +$ cargo test -p epiphany-ops --lib t8c_recarry_compares_against_the_carried_members_not_the_derived +test reduce::tests::t8c_recarry_compares_against_the_carried_members_not_the_derived ... ok + +$ cargo test -p epiphany-ops --lib t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent +test reduce::tests::t8d_recarry_after_reduction_onto_a_materialized_base_stays_idempotent ... ok + +``` + +## Gate 10 +``` +$ grep -n "pub const CURRENT_REDUCTION_ALGORITHM_VERSION" crates/epiphany-ops/src/lib.rs +181:pub const CURRENT_REDUCTION_ALGORITHM_VERSION: u32 = 1; + +$ git show HEAD:crates/epiphany-ops/src/lib.rs | grep -n "pub const CURRENT_REDUCTION_ALGORITHM_VERSION" +152:pub const CURRENT_REDUCTION_ALGORITHM_VERSION: u32 = 0; +``` + +### `Bumps` list verbatim +```rust +137: /// +138: /// This is a fact about the *baseline*, not about the current value: read the +139: /// declaration below for that, and the `Bumps` list for how the series got +140: /// there. +141: /// +142: /// # Bumps +143: /// +144: /// * `0` — the baseline. The semantics `canonical_reduction_order` and +145: /// `reduce_onto` implement as of P13-S27 (2026-08-08). No earlier version +146: /// exists; nothing predates this constant. +147: /// * `1` — **P13-S16** (2026-08-09, `spec/CONTRACT_P13S16_PROJECTION.md`), the +148: /// first real bump. It carries **one change of each kind**, and the two are +149: /// not interchangeable: +150: /// - a **reduction verdict** change — `CreateStaffGroup` carrying a non-empty +151: /// `members` now reduces to a `ContainerNotEmpty` no-op where version `0` +152: /// applied it. The effect recorded for that operation differs. +153: /// - a **canonical reduced state** change — `CreateStaff` carrying +154: /// `group: Some(g)` now appends the staff to `g`'s `members`. Its verdict is +155: /// unchanged (it still applies); the graph the reduction produces is what +156: /// differs. +157: /// +158: /// Either alone would require this bump. A base materialized under `0` holds +159: /// state this version would not have computed, so it must be rebuilt rather +160: /// than reused. +161: /// +162: /// A bump without its entry above leaves a number nobody can account for: this +163: /// list is the only record of *why* each version exists. +164: /// +165: /// **No mechanism detects a missed bump.** The authority check compares +166: /// *declared* versions, so it catches a base stamped with a version other than +167: /// this one — it cannot notice that the semantics changed while the constant +168: /// stood still. Every future change to a canonical reduction verdict **or to +169: /// canonical reduced state** must move this constant and add its entry here. +170: /// Both classes are named because a change that leaves every verdict intact +171: /// while altering the reduced graph is the easier one to overlook, and it +172: /// invalidates a base just as completely. That discipline is the whole +173: /// guarantee. +174: /// +175: /// # Layering +176: /// +177: /// This is a plain `u32`, and `epiphany-ops` **MUST NOT** gain a dependency on +178: /// `epiphany-bundle` in order to use that crate's `ReductionAlgorithmVersion` +179: /// wrapper. The wrapper is constructed at the composition boundary by whoever +180: /// depends on both (P13-S27 pin 1, §0.3). +181: pub const CURRENT_REDUCTION_ALGORITHM_VERSION: u32 = 1; +``` + +## Gate 11 — tripwires, BEFORE (HEAD) vs AFTER (staged), verbatim + + +### 11a serialize.rs assertion +``` +BEFORE (HEAD): +665: ReductionAlgorithmVersion(0), + +AFTER (staged): +667: ReductionAlgorithmVersion(1), +``` + +### 11b fixture capability and staged base +``` +BEFORE (HEAD): +400: reduction_algorithm_version: ReductionAlgorithmVersion(0), <-- NOT a gate-11 site: + an `acceleration_snapshots` entry, UNCHANGED in the staged tree and unrelated + to test 10b's canonical base. The authority check governs canonical bases only, + so this literal is unaffected by the bump. Listed here because the grep matched + it, and labelled rather than silently dropped. +872: /// The fixture is built with `synthetic_for_fixture(0)` and commits a base +901: BundleCapabilities::synthetic_for_fixture(0), +918: reduction_algorithm_version: ReductionAlgorithmVersion(0), + +AFTER (staged): +872: /// The fixture is built with `synthetic_for_fixture(1)` and commits a base +909: BundleCapabilities::synthetic_for_fixture(1), +926: reduction_algorithm_version: ReductionAlgorithmVersion(1), +``` + +### 11c success-arm assertion +``` +BEFORE (HEAD): +941: ReductionAlgorithmVersion(0) + +AFTER (staged): +949: ReductionAlgorithmVersion(1) +``` + +### 11d mutation-only Err arm +``` +BEFORE (HEAD): +947: assert_eq!(base, ReductionAlgorithmVersion(0)); + +AFTER (staged): +955: assert_eq!(base, ReductionAlgorithmVersion(1)); +``` + +### 11e literal-preservation doc comments (staged) +```rust +866: /// P13-S27 test 10b — the test M5b breaks, and **the only place in the rung +867: /// where the real authority meets a canonical base**. In `epiphany-testkit`, +868: /// which may reach the real constant. +869: /// +870: /// # Two provably independent operands +871: /// +872: /// The fixture is built with `synthetic_for_fixture(1)` and commits a base +873: /// carrying the **literal** `ReductionAlgorithmVersion(1)`; the reopen then +874: /// supplies `production_caps()`, which wraps the real constant. One operand +875: /// is a literal written into a fixture, the other is the authority read at +876: /// the reopen — neither derived from the other. +877: /// +878: /// **The literals track the constant's value by hand.** P13-S16 moved the +879: /// authority `0` → `1`, so every literal below moved with it — by editing, +880: /// never by referencing `CURRENT_REDUCTION_ALGORITHM_VERSION`. That this +881: /// test must be edited whenever the authority moves is the **point**, not +882: /// friction to be engineered away: it is the tripwire. A future rung that +883: /// bumps the constant will see this test fail, and updating these literals +884: /// is how it acknowledges the bump. +885: /// +886: /// **Round 3 caught the alternative**: if both the supplied capability and +887: /// the base version descended from `CURRENT_REDUCTION_ALGORITHM_VERSION`, +888: /// both would move together under M5b's mutation and the comparison would +889: /// pass for every value — §0.1's own tautology, reproduced inside the +890: /// mutation built to detect it. **Do not tidy either literal into the +891: /// constant** (§7 item 4b). +892: /// +893: /// # Both `Result` arms are written deliberately +894: /// +895: /// Round 5 pinned this: "assert it opens" was not enough, because under M5b +896: /// the reopen returns `Err` and **a `#[test]` returning `Err` asserts +897: /// nothing about that error's fields**. The `Err` arm below runs only under +898: /// mutation, and it is what makes M5b's required two-field observation a +899: /// *verified* one rather than a stack trace. The third arm exists so a +900: /// *different* error under mutation is reported rather than read as success. +901: #[test] +902: fn a_base_bearing_bundle_reopened_under_the_real_authority_validates() { +903: use epiphany_bundle::{BundleCapabilities, BundleError}; +904: +905: let mut bundle = Bundle::create( +906: MemStore::new(), +907: FileUuid([0x5E; 16]), +908: Manifest::empty(DocumentId([0x5E; 16])), +909: BundleCapabilities::synthetic_for_fixture(1), +910: ) +911: .expect("fixture bundle creates"); +912: +913: let staged = StagedChunk { +914: kind: ChunkKind::Snapshot, +915: schema_version: SchemaVersion::V0, +916: payload: vec![5u8, 5, 5], +917: }; +918: bundle +919: .commit(&[staged], |ctx| { +920: let mut m = ctx.previous_manifest.clone(); +921: let root = ctx.new_chunks[0]; +922: m.canonical_base = Some(SnapshotRef { +923: snapshot_id: SnapshotId([0x5E; 16]), +924: covers_causal_frontier: FrontierBytes::empty(), +925: // A deliberate LITERAL — not the constant. See above. +926: reduction_algorithm_version: ReductionAlgorithmVersion(1), +927: profile_id: ProfileId::Full, +928: hash: root.hash, +929: root, +930: }); +931: m +932: }) +933: .expect("committing the base under the matching synthetic capability succeeds"); +934: let image = bundle.into_store().into_bytes(); +935: +936: match Bundle::open(MemStore::from_bytes(image), crate::production_caps()) { +937: Ok(reopened) => { +938: assert!( +939: reopened.manifest().canonical_base.is_some(), +940: "the base must survive the reopen, or this asserts nothing" +941: ); +942: assert_eq!( +943: reopened +944: .manifest() +945: .canonical_base +946: .as_ref() +947: .unwrap() +948: .reduction_algorithm_version, +949: ReductionAlgorithmVersion(1) +950: ); +951: } +952: Err(BundleError::CanonicalBaseRequiresRebuild { base, current }) => { +953: // Reached only under M5b. Assert both fields, then fail loudly +954: // quoting them — that is the mutation's required observation. +955: assert_eq!(base, ReductionAlgorithmVersion(1)); +956: panic!( +957: "M5b observation: base={} current={} — the authority is load-bearing here", +958: base.0, current.0 +959: ); +960: } +961: Err(other) => panic!("unexpected error, not the authority verdict: {other:?}"), +962: } +963: } +``` +```rust +642: /// P13-S27 test 10a — the test M5a breaks. **In `epiphany-textproj`**, +643: /// because `epiphany-bundle` must not depend on `epiphany-ops` (pin 1, §0.3) +644: /// and so no test there can reach the real authority. +645: /// +646: /// # The `1` is a deliberate LITERAL, and that is load-bearing +647: /// +648: /// Comparing against `CURRENT_REDUCTION_ALGORITHM_VERSION` would compare the +649: /// constant with itself laundered through one function call: mutate the +650: /// constant and **both sides move**, so the assertion would hold for every +651: /// value and M5a could not break it. **Do not "tidy" this into the +652: /// constant** — doing so makes M5a vacuous while leaving every test green, +653: /// a failure invisible to the suite (contract §7 item 4b exists to catch it). +654: /// +655: /// **This test failed when P13-S16 bumped the authority `0` → `1`, exactly as +656: /// S27 predicted it would**, and the literal below was updated by hand. That +657: /// is the tripwire working, not friction: editing this literal is how a rung +658: /// *states* that the authority moved. A future bump must break this test +659: /// again. +660: #[test] +661: fn serialize_document_supplies_the_real_reduction_authority() { +662: let document = minimal_document(42); +663: let bundle = serialize_document(&document, MemStore::new(), FileUuid([1; 16])) +664: .expect("a base-free document serializes"); +665: assert_eq!( +666: bundle.capabilities().current_reduction_version, +667: ReductionAlgorithmVersion(1), +668: "the production writer must supply the real authority, not a literal of its own" +669: ); +670: } +``` + +## Gate 12 — dispatcher and both definitions + + +> **Method note.** M6a/M6b are applied by **deleting** the dispatch line, as M6 +> specifies, and **both the full-suite run and the structural gate above were taken +> under that deletion.** An earlier pass commented the line out instead. The +> compiled behaviour is identical, so the failure sets are unchanged (seven and +> one) — but the contract's unanchored needle still matches a commented-out call, +> so gate 12 read `1/1/1/1` and appeared to pass under M6a. **The mutation must +> remove the line, not disable it** — a commented-out call is invisible to the +> compiler and visible to grep, which is exactly backwards for this gate. The +> earlier comment-out runs were discarded rather than reused. + +### `check_invariants` signature and the invariant-21 call sites + +```rust +278: pub fn check_invariants(score: &Score) -> Vec { +304: // Invariant 21's two directions, dispatched separately (P13-S16 pin 6b). +305: // Each call site is independently deletable, which is what M6a and M6b +306: // delete; a single call handling both would leave the mutation with no way +307: // to fail one direction while the other still reports. +308: idx.check_staff_names_absent_group(&mut v); +309: idx.check_group_lists_unowned_staff(&mut v); +``` + +### Enclosing implementation header for both methods + +```rust +385: impl<'a> GraphIndex<'a> { +``` + +### The four counts, final candidate + +``` +$ grep -c "fn check_staff_names_absent_group" crates/epiphany-core/src/invariants.rs # a +1 +$ grep -c "fn check_group_lists_unowned_staff" crates/epiphany-core/src/invariants.rs # b +1 +$ grep -c "idx.check_staff_names_absent_group(&mut v)" crates/epiphany-core/src/invariants.rs # c +1 +$ grep -c "idx.check_group_lists_unowned_staff(&mut v)" crates/epiphany-core/src/invariants.rs # d +1 + => GATE 12 PASSES (a/b/c/d = 1/1/1/1) +``` + +### S->G definition +```rust +2795: /// Direction **S→G**: every live staff naming a group appears in that +2796: /// group's `members`. A maintenance gap — pin 2 failing to append — shows up +2797: /// here. +2798: /// +2799: /// A staff naming a group that does not exist is **not** flagged here: +2800: /// dangling reference resolution belongs to the referential invariants, and +2801: /// abstaining keeps this invariant's witnesses about *agreement* only. +2802: fn check_staff_names_absent_group(&self, out: &mut Vec) { +2803: let members: HashMap> = self +2804: .score +2805: .staff_groups +2806: .iter() +2807: .map(|group| (group.id, group.members.iter().copied().collect())) +2808: .collect(); +2809: for staff in &self.score.staves { +2810: let Some(group_id) = staff.group else { +2811: continue; +2812: }; +2813: if let Some(ids) = members.get(&group_id) { +2814: if !ids.contains(&staff.id) { +2815: out.push(InvariantViolation::new( +2816: GraphInvariant::StaffGroupMembershipAgreement, +2817: format!( +2818: "S->G: staff {:?} names group {:?}, but that group's members omit it", +2819: staff.id, group_id +2820: ), +2821: )); +2822: } +2823: } +2824: } +2825: } +``` + +### G->S definition +```rust +2827: /// Direction **G→S**: every staff a group lists names that group in its own +2828: /// `group` field. A stale projection — a member left behind, or one pointing +2829: /// at a different group — shows up here. +2830: /// +2831: /// A member id with no live staff is **not** flagged here, for the same +2832: /// reason as the S→G direction. +2833: fn check_group_lists_unowned_staff(&self, out: &mut Vec) { +2834: let owner: HashMap> = self +2835: .score +2836: .staves +2837: .iter() +2838: .map(|staff| (staff.id, staff.group)) +2839: .collect(); +2840: for group in &self.score.staff_groups { +2841: for member in &group.members { +2842: let Some(named) = owner.get(member) else { +2843: continue; +2844: }; +2845: if *named != Some(group.id) { +2846: out.push(InvariantViolation::new( +2847: GraphInvariant::StaffGroupMembershipAgreement, +2848: format!( +2849: "G->S: group {:?} lists staff {:?}, but that staff names {:?}", +2850: group.id, member, named +2851: ), +2852: )); +2853: } +2854: } +2855: } +2856: } +``` + +## Gate 13 / item 2f — `u5` +```rust +18157: /// (u5) **P13-S16 pin 5a.** Undoing a `CreateStaff` strips the staff's id +18158: /// from every live group's `members`. +18159: /// +18160: /// **This is the unguarded direction of projection maintenance** — *not* of +18161: /// invariant 21; see assertion 4 for why the distinction is load-bearing. The +18162: /// reverse direction is blocked: `undo_strand_block`'s +18163: /// `TypedObjectId::StaffGroup` arm refuses to undo a group a live staff still +18164: /// names (see `u2a`). Nothing blocks undoing the *staff*, so before pin 5 the +18165: /// undo removed it from `Score.staves` and left its id sitting in +18166: /// `g.members`: a group naming a staff that no longer exists. +18167: /// +18168: /// **Nothing permanent exercised this sequence before, checked rather than +18169: /// assumed.** Pin 8's four are group-undo guards; `u2tomb_a` undoes a staff +18170: /// but undoes the group along with it — it asserts *"the group leaves +18171: /// `Score.staff_groups`"* — so no *live* group's `members` is ever inspected. +18172: /// `m41`/`m41b` build materialized fixtures and never run the reducer's undo +18173: /// path at all. A mutation demonstrates the hazard once; only a test keeps it +18174: /// demonstrated. +18175: /// +18176: /// **Mutation (M5):** remove pin 5's strip from the `Staff` arm of +18177: /// `materialize_graph_tombstones`; assertion 2 fails with `s` still in +18178: /// `members`. +18179: /// +18180: /// **Observation harness (same rule as pin 7a).** Both the post-undo +18181: /// `members` and the invariant-21 violations are bound **before assertion +18182: /// 2**, and both appear in every assertion's message. Under M5 it is +18183: /// assertion 2 that fires, so assertion 3 never executes — computing the +18184: /// violations only where assertion 3 needs them would put M5's required +18185: /// witness behind an assertion M5 guarantees is unreachable. **The state a +18186: /// mutation owes must be bound before the assertion that mutation trips.** +18187: #[test] +18188: fn u5_undoing_a_staff_strips_it_from_the_live_groups_members() { +18189: let identity = IdentityContext::new(ReplicaId(1)); +18190: let instrument_id = InstrumentId::new(ReplicaId(9), 1); +18191: let mut base = Score::empty(identity); +18192: base.instruments +18193: .push(crate::valuegen::instrument(instrument_id)); +18194: +18195: let group_id = StaffGroupId::new(ReplicaId(1), 1); +18196: let staff_id = StaffId::new(ReplicaId(1), 5); +18197: let tx = TransactionId::new(ReplicaId(1), 900); +18198: +18199: let mut staff_value = crate::valuegen::staff(staff_id, instrument_id); +18200: staff_value.group = Some(group_id); +18201: +18202: let mut set = OperationSet::new(); +18203: set.accept_all(vec![ +18204: // The group is authored OUTSIDE the transaction, so undoing the +18205: // transaction takes the staff and leaves the group live — which is +18206: // what gives assertion 1 something to hold. +18207: staff_group_env( +18208: 1, +18209: 0, +18210: 10, +18211: CausalContext::new(), +18212: crate::valuegen::staff_group(group_id, vec![]), +18213: ), +18214: declare_transaction(1, 1, 20, seen_r1(0), tx), +18215: tx_member( +18216: 1, +18217: 2, +18218: 21, +18219: seen_r1(1), +18220: tx, +18221: OperationKind::CreateStaff(CreateStaffOp { staff: staff_value }), +18222: ), +18223: undo_env(1, 3, 30, seen_r1(2), tx, UndoPolicy::StrictInverse), +18224: ]); +18225: let out = reduce_operation_set_onto(&set, &base); +18226: +18227: // Bound BEFORE assertion 2 — see the harness note above. +18228: let members: Option> = out +18229: .score +18230: .staff_groups +18231: .iter() +18232: .find(|g| g.id == group_id) +18233: .map(|g| g.members.clone()); +18234: let agreement = epiphany_core::check_invariant( +18235: &out.score, +18236: epiphany_core::GraphInvariant::StaffGroupMembershipAgreement, +18237: ); +18238: let staff_present = out.score.staves.iter().any(|s| s.id == staff_id); +18239: let all_violations = epiphany_core::check_invariants(&out.score); +18240: let harness = format!( +18241: "\n post-undo g.members: {members:?}\ +18242: \n invariant-21 violations: {agreement:?}\ +18243: \n staff {staff_id:?} still in graph: {staff_present}\ +18244: \n ALL violations: {all_violations:?}" +18245: ); +18246: +18247: // 1. The group must still be live, or there is no projection left to be +18248: // wrong and this test asserts nothing. +18249: assert!( +18250: out.score.staff_groups.iter().any(|g| g.id == group_id), +18251: "the group must survive the staff's undo for this test to mean \ +18252: anything{harness}" +18253: ); +18254: // 1b. Not in pin 5a's list, added so a BLOCKED undo cannot be mistaken +18255: // for a failed strip: both leave `s` in `members`, and only this +18256: // tells them apart. +18257: assert!( +18258: !staff_present, +18259: "precondition: the staff's undo must actually have removed it from \ +18260: the graph — if it was blocked instead, assertion 2 below would fail \ +18261: for an unrelated reason{harness}" +18262: ); +18263: // 2. The strip itself. +18264: assert!( +18265: !members.as_deref().unwrap_or_default().contains(&staff_id), +18266: "P13-S16 pin 5: undoing the staff must strip {staff_id:?} from the \ +18267: live group's members{harness}" +18268: ); +18269: // 3. Pin 5a's third assertion: no invariant-21 residue in either +18270: // direction. +18271: assert!( +18272: agreement.is_empty(), +18273: "the post-undo graph must leave invariant 21 clean in both \ +18274: directions{harness}" +18275: ); +18276: // 4. Added during execution, because assertion 3 CANNOT see the residue +18277: // this test exists to catch — observed, not reasoned. Under M5 the +18278: // strip is gone and `members` keeps an id whose staff has left the +18279: // graph: that is a **dangling** reference, and invariant 21 +18280: // deliberately abstains on those (agreement is a claim about live +18281: // pairs; dangling resolution belongs to the referential invariants). +18282: // M5 was run and invariant 21 reported `[]`, while invariant 10 +18283: // `CrossCuttingRefsResolve` reported "staff group ... member staff +18284: // ... is not declared". Pin 5a expects assertion 3 to fail "on a +18285: // residue whichever direction it leaves"; on its own it does not, so +18286: // the whole set is asserted here. +18287: assert!( +18288: all_violations.is_empty(), +18289: "the post-undo graph must be invariant-clean overall — a stripped \ +18290: member must not be left dangling either{harness}" +18291: ); +18292: } +``` + +Assertions 1, 2, 3 are pin 5a's; 1b and 4 were added during execution and are so +labelled in source. All five carry `{harness}`. Verdict: ok. + +## Gate 14 / pin 7a — `t8b` +```rust +16440: /// (t8b) **P13-S16 pin 7 inverted this test.** The projection is +16441: /// **maintained** in the missing order, and the spurious form is +16442: /// **refused** — the same two authoring orders as before (§0.5), with the +16443: /// verdicts the ratified disposition A requires. +16444: /// +16445: /// **It previously pinned the exact opposite**, as +16446: /// `t8b_both_permitted_stale_forms_hold`: under disposition B both stale +16447: /// forms were *permitted states*, so the missing form left `g.members == []` +16448: /// and the spurious form let `g.members == [s]` reach the graph alongside +16449: /// `s.group == None`. **That is not a regression being fixed here** — it was +16450: /// the correct assertion under the ruling in force at the time. P13-S16 +16451: /// ratified disposition A, under which `Staff.group` is the sole authority +16452: /// and `StaffGroup.members` is maintained from it (pins 1 and 2), so neither +16453: /// disagreeing state is reachable any more and the assertions invert with the +16454: /// ruling. +16455: /// +16456: /// **Deleting this test is forbidden** — the *pairing* of the two orders is +16457: /// the coverage, because each order signs a different production change. +16458: /// +16459: /// **Mutation 1 (M1; spurious order, where `create_staff_group` runs +16460: /// SECOND):** remove pin 1's refusal; the group mints carrying `[s]` while +16461: /// `s.group` is `None`. +16462: /// +16463: /// **Mutation 2 (M2; missing order, where `create_staff` runs SECOND):** +16464: /// remove pin 2's append; `g.members` stays empty and invariant 21 fires. +16465: /// +16466: /// An earlier draft assigned these the other way round, which is impossible +16467: /// in both directions: `create_staff_group` runs first in the missing order +16468: /// and cannot append a staff that does not exist yet, and `create_staff` +16469: /// runs first in the spurious order and has no later group to repair. +16470: /// +16471: /// **Observation harness (pin 7a).** The two orders are two reductions over +16472: /// two *different* groups, so there are **four** observations, not three — +16473: /// and a `#[test]` emits nothing but its assertion diagnostics, so state not +16474: /// in those diagnostics is unobtainable. All four are bound **before any +16475: /// assertion** and formatted into **every** assertion's message: a failing +16476: /// test stops at its *first* failed assertion, and M1 and M2 trip +16477: /// *different* assertions, so each one must carry the whole set. Splitting +16478: /// the set per order would reintroduce the same gap one level down. +16479: #[test] +16480: fn t8b_the_projection_is_maintained_and_the_spurious_form_is_refused() { +16481: let instrument_id = InstrumentId::new(ReplicaId(1), 1); +16482: +16483: // Missing form: CreateStaffGroup(g, []) -> CreateStaff(s, Some(g)). +16484: let group_id = StaffGroupId::new(ReplicaId(1), 3); +16485: let staff_id = StaffId::new(ReplicaId(1), 5); +16486: let create_instrument = prim_env( +16487: 1, +16488: 0, +16489: 10, +16490: CausalContext::new(), +16491: OperationKind::CreateInstrument(CreateInstrumentOp { +16492: instrument: crate::valuegen::instrument(instrument_id), +16493: }), +16494: ); +16495: let create_group = staff_group_env( +16496: 1, +16497: 2, +16498: 20, +16499: CausalContext::new(), +16500: crate::valuegen::staff_group(group_id, vec![]), +16501: ); +16502: let mut staff = crate::valuegen::staff(staff_id, instrument_id); +16503: staff.group = Some(group_id); +16504: let create_staff = prim_env( +16505: 1, +16506: 4, +16507: 30, +16508: CausalContext::new(), +16509: OperationKind::CreateStaff(CreateStaffOp { staff }), +16510: ); +16511: let mut set = OperationSet::new(); +16512: set.accept_all(vec![create_instrument, create_group, create_staff]); +16513: let out = +16514: reduce_operation_set_onto(&set, &Score::empty(IdentityContext::new(ReplicaId(1)))); +16515: +16516: // Spurious form: CreateStaff(s, None) -> CreateStaffGroup(g, [s]). +16517: let group_id2 = StaffGroupId::new(ReplicaId(2), 3); +16518: let staff_id2 = StaffId::new(ReplicaId(2), 5); +16519: let create_instrument2 = prim_env( +16520: 2, +16521: 0, +16522: 10, +16523: CausalContext::new(), +16524: OperationKind::CreateInstrument(CreateInstrumentOp { +16525: instrument: crate::valuegen::instrument(instrument_id), +16526: }), +16527: ); +16528: let staff2 = crate::valuegen::staff(staff_id2, instrument_id); +16529: let create_staff2 = prim_env( +16530: 2, +16531: 2, +16532: 20, +16533: CausalContext::new(), +16534: OperationKind::CreateStaff(CreateStaffOp { staff: staff2 }), +16535: ); +16536: let create_group2 = staff_group_env( +16537: 2, +16538: 4, +16539: 30, +16540: CausalContext::new(), +16541: crate::valuegen::staff_group(group_id2, vec![staff_id2]), +16542: ); +16543: let spurious_group_env_id = create_group2.id; +16544: let mut set2 = OperationSet::new(); +16545: set2.accept_all(vec![create_instrument2, create_staff2, create_group2]); +16546: let out2 = +16547: reduce_operation_set_onto(&set2, &Score::empty(IdentityContext::new(ReplicaId(2)))); +16548: +16549: // --------------------------------------------------------------------- +16550: // Pin 7a's four bindings. ALL taken BEFORE ANY assertion, and read +16551: // through `find`/`map` rather than `expect` — an `expect` panic here +16552: // would preempt the harness and emit nothing. +16553: // --------------------------------------------------------------------- +16554: +16555: // [1] Spurious-order effect for the `CreateStaffGroup` op. M1 turns this +16556: // into an applied effect. +16557: let spurious_effect = out2 +16558: .state +16559: .effects +16560: .iter() +16561: .find(|(e, _)| *e == spurious_group_env_id) +16562: .map(|(_, eff)| eff.clone()); +16563: // [2] Spurious-order `StaffGroup.members` — `None` while pin 1 refuses +16564: // the mint outright. M1 makes it `Some([s])`: the spurious +16565: // membership that reached the graph. +16566: let spurious_members: Option> = out2 +16567: .score +16568: .staff_groups +16569: .iter() +16570: .find(|g| g.id == group_id2) +16571: .map(|g| g.members.clone()); +16572: // [3] Missing-order `StaffGroup.members` — `[s]` while pin 2 maintains +16573: // it. M2 leaves it empty. A DIFFERENT group in a DIFFERENT +16574: // reduction from [2]; one shared `members` local would satisfy this +16575: // harness while leaving one mutation's observation absent. +16576: let missing_members: Option> = out +16577: .score +16578: .staff_groups +16579: .iter() +16580: .find(|g| g.id == group_id) +16581: .map(|g| g.members.clone()); +16582: // [4] Missing-order invariant-21 verdict — the disagreement an +16583: // unmaintained projection leaves. Filtered from the missing-order +16584: // score; from the other reduction it would be the wrong verdict +16585: // rather than a missing one. +16586: let missing_agreement = epiphany_core::check_invariant( +16587: &out.score, +16588: epiphany_core::GraphInvariant::StaffGroupMembershipAgreement, +16589: ); +16590: +16591: let harness = format!( +16592: "\n [1] spurious-order CreateStaffGroup effect: {spurious_effect:?}\ +16593: \n [2] spurious-order g.members: {spurious_members:?}\ +16594: \n [3] missing-order g.members: {missing_members:?}\ +16595: \n [4] missing-order invariant-21 violations: {missing_agreement:?}" +16596: ); +16597: +16598: // ---- Missing order: the projection is maintained. -------------------- +16599: let missing_staff_group = out +16600: .score +16601: .staves +16602: .iter() +16603: .find(|s| s.id == staff_id) +16604: .map(|s| s.group); +16605: assert_eq!( +16606: missing_staff_group, +16607: Some(Some(group_id)), +16608: "missing order: s.group == Some(g) — the staff carries the sole \ +16609: authority{harness}" +16610: ); +16611: assert_eq!( +16612: missing_members.as_deref(), +16613: Some(&[staff_id][..]), +16614: "missing order: g.members is MAINTAINED to [s] (P13-S16 pin 2), not \ +16615: left empty as disposition B permitted{harness}" +16616: ); +16617: assert!( +16618: missing_agreement.is_empty(), +16619: "missing order: a maintained projection must leave invariant 21 \ +16620: clean{harness}" +16621: ); +16622: +16623: // ---- Spurious order: the mint is refused. --------------------------- +16624: assert_eq!( +16625: spurious_effect, +16626: Some(container_not_empty()), +16627: "spurious order: CreateStaffGroup carrying [s] must refuse \ +16628: ContainerNotEmpty (P13-S16 pin 1){harness}" +16629: ); +16630: assert_eq!( +16631: spurious_members, None, +16632: "spurious order: the refused mint must leave no group in the \ +16633: graph{harness}" +16634: ); +16635: let spurious_staff_group = out2 +16636: .score +16637: .staves +16638: .iter() +16639: .find(|s| s.id == staff_id2) +16640: .map(|s| s.group); +16641: assert_eq!( +16642: spurious_staff_group, +16643: Some(None), +16644: "spurious order: s.group stays None — CreateStaffGroup never writes \ +16645: Staff.group{harness}" +16646: ); +16647: } +``` + +[1],[2] from `out2` (spurious order, `group_id2`); [3],[4] from `out` (missing +order, `group_id`). Six assertions, six carry `{harness}`. Verdict: ok. + +## Item 2e — `m41` +```rust +6254: /// (m41) **Breaks S→G**: a staff whose `group` names a group whose `members` +6255: /// omit it — the shape a pin-2 maintenance gap produces. +6256: /// +6257: /// **Holds G→S**: `members` is empty, so that direction has nothing to +6258: /// disagree about. **Holds every other invariant**, which is what the exact +6259: /// cardinality assertion proves and what `any()` could never touch. +6260: /// +6261: /// **Mutation (M6a):** delete the `check_staff_names_absent_group` call from +6262: /// `check_invariants`. This fixture then goes **unreported** — the assertion +6263: /// prints `0` against `1` with an empty vector, which is the observation M6a +6264: /// owes, quoted rather than inferred. `m41b` must still pass. +6265: #[test] +6266: fn m41_check_invariants_dispatches_invariant_21_staff_names_absent_group() { +6267: let mut s = crate::generators::valid_score(4243); +6268: let replica = s.identity.replica_id; +6269: let group_id = StaffGroupId::new(replica, 21_001); +6270: s.staff_groups.push(StaffGroup { +6271: id: group_id, +6272: name: None, +6273: kind: StaffGroupKind::Bracket, +6274: members: Vec::new(), +6275: }); +6276: let staff_id = s.staves[0].id; +6277: s.staves[0].group = Some(group_id); +6278: +6279: // Bound before ANY assertion: the opposite-direction fact this fixture +6280: // depends on, then the violations. Nothing is asserted until the +6281: // cardinality check, which is the one M6a trips. +6282: let group_members: Option> = s +6283: .staff_groups +6284: .iter() +6285: .find(|group| group.id == group_id) +6286: .map(|group| group.members.clone()); +6287: let violations = check_invariants(&s); +6288: +6289: assert_eq!( +6290: violations.len(), +6291: 1, +6292: "expected exactly the invariant-21 S->G violation and nothing else, \ +6293: got {violations:?}" +6294: ); +6295: assert_eq!( +6296: violations[0].invariant, +6297: GraphInvariant::StaffGroupMembershipAgreement, +6298: "the single violation must be invariant 21, got {violations:?}" +6299: ); +6300: assert!( +6301: violations[0].witness.starts_with("S->G:"), +6302: "the witness must name the S->G direction so this test cannot pass \ +6303: on m41b's fixture, got {violations:?}" +6304: ); +6305: assert!( +6306: violations[0].witness.contains(&format!("{staff_id:?}")) +6307: && violations[0].witness.contains(&format!("{group_id:?}")), +6308: "the witness must name both the staff and the group id, got \ +6309: {violations:?}" +6310: ); +6311: // The G->S direction holds, asserted directly rather than left to follow +6312: // from the cardinality above: the group must genuinely list nobody, and +6313: // no G->S witness may be present. +6314: assert_eq!( +6315: group_members.as_deref(), +6316: Some(&[][..]), +6317: "fixture: the group must list nobody, so only S->G disagrees" +6318: ); +6319: assert!( +6320: !violations.iter().any(|v| v.witness.starts_with("G->S:")), +6321: "the G->S direction must hold on this fixture, got {violations:?}" +6322: ); +6323: } +``` + +## Item 2e — `m41b` +```rust +6325: /// (m41b) **Breaks G→S**: a group listing a staff whose own `group` is not +6326: /// that group — the shape a stale projection produces. +6327: /// +6328: /// **Holds S→G**: the listed staff's `group` is `None`, so it names no group +6329: /// and that direction abstains. **Holds every other invariant** — note the +6330: /// listed staff is genuinely declared, so this is a *disagreement*, not a +6331: /// dangling reference (invariant 21 abstains on those; invariant 10 owns +6332: /// them). +6333: /// +6334: /// **Mutation (M6b):** delete the `check_group_lists_unowned_staff` call from +6335: /// `check_invariants`. This fixture then goes unreported, printing `0` +6336: /// against `1`. **`m41b` is the ONLY test M6b breaks** — `m41`, the generator +6337: /// direction test and all four `all()` consumers use S→G fixtures, so +6338: /// without this test the G→S arm could be deleted and the suite would stay +6339: /// green. +6340: #[test] +6341: fn m41b_check_invariants_dispatches_invariant_21_group_lists_unowned_staff() { +6342: let mut s = crate::generators::valid_score(4244); +6343: let replica = s.identity.replica_id; +6344: let group_id = StaffGroupId::new(replica, 21_002); +6345: let staff_id = s.staves[0].id; +6346: s.staff_groups.push(StaffGroup { +6347: id: group_id, +6348: name: None, +6349: kind: StaffGroupKind::Bracket, +6350: members: vec![staff_id], +6351: }); +6352: +6353: // Bound before ANY assertion: the opposite-direction fact (`valid_score` +6354: // leaves every staff's `group` as `None`, which is what keeps S->G +6355: // abstaining), then the violations. This was asserted *before* the +6356: // binding in the first draft, which put a check ahead of the cardinality +6357: // assertion M6b trips — if the precondition ever broke, M6b's evidence +6358: // would be replaced by a fixture complaint. +6359: let listed_staff_group = s.staves[0].group; +6360: let violations = check_invariants(&s); +6361: +6362: assert_eq!( +6363: violations.len(), +6364: 1, +6365: "expected exactly the invariant-21 G->S violation and nothing else, \ +6366: got {violations:?}" +6367: ); +6368: assert_eq!( +6369: violations[0].invariant, +6370: GraphInvariant::StaffGroupMembershipAgreement, +6371: "the single violation must be invariant 21, got {violations:?}" +6372: ); +6373: assert!( +6374: violations[0].witness.starts_with("G->S:"), +6375: "the witness must name the G->S direction so this test cannot pass \ +6376: on m41's fixture, got {violations:?}" +6377: ); +6378: assert!( +6379: violations[0].witness.contains(&format!("{staff_id:?}")) +6380: && violations[0].witness.contains(&format!("{group_id:?}")), +6381: "the witness must name both the staff and the group id, got \ +6382: {violations:?}" +6383: ); +6384: // The S->G direction holds, asserted directly: the listed staff must name +6385: // no group at all, and no S->G witness may be present. Without the first +6386: // of these the fixture could silently become a both-directions one, which +6387: // would be reported after EITHER arm was deleted and so would sign +6388: // neither. +6389: assert_eq!( +6390: listed_staff_group, None, +6391: "fixture: the listed staff must name no group, so only G->S disagrees" +6392: ); +6393: assert!( +6394: !violations.iter().any(|v| v.witness.starts_with("S->G:")), +6395: "the S->G direction must hold on this fixture, got {violations:?}" +6396: ); +6397: } +``` + +## Items 2d/2e — generator test, both legs +```rust +1023: /// **P13-S16 touch row 8.** `violating_score`'s invariant-21 arm breaks the +1024: /// **S→G** direction ONLY — in the raw fixture **and after shrinking**. +1025: /// +1026: /// Invariant 21's two directions carry the same `GraphInvariant`, so every +1027: /// `all()`-driven test in this module is satisfied by either one and **none +1028: /// can observe which**. This is the only guard on the generator's direction, +1029: /// and `m41b` is the only permanent guard on the other direction being +1030: /// dispatched at all. +1031: /// +1032: /// **The shrunk leg is not redundant.** `shrink` rebuilds the witness, and +1033: /// nothing in its contract preserves *which way* the pair disagrees: a shrink +1034: /// that cleared the staff's `group` while leaving it listed in `members` +1035: /// would flip the direction, still violate invariant 21, and satisfy +1036: /// `every_invariant_shrinks_to_a_small_witness` and `shrink_is_idempotent` +1037: /// alike. +1038: /// +1039: /// **Mutation (M6a):** delete the `check_staff_names_absent_group` call from +1040: /// `check_invariants`; both legs report nothing and the cardinality +1041: /// assertions print `0` against `1`. Under **M6b** — deleting the G→S arm — +1042: /// this test must **pass**, and that asymmetry is the direction claim. +1043: #[test] +1044: fn invariant_21_negative_generator_breaks_staff_to_group_only() { +1045: let inv = GraphInvariant::StaffGroupMembershipAgreement; +1046: +1047: // The two legs are built and checked SEQUENTIALLY, and the raw leg is +1048: // fully validated before `shrink` is ever called. +1049: // +1050: // Building both in one array would evaluate `shrink` first — Rust +1051: // constructs every element before the loop body runs — and `shrink` +1052: // opens with `assert!(!check_invariant(score, inv).is_empty())`. Under +1053: // M6a that check returns empty, so shrink PANICS on its own entry +1054: // assertion before the raw leg's cardinality assertion executes, and M6a +1055: // would report "shrink starting point must violate the target invariant" +1056: // instead of the pinned `0` against `1`. **A panic upstream of the +1057: // pinned assertion destroys the evidence the mutation owes.** +1058: let raw = violating_score(inv, 0x2121_2121); +1059: assert_breaks_staff_to_group_only("raw", &raw, inv); +1060: +1061: let shrunk = shrink(&raw, inv); +1062: assert_breaks_staff_to_group_only("shrunk", &shrunk, inv); +1063: } +``` + +```rust +1065: /// Pin 6a's three properties for one leg of +1066: /// `invariant_21_negative_generator_breaks_staff_to_group_only`: exact +1067: /// cardinality, the S→G witness naming both ids, and the G→S direction +1068: /// holding — each asserted rather than implied. +1069: fn assert_breaks_staff_to_group_only(leg: &str, s: &Score, inv: GraphInvariant) { +1070: // Bound before any assertion, and read from the score so both legs +1071: // survive shrinking rather than hardcoding the generator's counter. The +1072: // ids are formatted here so this helper needs no extra id imports; the +1073: // named group's `members` is carried as a value because the G->S claim +1074: // must be checked against the FIXTURE, not against the checker's output. +1075: let named = s.staves.iter().find_map(|staff| { +1076: staff.group.map(|group| { +1077: let members = s +1078: .staff_groups +1079: .iter() +1080: .find(|candidate| candidate.id == group) +1081: .map(|candidate| candidate.members.clone()); +1082: (format!("{:?}", staff.id), format!("{group:?}"), members) +1083: }) +1084: }); +1085: let violations = check_invariants(s); +1086: +1087: // First, because it is the assertion M6a trips. +1088: assert_eq!( +1089: violations.len(), +1090: 1, +1091: "{leg}: expected exactly the invariant-21 S->G violation and nothing \ +1092: else, got {violations:?}" +1093: ); +1094: assert_eq!( +1095: violations[0].invariant, inv, +1096: "{leg}: the single violation must be invariant 21, got {violations:?}" +1097: ); +1098: assert!( +1099: violations[0].witness.starts_with("S->G:"), +1100: "{leg}: the generator must break the S->G direction only — a flipped \ +1101: direction still violates invariant 21 and no other test would \ +1102: notice; got {violations:?}" +1103: ); +1104: let (staff_id, group_id, group_members) = named.unwrap_or_else(|| { +1105: panic!("{leg}: the fixture must have a staff naming a group; got {violations:?}") +1106: }); +1107: assert!( +1108: violations[0].witness.contains(&staff_id) && violations[0].witness.contains(&group_id), +1109: "{leg}: the witness must name both {staff_id} and {group_id}, got \ +1110: {violations:?}" +1111: ); +1112: // The opposite direction holds, asserted against the FIXTURE. Checking +1113: // only that no `G->S:` witness was emitted would pass **vacuously under +1114: // M6b**: with the G->S arm deleted no such witness can appear whatever the +1115: // fixture holds, so a flipped or both-directions fixture would slip +1116: // through the leg that is supposed to guarantee the direction. The empty +1117: // `members` is the checker-independent fact, and `m41` asserts it the +1118: // same way. +1119: assert_eq!( +1120: group_members.as_deref(), +1121: Some(&[][..]), +1122: "{leg}: fixture — group {group_id} must list nobody, so nothing can \ +1123: disagree G->S; got {group_members:?}" +1124: ); +1125: assert!( +1126: !violations.iter().any(|v| v.witness.starts_with("G->S:")), +1127: "{leg}: the G->S direction must hold, got {violations:?}" +1128: ); +1129: } +``` diff --git a/spec/HANDOFF_2026-08-07.md b/spec/HANDOFF_2026-08-07.md index 5b79a17..78950ec 100644 --- a/spec/HANDOFF_2026-08-07.md +++ b/spec/HANDOFF_2026-08-07.md @@ -31,13 +31,15 @@ unpushed commits on any branch. > landed.)* **A base materialized before S16 declares `0` and must be rebuilt, not > reused.** > -> **P13-S16 also left six findings against its own contract** — see the `EXECUTED` -> append on its `spec/PASS13_CANDIDATES.md` row, and -> `spec/EVIDENCE_P13S16_EXECUTION.md` (untracked review artifact) for the runs behind -> them. The two that bite hardest elsewhere: `cargo test --workspace` **truncates the -> failure set** at the first failing suite, so mutation work needs `--no-fail-fast`; -> and invariant 21 **abstains on dangling membership**, which is invariant 10's -> concern, so it is not the detector for the undo hole §0.6 attributed to it. +> **P13-S16's corrections against its own contract are amended in at +> `spec/CONTRACT_P13S16_PROJECTION.md` §7**, with `spec/EVIDENCE_P13S16_EXECUTION.md` +> holding the runs behind them. *(Execution reported six; §7's own review withdrew one as +> false — pin 8's line numbers were exact on the ratified tree and only stopped matching +> because this rung inserted lines above them.)* The two that bite hardest elsewhere: +> `cargo test --workspace` **truncates the failure set** at the first failing suite, so +> mutation work needs `--no-fail-fast`; and invariant 21 **abstains on dangling +> membership**, which is invariant 10's concern, so it is not the detector for the undo +> hole §0.6 attributed to it. **Scope.** Written from the **spec / Pass-13 / format-epoch** session. A second session has been committing to this repository in parallel on the **editor / diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index 5428d5a..aa6469a 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 — 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`. **Blocking chain, 2026-07-31: S16 → P13-S27 → P13-S28.** S16 does **not** become dispatchable when S27 lands; it additionally needs S27's pin-2a legacy-base disposition, which S28 owns. **UNBLOCKED 2026-08-09 — P13-S27 landed and was accepted at `4df8e25`.** The preceding sentence is **superseded**: pin 2a's legacy-base disposition was settled from *outside* S27, by the format-epoch rung's pin 8 (legacy bases are refused by container epoch, never by version arithmetic), so the extra condition it names no longer exists — S27's pin 10 was amended in review round 12 for exactly this reason. **An authority now exists** (`epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION`, currently `0`) and a stale base is refused with `CanonicalBaseRequiresRebuild` on both the read and write paths, so pin 0's blocker is discharged. **UNBLOCKED IS NOT DISPATCHABLE:** `spec/CONTRACT_P13S16_PROJECTION.md` is a **DRAFT** and has not been through adversarial review; it needs ratification before dispatch, and its pin 11 was amended the same day since it mandated a ledger state ("blocked on P13-S27") that had become false. **RATIFIED 2026-08-09 at `25b4925`, on the authority of the repository owner, after twelve independent whole-artifact rounds — the last returning zero findings; the preceding sentence's "has not been through adversarial review" is superseded.** **PINS FROZEN**: executed, not edited; a defect found during execution is reported as its own amendment with its own review round. **DISPATCHABLE but NOT DISPATCHED — nothing is implemented, so this row does NOT move to RESOLVED.** 32 findings closed before ratification (19 in draft amendment 1 and revisions A–J, 13 across rounds 1–11); **none was in the pins' substance** — the maintenance rule, the refusal, invariant 21, the undo strip and the authority bump have been stable since draft amendment 1, and every finding was in the evidence apparatus. Two cells of §3's expected-outcome table (`t8d` under M2, `t9` under M1) are **predictions to be falsified at execution**, and §4a's landing obligation is outstanding by construction. **This rung's first act is bumping the authority to `1`**, because it changes `CreateStaffGroup`'s reduction verdict **EXECUTED 2026-08-09 — implementation complete and left in the worktree for review; NOTHING IS STAGED and nothing is accepted, so this row does NOT move to RESOLVED.** The refusal reuses **`ContainerNotEmpty`** (discriminant 10); a new `PreconditionFailureReason` was considered and proved **unnecessary** — the existing reason describes exactly this precondition, and adding one would move the accept set for no gain. The **base-ingest hazard** is closed by seeding `staff_group_values` with `members` emptied in `seed_from_graph`: a `group.clone()` there launders the *derived* value into the carried slot, so the re-carry misverdicts `RecreateContentMismatch` only **after a reload**, and `t8d` is the only test that crosses that boundary. **`t8b` inverted** to `t8b_the_projection_is_maintained_and_the_spurious_form_is_refused`, keeping both authoring orders with the verdicts reversed. **`t6`/`t7`/`t9` revised**: `t6`'s `CreateStaffGroup` arm now expects `ContainerNotEmpty` and no longer tests a referential loop; `t7`'s arm **inverts**, because an empty-container precondition asks only about the carried value and therefore refuses base-free too; `t9`'s group carries `[]` and its mutation set shrinks from three loop-drops to two. **The authority is now `1`** — the 'currently `0`' above is superseded — and **per pin 0 any canonical base materialized before this rung MUST be rebuilt, not reused**, since it holds state these semantics would not have computed; `open` and `commit` both refuse it with `CanonicalBaseRequiresRebuild`. **Execution reported four findings against the contract rather than patching pins:** (i) §0.6, pin 5a and pin 6b attribute the undo residue to invariant 21, which **abstains** on dangling members — M5 observed invariant 10 `CrossCuttingRefsResolve` firing instead, so that hole was already covered and `u5`'s direct members assertion is what signs pin 5; (ii) §3's M6a row names **six** failing tests where the observed set is **seven**, because its four-`all()`-consumer list omits `crates/epiphany-core/tests/score_graph.rs:146`; (iii) pin 10 cites **four of the nine** sites its instruction covers — eight carrying disposition-B semantics, plus `core_spec.tex`'s 'exactly 20 invariants' count sentence, which is not disposition-B prose and which gate 6 cannot see because it checks only that the enumeration ends at 21; (iv) `cargo test --workspace` **truncates** the failure set at the first failing suite, so every mutation run needs `--no-fail-fast` to produce the complete set §3 requires **ACCEPTED AND LANDED 2026-08-10 at `aee4ff9`, on the authority of the repository owner, after nineteen independent review rounds during execution.** The `EXECUTED … NOTHING IS STAGED` sentence above is **superseded**: the fourteen touch-table paths are committed and the working tree is clean. **RESOLVED — IMPLEMENTED 2026-08-10 (`aee4ff9`).** The rung's six findings against its own contract stand unamended and are the outstanding follow-up: (i) invariant 21's dangling abstention vs the undo-hole attribution in §0.6, pin 5a and pin 6b; (ii) §3's M6a row naming six failing tests where seven are observed; (iii) §3's `t8d`-under-M2 survivor cell, falsified — it fails on non-vacuity, not idempotence; (iv) pin 10 citing four of the nine sites its instruction covers; (v) `cargo test --workspace` truncating the failure set without `--no-fail-fast`; (vi) pin 8's drifted line numbers. **`spec/EVIDENCE_P13S16_EXECUTION.md` holds the verbatim runs behind all of it** — deliberately untracked, since no touch row covers it. `CLAUDE.md` and `spec/HANDOFF_2026-08-07.md` were reconciled in a separate commit after acceptance, per §4a | +| 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`. **Blocking chain, 2026-07-31: S16 → P13-S27 → P13-S28.** S16 does **not** become dispatchable when S27 lands; it additionally needs S27's pin-2a legacy-base disposition, which S28 owns. **UNBLOCKED 2026-08-09 — P13-S27 landed and was accepted at `4df8e25`.** The preceding sentence is **superseded**: pin 2a's legacy-base disposition was settled from *outside* S27, by the format-epoch rung's pin 8 (legacy bases are refused by container epoch, never by version arithmetic), so the extra condition it names no longer exists — S27's pin 10 was amended in review round 12 for exactly this reason. **An authority now exists** (`epiphany_ops::CURRENT_REDUCTION_ALGORITHM_VERSION`, currently `0`) and a stale base is refused with `CanonicalBaseRequiresRebuild` on both the read and write paths, so pin 0's blocker is discharged. **UNBLOCKED IS NOT DISPATCHABLE:** `spec/CONTRACT_P13S16_PROJECTION.md` is a **DRAFT** and has not been through adversarial review; it needs ratification before dispatch, and its pin 11 was amended the same day since it mandated a ledger state ("blocked on P13-S27") that had become false. **RATIFIED 2026-08-09 at `25b4925`, on the authority of the repository owner, after twelve independent whole-artifact rounds — the last returning zero findings; the preceding sentence's "has not been through adversarial review" is superseded.** **PINS FROZEN**: executed, not edited; a defect found during execution is reported as its own amendment with its own review round. **DISPATCHABLE but NOT DISPATCHED — nothing is implemented, so this row does NOT move to RESOLVED.** 32 findings closed before ratification (19 in draft amendment 1 and revisions A–J, 13 across rounds 1–11); **none was in the pins' substance** — the maintenance rule, the refusal, invariant 21, the undo strip and the authority bump have been stable since draft amendment 1, and every finding was in the evidence apparatus. Two cells of §3's expected-outcome table (`t8d` under M2, `t9` under M1) are **predictions to be falsified at execution**, and §4a's landing obligation is outstanding by construction. **This rung's first act is bumping the authority to `1`**, because it changes `CreateStaffGroup`'s reduction verdict **EXECUTED 2026-08-09 — implementation complete and left in the worktree for review; NOTHING IS STAGED and nothing is accepted, so this row does NOT move to RESOLVED.** The refusal reuses **`ContainerNotEmpty`** (discriminant 10); a new `PreconditionFailureReason` was considered and proved **unnecessary** — the existing reason describes exactly this precondition, and adding one would move the accept set for no gain. The **base-ingest hazard** is closed by seeding `staff_group_values` with `members` emptied in `seed_from_graph`: a `group.clone()` there launders the *derived* value into the carried slot, so the re-carry misverdicts `RecreateContentMismatch` only **after a reload**, and `t8d` is the only test that crosses that boundary. **`t8b` inverted** to `t8b_the_projection_is_maintained_and_the_spurious_form_is_refused`, keeping both authoring orders with the verdicts reversed. **`t6`/`t7`/`t9` revised**: `t6`'s `CreateStaffGroup` arm now expects `ContainerNotEmpty` and no longer tests a referential loop; `t7`'s arm **inverts**, because an empty-container precondition asks only about the carried value and therefore refuses base-free too; `t9`'s group carries `[]` and its mutation set shrinks from three loop-drops to two. **The authority is now `1`** — the 'currently `0`' above is superseded — and **per pin 0 any canonical base materialized before this rung MUST be rebuilt, not reused**, since it holds state these semantics would not have computed; `open` and `commit` both refuse it with `CanonicalBaseRequiresRebuild`. **Execution reported four findings against the contract rather than patching pins:** (i) §0.6, pin 5a and pin 6b attribute the undo residue to invariant 21, which **abstains** on dangling members — M5 observed invariant 10 `CrossCuttingRefsResolve` firing instead, so that hole was already covered and `u5`'s direct members assertion is what signs pin 5; (ii) §3's M6a row names **six** failing tests where the observed set is **seven**, because its four-`all()`-consumer list omits `crates/epiphany-core/tests/score_graph.rs:146`; (iii) pin 10 cites **four of the nine** sites its instruction covers — eight carrying disposition-B semantics, plus `core_spec.tex`'s 'exactly 20 invariants' count sentence, which is not disposition-B prose and which gate 6 cannot see because it checks only that the enumeration ends at 21; (iv) `cargo test --workspace` **truncates** the failure set at the first failing suite, so every mutation run needs `--no-fail-fast` to produce the complete set §3 requires **ACCEPTED AND LANDED 2026-08-10 at `aee4ff9`, on the authority of the repository owner, after nineteen independent review rounds during execution.** The `EXECUTED … NOTHING IS STAGED` sentence above is **superseded**: the fourteen touch-table paths are committed and the working tree is clean. **RESOLVED — IMPLEMENTED 2026-08-10 (`aee4ff9`).** The rung's six findings against its own contract stand unamended and are the outstanding follow-up: (i) invariant 21's dangling abstention vs the undo-hole attribution in §0.6, pin 5a and pin 6b; (ii) §3's M6a row naming six failing tests where seven are observed; (iii) §3's `t8d`-under-M2 survivor cell, falsified — it fails on non-vacuity, not idempotence; (iv) pin 10 citing four of the nine sites its instruction covers; (v) `cargo test --workspace` truncating the failure set without `--no-fail-fast`; (vi) pin 8's drifted line numbers. **`spec/EVIDENCE_P13S16_EXECUTION.md` holds the verbatim runs behind all of it** — deliberately untracked, since no touch row covers it. `CLAUDE.md` and `spec/HANDOFF_2026-08-07.md` were reconciled in a separate commit after acceptance, per §4a **AMENDED 2026-08-10: the six findings are now carried in `spec/CONTRACT_P13S16_PROJECTION.md` §7 as one consolidated post-landing amendment, and reviewing them there WITHDREW finding (vi) as false.** Pin 8's line numbers were **exact** on the ratified tree `34232dc` — all four verified — and only stopped matching because this rung inserted ~1,500 lines above them; that is a contract describing the tree it was written against, not a defect. The claim had been reported without ever measuring the cited locations. **Five findings stand**, and §7 groups them by two shared root causes: reasoning about mechanism where the question was what the test asserts (findings 1 and 3), and enumerating where completeness required deriving (findings 2 and 4). **Touch row 12 was added** so `spec/EVIDENCE_P13S16_EXECUTION.md` can be committed rather than left untracked | | 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 |