From cc49533c76d9c6d0ef60765b3f833ccca3596fad Mon Sep 17 00:00:00 2001 From: Levi Neuwirth Date: Thu, 30 Jul 2026 21:38:15 -0400 Subject: [PATCH] P13-S22: the fragment count follows the inventory it describes Adding Registered = 16 made the inventory six fragments -- 24-29, 34, 35-38, 39, 16, and 1 -- but the repair sentence still said "superseding the five scattered fragments rather than adding a sixth". The count was right when written and went stale in the same commit that lengthened the list it counts, which is the entry's own subject matter arriving one row early. Ledger-only. No code, wire, or specification change. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01QjsEnYhm1gPpf6ii2iFxFV --- spec/PASS13_CANDIDATES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/PASS13_CANDIDATES.md b/spec/PASS13_CANDIDATES.md index f33b4b3..c06bc8e 100644 --- a/spec/PASS13_CANDIDATES.md +++ b/spec/PASS13_CANDIDATES.md @@ -99,4 +99,4 @@ visible — a value with a wire form and no canonical carrier to reach it.) | P13-S19 | **`CreateMeasure`'s ordering and boundary-distance preconditions are vacuous for an instance's first measure, so pickup/anacrusis measures are unauthored by this rung.** Genesis tranche G3b (`spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9) makes clauses 1 and 3 of `create_measure`'s append-only discipline vacuous when there is no predecessor measure, and invariant 20's boundary clause is symmetrically exempt for a first measure (core specification, invariant 20's doc comment) — a partial first measure MUST NOT be refused or flagged by either. This is a scoped deferral, not an oversight: a pickup measure's *own* internal consistency (its declared duration against its content) is a decomposition-sum question, not a measure-to-measure boundary question, and modelling it correctly needs a notion of "partial measure" this rung does not introduce | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` pin 9 (filed 2026-07-30 during the G3b contract's own drafting) | **open, deliberately.** A pickup/anacrusis authoring story — whatever shape it takes — is later schema-fill work, sequenced after the genesis ladder closes | | P13-S20 | **`decode.rs`'s `precondition_reason` decoder stopped at discriminant 13, so `PreconditionFailureReason` 14 (`AcousticRealizationPinned`) and 15 (`TranspositionOutOfRange`), both live since Push 4a, encoded but could not decode.** A materialized effect carrying either reason failed canonical round-trip in production code, undetected because `epiphany-testkit`'s `precondition_failure_reason` generator (`generators.rs:417`, then `rng.below(14)`) never drew past 13 despite its doc comment claiming "every core and registered variant" | `spec/CONTRACT_GENESIS_G3B_MEASURE.md` §0 / touch-table row 12a (found 2026-07-30 during the G3b contract's own drafting, verified against the working tree: `decode.rs:205`ff ended at 13, `generators.rs:417` drew `below(14)`) | **RESOLVED in this rung** (genesis tranche G3b packet 1, `e64a4b7`). `decode.rs`'s `precondition_reason` now decodes discriminants 14 through 18 (the pre-existing 14/15 hole plus G3b's own 16–18), and `generators.rs`'s `precondition_failure_reason` now draws `below(19)` with arms for all of them — the generator's doc comment claim is true again, and the decode hole this rung found already latent in the tree, not introduced by it, is closed alongside G3b's own additions | | P13-S21 | **The wire specification never documented `PreconditionFailureReason` 14 and 15, so the decoder hole P13-S20 repaired had no normative text to be measured against.** `binary_format.tex`'s bounded reason table (`\sectionsc{Bounded Enumerations}`) ran `\tablenums{13}` straight to G3b's `\tablenums{16}`, and Push 4a's own Revision History row recorded only `OperationKind` `\tablenums{30}` (`TransposeInterval`) while saying nothing about the two reasons it appended in the same epoch. `AcousticRealizationPinned` and `TranspositionOutOfRange` appeared **nowhere** in the document, though the Operation Catalog documented both at 0.8.0 and `effect.rs` has carried both since Push 4a. This is P13-S20's specification-side twin: the same two variants, the same silence, and the reason a decoder that stopped at 13 could sit in the tree unchallenged — a conforming implementer reading only the wire specification would have built exactly that decoder and been right | Found 2026-07-30 while verifying genesis tranche G3b packet 3b (`d58eee8`), whose touch-table row 28 scoped the reason table to discriminants 16–18 only; the executing agent correctly declined to widen scope and reported the gap instead | **RESOLVED in this rung** (the G3b pre-push repair). The bounded table gains `\tablenums{14}` and `\tablenums{15}` with their refusal conditions, and Push 4a's Revision History row is amended to record both appends in its own epoch — no version bump and no new history row, because this documents an assignment that has been normative since Push 4a rather than making one. `binary_format_history.rs` gains a bounded regression test requiring both names in the reason table **and** in Push 4a's own row segment, so neither the G3b row's prose nor the Operation Catalog's coverage can satisfy it | -| P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 24–29 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 35–38 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 2–15, 17–23, and 30–33 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548`–`:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental** — `ops/src/vectors.rs:201`–`:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the five scattered fragments rather than adding a sixth — a sixth band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** | +| P13-S22 | **`OperationKindTag`'s normative tag-to-byte mapping is asserted for a minority of the vocabulary; the rest is defended only incidentally, by frozen byte artifacts that cannot say what broke.** P13-S15 closed the `OperationKind` half with one table covering 0..=39. The tag half has no equivalent. **Semantic locks — a named tag bound to a literal byte — exist only for:** 24–29 (`phase3_tag_discriminants_are_golden`, `payload.rs:2728`), 34 (one assertion inside a G2b reduction test, `reduce.rs:12744`), 35–38 (`t1_g3a_kinds_and_tags_are_35_to_38_in_both_spaces`, `reduce.rs:15931`), 39 (`payload.rs:2936`); **16** (`Registered`, whose corpus row is emitted under its *variant* name at `ops/src/vectors.rs:210` and whose committed literal leads with `0x10` at `spec/vectors/decode_vectors.txt:80`, so the drift comparison binds the association); and — incidentally — 1, spelled in a comment inside a golden blob (`barrier.rs:1058`, *"len 1, DeleteEvent (tag 1)"*). **Tags 0, 2–15, 17–23, and 30–33 have no semantic lock at all.** The derived tests do not supply one: `the_tag_vocabulary_is_complete` (`payload.rs:2652`) proves **completeness, density, and round-trip** — that the payload-free discriminants are exactly `0..unknown` with no gaps and each decodes — which constrains the *shape* of the assignment, not *which tag holds which byte*, and `operation_kind_tag_vocabulary!` guarantees coverage rather than value. **What actually catches a permutation is byte-level goldens that embed the tag by accident**, and they diagnose it as a blob mismatch: three probes, three catches, none of them naming a tag (below) | this file (found 2026-07-30 while closing P13-S15, whose kind-side extension made the asymmetry visible; **the entry was rewritten the same day after its own probes falsified its first draft.** That draft claimed a permutation was invisible and named 32↔33 as the demonstration. Three permutations were then executed against the working tree at `dcb28f0` and **all three failed**, so the claim was wrong and the severity is lower than filed: 32↔33 (`SetCanvasLayoutDefaults`/`SetSpellingPrecedence`) → caught by `the_committed_corpus_matches_the_generator` (`testkit/src/vectors.rs:225`); 1↔2 (`DeleteEvent`/`ModifyEvent`) → caught by `edit_barriers_blob_bytes_are_golden` (`layout-ir/src/barrier.rs:1061`); 2↔3 (`ModifyEvent`/`RespellPitch`) → caught by the corpus again. Each mutation was restored by hand and the suite returned to 1541/0) | **open.** **Not a live incorrectness, and — corrected — not an undefended one either:** every tag discriminant is currently correct, `binary_format.tex:1548`–`:1552` carries the mapping normatively, and no probe escaped. **The gap is intent and diagnosis, not exposure.** A permutation fails as *"the committed corpus does not match the generator"* or *"blob bytes are not golden"* — artifacts that regenerate, and whose failure reads as corpus drift rather than as a moved wire discriminant. **The corpus's tag coverage is deliberate, not accidental** — `ops/src/vectors.rs:201`–`:204` emits one row per tag straight from the vocabulary and names the reason: *"A hand-picked subset is how `TransposeInterval` shipped encoding to a byte its own decoder rejected: the corpus never named it."* **But those rows lock byte→byte, not variant→byte.** Each is named `tag_{discriminant}` and carries `[discriminant]`, both derived from the value alone, so `tag_32` asserts that `0x20` round-trips — never that `SetCanvasLayoutDefaults` is 32. Every one of the 40 rows is identical under a permutation; what actually moves is their **order**, since `PAYLOAD_FREE` is declaration order. That is why the 32↔33 probe failed, and it is exactly the property `Registered`'s row has and the numbered rows do not — its row is named for the variant. **The gap is that one row's discipline is not the vocabulary's.** **Likely shape of the repair:** one table over the whole tag vocabulary asserting tag → byte directly, superseding the six scattered fragments rather than adding a seventh — a seventh band is how this got here — so that moving a tag fails by *name*. **Probe design note for whoever takes this:** do not reuse 32↔33 or 1↔2; both are now known to be caught, and a probe that fails proves the lock exists, not that it is missing. The mutation that would sign this rung is the **inverse**: delete the proposed table and show that some permutation then passes, or show the surviving failure names no tag. **Its own rung, not a rider** |